Simple Termination Revisited

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 simpli cation order. The basic ingredient of a simpli cation order is the subterm property, but in the literature two di erent de nitionsare given: one basedon strict partial orders and another one based on preorders or quasi-orders. In the rst part of the paper we argue that there is no reason to choose the second one, while the rst one has certain advantages. Simpli cation orders are known to be well-founded orders on terms over a nite signature. This important result no longer holds if we consider in nite signatures. Nevertheless, well-known simpli cation orders like the recursive path order are also well-founded on terms over in nite signatures, provided the underlying precedence is well-founded. We propose a new de nition of simpli cation order, which coincides with the old one based on partial orders in case of nite s...

• Type: Conference
• Year: 1994
• Where: CADE
• Authors: Aart Middeldorp, Hans Zantema
• Keywords: CADE 1994, Logical Reasoning, Nite Signatures, Partial Orders, Simpli Cation Order