@article{oai:nagoya.repo.nii.ac.jp:00025691,
 author = {Nishida, Naoki and Palacios, Adrián and Vidal, Germán},
 journal = {Journal of Logical and Algebraic Methods in Programming},
 month = {Jan},
 note = {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},
 pages = {128--149},
 title = {Reversible computation in term rewriting},
 volume = {94},
 year = {2018}
}