没有线索的 Haskell 初学者

Question

我花了一段时间才弄清楚这个问题在寻找什么。我只需要返回那些对 True 进行整体评估的命题。我们的例子是 And p (Or q (Not q)) 并且我知道 p 必须是 True 并且 q 可以是 True 或 False。为了实现我们的目标，我们已经开始使用一些函数。

type Variable = String
type Valuation = [(Variable, Bool)]

data Prop = Falsum         -- a contradiction, or
          | Var Variable   -- a variable, or
          | Not Prop       -- a negation of a formula, or
          | Or  Prop Prop  -- a disjunction of two formulae, or
          | And Prop Prop  -- a conjunction of two formulae, or
          | Imp Prop Prop  -- a conditional of two formulae.
            deriving (Eq, Show)

example = And p (Or q (Not q))

vars :: Prop -> [Variable]
vars = nub . vars'
    where
      vars' Falsum    = []
      vars' (Var v)   = [v]
      vars' (Not f)   = vars' f
      vars' (Or  f g) = vars' f ++ vars' g
      vars' (And f g) = vars' f ++ vars' g 
      vars' (Imp f g) = vars' f ++ vars' g 

eval :: Valuation -> Prop -> Bool
eval val Falsum    = False
eval val (Var v)   = case (lookup v val) of
                       Nothing -> error ("Unbound variable: " ++ v)
                       Just t  -> t 
eval val (Not f)   = not (eval val f)
eval val (Or  f g) = (eval val f) || (eval val g)
eval val (And f g) = (eval val f) && (eval val g)
eval val (Imp f g) = eval val (Or (Not f) g)

valuations :: [Variable] -> [Valuation]
valuations []     = [[]]
valuations (v:vs) = map ((v,True):) ds ++ map ((v,False):) ds 
    where ds = valuations vs

我现在必须编写一个模型函数，并且我发现 typeline 必须是

models :: Prop -> [Valuations]

作为我的示例，必须返回评估为 True 的评估列表，即： 模型示例 == [[("p",True)("q",True)],[("p",True)("q",False)]]

我知道 vars 返回没有重复的变量列表，在本例中为 ["p","q"]，并且将 vars 的结果传递给评估会生成将 True 和 False 应用于“p”和“q”。到目前为止，我只能使用 evals 函数获得该列表的第一个输出来评估。这是我的代码：

models :: Prop -> Bool
models form = eval v form where (v:vs) = valuations (vars form)

我尝试更改代码以评估 vs 的其余部分，但我不断收到错误消息：

Couldn't match expected type '[Bool]' with actual type 'Bool'

这是我修改后的代码：

models :: Prop -> [Bool]
models form = eval v form : eval vs form where (v:vs) = valuations (vars form)

理想情况下，我相信我想丢弃评估结果，而不是将它们保存在列表中，并且只返回那些评估为 True 的估值。我只是被困在如何递归地评估其余的 vs.

我相信，一旦我可以使用 evals 函数评估列表中的所有元素，我就可以使用某种形式的等式分配将评估为 True 的元素添加，例如：

where finalList == True = 

唉，这甚至看起来都不正确。

对我的逻辑的任何帮助都会有所帮助。哦，如果我能解释一下我如何递归评估列表的其余部分，我们将不胜感激。

Answer 1

我假设你想要models :: Prop -> [Valuation]，就像你开始写的那样。模型将返回满足命题的每个Valuation。从接近你所拥有的东西开始

models form = valuations (vars form)

让我们走到了一半；它具有正确的类型，Prop -> [Valuation]。这只是列出了form 中变量的每个Valuation。我们想要的是只有那些满足命题的结果。这些可以由您的eval 函数确定。

models :: Prop -> [Valuation]
models form = filter satisfies (valuations (vars form))
    where satisfies val = eval val form 

要运行它，我们需要修复您的示例以便它编译，并且可能添加几个我自己的示例：

example = And (Var "p") (Or (Var "q") (Not (Var "q")))

main = do
    print $ models Falsum
    print $ models example
    print $ models $ And (Var "p") (Not (Var "p"))
    print $ models $ Or (Var "p") (Not (Var "p"))

这个输出

[]
[[("p",True),("q",True)],[("p",True),("q",False)]]
[]
[[("p",True)],[("p",False)]]

现在，我们可能还需要一个函数来检查是否存在满足命题的Valuation。这将接受一个命题并返回一个布尔值。

satisfiable :: Prop -> Bool

我们可以很容易地把这个写成models

satisfiable :: Prop -> Bool
satisfiable = not . null . models

同样的四个例子

main = do
    print $ satisfiable Falsum
    print $ satisfiable example
    print $ satisfiable $ And (Var "p") (Not (Var "p"))
    print $ satisfiable $ Or (Var "p") (Not (Var "p"))

这个输出

False
True
False
True