4

私は、これらのデータ型定義をその一部として含む haskell プログラムに取り組んでいます。

data Term t (deriving Eq) where
Con     ::          a                               -> Term a
And     ::      Term Bool           -> Term Bool    -> Term Bool 
Or      ::      Term Bool           -> Term Bool    -> Term Bool 
Smaller ::      Term Int            -> Term Int     -> Term Bool
Plus    ::          Term Int        -> Term Int     -> Term Int

とデータフォーミュラtsどこ

data Formula ts where
Body   :: Term Bool                     -> Formula ()
Forall :: Show a 
     => [a] -> (Term a -> Formula as) -> Formula (a, as)

また、各 Term t を次のように評価する eval 関数:

eval :: Term t -> t
eval (Con i) =i
eval (And p q)=eval p && eval q
eval (Or p q)=eval p || eval q
eval(Smaller n m)=eval n < eval m
eval (Plus n m)    = eval n + eval m

そして、可能性のある値の置換に対して Formula が満足できるかどうかをチェックする次の関数:

satisfiable :: Formula ts -> Bool
satisfiable (Body( sth ))=eval sth
satisfiable (Forall xs f) = any (satisfiable . f . Con) xs

今、私は与えられた Formula を解く解関数を書くように頼まれました:

solutions :: Formula ts -> [ts]

また、テスト例として次の数式があり、ソリューションが次のように動作することを期待しています。

ex1 :: Formula ()
ex1 = Body (Con True)

ex2 :: Formula (Int, ())
ex2 = Forall [1..10] $ \n ->
    Body $ n `Smaller` (n `Plus` Con 1)

ex3 :: Formula (Bool, (Int, ()))
ex3 = Forall [False, True] $ \p -> 
  Forall [0..2] $ \n -> 
    Body $ p `Or` (Con 0 `Smaller` n)

ソリューション関数は次を返す必要があります。

*Solver>solutions ex1 
[()]

*Solver> solutions ex2
[(1,()),(2,()),(3,()),(4,()),(5,()),(6,()),(7,()),(8,()),(9,()),(10,())]

*Solver> solutions ex3
[(False,(1,())),(False,(2,())),(True,(0,())),(True,(1,())),(True,(2,()))]

これまでのところ、この関数の私のコードは次のとおりです。

solutions :: Formula ts -> [ts]
solutions(Body(sth))|satisfiable (Body( sth ))=[()]
        |otherwise=[]

solutions(Forall [a] f)|(satisfiable (Forall [a] f))=[(a,(helper $(f.Con) a) )]

|otherwise=[]
solutions(Forall (a:as) f)=solutions(Forall [a] f)++ solutions(Forall as f)

ヘルパー関数は次のとおりです。

helper :: Formula ts -> ts
helper (Body(sth))|satisfiable (Body( sth ))=()
helper (Forall [a] f)|(satisfiable (Forall [a] f))=(a,((helper.f.Con) a) )

最後に、ここに私の質問があります: このソリューション関数を使用すると、ex1 や ex2 のような数式を問題なく解くことができますが、ex3 を解くことができないという問題があります。 「フォーオール」の . これを行う方法について何か助けがあれば、よろしくお願いします。

4

1 に答える 1

2

solutionsForall任意の数のレイヤーを剥がすことができるように、再帰的でなければなりません:

solutions :: Formula ts -> [ts]
solutions (Body term) = [() | eval term]
solutions (Forall xs formula) = [ (x, ys) | x <- xs, ys <- solutions (formula (Con x)) ]

例:

λ» solutions ex1
[()]
λ» solutions ex2
[(1,()),(2,()),(3,()),(4,()),(5,()),(6,()),(7,()),(8,()),(9,()),(10,())]
λ» solutions ex3
[(False,(1,())),(False,(2,())),(True,(0,())),(True,(1,())),(True,(2,()))]

（余談ですが、Forall名前はかなり誤解を招くExistsので、に変更する必要があると思います。satisfiable関数（およびsolutions精神を維持するために私の関数）は、評価する変数の選択肢がある式を受け入れるためですTrue）

于 2014-11-30T16:04:23.733 に答える