Abstract
In this paper we give another characterization of a set of rules which defines a Church-Rosser reduction on the term algebra specified by some associative and commutative equations. This characterization requires fewer conditions to be satisfied than those previously given in the literature do. As a result, when the required conditions are satisfied, the word problem in the term algebra defined by the set of rules and the set of associative and commutative equations can be solved by successive applications of rewriting to the elements in question.
In addition, what makes this approach different from the others is that notions such as AC-compatibility or coherence modulo AC of reductions induced by sets of rules, which are essential in [Pe-S] or [Jo-Ki] respectively, are not required here. Consequently, a proof of correctness of the completion algorithm (given in [Lai 2]) for constructing a desired set of rules based on this approach can be compared directly with that of Huet in [Hu 2]. In fact, it turns out that all we have to do is to replace terms in [Hu 2] by AC-equivalence classes of terms. The main reason is that all the complications due to AC-compatibility or coherence modulo AC simply are not present here.
Finally, we shall discuss how to minimize the unnecessary computation of some critical pairs during the completion.
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
Supported by the U.K. Science and Engineering Research Council under grant GR/E83634
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
L.Bachmair “Proof Methods for Equational Theories” Ph.D. Thesis Univ. of Illinois. (1987)
G. Huet “Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems” J.ACM 27 797–821 (1980)
G.Huet “A complete Proof of Correctness of the Knuth-Bendix Completion Algorithm” J.Com. and Sys. Sci. 27 (1981)
J. Jouannand and H. Kirchner “Completion of A Set of Rules Modulo A Set of Equations” SIAM J. Computing 15 1155–1194 (1986)
D.Kapur, D.Musser and P.Narendran “Only Prime Superpositions Need be Considered in the Knuth-Bendix Completion Procedure” J.of Symbolic Computation (1988)
D.Knuth and P.Bendix “Simple Word Problems in Universal Algebras” In Computational Problems in Abstract Algebra, Pergamon Press 263–297 (1970)
D.S.Lankford and A.M.Ballantyne “Decision Procedures for Simple Equational Theories with Permutative Equations: Complete Sets of Permutative Reductions” Tech. Rep., Maths. Dep., Univ. of Texas, April (1977)
D.S.Lankford and A.M.Ballantyne “Decision Procedures for Simple Equational Theories with Permutative Equations: Complete Sets of Permutative Reductions” Tech. Rep., Maths. Dep., Univ. of Texas, August (1977)
M.Lai “A Peak Reduction in Rewritings of Term Algebras ‘Associatively and Commutatively”’ To appear (1988)
M.Lai “A Knuth-Bendix Completion Algorithm Using Peak Reduction Lemma” To appear (1988)
J. Pedersen “Obtaining Complete Sets of Reductions and Equations Without Using Special Unification Algorithms” Proc. Eurocal 85 Lect. Notes in Comp. Sci. 204 422–423 (1985)
G. Peterson and M. Stickel “Complete Sets of Reductions for Some Equational Theories” J.ACM 28 233–264 (1981)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1989 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Lai, M. (1989). On how to move mountains ‘associatively and commutatively’. 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_109
Download citation
DOI: https://doi.org/10.1007/3-540-51081-8_109
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