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.
Preview
Unable to display preview. Download preview PDF.
References
N. Dershowitz, A Note on Simplification Orderings, Information Processing Letters 9(5), pp. 212–215, 1979.
N. Dershowitz, Orderings for Term-Rewriting Systems, Theoretical Computer Science 17(3), pp. 279–301, 1982.
N. Dershowitz, Termination of Rewriting, Journal of Symbolic Computation 3(1), pp. 69–116, 1987.
N. Dershowitz and J.-P. Jouannaud, Rewrite Systems, in: Handbook of Theoretical Computer Science, Vol. B (ed. J. van Leeuwen), North-Holland, pp. 243–320, 1990.
N. Dershowitz and Z. Manna, Proving Termination with Multiset Orderings, Communications of the ACM 22(8), pp. 465–476, 1979.
M.C.F. Ferreira and H. Zantema, Total Termination of Term Rewriting, Proceedings of the 5th International Conference on Rewriting Techniques and Applications, Montreal, Lecture Notes in Computer Science 690, pp. 213–227, 1993.
J. Gallier, What's so Special about Kruskal's Theorem and the Ordinal γ0? A Survey of Some Results in Proof Theory, Annals of Pure and Applied Logic 53, pp. 199–260, 1991.
G. Huet and D. Lankford, On the Uniform Halting Problem for Term Rewriting Systems, report 283, INRIA, 1978.
J.W. Klop, Term Rewriting Systems, in: Handbook of Logic in Computer Science, Vol. II (eds. S. Abramsky, D. Gabbay and T. Maibaum), Oxford University Press, pp. 1–112, 1992.
J.B. Kruskal, Well-Quasi-Ordering, the Tree Theorem, and Vazsonyi's Conjecture, Transactions of the American Mathematical Society 95, pp. 210–225, 1960.
M. Kurihara and A. Ohuchi, Modularity of Simple Termination of Term Rewriting Systems, Journal of the Information Processing Society Japan 31(5), pp. 633–642, 1990.
E. Ohlebusch, A Note on Simple Termination of Infinite Term Rewriting Systems, report nr. 7, Universität Bielefeld, 1992.
D.A. Plaisted, Equational Reasoning and Term Rewriting Systems, To appear in: Handbook of Logic in Artificial Intelligence and Logic Programming, Vol. I (eds. D. Gabbay and J. Siekmann), Oxford University Press, 1993.
H. Zantema, Termination of Term Rewriting by Interpretation, Proceedings of the 3rd International Workshop on Conditional Term Rewriting Systems, Pont-à-Mousson, Lecture Notes in Computer Science 656, pp. 155–167, 1993. Full version to appear as Termination of Term Rewriting: Interpretation and Type Elimination in Journal of Symbolic Computation, 1994.
H. Zantema, Termination of Term Rewriting by Semantic Labelling, report RUU-CS-93-24, Utrecht University, 1993. Submitted.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Middeldorp, A., Zantema, H. (1994). Simple termination revisited. In: Bundy, A. (eds) Automated Deduction — CADE-12. CADE 1994. Lecture Notes in Computer Science, vol 814. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58156-1_33
Download citation
DOI: https://doi.org/10.1007/3-540-58156-1_33
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-58156-7
Online ISBN: 978-3-540-48467-7
eBook Packages: Springer Book Archive