SIMPLE TERMINATION OF REWRITE SYSTEMS

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 ord ers and another one based on preorders (or quasi-orders), We argue tha t there is no reason to choose the second one as the first one has cer tain advantages. Simplification orders are known to be well-founded or ders on terms over a finite signature. This important result no longer holds if we consider infinite signatures. Nevertheless, well-known si mplification orders like the recursive path order are also well-founde d on terms over infinite signatures, provided the underlying precedenc e is well-founded. We propose a new definition of simplification order , which coincides with the old one (based on partial orders) in case o f finite signatures, but which is also well-founded over infinite sign atures and covers orders like the recursive path order. We investigate the properties of the ensuing class of simply terminating systems.