Word problem (mathematics)

A prototypical example is the word problem for groups, but there are many other instances as well.

A deep result of computational theory is that answering this question is in many important cases undecidable.

The question naturally arises of whether there is an algorithm which, given as input two expressions, decides whether they represent the same element.

Such an algorithm is called a solution to the word problem.

are symbols representing real numbers - then a relevant solution to the word problem would, given the input

The most direct solution to a word problem takes the form of a normal form theorem and algorithm which maps every element in an equivalence class of expressions to a single encoding known as the normal form - the word problem is then solved by comparing these normal forms via syntactic equality.

, and devise a transformation system to rewrite those expressions to that form, in the process proving that all equivalent expressions will be rewritten to the same normal form.

[2] But not all solutions to the word problem use a normal form theorem - there are algebraic properties which indirectly imply the existence of an algorithm.

containing variables have instances that are equal, or in other words whether the equation

is a unification problem in the same group; since the former terms happen to be equal in

One of the most deeply studied cases of the word problem is in the theory of semigroups and groups.

[27] Even the word problem restricted to ground terms is not decidable for certain finitely presented semigroups.

It was shown by Pyotr Novikov in 1955 that there exists a finitely presented group G such that the word problem for G is undecidable.

[31] One of the earliest proofs that a word problem is undecidable was for combinatory logic: when are two strings of combinators equivalent?

Because combinators encode all possible Turing machines, and the equivalence of two Turing machines is undecidable, it follows that the equivalence of two strings of combinators is undecidable.

[32] Likewise, one has essentially the same problem in (untyped) lambda calculus: given two distinct lambda expressions, there is no algorithm which can discern whether they are equivalent or not; equivalence is undecidable.

For several typed variants of the lambda calculus, equivalence is decidable by comparison of normal forms.

The word problem for an abstract rewriting system (ARS) is quite succinct: given objects x and y are they equivalent under

[29] The word problem for an ARS is undecidable in general.

However, there is a computable solution for the word problem in the specific case where every object reduces to a unique normal form in a finite number of steps (i.e. the system is convergent): two objects are equivalent under

[33] The Knuth-Bendix completion algorithm can be used to transform a set of equations into a convergent term rewriting system.

In universal algebra one studies algebraic structures consisting of a generating set A, a collection of operations on A of finite arity, and a finite set of identities that these operations must satisfy.

The word problem for an algebra is then to determine, given two expressions (words) involving the generators and operations, whether they represent the same element of the algebra modulo the identities.

[1] The word problem on free Heyting algebras is difficult.

This set of words contains many expressions that turn out to denote equal values in every lattice.

A relation ≤~ on W(X) may be defined inductively by setting w ≤~ v if and only if one of the following holds: This defines a preorder ≤~ on W(X), so an equivalence relation can be defined by w ~ v when w ≤~ v and v ≤~ w. One may then show that the partially ordered quotient set W(X)/~ is the free bounded lattice FX.

[35][36] The equivalence classes of W(X)/~ are the sets of all words w and v with w ≤~ v and v ≤~ w. Two well-formed words v and w in W(X) denote the same value in every bounded lattice if and only if w ≤~ v and v ≤~ w; the latter conditions can be effectively decided using the above inductive definition.

The case of lattices that are not bounded is treated similarly, omitting rules 2 and 3 in the above construction of ≤~.

Bläsius and Bürckert [37] demonstrate the Knuth–Bendix algorithm on an axiom set for groups.

Since the normal forms are literally different, the original terms cannot be equal in every group.