Abstract
This paper extends the termination proof techniques based on rewrite orderings to a higher-order setting, by defining a recursive path ordering for simply typed higher-order terms in η-long β-normal form. This ordering is powerful enough to show termination of several complex examples.
This work was partly supported by the ESPRIT Basic Research Action CCL and the EU Human Capital and Mobility Network Console.
This work results from a stay of the author at the Technical University of Catalonia.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Henk Barendregt. Handbook of Theoretical Computer Science, volume B, chapter Functional Programming and Lambda Calculus, pages 321–364. North-Holland, 1990. J. van Leeuwen ed.
Henk Barendregt. Handbook of Logic in Computer Science, chapter Typed lambda calculi. Oxford Univ. Press, 1993. eds. Abramsky et al.
Jaco Van de Pol and Helmut Schwichtenberg. Strict functional for termination proofs. In Proceedings of the International Conference on Typed Lambda Calculi and Applications, Edinburgh, Great Britain, 1995.
Nachum Dershowitz. Orderings for term rewriting systems. Theoretical Computer Science, 17(3):279–301, March 1982.
Nachum Dershowitz and Jean-Pierre Jouannaud. Rewrite systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, pages 243–309. North-Holland, 1990.
Maribel Fernández and Jean-Pierre Jouannaud. Modular termination of term rewriting systems revisited. In Egidio Astesiano, Gianni Reggio, and Andrzej Tarlecki, editors, Recent Trends in Data Type Specification, volume 906 of Lecture Notes in Computer Science. Springer-Verlag, 1995. Refereed selection of papers presented at ADT'94.
Deepak Kapur and Han Tao Zhang. An overview of the rewrite rule laboratory (RRL). In Proc. 3rd Rewriting Techniques and Applications, Chapel Hill, LNCS 355, pages 559–563. Springer-Verlag, 1989.
Carlos Loría-Sáenz. A Theoretical Framework for Reasoning about Program Construction based on Extensions of Rewrite Systems. PhD thesis, Fachbereich Informatik der Universität Kaiserslautern, 1993.
Carlos Loría-Sáenz and Joachim Steinbach. Termination of combined (rewrite and λ-calculus) systems. In Proc. 3rd Int. Workshop on Conditional Term Rewriting Systems, Pont-à-Mousson, LNCS 656, volume 656 of Lecture Notes in Computer Science, pages 143–147. Springer-Verlag, 1992.
Olav Lysne and Javier Piris. A termination ordering for higher order rewrite systems. In Proc. 6th Rewriting Techniques and Applications, Kaiserslautern, LNCS 914, Kaiserslautern, Germany, 1995.
Claude Marché. Normalised rewriting and normalised completion. In Proceedings of the Ninth Annual IEEE Symposium on Logic in Computer Science, Paris, France, July 1994. IEEE Comp. Soc. Press.
Tobias Nipkow. Higher order critical pairs. In Proc. IEEE Symp. on Logic in Comp. Science, Amsterdam, 1991.
Pilar Nivela and Robert Nieuwenhuis. Practical results on the saturation of full first-order clauses: Experiments with the saturate system. (system description). In C. Kirchner, editor, 5th International Conference on Rewriting Techniques and Applications, LNCS 690, Montreal, Canada, June 16–18, 1993. Springer-Verlag.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Jouannaud, JP., Rubio, A. (1996). A recursive path ordering for higher-order terms in η-long β-normal form. In: Ganzinger, H. (eds) Rewriting Techniques and Applications. RTA 1996. Lecture Notes in Computer Science, vol 1103. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61464-8_46
Download citation
DOI: https://doi.org/10.1007/3-540-61464-8_46
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61464-7
Online ISBN: 978-3-540-68596-8
eBook Packages: Springer Book Archive