On 18-Aug-2005, Keean Schupke
I was wondering if anyone has any comments on my implementation of unify? For example can the algorithm be simplified from my nieve attempt? Most importantly is it correct?
type Subst = [(Vname,Term)] data Term = Func Fname [Term] | Var Vname deriving (Eq,Show) type Fname = String data Vname = Name String | Auto Integer deriving (Eq,Show)
unify :: Subst -> (Term,Term) -> [Subst] unify s (t,u) | t == u = [s]
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. -- Fergus J. Henderson | "I have always known that the pursuit Galois Connections, Inc. | of excellence is a lethal habit" Phone: +1 503 626 6616 | -- the last words of T. S. Garp.