Total termination of term rewriting

We investigate proving termination of term rewriting systems by a compositional interpretation of terms in a total well-founded order. This kind of termination is calledtotal termination. Equivalently total termination can be characterized by the existence of an order on ground terms which is total, wellfounded and closed under contexts. For finite signatures, total termination implies simple termination. The converse does not hold. However, total termination generalizes most of the usual techniques for proving termination (including the well-known recursive path order). It turns out that for this kind of termination the only interesting orders below 0 are built from the natural numbers by lexicographic product and the multiset construction. By examples we show that both constructions are essential. Most of the techniques used are based on ordinal arithmetic