13.4 Proofs and Substitutions

13.4.3 Unification

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 if they do not unify.

1:procedure Unify(t1,t2)
2:      Inputs
3:            t1,t2: atoms or terms       
4:      Output
5:            most general unifier of t1 and t2 if it exists or otherwise
6:      Local
7:            E: a set of equality statements
8:            S: substitution       
9:      E{t1=t2}
10:      S={}
11:      while E{} do
12:            select and remove α=β from E
13:            if β is not identical to α then
14:                 if α is a variable then
15:                       replace α with β everywhere in E and S
16:                       S{α/β}S
17:                 else if β is a variable then
18:                       replace β with α everywhere in E and S
19:                       S{β/α}S
20:                 else if α is p(α1,,αn) and β is p(β1,,βn) then
21:                       EE{α1=β1,,αn=βn}
22:                 else
23:                       return                                    
24:      return S
Figure 13.3: Unification algorithm for Datalog

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 α/β is in the substitution S, then, by construction, α is a variable that does not appear elsewhere in S or in E. In line 20, α and β must have the same predicate and the same number of arguments; otherwise the unification fails.

Example 13.22.

Suppose you 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.

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