Solving Word Problems in Free Algebras Using Complexity Functions
We present a new method for solving word problems using complexity functions. Complexity functions are used to compute normal forms. Given a set of (conditional) equations E, complexity functions are used to convert these equations into reductions (rewrite rules decreasing the complexity of terms). Using the top-down reduction extension Rep induced by a set of equations E and a compIexity function, we investigate properties which guarantee that any two (ground) terms t1 and t2 are congruent modulo the congruence ≌E if and only if Rep(t1)=Rep ( t2). Our method actually consists in computing Rep incrementally, as the composition of a sequence of top-down reduction extensions induced by possibly different complexity functions. This method relaxes some of the restrictions imposed by the Cburch-Rosser property.
KeywordsNormal Form Complexity Function Word Problem Free Algebra Conditional Equation
Unable to display preview. Download preview PDF.
- Brand, D., Darringer, J., and Joyner, W., Completeness of Conditional Reductions, IBM Technical Report RC-7404 (1978), T.J. Watson Research Center, Yorktown Heights, N.Y.Google Scholar
- Gallier, J,H. and Book, R.V., Reductions in Tree-Rewriting Systems, to appear in Theoretical Comput er Sci ence (1984).Google Scholar
- Huet, G. and Oppen, D., Equations and Rewrite Ru]es, in Formal Languages: Perspec tives and Open Problems, R.V. Book, Ed., Academic Press (1980), 349–405.Google Scholar
- Knuth, D. and Bendix, P., Simple Word Problems in Universal Algebras, In Computational Problems in Abst ract Algebra, Leach J., Ed., Pergamon Press (1970), 263–297.Google Scholar
- Lankford, D.S. and Ballantyne, A.M., Decision Procedures for Simple Equational Theories with Permutative Axioms: Complete Sets of Permutative Reductions, Report ATP-37, Department of Mathematics and Computer Science, University of Texas, Austin, Texas (1977).Google Scholar
- Pelin A. and Gallier, J.H., Comput ing Normal Forms Using Complexity Functions over Nk, in preparation.Google Scholar
- Plaisted, D., Well-Founded Orderings for Proving Termination of Systems of Rewrite Rules, Report R-78-932, Department of Computer Science, University of Illinois, Urbana, Ill. (1978).Google Scholar
- Siekman, J. and Szabo, P., Universal Unification and Regular Equational ACFM Theories, Technical Report, University of Karlsruhe (1981).Google Scholar