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