On how to move mountains ‘associatively and commutatively’
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.
KeywordsEquivalence Relation Peak Reduction Word Problem Free Algebra Free Abelian Group
Unable to display preview. Download preview PDF.
- [Ba]L.Bachmair “Proof Methods for Equational Theories” Ph.D. Thesis Univ. of Illinois. (1987)Google Scholar
- [Hu 1]G. Huet “Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems” J.ACM 27 797–821 (1980)Google Scholar
- [Hu 2]G.Huet “A complete Proof of Correctness of the Knuth-Bendix Completion Algorithm” J.Com. and Sys. Sci. 27 (1981)Google Scholar
- [Jo-Ki]J. Jouannand and H. Kirchner “Completion of A Set of Rules Modulo A Set of Equations” SIAM J. Computing 15 1155–1194 (1986)Google Scholar
- [Ka-Mu-Na]D.Kapur, D.Musser and P.Narendran “Only Prime Superpositions Need be Considered in the Knuth-Bendix Completion Procedure” J.of Symbolic Computation (1988)Google Scholar
- [Kn-Be]D.Knuth and P.Bendix “Simple Word Problems in Universal Algebras” In Computational Problems in Abstract Algebra, Pergamon Press 263–297 (1970)Google Scholar
- [La-Ba 4]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)Google Scholar
- [La-Ba 8]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)Google Scholar
- [Lai 1]M.Lai “A Peak Reduction in Rewritings of Term Algebras ‘Associatively and Commutatively”’ To appear (1988)Google Scholar
- [Lai 2]M.Lai “A Knuth-Bendix Completion Algorithm Using Peak Reduction Lemma” To appear (1988)Google Scholar
- [Pe]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)Google Scholar
- [Pe-S]G. Peterson and M. Stickel “Complete Sets of Reductions for Some Equational Theories” J.ACM 28 233–264 (1981)Google Scholar