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.