Word equation

One reason for this is that it was expected,[11] (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.Further contributions were made in the early 1970s with the work of André Lentin and Juri Ilich Hmelevskii.

[12] In 1976, Gennady Makanin introduced[3] 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.

[11] Makanin's algorithm is considered to be one of the most conceptually difficult existing in literature,[6] and it is also highly intractable, requiring (in its initial formulation) triply exponential time.

[13] In 1999, Wojciech Plandowski introduced a novel algorithm, showing[14] that the solubility problem for word equations is in PSPACE.

In 2006, Plandowski and Wojciech Rytter showed[15] that minimal solutions of word equations are highly (i.e., exponentially) compressible using Lempel-Ziv encoding.

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

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[15]).

[16] The algorithms mentioned above are all of theoretical interest, but they'll not help in solving a word equation by hand, for instance.

By taking a suitable conjugacy in this identity, one can infer that there exists some conjugate

is soluble, with the caveat that the method terminates only on quadratic word equations (as defined above).

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.

A natural extension is to consider Boolean formulas of word equations,[4] in which also negation and disjunction is allowed.

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.

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.

It should be also noted that even characterising the solution set of a single word equation is complicated.

Hmelevskii[9] 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.

For instance, in 1968, Yuri Matiyasevich considered[20] an extension of word equations by "length constraints" as a possible tool for showing the unsolvability of Hilbert's tenth problem.

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.

[22] For Matiyasevich's extension with the length constraints, the solubility problem still has open decidability status.

[17] 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.

[23] These tools, which are increasingly popular,[24] seek to solve algorithmically constraint satisfaction problems about strings.

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.

[24] 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).

[16] There has been much research into formulating and solving equations within different structures of abstract algebra (e.g., groups and semigroups).

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[29] states that the solubility problem for equations in free groups is again decidable.