Lazy Rewriting and Context-Sensitive Rewriting

Author

Salvador Lucas

Abstract

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.