Abstract
There is an increasing use of (first- and higher-order) rewrite rules in many programming languages and logical systems. The recursive path ordering (RPO) is a well-known tool for proving termination of such rewrite rules in the first-order case. However, RPO has some weaknesses. For instance, since it is a simplification ordering, it can only handle simply terminating systems. Several techniques have been developed for overcoming these weaknesses of RPO. A very recent such technique is the monotonic semantic path ordering (MSPO), a simple and easily automatable ordering which generalizes other more ad-hoc methods. Another recent extension of RPO is its higher-order version HORPO. HORPO is an ordering on terms of a typed lambda-calculus generated by a signature of higher-order function symbols. Although many interesting examples can be proved terminating using HORPO, it inherits the weaknesses of the first-order RPO.
Therefore, there is an obvious need for higher-order termination orderings without these weaknesses. Here we define the first such ordering, the monotonic higher-order semantic path ordering (MHOSPO), which is still automatable like MSPO. We give evidence of its power by means of several natural and non-trivial examples which cannot be handled by HORPO.
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
T. Arts and J. Giesl. Termination of term rewriting using dependency pairs.Theoretical Computer Science, 236:133–178, 2000.
H. P. Barendregt. Lambda calculi with types. In S. Abramsky, D. M. Gabbay and T. S. E. Maibaum, eds., Handbook of Logic in Computer Science. Oxford University Press, 1992.
C. Borralleras, M. Ferreira, and A. Rubio. Complete monotonic semantic path orderings. Proc. of the 17th International Conference on Automated Deduction, LNAI 1831, pp. 346–364, Pittsburgh, USA, 2000. Springer-Verlag.
C. Borralleras and A. Rubio. A monotonic higher-order semantic path ordering (Long version). Available at www.lsi.upc.es/~albert/papers.html,2001.
N. Dershowitz. Orderings for term-rewriting systems. Theoretical ComputerScience, 17(3):279–301, 1982.
N. Dershowitz and J.-P. Jouannaud. Rewrite systems. In Jan van Leeuwen,ed., Handbook of Theoretical Computer Science, vol. B: Formal Models and Semantics, chap. 6, pp. 244–320. Elsevier Science Publishers B.V., 1990.
J-P. Jouannaud and A. Rubio. Rewite orderings for higher-order terms in ή-long β-normal form and the recursive path ordering. Theoretical Computer Science, 208:33–58, 1998.
J-P. Jouannaud and A. Rubio. The higher-order recursive path ordering. In 14th IEEE Symposium on Logic in Computer Science(LICS), pp. 402–411, 1999.
J.-P. Jouannaud and A. Rubio. Higher-order Recursive Path Orderings à la carte (draft), 2001.
S. Kamin and J.-J. Lévy. Two generalizations of the recursive path ordering. Unpublished note, Dept. of Computer Science, Univ. of Illinois, Urbana, IL,1980.
C. Loría-Sáenz and J. Steinbach. Termination of combined (rewrite and λ-calculus) systems. In Proc. 3rd Int. Workshop on Conditional Term Rewriting Systems, LNCS 656, pp. 143–147, 1992. Springer-Verlag.
Richard Mayr and Tobias Nipkow. Higher-order rewrite systems and their confluence. Theoretical Computer Science, 192(1):3–29, 1998.
Brigitte Pientka. Termination and reduction checking for higher-order logic programs. Proc. First International Joint Conference on Automated Reasoning, volume 2083 of LNAI, pp. 402–415, 2001. Springer-Verlag.
J. van de Pol. Termination of Higher-Order Rewrite Systems. PhD thesis,Departament of Philosophy Utrecht University, 1996.
J. van de Pol and H. Schwichtenberg. Strict functional for termination proofs. In Proc. of the International Conference on Typed Lambda Calculi and Applications,1995.
Femke van Raamsdonk. On termination of higher-order rewriting. 12th Int. Conf. on Rewriting Techniques and Applications, LNCS 2051, pp. 261–275, 2001.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Borralleras, C., Rubio, A. (2001). A Monotonic Higher-Order Semantic Path Ordering. In: Nieuwenhuis, R., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2001. Lecture Notes in Computer Science(), vol 2250. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45653-8_37
Download citation
DOI: https://doi.org/10.1007/3-540-45653-8_37
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42957-9
Online ISBN: 978-3-540-45653-7
eBook Packages: Springer Book Archive