[Haskell-cafe] embedding prolog in haskell.

[Keean Schupke]

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.
>
>  
>