Problème du mot

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. A deep result of computational theory is that answering this question is in many important cases undecidable. 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 are symbols representing real numbers - then a relevant solution to the word problem would, given the input , produce the output EQUAL, and similarly produce NOT_EQUAL from . 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. For example one might decide that is the normal form of , , and , 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 which 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 containing variables have instances that are equal, or in other words whether the equation has any solutions. As a common example, is a word problem in the integer group Z, while is a unification problem in the same group; since the former terms happen to be equal in Z, the latter problem has the substitution as a solution.