A termination ordering for higher order rewrite systems

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 sufficient properties of the termination functions for our method to apply. Thereby we describe a class of different orderings. Finally we compare our method to previously published extensions of the recursive path ordering into the higher order setting.