Two terms made equal, and no more

Resolution works on clauses — disjunctions of literals — and its one rule cancels a literal against its negation. In propositional logic that is a matter of spotting $p$ in one clause and $\neg p$ in another. In first-order logic the literals carry terms, $P(x, f(y))$ and $\neg P(g(a), z)$, and whether they cancel depends on what the variables stand for. Here they cancel if $x$ is $g(a)$ and $z$ is $f(y)$ — but they also cancel if $x$ is $g(a)$, $y$ is $b$ and $z$ is $f(b)$, and in infinitely many other ways.

The naive procedure, the Herbrand expansion, deals with this by substituting every ground term in turn and running propositional resolution on the result. It is complete, and it is hopeless: the instance that closes the proof sits somewhere in a supply of terms that grows doubly exponentially with depth. In 1965 J. Alan Robinson replaced the guessing with a computation. Two literals are resolved on exactly when some substitution makes them identical, and among all such substitutions there is one that is most general — every other is obtained from it by substituting further. Compute that one, resolve, and move on. The instance is not guessed; it is solved for.

Terms are trees, and equality is shape #

A first-order term is built from constants, variables and function symbols, and it is best seen as a tree: the function symbol at the root, its arguments as subtrees, constants and variables at the leaves.

Two terms are equal when their trees are identical, node for node. A substitution replaces each occurrence of a variable by a term — it grafts a subtree onto every leaf carrying that variable — and a unifier of two terms is a substitution after which their trees coincide.

In the figure, both trees have $f$ at the root with two children, so the unifier must make the children agree pairwise. On the left, $x$ faces $h(y)$, so $x$ must become $h(y)$. On the right, $g(x)$ faces $g(z)$; with $x$ now $h(y)$, that says $z$ must be $h(y)$ too. Nothing is required of $y$. So the unifier is $x \mapsto h(y),\ z \mapsto h(y)$, and it leaves $y$ free.

Leaving $y$ free is the point. The substitution $y \mapsto a$ on top of it gives another unifier, and so does $y \mapsto g(b)$, and so on without end; every unifier of these two terms arises this way. The one that commits to nothing it does not have to is the most general unifier, and it is unique up to renaming its variables.

Four rules and a list of equations #

The procedure the figure ran can be stated as rules for rewriting a list of equations between terms, starting from the single equation $s = t$. This is Martelli and Montanari’s 1982 formulation, and it is the cleanest way to see that unification is a calculation rather than a search.

The four rules:

• Decompose. If both sides have the same function symbol, replace $f(s_1, \dots, s_k) = f(t_1, \dots, t_k)$ by the $k$ equations $s_i = t_i$.
• Delete. Drop an equation whose two sides are already identical.
• Orient. Rewrite $t = x$, with $x$ a variable and $t$ not, as $x = t$.
• Eliminate. Given $x = t$ with $x$ not occurring in $t$, record $x \mapsto t$ and replace $x$ by $t$ in every remaining equation and in every recorded substitution.

Two situations stop the procedure with no unifier. A clash is an equation between different function symbols, $f(\dots) = g(\dots)$, or between different constants: no substitution can change a function symbol, so the trees can never match. And an occurs failure is an equation $x = t$ where $x$ appears inside $t$ but $t$ is not $x$ itself.

Each rule either shrinks the equations or removes a variable from them for good, so the procedure always halts. When it halts with no equations left, the recorded substitution is a unifier, and it is most general because every step was forced: any unifier must satisfy each equation the rules produced, so it must agree with every elimination made.

The occurs check, and a term that does not exist #

The occurs failure is the rule that is easiest to forget and most dangerous to omit.

The equation $x = f(x)$ asks for a tree equal to itself with one extra node on top. No finite tree is, because the one with the extra node is one level deeper. The rewriting procedure, run without the check, would eliminate $x$ by $f(x)$ and find the same equation again, deeper, for ever.

The occurs check also catches cases where the circularity is hidden behind other variables.

Omitting the check is not merely slow; it is unsound. Many Prolog systems historically skip it for speed, and with it skipped they will unify $x$ with $f(x)$ and report success. Translated back into logic, that success derives conclusions that do not follow. The standard example is a pair of clauses that are perfectly consistent — every number is less than its successor, $x < s(x)$, and no number is less than itself, $\neg(y < y)$ — and resolution without the check refutes them, by unifying $x < s(x)$ with $y < y$ through the impossible $y = s(y)$. Resolution with the check is sound; without it, it proves false things, and the error is invisible because the step that went wrong produced a term that cannot be printed.

