Context-Sensitive Rewriting, Lazy Rewriting, and On-Demand Rewriting

Salvador Lucas

In Proc. of the International Workshop on Functional and (Constraint) Logic Programming (WFLP 2001) , Report No. 2017, University of Kiel

Abstract

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.