Reversible Term Rewriting

Abstract

Essentially, in a reversible programming language, for each forward
computation step from state S to state S', there exists a
constructive and deterministic 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 paper,
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 and deterministic
method to get t1 from t2.  Here, we introduce a conservative
extension of term rewriting that becomes reversible.  Furthermore, we
also define a transformation to make a rewrite system reversible using
standard term rewriting.