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

2023年7月26日 241次阅读

我正在开发一个包含这些数据类型定义的
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)

还有一个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.意味着我的函数不适用于包含嵌套的公式“Forall”.任何有关我如何做到这一点的帮助,将不胜感激,提前谢谢.

最佳答案 解决方案必须是递归的,以便它可以剥离任意数量的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,因为你可以满足的功能(以及我的解决方案功能,保持精神)接受公式,其中有一些选择要评估的变量为True)

点赞