The following technical report is available from http://aib.informatik.rwth-aachen.de:
Jürgen Giesl, Aart Middledorp Transformation Techniques for Context-Sensitive Rewrite Systems 2002-02
Abstract: Context-sensitive rewriting is a term rewriting strategy used to model non-strict (lazy) evaluation in functional programming. The goal of this paper is the study and development of techniques to analyse the termination behavior of context-sensitive rewrite systems. For that purpose, several methods have been proposed in the literature which transform context-sensitive rewrite systems into ordinary rewrite systems such that termination of the transformed ordinary system implies termination of the original context-sensitive system. In this way, the huge variety of existing techniques for termination analysis of ordinary rewriting can be used for context-sensitive rewriting, too.
We analyse the existing transformation techniques for proving termination of context-sensitive rewriting and we suggest two new transformations. Our first method is simple, sound, and more powerful than the previously proposed transformations. However, it is not complete, i.e., there are terminating context-sensi-tive rewrite systems that are transformed into non-terminating term rewrite systems. The second method that we present in this paper is both sound and complete. All these observations also hold for rewriting modulo associativity and commutativity. Our completeness result can be interpreted as stating that one no longer needs any special techniques for the termination analysis of context-sensitive rewriting.
Regards, Volker Stolz