Abstract
Context-sensitive term rewriting is a kind of term rewriting in which reduction is not allowed inside some fixed arguments of some function symbols. We introduce two new techniques for proving termination of context-sensitive rewriting. The first one is a modification of the technique of interpretation in a well-founded order, the second one is implied by a transformation in which context-sensitive termination of the original system can be concluded from termination of the transformed one. In combination with purely automatic techniques for proving ordinary termination, the latter technique is purely automatic too.
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
Arts, T., and Giesl, J. Termination of constructor systems. In Proceedings of the 7th Conference on Rewriting Techniques and Applications (1996), vol. 1103 of Lecture Notes in Computer Science, Springer, pp. 63–77.
Bellegarde, F., and Lescanne, P. Termination by completion. Applicable Algebra in Engineering, Communication and Computing 1, 2 (1990), 79–96.
Ben-Cherifa, A., and Lescanne, P. Termination of rewriting systems by polynomial interpretations and its implementation. Science of Computing Programming 9, 2 (1987), 137–159.
Dershowitz, N. Termination of rewriting. Journal of Symbolic Computation 3, 1 and 2 (1987), 69–116.
Lucas, S. Fundamentals of context-sensitive rewriting. In Proceedings of the 22nd Seminar on Current Trends in Theory and Practice of Informatics (SOFSEM95) (1995), J. S. M. Bartosek and J. Wiedermann, Eds., vol. 1012 of Lecture Notes in Computer Science, Springer, pp. 405–412.
Lucas, S. Context-sensitive computations in confluent programs. In Proceedings of the 8th International Symposium on Programming Languages: Implementations, Logics and Programs (PLILP96) (1996), H. Kuchen and S. D. Swierstra, Eds., vol. 1140 of Lecture Notes in Computer Science, Springer, pp. 403–422.
Lucas. S. Termination of context-sensitive rewriting by rewriting. In Proceedings of the 23rd International Colloquium on Automata, Languages and Programming (ICALP96) (1996), F. Meyer auf der Heide and B. Monien, Eds., vol. 1099 of Lecture Notes in Computer Science, Springer, pp. 122–133.
Steinbach, J. Simplification orderings: history of results. Fundamenta Informaticae 24 (1995), 47–87.
Zantema, H. Termination of term rewriting: interpretation and type elimination. Journal of Symbolic Computation 17 (1994), 23–50.
Zantema, H. Termination of term rewriting by semantic labelling. Fundamenta Informaticae 24 (1995), 89–105.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Zantema, H. (1997). Termination of context-sensitive rewriting. In: Comon, H. (eds) Rewriting Techniques and Applications. RTA 1997. Lecture Notes in Computer Science, vol 1232. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-62950-5_69
Download citation
DOI: https://doi.org/10.1007/3-540-62950-5_69
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-62950-4
Online ISBN: 978-3-540-69051-1
eBook Packages: Springer Book Archive