Reversible Computation in Term Rewriting

TL;DR

This paper introduces a reversible extension to term rewriting, enabling backward computation, with transformations for injectivization and inversion, applicable in bidirectional program transformation.

Contribution

It proposes a conservative extension of term rewriting to achieve reversibility and defines transformations to make rewrite systems reversible.

Findings

Reversible term rewriting system developed

Injectivization and inversion transformations defined

Application demonstrated in bidirectional program transformation

Abstract

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 \rightarrow 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.