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
x,y,z
(x ⋅ y)/zl{\overset{?}{=}}(x/z) ⋅ y
EQUAL, and similarly produce NOT_EQUAL from (x ⋅ y)/zl{\overset{?}{=}}(x/x) ⋅ y
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.[1] For example one might decide that
x ⋅ y ⋅ z-1
(x ⋅ y)/z
(x/z) ⋅ y
(y/z) ⋅ x
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
t1,t2
t1=t2
2+3l{\overset{?}{=}}8+(-3)
Z
2+xl{\overset{?}{=}}8+(-x)
Z
\{x\mapsto3\}
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:[3] [4]
The accessibility problem for string rewriting systems (semi-Thue systems or semigroups) can be stated as follows: Given a semi-Thue system
T:=(\Sigma,R)
u,v\in\Sigma*
u
v
R
The accessibility and word problems are undecidable, i.e. there is no general algorithm for solving this problem.[6] 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.[5] Even the word problem restricted to ground terms is not decidable for certain finitely presented semigroups.[7]
\langleS\midl{R}\rangle
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. Alonzo Church observed this in 1936.[9]
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
\stackrel{*}{\leftrightarrow}
\stackrel{*}{\leftrightarrow}
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. The word problems for groups and semigroups can be phrased as word problems for algebras.[1]
The word problem on free Heyting algebras is difficult.[12] The only known results are that the free Heyting algebra on one generator is infinite, and that the free complete Heyting algebra on one generator exists (and has one more element than the free Heyting algebra).
|
|
The word problem on free lattices and more generally free bounded lattices has a decidable solution. Bounded lattices are algebraic structures with the two binary operations ∨ and ∧ and the two constants (nullary operations) 0 and 1. The set of all well-formed expressions that can be formulated using these operations on elements from a given set of generators X will be called W(X). This set of words contains many expressions that turn out to denote equal values in every lattice. For example, if a is some element of X, then a ∨ 1 = 1 and a ∧ 1 = a. The word problem for free bounded lattices is the problem of determining which of these elements of W(X) denote the same element in the free bounded lattice FX, and hence in every bounded lattice.
The word problem may be resolved as follows. 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.[13] [14] 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 table shows an example computation to show that the words x∧z and x∧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 [15] demonstrate the Knuth–Bendix algorithm on an axiom set for groups. The algorithm yields a confluent and noetherian term rewrite system that transforms every term into a unique normal form.[16] 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
((a-1 ⋅ a) ⋅ (b ⋅ b-1))-1l{\overset{R2}{\rightsquigarrow}}(1 ⋅ (b ⋅ b-1))-1l{\overset{R13}{\rightsquigarrow}}(1 ⋅ 1)-1l{\overset{R1}{\rightsquigarrow}}1-1l{\overset{R8}{\rightsquigarrow}}1
b ⋅ ((a ⋅ b)-1 ⋅ a)l{\overset{R17}{\rightsquigarrow}}b ⋅ ((b-1 ⋅ a-1) ⋅ a)l{\overset{R3}{\rightsquigarrow}}b ⋅ (b-1 ⋅ (a-1 ⋅ a))l{\overset{R2}{\rightsquigarrow}}b ⋅ (b-1 ⋅ 1)l{\overset{R11}{\rightsquigarrow}}b ⋅ b-1l{\overset{R13}{\rightsquigarrow}}1
1
1 ⋅ (a ⋅ b)
b ⋅ (1 ⋅ a)
a ⋅ b
b ⋅ a
| A1 | 1 ⋅ x | =x | |
| A2 | x-1 ⋅ x | =1 | |
| A3 | (x ⋅ y) ⋅ z | =x ⋅ (y ⋅ z) |
| R1 | 1 ⋅ x | \rightsquigarrowx | |
| R2 | x-1 ⋅ x | \rightsquigarrow1 | |
| R3 | (x ⋅ y) ⋅ z | \rightsquigarrowx ⋅ (y ⋅ z) | |
| R4 | x-1 ⋅ (x ⋅ y) | \rightsquigarrowy | |
| R8 | 1-1 | \rightsquigarrow1 | |
| R11 | x ⋅ 1 | \rightsquigarrowx | |
| R12 | (x-1)-1 | \rightsquigarrowx | |
| R13 | x ⋅ x-1 | \rightsquigarrow1 | |
| R14 | x ⋅ (x-1 ⋅ y) | \rightsquigarrowy | |
| R17 | (x ⋅ y)-1 | \rightsquigarrowy-1 ⋅ x-1 |