Logic in Computer Science (LICS 1999)

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

Authors: J.-P. Jouannaud A. 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 = 	 {J.-P. Jouannaud and A. Rubio},
    title = 	 {The Higher-Order Recursive Path Ordering},
    booktitle =  {Proceedings of the Fourteenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1999},
    year =	 1999,
    editor =	 {Giuseppe Longo},
    month =	 {July}, 
    pages =      {402--411},
    location =   {Trento, Italy}, 
    publisher =	 {IEEE Computer Society Press}
  }