Most General Unifier

type-theory

Definition

Most General Unifier

A most general unifier of two expressions $s$ and $t$ is a unifier $U$ such that every other unifier factors through $U$.

Formally, $U$ is a most general unifier iff:

$$U(s)=U(t)$$

and for every unifier $S$ with $S(s)=S(t)$, there exists a substitution $R$ such that

$$S=R\circ U.$$

Thus $U$ makes $s$ and $t$ equal while committing to no unnecessary substitutions.