I am trying to unify two expressions given a unification algorithm $unify$ applied to the unification graph of the two expressions. However, I struggle a lot in understanding how exactly the steps of this algorithm is actually done - and my teacher failed to explain this in much detail. The following example is part of an exercise.
The two expressions I am trying to unify are: $$list(int) * list(alpha)$$ $$alpha * beta$$
With the following unification graph:
* *
/ \ / \
/ \ / \
list list / \
| | / \
| | / \
int alpha beta
The algorithm is from the Dragon Book
and shown below:
boolean unify(Node m, Node n) {
s = find(m); t = find(n)
if (s = t) then true;
else if (nodes s and t represent the same basic type) return true;
else if (s is an op-node with children s1 & s2 and
t is an op-node with children t1 & t2) {
union(s,t)
return unify(s1,t1) and unify(s2,t2)
}
else if (s or t represents a variable) {
union(s,t)
return true;
}
else return false;
}
My method of approach with this algorithm yielded the following result:
(1) Union the two constructors $*$ and call unify(list,alpha) and unify(list,beta)_
(2) Since the dragon book states that a variable is a leaf node, I can use Step III to union list <- alpha, and list <- beta. This returns true in the function._
From above I have that $alpha = list(int)$ and $beta = list(alpha)$. I can then construct the unified type to be: $$list(int) * list(list(int))$$
Can anyone verify for me if this is correct? I found the algorithm a bit tricky to understand, especially since I compare a constructor list
with basic types in the (2) step.