2026-08-18T23:34:08Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:5984 2024-03-06T10:37:26Z ddc:004 open_access

Reversible Term Rewriting Nishida, Naoki Palacios, Adrián Vidal, Germán term rewriting reversible computation program transformation Essentially, in a reversible programming language, for each forward computation step from state S to state S', there exists a constructive and deterministic method to go backwards from state S' 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 paper, 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 t1 -> t2, we do not always have a decidable and deterministic method to get t1 from t2. Here, we introduce a conservative extension of term rewriting that becomes reversible. Furthermore, we also define a transformation to make a rewrite system reversible using standard term rewriting. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Naoki Nishida and Adrián Palacios and Germán Vidal 2016 Is Part Of LIPIcs, Volume 52, 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2016.28 urn:nbn:de:0030-drops-59841 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.28 eng https://creativecommons.org/licenses/by/3.0/legalcode