1. Unification

Unification Problem

A unification problem $\mathcal{U}$ is a set of equations between terms containing variables.

$$\{s_1=t_1,\dots ,t_n=t_n\}$$

A solution to $\mathcal{U}$, also called a unifier, is a substitution $\sigma$, such that when applied to every term in $\mathcal{U}$, for each equation $s_i=t_i$, the terms $s_i\sigma$ and $t_i\sigma$ are syntactically identical.

Link to original

Most General Unifier

Most general unifier (semantics)

The most general unifier of $\mathcal{U}$ is a unifier $\sigma$ such that any other unifier $p$ is an instance of $\sigma$.

Link to original

Consider the unification problem $\mathcal{U}=\{f(X)=f(Y)\}$ and substitutions $\sigma =\{X\mapsto Y\}$ and $p=\{X\mapsto a;Y\mapsto a\}$.

Both substitutions make the terms $f(X)$ and $f(Y)$ syntactically identical:

• $f(X)\sigma =f(Y)=f(Y)\sigma$
• $f(X)\rho =r(a)=f(Y)\rho$

Hence they are both unifiers. However, $\sigma$ is more general than $\rho$ because $\rho$ is an instance of $\sigma$. (apply the substitution $\gamma =\{Y\mapsto a\}$ after $\sigma$ gives us $\rho$), but $\rho$ is not an instance of $\sigma$ (we cannot get $\sigma$ from $\rho$).

In this case, we can also say that $\sigma$ is the most general unifier because no other unifier is more general than $\sigma$ is.

Intuition

Substitutions applied to entire clauses allow them to resolve. Those that “commit” variables to specific terms (constants, function terms) prevent future substitutions from being able to act as unifiers.

Example of "committing" variables

We can unify the atoms $p(X)$ and $p(Y)$ in the clauses: $p(X)\vee \neg q(X)\text{ and }\neg p(Y)$ either by replacing $X$ by $Y$ (or $Y$ by $X$), or by replacing both $X$ and $Y$ by some constant.

The first two substitutions would allow us to unify the resolvent $\neg q(X)$ (or $\neg q(Y))$ with the clause $q(b)$, the former would not.

Replacing $X$ and $Y$ by $a$ early commits the variable $X$ (or $Y$) to the constant $a$, generating the new clause $\neg q(a)$ and would not allow resolution of this clause with any atom involving anything other than $a$. So we want to leave variables “free”, unless we need to bind them for unification to succeed.

Unification Algorithm

The unification algorithm finds the most general unifier for a unification problem if a solution exists, or otherwise fails, indicating there are no solutions. To find the mgu, the algorithm simplifies the set of equations using a set of transformation rules.

At each step, either a new set of equations is produced or a failure case arises. Algorithm terminates and outputs mgu when no rule may be applied.

The algorithm has:

• an input of: a finite set of term equations $\{s_1=t_1,\dots ,s_n=t_n\}$
• an output of: the mgu of those equations or failure

We follow the rules:

1. $f(s_1,\dots ,s_n)=f(t_1,\dots ,t_n),E\to s_1=t_1,\dots ,s_n=t_N,E$ this and the following rule also apply to constants
2. $f(s_1,\dots ,s_n)=f(t_1,\dots ,t_n),E\to \text{failure}$
3. $X=X,E\to E$
4. $t=X,E\to X=t,E\text{ if }t\text{ is not a variable}$
5. $X=t,E\to X=t,E\{X\mapsto t\}\text{ if }X\text{ not in }t\text{ and }X\text{ in }E$
6. $X=t,E\to \text{failure if }X\text{ occurs in }t\text{ and }X\ne t$ this is called an occur-check for example if $X=f(X)$ is a failure case this step is time-consuming and sometimes omitted

The unification algorithm applies the rules in a non-deterministic way until no further rules can be applied or a failure case arises. In the case of success, we can change each $=$ in the final set of equations to $\mapsto$ in order to obtain the mgu of the initial set of terms.

Unification Examples

$\{f(a,a)=f(X,a)\}$

1. use rule (1) with the first equation: $\{a=X,a=a\}$
2. use rule (4) with the first equation: $\{X=a,a=a\}$
3. use rule (1) with the second equation: $\{X=a\}$

Output: $\{X\mapsto a\}$

$\{[X|L]=[0],Y=[1,2],[X|Z]=U\}$

1. use rule (1) with the first equation: $\{X=0,L=[],Y=[1,2],[X|Z]=U\}$
2. use rule (5) with the first equation: $\{X=0,L=[],Y=[1,2],[0|Z]=U\}$
3. use rule (4) with the last equation: $\{X=0,L=[],Y=[1,2],U=[0|Z]\}$

Output: $\{X\mapsto 0,L\mapsto [],Y\mapsto [1,2],U\mapsto [0|Z]\}$

$\{f(g(a),b)=f(X,b),X=g(Z),f(a,Y)=f(Z,Y)\}$

1. use rule (1) on 1: $\{g(a)=X,b=b,X=g(Z),f(a,Y)=f(Z,Y)\}$
2. use rule (4) on 1: $\{X=g(a),b=b,X=g(Z),f(a,Y)=f(Z,Y)\}$
3. use rule (5) on 1: $\{X=g(a),b=b,g(a)=g(Z),f(a,Y)=f(Z,Y)\}$
4. use rule (1) on 2: $\{X=g(a),g(a)=g(Z),f(a,Y)=f(Z,Y)\}$
5. use rule (1) on 2: $\{X=g(a),a=Z,f(a,Y)=f(Z,Y)\}$
6. use rule (4) on 2: $\{X=g(a),Z=a,f(a,Y)=f(Z,Y)\}$
7. use rule (5) on 2: $\{X=g(a),Z=a,f(a,Y)=f(a,Y)\}$
8. use rule (1) on 3: $\{X=g(a),Z=a,a=a,Y=Y\}$
9. use rule (1) on 3: $\{X=g(a),Z=a,Y=Y\}$
10. use rule (3) on 3: $\{X=g(a),Z=a\}$

Output: $\{X\mapsto g(a),Z\mapsto a\}$