Thanks for that, altough I have completely rewritten it! Here's the new implementation: unify :: Subst -> (Term,Term) -> [Subst] unify sigma (s,t) = let s' = if isVar s then subst s sigma else s t' = if isVar t then subst t sigma else t in if isVar s' && s'==t' then [sigma] else if isFunc s' && isFunc t' then if fname s' == fname t' && arity s' == arity t' then unify' sigma (terms s') (terms t') else [] else if not (isVar s) then unify sigma (t',s') else [s' ~> t' : sigma] unify' :: Subst -> [Term] -> [Term] -> [Subst] unify' s (t0:ts) (u0:us) = case unify s (t0,u0) of s@(_:_) -> unify' (concat s) ts us _ -> [] unify' s [] [] = [s] unify' _ _ _ = [] Once again, thoughts or improvements greatly appreciated... Regards, Keean. Fergus Henderson wrote:
You should delete the line above. It's not needed and could cause serious efficiency problems. With that line present, unifying two lists of length N which differ only in the last element would take time proportional to N squared, but without it, the time should be linear in N.
unify s (Var x,t) = [(x,t):s] -- no occurs check unify s (t,Var x) = [(x,t):s] -- no occurs check
These are not right; you need to look up the variable x in the substitution s, and if it is already bound, then you need to unify what it is bound to with the term t.