A Termination Ordering for Higher Order Rewrite Systems

Author

Olav Lysne, Javier Piris

Abstract

We present an extension of the recursive path ordering for the purpose of showing termination of higher order rewrite systems. Keeping close to the general path ordering of Dershowitz and Hoot, we demonstrate the necessary properties of the termination functions for our method to apply, thus describe a class of different orderings. We also give a counterexample to a previously published extension of the recursive path ordering into the higher order setting. Regarding another extension we show that our ordering is significantly stronger.