On the off chance that you are trying to write a Prolog interpreter, don't do what I did.

What did I do? I tried to store a bunch of equations amongst the various variables, and used a connected-component-finding algorithm to determine whether two things are required to be equal.

Instead, do what everyone else does, which is to just make substitutions directly in the unificands (?). This way, equals will still be required to be equal, but you don't have to search the graph every time you want to check whether two things are meant to be equal. My original algorithm was 50 lines of ML, and the bloody thing actually worked, but after I did some reading about unification, I sat down and wrote this:

fun unify [] result = result
  | unify ((Leaf name, T)::others) result =
	unify (map (cross (subst(Leaf name, T))) others)
			([(Leaf name, T)] @ result)
  | unify ((T, Leaf name)::others) result =
	unify (map (cross (subst(Leaf name, T))) others) 
			([(T, Leaf name)] @ result)
  | unify ((Op(sop, sargs), Op(top, targs))::others) result =
  	if sop = top then
		unify (zip sargs targs @ others) result
	else
		unify others result;

For those at home, that's 12 lines (the utilty routines are given in a footnote, for bean counters), and it actually does more than my naive 50-line monster. I tweaked the above about three times before I got it, and then it worked: I spent about an hour. The bulk of yesterday and today got the surrounding code that does the searching and matching on full Prolog expressions.

The morning after I wrote the above (Monday), I got out of bed and pulled out Pierce, Types and Programming Languages, and here's what he has:

unify(C) = if C = ∅, then [ ]
           else let {S = T} ∪ C' = C in
               if S = T
                   then unify(C')
               else if S = X and X ∉ FV(T)
                   then unify([X = T]C') ∘ [X = T]
               else if T = X and X ∉ FV(S)
                   then unify([X = S]C') ∘ [X = S]
               else if S = S1 → S2 and T = T1 → T2
                   then unify(C' ∪ {S1 = T1, S2 = T2})
               else
                   fail

Almost exactly the same thing. The key differences are that I didn't do the free-variable check (X ∉ FV(T)) and I didn't compose the new substitution onto the result of the recursive call (that's the "∘ [X â†’ T]" clause). So, mine could be made to break. Still, I did pretty good for a guy who didn't really know what he was doing.

---

Appendix

The details.

datatype TermTree =   Var of string | Const of string
                    | Op of string * TermTree list;

fun cross f(X, Y) = (f X, f Y);

fun zip [] [] = []
  | zip (x::xs) (y::ys) = (x, y) :: zip xs ys
  | zip _ _ = raise LengthMismatch;
  
fun subst (this, that) (Const C) = Const C
  | subst (this, that) (Var X) = if this = Var X then that else Var X
  | subst (this, that) (Op(name, args)) =
                                  Op(name, map (subst (this, that)) args);

I also updated it to treat constants and variables differently:

fun unify [] result = SOME result
  | unify ((Const c, Const d)::others) result = 
  	if c = d then
  		unify others result
  	else
  		NONE
  | unify ((Var name, T)::others) result =
	unify (map (cross (subst(Var name, T))) others)
			(comp_one result (Var name, T))
  | unify ((T, Var name)::others) result =
	unify (map (cross (subst(Var name, T))) others) 
			(comp_one result (Var name, T))
  | unify ((Op(sop, sargs), Op(top, targs))::others) result =
  	if sop = top then
		unify (zip sargs targs @ others) result
	else
		NONE
  | unify _ _ = NONE;