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∨y)∧z(x∨y)∧z may be rewritten, by distributivity, as (x∧z)∨(y∧z)(x∧z)∨(y∧z). The mechanism is also easy to describe: Push ¬¬ down by de Morgan, then pull ∨∨ above ∧∧ 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.
5 comments:
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 «Orfs»,recursivelymapforμlas∈«fs»→DNFsbythecatamorϕsm,thusweobta∈avalueoftype«a→mconjunctiondisjunctiondisjunction»,thenjo∈(by«List.concat»∈ML)rightmostdisjunctions.⋅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.
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
| Andhs→List.fold≤ftfoldghs∣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∧h ang g is in DNF. At the beginning f=1∧f and at the end f=g∧1.
(It's annoying that so much of HTML is disallowed in comments. Sorry.)
The solution I had yesterday was more complicated. Suppose you have a term a∧b∧c represented as a list [a;b;c]. If we discover that b and c are in fact conjunctions, then we expand [a;b1∧b2;c1∧c2] into [a;b1;b2;c1;c2]. If we discover that they are in fact disjunctions, then we expand [a;b1∨b2;c1∨c2] into [a;b1;c1]; [a;b1;c2]; [a;b2;c1]; [a;b2;c2]. We recurse the expansion until all members are atomic.
The expansion in the ∨ 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
... cartesian is basically your distrib
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».
Post a Comment
Note: (1) You need to have third-party cookies enabled in order to comment on Blogger. (2) Better to copy your comment before hitting publish/preview. Blogger sometimes eats comments on the first try, but the second works. Crazy Blogger.