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.
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
