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.
This paper has been published in Naoki Nishida, Adrián Palacios, Germán Vidal. Reversible Term Rewriting. In Delia Kesner and Brigitte Pientka, editors, Proceedings of the First International Conference on Formal Structures for Computation and Deduction, FSCD 2016, June 22-26, 2016,
Porto, Portugal. LIPIcs 52, 28:1–28:18, Schloss Dagstuhl – Leibniz-Zentrum fuer Informatik, 2016.