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 where

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

还有一个 eval 函数，它将每个 Term t 评估为：

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

以下检查公式是否可满足任何可能的值替换的函数：

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

现在，我被要求编写一个求解给定公式的求解函数：

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

solutions必须是递归的，以便它可以剥离任意数量的Forall层：

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 回答