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.