Haskell中列表推导|符号用法及n选m逻辑命题生成问题

1. 「|」标记的含义 #

你在代码中看到的|是Haskell列表推导式的语法分隔符，不属于函数或者运算符，所以在Hoogle（查询函数/类型的工具）上搜不到。它的作用是分隔列表推导的「结果表达式」和后面的「生成器、过滤条件」部分。

2. 现有代码的核心问题 #

你当前的实现逻辑和需求完全不匹配，问题集中在3个点：

• 合取子句构造错误：你要求每个合取子句覆盖所有n个命题（选中的取肯定、未选中的取否定），但现有代码生成的每个Conj仅包含2个文字：一个选中下标的肯定命题、一个未选中下标的否定命题，其余n-2个命题完全没有出现在子句中，逻辑不成立。
• 下标范围错误：[0 .. n]生成的是n+1个下标，对应n+1个命题，如果你要处理n个命题，下标范围应为[0 .. n-1]。
• 列表推导逻辑错误：你需要的是select里的每个m元下标组合对应一个合取子句，现有代码对每个组合会生成m*(n-m)个合取子句，数量和逻辑都不符合需求。

3. 修正后的代码 #

genXorM :: Int -> Int -> Form 
genXorM n m = Disj [ Conj (map positive z ++ map negative rest) | z <- select, let rest = [0 .. n-1] \\ z ]
  where
    select = combinations m [0 .. n-1]
    positive x = PrpF $ P x
    negative x = Neg $ PrpF $ P x

修正后的逻辑符合要求：

• 对每个m元下标组合z，先拿到所有未选中的下标rest
• 选中的下标全部生成肯定形式的命题，未选中的全部生成否定形式的命题
• 所有命题合取为一个子句，所有子句再析取，最终的语句就等价于「n个命题中恰好m个为真」

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