= First-order unification
<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.<An Efficient Unification Algorithm by Alberto Martelli and Ugo Montanari>[section 2, Theorems 2.1–2.2 and Algorithm 1]{ref}
For example,
$$
f(x,y)=f(g(y),a)
$$
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>.
Back to article page
