2024-03-28T21:36:45Z
https://nagoya.repo.nii.ac.jp/oai
oai:nagoya.repo.nii.ac.jp:00025691
2023-01-16T04:15:25Z
312:313:314
Reversible computation in term rewriting
Nishida, Naoki
76074
Palacios, Adrián
76075
Vidal, Germán
76076
Term rewriting
Reversible computation
Program transformation
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.
ファイル公開:2020-01-01
journal article
Elsevier
2018-01
application/pdf
Journal of Logical and Algebraic Methods in Programming
94
128
149
23522208
https://nagoya.repo.nii.ac.jp/record/25691/files/paper_NPV17_jlamp_preprint.pdf
eng
https://doi.org/10.1016/j.jlamp.2017.10.003
© 2018. This manuscript version is made available under the CC-BY-NC-ND 4.0 license http://creativecommons.org/licenses/by-nc-nd/4.0/