Decision Procedures for Word Equations and Unification

An equation between two words built from constants and variables asks whether there is a substitution of concrete words for the variables that makes the two sides identical. The problem looks like a fragment of arithmetic and behaves nothing like it. It is decidable, the decision procedure is old enough to predate most of the field’s practical tools, and the complexity is so bad that the procedure has never been the basis of a general-purpose string solver.

The problem, stated precisely

Fix a finite alphabet Σ of constants. Let V be a set of variables. A word equation is a pair of words over Σ ∪ V, written u = v, and a solution is a map from V to Σ* extended homomorphically to both sides so that the two images are equal.

For a concrete example, take the equation xab = ay, where x and y are variables and a, b are constants. A solution must satisfy x·a·b = a·y. Setting x to the empty word gives ab = ay, forcing y = b. Setting x to a gives aab = ay, forcing y = ab. In general x = aᵏ gives y = aᵏb, so this equation has infinitely many solutions, and any decision procedure must handle that. The solution set here happens to be describable by a simple parameter, but the general case is not.

Two restrictions make the problem easy enough to see the shape of the difficulty. With no variables at all, the equation is a comparison of two constant words and is decided by a linear scan. A single equation in one variable with the variable occurring once per side is decided by comparing the constant prefix and suffix around the two occurrences and then checking that the two remaining gaps have equal length. The interesting behaviour starts at two variables, where the interaction between two unknowns cannot be eliminated locally.

The bound that makes search possible

The decision procedure rests on a finiteness lemma: if a word equation has a solution, it has one in which the substituted words are bounded in length by a function of the equation’s size. Makanin’s original analysis gave an enormous bound, and later work improved it substantially, but the bounds remain at least exponential in the size of the equation.

The reason a bound exists at all is combinatorial. Consider a minimal solution, meaning one whose total length is as small as possible. If the substituted words are very long, then the equation forces periodic structure: long stretches of the two sides must match, and that matching propagates constraints between the variables. A minimal solution cannot have arbitrary long words because periodicity would allow the solution to be shortened while still satisfying the equation. The periodicity lemma of Fine and Wilf quantifies the relevant notion: if a word has periods p and q and length at least p + q − gcd(p, q), then it also has period gcd(p, q). Applied to the overlaps forced by a long solution, this yields the bound.

With a bound in hand, the decision problem becomes a finite search: enumerate all substitutions whose substituted words are within the bound, and test each. The enumeration is finite and the test is a linear scan, so the procedure terminates. It is a decision procedure in the strict sense — it halts on every input with a correct yes or no — and it is unusable in practice, because the number of candidate substitutions grows exponentially in the bound, and the bound itself grows at least exponentially in the equation length.

This is the general pattern for hard-but-decidable problems. Decidability guarantees an answer; it says nothing about getting it in reasonable time. The distinction matters when a solver is described as complete: a complete procedure for word equations is one that terminates on every input, and that guarantee is compatible with running for longer than the age of the universe on a fifteen-character input.

Makanin’s method in outline

Enumerating substitutions directly is not how Makanin’s algorithm works; the bound justifies the search but the algorithm prunes it structurally. The method is a rewrite system over the equation itself, maintaining a set of constraints and reducing them step by step.

The state of the algorithm is a parametric equation: a word equation together with a set of inequalities between variables and a set of “the variable occurs in this region” constraints. At each step, a rule is applied based on the first symbols of the two sides:

• If both sides begin with the same constant, cancel it and continue with the remainders. This is the only rule that shortens the equation unconditionally.
• If one side begins with a constant and the other with a variable, the variable must begin with that constant. The rule splits into the case where the variable is exactly that constant (and is then substituted away) and the case where it is that constant followed by a fresh variable, with the constraint that the fresh variable is non-empty.
• If both sides begin with variables, the rule considers the relative lengths of the two variables and introduces a case split over which is a prefix of which, expressed with fresh variables. This is where the branching comes from.

Each rule preserves solvability: the original equation has a solution if and only if at least one branch of the resulting system does. The process terminates because a well-founded measure over the system decreases — roughly, the number of variables that occur on both sides plus a weight on the overlaps between variable occurrences. The termination proof is the difficult part of Makanin’s paper, and later work reformulated it in terms of a tree structure over the variable occurrences, which makes the measure easier to state.

The output, when a branch terminates successfully, is a description of a family of solutions rather than a single solution. The description is a system of the form “x = u₀ y₁ u₁ y₂ … yₘ uₘ”, where the yᵢ are fresh variables subject to no constraints; such a system generates infinitely many solutions when m > 0. This is why the algorithm answers “is there a solution” and not “list the solutions”.

Unification as a restricted case

