word equation

{{Short description|Relation in Theoretical Computer Science}}

{{Technical|date=October 2024}}

A word equation is a formal equality E := u \overset{\cdot}{=} v between a pair of words u and v, each over an alphabet \Sigma \cup \Xi comprising both constants (cf. \Sigma) and unknowns (cf. \Xi).{{Cite book |url=https://www.cambridge.org/core/books/combinatorics-on-words/6FEBB4FCCB43895CCEFA8D69A0983374 |title=Combinatorics on Words |date=1997 |publisher=Cambridge University Press |isbn=978-0-521-59924-5 |editor-last=Lothaire |editor-first=M. |edition=2 |series=Cambridge Mathematical Library |location=Cambridge |doi=10.1017/cbo9780511566097}}  An assignment h of constant words to the unknowns of E is said to solve E if it maps both sides of E to identical words. In other words, the solutions of E are those morphisms h:(\Sigma\cup\Xi)^*\to\Sigma^* whose restriction to \Sigma is the identity map, and which satisfy h(u)=h(v). Word equations are a central object in combinatorics on words; they play an analogous role in this area as do Diophantine equations in number theory. One stark difference is that Diophantine equations have an undecidable solubility problem,{{Cite book |last1=Cooper |first1=S. Barry |date=2017-09-06 |title=Computability Theory |url=http://dx.doi.org/10.1201/9781315275789 |doi=10.1201/9781315275789|isbn=978-1-315-27578-9 }} whereas the analogous problem for word equations is decidable.{{Cite journal |last=Makanin |first=G S |date=1977-02-28 |title=The Problem of Solvability of Equations in a Free Semigroup |url=http://dx.doi.org/10.1070/sm1977v032n02abeh002376 |journal=Mathematics of the USSR-Sbornik |volume=32 |issue=2 |pages=129–198 |doi=10.1070/sm1977v032n02abeh002376 |bibcode=1977SbMat..32..129M |issn=0025-5734|url-access=subscription }}

A classical example of a word equation is the commutation equation xw\overset{\cdot}{=}wx, in which x is an unknown and w is a constant word. It is well-known{{Cite book |url=https://link.springer.com/book/10.1007/978-3-642-59136-5 |title=Handbook of Formal Languages |date=1997 |language=en |doi=10.1007/978-3-642-59136-5 |isbn=978-3-642-63863-3 |editor-last1=Rozenberg |editor-last2=Salomaa |editor-first1=Grzegorz |editor-first2=Arto }} that the solutions of the commutation equation are exactly those morphisms h mapping x to some power of w. Another example is the conjugacy equation{{Cite book |last=Lothaire |first=M. |url=https://www.cambridge.org/core/books/algebraic-combinatorics-on-words/F0C477102253C41503EB7D6AE7C0F367 |title=Algebraic Combinatorics on Words |date=2002 |publisher=Cambridge University Press |isbn=978-0-521-81220-7 |series=Encyclopedia of Mathematics and its Applications |location=Cambridge |doi=10.1017/cbo9781107326019}} xz\overset{\cdot}{=}zy, in which x, y,  and z are all unknowns. The solutions of this equation are precisely those morphisms h sending x and y to conjugate words, with the image h(z) being filled in as appropriate.

Many subclasses of word equations have been introduced, some of which include:

  • constant-free equations,{{Cite web |last1=Berstel |first1=Jean |last2=Karhumäki |first2=Juhani |date=February 2003 |title=Combinatorics on Words – A Tutorial |url=http://www-igm.univ-mlv.fr/~berstel/Articles/2003TutorialCoWdec03.pdf |access-date=18 October 2024}} which are those u\overset{\cdot}{=}v such that u,v comprise unknowns only. Such equations have a trivial solution wherein all their unknowns are erased; as such, they are usually studied over free semigroups.
  • quadratic equations, which are those containing each of their unknowns at most twice. This is exactly the class of word equations on which the Nielsen Transformations algorithm (cf. below) terminates.
  • word equations in one unknown, which can be checked for their solubility in linear time.{{Cite journal |last=Jeż |first=Artur |date=2016-01-01 |title=One-Variable Word Equations in Linear Time |journal=Algorithmica |language=en |volume=74 |issue=1 |pages=1–48 |doi=10.1007/s00453-014-9931-3 |issn=1432-0541|doi-access=free |arxiv=1302.3481 }}

History

The study of word equations was initiated by Willard Quine as early as 1946. Quine proved{{Cite journal |last=Quine |first=W. V. |date=December 1946 |title=Concatenation as a basis for arithmetic |url=https://www.cambridge.org/core/journals/journal-of-symbolic-logic/article/abs/concatenation-as-a-basis-for-arithmetic/4A4E16B4F4B54751FEDD97C30231963D |journal=The Journal of Symbolic Logic |language=en |volume=11 |issue=4 |pages=105–114 |doi=10.2307/2268308 |jstor=2268308 |issn=0022-4812|url-access=subscription }} that the first-order theory of word equations is essentially equivalent to the first-order theory of arithmetic. In 1954, Andrey Markov coined the term "word equation", and introduced{{Cite book |last1=Markov |first1=A. A. |title=The theory of algorithms |last2=Nagornyĭ |first2=N. M. |date=1988 |publisher=Kluwer Academic |isbn=978-90-277-2773-2 |series=Mathematics and its applications (Soviet series) |location=Dordrecht; Boston |language=en, ru}} the solubility problem for them: decide whether a given word equation admits a solution. For a long time, it was hoped that this problem was undecidable. One reason for this is that it was expected,{{Cite book |last1=Obono |first1=S. Eyono |last2=Goralcik |first2=P. |last3=Maksimenko |first3=M. |date=1994 |editor-last=Prívara |editor-first=Igor |editor2-last=Rovan |editor2-first=Branislav |editor3-last=Ruzička |editor3-first=Peter |chapter=Efficient solving of the word equations in one variable |chapter-url=https://link.springer.com/chapter/10.1007/3-540-58338-6_80 |title=Mathematical Foundations of Computer Science 1994 |series=Lecture Notes in Computer Science |volume=841 |language=en |location=Berlin, Heidelberg |publisher=Springer |pages=336–341 |doi=10.1007/3-540-58338-6_80 |isbn=978-3-540-48663-3}} (incorrectly, it turns out), that word equations might provide an intermediary step between Hilbert's Tenth Problem and the undecidable problems relating to Turing machines.File:Маканин Г.С..jpg, who introduced Makanin's algorithm.]]Further contributions were made in the early 1970s with the work of André Lentin and Juri Ilich Hmelevskii.{{Cite journal |last1=Berstel |first1=Jean |last2=Perrin |first2=Dominique |date=2007-04-01 |title=The origins of combinatorics on words |url=https://linkinghub.elsevier.com/retrieve/pii/S0195669805001629 |journal=European Journal of Combinatorics |volume=28 |issue=3 |pages=996–1022 |doi=10.1016/j.ejc.2005.07.019 |issn=0195-6698}} In 1976, Gennady Makanin introduced a method by which it could be determined whether any given word equation admitted a solution. That this procedure, which has come to be known as Makanin's algorithm, exists is very difficult to prove, and it is one of the most celebrated results in combinatorics on words. Makanin's algorithm is considered to be one of the most conceptually difficult existing in literature, and it is also highly intractable, requiring (in its initial formulation) triply exponential time.{{Cite journal |last1=Kościelski |first1=Antoni |last2=Pacholski |first2=Leszek |date=1996-07-01 |title=Complexity of Makanin's algorithm |url=https://dl.acm.org/doi/10.1145/234533.234543 |journal=J. ACM |volume=43 |issue=4 |pages=670–684 |doi=10.1145/234533.234543 |issn=0004-5411}} Thus, there were many attempts to improve upon it. In 1999, Wojciech Plandowski introduced a novel algorithm, showing{{Cite book |last=Plandowski |first=W. |chapter=Satisfiability of word equations with constants is in PSPACE |date=1999 |title=40th Annual Symposium on Foundations of Computer Science (Cat. No.99CB37039) |chapter-url=https://ieeexplore.ieee.org/document/814622 |publisher=IEEE Comput. Soc |pages=495–500 |doi=10.1109/SFFCS.1999.814622 |isbn=978-0-7695-0409-4}} that the solubility problem for word equations is in PSPACE.

In 2006, Plandowski and Wojciech Rytter showed{{Cite book |last1=Plandowski |first1=Wojciech |last2=Rytter |first2=Wojciech |date=1998 |editor-last=Larsen |editor-first=Kim G. |editor2-last=Skyum |editor2-first=Sven |editor3-last=Winskel |editor3-first=Glynn |chapter=Application of Lempel-Ziv encodings to the solution of word equations |chapter-url=https://link.springer.com/chapter/10.1007/BFb0055097 |title=Automata, Languages and Programming |series=Lecture Notes in Computer Science |volume=1443 |language=en |location=Berlin, Heidelberg |publisher=Springer |pages=731–742 |doi=10.1007/BFb0055097 |isbn=978-3-540-68681-1}} that minimal solutions of word equations are highly (i.e., exponentially) compressible using Lempel-Ziv encoding. It is conjectured that the length of a minimal solution of a word equation E is (at most) singly exponential in the length |E| of E. If this conjecture is true, then Plandowski and Rytter's result yields a straightforward "guess-and-verify" NP algorithm for the solubility problem: they show that a solution h can be verified whilst working only with its LZ-compressed representation LZ(h), and the conjecture being true would imply that LZ(h) has size polynomial in |E|. As it stands, the last part of the complexity analysis—the question as to whether solving word equations is NP-complete—remains open. (NP-hardness follows immediately from the fact that solving word equations generalises the NP-complete problem of pattern matching).

Methods of solution

There is no "elementary" algorithm for determining whether a given word equation admits a solution.{{Cite web |last=Karhumäki |first=Juhani |title=Combinatorics of Words |url=https://www.math.utu.fi/en/home/karhumak/pdf/combwo.pdf |access-date=18 October 2024}} The algorithms mentioned above are all of theoretical interest, but they'll not help in solving a word equation by hand, for instance. There exist however a few methods that can sometimes help with this:

= Length arguments =

Because a solution h to a word equation E must unify its two sides, one can use the multiset of symbols occurring on either side of E to deduce a linear equality in the lengths of the images of the unknowns. For instance, the form of xx\overset{\cdot}{=}y implies that its solutions h must satisfy |h(y)|=2|h(x)|, which narrows down the set of possible h to check. Similar arguments can allow for a word equation E to be "split up" into smaller ones if it can be deduced positions within the two sides of E which must line up in all solutions of E. For instance, the midpoints of each side of xyyx\overset{\cdot}{=}uvvu can be detected via a length argument, and hence that word equation can be split into the system \left\lbrace\begin{matrix}xy\overset{\cdot}{=}uv \\ yx\overset{\cdot}{=}vu\end{matrix}\right..

= Appeal to periodicity =

Another useful tool for reasoning about word equations is the Periodicity Lemma of Fine and Wilf, which describes what happens if a certain word has multiple periods (i.e., distances at which its letters repeat). Consider, for instance, the word equation E:=x^2y^2\overset{\cdot}{=}z^2. Suppose that (x,y,z)\mapsto(w_x,w_y,w_z) is one of its solutions. Then w_x^2w_y^2=w_z^2. By taking a suitable conjugacy in this identity, one can infer that there exists some conjugate z' of z which is such that z'^2 = w_xw_y^2w_x. Now a length argument permits for the midpoint of each side to be identified here, and it follows from this observation that w_xw_y=z'=w_yw_x. Herein is the commutation equation, whence w_x and w_y are powers of a common word. Now the infinite words w_x^\omega and w_z^\omega have a common prefix of length |w_z^2|. Since |w_z^2|=2|w_z|\ge|w_z|+|w_x|\ge|w_z|+|w_x|-\gcd(|z|,|x|), the Periodicity Lemma can be applied. Its conclusion here is that w_z and w_x are powers of a common word too. Thus, every solution h of E maps x,y, and z to powers of a common word.

= Nielsen transformations =

{{See also|Levi's lemma#Applications}}

File:Nielsen transformations graph.png

Let E:=xu\overset{\cdot}{=}yv be a word equation, such that x,y\in\Sigma\cup\Xi, and u,v\in(\Sigma\cup\Xi)^*. Here shall be presented a conceptually simple method (called Nielsen transformations algorithm, or Levi's Method.{{Cite journal |last1=Lin |first1=Anthony W. |last2=Majumdar |first2=Rupak |date=2021-10-29 |title=Quadratic Word Equations with Length Constraints, Counter Systems, and Presburger Arithmetic with Divisibility |url=https://lmcs.episciences.org/6693 |journal=Logical Methods in Computer Science |language=en |volume=17 |issue=4 |doi=10.46298/lmcs-17(4:4)2021 |issn=1860-5974|arxiv=2007.15478 }}) to determine whether E is soluble, with the caveat that the method terminates only on quadratic word equations (as defined above).

The idea of the algorithm is to "guess" how the lengths of x and y compare in some solution of E. Either |h(x)|>|h(y)|, |h(x)|<|h(y)|, or h(x)=h(y). In the first case, one can apply the string-rewriting rule x\mapsto yx to E, where x (after the rewriting) is a new quantity whose meaning is "what's left of the old x once y is removed". Symmetrically, in the second case, one can apply the rule y\mapsto xy, and in the third case x\mapsto y. The present method actually makes all three guesses; for each of them (separately) it rewrites E to account for the guess having been made.

By construction, there will be some cancellation at the start of E after applying each string-rewriting rule. (For instance, applying x\mapsto ax to the equation xab\overset{\cdot}{=} abx yields axab\overset{\cdot}{=} abax, which cancels down to xab\overset{\cdot}{=} bax). The method always takes advantage of this cancellation; the hope is that it is enough to counteract the string-rewriting rule, which (in general) will have made the equation longer.

The algorithm thus amounts to exhaustively applying these transformations. It is natural to view the workings of the algorithm as the construction of a graph \mathcal{G}(E), whose nodes are the reached equations, and edges are the transformations between them. If the trivial word equation \varepsilon\overset{\cdot}{=} \varepsilon, (where \varepsilon is the empty word) is ever encountered during this construction, then E is surely solvable. Conversely, if E is soluble, then \varepsilon\overset{\cdot}{=} \varepsilon must appear in \mathcal{G}(E). So, by this method (assuming \mathcal{G}(E) is finite) it can be determined whether E admits a solution.

Systems of word equations

One can define systems of word equations in the natural way. A solution of such a system S is a morphism h that solves simultaneously every equation in S.  A natural extension is to consider Boolean formulas of word equations, in which also negation and disjunction is allowed. In fact, every system (and even every Boolean formula) of word equations, is equivalent to a single word equation. Thus, many results on word equations generalise immediately to such systems (resp. formulas). It must be said, however, that the transformation into a single word equation can introduce extra unknowns, and this is sometimes by necessity.

Two word equations (or systems thereof) are called equivalent if they have the same set of solutions. A system of word equations is called independent if it is not equivalent to any of its proper subsystems. Put another way, an independent system S of word equations is one such that every E\in S can be solved "independently", i.e., without solving any of the other E'\in S. An interesting compactness theorem, usually bearing the name of Andrzej Ehrenfeucht, states that an infinite system of word equations, and with a finite number of unknowns, is necessarily equivalent to one of its finite subsystems.{{Cite journal |last1=Albert |first1=M. H. |last2=Lawrence |first2=J. |date=1985-01-01 |title=A proof of Ehrenfeucht's Conjecture |url=https://linkinghub.elsevier.com/retrieve/pii/0304397585900660 |journal=Theoretical Computer Science |volume=41 |pages=121–123 |doi=10.1016/0304-3975(85)90066-0 |issn=0304-3975|url-access=subscription }} It follows that any independent system of word equations with a finite number of unknowns is itself finite.

Expressing formal languages and relations

Word equations can be used to characterise properties of (tuples of) words. For instance, a word ends in a if and only if it is the image h(x) in some solution of the word equation x\overset{\cdot}{=} ya. Similarly, two words commute if and only if they are the images h(x), h(y) in some solution of the word equation xy\overset{\cdot}{=}yx. In this sense, word equations can be thought of as mechanisms for expressing formal languages,{{Cite journal |last1=Karhumäki |first1=Juhani |last2=Mignosi |first2=Filippo |last3=Plandowski |first3=Wojciech |date=2000-05-01 |title=The expressibility of languages and relations by word equations |url=https://dl.acm.org/doi/10.1145/337244.337255 |journal=J. ACM |volume=47 |issue=3 |pages=483–505 |doi=10.1145/337244.337255 |issn=0004-5411}} in analogy with automata and formal grammars. It is not known exactly which properties of (tuples of) words are expressible in via word equations in this way. In particular, to show that a relation is inexpressible by word equations is often quite challenging. (An example of an inexpressible property is "x is primitive").

It should be also noted that even characterising the solution set of a single word equation is complicated. Hmelevskii{{Cite book |last1=Chmelevskij |first1=Jurij I. |title=Equations in free semigroups |last2=Chmelevskij |first2=Jurij I. |date=1976 |publisher=American Mathematical Soc |isbn=978-0-8218-3007-9 |series=Proceedings of the Steklov Institute of Mathematics |location=Providence, RI}} proved that, although the solutions to three-unknown constant-free equations can be given in terms of finite expressions with word and integer parameters, this is not true (in general) for four-unknown constant-free equations. In fact, xyz\overset{\cdot}{=}ztx is an example of such a "non-parametrisable" word equation.

Extended theories and connections to string solving

One can augment word equations with other types of constraints on the values h(x), x\in \Xi. For instance, in 1968, Yuri Matiyasevich considered{{Cite web |last=Matiyasevich |first=Yuri |date=1968 |title=СВЯЗЬ СИСТЕМ УРАВНЕНИЙ В СЛОВАХ И ДЛИНАХ С 10-Й ПРОБЛЕМОЙ ГИЛЬБЕРТА |url=https://www.mathnet.ru/links/d8d673076fce68ed85cedc678c6e2292/znsl2256.pdf |access-date=19 October 2024 |website=Math-Net.Ru}} an extension of word equations by "length constraints" as a possible tool for showing the unsolvability of Hilbert's tenth problem. These length constraints amounted to linear inequalities in the unknowns |h(x)|, x\in \Xi. Sometimes, allowing extra constraints (alongside word equations) leads to theories with undecidable solubility problems, but it is also possible to add less powerful constraints and end up with a theory that's still decidable. An example of the former type of constraint is requiring that some h(x),h(y) should be Abelian equivalent (i.e., anagrams of one another);{{Cite book |last1=Day |first1=Joel D. |last2=Ganesh |first2=Vijay |last3=He |first3=Paul |last4=Manea |first4=Florin |last5=Nowotka |first5=Dirk |chapter=The Satisfiability of Word Equations: Decidable and Undecidable Theories |series=Lecture Notes in Computer Science |date=2018 |volume=11123 |editor-last=Potapov |editor-first=Igor |editor2-last=Reynier |editor2-first=Pierre-Alain |title=Reachability Problems |chapter-url=https://link.springer.com/chapter/10.1007/978-3-030-00250-3_2 |language=en |location=Cham |publisher=Springer International Publishing |pages=15–29 |doi=10.1007/978-3-030-00250-3_2 |isbn=978-3-030-00250-3}} an example of the latter type is requiring that some h(x) should belong to a given regular language L.{{Cite journal |last1=Diekert |first1=Volker |last2=Gutierrez |first2=Claudio |last3=Hagenah |first3=Christian |date=2005-11-01 |title=The existential theory of equations with rational constraints in free groups is PSPACE-complete |url=https://linkinghub.elsevier.com/retrieve/pii/S0890540105000854 |journal=Information and Computation |volume=202 |issue=2 |pages=105–140 |doi=10.1016/j.ic.2005.04.002 |issn=0890-5401|arxiv=cs/0103018 }} For Matiyasevich's extension with the length constraints, the solubility problem still has open decidability status.

There has been recent interest in the theory of word equations (and more general theories based on it), from the practical point of view of those developing software verification tools called string solvers.{{Cite journal |last1=Lin |first1=Anthony W. |last2=Barceló |first2=Pablo |date=2016-01-11 |title=String solving with word equations and transducers: towards a logic for analysing mutation XSS |url=https://dl.acm.org/doi/10.1145/2914770.2837641 |journal=SIGPLAN Not. |volume=51 |issue=1 |pages=123–136 |doi=10.1145/2914770.2837641 |issn=0362-1340|url-access=subscription }} These tools, which are increasingly popular,{{Cite journal |last=Amadini |first=Roberto |date=2021-11-23 |title=A Survey on String Constraint Solving |url=https://dl.acm.org/doi/10.1145/3484198 |journal=ACM Comput. Surv. |volume=55 |issue=1 |pages=16:1–16:38 |doi=10.1145/3484198 |hdl=11585/850408 |issn=0360-0300|arxiv=2002.02376 }} seek to solve algorithmically constraint satisfaction problems about strings. Such problems take the form of a set of constraints, which an unknown set of strings must satisfy. The string solver should then determine whether strings exist which satisfy all the given constraints. A typical goal of such a tool would be to guarantee that a particular piece of software was free from some string-related vulnerability, such as cross-site scripting or code injection.{{Cite book |last1=Thome |first1=Julian |last2=Shar |first2=Lwin Khin |last3=Bianculli |first3=Domenico |last4=Briand |first4=Lionel |chapter=Search-Driven String Constraint Solving for Vulnerability Detection |date= 2017|title=2017 IEEE/ACM 39th International Conference on Software Engineering (ICSE) |chapter-url=https://ieeexplore.ieee.org/document/7985662 |publisher=IEEE |pages=198–208 |doi=10.1109/ICSE.2017.26 |isbn=978-1-5386-3868-2|url=https://ink.library.smu.edu.sg/sis_research/4777 }}

The building blocks of the constraints used in these tools are the standard questions one might ask of strings, such as "is x a substring of y?", "what is the length of string x?", and "what is the index of string x in string y?". Ostensibly, these constraints can be modelled by theories based on word equations, and as such, string solver tools must be capable of dealing with these theories algorithmically, (at least in the subcase of those equations and formulas that actually arise in practice).

Relation to the defect effect

The defect theorem is a central result to combinatorics on words. It says that, if a set X of words satisfies a nontrivial relation, then the words of X can be (simultaneously) expressed as products of |X|-r words, where r\ge 1. Such a set X is then said to possess a "defect effect" of order r. Systems of word equations, (at least "nontrivial" ones), express the fact that a certain finite set of words, (namely the images h(x) of the unknowns x\in\Xi), satisfy some nontrivial relation(s). So it can be said that systems S of word equations cause a defect effect in the sets of words X=\{h(x) : x\in\Xi\} coming from solutions h of S.

The defect effect caused by certain systems of word equations has been studied.,{{Citation |last1=Karhumäki |first1=Juhani |title=On the Defect Effect of Many Identities in Free Semigroups |date= 1994|work=Mathematical Aspects of Natural and Formal Languages |pages=225–232 |url=http://www.worldscientific.com/doi/abs/10.1142/9789814447133_0012 |access-date=2024-10-19 |publisher=World Scientific |language=en |doi=10.1142/9789814447133_0012 |isbn=978-981-02-1914-7 |last2=Plandowski |first2=Wojciech|url-access=subscription }} and there exist some surprising results to this end showing that the "dimensionality properties" of sets of words are actually quite weak. For instance, it is known that here exists an independent system S of equations of size \Omega(n^2), containing n unknowns, which is such that S causes only a defect effect of order 1.

Role within abstract algebra

There has been much research into formulating and solving equations within different structures of abstract algebra (e.g., groups and semigroups).{{Cite journal |last1=Ciobanu |first1=Laura |last2=Holt |first2=Derek |last3=Rees |first3=Sarah |date=2020-03-01 |title=Equations in groups that are virtually direct products |url=https://linkinghub.elsevier.com/retrieve/pii/S0021869318306677 |journal=Journal of Algebra |series=Special Issue in Memory of Charles Sims |volume=545 |pages=88–99 |doi=10.1016/j.jalgebra.2018.10.044 |issn=0021-8693|arxiv=1806.00244 }}{{Citation |last=Schiek |first=Helmut |title=Equations Over Groups |date=1973-01-01 |work=Studies in Logic and the Foundations of Mathematics |volume=71 |pages=563–567 |editor-last=Boone |editor-first=W. W. |url=https://linkinghub.elsevier.com/retrieve/pii/S0049237X08719207 |access-date=2024-10-19 |series=Word Problems |publisher=Elsevier |doi=10.1016/s0049-237x(08)71920-7 |isbn=978-0-7204-2271-9 |editor2-last=Cannonito |editor2-first=F. B. |editor3-last=Lyndon |editor3-first=R. C.|url-access=subscription }} Word equations, as presented here, are simply equations in free monoids. Equations in free semigroups are closely related to these; in fact, they are just word equations with the additional requirement that the solution morphism h is nonerasing. One can also consider equations in free groups, although the theory of such objects differs in many ways from the discussion presented here. Another result of Makanin's{{Cite journal |last=Makanin |first=G S |date=1983-06-30 |title=Equations in a Free Group |url=https://www.mathnet.ru/eng/im1703 |journal=Mathematics of the USSR-Izvestiya |volume=21 |issue=3 |pages=483–546 |doi=10.1070/IM1983v021n03ABEH001803 |bibcode=1983IzMat..21..483M |issn=0025-5726|url-access=subscription }} states that the solubility problem for equations in free groups is again decidable.

References

{{reflist}}

{{Improve categories|date=October 2024}}

Category:Combinatorics on words