Abstract
The effective calculation with term rewriting systems presumes termination. Orderings on terms are able to guarantee termination. This report deals with some of those term orderings: Several path and decomposition orderings and the Knuth-Bendix ordering. We pursue three aims:
-
•Known orderings will be newly defined.
-
•New ordering methods will be introduced: We will extend existing orderings by adding the principle of status (see [KL80]).
-
•The comparison of the power as well as the time behaviour of all orderings will be discussed.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
J. Avenhaus, R. Göbel, B. Gramlich, K. Madlener, J. Steinbach 1987: TRSPEC: A Term Rewriting Based System for Algebraic Specifications, Proc. 1st Int. Workshop on Conditional Rewriting Systems, LNCS 308, Orsay, 245–248
M. Dauchet 1988: Termination of rewriting is undecidable in the one rule case, Proc. 14th Mathematical foundations of computer science, LNCS 324, Carlsbad, 262–268
N. Dershowitz 1985: Termination, Proc. 1st RTA, LNCS 202, Dijon, 180–224
N. Dershowitz 1982: Orderings for term rewriting systems, J. Theor. Comp. Sci., Vol. 17, No. 3, 279–301
J.-P. Jouannaud, P. Lescanne, F. Reinig: Recursive decomposition ordering, I.F.I.P. Working Conf. on Formal Description of Programming Concepts II, North Holland, Garmisch Partenkirchen, 331–348
D. E. Knuth, P. B. Bendix: Simple word problems in universal algebras, Computational problems in abstract algebra, Pergamon Press, 263–297
S. Kamin, J.-J. Lévy: Attempts for generalizing the recursive path orderings, Unpublished manuscript, Dept. of Computer Science, Univ. of Illinois
D. Kapur, P. Narendran, G. Sivakumar 1985: A path ordering for proving termination of term rewriting systems, Proc. 10th CAAP, LNCS 185, 173–187
D. S. Lankford 1979: On proving term rewriting systems are noetherian, Memo MTP-3, Mathematics Dept., Louisiana Tech. Univ., Ruston
D. S. Lankford 1977: Some approaches to equality for computational logic: A survey and assessment, Report ATP-36, Depts. of Mathematics and Computer Science, Univ. of Texas, Austin
P. Lescanne 1984: Uniform termination of term rewriting systems — the recursive decomposition ordering with status, Proc. 9th CAAP, Cambridge University Press, Bordeaux, 182–194
U. Martin 1987: How to choose the weights in the Knuth-Bendix ordering, Proc. 2nd RTA, LNCS 256, Bordeaux, 42–53
D. A. Plaisted: A recursively defined ordering for proving termination of term rewriting systems, Report UIUCDCS-R-78-943, Dept. of Computer Science, Univ. of Illinois
M. Rusinowitch 1987: Path of subterms ordering and recursive decomposition ordering revisited, J. Symbolic Computation 3 (1 & 2), 117–131
C. C. Sims 1987: Verifying nilpotence, J. Symbolic Computation 3 (1 & 2), 231–247
J. Steinbach: Term orderings with status, SEKI REPORT SR-88-12, Artificial Intelligence Laboratories, Dept. of Computer Science, Univ. of Kaiserslautern
J. Steinbach: Comparison of simplification orderings, SEKI REPORT SR-88-02. Artificial Intelligence Laboratories, Dept. of Computer Science, Univ. of Kaiserslautern
J. Steinbach: Orderings for term rewriting systems, M.S. thesis, Dept. of Computer Science, Univ. of Kaiserslautern (in German)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1989 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Steinbach, J. (1989). Extensions and comparison of simplification orderings. In: Dershowitz, N. (eds) Rewriting Techniques and Applications. RTA 1989. Lecture Notes in Computer Science, vol 355. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-51081-8_124
Download citation
DOI: https://doi.org/10.1007/3-540-51081-8_124
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-51081-9
Online ISBN: 978-3-540-46149-4
eBook Packages: Springer Book Archive