Prolog User Golfing System

HaskellでPrologっぽいものを作ってみた。正しいPrologの挙動が分からないのでアレだけども

{-# OPTIONS -fglasgow-exts #-}
{-# OPTIONS -fno-monomorphism-restriction #-}
module Prolog where
import List(nub)
import Monad(liftM)
import Control.Monad.State
data Term = LVar String
          | Atom String
          | IntT Integer
          | Nil
          | Cons Term Term deriving (Eq,Show)

data Predicate = Eq Term Term
               | And Predicate Predicate
               | Or Predicate Predicate deriving Show

type Subst = [(String , Term)]

--Substの適用
subst :: Subst -> Term -> Term
subst [] t = t
subst (a:as) t = subst as (subst' a t)
 where
  subst' (n , t) (LVar v) = if (n==v) then t else (LVar v)
  subst' s (Cons x y)  = Cons (subst' s x) (subst' s y)
  subst' s x = x

--Substの合成
substC :: Subst -> Subst -> Maybe Subst
substC theta1 theta2 = substR (theta1++theta2)
 where
  substR theta = substR' [] (Just theta)
  substR' _ Nothing = 
   fail "failed to compose"
  substR' prev (Just theta) = 
   if (prev==theta) then (return theta) else (substR' theta $ next theta)
  next theta = 
   let n=[(n,subst theta t)|(n,t)<-theta] in 
    if (contradict n) then Nothing else (Just n)
  contradict theta = 
   all (\x->length x/=1) (nub[map snd $ filter (\(v,t)->v==v') theta|(v',t')<-theta])


occurs :: String -> Term -> Bool
occurs s (LVar n) = (s==n)
occurs s (Cons t1 t2) = (occurs s t1) || (occurs s t2)
occurs _ _ = False

unify ::  Term -> Term -> Maybe Subst
unify t1 t2 = unifyT [] t1 t2

unifyT :: Subst -> Term -> Term -> Maybe Subst
unifyT theta (LVar v1) (LVar v2) = 
 if (v1==v2) then (return theta) else (fail "can't unify")
unifyT theta (LVar v) t = 
 if (occurs v t) then (fail "can't unify") else (substC [(v,t)] theta)
unifyT theta t (LVar v) = 
 if (occurs v t) then (fail "can't unify") else (substC [(v,t)] theta)
unifyT theta (Cons t1 t2) (Cons t1' t2') =
 do eta<-unifyT theta (subst theta t1) (subst theta t1')
    unifyT eta t2 t2'
unifyT theta x y = 
 if (x==y) then (return theta) else (fail "can't unify")


solve' ::  Subst -> Predicate -> Maybe [Subst]
solve' init (Eq p q) = 
 do a<-unify (subst init p) (subst init q)
    ret<-substC init a
    return [ret]
solve' init (Or p q) =
 case (solve' init p) of
  Just ps -> case (solve' init q) of {Just qs->return (ps++qs);Nothing->return ps}
  Nothing -> solve' init q
solve' init (And p q) = 
 case (solve' init p) of
  Nothing -> Nothing
  Just ps -> let tmp = (map (\x->solve' x q) ps) in
   if (all (Nothing==) tmp) then Nothing else return $ concat[x|Just x<-tmp]


solve :: (Monad m)=> Predicate -> m [Subst]
solve p = case (solve' [] p) of{Just x->return x;Nothing->fail "failed"}

Termの方は、整数とか、シンボルとか、リストを扱える。で、Predicate。例えば、

like(john , taro).
like(masaki , abeTakakazu).

は

like :: Term -> Term -> Predicate
like a b = (Or (And (Eq a (Atom "John")) (Eq b (Atom "taro")))
                 (And (Eq a (Atom "masaki")) (Eq b (Atom "abeTakakazu"))))

とかいう感じの式になる。で、

*Main> solve $ like (LVar "x") (LVar "y")
[[("x",Atom "John"),("y",Atom "taro")],
 [("x",Atom "masaki"),("y",Atom "abeTakakazu")]]

とか、そんな感じ。

リストのappendとかは、

append :: Term -> Term -> Term -> Predicate
append ps qs rs = (Or (And (Eq ps Nil) 
                           (Eq qs rs))
                      (And (And (Eq ps (Cons (LVar "X") (LVar "Xs"))) 
                                (Eq rs (Cons (LVar "X") (LVar "Ys"))))
                            (append (LVar "Xs") qs (LVar "Ys"))))

とかだと多分まずい。っつーのは、appendを実際に評価したとき、何もしないと、appendの中にあるappendが再帰的にどんどん展開されて、無限に長い論理式ができるけど、そんときに、(LVar "X")とか(LVar "Ys")が違うスコープで何回もでてきて、衝突するから。なんで、gensymみたいな関数で、毎回、違う名前を生成しないといけない。とりあえず、お手軽に解決。

gensym :: State Int Term
gensym = do{n<-get;put $ n+1;return $ LVar(show n)}

app :: Term -> Term -> Term -> State Int Predicate
app ps qs rs = 
 do{x<-gensym;
    xs<-gensym;
    ys<-gensym;
    n<-app xs qs ys;
    return  (Or (And (Eq ps Nil) (Eq qs rs)) 
                (And (And (Eq ps (Cons x xs)) (Eq rs (Cons x ys))) n))}

で、

*Main> solve $ evalState (app (LVar "x") (LVar "y") (Cons (IntT 3) (Cons (IntT 4) Nil))) 0
[[("x",Nil),("y",Cons (IntT 3) (Cons (IntT 4) Nil))],[("x",Cons (IntT 3) Nil),("3",Cons (IntT 4) Nil),("0",IntT 3),("1",Nil),("y",Cons (IntT 4) Nil)],[("x",Cons (IntT 3) (Cons (IntT 4) Nil)),("3",Cons (IntT 4) Nil),("0",IntT 3),("1",Cons (IntT 4) Nil),("7",Nil),("4",IntT 4),("5",Nil),("y",Nil)]]

とか。一応正しく答えがでてるような気がする。あと、
solve (Eq (IntT 4) (IntT 3))
はfailして、
solve (Eq (IntT 3) (IntT 3))
は、[]が返ってくる。

いくつか、問題があって、一つは異なる論理変数XとYの単一化を無条件で失敗にしている点。これは、色々ダメな気がするけど、どうすれば綺麗に解決できるのか分からなかった。もう一点は、(And p q)解くときに、まずpを解いて、次にqを解いてるけど、qがfailする場合にはfailとしちゃっていいんだけど、pの計算が終了しない場合、全体として計算が停止しなくなる。要するに、pとqの計算は、本来並列に実行されるべきなのに、逐次計算になってるのがまずい。と思ったんだけど、よく考えると、Prologも前から順に計算していくなぁ

SWI-Prologで挙動確認してみると

hoge(X,Y) :- X=Y,Y=X,X=3.

は正しい答えを求めてくれる。appendの方は

append(X,Y,Z) :- X=[],Y=Z.
append(X,Y,Z) :- append(X1,Y,Z1),X=[W|X1],Z=[W|Z1].

と

append(X,Y,Z) :- X=[],Y=Z.
append(X,Y,Z) :- X=[W|X1],append(X1,Y,Z1),Z=[W|Z1].

は理屈上は同じ振る舞いをすべきだという気がするけど、前者で
?- append([],X,[1,2,3,4])
とかやると、解を一個求めて、更に計算を続行しようとすると、処理が戻ってこない。まあ、実行順序不定にしてしまうと
?- print(abe),print(takakazu)
とかも、出力がおかしくなるわけだけど、なんだかなぁ