  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.
