View source for Word problem (mathematics)

{{Short description|Decision problem pertaining to equivalence of expressions}}
{{About|algorithmic word problems in mathematics and computer science|the term 'word problem' as often used in education|Word problem (mathematics education)|other uses|Word problem (disambiguation){{!}}Word problem}}

In [[computational mathematics]], a '''word problem''' is the [[decision problem|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 result]]s of computational theory concern the [[undecidable problem|undecidability]] of this question in many important cases.<ref name=Evans/>

== 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 <math>x,y,z</math> are symbols representing [[real number]]s - then a relevant solution to the word problem would, given the input <math>(x \cdot y)/z \mathrel{\overset{?}{=}} (x/z)\cdot y</math>, produce the output <code>EQUAL</code>, and similarly produce <code>NOT_EQUAL</code> from <math>(x \cdot y)/z \mathrel{\overset{?}{=}} (x/x)\cdot y</math>.

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 [[Canonical form|normal form]] - the word problem is then solved by comparing these normal forms via [[syntactic equality]].<ref name=Evans>{{cite journal |last1=Evans |first1=Trevor |author1-link=Trevor Evans (mathematician)|title=Word problems |journal=[[Bulletin of the American Mathematical Society]] |date=1978 |volume=84 |issue=5 |pages=790 |doi=10.1090/S0002-9904-1978-14516-9|doi-access=free }}</ref> For example one might decide that <math>x \cdot y \cdot z^{-1}</math> is the normal form of <math>(x \cdot y)/z</math>, <math>(x/z)\cdot y</math>, and <math>(y/z)\cdot x</math>, 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.<ref>{{cite book |last1=Cohen |first1=Joel S. |title=Computer algebra and symbolic computation: elementary algorithms |date=2002 |publisher=A K Peters |location=Natick, Mass. |isbn=1568811586 |pages=90–92}}</ref> 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.<ref name=Evans/>

