Unifier (source code)
= Unifier
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.<An Efficient Unification Algorithm by Alberto Martelli and Ugo Montanari>[Introduction and Section2, substitutions and solved equation systems]{ref}
Back to article page
