Incomputational mathematics, aword problem is theproblem of deciding whether two given expressions are equivalent with respect to a set ofrewriting identities. A prototypical example is theword problem for groups, but there are many other instances as well. Somedeep results of computational theory concern theundecidability of this question in many important cases.^[1]

Incomputer algebra one often wishes to encode mathematical expressions using an expression tree. But there are often multiple equivalent expression trees. 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 asolution to the word problem. For example, imagine that${\displaystyle x,y,z}$ are symbols representingreal numbers - then a relevant solution to the word problem would, given the input${\displaystyle (x\cdot y)/z\stackrel{?}{=}(x/z)\cdot y}$, produce the outputEQUAL, and similarly produceNOT_EQUAL from${\displaystyle (x\cdot y)/z\stackrel{?}{=}(x/x)\cdot y}$.

The most direct solution to a word problem takes the form of a normal form theorem and algorithm that maps every element in anequivalence class of expressions to a single encoding known as thenormal form - the word problem is then solved by comparing these normal forms viasyntactic equality.^[1] For example one might decide that${\displaystyle x\cdot y\cdot z^{-1}}$ is the normal form of${\displaystyle (x\cdot y)/z}$,${\displaystyle (x/z)\cdot y}$, and${\displaystyle (y/z)\cdot x}$, 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 that indirectly imply the existence of an algorithm.^[1]

While the word problem asks whether two terms containingconstants are equal, a proper extension of the word problem known as theunification problem asks whether two terms${\displaystyle t_1,t_2}$ containingvariables haveinstances that are equal, or in other words whether the equation${\displaystyle t_1=t_2}$ has any solutions. As a common example,${\displaystyle 2+3\stackrel{?}{=}8+(-3)}$ is a word problem in theinteger group${\displaystyle \mathbb{Z}}$,while${\displaystyle 2+x\stackrel{?}{=}8+(-x)}$ is a unification problem in the same group; since the former terms happen to be equal in${\displaystyle \mathbb{Z}}$, the latter problem has thesubstitution${\displaystyle \{x\mapsto 3\}}$ as a solution.

One of the most deeply studied cases of the word problem is in the theory ofsemigroups andgroups. A timeline of papers relevant to theNovikov–Boone theorem is as follows:^[3][4]

• 1910 (1910):Axel Thue poses a general problem of term rewriting on tree-like structures. He states "A solution of this problem in the most general case may perhaps be connected with unsurmountable difficulties".^[5][6]
• 1911 (1911):Max Dehn poses the word problem forfinitely presented groups.^[7]
• 1912 (1912):Dehn presentsDehn's algorithm, and proves it solves the word problem for thefundamental groups of closed orientable two-dimensionalmanifolds of genus greater than or equal to 2.^[8] Subsequent authors have greatly extended it to a wide range ofgroup-theoretic decision problems.^[9][10][11]
• 1914 (1914):Axel Thue poses the word problem for finitely presented semigroups.^[12]
• 1930 (1930) – 1938 (1938):TheChurch–Turing thesis emerges, defining formal notions ofcomputability and undecidability.^[13]
• 1947 (1947):Emil Post andAndrey Markov Jr. independently construct finitely presented semigroups with unsolvable word problem.^[14][15] Post's construction is built onTuring machines while Markov's uses Post's normal systems.^[3]
• 1950 (1950):Alan Turing shows the word problem forcancellation semigroups is unsolvable,^[16] by furthering Post's construction. The proof is difficult to follow but marks a turning point in the word problem for groups.^[3]: 342
• 1955 (1955):Pyotr Novikov gives the first published proof that the word problem for groups is unsolvable, using Turing's cancellation semigroup result.^{[17][3]: 354} The proof contains a "Principal Lemma" equivalent toBritton's Lemma.^[3]: 355
• 1954 (1954) – 1957 (1957):William Boone independently shows the word problem for groups is unsolvable, using Post's semigroup construction.^[18][19]
• 1957 (1957) – 1958 (1958):John Britton gives another proof that the word problem for groups is unsolvable, based on Turing's cancellation semigroups result and some of Britton's earlier work.^[20] An early version of Britton's Lemma appears.^[3]: 355
• 1958 (1958) – 1959 (1959):Boone publishes a simplified version of his construction.^[21][22]
• 1961 (1961):Graham Higman characterises thesubgroups of finitely presented groups withHigman's embedding theorem,^[23] connecting recursion theory with group theory in an unexpected way and giving a very different proof of the unsolvability of the word problem.^[3]
• 1961 (1961) – 1963 (1963):Britton presents a greatly simplified version of Boone's 1959 proof that the word problem for groups is unsolvable.^[24] It uses a group-theoretic approach, in particularBritton's Lemma. This proof has been used in a graduate course, although more modern and condensed proofs exist.^[25]
• 1977 (1977):Gennady Makanin proves that the existential theory of equations overfree monoids is solvable.^[26]

