A Recursive Path Ordering for Higher-Order Terms in eta-Long beta-Normal
Form
This paper extends the termination proof techniques based on rewrite
orderings to a higher-order setting, by defining a recursive path
ordering for simply typed algebraic lambda-terms in eta-long
beta-normal form. This ordering extends, on the one hand a
precedence on the functions symbols, on the other hand a well-founded
ordering on the type structure compatible with the signature, that is,
such that a term has a type bigger than or equal to the type of any of
its subterms. Terms are compared by type first, then by head function
symbol, before to apply recursively on the term structure. Several
examples are carried out.