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. |