Proposition normalization.md

isNorm.hs

data Proposition = Var String
                  | F
                  | T
                  | Not Proposition
                  | Proposition :|: Proposition
                  | Proposition :&: Proposition
                  deriving (Eq, Ord, Show)
                  
isNorm :: Proposition -> Bool
isNorm p = p == norm p

norm :: Proposition -> Proposition
norm (Not F) = T
norm (Not T) = F
norm (Not (Var p)) = Not (Var p)
norm (Not (Not p)) = p
norm (Not (p :|: q)) = norm (Not p) :&: norm (Not q)
norm (Not (p :&: q)) = norm (Not p) :|: norm (Not q)
norm ((Not p) :&: (Not q)) = norm (Not (p :|: q))
norm ((Not p) :|: (Not q)) = norm (Not (p :&: q))
norm p = p

main =  do
        print $ isNorm (Var "p" :&: Not (Var "q")) -- True
        print $ isNorm (Not (Var "p" :|: Var "q")) -- False
        print $ isNorm (Not (Not (Var "p")) :|: Not T) -- False
        print $ isNorm (Not (Var "p" :&: Not (Var "q"))) -- False

norm.hs

data Proposition = Var String
                  | F
                  | T
                  | Not Proposition
                  | Proposition :|: Proposition
                  | Proposition :&: Proposition
                  deriving (Eq, Ord, Show)

norm :: Proposition -> Proposition
norm (Not F) = T
norm (Not T) = F
norm (Not (Var p)) = Not (Var p)
norm (Not (Not p)) = p
norm (Not (p :|: q)) = norm (Not p) :&: norm (Not q)
norm (Not (p :&: q)) = norm (Not p) :|: norm (Not q)
norm ((Not p) :&: (Not q)) = norm (Not (p :|: q))
norm ((Not p) :|: (Not q)) = norm (Not (p :&: q))
norm p = p

main =  do
        print $ norm (Not (Var "p" :|: Var "q")) -- Not (Var "p") :&: Not (Var "q")
        print $ norm (Not (Not (Var "p")) :|: (Not T)) -- (Var "p" :|: F)
        print $ norm (Not (Var "p" :&: Not (Var "q"))) -- Not (Var "p") :|: Var "q"

Proposition normalization.md

Proposition normalization

The following datatype represents propositions, as in propositional logic. (e.g., P &Q, Not P, …)

data Proposition = Var String
		  	| F
		  	| T
		  	| Not Proposition
		  	| Proposition :|: Proposition --or
		  	| Proposition :&: Proposition
		  	deriving (Eq, Ord, Show)

a. Write a function

isNorm :: Proposition -> Bool

that returns true when a proposition is in negation normal form. A proposition is in negation normal form if the only occurrences of logical negation (Not) are applied to variables. For example,

>isNorm (Var "p" :&: Not (Var "q")) = True
>isNorm (Not (Var "p" :|: Var "q")) = False
>isNorm (Not (Not (Var "p")) :|: Not T) = False
>isNorm (Not (Var "p" :&: Not (Var "q"))) = False

b. Write a function

norm :: Proposition -> Proposition

that converts a proposition to an equivalent proposition in negation normal form. A propositon may be converted to normal form by repeated application of the following equivalences:

Not F <-> T
Not T <-> F
Not (Not p) <-> p
Not (p :|: q) <-> Not p :&: Not q
Not (p :&: q) <-> Not p :|: Not q

For example,

>norm (Var "p" :&: Not (Var "q"))
= (Var "p" :&: Not (Var "q"))
>norm (Not (Var "p" :|: Var "q"))
= Not (Var "p") :&: Not (Var "q")
>norm (Not (Not (Var "p")) :|: Not T)
= (Var "p" :|: F)
>norm (Not (Var "p" :&: Not (Var "q")))
= Not (Var "p") :|: Var "q"