While the word problem asks whether two terms containing [[Constant (mathematics)|constants]] are equal, a proper extension of the word problem known as the ''[[unification (computer science)|unification problem]]'' asks whether two terms <math>t_1,t_2</math> containing [[Variable (mathematics)|variables]] have ''instances'' that are equal, or in other words whether the equation <math>t_1 = t_2</math> has any solutions. As a common example, <math>2 + 3 \mathrel{\overset{?}{=}} 8 + (-3)</math> is a word problem in the [[Integer#Algebraic properties|integer group]] <math>\mathbb{Z}</math>,
while <math>2 + x \mathrel{\overset{?}{=}} 8 + (-x)</math> is a unification problem in the same group; since the former terms happen to be equal in <math>\mathbb{Z}</math>, the latter problem has the [[substitution (logic)|substitution]] <math>\{x \mapsto 3\}</math> as a solution.

== History ==

One of the most deeply studied cases of the word problem is in the theory of [[semigroup]]s and [[group (mathematics)|group]]s. A timeline of papers relevant to the [[Novikov–Boone theorem]] is as follows:<ref name=Miller>{{cite journal |last1=Miller |first1=Charles F. |editor1-first=Rod |editor1-last=Downey |title=Turing machines to word problems |journal=Turing's Legacy |date=2014 |pages=330 |doi=10.1017/CBO9781107338579.010 |hdl=11343/51723 |isbn=9781107338579 |url=http://minerva-access.unimelb.edu.au/bitstream/11343/51723/1/cfm-lnl42-turings-legacy-pp329-385-2014.pdf |access-date=6 December 2021}}</ref><ref>{{cite journal |last1=Stillwell |first1=John |title=The word problem and the isomorphism problem for groups |journal=Bulletin of the American Mathematical Society |date=1982 |volume=6 |issue=1 |pages=33–56 |doi=10.1090/S0273-0979-1982-14963-1|doi-access=free }}</ref>

* {{Timeline-event |date={{Start date|1910}}|event=[[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".<ref name=Muller>{{cite arXiv  |last1=Müller-Stach |first1=Stefan |title=Max Dehn, Axel Thue, and the Undecidable |date=12 September 2021 |eprint=1703.09750 |page=13|class=math.HO }}</ref><ref>{{cite journal |last1=Steinby |first1=Magnus |last2=Thomas |first2=Wolfgang |title=Trees and term rewriting in 1910: on a paper by Axel Thue |journal=Bulletin of the European Association for Theoretical Computer Science|volume=72|pages=256–269 |date=2000|mr=1798015|citeseerx=10.1.1.32.8993 |language=English}}</ref>}}
* {{Timeline-event |date={{Start date|1911}}|event=[[Max Dehn]] poses the word problem for [[Presentation of a group#Finitely presented groups|finitely presented groups]].<ref>{{cite journal  | last1=Dehn | first1=Max | author1-link=Max Dehn | title=Über unendliche diskontinuierliche Gruppen | doi=10.1007/BF01456932 | mr=1511645  | year=1911 | journal=[[Mathematische Annalen]] | issn=0025-5831 | volume=71 | issue=1 | pages=116–144| s2cid=123478582 |url=http://gdz.sub.uni-goettingen.de/index.php?id=11&PPN=PPN235181684_0071&DMDID=DMDLOG_0013&L=1}}</ref>}}
* {{Timeline-event |date={{Start date|1912}}|event=Dehn presents [[Dehn's algorithm]], and proves it solves the word problem for the [[fundamental group]]s of closed orientable two-dimensional [[manifold]]s of genus greater than or equal to 2.<ref>{{cite journal | last1=Dehn | first1=Max | author1-link=Max Dehn | title=Transformation der Kurven auf zweiseitigen Flächen | doi=10.1007/BF01456725 | mr=1511705  | year=1912 | journal=[[Mathematische Annalen]] | issn=0025-5831 | volume=72 | issue=3 | pages=413–421| s2cid=122988176 |url=http://gdz.sub.uni-goettingen.de/index.php?id=11&PPN=PPN235181684_0072&DMDID=DMDLOG_0039&L=1}}</ref> Subsequent authors have greatly extended it to a wide range of [[group-theoretic]] decision problems.<ref>{{cite journal|last=Greendlinger|first=Martin|date=June 1959|title=Dehn's algorithm for the word problem|journal=[[Communications on Pure and Applied Mathematics]]|volume=13|issue=1|pages=67–83|doi=10.1002/cpa.3160130108}}</ref><ref>{{cite journal|last=Lyndon|first=Roger C.|author-link=Roger Lyndon|date=September 1966|title=On Dehn's algorithm|journal=Mathematische Annalen|volume=166|issue=3|pages=208–228|doi=10.1007/BF01361168|hdl=2027.42/46211|s2cid=36469569|url=http://gdz.sub.uni-goettingen.de/index.php?id=11&PPN=GDZPPN002296799&L=1|hdl-access=free}}</ref><ref>{{cite journal|author-link1=Paul Schupp|last1=Schupp|first1=Paul E.|date=June 1968|title=On Dehn's algorithm and the conjugacy problem|journal=Mathematische Annalen|volume=178|issue=2|pages=119–130|doi=10.1007/BF01350654|s2cid=120429853|url=http://gdz.sub.uni-goettingen.de/index.php?id=11&PPN=GDZPPN002300036&L=1}}</ref>}}
* {{Timeline-event |date={{Start date|1914}}|event=[[Axel Thue]] poses the word problem for finitely presented semigroups.<ref>{{cite arXiv |last1=Power |first1=James F. |title=Thue's 1914 paper: a translation |date=27 August 2013 |class=cs.FL |eprint=1308.5858}}</ref>}}
* {{Timeline-event |date={{Start date|1930}}|end_date={{End date|1938}}|event=The [[Church–Turing thesis]] emerges, defining formal notions of [[computability]] and undecidability.<ref>See [[History of the Church–Turing thesis]]. The dates are based on [[On Formally Undecidable Propositions of Principia Mathematica and Related Systems]] and [[Systems of Logic Based on Ordinals]].</ref>}}
* {{Timeline-event |date={{Start date|1947}}|event=[[Emil Post]] and [[Andrey Markov Jr.]] independently construct finitely presented semigroups with unsolvable word problem.<ref>{{cite journal |last1=Post |first1=Emil L. |title=Recursive Unsolvability of a problem of Thue |journal=[[Journal of Symbolic Logic]] |date=March 1947 |volume=12 |issue=1 |pages=1–11 |doi=10.2307/2267170 |jstor=2267170 |s2cid=30320278 |url=https://www.wolframscience.com/prizes/tm23/images/Post2.pdf |access-date=6 December 2021}}</ref><ref>{{cite journal |last1=Mostowski |first1=Andrzej |title=A. Markov. Névožmoinost' nékotoryh algoritmov v téorii associativnyh sistém (Impossibility of certain algorithms in the theory of associative systems). Doklady Akadémii Nauk SSSR, vol. 77 (1951), pp. 19–20. |journal=Journal of Symbolic Logic |date=September 1951 |volume=16 |issue=3 |pages=215 |doi=10.2307/2266407|jstor=2266407 }}</ref> Post's construction is built on [[Turing machine]]s while Markov's uses Post's normal systems.<ref name=Miller/>}}
* {{Timeline-event |date={{Start date|1950}}|event=[[Alan Turing]] shows the word problem for [[cancellation semigroup]]s is unsolvable,<ref>{{cite journal |last1=Turing |first1=A. M. |title=The Word Problem in Semi-Groups With Cancellation |journal=[[The Annals of Mathematics]] |date=September 1950 |volume=52 |issue=2 |pages=491–505 |doi=10.2307/1969481|jstor=1969481 }}</ref> by furthering Post's construction. The proof is difficult to follow but marks a turning point in the word problem for groups.{{r|Miller|p=342}}}}
* {{Timeline-event |date={{Start date|1955}}|event=[[Pyotr Novikov]] gives the first published proof that the word problem for groups is unsolvable, using Turing's cancellation semigroup result.<ref>{{cite journal |last=Novikov|first=P. S.|author-link=Pyotr Novikov|year=1955|title=On the algorithmic unsolvability of the word problem in group theory|language=ru| zbl=0068.01301 | journal=[[Proceedings of the Steklov Institute of Mathematics]]|volume=44|pages=1–143}}</ref>{{r|Miller|p=354}} The proof contains a "Principal Lemma" equivalent to [[Britton's Lemma]].{{r|Miller|p=355}}}}
* {{Timeline-event |date={{Start date|1954}}|end_date={{End date|1957}}|event=[[William Boone (mathematician)|William Boone]] independently shows the word problem for groups is unsolvable, using Post's semigroup construction.<ref>{{cite journal |last1=Boone |first1=William W. |title=Certain Simple, Unsolvable Problems of Group Theory. I|journal=Indagationes Mathematicae (Proceedings) |date=1954 |volume=57 |pages=231–237 |doi=10.1016/S1385-7258(54)50033-8}}</ref><ref>{{cite journal |last1=Boone |first1=William W. |title=Certain Simple, Unsolvable Problems of Group Theory. VI |journal=Indagationes Mathematicae (Proceedings) |date=1957 |volume=60 |pages=227–232 |doi=10.1016/S1385-7258(57)50030-9|doi-access=free }}</ref>}}
* {{Timeline-event |date={{Start date|1957}}|end_date={{End date|1958}}|event=[[John Britton (mathematician)|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.<ref>{{cite journal |last1=Britton |first1=J. L. |title=The Word Problem for Groups |journal=Proceedings of the London Mathematical Society |date=October 1958 |volume=s3-8 |issue=4 |pages=493–506 |doi=10.1112/plms/s3-8.4.493}}</ref> An early version of Britton's Lemma appears.{{r|Miller|p=355}}}}
* {{Timeline-event |date={{Start date|1958}}|end_date={{End date|1959}}|event=Boone publishes a simplified version of his construction.<ref>{{cite journal |last=Boone|first=William W.| author-link=William Boone (mathematician) | year=1958|title=The word problem|journal=[[Proceedings of the National Academy of Sciences]]|volume=44|issue=10|pages=1061–1065|url=http://www.pnas.org/cgi/reprint/44/10/1061.pdf|doi=10.1073/pnas.44.10.1061|zbl=0086.24701 |pmc=528693|pmid=16590307|bibcode=1958PNAS...44.1061B|doi-access=free}}</ref><ref>{{cite journal |last1=Boone |first1=William W. |title=The Word Problem |journal=The Annals of Mathematics |date=September 1959 |volume=70 |issue=2 |pages=207–265 |doi=10.2307/1970103|jstor=1970103 }}</ref>}}
* {{Timeline-event |date={{Start date|1961}}|event=[[Graham Higman]] characterises the [[subgroup]]s of finitely presented groups with [[Higman's embedding theorem]],<ref>{{cite journal |title=Subgroups of finitely presented groups |journal=Proceedings of the Royal Society of London. Series A. Mathematical and Physical Sciences |date=8 August 1961 |volume=262 |issue=1311 |pages=455–475 |doi=10.1098/rspa.1961.0132|bibcode=1961RSPSA.262..455H |last1=Higman |first1=G. |s2cid=120100270 }}</ref> connecting recursion theory with group theory in an unexpected way and giving a very different proof of the unsolvability of the word problem.{{r|Miller}}}}
* {{Timeline-event |date={{Start date|1961}} |end_date={{End date|1963}}|event=Britton presents a greatly simplified version of Boone's 1959 proof that the word problem for groups is unsolvable.<ref>{{cite journal |last1=Britton |first1=John L. |title=The Word Problem |journal=The Annals of Mathematics |date=January 1963 |volume=77 |issue=1 |pages=16–32 |doi=10.2307/1970200|jstor=1970200 }}</ref> It uses a group-theoretic approach, in particular [[Britton's Lemma]]. This proof has been used in a graduate course, although more modern and condensed proofs exist.<ref>{{cite web |last1=Simpson |first1=Stephen G. |title=A Slick Proof of the Unsolvability of the Word Problem for Finitely Presented Groups |url=http://www.personal.psu.edu/t20/logic/seminar/050517.pdf |access-date=6 December 2021 |date=18 May 2005}}</ref>}}
* {{Timeline-event |date={{Start date|1977}}|event=Gennady Makanin proves that the existential theory of equations over [[free monoid]]s is solvable.<ref>{{cite journal |title=Subgroups of finitely presented groups |journal=Mathematics of the USSR-Sbornik |date=13 February 1977 |volume=103 |issue=145 |pages=147–236 |doi=10.1070/SM1977v032n02ABEH002376}}</ref>}}

== The word problem for semi-Thue systems ==

The accessibility problem for [[string rewriting system]]s (semi-Thue systems or semigroups) can be stated as follows: Given a semi-Thue system <math>T:=(\Sigma, R)</math> and two words (strings) <math>u, v \in \Sigma^*</math>, can <math>u</math> be transformed into <math>v</math> by applying rules from <math>R</math>? Note that the rewriting here is one-way. The word problem is the accessibility problem for symmetric rewrite relations, i.e. Thue systems.<ref name=Matiyasevich>{{cite journal |last1=Matiyasevich |first1=Yuri |last2=Sénizergues |first2=Géraud |title=Decision problems for semi-Thue systems with a few rules |journal=Theoretical Computer Science |date=January 2005 |volume=330 |issue=1 |pages=145–169 |doi=10.1016/j.tcs.2004.09.016|doi-access=free }}</ref>

The accessibility and word problems are [[Undecidable problem|undecidable]], i.e. there is no general algorithm for solving this problem.<ref>{{cite book |last1=Davis |first1=Martin |chapter=What is a Computation? |title=Mathematics Today Twelve Informal Essays |date=1978 |pages=257–259 |doi=10.1007/978-1-4613-9435-8_10 |isbn=978-1-4613-9437-2 |chapter-url=https://www.cs.princeton.edu/courses/archive/spring11/cos116/handouts/daviscomputation.pdf |access-date=5 December 2021}}</ref> 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.<ref name=Matiyasevich/> Even the word problem restricted to [[ground term]]s is not decidable for certain finitely presented semigroups.<ref name=Nipkow/><ref>
* {{cite journal |last1=Matiyasevich |first1=Yu. V.|title= Простые примеры неразрешимых ассоциативных исчислений  |trans-title=Simple examples of undecidable associative calculi |journal=[[Proceedings of the USSR Academy of Sciences|Doklady Akademii Nauk SSSR]] |date=1967 |volume=173|issue=6|pages=1264–1266|url=http://mi.mathnet.ru/eng/dan/v173/i6/p1264 |language=Russian |issn=0869-5652}}
* {{cite journal |last1=Matiyasevich |first1=Yu. V. |title=Simple examples of undecidable associative calculi |journal=Soviet Mathematics |date=1967 |volume=8|issue=2 |pages=555–557|issn=0197-6788}}</ref>

==The word problem for groups==
{{main|Word problem for groups}}

Given a [[group presentation|presentation]] <math>\langle S\mid \mathcal{R} \rangle</math> 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 problem|undecidable]].<ref>{{Cite journal|last1=Novikov|first1=P. S.|author1-link=Pyotr Novikov|title=On the algorithmic unsolvability of the word problem in group theory|journal=Trudy Mat. Inst. Steklov|volume=44|year=1955|pages=1–143|language=ru}}</ref>

== The word problem in combinatorial calculus and lambda calculus ==
{{main | Combinatory logic#Undecidability of combinatorial calculus}}
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 machine]]s, 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.<ref>{{cite book |last1=Statman |first1=Rick |chapter=On the Word Problem for Combinators |title=Rewriting Techniques and Applications |series=Lecture Notes in Computer Science |date=2000 |volume=1833 |pages=203–213 |doi=10.1007/10721975_14|isbn=978-3-540-67778-9 }}</ref>

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; [[Lambda calculus#Undecidability of equivalence|equivalence is undecidable]]. For several typed variants of the lambda calculus, equivalence is decidable by comparison of normal forms.

== The word problem for abstract rewriting systems ==
[[File:Solving the word problem without and with completion_svg.svg|thumb|Solving the word problem: deciding if <math>x \stackrel{*}{\leftrightarrow} y</math> usually requires heuristic search ({{color|#c00000|red}}, {{color|#00c000|green}}), while deciding <math>x\downarrow = y\downarrow</math> is straightforward ({{color|#808080|grey}}).]]
The word problem for an [[abstract rewriting system]] (ARS) is quite succinct: given objects ''x'' and ''y'' are they equivalent under <math>\stackrel{*}{\leftrightarrow}</math>?<ref name=Nipkow>{{cite book |last1=Baader |first1=Franz |last2=Nipkow |first2=Tobias |title=Term Rewriting and All That |date=5 August 1999 |publisher=Cambridge University Press |isbn=978-0-521-77920-3 |pages=59–60 |url=https://books.google.com/books?id=N7BvXVUCQk8C&pg=PA59 |language=en}}</ref> The word problem for an ARS is [[undecidable problem|undecidable]] in general. However, there is a [[computable function|computable]] 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 is ''convergent''): two objects are equivalent under <math>\stackrel{*}{\leftrightarrow}</math> if and only if they reduce to the same normal form.<ref>{{cite journal |last1=Beke |first1=Tibor |title=Categorification, term rewriting and the Knuth–Bendix procedure |journal=Journal of Pure and Applied Algebra |date=May 2011 |volume=215 |issue=5 |page=730 |doi=10.1016/j.jpaa.2010.06.019|doi-access=free }}</ref>
The [[Knuth-Bendix completion algorithm]] can be used to transform a set of equations into a convergent [[term rewriting system]].

== The word problem in universal algebra ==

In [[universal algebra]] one studies [[algebraic structure]]s consisting of a [[generating set]] ''A'', a collection of [[operation (mathematics)|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.<ref name=Evans/>

The word problem on free [[Heyting algebra]]s is difficult.<ref>Peter T. Johnstone, ''Stone Spaces'', (1982) Cambridge University Press, Cambridge, {{isbn|0-521-23893-5}}. ''(See chapter 1, paragraph 4.11)''</ref>  
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 for free lattices==

{| style="float:right; border: 1px solid #808080"
|+ Example computation of ''x''∧''z'' ~ ''x''∧''z''∧(''x''∨''y'')
|-
|
{| style=" border: 1px solid #808080"
|-
|
| 
| align="right"|''x''∧''z''∧(''x''∨''y'') || ≤<sub>~</sub> || ''x''∧''z''
|-
| by 5.
| since
| align="right"|''x''∧''z'' || ≤<sub>~</sub> || ''x''∧''z''
|-
| by 1.
| since
| align="right"|''x''∧''z'' || = || ''x''∧''z''
|-
| &nbsp;
|-
| &nbsp;
|}
| 
{| style=" border: 1px solid #808080"
|-
|
|
| align="right"| ''x''∧''z'' || ≤<sub>~</sub> || ''x''∧''z''∧(''x''∨''y'')
|-
| by 7.
| since 
| align="right"|''x''∧''z'' || ≤<sub>~</sub> || ''x''∧''z''
| and 
|
|
| align="right"|''x''∧''z'' || ≤<sub>~</sub> || ''x''∨''y''
|-
| by 1.
| since
| align="right"|''x''∧''z'' || = || ''x''∧''z''
|
| by 6.
| since 
| align="right"|''x''∧''z'' || ≤<sub>~</sub> || ''x''
|-
|
|
|  ||   ||
|
| by 5.
| since 
| align="right"|''x'' || ≤<sub>~</sub> || ''x''
|-
|
|
|  ||   ||
|
| by 1.
| since 
| align="right"|''x'' || = || ''x''
|}
|}

The word problem on [[free lattice]]s and more generally free [[bounded lattice]]s has a decidable solution. Bounded lattices are algebraic structures with the two [[binary operation]]s ∨ and ∧ and the two constants ([[nullary operation]]s) 0 and 1. The set of all well-formed [[term (logic)|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''&thinsp;∨&thinsp;1 = 1 and ''a''&thinsp;∧&thinsp;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 ≤<sub>~</sub> on '''W'''(''X'') may be defined [[mathematical induction|inductively]] by setting ''w'' ≤<sub>~</sub> ''v'' [[if and only if]] one of the following holds:
# &nbsp; ''w'' = ''v'' (this can be restricted to the case where ''w'' and ''v'' are elements of ''X''),
# &nbsp; ''w'' = 0,
# &nbsp; ''v'' = 1,
# &nbsp; ''w'' = ''w''<sub>1</sub> ∨ ''w''<sub>2</sub> and both ''w''<sub>1</sub> ≤<sub>~</sub> ''v'' and ''w''<sub>2</sub> ≤<sub>~</sub> ''v'' hold,
# &nbsp; ''w'' = ''w''<sub>1</sub> ∧ ''w''<sub>2</sub> and either ''w''<sub>1</sub> ≤<sub>~</sub> ''v'' or ''w''<sub>2</sub> ≤<sub>~</sub> ''v'' holds,
# &nbsp; ''v'' = ''v''<sub>1</sub> ∨ ''v''<sub>2</sub> and either ''w'' ≤<sub>~</sub> ''v''<sub>1</sub> or ''w'' ≤<sub>~</sub> ''v''<sub>2</sub> holds,
# &nbsp; ''v'' = ''v''<sub>1</sub> ∧ ''v''<sub>2</sub> and both ''w'' ≤<sub>~</sub> ''v''<sub>1</sub> and ''w'' ≤<sub>~</sub> ''v''<sub>2</sub> hold.

This defines a [[preorder]] ≤<sub>~</sub> on '''W'''(''X''), so an [[equivalence relation]] can be defined by ''w'' ~ ''v'' when ''w'' ≤<sub>~</sub> ''v'' and ''v'' ≤<sub>~</sub> ''w''. One may then show that the [[partially ordered set|partially ordered]] [[quotient set]] '''W'''(''X'')/~ is the free bounded lattice ''FX''.<ref>{{cite journal |last1=Whitman |first1=Philip M.|author-link=Philip M. Whitman |title=Free Lattices |journal=The Annals of Mathematics |date=January 1941 |volume=42 |issue=1 |pages=325–329 |doi=10.2307/1969001|jstor=1969001}}</ref><ref>{{Cite journal|doi = 10.2307/1968883|jstor = 1968883|last1 = Whitman|first1 = Philip M.|title = Free Lattices II|journal = Annals of Mathematics|year = 1942|volume = 43|issue = 1|pages = 104–115}}</ref> The [[equivalence class]]es of '''W'''(''X'')/~ are the sets of all words ''w'' and ''v'' with ''w'' ≤<sub>~</sub> ''v'' and ''v'' ≤<sub>~</sub> ''w''. Two well-formed words ''v'' and ''w'' in '''W'''(''X'') denote the same value in every bounded lattice if and only if ''w'' ≤<sub>~</sub> ''v'' and ''v'' ≤<sub>~</sub> ''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 ≤<sub>~</sub>.

==Example: A term rewriting system to decide the word problem in the free group==

Bläsius and Bürckert 
<ref>{{cite book| title=Deduktionsssysteme| year=1992| pages=291| publisher=Oldenbourg| editor=K. H. Bläsius and H.-J. Bürckert}}; here: p. 126, 134</ref>
demonstrate the [[Knuth–Bendix algorithm]] on an axiom set for groups. 
The algorithm yields a [[Confluence (abstract rewriting)|confluent]] and [[Abstract rewriting system#Termination and convergence|noetherian]] [[rewrite system#Term rewriting systems|term rewrite system]] that transforms every term into a unique [[Normal form (abstract rewriting)|normal form]].<ref>Apply rules in any order to a term, as long as possible; the result doesn't depend on the order; it is the term's normal form.</ref> 
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
:<math>((a^{-1} \cdot a) \cdot (b \cdot b^{-1}))^{-1} \mathrel{\overset{R2}{\rightsquigarrow}} (1 \cdot (b \cdot b^{-1}))^{-1} \mathrel{\overset{R13}{\rightsquigarrow}} (1 \cdot 1)^{-1} \mathrel{\overset{R1}{\rightsquigarrow}} 1 ^{-1} \mathrel{\overset{R8}{\rightsquigarrow}} 1</math>, and
:<math>b \cdot ((a \cdot b)^{-1} \cdot a) \mathrel{\overset{R17}{\rightsquigarrow}} b \cdot ((b^{-1} \cdot a^{-1}) \cdot a) \mathrel{\overset{R3}{\rightsquigarrow}} b \cdot (b^{-1} \cdot (a^{-1} \cdot a)) \mathrel{\overset{R2}{\rightsquigarrow}} b \cdot (b^{-1} \cdot 1) \mathrel{\overset{R11}{\rightsquigarrow}} b \cdot b^{-1} \mathrel{\overset{R13}{\rightsquigarrow}} 1</math>
share the same normal form, viz. <math>1</math>; therefore both terms are equal in every group.
As another example, the term <math>1 \cdot (a \cdot b)</math> and <math>b \cdot (1 \cdot a)</math> has the normal form <math>a \cdot b</math> and <math>b \cdot a</math>, respectively. Since the normal forms are literally different, the original terms cannot be equal in every group. In fact, they are usually different in [[non-abelian group]]s.

{| style="border: 1px solid grey; float: left; margin: 1em 1em;"
|+ Group axioms used in Knuth–Bendix completion
|- 
| '''A1''' || <math>1 \cdot x</math> || <math>= x</math>
|-
| '''A2''' || <math>x^{-1} \cdot x</math> || <math>= 1</math>
|-
| '''A3''' &nbsp; &nbsp; || <math>(x \cdot y) \cdot z</math> || <math>= x \cdot (y \cdot z)</math>
|}
{| style="border: 1px solid grey; float: left; margin: 1em 1em;"
|+ Term rewrite system obtained from Knuth–Bendix completion
|-
| '''R1''' || <math>1 \cdot x</math> || <math>\rightsquigarrow x</math>
|-
| '''R2''' || <math>x^{-1} \cdot x</math> || <math>\rightsquigarrow 1</math>
|-
| '''R3''' || <math>(x \cdot y) \cdot z</math> || <math>\rightsquigarrow x \cdot (y \cdot z)</math>
|-
| '''R4''' || <math>x^{-1} \cdot (x \cdot y)</math> || <math>\rightsquigarrow y</math>
|-
| '''R8''' || <math>1^{-1}</math> || <math>\rightsquigarrow 1</math>
|-
| '''R11''' || <math>x \cdot 1</math> || <math>\rightsquigarrow x</math>
|-
| '''R12''' || <math>(x^{-1})^{-1}</math> || <math>\rightsquigarrow x</math>
|-
| '''R13''' || <math>x \cdot x^{-1}</math> || <math>\rightsquigarrow 1</math>
|-
| '''R14''' || <math>x \cdot (x^{-1} \cdot y)</math> || <math>\rightsquigarrow y</math>
|-
| '''R17'''  &nbsp; &nbsp; || <math>(x \cdot y)^{-1}</math> || <math>\rightsquigarrow y^{-1} \cdot x^{-1}</math>
|}
{{clear}}

==See also==
* [[Conjugacy problem]]
* [[Group isomorphism problem]]

==References==
{{Reflist}}

{{Authority control}}

[[Category:Abstract algebra]]
[[Category:Combinatorics on words]]
[[Category:Rewriting systems]]
[[Category:Computational problems]]