Haskell实现逻辑公式转析取范式（DNF）的代码问题求助

你编写的Haskell代码存在以下几处关键缺陷：

1. 函数名不匹配 #

代码中定义的函数类型是toDNF :: DNF -> DNF，但实现时用的函数名是dnf，这会直接导致编译错误——Haskell无法识别未定义的dnf函数。

2. Not操作的处理不完整 #

当Not作用于Var或C时，代码直接返回原表达式，虽然语法上合法，但缺少对常量的简化：比如Not (C True)应简化为C False，Not (C False)应简化为C True。

3. 分配律应用后未扁平化Or结构 #

DNF的定义要求是合取式的析取，不允许嵌套的Or结构。当前代码在应用分配律后，会产生嵌套的Or，比如处理And (Or a (Or b c)) d时，最终会得到Or (And a d) (Or (And b d) (And c d))，这不符合DNF的规范，需要将嵌套的Or展开为扁平结构。

4. 常量（C Bool）的简化规则缺失 #

逻辑常量的简化是DNF转换的重要环节，当前代码完全没有处理这类场景：

• And (C True) s 应简化为 toDNF s
• And (C False) s 应简化为 C False
• Or (C True) s 应简化为 C True
• Or (C False) s 应简化为 toDNF s
  这些缺失会导致结果中保留大量不必要的常量，无法得到最简DNF。

5. 合取式的冗余/矛盾项未处理 #

对于合取式中的重复变量或矛盾项，没有做简化：

• And (Var "x") (Var "x") 应简化为 Var "x"
• And (Var "x") (Not (Var "x")) 应简化为 C False
  这类简化能大幅减少结果的冗余度，当前代码完全没覆盖。

修正示例片段 #

针对部分缺陷，给出修正后的代码片段参考：

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

toDNF :: DNF -> DNF
-- 常量简化
toDNF (C b) = C b
toDNF (Not (C b)) = C (not b)
-- 双重否定消除
toDNF (Not (Not d)) = toDNF d
-- 德摩根定律
toDNF (Not (And s1 s2)) = toDNF $ Or (Not (toDNF s1)) (Not (toDNF s2))
toDNF (Not (Or s1 s2)) = toDNF $ And (Not (toDNF s1)) (Not (toDNF s2))
toDNF (Not v@(Var _)) = Not v
-- 分配律：And对Or分配 + 常量简化
toDNF (And s1 s2) = let d1 = toDNF s1; d2 = toDNF s2 in
  case (d1, d2) of
    (Or a b, c) -> toDNF $ Or (And a c) (And b c)
    (a, Or b c) -> toDNF $ Or (And a b) (And a c)
    (C True, c) -> c
    (c, C True) -> c
    (C False, _) -> C False
    (_, C False) -> C False
    _ -> And d1 d2
-- 扁平化Or结构 + 常量简化 + 去重
toDNF (Or s1 s2) = let d1 = toDNF s1; d2 = toDNF s2 in
  case (d1, d2) of
    (Or a b, c) -> toDNF $ Or a (Or b c)
    (a, Or b c) -> toDNF $ Or (Or a b) c
    (C True, _) -> C True
    (_, C True) -> C True
    (C False, c) -> c
    (c, C False) -> c
    _ -> if d1 == d2 then d1 else Or d1 d2
-- 基本情况
toDNF v@(Var _) = v

内容的提问来源于stack exchange，提问作者Someone21345