[Haskell-cafe] embedding prolog in haskell.
Keean Schupke
k.schupke at imperial.ac.uk
Thu Aug 18 09:14:22 EDT 2005
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.
More information about the Haskell-Cafe
mailing list