The accessibility problem forstring rewriting systems (semi-Thue systems or semigroups) can be stated as follows: Given a semi-Thue system${\displaystyle T:=(\mathrm{\Sigma },R)}$ and two words (strings)${\displaystyle u,v\in {\mathrm{\Sigma }}^{\ast }}$, can${\displaystyle u}$ be transformed into${\displaystyle v}$ by applying rules from${\displaystyle R}$? Note that the rewriting here is one-way. The word problem is the accessibility problem for symmetric rewrite relations, i.e. Thue systems.^[27]

The accessibility and word problems areundecidable, i.e. there is no general algorithm for solving this problem.^[28] This even holds if we limit the systems to have finite presentations, i.e. a finite set of symbols and a finite set of relations on those symbols.^[27] Even the word problem restricted toground terms is not decidable for certain finitely presented semigroups.^[29][30]

Given apresentation${\displaystyle ⟨S\mid \mathcal{R}⟩}$ for a groupG, the word problem is the algorithmic problem of deciding, given as input two words inS, whether they represent the same element ofG. The word problem is one of three algorithmic problems for groups proposed byMax Dehn in 1911. It was shown byPyotr Novikov in 1955 that there exists a finitely presented groupG such that the word problem forG isundecidable.^[31]

One of the earliest proofs that a word problem is undecidable was forcombinatory logic: when are two strings of combinators equivalent? Because combinators encode all possibleTuring machines, and the equivalence of two Turing machines is undecidable, it follows that the equivalence of two strings of combinators is undecidable.Alonzo Church observed this in 1936.^[32]

Likewise, one has essentially the same problem in (untyped)lambda calculus: given two distinct lambda expressions, there is no algorithm that 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 anabstract rewriting system (ARS) is quite succinct: given objectsx andy are they equivalent under${\displaystyle \stackrel{\ast }{\leftrightarrow }}$?^[29] The word problem for an ARS isundecidable in general. However, there is acomputable 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 isconvergent): two objects are equivalent under${\displaystyle \stackrel{\ast }{\leftrightarrow }}$ if and only if they reduce to the same normal form.^[33]TheKnuth-Bendix completion algorithm can be used to transform a set of equations into a convergentterm rewriting system.

Inuniversal algebra one studiesalgebraic structures consisting of agenerating setA, a collection ofoperations onA 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. The word problems for groups and semigroups can be phrased as word problems for algebras.^[1]

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

The word problem onfree lattices and more generally freebounded lattices has a decidable solution. Bounded lattices are algebraic structures with the twobinary operations ∨ and ∧ and the two constants (nullary operations) 0 and 1. The set of all well-formedexpressions that can be formulated using these operations on elements from a given set of generatorsX will be calledW(X). This set of words contains many expressions that turn out to denote equal values in every lattice. For example, ifa is some element ofX, thena ∨ 1 = 1 anda ∧ 1 =a. The word problem for free bounded lattices is the problem of determining which of these elements ofW(X) denote the same element in the free bounded latticeFX, and hence in every bounded lattice.

The word problem may be resolved as follows. A relation ≤_~ onW(X) may be definedinductively by settingw ≤_~vif and only if one of the following holds:

1.  w =v (this can be restricted to the case wherew andv are elements ofX),
2.  w = 0,
3.  v = 1,
4.  w =w₁ ∨w₂ and bothw₁ ≤_~v andw₂ ≤_~v hold,
5.  w =w₁ ∧w₂ and eitherw₁ ≤_~v orw₂ ≤_~v holds,
6.  v =v₁ ∨v₂ and eitherw ≤_~v₁ orw ≤_~v₂ holds,
7.  v =v₁ ∧v₂ and bothw ≤_~v₁ andw ≤_~v₂ hold.

