使用Haskell从公式中删除重言式

Question

好吧，我把我的巨大问题集分成了小部分，我一次只尝试一个。

我正在写一个函数，它将从公式中删除重言式。基本思想是，如果在一个子句中找到了一个文字及其否定词，那表示该子句将是真实的，而不管最终的值分配给该命题变量。我的任务是创建一个函数，将删除这个，但为一个条款和映射到公式。当然，我必须在开始时删除重复项。

module Algorithm where 

import System.Random 
import Data.Maybe 
import Data.List 

type Atom = String 
type Literal = (Bool,Atom) 
type Clause = [Literal] 
type Formula = [Clause] 
type Model = [(Atom, Bool)] 
type Node = (Formula, ([Atom], Model)) 
removeTautologies :: Formula -> Formula 
removeTautologies = map tC.map head.group.sort 
    where rt ((vx, x) : (vy, y) : clauses) | x == y = rt rest 
             | otherwise = (vx, x) : rt ((vy, y) : clauses) 

现在我有问题，当我尝试给它一个式（例如（A V B）（V-A）^（B）（V（C V）A））。考虑到例如第一子句包含文字甲和-A。这意味着该条款永远是真实的，在这种情况下，它可以简化整个集合（B v C v A）。但我得到以下

Loading package old-locale-1.0.0.2 ... linking ... done. 
Loading package time-1.1.4 ... linking ... done. 
Loading package random-1.0.0.2 ... linking ... done. 
[[(True,"A"),(True,"B")*** Exception: Algorithm.hs:(165,11)-(166,83): Non-exhaustive patterns in function rt 

我该怎么办？

Answer 1

想想当你通过[(True,"A"),(True,"B"),(False,"A")]到rt功能会发生什么：

rt [(True,"A"),(True,"B"),(False,"A")] = 
    = rt ((True,"A"):(True,"B"):[(False,"A")] = 
    -- (vx,x) = (True,"A"), (vy,y) = (True,"B"), clauses = [(False, "A")] 
    = (True, "A") : rt ((True,"B"):[(False, "A")] = 
    -- (vx,x) = (True,"B"), (vy,y) = (False,"A"), clauses = [] 
    = (True, "A") : (True,"B") : rt (False, "A"):[] = 
    -- (vx,x) = (True,"B"), (vy,y) = ??? 

在你的递归调用你正在逐渐通过短名单rt。但是你没有一个方程来处理少于一个元素的列表！

你需要有这样的等式。想想rt [(False, "A")]应该返回什么。我认为正确的答案是简单地返回[(False, "A")]不变：

rt [(vx,x)] = [(vx,x)] 

现在，你考虑让空公式的可能性？
“那么，一个空的公式是没有意义的！”

好吧，想想公式（A∨∨A）。这是一个重言式。如果你删除它，你只剩下一个空的公式！所以，一个空的公式确实有意义。这是最基本的重言式。

如果我们将一个空公式传递给rt会发生什么？再次，rt []没有公式。在这种情况下，您无法删除其他任何内容。你必须回到它不动，就像以前一样：

rt [] = [] 

如果你愿意，你可以在这两个额外的方程合并成一个单一的一个：

rt ((vx, x) : (vy, y) : clauses) | -- ... blah blah 
           | -- ... blah blah 
rt x = x