### 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 `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 ;)

Hi Matthias,

Recently I also needed some functional code for CNF and, after realizing it is not so easy to write it nicely myself, I found this bit of Agda code of Wojciech Jedynak:

https://github.com/wjzz/Agda-small-developments-and-examples/blob/master/DNF.agda

Hope it helps

Hi Danko,

Thanks for the pointer. It is actually the same code! Nice to see that we ended up with the same idea. Hope everything is well in Paris.

Here is my attempt in Agda (without the flattening operation): https://gist.github.com/gallais/10976846 The bulk of the work is done in _⟦∧⟧_.

I really like that your solution combines only primitive-recursive functions. But I’m quite happy with the symmetries involved in the definition of _⟦∧⟧_.

Hello Guillaume, thank you for the contribution. Is your development actually proving semantics preservation?

For the second part, I don’t think your atom definition is going to work because all atoms can unify with each other. You need a type such that all atoms (atom forms) have distinct types.

I can write this now, which type checks but I don’t think is what we want.

let dnf : type a . a form -> a dnf =

function

| X _ -> Dnf (Refl, Conj (X 5))

| _ -> assert false

(btw, I changed the type of dnf function, I think yours has a typo, it doesn’t even parse for me)

Thank you, I fixed the typo in the type of dnf. Regarding the definition of atom, I’m not sure what’s bothering you. What does not work (for a reason I can’t really grasp) is *not* giving a definition to atom, and leave it abstract. I actually have a solution involving ‘a atom = int. I’ll post it in a few days.

I agree with you that ideally solution should work for ‘a atom abstract. Maybe you are hitting new checks for injectivity and variance in 4.01

http://www.math.nagoya-u.ac.jp/~garrigue/papers/injectivity.pdf

Ok sorry, I’m getting your point only now. You’re right, defining atom with int is wrong (too permissive), my bad. I think it should be: type ‘a atom = ‘a.

Hi Matthias,

Some time ago I had to implement a conversion from an arbitrary logic formula to CNF in order to use it in a SAT solver that accepts formulas only in CNF. So I ended up in implementing a module which supports the conversion. It is a part of a small library that is able to find any or all solutions for a SAT problem, so this might interest you: https://github.com/zayac/ocaml-picosat/blob/master/lib/logic.ml

[…] is the answer to last post’s puzzle. I gave an algorithm to put a formula in disjunctive normal form, and suggested to prove it correct […]