하스켈을 사용하여 수식에서 동어 반복을 제거합니다.

Question

그래, 작은 부분으로 구성된 거대한 문제를 나누어서 한 번에 하나씩 처리하려고합니다.

수식에서 동어 반복을 제거하는 함수를 작성하고 있습니다. 기본 개념은 절에서 리터럴과 부정이 발견되면 마침내 값에 관계없이 절이 true라는 것을 의미합니다 우리의 방법은 절을 제거하고 공식에 매핑하는 함수를 만드는 것입니다. 물론, 나는 처음부터 중복을 제거해야한다. I (예 : (A 브이 B 브이 -A)^(B 브이 C 브이 A)에 대해) 한번 식을 수득 할 때

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) 

은 이제 문제가있다. 즉, 예를 고려할 때 상기 제 1 절 리터럴 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

당신이 rt 기능에 [(True,"A"),(True,"B"),(False,"A")]를 통과 할 때 일어나는 일에 대해 생각 : 당신의 재귀 호출에

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)] 

지금, 당신은 빈 공식을 가진 가능성을 고려하고있다?
"Nah, 비어있는 식은 말이 안됩니다!"

글쎄, 수식 (A ∨ ¬A)에 대해 생각해보십시오. 그것은 동어 반복이다. 제거하면 빈 수식이 남습니다! 그래서, 빈 수식은 이해가됩니다. 그것은 가장 기본적인 동음 해소법입니다.

빈 수식을 rt으로 전달하면 어떻게됩니까? 다시 말하면, rt []에 대한 방정식은 없습니다. 이 경우 다른 것을 제거 할 수 없습니다. 당신은 예전처럼, 그것은 그대로 반환해야합니다 :

rt [] = [] 

당신이 하나 하나에이 두 여분의 방정식을 결합 할 수 있습니다 원하는 경우 :

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