Abstract

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, while 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.

BibTeX Entry

@article{MZ-TCS97,
 author    = "Aart Middeldorp and Hans Zantema",
 title     = "Simple Termination of Rewrite Systems",
 journal   = "Theoretical Computer Science",
 volume    = 175,
 number    = 1,
 pages     = "127--158",
 year      = 1997,
 doi       = "10.1016/S0304-3975(96)00172-7"
}