This defines apreorder ≤_~ onW(X), so anequivalence relation can be defined byw ~v whenw ≤_~v andv ≤_~w. One may then show that thepartially orderedquotient setW(X)/~ is the free bounded latticeFX.^[35][36] Theequivalence classes ofW(X)/~ are the sets of all wordsw andv withw ≤_~v andv ≤_~w. Two well-formed wordsv andw inW(X) denote the same value in every bounded lattice if and only ifw ≤_~v andv ≤_~w; the latter conditions can be effectively decided using the above inductive definition. The table shows an example computation to show that the wordsx∧z andx∧z∧(x∨y) denote the same value in every bounded lattice. 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 theKnuth–Bendix algorithm on an axiom set for groups. The algorithm yields aconfluent andnoetherianterm rewrite system that transforms every term into a uniquenormal form.^[38] The rewrite rules are numbered incontiguous since some rules became redundant and were deleted during the algorithm run.The equality of two terms follows from the axioms if and only if both terms are transformed into literally the same normal form term. For example, the terms

${\displaystyle ((a^{-1}\cdot a)\cdot (b\cdot b^{-1}){)}^{-1}\stackrel{R2}{⇝}(1\cdot (b\cdot b^{-1}){)}^{-1}\stackrel{R13}{⇝}(1\cdot 1{)}^{-1}\stackrel{R1}{⇝}{1}^{-1}\stackrel{R8}{⇝}1}$, and

${\displaystyle b\cdot ((a\cdot b{)}^{-1}\cdot a)\stackrel{R17}{⇝}b\cdot ((b^{-1}\cdot a^{-1})\cdot a)\stackrel{R3}{⇝}b\cdot (b^{-1}\cdot (a^{-1}\cdot a))\stackrel{R2}{⇝}b\cdot (b^{-1}\cdot 1)\stackrel{R11}{⇝}b\cdot b^{-1}\stackrel{R13}{⇝}1}$

share the same normal form, viz.${\displaystyle 1}$; therefore both terms are equal in every group.As another example, the term${\displaystyle 1\cdot (a\cdot b)}$ and${\displaystyle b\cdot (1\cdot a)}$ has the normal form${\displaystyle a\cdot b}$ and${\displaystyle b\cdot a}$, respectively. Since the normal forms are literally different, the original terms cannot be equal in every group. In fact, they are usually different innon-abelian groups.

Group axioms used in Knuth–Bendix completion

A1	${\displaystyle 1\cdot x}$	${\displaystyle =x}$
A2	${\displaystyle x^{-1}\cdot x}$	${\displaystyle =1}$
A3	${\displaystyle (x\cdot y)\cdot z}$	${\displaystyle =x\cdot (y\cdot z)}$

Term rewrite system obtained from Knuth–Bendix completion

R1	${\displaystyle 1\cdot x}$	${\displaystyle ⇝x}$
R2	${\displaystyle x^{-1}\cdot x}$	${\displaystyle ⇝1}$
R3	${\displaystyle (x\cdot y)\cdot z}$	${\displaystyle ⇝x\cdot (y\cdot z)}$
R4	${\displaystyle x^{-1}\cdot (x\cdot y)}$	${\displaystyle ⇝y}$
R8	${\displaystyle 1^{-1}}$	${\displaystyle ⇝1}$
R11	${\displaystyle x\cdot 1}$	${\displaystyle ⇝x}$
R12	${\displaystyle (x^{-1}{)}^{-1}}$	${\displaystyle ⇝x}$
R13	${\displaystyle x\cdot x^{-1}}$	${\displaystyle ⇝1}$
R14	${\displaystyle x\cdot (x^{-1}\cdot y)}$	${\displaystyle ⇝y}$
R17	${\displaystyle (x\cdot y{)}^{-1}}$	${\displaystyle ⇝y^{-1}\cdot x^{-1}}$

• Conjugacy problem
• Group isomorphism problem

• Abstract algebra
• Combinatorics on words
• Rewriting systems
• Computational problems

• CS1 Russian-language sources (ru)
• Articles with short description
• Short description is different from Wikidata
• Pages with timeline metadata