Higher-order recursive path orderings

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 higher-order simply-typed lambda-terms. The main result is that this ordering is well-founded, compatible with beta-reductions, and with polymorphic typing. We also restrict the ordering so as to obtain a new ordering operating on higher-order terms in eta-long beta-normal form. Both orderings are powerful enough to allow for complex examples, including the polymorphic version of Gödel's recursor for simple inductive types.