Polymorphic Higher-Order recursive Path Orderings

This paper extends the termination proof techniques based on reduction orderings to a higher-order setting, by defining a family of recursive path orderings for terms of a typed lambda-calculus generated by a signature of polymorphic higher-order function symbols. These relations can be generated from two given well-founded orderings, on the function symbols and on the type constructors. The obtained orderings on terms are well-founded, monotonic, stable under substitution and include $\beta$-reductions. They can be used to prove the strong normalization property of higher-order calculi in which constants can be defined by higher-order rewrite rules using first-order pattern matching. For example, the polymorphic version of G{\"{o}}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. Many non-trivial examples are given which examplify the expressive power of these orderings.

This paper is an extended and improved version of~\cite{jouannaud99lics}. Polymorphic algebras have been made more expressive than in our previous framework. The notion of a polymorphic higher-order ordering is new. The higher-order recursive path ordering itself has been made much more powerful by replacing the congruence on types used there by an ordering on types satisfying some abstract properties. As a particular case obtained by using a restriction of Dershowitz's recursive path ordering for comparing types, we integrate both orderings into a single elegant one operating on terms and types as well. This presentation should in turn be considered as a key missing stone towards the definition of a recursive path ordering for dependent type calculi.

extended abstract

full paper