The following technical report is available from http://aib.informatik.rwth-aachen.de/:

Jürgen Giesl, Aart Middeldorp Innermost Termination of Context-Sensitive Rewriting 2002-04

Abstract: Context-sensitive rewriting is a term rewriting strategy used to model evaluation strategies in functional programming and in programming languages like OBJ. For example, under certain conditions termination of an OBJ program is equivalent to innermost termination of the corresponding context-sensitive rewrite system [Lucas, 2001]. To prove termination of context-sensitive rewriting, 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. None of these transformation methods is very satisfactory when it comes to proving innermost termination. We present a simple transformation which is both sound and complete for innermost termination.