2

我正在尝试创建一个将命题更改为析取范式的函数。

它将通过读取 Valuation 列表来做到这一点:

type Valuation = [(Variable, Bool)] -- Valuation of variables to truth values 

并使用这些:

findBool :: (Variable, Bool)->Bool
findBool (_,x) = x

findVar :: (Variable, Bool)->Variable
findVar (x,_) = x

命题也是:

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)

我认为到目前为止我所拥有的非常可靠,但我不知道该怎么处理空箱子。这是我到目前为止所拥有的:

minterm :: Valuation -> Prop
minterm [] = ?
minterm (x:xs) = if (findBool x) then (And (findVar x) (minterm xs)) else (And (Not(findVar x) (minterm xs)) 

我的目标是:minterm [("p",True),("q",False)]返回:And (Var "p") (Not (Var "q"))

编辑: Falsum 无效,但如果它没有返回任何东西,我会更喜欢。无论如何我可以排除它会被退回的情况,所以我可以得到这样的东西:

minterm [("p",True),("q",False)]==And (Var "p") (Not (Var "q"))

4

3 回答 3

2

什么都不返回的标准方法是返回Nothing

minterm :: Valuation -> Maybe Prop
minterm []     = Nothing
minterm (x:xs) =
    Just $ case minterm xs of
             Nothing -> y
             Just mt -> And y mt
  where
    y = if (findBool x)
            then findVar x
            else Not $ findVar x

请注意,现在您的顶级类型签名将反映这种失败的概念。

于 2013-11-14T12:54:40.320 回答
1

根据您的编辑,您是否可能只想对结局进行特殊处理以进行整理?

minterm :: Valuation -> Prop
minterm [] = Not Falsum
minterm [x] = oneTerm x
minterm (x : xs) = And (oneTerm x) (minterm xs)

oneTerm (x, True) = Var x
oneTerm (x, False) = Not (Var x)
于 2013-11-14T11:26:15.307 回答
1

您可以更改minterm函数以返回子句列表而不是术语:

minterm :: Valuation -> [Prop]
minterm [] = []
minterm (x:xs) = if (findBool x) then findVar x : minterm xs else Not (findVar x)  : minterm xs

然后编写另一个函数将其转换为 Prop:

and :: [Prop] -> Prop
and [] = Not Falsum
and xs = foldr1 And xs
于 2013-11-14T14:03:50.817 回答