Reversible computation in term rewriting

[EN] 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 t(1) -> t(2), we do not always have a decidable method to get t(1) from t(2). 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. (C) 2017 Elsevier Inc. All rights reserved.This work has been partially supported by the EU (FEDER) and the Spanish Ministerio de Economia y Competitividad (MINECO) under grants TIN2013-44742-C4-1-R and TIN2016-76843-C4-1-R, by the Generalitat Valenciana under grant PROMETE0-II/2015/013 (SmartLogic), and by the COST Action IC1405 on Reversible Computation extending horizons of computing. Adrian Palacios was partially supported by the EU (FEDER) and the Spanish Ayudas para contratos predoctorales para la formacian de doctores and Ayudas a la movilidad predoctoral para la realizacion de estancias breves en centros de I+D, MINECO (SEIDI), under FPI grants BES-2014-069749 and EEBB-I-16-11469. Part of this research was done while the second and third authors were visiting Nagoya University; they gratefully acknowledge their hospitality.Nishida, N.; Palacios, A.; Vidal, G. (2018). Reversible computation in term rewriting. Journal of Logical and Algebraic Methods in Programming. 94:128-149. https://doi.org/10.1016/j.jlamp.2017.10.003S1281499