Most General Unifier

A substitution, $\sigma$, is a most general unifier (mgu) of a set of expressions $E$ if it unifies $E$, and for any unifier, $\omega$, of $E$, there is a unifier, $\lambda$, such that $\omega = \sigma \circ \lambda$.

The idea is that $\sigma$ is less specific than (technically, no more specific than) $\omega$, that is, we can substitute for some of the variables of $\sigma$ and get $\omega$. Note that there can be more than one most general unifier, but such substitutions are the same except for variable renaming.

In the above example, $\sigma_2$ is the mgu of the set of expressions. We can see that $\sigma_1 = \sigma_2 \circ [a/x]$.

There is a simple algorithm for finding the most general unifier of a set of expressions. First, we need to define the disagreement set of a set of expressions. This is found by (textually) finding the first symbol starting from the left that is not the same in every expression and extracting the subexpressions that begin with that symbol at that position in each expression of the set. The resulting set of subexpressions is the disagreement set. For example, the disagreement set for $\{ P(x,y,a), P(x,f(g),b), P(x,f(g),x) \}$ is $\{y, f(g)\}$.

The algorithm for finding the most general unifier for a set of expressions $E$ is as follows:

$\sigma = [\;]$ (the empty substitution) 


while($E$ is not a singleton) { 

$D =$ disagreement set of $E$; 


if($D$ contains a variable, say $x$, and a term, say $t$, that doesn't contain $x$) { 

$E = [t/x](E)$; 

$\sigma = \sigma \circ [t/x]$; 

} 


else 


return ``Not unifiable''; 

} 


return $\sigma$;

We can prove, but won't, that this algorithm always returns the mgu, if one exists.