Abstract
In this article, we are concerned with the proofs of termination of rewrite systems by the method of interpretations. We propose a modified approach to subrecursive hierarchies of functions by means of a syntactical approach to ordinal recursion. Our method appears to be appropriate for finding interpretations in a systematic way. We provide several examples of applications. It is shown that three usual recursion schemas over the natural numbers, recursion with parameter substitution, simple nested recursion and unnested multiple recursion can be encoded directly in our system. As the corresponding ordinal terms are primitive recursively closed, we get a concise and intuitive proof for the closure of the class of primitive recursive functions under these schemes.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
E.A. Cichon and A. Weiermann: Term rewriting theory for the primitive recursive functions. 1995. Submitted.
E. Dennis-Jones and S.S. Wainer: Subrecursive Hierarchies Via Direct Limits. Logic Colloquium 83, Richter and Borger and Oberschelp and Schinzel and Thomas eds., Springer Lecture Notes 1104, pp 117–128.
N. Dershowitz and J.P. Jouannaud: Rewrite systems. Handbook of Theoretical Computer Science.
M. Fairtlough and S.S. Wainer: Ordinal Complexity of Recursive Definitions. Information and Computation 99 (1992), pp 123–153.
J. Gallier: What is so special about Kruskal's theorem and the ordinal γ 0? Annals of Pure and Applied Logic 53 (1991)
J-Y. Girard: π 12 Logic, Part 1, Ann. Math. Logic 21 (1981), pp 75–219.
D. Hofbauer: Termination proofs with multiset path orderings imply primitive recursive derivation lengths. Proc. 2nd ALP. LNCS 463 (1990), pp 243–320.
L. Kirby and J. Paris: Accessible independence results for Peano arithmetic. Bull. London Math. Soc. 14 (1982), pp 285–225.
R. Péter: Recursive Functions. Academic Press (1967).
A. Weiermann: Termination proofs by lexicographic path orderings yield multiply recursive derivation lengths. To appear in TCS.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cichon, E.A., Touzet, H. (1996). An ordinal calculus for proving termination in term rewriting. 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_40
Download citation
DOI: https://doi.org/10.1007/3-540-61064-2_40
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