Higher-order recursive path orderings
Jean-Pierre Jouannaud, Alberto Rubio Gimeno · LA Referencia (Red Federada de Repositorios Institucionales de Publicaciones Científicas) · 1998
: 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 simplytyped -terms. The main result is that this ordering is well-founded, compatible with fi-reductions, and with polymorphic typing. We also restrict the ordering so as to obtain a new ordering operating on higher-order terms in j-long fi-normal form. Both orderings are powerful enough to allow for complex examples, including the polymorphic version of Godel's recursor for simple inductive types. Key words: higher-order rewriting ; typed lambda calculus; Godel's polymorphic recursor ; termination orderings. 1 Introduction Rewrite rules are increasingly used in programming languages and logical systems, with two main goals: defining functions by pattern matching; describing rule-based decision procedures. ML, Elf [16] and Isabelle [15] examplify the first use. A future version of Coq [8] will examplify the...