The check is also the whole difference between terms and a richer world of objects in which $x = f(x)$ does have a solution. Allow infinite trees — rational trees, which repeat — and the equation is solved by the tree that is $f$ all the way down. Some logic-programming languages adopted exactly that semantics, and in them skipping the check is not an error but a different logic. What cannot be done is mix the two: reason as if terms were finite, and unify as if they could be infinite. That mixture is the unsoundness.

The instance that is never chosen #

Here is a refutation that shows what the most general unifier buys. Three clauses: a relation $L$ is symmetric, $L(a, f(z))$ holds for every $z$, and $L(f(b), a)$ fails.

The middle clause is the thing to look at. It says $L(f(z), a)$ for every $z$ — a lemma, general in $z$, obtained without deciding what $z$ is. A ground procedure would have had to guess $z = b$ at the first step, before there was any reason to; unification postponed the decision until the goal clause forced it. In a longer proof the same lemma might be used several times with different values of $z$, and it is derived once.

This is what makes first-order resolution practical. Every derived clause is as general as the premises allow, so a single resolvent stands in for all its ground instances, and the proof search works on a handful of general clauses rather than an infinite supply of specific ones.

The figure’s three clauses are small enough that the saving looks modest — one guess avoided. It compounds. A proof that uses the symmetry clause five times, each time with different terms, would need five correctly guessed ground instances of it, each drawn from a term supply that grows without bound; the unifying proof needs the one clause, renamed apart five times, with every instance computed at the moment it is used. Where the propositional search branches on the values of variables, the first-order search never branches on the values of terms at all.

Where the function symbols come from #

The clauses in the figure contain function symbols — $f$ in $L(a, f(z))$ — and in first-order proving they usually arrive by a specific route. A statement such as for every $x$ there is a $y$ with $L(x, y)$ cannot be written as a clause directly, because a clause has only universal variables. The conversion replaces the existential $y$ by a new function of the universal variables it depends on: for every $x$, $L(x, f(x))$, where $f$ names whichever witness exists. The new function is called a Skolem function, and adding it changes the meaning of the statement — $f$ is a specific choice the original did not make — but not whether the whole set of clauses can be satisfied, which is all a refutation needs.

So a first-order refutation is typically carrying terms built from Skolem functions, and unification is what lets it reason about the witnesses without ever knowing what they are. When the lift figure’s refutation unifies $f(z)$ with $f(b)$, it is saying that the witness promised for $b$ is the one the goal is about, and it says so without computing any witness at all.

The conversion is also why first-order proving is only semi-decidable in a way that no cleverness about unification can repair. The Skolem terms nest — $f(f(f(a)))$ is a perfectly good term — so the supply of possible instances is infinite, and a set of clauses with no refutation can keep a prover generating new resolvents for ever. Unification makes each step exact; it does not bound the number of steps. That limit is Church’s and Turing’s theorem, and it is a statement about all procedures, not about this one.

Every ground proof has a general shadow #

Robinson’s completeness argument turns on a single lemma. Lifting: if two ground instances of clauses $C_1$ and $C_2$ resolve to a ground clause $R$, then $C_1$ and $C_2$ resolve, using a most general unifier, to a clause of which $R$ is an instance.

Put that together with Herbrand’s theorem and completeness follows. A set of first-order clauses is unsatisfiable exactly when some finite set of its ground instances is propositionally unsatisfiable; propositional resolution refutes those instances; and lifting carries every step of that refutation up to a first-order step with a most general unifier, the ground clause at each stage being an instance of the lifted one. The ground empty clause is an instance of only one clause — the empty one — so the lifted refutation ends in the empty clause too. Every refutation the guessing procedure could find, the unifying procedure finds in a form at least as general, and usually far shorter.

The lemma is where the “most” in most general unifier earns its place. If the procedure picked some unifier that was not most general, it would commit to a choice the ground proof might contradict later, and the lifting would fail. Only the most general unifier is guaranteed to have every ground choice as an instance.

A problem of linear size with an exponential answer #

Written as trees, unifiers can be very large.

Each equation is short, and the whole list has size proportional to $n$. But $x_n$ has to become a term in which $x_0$ appears $2^n$ times, and a procedure that represents terms as trees must write all of it out. The same term as a graph — each distinct subterm stored once, with pointers to it — is a chain of $n + 1$ nodes, because $f(x_1, x_1)$ can point twice at a single copy of $x_1$.

Mike Paterson and Mark Wegman gave a unification algorithm in 1976 that works on shared representations and runs in time linear in the size of the input, occurs check included. Practical provers use near-linear variants. The figure’s lesson is the same one Tseitin’s clauses taught about proofs: the cost of a calculation can be decided entirely by the notation it is carried out in, and the same answer is exponentially large in one representation and linear in another.

