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 [18]. 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.
Partially supported by the Grant-in-Aid for Scientific Research (C)(2) 13224006 of the Ministry of Education, Culture, Sports, Science and Technology of Japan.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
T. Arts and J. Giesl. Termination of term rewriting using dependency pairs. Theoretical Computer Science, 236:133–178, 2000.
F. Baader and T. Nipkow. Term Rewriting and All That. Cambr. Univ. Pr., 1998.
C. Borralleras, S. Lucas, and A. Rubio. Recursive path orderings can be contextsensitive. In Proc. 18th CADE, volume 2392 of LNAI, pages 314–331, 2002.
M. Clavel, S. Eker, P. Lincoln, and J. Meseguer. Principles of Maude. In Proc. 1st WRLA, volume 4 of ENTCS, 1996.
R. Diaconescu and K. Futatsugi. CafeOBJ Report, volume 6 of AMAST Series in Computing. World Scientific, 1998.
S. Eker. Term rewriting with operator evaluation strategies. In Proc. 2nd WRLA, volume 15 of ENTCS, pages 1–20, 1998.
M.C.F. Ferreira and A.L. Ribeiro. Context-sensitive AC-rewriting. In Proc. 10th RTA, volume 1631 of LNCS, pages 173–187, 1999.
O. Fissore, I. Gnaedig, and H. Kirchner. Induction for termination with local strategies. In Proc. 4th International Workshop on Strategies in Automated Deduction, volume 58 of ENTCS, 2001.
J. Giesl and A. Middeldorp. Transforming context-sensitive rewrite systems. In Proc. 10th RTA, volume 1631 of LNCS, pages 271–285, 1999.
J. Giesl and A. Middeldorp.Innermost termination of context-sensitive rewriting. Technical Report AIB-2002-048, RWTH Aachen, Germany, 2002.
J. Giesl and A. Middeldorp. Transformation techniques for context-sensitive rewrite systems. Technical Report AIB-2002-028, RWTH Aachen, Germany, 2002. Extended version of [9].
J. Goguen, T. Winkler, J. Meseguer, K. Futatsugi, and J.-P. Jouannaud. Introducing OBJ. In J. Goguen and G. Malcolm, editors, Software Engineering with OBJ: algebraic specification in action. Kluwer, 2000.
B. Gramlich. Abstract relations between restricted termination and confluence properties of rewrite systems. Fundamenta Informaticae, 24:3–23, 1995.
B. Gramlich and S. Lucas. Modular termination of context-sensitive rewriting. In Proc. 4th PPDP, pages 50–61. ACM Press, 2002.
B. Gramlich and S. Lucas. Simple termination of context-sensitive rewriting. In Proc. 3rd Workshop on Rule-Based Programming, pages 29–41. ACM Press, 2002.
S. Lucas. Termination of context-sensitive rewriting by rewriting. In Proc. 23rd ICALP, volume 1099 of LNCS, pages 122–133, 1996.
S. Lucas. Context-sensitive computations in functional and functional logic programs. Journal of Functional and Logic Programming, 1:1–61, 1998.
S. Lucas. Termination of rewriting with strategy annotations. In Proc. 8th LPAR, volume 2250 of LNAI, pages 669–684, 2001.
S. Lucas, 2001-2002. Personal communication.
S. Lucas. Termination of (canonical) context-sensitive rewriting. In Proc. 13th RTA, volume 2378 of LNCS, pages 296–310, 2002.
T. Nagaya. Reduction Strategies for Term Rewriting Systems. PhD thesis, School of Information Science, Japan Advanced Institute of Science and Technology, 1999.
M. Nakamura and K. Ogata. The evaluation strategy for head normal form with and without on-demand flags. In Proc. 3rd WRLA, volume 36 of ENTCS, 2001.
H. Zantema. Termination of context-sensitive rewriting. In Proc. 8th RTA, volume 1232 of LNCS, pages 172–186, 1997.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Giesl, J., Middeldorp, A. (2003). Innermost Termination of Context-Sensitive Rewriting. In: Ito, M., Toyama, M. (eds) Developments in Language Theory. DLT 2002. Lecture Notes in Computer Science, vol 2450. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45005-X_20
Download citation
DOI: https://doi.org/10.1007/3-540-45005-X_20
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-40431-6
Online ISBN: 978-3-540-45005-4
eBook Packages: Springer Book Archive