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.
Background and motivation 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 x , y , z {\displaystyle x,y,z} are symbols representing real numbers - then a relevant solution to the word problem would, given the input ( x ⋅ y ) / z = ? ( x / z ) ⋅ y {\displaystyle (x\cdot y)/z\mathrel {\overset {?}{=}} (x/z)\cdot y} , produce the output EQUAL, and similarly produce NOT_EQUAL from ( x ⋅ y ) / z = ? ( x / x ) ⋅ y {\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 x ⋅ y ⋅ z − 1 {\displaystyle x\cdot y\cdot z^{-1}} is the normal form of ( x ⋅ y ) / z {\displaystyle (x\cdot y)/z} , ( x / z ) ⋅ y {\displaystyle (x/z)\cdot y} , and ( y / z ) ⋅ x {\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 t 1 , t 2 {\displaystyle t_{1},t_{2}} containing variables have instances that are equal, or in other words whether the equation t 1 = t 2 {\displaystyle t_{1}=t_{2}} has any solutions. As a common example, 2 + 3 = ? 8 + ( − 3 ) {\displaystyle 2+3\mathrel {\overset {?}{=}} 8+(-3)} is a word problem in the integer group Z {\displaystyle \mathbb {Z} } , while 2 + x = ? 8 + ( − x ) {\displaystyle 2+x\mathrel {\overset {?}{=}} 8+(-x)} is a unification problem in the same group; since the former terms happen to be equal in Z {\displaystyle \mathbb {Z} } , the latter problem has the substitution { x ↦ 3 } {\displaystyle \{x\mapsto 3\}} as a solution.
History 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:
… excerpt ends here. Continue reading the full article.
