The unification problem in free semigroups, where

and the set of terms are built up as usual over constants, variables, but only one function symbol f with arity( f) = 2 is called string unification, since we can just drop the f s and brackets and write strings (or words as they are more commonly called in the mathematical literature [56, 57]) over the alphabet of constants and variables. In addition we will simply write = for the equality of strings instead of =A. This is probably the most famous unification problem, respectively called the solvability of word equations and the question is: can similar results as in 4.1. above be obtained as well for strings.

In the 1950s A. A. Markov was interested in Hilbert’s 10th problem, which is one of the 23 famous problems Hilbert proposed in 1900 during his seminal talk in Paris. It is the following problem: Does there exist an algorithm (a decision procedure) to compute whether a Diophantine equation has a solution in rational integers. Martin Davis and Julia Robinson, working first separately and then, joined by Hilary Putnam, in collaboration, proved that it would follow that there is no such algorithm, if a single polynomial equation were found with a particular exponential growth property [21]. Finally, the young mathematician Yuri Matiyasevich [60] solved the problem by producing such an equation, something the three had been unable to accomplish despite a decade of trying [19].[1]

A.A. Markov tried to reduce it to the solvability of word equations in free semigroups: he noted that every word equation over a two constant alphabet can be translated into a set of diophantine equations [59]. Using this translation he hoped to find a proof for the unsolvability of Hilbert’s 10th problem by showing that the solvability of word equations is undecidable [61]. This put the problem firmly on the map and others joined in: Lentin and Schutzenberger [54], J.I. Hmelevskij [34-36], V.K. Bulitko [13], A. Lentin [53], V.G. Durnev [28] and many others, see [1] for a survey as well as the volumes edited by several mathematicians under the pseudonym of M. Lothaire on Algebraic Combinatorics on Words [56, 57].

The problem was finally solved in the affirmative in the seminal work by G.S. Makanin [58]. An exposition of Makanin’s algorithm with several improvements is presented inter alia by Klaus Schulz [70, 71] and by Volker Diekert [24]. Algorithms for the computation of a minimal set of unifiers are given in [26, 43] and there is a history of improved algorithms and their complexity bounds, a standard reference is [62]. Some more recent articles are for example [14, 27, 51] and since then the amount of works and results for this and related problems has exploded even more.[2]

The most interesting observation is probably that the problem is decidable, whereas H10 is undecidable—hence Markov’s idea would not have worked anyway.

The decision procedure for word equations due to G. Makanin is one of the most complex known algorithms and it marks in an interesting way the borderline between decidable and undecidable problems.

Apart from its theoretical and mathematical interest, the problem became more widely known, because of its relevance in computer science, artificial intelligence and automated reasoning. Examples are equations over lists with concatenation, the data structure string in pattern invoked procedures in AI and finally building associativity into a resolution style theorem prover. Gordon Plotkin [63], Jorg Siekmann [55, 72, 73] and Andre Lentin [53] independently found an algorithm to enumerate the set of most general unifiers for strings, which is infinite in general.

As opposed to the above cited works on decidability, which just enumerate all solutions and make the decidability or the existence of a solution their primary focus, in our community we are more interested in the latter works, inspired by automated theorem proving, where the set aU ? of the most general unifiers is the focus of attention.

The most common and simple example to show that string unification in free semigroups is infinitary is the following already mentioned case:

with the set of most general unifiers

It is easy to see that indeed this is a solution set and it is not as immediate, but still not too hard to show that there does not exist any other more general set of unifiers IxU ? for this problem. Finally /aU ? is minimal, which again is obvious, as an is ground and thus the unifiers do not yield to instantiation. Hence in general

As we have said, this is a well known fact since the mid seventies and it is probably the most often quoted example in any lecture or monograph on unification theory.

A similar example

is usually chosen to demonstrate that the naive string unification algorithms as for example in [55, 63, 72, 73] are not decision procedures: although it is obvious that the above example is not unifiable, the naive algorithms would run forever. However J. Jaffar’s algorithm [43], which is built upon Makanin’s work, would recognize this situation and halt.

In contrast to string unification as it has been understood up to now, the first problem has a finite set (in fact an even e-unitary set) of essential unifiers

and any other most general unifier can be obtained with Xn = {x ^ an-1 x}, n > 1. In other words, for any unifier an = {x ^ an}, n > 1:

where Xn obeys the structural property, as defined in Sect.2.6.

Once this observation had been made many years ago, there was an intense struggle to find the correct definitional framework in order to generalize this observation to the whole string unification problem and to prove the conjecture

We have shown in [37, 38] that this conjecture is false in general, albeit it holds for subclasses of strings, for example the one variable strings.

Let us summarize the main results and denote the set of string equations as Г = {u 1 = v1,...,un = vn} where the ui and the vi are strings. Var (Г) is the set of free variable symbols occurring in ui and vi. Let V = Var(Г), then a (string-) unifier a : V ^ L* is a solution for Г if ui a = vi a, 1 < i < n. The set of all unifiers is denoted as U LA (Г) and we may now drop the A.

Let us look first at a few motivating examples, which show that indeed an infinite set of most general unifiers L collapses to a finite set of essential unifiers eU L. Our first example is the well known string unification problem mentioned in the introduction:

