Abstract
We show that a simple, and easily implementable, restriction on the recursive path ordering, which we call the “binary path condition”, suffices for establishing termination of extended rewriting modulo associativity and commutativity.
This research was supported in part by the U. S. National Science Foundation under Grants CCR-90-07195 and CCR-90-24271.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Leo Bachmair. Associative-commutative reduction orderings. Information Processing Letters. To appear.
Leo Bachmair and David A. Plaisted. Termination orderings for associative-commutative rewrite systems. J. of Symbolic Computation, vol. 1, pages 329–349 (1985).
Ahlem Ben Cherifa and Pierre Lescanne. Termination of rewriting systems by polynomial interpretations and its implementation. Science of Computer Programming, vol. 9, pages 137–159 (1987).
Dines Bjorner, editor. Proceedings of the IFIP Working Conference on Formal Description of Programming Concepts-II. Garmisch-Partenkirchen, West Germany, North-Holland 1982.
Nachum Dershowitz. Termination of rewriting. J. of Symbolic Computation, vol. 3, pages 69–116 (1987).
Nachum Dershowitz and Jieh Hsiang and N. Alan Josephson and David A. Plaisted. Associative-commutative rewriting. In Proceedings of the Eighth International Joint Conference on Artificial Intelligence, Karlsruhe, West Germany, pages 940–944, 1983.
Nachum Dershowitz and Jean-Pierre Jouannaud. Rewrite systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, chapter 6, pages 243–320, North-Holland, Amsterdam, 1990.
Deepak Kapur, G. Sivakumar and Hantao Zhang. A new method for proving termination of AC-rewrite systems. In Proceedings of the Tenth International Conference of Foundations of Software Technology and Theoretical Computer Science, vol. 472 of Lecture Notes in Computer Science, pages 133–148, Springer-Verlag, Berlin, 1990.
Dallas S. Lankford. On proving term rewriting systems are Noetherian. Memo MTP-3, Mathematics Department, Louisiana Tech. University, Ruston, LA, 1979.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dershowitz, N., Mitra, S. (1993). Path orderings for termination of associative-commutative rewriting. In: Rusinowitch, M., Rémy, JL. (eds) Conditional Term Rewriting Systems. CTRS 1992. Lecture Notes in Computer Science, vol 656. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-56393-8_13
Download citation
DOI: https://doi.org/10.1007/3-540-56393-8_13
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-56393-8
Online ISBN: 978-3-540-47549-1
eBook Packages: Springer Book Archive