Termination of term rewriting by semantic labelling

    Research output: Contribution to journalArticleAcademicpeer-review

    122 Citations (Scopus)
    2 Downloads (Pure)


    A new kind of transformation of term rewriting systems (TRS) is proposed, depending on a choice for a model for the TRS. The labelled TRS is obtained from the original one by labelling operation symbols, possibly creating extra copies of same rules. This construction has the remarkable property that the labelled TRS is terminating if and only if the original TRS is terminating. Although the labelled version has more operation symbols and may have more rules (sometimes infinitely many), termination is of ten easier to prove for the labelled TRS than for the original one. This provides a new technique for proving termination, making classical techniques like path orders and polynomial interpretations applicable even for non-simplifying TRS's. The requirement ofhaving a model can slightly be weakened, yielding a remarkably simple termination proof of the system SUBST of [11] describing explicit substitution in ¿-calculus.
    Original languageEnglish
    Pages (from-to)89-105
    JournalFundamenta Informaticae
    Issue number1-2
    Publication statusPublished - 1995


    Dive into the research topics of 'Termination of term rewriting by semantic labelling'. Together they form a unique fingerprint.

    Cite this