has infinitely many most general unifiers an, but there is just one e-unifier a0 = {x ^ a} because of

The next example taken from the Burris-Problem-List[3] has two variables:

and it has infinitely many most general unifiers o',j = {x ^ z', y ^ zj}, i, j > 0, where i and j are relative prime, i.e. gcd(i, j) = 1. The condition for i and j to be relatively prime ensures that we get only most general unifiers, not just any unifier (see example 15in the Burris-Problem-List).

But it has only one e-unifier o0 = {x ^ z, y ^ z} because of

Our next example is taken from J. Karhumaki in Combinatorics of Words [15] see also [56, 57]. The system

has infinitely many most general unifiers

But it has only one e-unifier o0 = {x ^ b, y ^ a} because of

Exploiting the analogy between the first and the second example above, we can easily construct more examples in this spirit.

Our fourth example is taken from J. Karhumaki as well:

It has infinitely many most general unifiers

but it has only one e-unifier o1,0 = {x ^ a, y ^ a} which is essential because of

that is o1,0 c Oi, j and o1,0 does not encompass any other unifier. The final example is a bit more elaborate but still in the same spirit:

has infinitely many most general unifiers

but it has only one e-unifier, namely o1 ={x ^ bba, y ^ bab, z ^ b} because of

String unification with at most one variable is e-finitary

Let us assume our unification problem

over the signature ? has at most one variable, but arbitrarily many constants. Without loss of generality, each set of string equations can be encoded into a single string equation preserving the solutions, which is well known (for example see J.I. Hmeleyskij [36]). Volker Diekert in [24] used the following construction

where a and b are distinct constants. It can be shown, that the two equational problems have the same solutions.

The following facts are known, see [16] and also [44], and we shall use them for our main result as well. Note, a word is primitive if it is not a power of any other word.

Theorem 11.3 A string unification problem Г in one variable has either no solution or ц-U ?А(Г) = F U{x i—> (pq)'+1 p, i > 0} for some p, q in ?, pq is primitive and F is a finite set of unifiers, which is bounded by O(log | Г |).

Proof see Theorem 3 and Lemma 1 in [16] ?

It is also known that

Proposition 11.7 Let Г = {u0xu1.. .xun = xv1.. .xvn} be a solvable string equation with at most one variable x. Then all unifiers are ground substitutions:

Vo e U ? a (Г) : x o e ?*

Proof Suppose by contradiction with an arbitrary unifier {x ^ w}e U ?A (Г) : w = w1 zw2 where z is a new variable z = x such that w1 is the ground prefix of w. Applying the unifier x ^ w1 zw2 yields

Consider the prefixes u0w1... = w1 z... Since |u0w11 > |w1 z| and u0 is nonempty, z must be a symbol in u0 w1, which is impossible, since u0 and w1 are ground by assumption.

Hence Var (w) is empty and the set of solutions is even minimal:

U ?A (Г) = fzU ?а(Г). ?

So finally we have

Theorem 11.4 String unification with one variable is e-finitary and the number of unifiers is bounded by O(log | Г |).

Proof In [38] ?

String unification in general is e-infinitary

String unification with at most one variable in the signature ? is e-finitary as we have seen above and surely there are many more special cases of signature restrictions, where the set of e-unifiers is always finite or even unitary.

However the general result for essential string unification is:

Theorem 11.5 String unification with more than one variable is e-infinitary

Proof see [38] ?

A general A-theorem

Let E be a set of equational axioms containing the associativity axiom of a binary operator *, i.e. A = {x * (y * z) = (x * y) * z} and E = A U R, where R is some set of equations. We call the theory modulo E A-separate, if any equation in R can not be applied to a pure string s1 * s2 *•••* sn (the brackets are suppressed).

For instance consider distributivity (which is an infinitary unification theory), see [6, 80]

then the theory of E = A U D is A-separate. To see this, note that no equation of D can be applied to a string of x1 * x2 *•••* xn, simply because there are no sums involving the plus sign +, but each equation in D has the sum symbol + on its left and on its right hand side.

Formally, E = A U R is A-separate, if for all elements u of the A-theory u =R v implies u = v.

Theorem 11.6 All not e-nullary A-separate E-theories are e-infinitary Proof see [38] ?

As noted above the not e-nullary theory A U D is A-separate and hence:

Theorem 11.7 The theory A U D is e-infinitary.

Note that the theorem does not imply that D alone is e-infinitary: D is infinitary [79, 80], but the essential case for D is not yet known.

  • [1] See also There is actually anice film about the three and how John McCarthy informed Martin about the result, see
  • [2] Google scholar finds 62,600,000 entries in 0.21 s for word equations this year (not all of whichis relevant for our topic of course, but narrowing it down to “word equations” still leads to 1500entries in 0.16 s) and several 100,000 more entries if one is patient enough to continue the searchand to filter gold from garbage. In the year 2008, at the unification workshop, where we publisheda preliminary result, we asked Dr. Google and “he” found 70,300 entries for “word equations” in0.13 s—so what are we to make of this fact?
  • [3] See, example 15.
< Prev   CONTENTS   Source   Next >