Solving Word Problems in Free Algebras Using Complexity Functions

  • Alex Pelin
  • Jean H. Gallier
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 170)


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.


Normal Form Complexity Function Word Problem Free Algebra Conditional Equation 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    Book, R., Confluent and other Types of Thue Systems, JACM 29 (1982), 171–182.MathSciNetCrossRefzbMATHGoogle Scholar
  2. [2]
    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
  3. [3]
    Dershowitz, N., Orderlngs for Term-Rewriting Systems, Theoretical Computer Science 17 (1982), 279–301.MathSciNetCrossRefzbMATHGoogle Scholar
  4. [4]
    Gallier, J,H. and Book, R.V., Reductions in Tree-Rewriting Systems, to appear in Theoretical Comput er Sci ence (1984).Google Scholar
  5. [5]
    Huet, G., Confluent Reductions: Abstract Properties and Applications to Term-Rewriting Systems, JACM 27(4) (1980), 797–821.MathSciNetCrossRefzbMATHGoogle Scholar
  6. [6]
    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
  7. [7]
    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
  8. [8]
    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
  9. [9]
    Pelin A. and Gallier, J.H., Comput ing Normal Forms Using Complexity Functions over Nk, in preparation.Google Scholar
  10. [10]
    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
  11. [11]
    Siekman, J. and Szabo, P., Universal Unification and Regular Equational ACFM Theories, Technical Report, University of Karlsruhe (1981).Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1984

Authors and Affiliations

  • Alex Pelin
    • 1
  • Jean H. Gallier
    • 2
  1. 1.Department of Computer and Information ScienceTemple UniversityPhiladelphia
  2. 2.Department of Computer and Information ScienceUniversity of PennsylvaniaPhiladelphia

Personalised recommendations