Polymorphic higher-order recursive path orderings

9 years 8 months ago
Polymorphic higher-order recursive path orderings
This paper extends the termination proof techniques based on reduction orderings to a higher-order setting, by defining a family of recursive path orderings for terms of a typed lambda-calculus generated by a signature of polymorphic higher-order function symbols. These relations can be generated from two given well-founded orderings, on the function symbols and on the type constructors. The obtained orderings on terms are well-founded, monotonic, stable under substitution and include β-reductions. They can be used to prove the strong normalization property of higher-order calculi in which constants can be defined by higher-order rewrite rules using first-order pattern matching. For example, the polymorphic version of G¨odel’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. Many non-trivial examp...
Jean-Pierre Jouannaud, Albert Rubio
Added 15 Dec 2010
Updated 15 Dec 2010
Type Journal
Year 2007
Where JACM
Authors Jean-Pierre Jouannaud, Albert Rubio
Comments (0)