Simple termination revisited

9Citations
Citations of this article
1Readers
Mendeley users who have this article in their library.
Get full text

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). In the first part of the paper 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.

Cite

CITATION STYLE

APA

Middeldorp, A., & Zantema, H. (1994). Simple termination revisited. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 814 LNAI, pp. 451–465). Springer Verlag. https://doi.org/10.1007/3-540-58156-1_33

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free