12.4.2.1 Unification

The preceding algorithms assumed that we could find the most general unifier of two atoms. The problem of unification is the following: given two atoms, determine if they unify, and, if they do, return an MGU of them.

1: Procedure Unify(t1,t2)
2:           Inputs
3:                     t1,t2: atoms Output
4:                     most general unifier of t1 and t2 if it exists or ⊥ otherwise
5:           Local
6:                     E: a set of equality statements
7:                     S: substitution
8:           E ←{t1=t2}
9:           S={}
10:           while (E≠{})
11:                     select and remove x=y from E
12:                     if (y is not identical to x) then
13:                               if (x is a variable) then
14:                                         replace x with y everywhere in E and S
15:                                         S←{x/y}∪S
16:                               else if (y is a variable) then
17:                                         replace y with x everywhere in E and S
18:                                         S←{y/x}∪S
19:                               else if (x is f(x1,...,xn) and y is f(y1,...,yn)) then
20:                                         E←E∪{x1=y1,...,xn=yn}
21:                               else
22:                                         return ⊥
23:           return S
Figure 12.5: Unification algorithm for Datalog

The unification algorithm is given in Figure 12.5. 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 x/y is in the substitution S, then, by construction, x is a variable that does not appear elsewhere in S or in E. In line 19, x and y must have the same predicate and the same number of arguments; otherwise the unification fails.

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