Simple termination of rewrite systems

A. Middeldorp, H. Zantema

    Research output: Contribution to journalArticleAcademicpeer-review

    37 Citations (Scopus)
    3 Downloads (Pure)


    In this paper we investigate the concept of simple termination. A term rewriting system is called simply terminating if its termination can be proved by means of a simplification order. The basic ingredient of a simplification order is the subterm property, but in the literature two different definitions are given: one based on (strict) partial orders and another one based on preorders (or quasi-orders). We argue that there is no reason to choose the second one as the first one has certain advantages. Simplification orders are known to be well-founded orders on terms over a finite signature. This important result no longer holds if we consider infinite signatures. Nevertheless, well-known simplification orders like the recursive path order are also well-founded on terms over infinite signatures, provided the underlying precedence is well-founded. We propose a new definition of simplification order, which coincides with the old one (based on partial orders) in case of finite signatures, but which is also well-founded over infinite signatures and covers orders like the recursive path order. We investigate the properties of the ensuing class of simply terminating systems.
    Original languageEnglish
    Pages (from-to)127-158
    Number of pages32
    JournalTheoretical Computer Science
    Issue number1
    Publication statusPublished - 1997

    Fingerprint Dive into the research topics of 'Simple termination of rewrite systems'. Together they form a unique fingerprint.

    Cite this