## Paper: The Higher-Order Recursive Path Ordering (at LICS 1999)

**Jean-Pierre Jouannaud Albert Rubio**

### Abstract

This paper extends the termination proof techniques based on reduction orderings to a higher-order setting, by adapting the recursive path ordering definition to terms of a typed lambda-calculus generated by a signature of polymorphic higher-order function symbols. The obtained ordering is well-founded, compatible with _-reductions and with polymorphic typing, monotonic with respect to the function symbols, and stable under substitution. It can therefore be used to prove the strong normalization property of higher-order calculi in which constants can be defined by higher-order rewrite rules. For example, the polymorphic version of Gödel's recursor for the natural numbers is easily oriented. And indeed, our ordering is polymorphic, in the sense that a single comparison allows to prove the termination property of all monomorphic instances of a polymorphic rewrite rule. Several other non-trivial examples are given which examplify the expressive power of the ordering.

### BibTeX

@InProceedings{JouannaudRubio-TheHigherOrderRecur, author = {Jean-Pierre Jouannaud and Albert Rubio}, title = {The Higher-Order Recursive Path Ordering}, booktitle = {Proceedings of the Fourteenth Annual IEEE Symposium on Logic in Computer Science (LICS 1999)}, year = {1999}, month = {July}, pages = {402--411}, location = {Trento, Italy}, publisher = {IEEE Computer Society Press} }