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

Question

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.

Answer 1

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".