The recursive path and polynomial ordering∗

In most termination tools two ingredients, namely recursive path orderings (RPO) and polynomial interpretation orderings (POLO), are used in a consecutive disjoint way to solve the final constraints generated from the termination problem. We present a simple ordering that combines both RPO and POLO and defines a family of orderings that includes both, and extends them with the possibility of having, at the same time, an RPO-like treatment for some symbols and a POLO-like treatment for the others. The ordering is extended to higher-order terms, providing an automatable use of polynomial interpretations in combination with beta-reduction.