In computational mathematics, a word problem is the problem of deciding whether two given expressions are equivalent with respect to a set of rewriting identities. A prototypical example is the word problem for groups, but there are many other instances as well. Some deep results of computational theory concern the undecidability of this question in many important cases.

In computer 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 a solution to the word problem. For example, imagine that ${\displaystyle x,y,z}$ are symbols representing real numbers - then a relevant solution to the word problem would, given the input ${\displaystyle (x\cdot y)/z\mathrel {\overset {?}{=}} (x/z)\cdot y}$, produce the output EQUAL, and similarly produce NOT_EQUAL from ${\displaystyle (x\cdot y)/z\mathrel {\overset {?}{=}} (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 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. 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. 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.

While the word problem asks whether two terms containing constants are equal, a proper extension of the word problem known as the unification problem asks whether two terms ${\displaystyle t_{1},t_{2}}$ containing variables have instances 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\mathrel {\overset {?}{=}} 8+(-3)}$ is a word problem in the integer group ${\displaystyle \mathbb {Z} }$, while ${\displaystyle 2+x\mathrel {\overset {?}{=}} 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 the substitution ${\displaystyle \{x\mapsto 3\}}$ as a solution.

One of the most deeply studied cases of the word problem is in the theory of semigroups and groups. A timeline of papers relevant to the Novikov–Boone theorem is as follows:

The accessibility problem for string rewriting systems (semi-Thue systems or semigroups) can be stated as follows: Given a semi-Thue system ${\displaystyle T:=(\Sigma ,R)}$ and two words (strings) ${\displaystyle u,v\in \Sigma ^{*}}$, 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.

The accessibility and word problems are undecidable, i.e. there is no general algorithm for solving this problem. 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. Even the word problem restricted to ground terms is not decidable for certain finitely presented semigroups.

Given a presentation ${\displaystyle \langle S\mid {\mathcal {R}}\rangle }$ for a group G, the word problem is the algorithmic problem of deciding, given as input two words in S, whether they represent the same element of G. The word problem is one of three algorithmic problems for groups proposed by Max Dehn in 1911. 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.