The blow-up is not an artefact of a contrived example either. Chains of equations of this shape arise naturally in type inference, where a function applied to itself a few times acquires a type whose written form doubles at each application, and in resolution proofs that compose a lemma with itself. Sharing is not an optimisation bolted on afterwards; it is what makes the algorithm’s running time proportional to the problem rather than to the answer.

The same algorithm, typing a program #

Unification has a second life that has nothing to do with proofs, or rather that turns out to be the same life. When a compiler for a language like ML or Haskell infers the type of an expression nobody annotated, it assigns every unknown a type variable and collects equations between types: applying a function of type $\alpha \to \beta$ to an argument of type $\gamma$ requires $\alpha = \gamma$, and so on. Solving those equations is unification, the most general unifier is the most general type — the principal type, in Hindley and Milner’s terminology — and the occurs check is what rejects an expression like $\lambda x.\, x\, x$, which would need a type $\alpha$ equal to $\alpha \to \beta$.

That is not an analogy. Under the correspondence between proofs and programs, a type is a formula and a well-typed program is a proof of it, and type inference is proof search in a logic where the only question is which propositional formulas to substitute for the variables. Robinson’s algorithm for theorem provers and Milner’s algorithm for type checkers were found independently, a decade apart, and they are the same four rules.

What the drawings leave out #

Every term here is small, and the algorithm is not the hard part. The figures unify terms with a handful of symbols, and unification is fast on everything. What makes first-order proving hard is not computing unifiers but deciding which pairs of literals to try — the search over resolution steps, which the drawings do not show. That search is unbounded, and no unification algorithm changes it.

Variables are renamed silently. Before resolving two clauses a prover renames the variables of one so the two share none; the figures do this without comment, and a refutation that forgot would unify variables that were only accidentally spelled alike.

Equality is not built in. Unification decides syntactic identity. If the clauses contain an equality predicate with its own axioms, then $f(a)$ and $b$ may be equal in every model without being unifiable, and a prover needs additional rules — paramodulation, or unification modulo a theory — to reason about it. Unification modulo associativity and commutativity, for instance, can have many most general unifiers rather than one.

The clauses arrive already in clause form. The figures start from clauses and never show the conversion that produces them — pushing negations inward, moving quantifiers to the front, replacing each existential by a new function of the universals it depends on. That conversion is where function symbols like $f$ in $L(a, f(z))$ usually come from, and it preserves satisfiability rather than meaning, which is enough for a refutation and not for anything else.

Still open: how the search should be steered #

Unification settles which instance to use once two literals are chosen, and Robinson’s lifting lemma settles that nothing is lost by using it. What it leaves open is the search itself, and there the questions are live. First-order validity is undecidable, so no strategy finishes on every non-theorem; but among strategies that are complete, which ones find proofs quickly is decided empirically, by competitions between provers on libraries of thousands of problems, and the theoretical understanding of why one ordering of clauses beats another is thin.

A sharper open question lives inside unification itself. For higher-order terms — where variables can stand for functions and be applied to arguments — unification is undecidable in general, and the fragments where it is decidable and has most general unifiers are known only piecemeal. Proof assistants that work in higher-order logic rely on those fragments and on heuristics outside them, and where exactly the decidable territory ends is still being mapped.

Even the first-order question has a quantitative edge. Unification with the occurs check is linear; resolution with unification is complete; and yet the sizes of shortest first-order refutations, compared with the ground refutations they lift from, are not well understood. Lifting can shorten a proof enormously, since one general clause replaces many ground ones used separately. How large the gain can be in general, and how to predict from the clauses alone whether a short lifted proof exists, is not well understood — which is one reason prover competitions are still decided by experiment.

A choice deferred until something forces it #

The Herbrand procedure asks, at every step, which instance to try, and has no good way to answer. Unification asks instead what the instance must be, given the literals that have to clash, and answers exactly — once, with the most general answer, leaving every choice not yet forced still open. It is a small algorithm and it does something large: it lets a proof carry its variables for as long as they are not needed, and fix them only at the step where a contradiction requires it.

That deferral is the same move made over and over in this subject. A tableau branch closes when two formulas clash; a two-literal clause set is refuted when a path closes a loop; and here two literals clash when a unifier exists. In each case the proof procedure does not decide anything until the structure of the formulas forces a decision, and the most general unifier is the precise form that forcing takes when the formulas have variables in them. Everything a unifier leaves free is a decision the proof has not yet had to make, and a proof that finishes with variables still free has proved something about all their values at once.