Unification

Unification finds a substitution making given first-order terms syntactically identical. In first-order unification, a substitution replaces variables by first-order terms while leaving function symbols fixed. A most general unifier captures the necessary identifications: every other unifier follows by a further substitution.^[ref]

For example, $f(x,g(y))$ and $f(g(z),g(a))$ have most general unifier $\{x\mapsto g(z),y\mapsto a\}$. The variable $z$ remains free; assigning it a particular first-order term gives a more specific unifier. Requiring $f(x,x)=f(a,b)$ forces both $x=a$ and $x=b$, so distinct constant symbols $a,b$ make it impossible.

Syntactic identity is essential. With addition treated as a binary function symbol, the first-order terms $x+0$ and $x$ are different even though their values agree under ordinary arithmetic. Equational unification incorporates specified identities and is a different problem. For finite first-order terms, the occurs check rejects $x=f(x)$: a finite first-order term cannot equal one of its proper subterms. Unification makes resolution possible by aligning atomic formulas before inference.

Equational unification asks for a first-order substitution making two first-order terms equal under specified identities, rather than requiring them to become literally the same first-order term. Writing ${=}_E$ for equality justified by those identities, a solution $\sigma$ satisfies $s\sigma {=}_{E}t\sigma$.

For example, the first-order terms $f(a,b)$ and $f(b,a)$ have no syntactic unifier when $a,b$ are distinct constant symbols and $f$ is an uninterpreted binary function symbol. If the specified identity is commutativity, $f(x,y)=f(y,x)$, then the unchanged first-order terms are already equal modulo that identity: the empty first-order substitution is an equational unifier.

The identity set changes the problem. Ordinary first-order unification can decompose equal outer constructors because equality of free first-order terms forces equality of corresponding arguments. Modulo commutativity, argument positions can be exchanged, so that decomposition alone would reject legitimate solutions. A useful implementation must state its identities and its notion of solution, rather than treating equality of interpreted values as syntactic equality.

A unifier of first-order terms $s,t$ is a first-order substitution $\sigma$ for which $s\sigma =t\sigma$. The first-order substitution replaces variables by first-order terms; it does not alter function symbols. For example, $\{x\mapsto a,y\mapsto b\}$ unifies $f(x,g(y))$ with $f(a,g(b))$.

A most general unifier leaves every identification not forced by the original equations available for later choice. For $f(x,y)=f(y,z)$, one solution is $\{x\mapsto z,y\mapsto z\}$. The remaining variable $z$ is free. Replacing it by any finite first-order term gives a more specific unifier; arbitrarily choosing $z=a$ during the initial computation would discard that generality.

Not every pair is unifiable. Distinct constant symbols cannot be made equal by replacing variables, and the occurs check rejects $x=f(x)$ for finite first-order terms. These are structural restrictions, not numerical inequalities. Unifiers allow a resolution step to align the relevant atomic formulas before the logical inference is performed.^[ref]

First-order unification solves a finite system of equations between first-order terms. A useful rule presentation deletes $t=t$, orients $t=x$ to $x=t$ when $x$ is a variable, decomposes equal outer function symbols into argument equations, and rejects unequal outer function symbols. For $x=t$, reject a nontrivial occurrence of $x$ in $t$ by the occurs check; otherwise propagate the substitution $x\mapsto t$ through the other equations. A solved system assigns distinct variables that do not occur in its right sides.^[ref]

For example,first becomes $x=g(y),y=a$. Propagating $y\mapsto a$ gives $x=g(a),y=a$, hence a most general unifier. Keeping $x=g(y)$ without composing the later substitution would leave an unsolved dependency.

The rules preserve the possible unifiers, apart from explicitly rejecting impossible equations. Decomposition works because identical first-order terms have identical constructors and arguments. At a solved system, any other unifier is obtained by instantiating its remaining free variables; this proves the most general unifier property. Efficient implementations share term graphs rather than repeatedly copying growing first-order terms.

A term graph represents the structure of first-order terms with labelled nodes and ordered argument graph edges. For finite acyclic first-order terms, the representation can be a directed acyclic graph, allowing identical subterms to share nodes rather than being copied into separate branches of a tree.

The first-order term $f(g(a),g(a))$ has five occurrences in its ordinary syntax tree: one $f$, two $g$ and two $a$. A shared term graph can use only three nodes, with the two argument graph edges of $f$ pointing to the same $g$ node. Sharing a variable node is also useful: identifications made by a unification algorithm can be represented once and followed from every occurrence.^[ref]

Sharing changes storage, not the meaning of an acyclic finite first-order term. A cycle is different. A node labelled $f$ whose argument points back to itself unfolds to an infinite rational tree; it cannot represent a finite solution to $x=f(x)$. An implementation must therefore state whether it supports infinite rational trees or enforces the finite-term occurs check.

A rational tree is a possibly infinite tree with only finitely many distinct rooted subtrees. It therefore has a finite representation as a term graph, possibly with cycles. Here “rational” describes finite representability, not values in the rational numbers.

For example, the equation $X=f(X)$ describes the infinite expression $f(f(f(\cdots )))$. A single node labeled $f$ with an edge back to itself represents it. There is no solution among finite first-order terms: the occurs check rejects binding a variable to a first-order term containing that variable. Unification over rational trees instead admits this cyclic representation, so implementations must specify which semantics they use. SWI-Prolog explicitly supports cyclic terms for many term operations.^[ref]

The Robinson unification algorithm solves equations between first-order terms by finding a substitution making them identical. Repeatedly delete equal terms, decompose equal function symbols into argument equations, reject incompatible symbols, and substitute a variable by its proposed term. The occurs check rejects $x=f(x)$ for finite-term unification, since no finite term equals a proper term containing itself. For $f(x,a)=f(b,y)$ it returns $x\mapsto b$, $y\mapsto a$. Successful finite-term unification yields a most general unifier: every other unifier is obtained by further substitution. Implementations that omit the occurs check instead admit a different cyclic-term interpretation.

A most general unifier is a unifying substitution through which every other unifier factors by a further substitution. It records exactly the equality constraints forced by the terms.