haskell - 如何解决haskell中的逻辑公式？

Question

我正在开发一个包含这些数据类型定义的 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 。这意味着我的函数不适用于包含嵌套的公式“福尔”。任何帮助我如何做到这一点，将不胜感激，提前致谢。

Answer 1

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 )