问Haskell:析取范式
EN

Stack Overflow用户

提问于 2022-10-01 10:44:56

回答 1查看 169关注 0票数 1

我试图创建公式，从逻辑语言到析取范式。到目前为止我所拥有的一切；

data DNF = Var String| C Bool | Not DNF | And DNF DNF | Or DNF DNF 

toDNF :: DNF -> DNF
dnf (And (Or s1 s2) s3) = Or (And (dnf s1) (dnf s3)) (And (dnf s2) (dnf s3))
dnf (And s1 (Or s2 s3)) = Or (And (dnf s1) (dnf s2)) (And (dnf s1) (dnf s3))

dnf (And s1 s2) = And (dnf s1) (dnf s2)
dnf (Or s1 s2) = Or (dnf s1) (dnf s2)

dnf (Not (Not d)) = dnf d
dnf (Not (And s1 s2)) = Or (Not (dnf s1)) (Not (dnf s2))
dnf (Not (Or s1 s2)) = And (Not (dnf s1)) (Not (dnf s2))

dnf s = s

根据我的理解，我需要导航和，而不是向内，反之亦然，如果有人可以帮助并指出我的缺陷在哪里，这将大大有助于！

haskell

math

logic

媒体处理1元起

智能、强大、全面的多媒体数据处理服务，助您提升媒体质量、降低成本，媒体处理套餐低至1元

回答 1

Stack Overflow用户

发布于 2022-10-01 12:37:17

对于这些类型的问题，很容易陷入特殊的地狱。问题的一部分是，根据一些注释，DNF数据类型太笼统了。在其中一种情况下递归调用dnf s1之后，您实际上完全不知道您在看什么。有许多可用DNF类型表示的潜在有效的DNF“表单”，dnf s1可以是其中的任何一个。这使得很难编写直接的递归操作来处理这些子项。

类型系统可以提供帮助。考虑分离表示输入表达式的类型：

data Expr = Var String | C Bool | Not Expr | And Expr Expr | Or Expr Expr

来自表示DNF输出的限制性更强的类型：

newtype DNF  = Disj [Conj]             -- DNF is a disjuction
newtype Conj = Conj [Term]             -- of conjunctions
data    Term = JustT VarT | NotT VarT  -- of possibly negated
newtype VarT = VarT String             -- variables

现在，您可以将问题简化为Expr中每个构造函数的一种模式。(不过，正如我们下面将看到的那样，Not的处理方式比其他的要好。)

dnf :: Expr -> DNF
dnf (And s1 s2) = dnfAnd (dnf s1) (dnf s2)
dnf (Or s1 s2)  = dnfOr (dnf s1) (dnf s2)
dnf (Not s1)    = dnfNot (dnf s1)
dnf (C b)       = dnfC b
dnf (Var x)     = dnfVar x

当您编写这些帮助函数之一(比如dnfOr )时，您现在确切地知道了这两个输入是什么样子，以及输出应该是什么样子，这使得其中一些非常琐碎：

dnfOr (Disj conjs1) (Disj conjs2) = Disj (conjs1 ++ conjs2)

这个框架可以提供很高的信心，相信您的最终解决方案将是正确的，并且不会“错过”任何情况，当您使用原始表达式数据类型做所有事情时，这是很难做到的。

如果您需要更多的帮助，下面是一个完整的解决方案。

扰流器跟随

。

上面的dnfOr函数很简单。一旦您理解了受限的DNF表示，其他的一些也是非常琐碎的：

例如，VarT的情况是该变量的单例连接的单例分离：

dnfVar x = Disj [Conj [JustT (VarT x)]]

对于dnfC，我们可以从DNF中消除布尔常量，方法是使用这样的约定：False是空分离，而True是包含空连接的单例析取。多亏了数学，这些不仅仅是“约定”。它们是可靠和一致的DNF表示，将与递归中的其他术语很好地配合：

dnfC False = Disj []
dnfC True = Disj [Conj []]

现在我们到了“难”的地方。dnfAnd遵循分布规律，导致了新的两两连词的分离。经过一段时间的思考，我把它归结为一条线：

dnfAnd (Disj conjs1) (Disj conjs2) = Disj [c1 ++ c2 | c1 <- conjs1, c2 <- conjs2]

最难的是dnfNot。原来你必须写这样的东西，我不会费心解释的：

