Abstract
This paper deals with termination proofs for Higher-Order Rewrite Systems (HRSs), introduced in [12]. This formalism combines the computational aspects of term rewriting and simply typed lambda calculus. The result is a proof technique for the termination of a HRS, similar to the proof technique “Termination by interpretation in a well-founded monotone algebra”, described in [8, 19]. The resulting technique is as follows: Choose a higher-order algebra with operations for each function symbol in the HRS, equipped with some well-founded partial ordering. The operations must be strictly monotonic in this ordering. This choice generates a model for the HRS. If the choice can be made in such a way that for each rule the interpretation of the left hand side is greater than the interpretation of the right hand side, then the HRS is terminating. At the end of the paper some applications of this technique are given, which show that this technique is natural and can easily be applied.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
G.J. Akkerman and J.C.M. Baeten. Term rewriting analysis in process algebra. Technical Report CS-R9130, Centre for Mathematics and Computer Science, June 1991.
H.P. Barendregt. The Lambda Calculus. Its Syntax and Semantics. North-Holland, Amsterdam, second, revised edition, 1984.
M. Bezem and J.F. Groote, editors. Proceedings of the 1 st International Conference on Typed Lambda Calculi and Applications, TLCA '93, Utrecht, The Netherlands, volume 664 of Lecture Notes in Computer Science. Springer-Verlag, 1993.
V. Breazu-Tannen. Combining algebra and higher-order types. In Proceedings 3 th Annual Symposium on Logic in Computer Science, Edinburgh, pages 82–90, July 1988.
R. de Vrijer. Surjective Pairing and Strong Normalization: Two Themes in Lambda Calculus. PhD thesis, University of Amsterdam, 1987.
R.O. Gandy. Proofs of strong normalization. In J.R. Hindley and J.P. Seldin, editors, To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pages 457–477. Academic Press, 1980.
J.F. Groote and A. Ponse. The syntax and semantics of μCRL. Report CS-R9076, CWI, Amsterdam, 1990.
G. Huet and D.C. Oppen. Equations and rewrite rules: A survey. In R. Book, editor, Formal Language Theory: Perspectives and Open Problems, pages 349–405. Academic Press, 1980.
J.P. Jouannaud and M. Okada. A computation model for executable higher-order algebraic specification languages. In Proceedings 6 th Annual Symposium on Logic in Computer Science, Amsterdam, The Netherlands, pages 350–361, 1991.
Z. Khasidashvili. Perpetual reductions and strong normalization in orthogonal term rewriting systems. Technical Report CS-R9345, CWI, Amsterdam, July 1993.
J.W. Klop. Combinatory Reduction Systems, volume 127 of Mathematical Centre Tracts. Mathematisch Centrum, Amsterdam, 1980.
T. Nipkow. Higher-order critical pairs. In Proceedings 6 th Annual Symposium on Logic in Computer Science, Amsterdam, The Netherlands, pages 342–349, 1991.
T. Nipkow. Orthogonal higher-order rewrite systems are confluent. In Bezem and Groote [3], pages 306–317.
C. Paulin-Mohring. Inductive definitions in the system Coq. Rules and properties. In Bezem and Groote [3], pages 328–345.
L. C. Paulson. Isabelle: The next 700 theorem provers. In P. Odifreddi, editor, Logic and Computer Science, pages 361–386. Academic Press Limited, London, 1990. In: The APIC-series 31.
M.P.A. Sellink. Verifying process algebra proofs in type theory. Technical Report 87, Logic Group Preprint Series, Utrecht University, March 1993.
V. van Oostrom and F. van Raamsdonk. Comparing combinatory reduction systems and higher-order rewrite systems. Technical Report IR-333, Vrije Universiteit Amsterdam, August 1993. Appears in this Volume.
D.A. Wolfram. The Clausal Theory of Types, volume 21 of Cambridge tracts in theoretical computer science. Cambridge University Press, Cambridge, 1993.
H. Zantema. Termination of term rewriting by interpretation. In M. Rusinowitch and J.L. Rémy, editors, Conditional Term Rewriting Systems, proceedings third international workshop CTRS-92, volume 656 of Lecture Notes in Computer Science, pages 155–167. Springer-Verlag, 1993. Full version appeared as report RUU-CS-92-14, Utrecht University.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
van de Pol, J. (1994). Termination proofs for higher-order rewrite systems. In: Heering, J., Meinke, K., Möller, B., Nipkow, T. (eds) Higher-Order Algebra, Logic, and Term Rewriting. HOA 1993. Lecture Notes in Computer Science, vol 816. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58233-9_14
Download citation
DOI: https://doi.org/10.1007/3-540-58233-9_14
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-58233-5
Online ISBN: 978-3-540-48579-7
eBook Packages: Springer Book Archive