# Inference and Unification algorithm provided to a Unification graph of two expressions

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.

Yes, your solution and process are correct, assuming that alpha and beta are variables. It might help to rewrite your terms in a more uniform way, e.g.

T1 = *(list(int), list(alpha))
T2 = *(alpha, beta)


Here, a term always satisfies the grammar:

Term ::= Constant
| Variable
| Func "(" Term+ ")"


Furthermore, it might clarify things to think of the unification process as taking a third argument: a substitution in which the two terms are to be unified. This substitution is simply an association between variables and terms, and it provides a context in which to resolve variables. Additionally, the unification process results in either a failure (if the terms do not unify in the substitution), or a substitution which both indicates success and provides a way to construct a "most general unifier".