Hostname: page-component-7c8c6479df-7qhmt Total loading time: 0 Render date: 2024-03-27T19:39:24.666Z Has data issue: false hasContentIssue false

Transformation techniques for context-sensitive rewrite systems

Published online by Cambridge University Press:  07 June 2004

JÜRGEN GIESL
Affiliation:
LuFG Informatik II, RWTH Aachen, Ahornstr. 55, 52074 Aachen, Germany (e-mail: giesl@informatik.rwth-aachen.de)
AART MIDDELDORP
Affiliation:
Institute of Information Sciences and Electronics, University of Tsukuba, Tsukuba 305-8573, Japan (e-mail: ami@is.tsukuba.ac.jp)
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

Context-sensitive rewriting is a computational restriction of term rewriting used to model non-strict (lazy) evaluation in functional programming. The goal of this paper is the study and development of techniques to analyze 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 analyze 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-sensitive 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.

Type
Article
Copyright
© 2004 Cambridge University Press

Footnotes

A preliminary version of this paper appeared in the Proceedings of the 10th International Conference on Rewriting Techniques and Applications, Lecture Notes in Computer Science 1631, pp. 271–285, 1999.
Submit a response

Discussions

No Discussions have been published for this article.