Syntactic unification asks whether two first-order terms can be made equal by substituting for variables. It is the same shape of problem with a crucial restriction: the terms are built from function symbols applied to variables and constants, and a variable may be substituted by a term of arbitrary depth. The restriction is that the structure is a term algebra, not a free monoid, so every subterm has a unique top-level constructor. That restriction makes the problem decidable far more cheaply than the general word equation, and the standard algorithms are close to linear in the size of the terms once the bookkeeping is done properly.

Robinson’s unification algorithm computes a most general unifier: a substitution σ such that every unifier factors through σ. The algorithm walks the two terms in parallel, maintaining a set of equations between subterms. For each equation:

• If both sides are the same variable, discard it.
• If one side is a variable and the other is a term not containing that variable, record the binding and apply it to the remaining equations.
• If both sides are applications of the same function symbol with the same arity, replace the equation by equations between corresponding arguments.
• If both sides are applications of different function symbols, fail: no unifier exists.

The occurs check is the third case’s side condition. Binding x to a term containing x would require an infinite term, so it fails. Omitting the check is a common implementation shortcut that produces cyclic structures; it makes the algorithm answer a different question and turns the near-linear bound into something weaker.

def walk(t, subst):
    """Follow variable bindings until the term is no longer a bound variable."""
    while t[0] == 'var' and t[1] in subst:
        t = subst[t[1]]
    return t

def occurs(name, t, subst):
    """True if the variable name appears anywhere inside term t."""
    t = walk(t, subst)
    if t[0] == 'var':
        return t[1] == name
    return any(occurs(name, arg, subst) for arg in t[2])

def unify(eqs, subst=None):
    """eqs: list of (term, term) pairs. Terms are ('var', name) or
    ('app', symbol, [args...]). Returns a substitution or None."""
    subst = dict(subst or {})
    work = list(eqs)
    while work:
        lhs, rhs = work.pop()                   # pop once: one equation per round
        a, b = walk(lhs, subst), walk(rhs, subst)
        if a == b:
            continue
        if a[0] == 'var':
            if occurs(a[1], b, subst):
                return None                     # would require an infinite term
            subst[a[1]] = b
        elif b[0] == 'var':
            if occurs(b[1], a, subst):
                return None
            subst[b[1]] = a
        elif a[1] == b[1] and len(a[2]) == len(b[2]):
            work.extend(zip(a[2], b[2]))        # same symbol: descend into arguments
        else:
            return None                         # distinct rigid symbols cannot unify
    return subst

The walk helper applies existing bindings until a term is no longer a bound variable; without it the loop re-derives the same equations. The algorithm’s cost is dominated by the occurs check, which is a traversal of the term being bound and, repeated for every binding, can reach quadratic behaviour in the term size; a union-find structure over variable occurrences replaces the repeated traversal with an equivalence test.

The contrast with word equations is the whole point. In the free monoid, a variable stands for a word and concatenation is associative but not commutative; the lack of a constructor structure means the “descend into arguments” step has no analogue, and the algorithm must reason about how the two sides can overlap. In the term algebra, every term has a unique top-level constructor, so the parallel walk either matches constructors or fails immediately.

Where decidability stops being useful

Three practical observations follow from the theory, and each is a constraint on tool design.

String constraint solvers do not run Makanin. Solvers for program verification handle word equations by bounding the length of substituted words — the “bounded string” fragment — and by reducing to automata for restricted cases. The bound makes the problem decidable by construction, at the cost of losing completeness for equations with longer solutions. A solver that reports “unknown” for a satisfiable equation is behaving correctly under a bounded semantics and incompletely under the full one.

Unification modulo theories is a different problem. Unification modulo associativity and commutativity, or modulo a set of equations, is undecidable in general — the word problem for finitely presented semigroups reduces to it. Practical systems use unification modulo specific theories with known decision procedures, and fail outside them.

Complexity is the separate axis. An exhaustive search over substitutions inside Makanin’s bound costs time exponential in the bound, which makes the bound itself the wrong object to compute with. Makanin’s rewriting method avoids enumerating substitutions and is the substantive algorithm, but the worst-case cost of deciding word equations remains far above what a general-purpose solver will pay. The gap between “decidable” and “tractable” is the reason Presburger Arithmetic and the Decidable Side of Number Theory treats quantifier elimination as a completeness result rather than a performance claim.

The invariant that ties it together

Both problems are about the existence of a substitution, and in both cases the decision procedure’s correctness rests on an invariant about what a partial substitution commits to. For unification, the invariant is that the accumulated substitution is the most general one consistent with the equations processed so far, and the occurs check preserves it. For word equations, the invariant is that the current parametric system generates exactly the solution set of the original, and each rewrite rule preserves that set while decreasing a measure.

The second invariant is much harder to maintain because the branching is not over the structure of a term but over the possible lengths of overlapping words. That is the technical content of Makanin’s theorem, and it is also why the algorithm is rarely implemented. The theory’s value is in what it guarantees: a general word equation always has an answer, the answer can be computed, and the cost of computing it is severe enough that a bounded solver is the practical alternative rather than a shortcut.