Some notes on Unification G6021 Comparative Programming
1 Introduction
Unification is about finding a substitution that makes two terms equal. We have seen this with both types and Prolog as examples. The way unification works is to:
1. Find the first place that the terms disagree: this is called a disagreement pair. One way to find this is to search depth first in the term. You may find it helpful to draw the term as a tree.
2. Using the disagreement pair, we check:
(a) are the two terms incompatible, in which case fail;
(b) if one term is a variable, then we can make a substitution (unless we have the occur check);
(c) if the pair is empty then stop – we have found a unifying substitution.
3. Apply the substitution to both terms and go back to step.
We look at some examples from types and Prolog.
2 Types
Assume we have some base types, say int and bool, and type variables, A, B, etc., and function types, of the form (σ → τ), where σ and τ can be any type. We drop brackets when we can (they associate to the right!)
Exercise: Which of the following are valid types?
int,bool,int → bool,bool → int,A → int,(int → int) → bool,bool → A → A
See footnote for solutions.1
Given two types, we can find the disagreement pair by searching through the two types for the first place that they differ.
Exercise: for each pair of types P, Q in the table below, find the first disagreement pair:
P
Q
int
int
A
A
A→B A→B→C (A → int) → B A→B→C
int
bool
int
B→A
A→A A→B→B
B → bool → bool int → int
1All of them.
1
(Hint: put brackets in to help with this.)
Answer:
If the disagreement set it empty, it means that the types are the same (there is nothing to do to unify them). If the disagreement pair contains two different base types, for example (int, bool) then the types do not unify. If the pair contains a variable and a type, say (A, int → B) then we can replace all occurrences of A by int → B in both P and Q and repeat the process. Finally, if the pair contains a variable and a type, say (A,int → A) where the variable A occurs in the second type, the these cannot unify (this is called the occur check).
Exercise: When a substitution can be created from the disagreement pair, show the types P and Q with the substitution applied.
Answer:
P
Q
D(P, Q)
int
int
A
A
A→B A→B→C (A → int) → B A→B→C
int
bool
int
B→A
A→A A→B→B
B → bool → bool int → int
∅
(int, bool) (A, int)
(A, B → A) (B,A) (C,B)
(A → int, B) (A, int)
P
Q
D(P, Q)
P
Q
int
int
A
A
A→B A→B→C (A → int) → B A→B→C
int
bool
int
B→A
A→A A→B→B
B → bool → bool int → int
∅
(int, bool) (A, int)
(A, B → A) (B,A) (C,B)
(A → int, B) (A, int)
int
−
int
−
B→B
A→C→C
(A → int) → A → int int → B → C
int
−
int
−
B→B
A→C→C
(A → int) → bool → bool int → int
We can repeat this process of finding the disagreement pair and creating a substitution until either the unification fails or the disagreement set it empty (in which case we have found a substitution that makes them unify). Try to complete this process (hint: the last two do not unify).
3 Prolog
The same ideas from above work also for Prolog: for each term we find a substitution to make the terms equal. We follow exactly the same algorithm: find the disagreement pair and repeat until either we find that the terms cannot unity or we find a substitution that makes the terms equal.
Exercise: which of these pairs of terms unify? Write the unifying substitution if they unify.
Answer:
0
X
f(A,[],A)
f (1, g([1, 2])) f (0, g([1, 2]))
s(0)
[1, 2] f([],X,X) f(H,g([H|T])) f(H,g([H|T]))
2
0
X
f(A,[],A)
f (1, g([1, 2])) f (0, g([1, 2]))
s(0)
[1, 2] f([],X,X) f(H,g([H|T])) f(H,g([H|T))
−(f ail)
X = [1, 2]
A = [], X = []
H = 1, T = [2]
H = 0,H = 1(fail)
4 Type Trees
You may find it useful to draw types/terms as trees and then do depth first search to find the disagreement pair.
Wecandefinethetreeforabasetypeoravariabletobealeafofthetree. ThenT(A→B), the tree of A → B, would be given by:
→
T (B) Draw P and Q from above as trees to test out this idea.
Exercise: how would you draw Prolog terms as trees in this way? Try to draw some examples.
T (A)
3
E
‘