# 13.4.1 Instances and Substitutions

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},\ldots,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}$.

###### Example 13.14.

For example, $\{X/Y,Z/a\}$ is a substitution in normal form that binds $X$ to $Y$ and binds $Z$ to $a$. The substitution$\{X/Y,Z/X\}$ 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},\ldots,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$.

###### Example 13.15.

Some applications of substitutions are

 $\displaystyle{p(a,X)\{X/c\}=p(a,c).}$ $\displaystyle{p(Y,c)\{Y/a\}=p(a,c).}$ $\displaystyle{p(a,X)\{Y/a,Z/X\}=p(a,X).}$ $\displaystyle{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 $\{X/Y,Z/a\}$ to the clause

 $p(X,Y)\leftarrow\mbox{}q(a,Z,X,Y,Z)$

is the clause

 $p(Y,Y)\leftarrow\mbox{}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.

###### Example 13.16.

$\{X/a,Y/b\}$ is a unifier of $t(a,Y,c)$ and $t(X,b,c)$ 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.

###### Example 13.17.

Atoms $p(X,Y)$ and $p(Z,Z)$ have many unifiers, including $\{X/b,Y/b,Z/b\}$, $\{X/c,Y/c,Z/c\}$, $\{X/Z,Y/Z\}$ and $\{Y/X,Z/X\}$. 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}$.

###### Example 13.18.

$\{X/Z,Y/Z\}$ and $\{Z/X,Y/X\}$ are both MGUs of $p(X,Y)$ and $p(Z,Z)$. The resulting applications

 $\displaystyle{p(X,Y)\{X/Z,Y/Z\}=p(Z,Z)}$ $\displaystyle{p(X,Y)\{Z/X,Y/X\}=p(X,X)}$

are renamings of each other.