Context-Sensitive Rewriting, Lazy Rewriting, and
On-demand Rewriting
Author
Salvador Lucas
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.
Keywords
Declarative programming, replacement
restrictions, term rewriting, termination.