2017/10/08 by Naoki Nishida, Adrián Palacios, Nishida, Naoki +3
Computer Science · #Cellular Automata and Applications #Computability, Logic, AI Algorithms #FOS: Computer and information sciences #Programming Languages (cs.PL) #Quantum Computing Algorithms and Architecture #cs.PL
paper · pdf · doi:10.48550/arxiv.1710.02804
To appear in the Journal of Logical and Algebraic Methods in Programming
arxiv created 2017/10/08 · openalex publication_date 2017/10/08 · arxiv updated 2017/10/10 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Essentially, in a reversible programming language, for each forward computation from state S to state S', there exists a constructive 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 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 t1 → t2, we do not always have a decidable method to get t1 from t2. 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.