CS 251 - Discrete Structures II (Spring 2016)

See also Wikipedia, Norvig's note on a bug.

unify (t1, t2, subst):
    if t1 is var
       if t1 in subst
           return unify(t2, lookup(t1, subst), subst)
       if t2 is var ∧ t2 in subst
           return unify(t1, lookup(t2, subst), subst)
       if t1 is in t2
           fail
       return subst[t1 → t2]
    if t2 is var
        return unify(t2, t1, subst)
    if head t1 ≠ head t2
        fail
    subst' ← unify each argument in turn
    return subst'