The Higher-Order recursive Path Ordering
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 beta-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.
extended abstract
full paper