Abstract
In this paper we introduce a new class of orderings — associative path orderings — for proving termination of associative commutative term rewriting systems. These orderings are based on the concept of simplification orderings and extend the well-known recursive path orderings to E-congruence classes, where E is an equational theory consisting of associativity and commutativity axioms. The associative path ordering is similar to another termination ordering for proving AC termination, described in Dershowitz, et al. (83), which is also based on the idea of transforming terms. Our ordering is conceptually simpler, however, since any term is transformed into a single term, whereas in Dershowitz, et al. (83) the transform of a term is a multiset of terms. More important yet, we show how to lift our ordering to non-ground terms, which is essential for applications of the Knuth-Bendix completion method but was not possible with the previous ordering.
Associative path orderings require less expertise than polynomial orderings. They are applicable to term rewriting systems for which a precedence ordering on the set of operator symbols can be defined that satisfies a certain condition, the associative pair condition. The precedence ordering can often be derived from the structure of the reduction rules. We include termination proofs for various term rewriting systems (for rings, boolean algebra, etc.) and, in addition, point out ways of dealing with equational theories for which the associative pair condition does not hold.
This research was supported in part by the National Science Foundation under grant MCS 83-07755.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
L. Bachmair, Termination orderings for associative commutative rewriting systems, Report UIUCDCS-R-84-1179, Dept. of Computer Science, Univ. of Illinois at Urbana-Champaign, December 1984.
N. Dershowitz, A note on simplification orderings. Information Processing Letters 9 (1979), 212–215.
N. Dershowitz, Orderings for term-rewriting systems, Theoretical Computer Science 17 (1982), 279–301.
N. Dershowitz, J. Hsiang, N.A. Josephson and D.A. Plaisted, Associative-commutative rewriting. Proc. 8th IJCAI, Karlsruhe, 1983, 990–994.
J. Hsiang, Topics in automated theorem proving and program generation, Ph. D. thesis, Univ. of Illinois at Urbana-Champaign, 1983.
G. Huet, Confluent reductions: abstract properties and applications to term rewriting systems. J. ACM 27 (1980), 797–821.
G. Huet and D.C. Oppen, Equations and rewrite rules: a survey. Formal languages: Perspectives and Open Problems (R. Book, ed.), New York: Academic Press, 1980, 349–405.
J.-M. Hullot, A catalogue of canonical term rewriting systems, Technical Report CSL-113, SRI International, Menlo Park, Calif., April 1980.
J.-P. Jouannaud and H. Kirchner, Completion of a set of rules modulo a set of equations, 11th Ann. ACM Symp. on Principles of Programming Languages, Salt Lake City, Utah, 1984, 83–92.
J.-P. Jouannaud and M. Munoz, Termination of a set of rules modulo a set of equations, Proc. 7th Int. Conf. on Automated Deduction (R. Shostak, ed.). Lecture Notes in Comp. Scie. 170, Berlin: Springer Verlag, 1984, 175–193.
D. Knuth and P. Bendix, Simple word problems in universal algebras. Computational Problems in Abstract Algebra (J. Leech, ed.), Pergamon Press, 1970, 263–297.
D. Lankford and A. Ballantyne, Decision procedures for simple equational theories with associative commutative axioms: complete sets of associative commutative reductions. Technical Report, Univ. of Texas at Austin, Dept. of Math. and Comp. Scie., 1977.
M. Munoz, Probleme de terminaison finie des systemes de reecriture equationnels. Ph. D. thesis, Universite Nancy 1, 1983.
G.E. Peterson and M.E. Stickel, Complete sets of reductions for some equational theories, J. ACM 28 (1981), 233–264.
D.A. Plaisted, An associative path ordering, Proc. NSF Workshop on the Rewrite Rule Laboratory, Report 84GEN008, General Electric, Schenectady, New York, April 1984, 123–136.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1985 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bachmair, L., Plaisted, D.A. (1985). Associative path orderings. In: Jouannaud, JP. (eds) Rewriting Techniques and Applications. RTA 1985. Lecture Notes in Computer Science, vol 202. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-15976-2_11
Download citation
DOI: https://doi.org/10.1007/3-540-15976-2_11
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-15976-6
Online ISBN: 978-3-540-39679-6
eBook Packages: Springer Book Archive