Disjunctive Normal Form

[Jim Burton]

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

[Luke Palmer-2]

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

Luke

On 11/1/07, Jim Burton <jim@...> 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@...
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@...
http://www.haskell.org/mailman/listinfo/haskell-cafe

[clconway]

Jim,

Lukes suggestion is a good one, and should help focus you on the
syntactic constraints of DNF. A property that your dnf function should
have is that the right-hand side of each case should yield a DNF
formula. Take, for example,

dnf (And s1 s2)         = And (dnf s1) (dnf s2)

Does And'ing two DNF formulas together yield a DNF?

Regards,
Chris

On 11/1/07, Luke Palmer <lrpalmer@...> 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...
>
> Luke
>
> On 11/1/07, Jim Burton <jim@...> 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@...
> > http://www.haskell.org/mailman/listinfo/haskell-cafe
> >
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe@...
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
>

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@...
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Jules Bean]

It's much much easier to work with n-ary than binary.

It's also easier to define disjunctive normal form by mutual recursion
with conjunctive normal form.

Jules
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@...
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Arnar Birgisson]

Hey folks,

On Nov 1, 2007 6:41 PM, Luke Palmer <lrpalmer@...> 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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@...
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Luke Palmer-2]

On 11/1/07, Arnar Birgisson <arnarbi@...> wrote:
> I'm learning too and found this an interesting problem. Luke, is this
> similar to what you meant?

Heh, your program is almost identical to the one I wrote to make sure
I wasn't on crack.  :-)

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

These two are doing a little extra work:

dnf (Not (And l1 l2)) = dnf (Or (Not l1) (Not l2))
dnf (Not (Or l1 l2))  = dnf (And (Not l1) (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))

Luke
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@...
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Luke Palmer-2]

On 11/2/07, Luke Palmer <lrpalmer@...> wrote:

> On 11/1/07, Arnar Birgisson <arnarbi@...> wrote:
> > 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]
>
> These two are doing a little extra work:
>
> dnf (Not (And l1 l2)) = dnf (Or (Not l1) (Not l2))
> dnf (Not (Or l1 l2))  = dnf (And (Not l1) (Not l2))

I should clarify.  I meant that *you* were doing a little extra work,
by re-implementing that logic for the not cases.  I'm a fan of only
implementing each "unit" of logic in one place, whatever that means.

But to appease the pedantic, my versions are actually doing more
computational work: they are doing one extra pattern match when these
patterns are encountered.  Whoopty-doo.  :-)

Luke
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@...
http://www.haskell.org/mailman/listinfo/haskell-cafe