PROBLEM 2 (Regular): Negation normal form (NNF) refers to a form of Boolean formulae in which negation is applied only to propositional variables, never to conjunctions, disjunctions, or other negations. For example, this formula is in NNF: A \/ (~B /\ ~C) while this formula is not A \/ ~(B \/ C) Your next task is to write a function `nnf` which transforms arbitrary input Boolean formulae into NNF. You will need the following equations (where A, B, and C are arbitrary formulae): De Morgan's Laws: ~(A /\ B) == ~A \/ ~B ~(A \/ B) == ~A /\ ~B Double negation elimination: ~~A == A You do not need to perform other simplifications (such as reducing A /\ A to A or reducing A \/ ~A to True). The subtlety of this problem is in the structure of recursive calls: for example, when normalizing the term "~(~A /\ B)", should you normalize the subformulae "~A" and "B" before or after applying De Morgan's law? For testing, I have provided a function `isNnf`, which returns `True` if its input is in negation normal form and `False` otherwise. You should NOT use the `isNnf` function in your implementation of `nnf`. -------------------------------------------------------------------------------} nnf :: Formula -> Formula nnf = error "nnf not implemented" isNnf (And a b) = isNnf a && isNnf b isNnf (Or a b) = isNnf a && isNnf b isNnf (Not (Var _)) = True isNnf (Var _) = True isNnf _ = False nnfTests = TestList [ "double negation" ~: isNnf (nnf (Not (Not (Var "x")))) ~?= True , "de Morgan's laws" ~: isNnf (nnf (Not (Or (Var "x") (Var "y")))) ~?= True -- Your tests go here ]