A monotonic higher-order semantic path ordering

Abstract

There is an increasing use of (first- and higher-order) rewrite rules in many programming languages and logical systems. The recursive path ordering (RPO) is a well-known tool for proving termination of such rewrite rules in the first-order case. However, RPO has some weaknesses. For instance, since it is a simplification ordering, it can only handle simply terminating systems. Several techniques have been developed for overcoming these weaknesses of RPO. A very recent such technique is the monotonic semantic path ordering (MSPO), a simple and easily automatable ordering which generalizes other more ad-hoc methods. Another recent extension of RPO is its higher-order version HORPO. HORPO is an ordering on terms of a typed lambda-calculus generated by a signature of higher-order function symbols. Although many interesting examples can be proved terminating using HORPO, it inherits the weaknesses of the first-order RPO. Therefore, there is an obvious need for higher-order termination orderings without these weaknesses. Here we define the first such ordering, the monotonic higher-order semantic path ordering (MHOSPO), which is still automatable like MSPO. We give evidence of its power by means of several natural and non-trivial examples which cannot be handled by HORPO.