Skip to main content
SpringerLink
Log in

A termination ordering for higher order rewrite systems

  • Regular Papers
  • Conference paper
  • First Online:
Rewriting Techniques and Applications (RTA 1995)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 914))

Included in the following conference series:

Abstract

We present an extension of the recursive path ordering for the purpose of showing termination of higher order rewrite systems. Keeping close to the general path ordering of Dershowitz and Hoot, we demonstrate sufficient properties of the termination functions for our method to apply. Thereby we describe a class of different orderings. Finally we compare our method to previously published extensions of the recursive path ordering into the higher order setting.

On leave from Dep. of Informatics, University of Oslo, P.O. box 1080 Blindern, 0316 Oslo, Norway. Supported by the Norwegian Research Council.

On leave from U.P.V., D.S.I.C., Camino de Vera S/N, P.O. box 22012, 46071 Valencia, Spain. Partially supported by CICYT under grant TIC 92-0793-C02-02.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. H. P. Barendregt. The Lambda Calculus, its Syntax and Semantics. North Holland, Amsterdam, 2nd ed., 1984.

    Google Scholar 

  2. H. P. Barendregt. Handbook of Logic in Computer Science, chapter Typed lambda calculi. Oxford Univ. Press, 1993. eds. Abramsky et al.

    Google Scholar 

  3. V. Breazu-Tannen. Combining algebra and higher-order types. In Proceedings 3rd IEEE Symposium on Logic in Computer Science, Edinburgh (UK), July 1988.

    Google Scholar 

  4. N. Dershowitz. Orderings for term-rewriting systems. Theoretical Computer Science, 17:279–301, 1982.

    Article  Google Scholar 

  5. N. Dershowitz and C. Hoot. Topics in termination. In Proceedings 5th Conference on Rewriting Techniques and Applications, Montreal (Canada), volume 690 of Lecture Notes in Computer Science, pages 198–212. Springer-Verlag, 1993.

    Google Scholar 

  6. N. Dershowitz and J.-P. Jouannaud. Rewrite systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, chapter 6. Elsevier, Amsterdam, 1990.

    Google Scholar 

  7. M. C. F. Ferreira and H. Zantema. Well-foundedness of term orderings. In Proceedings 4th International Workshop on Conditional Term Rewriting Systems, Jesuralem (Israel), 1994. To be published by Springer Verlag.

    Google Scholar 

  8. R. Hindley and J. Seldin. Introduction to Combinators and λ-calculus. Cambridge University Press, 1986.

    Google Scholar 

  9. G. Huet. A unification algorithm for typed λ-calculus. Theoretical Computer Science, 1(1):27–57, June 1975.

    Article  Google Scholar 

  10. J.-P. Jouannaud and M. Okada. A computation model for executable higer-order algebraic specification languages. In Proceedings 6th IEEE Symposium on Logic in Computer Science, pages 350–361, 1991.

    Google Scholar 

  11. S. Kamin and J.-J. Lévy. Two generalizations of the recursive path ordering. Unpublished Note, Department of Computer Science, University of Illinois, Urbana, IL, 1980.

    Google Scholar 

  12. J. W. Klop. Combinatory Reduction Systems. Mathematical Centre Tracts 127, Mathematisch Centrum, Amsterdam, 1980.

    Google Scholar 

  13. C. 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.

    Google Scholar 

  14. C. Loría-Sáenz and J. Steinbach. Termination of combined (rewrite and λ-calculus) systems. In Proceedings 3rd International Workshop on Conditional Term Rewriting Systems, Pont-a-Mousson (France), volume 656 of Lecture Notes in Computer Science, pages 143–147. Springer-Verlag, 1992.

    Google Scholar 

  15. D. Miller. A logic programming language with lambda-abstraction function variables, and simple unification. Journal of Logic and Computation, 1(4):497–536, 1991.

    Google Scholar 

  16. T. Nipkow. Higher order critical pairs. In Proceedings 6th IEEE Symposium on Logic in Computer Science, pages 342–349, 1991.

    Google Scholar 

  17. J. van de Pol. Termination proofs for higher-order rewrite systems. In First International Workshop on Higher-Order Algebra, Logic and Term Rewriting, volume 816 of Lecture Notes in Computer Science, pages 305–325. Springer-Verlag, 1993.

    Google Scholar 

  18. H. Zantema. Termination of term rewriting by interpretation. In Proceedings 3rd International Workshop on Conditional Term Rewriting Systems, Pont-a-Mousson (France), volume 656 of Lecture Notes in Computer Science, pages 155–167. Springer-Verlag, 1992.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Laboratoire de Recherche en Informatique, Bat. 490, 91405, Orsay Cedex, France

    Olav Lysne & Javier Piris

Authors
  1. Olav Lysne
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Javier Piris
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Jieh Hsiang

Rights and permissions

Reprints and permissions

Copyright information

© 1995 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Lysne, O., Piris, J. (1995). A termination ordering for higher order rewrite systems. In: Hsiang, J. (eds) Rewriting Techniques and Applications. RTA 1995. Lecture Notes in Computer Science, vol 914. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-59200-8_45

Download citation

  • DOI: https://doi.org/10.1007/3-540-59200-8_45

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-59200-6

  • Online ISBN: 978-3-540-49223-8

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation