Paper: The Higher-Order Recursive Path Ordering (at LICS 1999)

Authors: Jean-Pierre Jouannaud Albert Rubio

Abstract

This paper extends the termination proof techniques based on reduction orderings to a higher-order setting, by adapting the recursive path ordering definition to terms of a typed lambda-calculus generated by a signature of polymorphic higher-order function symbols. The obtained ordering is well-founded, compatible with _-reductions and with polymorphic typing, monotonic with respect to the function symbols, and stable under substitution. It can therefore be used to prove the strong normalization property of higher-order calculi in which constants can be defined by higher-order rewrite rules. For example, the polymorphic version of Gödel'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. Several other non-trivial examples are given which examplify the expressive power of the ordering.

BibTeX

  @InProceedings{JouannaudRubio-TheHigherOrderRecur,
    author = 	 {Jean-Pierre Jouannaud and Albert Rubio},
    title = 	 {The Higher-Order Recursive Path Ordering},
    booktitle =  {Proceedings of the Fourteenth Annual IEEE Symposium on Logic in Computer Science (LICS 1999)},
    year =	 {1999},
    month =	 {July}, 
    pages =      {402--411},
    location =   {Trento, Italy}, 
    publisher =	 {IEEE Computer Society Press}
  }