Disjunctive normal forms in big steps
by Matthias Puech
This is probably a second-semester functional programming exercise, but I found it surprisingly hard, and could not find a solution online. So at the risk of depriving a TA from a problem for its mid-term exam, here is my take on it, that I painfully put together yesterday.
Given a formula built out of conjunction, disjunction and atoms, return its disjunctive normal form, in big step or natural semantics, that is, not applying repetitively the distributivity and associativity rules, but in a single function run. Before you go any further, please give it a try and send me your solution!
Formulas are described by the type
type atom = int type form = | X of atom | And of form * form | Or of form * form
To ensure the correctness of the result, I represent disjunctive normal form by a restriction of this type,
disj, by stratifying it into conjunctions and disjunctions:
type conj = X of atom | And of atom * conj type disj = Conj of conj | Or of conj * disj
There are actually two restrictions at stake here: first, conjunctions cannot contain disjunctions, and second, all operators are necessarily right-associative. Constructor
Conj is just a logically silent coercion. If you look carefully enough, you will notice that
disj) is isomorphic to a non-empty list of
The first step is to lift the second restriction (associativity), and prove that we can always build a conjunction of
conj, resp. a disjunction of
disj. Easy enough if you think about lists: these functions look like concatenation.
let rec conj : conj -> conj -> conj = fun xs ys -> match xs with | X x -> And (x, ys) | And (x, xs) -> And (x, conj xs ys) let rec disj : disj -> disj -> disj = fun xs ys -> match xs with | Conj c -> Or (c, ys) | Or (x, xs) -> Or (x, disj xs ys)
Then, we will lift the second restriction, using distributivity. We must show that it is always possible to form a conjunction. First, we show how to build the conjunction of a
conj and a
let rec map : conj -> disj -> disj = fun x -> function | Conj y -> Conj (conj x y) | Or (y, ys) -> Or (conj x y, map x ys)
The first case is trivial, the second reads as the distributivity of conjunction over disjunction. By analogy to lists again, I called this function
map because it maps function
conj x to all cells of the list.
Next, we show how to build the conjunction of two
let rec cart : disj -> disj -> disj = fun xs ys -> match xs with | Conj c -> map c ys | Or (x, xs) -> disj (map x ys) (cart xs ys)
Considering the meaning of the previously defined functions, the first case is trivial, and the second, again, reads as distributivity, only in the other direction. I called this function
cart because it computes the cartesian product of the two “lists” passed as arguments (only on non-empty lists).
Now we can easily put together the final function computing the DNF:
let rec dnf : form -> disj = function | X x -> Conj (X x) | Or (a, b) -> disj (dnf a) (dnf b) | And (a, b) -> cart (dnf a) (dnf b)
It is easy to see that all function terminate: they are primitive recursive.
Wait, let’s not forget to test our contraption:
let () = assert (dnf (Or (And (X 1, X 2), X 3)) = Or (And (1, X 2), Conj (X 3))); assert (dnf (And (Or (X 1, X 2), X 3)) = Or (And (1, X 3), Conj (And (2, X 3)))); assert (dnf (And (Or (And (X 0, X 1), X 2), And (X 3, X 4))) = Or (And (0, And (1, And (3, X 4))), Conj (And (2, And (3, X 4)))))
That’s my solution. Reader, is there another one? Is there a better explanation, for instance based on Danvy’s small-step to big-step derivation? I believe there is…
Technically, there still could be bugs in this code. Prove that it is correct wrt. the small-step rewrite rules, using only OCaml and GADTs. Here is the beginning of an idea: annotate
disj with their meaning in terms of OCaml types:
type ('a, 'b) union = Inl of 'a | Inr of 'b type 'a atom = int type 'a form = | X : 'a atom -> 'a form | And : 'a form * 'b form -> ('a * 'b) form | Or : 'a form * 'b form -> ('a, 'b) union form type 'a conj = | X : 'a atom -> 'a conj | And : 'a atom * 'b conj -> ('a * 'b) conj type 'a disj = | Conj : 'a conj -> 'a disj | Or : 'a conj * 'b disj -> ('a, 'b) union disj
(the definition of
union is irrelevant here), state the relation between equivalent types as a type:
type ('a, 'b) equiv = | Refl : ('a, 'a) equiv | Trans : ('a, 'b) equiv * ('b, 'c) equiv -> ('a, 'c) equiv | AssocA : (('a * 'b) * 'c, 'a * ('b * 'c)) equiv | AssocO : ((('a, 'b) union, 'c) union, ('a, ('b, 'c) union) union) equiv | DistribL : ('a * ('b, 'c) union, ('a, 'b) union * ('a, 'c) union) equiv | DistribR : (('b, 'c) union * 'a, ('b, 'a) union * ('c, 'a) union) equiv
pack up a solution as an existential: an equivalence proof together with a DNF:
type 'a dnf = Dnf : ('a, 'b) equiv * 'b disj -> 'a dnf
and code a function:
let dnf : type a. a form -> a dnf = function _ -> (assert false) (* TODO *)
Ok fair enough, it’s not an exercise, it’s something I haven’t been able to put together yet ;)