Skip to main content
SpringerLink
Log in

A Higher-Order Iterative Path Ordering

  • Conference paper
Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2008)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 5330))

Abstract

The higher-order recursive path ordering (HORPO) defined by Jouannaud and Rubio provides a method to prove termination of higher-order rewriting. We present an iterative version of HORPO by means of an auxiliary term rewriting system, following an approach originally due to Bergstra and Klop. We study well-foundedness of the iterative definition, discuss its relationship with the original HORPO, and point out possible ways to strengthen the ordering.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Bergstra, J., Klop, J.W.: Algebra of communicating processes. Theoretical Computer Science 37(1), 171–199 (1985)

    MathSciNet  MATH  Google Scholar 

  2. Blanqui, F., Jouannaud, J.-P., Rubio, A.: The computability path ordering: The end of a quest. In: Kaminski, M., Martini, S. (eds.) CSL 2008. LNCS, vol. 5213, pp. 1–14. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  3. Buchholz, W.: Proof-theoretic analysis of termination proofs. Annals of Pure and Applied Logic 75(1–2), 57–65 (1995)

    Article  MathSciNet  MATH  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  5. Jouannaud, J.-P., Okada, M.: A computation model for executable higher-order algebraic specification languages. In: Proceedings of LICS 1991, Amsterdam, The Netherlands, pp. 350–361 (July 1991)

    Google Scholar 

  6. Jouannaud, J.-P., Rubio, A.: The higher-order recursive path ordering. In: Proceedings of LICS 1999, Trento, Italy, pp. 402–411 (July 1999)

    Google Scholar 

  7. Jouannaud, J.-P., Rubio, A.: Higher-order orderings for normal rewriting. In: Pfenning, F. (ed.) RTA 2006. LNCS, vol. 4098, pp. 387–399. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  8. Jouannaud, J.-P., Rubio, A.: Polymorphic higher-order recursive path orderings. Journal of the ACM 54(1), 1–48 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  9. Kamin, S., Lévy, J.-J.: Two generalizations of the recursive path ordering. University of Illinois (1980)

    Google Scholar 

  10. Klop, J.W., van Oostrom, V., de Vrijer, R.: Iterative lexicographic path orders. In: Futatsugi, K., Jouannaud, J.-P., Meseguer, J. (eds.) Algebra, Meaning, and Computation. LNCS, vol. 4060, pp. 541–554. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  11. Koprowski, A.: Coq formalization of the higher-order recursive path ordering. Technical Report CSR-06-21, Eindhoven University of Technology (August 2006)

    Google Scholar 

  12. Nipkow, T.: Higher-order critical pairs. In: Proceedings of LICS 1991, Amsterdam, The Netherlands, pp. 342–349 (July 1991)

    Google Scholar 

  13. van Oostrom, V.: Personal communication (2008)

    Google Scholar 

  14. van Raamsdonk, F.: On termination of higher-order rewriting. In: Middeldorp, A. (ed.) RTA 2001. LNCS, vol. 2051, pp. 261–275. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  15. Tait, W.W.: Intensional interpretations of functionals of finite type I. Journal of Symbolic Logic 32(2), 198–212 (1967)

    Article  MathSciNet  MATH  Google Scholar 

  16. Terese: Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science, vol. 55. Cambridge University Press, Cambridge (2003)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Theoretical Computer Science, Vrije Universiteit, De Boelelaan 1081a, 1081 HV, Amsterdam, The Netherlands

    Cynthia Kop & Femke van Raamsdonk

Authors
  1. Cynthia Kop
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Femke van Raamsdonk
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Carnegie Mellon University, Doha, Qatar

    Iliano Cervesato

  2. Technische Universität Darmstadt, Germany

    Helmut Veith

  3. University of Manchester, UK

    Andrei Voronkov

Rights and permissions

Reprints and permissions

Copyright information

© 2008 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Kop, C., van Raamsdonk, F. (2008). A Higher-Order Iterative Path Ordering. In: Cervesato, I., Veith, H., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2008. Lecture Notes in Computer Science(), vol 5330. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-89439-1_48

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-89439-1_48

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-89438-4

  • Online ISBN: 978-3-540-89439-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation