Skip to main content
SpringerLink
Log in

An LPO-based termination ordering for higher-order terms without λ-abstraction

  • Refereed Papers
  • Conference paper
  • First Online:
Theorem Proving in Higher Order Logics (TPHOLs 1998)

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

Included in the following conference series:

Abstract

We present a new precedence-based termination ordering for (polymorphic) higher-order terms without λ-abstraction. The ordering has been designed to strictly generalize the lexicographic path ordering (on first-order terms). It is relatively simple, but can be used to prove termination of many higher-order rewrite systems, especially those corresponding to typical functional programs. We establish the relevant properties of the ordering, include a number of examples, and also discuss certain limitations of the ordering and possible extensions.

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. Nachum Dershowitz and Charles Hoot. Natural termination. Theoretical Computer Science, 142(2):179–207, May 1995.

    Article  MATH  MathSciNet  Google Scholar 

  2. Nachum Dershowitz and Jean-Pierre Jouannaud. Rewrite systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B: Formal Methods and Semantics, chapter 6, pages 243–320. North-Holland, Amsterdam, 1990.

    Google Scholar 

  3. Stephen J. Garland and John V. Guttag. LP, the Larch Prover: Version 3.1. MIT Laboratory for Computer Science, January 1995. Available electronically at http://larch.lcs.mit.edu:8001/larch/LP/overview.html.

    Google Scholar 

  4. Jean-Pierre Jouannaud and Albert Rubio. A recursive path ordering for higher-order terms in η-long Β-normal form. In Harald Ganzinger, editor, Proceedings of the 7th International Conference on Rewriting Techniques and Applications (RTA-96), volume 1103 of Lecture Notes in Computer Science, pages 108–122, New Brunswick, NJ, USA, July 27–30 1996. Springer-Verlag.

    Google Scholar 

  5. Jean-Pierre Jouannaud and Albert Rubio. Rewrite orderings for higher-order terms in η-long Β-normal form and the recursive path ordering. To appear in Theoretical Computer Science, 1998. Available also at http://www-lsi.upc.es/~albert/papers/horpo.ps.gz.

    Google Scholar 

  6. Stefan Kahrs. Towards a domain theory for termination proofs. In Jieh Hsiang, editor, Proceedings of the 6th International Conference on Rewriting Techniques and Applications (RTA-95), volume 914 of Lecture Notes in Computer Science, pages 241–255, Kaiserslautern, Germany, April 5–7 1995. Springer-Verlag.

    Google Scholar 

  7. Maxim Lifantsev. Term rewriting systems. Diploma thesis, Moscow State Engineering-Physics Institute (Technical University), Moscow, Russia, February 1996. In Russian.

    Google Scholar 

  8. Carlos Loria-Saenz and Joachim Steinbach. Termination of combined (rewrite and λ-calculus) systems. In MichaËl Rusinowitch and Jean-Luc Rémy, editors, Conditional Term Rewriting Systems, Third International Workshop, volume 656 of Lecture Notes in Computer Science, pages 143–147, Pont-à-Mousson, France, July 8–10, 1992. Springer-Verlag.

    Google Scholar 

  9. Olav Lysne and Javier Piris. A termination ordering for higher order rewrite systems. In Jieh Hsiang, editor, Proceedings of the 6th International Conference on Rewriting Techniques and Applications (RTA-95), volume 914 of Lecture Notes in Computer Science, pages 26–40, Kaiserslautern, Germany, April 5–7 1995. Springer-Verlag.

    Google Scholar 

  10. M.J.C. Gordon and T.F. Melham. Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, 1993.

    Google Scholar 

  11. Sam Owre and Natarajan Shankar. The formal semantics of PVS. Technical Report SRI-CSL-97-2, Computer Science Laboratory, SRI International, Menlo Park, CA, August 1997.

    Google Scholar 

  12. Lawrence C. Paulson. Introduction to Isabelle. Technical Report 280, University of Cambridge, Computer Laboratory, 1993.

    Google Scholar 

  13. Jaco Van de Pol. Termination proofs for higher-order rewrite systems. In J. Heering, K. Meinke, B. Moeller, and T. Nipkow, editors, Higher-Order Algebra, Logic, and Term Rewriting, First International Workshop, volume 816 of Lecture Notes in Computer Science, pages 350–325, Amsterdam, The Netherlands, September 1993. Springer-Verlag.

    Google Scholar 

  14. Jaco Van de Pol and Helmut Schwichtenberg. Strict functionals for termination proofs. In M. Dezani-Ciancaglini and G. Plotkin, editors, Proceedings of the International Conference on Typed Lambda Calculi and Applications, volume 902 of Lecture Notes in Computer Science, pages 350–364, Edinburgh, Scotland, April 1995. Springer-Verlag.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, SUNY at Stony Brook, 11794, Stony Brook, NY, USA

    Maxim Lifantsev & Leo Bachmair

Authors
  1. Maxim Lifantsev
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Leo Bachmair
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Jim Grundy Malcolm Newey

Rights and permissions

Reprints and permissions

Copyright information

© 1998 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Lifantsev, M., Bachmair, L. (1998). An LPO-based termination ordering for higher-order terms without λ-abstraction. In: Grundy, J., Newey, M. (eds) Theorem Proving in Higher Order Logics. TPHOLs 1998. Lecture Notes in Computer Science, vol 1479. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0055142

Download citation

  • DOI: https://doi.org/10.1007/BFb0055142

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-64987-8

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

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation