Haskell:析取范式
我试图创建公式，从逻辑语言到析取范式。到目前为止我所拥有的一切；
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根据我的理解，我需要导航和，而不是向内，反之亦然，如果有人可以帮助并指出我的缺陷在哪里，这将大大有助于！
回答 1
Stack Overflow用户
发布于 2022-10-01 20: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
]https://stackoverflow.com/questions/73920914
复制相似问题
腾讯云开发者
