Reversible computation in term rewriting

DOI10.1016/J.JLAMP.2017.10.003MaRDI QIDQ1683707zbMATH OpenOpenAlexWikidataFDO

Authors Naoki Nishida, Adrián Palacios, Germán Vidal

Publication date 1 December 2017

Published in Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1710.02804, http://hdl.handle.net/10251/121738

zbMATH Keywords

reversible computationterm rewritingprogram transformation

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Grammars and rewriting systems (68Q42)

Abstract: Essentially, in a reversible programming language, for each forward computation from state $S$ to state $S^{\prime }$, there exists a constructive method to go backwards from state $S^{\prime }$ to state $S$. Besides its theoretical interest, reversible computation is a fundamental concept which is relevant in many different areas like cellular automata, bidirectional program transformation, or quantum computing, to name a few. In this work, we focus on term rewriting, a computation model that underlies most rule-based programming languages. In general, term rewriting is not reversible, even for injective functions; namely, given a rewrite step $t_{1}ightarrow{t}_2$, we do not always have a decidable method to get $t_1$ from $t_2$. Here, we introduce a conservative extension of term rewriting that becomes reversible. Furthermore, we also define two transformations, injectivization and inversion, to make a rewrite system reversible using standard term rewriting. We illustrate the usefulness of our transformations in the context of bidirectional program transformation.

Recommendations

• Reversible term rewriting
• A reversible semantics for Erlang
• Reversible computation in nets with bonds
• A theory of reversibility for Erlang
• Reversible Programs Have Reversible Semantics

Cites work

• scientific article; zbMATH DE number 1889386 (Why is no real title available?)
• A structural approach to reversible computation
• Automated Complexity Analysis Based on the Dependency Pair Method
• Automatic Partial Inversion of Inductively Sequential Functions
• Bidirectionalization transformation based on automatic derivation of view complement functions
• Completeness results for basic narrowing
• Computation and construction universality of reversible cellular automata
• Computation in reversible cellular automata
• Conditional rewrite rules: Confluence and termination
• Determinization of conditional term rewriting systems
• Fundamental approaches to software engineering. 17th international conference, FASE 2014, held as part of the European joint conferences on theory and practice of software, ETAPS 2014, Grenoble, France, April 5--13, 2014, Proceedings
• Fundamentals of reversible flowchart languages
• Irreversibility and Heat Generation in the Computing Process
• Logical Reversibility of Computation
• Mathematics of Program Construction
• Program inversion for tail recursive functions
• Reachability analysis of innermost rewriting
• Reachability in conditional term rewriting systems
• Reverse code generation for parallel discrete event simulation
• Reversible Flowchart Languages and the Structured Reversible Program Theorem
• Reversible combinatory logic
• Reversible simulation of one-dimensional irreversible cellular automata
• Reversible simulation of space-bounded computations
• Reversible term rewriting
• Soundness of unravelings for conditional term rewriting systems via ultra-properties related to linearity
• Update semantics of relational views

Cited in

(16)

• A reversible semantics for Erlang
• Tail recursion transformation for invertible functions
• Towards a taxonomy for reversible computation approaches
• Semi-inversion of conditional constructor term rewriting systems
• Reversible term rewriting
• A structural approach to reversible computation
• Reversible computing from a programming language perspective
• Narrowing trees for syntactically deterministic conditional term rewriting systems
• Describing and Optimising Reversible Logic Using a Functional Language
• Reversible combinatory logic
• scientific article; zbMATH DE number 7447776 (Why is no real title available?)
• Reversibility in space-bounded computation
• Reversify any sequential algorithm
• Controlled reversibility in communicating reaction systems
• A theory of reversibility for Erlang
• Characterizing Compatible View Updates in Syntactic Bidirectionalization

This page was built for publication: Reversible computation in term rewriting

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1683707)