Abstract

Context-sensitive rewriting is a restriction of term rewriting 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, LPAR'01). 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. Most of these transformations are not very satisfactory when it comes to proving innermost termination. We investigate the relationship between termination and innermost termination of context-sensitive rewriting and we examine the applicability of the different transformations for innermost termination proofs. Finally, we present a simple transformation which is both sound and complete for innermost termination.

BibTeX Entry

@inproceedings{GM-DLT02,
 author    = "J{\"u}rgen Giesl and Aart Middeldorp",
 title     = "Innermost Termination of Context-Sensitive Rewriting",
 booktitle = "Proceedings of the 6th International Conference on
              Developments in Language Theory",
 series    = "Lecture Notes in Computer Science",
 volume    = 2450,
 pages     = "231--244",
 year      = 2003,
 doi       = "10.1007/3-540-45005-X\_20"
}