Abstract
A technique to prove termination of term rewrite systems, or more precise, constructor systems (CSs) is presented. Soundness of this technique is proved and it is described how the technique can be performed automatically for a subclass of the CSs. Whereas simplification orders fail in proving termination of CSs that are not simply terminating, the presented technique may still automatically prove termination of these CSs.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Thomas Arts. A technique for automatically proving termination of constructor systems. Technical Report UU-CS-1995-17, Utrecht University, October 1995.
Thomas Arts and Hans Zantema. Termination of logic programs via labelled term rewrite systems. In Proceedings of CSN 1995. Sion, November 1995. Full version appeared as technical report UU-CS-1994-20.
N. Dershowitz. Termination of rewriting. Journal of Symbolic Computation, 3(1):69–116, 1987.
N. Dershowitz and J.-P. Jouannaud. Rewrite systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, pages 243–320. North-Holland, 1990.
Maria Ferreira and Hans Zantema. Syntactical analysis of total termination. Proceedings of ALP'94, LNCS(850):204–222, September 1994.
J. Giesl. Termination analysis for functional programs using term orderings. In Proceedings of the Second International Static Analysis Symposium, LNCS 983, Glasgow, Scotland, 1995.
Bernhard Gramlich. Abstract relations between restricted termination and confluence properties of rewrite systems. Fundamenta Informaticae, 24:3–23, 1995.
M. Hanus. The intergration of functions into logic programming: From theory to practice. Journal of Logic Programming, 19–20:583–628, 1994.
G. Huet and D. Lankford. On the uniform halting problem for term rewriting systems. Technical Report report 283, INRIA, 1978.
S. Hölldobler. Foundations of Equational Logic Programming, volume 353 of LNAI. Springer-Verlag, Berlin, 1989. Subseries of LNCS.
J.M. Hullot. Canonical forms and unification. 5th International Conference on Automated Deduction, LNCS(87):318–334, 1980.
Richard Kennaway. Complete term rewrite systems for decimal arithmetic and other total recursive functions. Workshop on Termination, La Bresse, France, May 1995.
J.W. Klop. Term rewriting systems. In S. Abramsky, D.M. Gabbay, and T.S.E. Maibaum, editors, Handbook of Logic in Computer Science, volume 2, pages 1–116. Oxford University Press, New York, 1992.
J.H. Siekmann. Unification theory. Journal of Symbolic Computation, 7:207–274, 1989.
Joachim Steinbach. Automatic termination proofs with transformation orderings. Proceedings of RTA-95, LNCS(914):11–26, April 1995.
H. Zantema. Termination of term rewriting: interpretation and type elimination. Journal of Symbolic Computation, 17:23–50, 1994.
H. Zantema. Termination of term rewriting by semantic labelling. Fundamenta lnformaticae, 24:89–105, 1995. Our technical reports and papers are available at http: //www. cs. ruu.nl/∼thomas
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Arts, T. (1996). Termination by absence of infinite chains of dependency pairs. In: Kirchner, H. (eds) Trees in Algebra and Programming — CAAP '96. CAAP 1996. Lecture Notes in Computer Science, vol 1059. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61064-2_38
Download citation
DOI: https://doi.org/10.1007/3-540-61064-2_38
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61064-9
Online ISBN: 978-3-540-49944-2
eBook Packages: Springer Book Archive