Re: [Haskell-cafe] embedding prolog in haskell.
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
Re: [Haskell-cafe] embedding prolog in haskell.
On 18-Aug-2005, Keean Schupke [EMAIL PROTECTED] 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. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] embedding prolog in haskell.
Okay, I have found the missing definition (code was split by page break), and found the type error: type Subst = [(Var,Term)] should be: type Subst = [(Vname,Term)] And have written a simple implementation of unify from a description of the algorithm. 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] unify s (Var x,t) = [(x,t):s] -- no occurs check unify s (t,Var x) = [(x,t):s] -- no occurs check unify s (Func f ts,Func g us) | f == g = unify' s ts us | otherwise = [] unify' :: Subst - [Term] - [Term] - [Subst] unify' s [] [] = [s] unify' s (t0:ts) (u0:us) = case unify s (t0,u0) of s@(_:_) - unify' (concat s) ts us _ - [] Keean. Keean Schupke wrote: Does anyone know if the source code for the embedded prolog (by Silvija Seres Michael Spivey) is available for download from anywhere? I have read the paper and found some of the types are wrong, some critical definitions are missing, and the definition of unify is missing. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] embedding prolog in haskell.
Keean Schupke wrote: implementation of unify? For example can the algorithm be simplified from my nieve attempt? Most importantly is it correct? It will not be correct without occurs check. You may also get different terms for the same variable in your substitution list. The simplest form of unification does not take a substitution as input and uses functions to compose two substitutions and to apply a substitution to a term. unify :: Subst - (Term,Term) - [Subst] Do you ever get real lists? The result type Maybe Subst is more appropriate. unify' s [] [] = [s] unify' s (t0:ts) (u0:us) = case unify s (t0,u0) of s@(_:_) - unify' (concat s) ts us _ - [] input lists of different lengths should not cause a runtime error but only a unification failure (indicated by Nothing or [] in your case.) HTH Christian Here's a part of my version: unify' (t0:ts) (u0:us) = do s1 - unify (t0,u0) s2 - unify' (map (applySubst s1) ts) (map (applySubst s1) us) return (composeSubst s1 s2) ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] embedding prolog in haskell.
Christian Maeder wrote: Keean Schupke wrote: implementation of unify? For example can the algorithm be simplified from my nieve attempt? Most importantly is it correct? It will not be correct without occurs check. You may also get different terms for the same variable in your substitution list. Prolog does not use an occurs check... and this is embedding prolog. However I accept this point, thats why there was the comment about no occurs check in the code. I actually want to cope with recursive definitions as Prolog does, so the solution to: X = f(X) should be: f(f(f(f(... which is an infinite recursion. The simplest form of unification does not take a substitution as input and uses functions to compose two substitutions and to apply a substitution to a term. unify :: Subst - (Term,Term) - [Subst] This signature came from the paper... The input subst is an accumulator and it would normally be Id when calling - so there is effectively no input substitution. Do you ever get real lists? The result type Maybe Subst is more appropriate. No, I dont think the algorithm gives real lists, Maybe would be better, although I think I will get it working before playing with changing the rest of the code. Is it possible to ever have more than one meaningful answer from unification? unify' s [] [] = [s] unify' s (t0:ts) (u0:us) = case unify s (t0,u0) of s@(_:_) - unify' (concat s) ts us _ - [] input lists of different lengths should not cause a runtime error but only a unification failure (indicated by Nothing or [] in your case.) Aha, a genuine bug... thanks! HTH Christian Here's a part of my version: unify' (t0:ts) (u0:us) = do s1 - unify (t0,u0) s2 - unify' (map (applySubst s1) ts) (map (applySubst s1) us) return (composeSubst s1 s2) I am now using: 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' _ _ _ = [] Regards, Keean. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] embedding prolog in haskell.
Does anyone know if the source code for the embedded prolog (by Silvija Seres Michael Spivey) is available for download from anywhere? I have read the paper and found some of the types are wrong, some critical definitions are missing, and the definition of unify is missing. Regards, Keean. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
