(* Conversion to the conjunctive normal form *)
(* Wikipedia:
``In Boolean logic, a formula is in conjunctive normal form (CNF) or
clausal normal form if it is a conjunction of one or more clauses,
where a clause is a disjunction of literals; otherwise put, it is an
AND of ORs. As a canonical normal form, it is useful in automated
theorem proving and circuit theory.''
(L1 OR L2 ...) AND ...
Furthermore,
``In automated theorem proving, the notion "clausal normal form" is
often used in a narrower sense, meaning a particular representation of
a CNF formula as a set of sets of literals.''
We will use this representation below.
*)
(* L
#load "basic_gates.cmo";;
#load "bconst_prop.cmo";;
*)
open Basic_gates
open Bconst_prop
(* Standard Algorithm (cited in Wikipedia):
1. Convert to negation normal form:
move NOTs inwards by repeatedly applying De Morgan's Law
2. Distribute ORs inwards over ANDs:
repeatedly replace P ∨ ( Q ∧ R ) with ( P ∨ Q ) ∧ ( P ∨ R)
Note the two phases of the algorithm, and the phrase
``repeatedly replace''
The algorithm is very syntactic: term rewriting in a very specific sequence
At previous tutorials (at the first Metaprogramming Summer School)
I really showed that re-writing in tagless-final style. But now we will do
something different
*)
(* Cartesian product, applying the function f to a pair of elements
taken from the two input lists:
{ f x y | x <- xs, y <- ys }
The order of the result list is not defined.
*)
let cart : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list = fun f xs ys ->
let rec outer acc = function
| [] -> acc
| h1::t1 ->
let rec inner acc = function
| [] -> outer acc t1
| h2::t2 -> inner (f h1 h2::acc) t2
in inner acc ys
in outer [] xs
let [(3, 11); (3, 10); (2, 11); (2, 10); (1, 11); (1, 10)]
= cart (fun x y -> (x,y)) [1;2;3] [10;11]
(* Somewhat optimized, taking advantage of the unit absorbtion law
Could also be a standard function. But it is easy to write.
*)
let fold_monoid : ('a -> 'a -> 'a) -> 'a -> 'a list -> 'a = fun op z ->
function
| [] -> z
| h::t -> List.fold_left op h t
(* Laws
* Distributivity of OR over AND
* (A && B) || C = (A || C) && (B || C)
* De Morgan laws
* NOT (A && B) = NOT A || NOT B
* NOT (A || B) = NOT A && NOT B
*)
(* Remember that phrase from Wikipedia?
``In automated theorem proving, the notion "clausal normal form" is
often used in a narrower sense, meaning a particular representation of
a CNF formula as a set of sets of literals.''
*)
module CNF(I:SYMO) = struct
type repr = claw list (* can be empty, if TRUE *)
and claw = atom list (* can be empty, if FALSE *)
and atom = Atom of polarity * literal
and polarity = Pos | Neg
and literal = I.repr
let atom : I.repr -> repr = fun x -> [[Atom (Pos,x)]]
let inj : I.repr -> repr = atom
let lit x : repr = atom (I.lit x)
(* conjoin the clauses (i.e., disjuncts) *)
let (&&) : repr -> repr -> repr = (@)
(* apply distributivity of OR over AND: Cartesian product *)
let (||) : repr -> repr -> repr = cart (@)
let neg : repr -> repr =
let neg_atom : atom -> atom = function
| Atom (Pos,x) -> Atom (Neg,x)
| Atom (Neg,x) -> Atom (Pos,x)
in
let neg_claw : claw -> repr = List.map (fun x -> [neg_atom x])
in
fun cs -> List.map neg_claw cs |> List.fold_left (||) [[]]
(* Convert back to the SYM term: `readout' *)
let prj : repr -> I.repr =
let build_lit : atom -> I.repr = function
| Atom (Pos,x) -> x
| Atom (Neg,x) -> I.neg x
in let build_disj : claw -> I.repr = fun l ->
List.map build_lit l |> fold_monoid I.(||) (I.lit false)
in let build_conj : claw list -> I.repr = fun l ->
List.map build_disj l |> fold_monoid I.(&&) (I.lit true)
in build_conj
type obs = I.obs
let observe e = I.observe @@ prj e
end
(* Comparison with the rewriting approach (syntactic approach):
in re-writing, the cnf conversion has the type
cnf : smdata -> symdata
If we forget to distribute something properly and hence the result isn't
actually a conjunction of disjunctions of atoms, the type checker offers no
help.
With CNF, the normal term has a different type, and a different form:
CNF(I).repr vs I.repr.
Therefore, the silly errors in nomalization will get caught. The point is
that CNF(I).repr is a representation of a normal form
*by its very construction*
*)
let _ = ex1(module SWO0)
let _ = ex1(module CNF(SWO0))
module CNFW(I:SYMWO) = struct
include CNF(I)
let wire_x = inj I.wire_x
let wire_y = inj I.wire_y
let wire_z = inj I.wire_z
end
let _ = ex2(module SWO0)
let _ = ex2(module CNFW(SWO0))
let _ = let module I = CNFW(SWO0) in
I.observe @@ ex2(module I)
(* One of the Wikipedia examples *)
let wex1 : type a. a symwmod -> a = function (module I) -> let open I in
(wire_x && wire_y) || wire_z
let _ = wex1 (module SWO0)
let _ = let module I = CNFW(SWO0) in I.observe @@ wex1 (module I)
(* a && (b || (d && e))
--> a && (b || d) && (b || e)
*)
let wex2 : type a. a symwmod -> a*a*a*a -> a = fun (module I) (a,b,d,e) ->
let open I in
a && (b || (d && e))
let _ = let module I = CNFW(SWO0) in
I.observe @@ wex2 (module I) I.(inj "a",inj "b",inj "d",inj "e")
let _ = exadd2 (module SWO0)
let _ = exadd2 (module CNFW(SWO0))
let _ = let module I = CNFW(SWO0) in I.observe @@ exadd2 (module I)
let _ = exadd3 (module SWO0)
let _ = let module I = CNFW(SWO0) in I.observe @@ exadd3 (module I)
(* Composability of transformations *)
let _ = exadd_xy1 (module SWO0)
let _ = let module I = CNFW(SWO0) in I.observe @@ exadd_xy1 (module I)
let _ = let module I = CNFW(CPW(SWO0)) in I.observe @@ exadd_xy1 (module I)
let _ = exadd_xy1 (module CPW(CNFW(SWO0)))
let _ = let module I = CPW(CNFW(SWO0)) in I.observe @@ exadd_xy1 (module I)
(* QUIZ
The results of optimizations in a different order differ a bit:
generally, the order matters.
That's why in compilers, optimization passes are repeated several times.
Implement the facility to repeat transformations n times.
*)
;;
(* QUIZ
The result of CNFW(CPW(SW0)) shows there is still room for simplification.
Implement it
*)
(* QUIZ
Exercise: CNF conversion can lead to exponential explosion.
Implement Tseitin's algorithm that has only linear increase in size.
*)