[Haskell-cafe] Disjunctive Normal Form

Luke Palmer lrpalmer at gmail.com
Thu Nov 1 14:41:22 EDT 2007

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...


On 11/1/07, Jim Burton <jim at sdf-eu.org> wrote:
> I am trying to rewrite sentences in a logical language into DNF, and wonder
> if someone would point out where I'm going wrong. My dim understanding of it
> is that I need to move And and Not inwards and Or out, but the function
> below fails, for example:
> > dnf (Or (And A B) (Or (And C D) E))
> And (Or A (And (Or C E) (Or D E))) (Or B (And (Or C E) (Or D E)))
> data LS = Var | Not LS | And LS LS | Or LS LS
> --convert sentences to DNF
> dnf :: LS -> LS
> dnf (And (Or s1 s2) s3) = Or (And (dnf s1) (dnf s3)) (And (dnf s2) (dnf s3))
> dnf (And s1 (Or s2 s3)) = Or (And (dnf s1) (dnf s2)) (And (dnf s1) (dnf s3))
> dnf (And s1 s2)         = And (dnf s1) (dnf s2)
> dnf (Or s1 s2)          = Or (dnf s1) (dnf s2)
> dnf (Not (Not d))       = dnf d
> dnf (Not (And s1 s2))   = Or (Not (dnf s1)) (Not (dnf s2))
> dnf (Not (Or s1 s2))    = And (Not (dnf s1)) (Not (dnf s2))
> dnf s                   = s
> Thanks,
> Jim
> --
> View this message in context: http://www.nabble.com/Disjunctive-Normal-Form-tf4733248.html#a13534567
> Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe

More information about the Haskell-Cafe mailing list