Context-Sensitive Rewriting, Lazy Rewriting, and On-Demand Rewriting
In Proc. of the International Workshop on Functional and (Constraint) Logic Programming (WFLP 2001)
, Report No. 2017, University of Kiel
On-demand rewriting provides an operational model for term rewriting
controlled by annotations consisting of (sets of) positive and negative
integers referring the arguments of function symbols.
Context-sensitive rewriting and lazy rewriting provide (different)
operational models for positive annotations. In this paper we prove that,
under certain conditions, the three operational models coincide. In this
case, it makes sense using context-sensitive rewriting as it is the
simplest one. This fact also permits proving termination
of lazy rewriting by proving termination of context-sensitive rewriting
for a transformed rewrite system.