### Disjunctive normal forms in big steps

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. 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 ;)