(define unify
   X Y -> (unify-loop X Y []))

(define unify-loop
   X X MGU -> MGU
   X Y MGU -> [[X | Y] | MGU]    where (and (variable? X) (occurs-check? X Y))
   X Y MGU -> [[Y | X] | MGU]    where (and (variable? Y) (occurs-check? Y X))
   [X | Y] [W | Z] MGU -> (let NewMGU (unify-loop X W MGU)
                               (unify-loop (deref Y NewMGU) 
                                           (deref Z NewMGU) 
                                           NewMGU))
    _ _ _ ->  (error "unification failure"))

(define occurs-check?
   X X -> false
   X [Y | Z] -> (and (occurs-check? X Y) (occurs-check? X Z))
   _ _ -> true)

(define deref
   [X | Y] MGU -> (map (/. Term (deref Term MGU)) [X | Y])
   X MGU -> (let Binding (assoc X MGU)
                 (if (empty? Binding) 
                     X 
                     (deref (tl Binding) MGU))))