The role of term symmetry in E-completion procedures

ABSTRACT

A major portion of the work and time involved in completing an incomplete set of reductions using an E-completion procedure such as the one described by Knuth and Bendix or its extension to associative-commutative equational theories as described by Peterson and Stickel is spent calculating critical pairs and subsequently testing them for confluence and coherence. A pruning technique which removes from consideration those critical pairs that represent redundant or superfluous information can make a marked difference in the run time and efficiency of an E-completion procedure to which it is applied. In this paper, a technique is proposed for removing critical pairs from consideration at various points before, during, or after their formation. This method is based on the property of term symmetry, which will be defined and explored with respect to E-unification and E-completion procedures. Informally, term symmetry exists between two terms when one can be transformed into the other through variable renaming. By identifying and eliminating various forms of term symmetry which arise between syntactic structures such as, reductions, critical pairs, subterms, and unifiers, it is possible to derive an E-completion procedure that produces the same results without processing these symmetric redundancies.

REFERENCES

• AH74: Alfred V. Aho , John E. Hopcroft, The Design and Analysis of Computer Algorithms, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1974
• CL88: Christian, J., and Lincoln, P. (1988) "Adventures in associative-commutative unification."Technical Report ACA-ST-275-87, Microelectronics and Computer Technology Corp., Austin, TX.
• Fa84: François Fages, Associative-Commutative Unification, Proceedings of the 7th International Conference on Automated Deduction, p.194-208, May 14-16, 1984
• HO80: Huet, G., and Oppen, D. (1980) "Equations and rewrite rules: a survey." Perspectives and Open Problems, R. Book, ed., Academic Press, Orlando, FL.
• Hu78: Huet, G. (1978). "An algorithm to generate the basis of solutions to homogeneous linear diophantine equations."Information Processing Letters, volume 7, pp. 144-147.
• JK86: Jean-Pierre Jouannaud , Hélène Kirchner, Completion of a set of rules modulo a set of equations, SIAM Journal on Computing, v.15 n.4, p.1155-1194, Nov. 1986 [doi>10.1137/0215084]
• KM86: Kapur, D., Musser, D., and Narendran, P. (1986). "Only prime superpositions need be considered in the Knuth-Bendix completion procedure." Technical Report, General Electric Research and Development Center, Schenectady, NY.
• KB70: Knuth, D., and Bendix, P. (1970). "Simple word problems in universal algebras." Computational Problems in Abstract Algebras, J. Leech, ed., Pergamon Press, Oxford, England, pp. 263-297.
• La87: Lankford, D. (1987). "Non-negative basis algorithms for linear equations with integer coefficients." Technical Report, Louisiana Tech University, Ruston, LA.
• LS76: Livesey, M., and Siekmarm, J. (1976). "Unification of A+C-terms (bags) and A + C + I-terms (sets)." Technical Report, Universitat Karlsruhe, Karlsruhe, West Germany.
• Ma88: Blayne E. Mayfield , Ralph W. Wilkerson, The role of term symmetry in e-unification and e-completion, 1988
• PS81: Gerald E. Peterson , Mark E. Stickel, Complete Sets of Reductions for Some Equational Theories, Journal of the ACM (JACM), v.28 n.2, p.233-264, April 1981 [doi>10.1145/322248.322251]
• Ro65: J. A. Robinson, A Machine-Oriented Logic Based on the Resolution Principle, Journal of the ACM (JACM), v.12 n.1, p.23-41, Jan. 1965 [doi>10.1145/321250.321253]
• Si79: Jörg H. Siekmann, Matching under commutativity, Proceedings of the International Symposiumon on Symbolic and Algebraic Computation, p.531-545, June 01, 1979
• St75: Stickel, M. (1975). "A complete unification algorithm for associative-commutative functions." Proceedings of the 4th International Joint Conference on Artificial Intelligence, Tbilisi, pp. 71-82.
• Ye85: Kathy Yelick, Combining unification algorithms for confined regular equational theories, Proc. of the first international conference on Rewriting techniques and applications, p.365-380, December 1985, Dijon, France

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES

Additional Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES

General Terms:
Algorithms, Theory