[Haskell-cafe] embedding prolog in haskell.

[Fergus Henderson]

On 18-Aug-2005, Keean Schupke <k.schupke at imperial.ac.uk> wrote:
> 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.