Intelligence 2E

foundations of computational agents

The problem of unification is the following: given two atoms or terms, determine whether they unify, and, if they do, return a unifier of them. The unification algorithm finds a most general unifier (MGU) of two atoms or returns $\perp $ if they do not unify.

The unification algorithm is given in Figure 13.3. $E$ is a set of equality statements implying the unification, and $S$ is a set of equalities of the correct form of a substitution. In this algorithm, if $\alpha /\beta $ is in the substitution $S$, then, by construction, $\alpha $ is a variable that does not appear elsewhere in $S$ or in $E$. In line 20, $\alpha $ and $\beta $ must have the same predicate and the same number of arguments; otherwise the unification fails.

Suppose you want to unify ${p}{\mathit{}}{\mathrm{(}}{X}{\mathrm{,}}{Y}{\mathrm{,}}{Y}{\mathrm{)}}$ with ${p}{\mathit{}}{\mathrm{(}}{a}{\mathrm{,}}{Z}{\mathrm{,}}{b}{\mathrm{)}}$. Initially ${E}$ is ${\mathrm{\{}}{p}{\mathit{}}{\mathrm{(}}{X}{\mathrm{,}}{Y}{\mathrm{,}}{Y}{\mathrm{)}}{\mathrm{=}}{p}{\mathit{}}{\mathrm{(}}{a}{\mathrm{,}}{Z}{\mathrm{,}}{b}{\mathrm{)}}{\mathrm{\}}}$. The first time through the while loop, ${E}$ becomes ${\mathrm{\{}}{X}{\mathrm{=}}{a}{\mathrm{,}}{Y}{\mathrm{=}}{Z}{\mathrm{,}}{Y}{\mathrm{=}}{b}{\mathrm{\}}}$. Suppose ${X}{\mathrm{=}}{a}$ is selected next. Then ${S}$ becomes ${\mathrm{\{}}{X}{\mathrm{/}}{a}{\mathrm{\}}}$ and ${E}$ becomes ${\mathrm{\{}}{Y}{\mathrm{=}}{Z}{\mathrm{,}}{Y}{\mathrm{=}}{b}{\mathrm{\}}}$. Suppose ${Y}{\mathrm{=}}{Z}$ is selected. Then ${Y}$ is replaced by ${Z}$ in ${S}$ and ${E}$. ${S}$ becomes ${\mathrm{\{}}{X}{\mathrm{/}}{a}{\mathrm{,}}{Y}{\mathrm{/}}{Z}{\mathrm{\}}}$ and ${E}$ becomes ${\mathrm{\{}}{Z}{\mathrm{=}}{b}{\mathrm{\}}}$. Finally ${Z}{\mathrm{=}}{b}$ is selected, ${Z}$ is replaced by ${b}$, ${S}$ becomes ${\mathrm{\{}}{X}{\mathrm{/}}{a}{\mathrm{,}}{Y}{\mathrm{/}}{b}{\mathrm{,}}{Z}{\mathrm{/}}{b}{\mathrm{\}}}$, and ${E}$ becomes empty. The substitution ${\mathrm{\{}}{X}{\mathrm{/}}{a}{\mathrm{,}}{Y}{\mathrm{/}}{b}{\mathrm{,}}{Z}{\mathrm{/}}{b}{\mathrm{\}}}$ is returned as an MGU.

Consider unifying ${p}{\mathit{}}{\mathrm{(}}{a}{\mathrm{,}}{Y}{\mathrm{,}}{Y}{\mathrm{)}}$ with ${p}{\mathit{}}{\mathrm{(}}{Z}{\mathrm{,}}{Z}{\mathrm{,}}{b}{\mathrm{)}}$. ${E}$ starts off as ${\mathrm{\{}}{p}{\mathit{}}{\mathrm{(}}{a}{\mathrm{,}}{Y}{\mathrm{,}}{Y}{\mathrm{)}}{\mathrm{=}}{p}{\mathit{}}{\mathrm{(}}{Z}{\mathrm{,}}{Z}{\mathrm{,}}{b}{\mathrm{)}}{\mathrm{\}}}$. In the next step, ${E}$ becomes ${\mathrm{\{}}{a}{\mathrm{=}}{Z}{\mathrm{,}}{Y}{\mathrm{=}}{Z}{\mathrm{,}}{Y}{\mathrm{=}}{b}{\mathrm{\}}}$. Then ${Z}$ is replaced by ${a}$ in ${E}$, and ${E}$ becomes ${\mathrm{\{}}{Y}{\mathrm{=}}{a}{\mathrm{,}}{Y}{\mathrm{=}}{b}{\mathrm{\}}}$. Then ${Y}$ is replaced by ${a}$ in ${E}$, and ${E}$ becomes ${\mathrm{\{}}{a}{\mathrm{=}}{b}{\mathrm{\}}}$, and then ${\mathrm{\perp}}$ is returned indicating that there is no unifier.