dnfNot (Disj conjs) = foldr dnfAnd (dnfC True) [conjNot c | c <- conjs]
  where
    conjNot (Conj ts) = Disj [Conj [termNot t] | t <- ts]
    termNot (JustT v) = NotT v
    termNot (NotT v) = JustT v

问题是，Not是使用原始Expr类型最容易解决的一个操作，因为它很容易“向下推”Nots，直到它们都在变量旁边：

notExpr (And e1 e2) = (Or (notExpr e1) (notExpr e2))
notExpr (Or e1 e2) = (And (notExpr e1) (notExpr e2))
notExpr (Not e1) = e1
notExpr (C b) = C (not b)
notExpr (Var e1) = Not (Var e1)

因此，与其通过首先获得Not的子项DNF，然后否定它，不如将其转换为Expr，然后再将其更改为DNF：

dnf (Not s1) = dnf (notExpr s1)

请注意，此递归将导致无限循环，除非我们添加一个基本情况来处理notExpr在其输出Exprs中生成的一种类型的Expr表达式：

-- handle the base case produced by `notExpr`
dnf (Not (Var x)) = Disj [Conj [NotT (VarT x)]]
-- every other occurrence of `Not` gets processed by `notExpr`
dnf (Not s)       = dnf (notExpr s)

完整的代码如下。请注意，我的解决方案在特定情况下会产生不太理想的结果(请参阅main中的最后一个示例)。作为练习，您可能希望尝试修复这个问题，并考虑如何处理从最终解决方案中删除冗余项的更普遍的问题。

import Data.List

data Expr = Var String | C Bool | Not Expr | And Expr Expr | Or Expr Expr
  deriving (Show)
infixl 3 `And`
infixl 2 `Or`

newtype DNF  = Disj [Conj] deriving (Show)  -- DNF is a disjuction
newtype Conj = Conj [Term] deriving (Show)  -- of conjunctions
data    Term = JustT VarT
             | NotT VarT   deriving (Show)  -- of possibly negated
newtype VarT = VarT String deriving (Show)  -- variables

prettyDNF :: DNF -> String
prettyDNF (Disj conjs)
  = [parens (map prettyTerm ts `sepBy` "∧") | Conj ts <- conjs] `sepBy` "∨"
  where prettyTerm (JustT (VarT x)) = x
        prettyTerm (NotT (VarT x)) = "¬" ++ x

        xs `sepBy` sep = intercalate sep xs
        parens str = "(" ++ str ++ ")"

dnf :: Expr -> DNF

dnf (And s1 s2) = dnfAnd (dnf s1) (dnf s2)
  where
    dnfAnd :: DNF -> DNF -> DNF
    dnfAnd (Disj conjs1) (Disj conjs2) = Disj [Conj (c1 ++ c2) | Conj c1 <- conjs1, Conj c2 <- conjs2]

dnf (Or s1 s2)  = dnfOr (dnf s1) (dnf s2)
  where
    dnfOr :: DNF -> DNF -> DNF
    dnfOr (Disj d1) (Disj d2) = Disj (d1 ++ d2)

dnf (Not (Var x)) = Disj [Conj [NotT (VarT x)]]
dnf (Not s)       = dnf (notExpr s)
  where
    notExpr :: Expr -> Expr
    notExpr (And e1 e2) = (Or (notExpr e1) (notExpr e2))
    notExpr (Or e1 e2) = (And (notExpr e1) (notExpr e2))
    notExpr (Not e1) = e1
    notExpr (C b) = C (not b)
    notExpr (Var e1) = Not (Var e1)

dnf (C b)       = dnfC b
  where
    dnfC :: Bool -> DNF
    dnfC False = Disj []
    dnfC True = Disj [Conj []]

dnf (Var x)     = dnfVar x
  where
    dnfVar :: String -> DNF
    dnfVar x = Disj [Conj [JustT (VarT x)]]

main = mapM_ (putStrLn . prettyDNF . dnf)
  [ (Var "a" `Or` Var "b") `And` (Var "c" `Or` Var "d")
  , Not ((Var "a" `Or` Var "b") `And` (Var "c" `Or` Var "d"))
  , Not (Var "a" `And` Var "b") `Or` (Var "c" `And` Var "d")
  -- This last case prints (a)∨() which is technically correct
  -- but can be further simplified to (), the singleton
  -- disjunction of an empty conjunction representing "true"
  , Var "a" `Or` C True
  ]