ハスケルを使って式からトートロジを削除する

Question

私は大きな問題を小さな部分に分けて、一度に1つずつしようとしています。

私は、式からトートロジを削除する関数を書いています。基本的な考え方は、リテラルとその否定が見つかった場合、その値が最終的に私のアプローチは、これを削除する関数を作成することですが、節のためにそれを数式にマップします。もちろん、私は最初に重複を削除する必要があります。

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) 

私はそれを（例えば（V BはVの-A）^（BのV CのVのA））の式を与えることをしようとすると、今、私は問題を抱えている。その一例を考えると最初の句は、リテラル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 

どうすればよいですか？あなたは徐々に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) = ??? 

：

Answer 1

あなたはrt関数に[(True,"A"),(True,"B"),(False,"A")]を渡すときに何が起こるか考えてみてください。しかし、要素が1つ未満のリストを処理する式はありません。

このような式が必要です。 rt [(False, "A")]が何を返すべきか考えてみてください。私は、正しい答えは単純[(False, "A")]はそのまま返すことだろうと思う：

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

さて、あなたは空の式を有する可能性を検討していますか？
"空ではない式がない！"

さて、式（A∨¬A）について考えてみましょう。それは同音異義語です。それを削除すると、空の数式が残されます。したがって、空の数式は意味をなさない。それは最も基本的な同音異義語です。

空の数式をrtに渡すとどうなりますか？ここでも、rt []の式はありません。この場合、他のものを削除することはできません。あなただけの前のように、そのままそれを返す必要があります：

rt [] = [] 

したい場合は、単一のものにこれら2つの追加の式を組み合わせることができます。

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