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 `form`

:

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 `conj`

(resp. `disj`

) is isomorphic to a non-empty list of `atom`

s (resp. `conj`

).

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 `disj`

:

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 `disj`

:

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…

#### Supplementary exercise

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 `form`

, `conj`

and `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 b. 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 ;)