Lazy Rewriting and Context-Sensitive Rewriting

AbstractLazy 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 are a number of different techniques for proving termination of CSR, this provides a formal framework for proving termination of lazy rewriting