Lazy Rewriting and Context-Sensitive Rewriting
Lazy rewriting (LR) is intended to
improve the termination behavior of TRSs. This is attempted by
restricting reductions for selected arguments of functions.
Similarly, context-sensitive rewriting (CSR) forbids any
reduction on those arguments.
We show that LR and CSR coincide under certain conditions.
On the basis of this result, we also describe a transformation
which permits us to prove termination of
LR as termination of CSR for the transformed system. Since there
is a number of different techniques for proving termination
of CSR, this provides a formal framework for proving
termination of lazy rewriting.