Total termination of term rewriting

M.C.F. Ferreira, H. Zantema

    Research output: Contribution to journalArticleAcademicpeer-review

    14 Citations (Scopus)
    2 Downloads (Pure)


    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.
    Original languageEnglish
    Pages (from-to)133-162
    Number of pages30
    JournalApplicable Algebra in Engineering, Communication and Computing
    Issue number2
    Publication statusPublished - 1996

    Fingerprint Dive into the research topics of 'Total termination of term rewriting'. Together they form a unique fingerprint.

    Cite this