## 18 August 2011

### Putting Formulas in Normal Form

What would be a beautiful description for conversion to DNF?

The problem of converting a formula to DNF is easy to explain: Given a boolean formula, write it as a disjunction of conjunctions. For example, $(x \lor y) \land z$ may be rewritten, by distributivity, as $(x \land z) \lor (y \land z)$. The mechanism is also easy to describe: Push $\lnot$ down by de Morgan, then pull $\lor$ above $\land$ by distributivity.

How to turn this description into an algorithm?

I know a nice algorithm for the first half. Expressed in OCaml, it goes like this: We want a function with the type f1->f2, where

type f1 = [Var of string | Not of f1 | And of f1 list | Or of f1 list]
type f2 = [Pos of string | Neg of string | And of f2 list | Or of f2 list]


The trick is to keep around a parity.

let rec pnd (p : bool) : f1 -> f2 = function
| Var x -> if p then Pos x else Neg x
| Not f -> pnd (not p) f
| And fs ->
let fs = List.map (pnd p) fs in
if p then And fs else Or fs
| Or fs ->
let fs = List.map (pnd p) fs in
if p then Or fs else And fs


This algorithm I use when I do boolean manipulations on paper. So I like it. The code is nice, rather than beautiful, because it has some repetition.

What would be a similarly nice solution for the second half—applying distributivity? Expressed in OCaml, we want a function with the type f2->dnf, where

type dnf = [Pos of string | Neg of string] list list


Of course, I'm interested in solutions in any language.

beroal said...

What would be a similarly nice solution for the second half—applying distributivity?
Why not? First, I suppose you intended to write «dnf» instead of «cnf». The meaning of «cnf», i.e. of «atom list list» is «atom conjunction disjunction». I define type constructors «conjunction» and «disjunction» as synonyms for «list», they just describe meaning. (Atom=literal. I will use double angle quotes to denote source code, it seems that the HTML tag "code" does not work here.)

I would describe this algorithm as such: map a value of type «f2» by the catamorphism into a suitable algebra «A». «A» has the carrier «dnf» and the following operations:

* For «Or fs», recursively map formulas in «fs» to DNFs by the catamorphism, thus we obtain a value of type «atom conjunction disjunction disjunction», then join (by «List.concat» in ML) rightmost disjunctions.
* For «And fs», recursively map formulas in «fs» to DNFs by the catamorphism, thus we obtain a value of type «atom conjunction disjunction conjunction». Converting this to DNF is more intricate. We should exchange bolded disjunction and conjunction (lets call the exchanging function «distrib»), then join leftmost conjunctions.

«distrib» has type «'a disjunction conjunction -> 'a conjunction disjunction». Moreover, «distrib» makes sense in any ring. If the bolded conjunction is 2-ary, i.e. the argument of «distrib» has the form «[d0;d1]», then we should conjoin every element of d0 with every element of d1, i.e. apply the function «fun x0 x1 -> [x0; x1]» to all pairs of elements.

In Haskell this can be done with «liftA2 (\x0 x1 -> [x0,x1]) d0 d1». In ML we can define «liftA2» as here. And if the argument of «distrib» has >=2 elements, we should fold it by a similar function «liftA2 (\x0 x1 -> x0:x1)».

Therefore «distrib» can be defined «foldr (liftA2 (:)) [[]]». I attached a ML version of «distrib» to the link above and a Haskell version here. The Haskell version is simplified and does not contain explicit «distrib» though.

rgrig said...

Yes, I meant dnf, not cnf. Fixed and thanks.

Cool. The solution I use now (found with Rasmus) is the following.

let dnf f =
let cons x xs = x :: xs in
let rec fold g = function
| And hs -> List.fold_left fold g hs
| Or hs -> List.concat (List.map (fold g) hs)
| h -> List.map (cons h) g in
fold [[]] (pnd true f)

Whenever fold g h is called we have $f=g \land h$ ang $g$ is in DNF. At the beginning $f=1 \land f$ and at the end $f=g \land 1$.

(It's annoying that so much of HTML is disallowed in comments. Sorry.)

rgrig said...

The solution I had yesterday was more complicated. Suppose you have a term $a \land b \land c$ represented as a list $[a;b;c]$. If we discover that $b$ and $c$ are in fact conjunctions, then we expand $[a;b_1 \land b_2;c_1 \land c_2]$ into $[a;b_1;b_2;c_1;c_2]$. If we discover that they are in fact disjunctions, then we expand $[a;b_1 \lor b_2; c_1 \lor c_2]$ into $[a;b_1;c_1]$; $[a;b_1;c_2]$; $[a;b_2;c_1]$; $[a;b_2;c_2]$. We recurse the expansion until all members are atomic.

The expansion in the $\lor$ case was

let cartesian xss =
let rec f acc = function
| [] -> List.map List.rev acc
| xs :: xss ->
let ys = List.map (fun x -> List.map (fun ys -> x :: ys) acc) xs in
f (List.concat ys) xss in
f [[]] xss

rgrig said...

... cartesian is basically your distrib

beroal said...

This algorithm has several equivalent variants. We can exchange «fold_left» and «fold_right», reverse lists, because conjunction and disjunction are associative and commutative. We can write recursion explicitely or use recursion in library functions.

Rasmus's «fold» function conjoins «dnf» and «f2» to «dnf» (I would rather call it «conj_dnf_f2»), whereas my «logicDistrib» lacks the «dnf» argument. Therefore in «logicDistrib»: 0) the «And» branch is longer because it requires «liftA2» to conjoin «dnf» and «dnf»; 1) the «Or» and atom branches are shorter because they are free from the «dnf» argument.

I am pretty sure that simplification from «logic_distrib» in ML to «logicDistrib» in Haskell can be done with monad axioms. I would be happy to know what theorems are useful to pass from «logicDistrib» to «fold».