foundations of computational agents
An instance of a clause is obtained by uniformly substituting terms for variables in the clause. All occurrences of a particular variable are replaced by the same term.
The specification of which value is assigned to each variable is called a substitution. A substitution is a set of the form $\{{V}_{1}/{t}_{1},\mathrm{\dots},{V}_{n}/{t}_{n}\}$, where each ${V}_{i}$ is a distinct variable and each ${t}_{i}$ is a term. The element ${V}_{i}/{t}_{i}$ is a binding for variable ${V}_{i}$. A substitution is in normal form if no ${V}_{i}$ appears in any ${t}_{j}$.
For example, ${\mathrm{\{}}{X}{\mathrm{/}}{Y}{\mathrm{,}}{Z}{\mathrm{/}}{a}{\mathrm{\}}}$ is a substitution in normal form that binds ${X}$ to ${Y}$ and binds ${Z}$ to ${a}$. The substitution${\mathrm{\{}}{X}{\mathrm{/}}{Y}{\mathrm{,}}{Z}{\mathrm{/}}{X}{\mathrm{\}}}$ is not in normal form, because the variable ${X}$ occurs both on the left and on the right of a binding.
The application of a substitution $\sigma =\{{V}_{1}/{t}_{1},\mathrm{\dots},{V}_{n}/{t}_{n}\}$ to expression $e$, written $e\sigma $, is an expression that is the same as the original expression $e$ except that each occurrence of ${V}_{i}$ in $e$ is replaced by the corresponding ${t}_{i}$. The expression $e\sigma $ is called an instance of $e$. If $e\sigma $ does not contain any variables, it is called a ground instance of $e$.
Some applications of substitutions are
${p}{}{(}{a}{,}{X}{)}{}{\{}{X}{/}{c}{\}}{=}{p}{}{(}{a}{,}{c}{)}{.}$ | ||
${p}{}{(}{Y}{,}{c}{)}{}{\{}{Y}{/}{a}{\}}{=}{p}{}{(}{a}{,}{c}{)}{.}$ | ||
${p}{}{(}{a}{,}{X}{)}{}{\{}{Y}{/}{a}{,}{Z}{/}{X}{\}}{=}{p}{}{(}{a}{,}{X}{)}{.}$ | ||
${p}{}{(}{X}{,}{X}{,}{Y}{,}{Y}{,}{Z}{)}{}{\{}{X}{/}{Z}{,}{Y}{/}{t}{\}}{=}{p}{}{(}{Z}{,}{Z}{,}{t}{,}{t}{,}{Z}{)}{.}$ |
Substitutions can apply to clauses, atoms, and terms. For example, the result of applying the substitution ${\mathrm{\{}}{X}{\mathrm{/}}{Y}{\mathrm{,}}{Z}{\mathrm{/}}{a}{\mathrm{\}}}$ to the clause
$${p}{}{(}{X}{,}{Y}{)}{\leftarrow}{}{q}{}{(}{a}{,}{Z}{,}{X}{,}{Y}{,}{Z}{)}$$ |
is the clause
$${p}{}{(}{Y}{,}{Y}{)}{\leftarrow}{}{q}{}{(}{a}{,}{a}{,}{Y}{,}{Y}{,}{a}{)}{.}$$ |
A substitution $\sigma $ is a unifier of expressions ${e}_{1}$ and ${e}_{2}$ if ${e}_{1}\sigma $ is identical to ${e}_{2}\sigma $. That is, a unifier of two expressions is a substitution that when applied to each expression results in the same expression.
${\{}{X}{/}{a}{,}{Y}{/}{b}{\}}$ is a unifier of ${t}{\mathit{}}{\mathrm{(}}{a}{\mathrm{,}}{Y}{\mathrm{,}}{c}{\mathrm{)}}$ and ${t}{\mathit{}}{\mathrm{(}}{X}{\mathrm{,}}{b}{\mathrm{,}}{c}{\mathrm{)}}$ as
$${t}{}{(}{a}{,}{Y}{,}{c}{)}{}{\{}{X}{/}{a}{,}{Y}{/}{b}{\}}{=}{t}{}{(}{X}{,}{b}{,}{c}{)}{}{\{}{X}{/}{a}{,}{Y}{/}{b}{\}}{=}{t}{}{(}{a}{,}{b}{,}{c}{)}{.}$$ |
Expressions can have many unifiers.
Atoms ${p}{\mathit{}}{\mathrm{(}}{X}{\mathrm{,}}{Y}{\mathrm{)}}$ and ${p}{\mathit{}}{\mathrm{(}}{Z}{\mathrm{,}}{Z}{\mathrm{)}}$ have many unifiers, including ${\mathrm{\{}}{X}{\mathrm{/}}{b}{\mathrm{,}}{Y}{\mathrm{/}}{b}{\mathrm{,}}{Z}{\mathrm{/}}{b}{\mathrm{\}}}$, ${\mathrm{\{}}{X}{\mathrm{/}}{c}{\mathrm{,}}{Y}{\mathrm{/}}{c}{\mathrm{,}}{Z}{\mathrm{/}}{c}{\mathrm{\}}}$, ${\mathrm{\{}}{X}{\mathrm{/}}{Z}{\mathrm{,}}{Y}{\mathrm{/}}{Z}{\mathrm{\}}}$ and ${\mathrm{\{}}{Y}{\mathrm{/}}{X}{\mathrm{,}}{Z}{\mathrm{/}}{X}{\mathrm{\}}}$. The last two unifiers are more general than the first two, because the first two both have ${X}$ the same as ${Z}$ and ${Y}$ the same as ${Z}$ but make more commitments to what these values are.
Substitution $\sigma $ is a most general unifier (MGU) of expressions ${e}_{1}$ and ${e}_{2}$ if
$\sigma $ is a unifier of the two expressions, and
if substitution ${\sigma}^{\prime}$ is also a unifier of ${e}_{1}$ and ${e}_{2}$, then $e{\sigma}^{\prime}$ must be an instance of $e\sigma $ for all expressions $e$.
Expression ${e}_{1}$ is a renaming of ${e}_{2}$ if they differ only in the names of variables. In this case, they are both instances of each other.
If two expressions have a unifier, they have at least one MGU. The expressions resulting from applying the MGUs to the expressions are all renamings of each other. That is, if $\sigma $ and ${\sigma}^{\prime}$ are both MGUs of expressions ${e}_{1}$ and ${e}_{2}$, then ${e}_{1}\sigma $ is a renaming of ${e}_{1}{\sigma}^{\prime}$.
${\{}{X}{/}{Z}{,}{Y}{/}{Z}{\}}$ and ${\mathrm{\{}}{Z}{\mathrm{/}}{X}{\mathrm{,}}{Y}{\mathrm{/}}{X}{\mathrm{\}}}$ are both MGUs of ${p}{\mathit{}}{\mathrm{(}}{X}{\mathrm{,}}{Y}{\mathrm{)}}$ and ${p}{\mathit{}}{\mathrm{(}}{Z}{\mathrm{,}}{Z}{\mathrm{)}}$. The resulting applications
${p}{}{(}{X}{,}{Y}{)}{}{\{}{X}{/}{Z}{,}{Y}{/}{Z}{\}}{=}{p}{}{(}{Z}{,}{Z}{)}$ | ||
${p}{}{(}{X}{,}{Y}{)}{}{\{}{Z}{/}{X}{,}{Y}{/}{X}{\}}{=}{p}{}{(}{X}{,}{X}{)}$ |
are renamings of each other.