Higher-order recursive path orderings
Document typeResearch report
Rights accessOpen Access
All rights reserved. This work is protected by the corresponding intellectual and industrial property rights. Without prejudice to any existing legal exemptions, reproduction, distribution, public communication or transformation of this work are prohibited without permission of the copyright holder
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.
CitationJouannaud, J., Rubio, A. "Higher-order recursive path orderings". 1998.