Word Problem (mathematics) - The Word Problem in Universal Algebra

The Word Problem in Universal Algebra

In algebra, one often studies infinite algebras which are generated (under the finitary operations of the algebra) by finitely many elements. In this case, the elements of the algebra have a natural system of finite encoding as expressions in terms of the generators and operations. The word problem here is thus to determine, given two such expressions, whether they represent the same element of the algebra.

Roughly speaking, the word problem in an algebra is: given a set of identities E (an equational theory), and two terms x and y, is it possible to transform x into y using the identities in E as rewriting rules in both directions?. The act of discovering such equivalences is known as unification. The process of unification requires discovering substitutions to demonstrate equality. Substitutions may be ordered into a partial order, thus, unification is the act of finding a join on a lattice. In this sense, the word problem on a lattice has a solution, namely, the set of all equivalent words is the free lattice.

One of the most deeply studied cases of the word problem is in the theory of semigroups and groups. There are many groups for which the word problem is not decidable, in that there is no Turing machine that can determine the equivalence of any two words in a finite time.

The word problem on ground terms is not decidable.

The word problem on free Heyting algebras is difficult. The only known results are that the free Heyting algebra on one generator is infinite, and that the free complete Heyting algebra on one generator exists (and has one more element than the free Heyting algebra).