[Haskell-cafe] Disjunctive Normal Form

[Arnar Birgisson]

Hey folks,

On Nov 1, 2007 6:41 PM, Luke Palmer <lrpalmer at gmail.com> wrote:
> A good way to approach this is data-structure-driven programming.  You
> want a data structure which represents, and can _only_ represent,
> propositions in DNF.  So:
>
> data Term = Pos Var | Neg Var
> type Conj = [Term]
> type DNF  = [Conj]
>
> Then write:
>
> dnf :: LS -> DNF
>
> The inductive definition of dnf is straightforward given this output type...

Jim, if you don't want to see an attempt at a solution, don't read further.

I'm learning too and found this an interesting problem. Luke, is this
similar to what you meant?

data LS = Var String | Not LS | And LS LS | Or LS LS deriving Show

data Term = Pos String | Neg String deriving Show
type Conj = [Term]
type DNF = [Conj]

dnf :: LS -> DNF
dnf (Var s) = [[Pos s]]
dnf (Or l1 l2) = (dnf l1) ++ (dnf l2)
dnf (And l1 l2) = [t1 ++ t2 | t1 <- dnf l1, t2 <- dnf l2]
dnf (Not (Not d)) = dnf d
dnf (Not (And l1 l2)) = (dnf $ Not l1) ++ (dnf $ Not l2)
dnf (Not (Or l1 l2)) = [t1 ++ t2 | t1 <- dnf $ Not l1, t2 <- dnf $ Not l2]
dnf (Not (Var s)) = [[Neg s]]

-- test cases
x = (Or (And (Var "A") (Var "B")) (Or (And (Not $ Var "C") (Var "D"))
(Var "E")))
y = (Not (And (Var "A") (Var "B")))
z = (Not (And (Not y) y))


 Also, is it correct?

cheers,
Arnar