### Typeful disjunctive normal form

#### by Matthias Puech

This 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 *in OCaml*, thanks to GADTs. My solution happens to include a wealth of little exercises that could be reused I think, so here it is.

I put the code snippets in the order that I think is more pedagogical, and leave to the reader to reorganize them in the right one.

First, as I hinted previously, we are annotating formulas, conjunctions and disjunctions with their corresponding OCaml type, in order to reason on these types:

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

What we are eventually looking for is a function `dnf`

mapping an `'a form `

to a `'b disj`

, but now these two must be related: they must represent two *equivalent* formulae. So, correcting what I just said: `dnf`

must return the pair of a `'b disj`

and a proof that `'a`

and `'b`

are equivalent. This pair is an existential type, which is easily coded with a GADT (we do similarly for conjunctions):

type 'a cnj = Cnj : 'b conj * ('a, 'b) equiv -> 'a cnj type 'a dsj = Dsj : 'b disj * ('a, 'b) equiv -> 'a dsj

Let’s leave out the definition of `equiv`

for a while. Now the code from the previous post is fairly easily adapted:

let rec conj : type a b. a conj -> b conj -> (a * b) cnj = fun xs ys -> match xs with | X x -> Cnj (And (x, ys), refl) | And (x, xs) -> let Cnj (zs, e) = conj xs ys in Cnj (And (x, zs), lemma0 e) let rec disj : type a b. a disj -> b disj -> (a, b) union dsj = fun xs ys -> match xs with | Conj c -> Dsj (Or (c, ys), refl) | Or (x, xs) -> let Dsj (zs, e) = disj xs ys in Dsj (Or (x, zs), lemma1 e) let rec map : type a b. a conj -> b disj -> (a * b) dsj = fun x -> function | Conj y -> let Cnj (z, e) = conj x y in Dsj (Conj z, e) | Or (y, ys) -> let Cnj (z, e1) = conj x y in let Dsj (t, e2) = map x ys in Dsj (Or (z, t), lemma2 e1 e2) let rec cart : type a b. a disj -> b disj -> (a * b) dsj = fun xs ys -> match xs with | Conj c -> map c ys | Or (x, xs) -> let Dsj (z, e1) = map x ys in let Dsj (t, e2) = cart xs ys in let Dsj (u, e3) = disj z t in Dsj (u, lemma3 e1 e2 e3) let rec dnf : type a. a form -> a dsj = function | X x -> Dsj (Conj (X x), refl) | Or (a, b) -> let Dsj (c, e1) = dnf a in let Dsj (d, e2) = dnf b in let Dsj (e, e3) = disj c d in Dsj (e, lemma4 e1 e2 e3) | And (a, b) -> let Dsj (c, e1) = dnf a in let Dsj (d, e2) = dnf b in let Dsj (e, e3) = cart c d in Dsj (e, lemma5 e1 e2 e3)

It seems more verbose, but since the functions now return existentials, we need to deconstruct them and pass them around. I abstracted over the combinators that compose the proofs of equivalence `lemma1`

…`lemma5`

, we’ll deal with them in a moment. For now, you can replace them by `Obj.magic`

and read off their types with `C-c C-t`

to see if they make sense logically. Look at the last function’s type. It states, as expected: for any formula , there exists a disjuctive normal form such that .

Now on this subject, what is it for two types to be equivalent? Well, that’s the “trick”: let’s just use our dear old Curry-Howard correspondence! `'a`

and `'b`

are equivalent if there are two functions `'a -> 'b`

and `'b -> 'a`

(provided of course that we swear to use only the purely functional core of OCaml when giving them):

type ('a, 'b) equiv = ('a -> 'b) * ('b -> 'a)

Now we can state and prove a number of small results on equivalence with respect to the type constructors we’re using (pairs and unions). Just help yourself into these if you’re preparing an exercise sheet on Curry-Howard :)

(* a = a *) let refl : type a. (a, a) equiv = (fun a -> a), (fun a -> a) (* a = b -> b = a *) let sym : type a b. (a, b) equiv -> (b, a) equiv = fun (ab, ba) -> (fun b -> ba b), (fun a -> ab a) (* a = b -> b = c -> a = c *) let trans : type a b c. (b, c) equiv -> (a, b) equiv -> (a, c) equiv = fun (bc, cb) (ab, ba) -> (fun a -> bc (ab a)), (fun c -> ba (cb c)) (* a = b -> c = d -> c * a = d * b *) let conj_morphism : type a b c d. (a, b) equiv -> (c, d) equiv -> (c * a, d * b) equiv = fun (ab, ba) (cd, dc) -> (fun (c, a) -> cd c, ab a), (fun (c, b) -> dc c, ba b) let conj_comm : type a b. (a * b, b * a) equiv = (fun (x, y) -> y, x), (fun (x, y) -> y, x) (* (a * b) * c = a * (b * c) *) let conj_assoc : type a b c. ((a * b) * c, a * (b * c)) equiv = (fun ((x, y), z) -> x, (y, z)), (fun (x, (y, z)) -> (x, y), z) (* a = b -> c + a = c + b *) let disj_morphism : type a b c d. (a, b) equiv -> (c, d) equiv -> ((c, a) union, (d, b) union) equiv = fun (ab, ba) (cd, dc) -> (function Inl c -> Inl (cd c) | Inr a -> Inr (ab a)), (function Inl d -> Inl (dc d) | Inr b -> Inr (ba b)) (* (a + b) + c = a + (b + c) *) let disj_assoc : type a b c. (((a, b) union, c) union, (a, (b, c) union) union) equiv = (function Inl (Inl a) -> Inl a | Inl (Inr b) -> Inr (Inl b) | Inr c -> Inr (Inr c)), (function Inl a -> Inl (Inl a) | Inr (Inl b) -> Inl (Inr b) | Inr (Inr c) -> Inr c) (* a * (b + c) = (a * b) + (a * c) *) let conj_distrib : type a b c. (a * (b, c) union, (a * b, a * c) union) equiv = (function a, Inl b -> Inl (a, b) | a, Inr c -> Inr (a, c)), (function Inl (a, b) -> a, Inl b | Inr (a, c) -> a, Inr c)

Finally, thanks to these primitive combinators, we can prove the lemmas we needed. Again, these are amusing little exercises.

let lemma0 : type a b c d. (a * b, c) equiv -> ((d * a) * b, d * c) equiv = fun e -> trans (conj_morphism e refl) conj_assoc let lemma1 : type a b c d. ((a, b) union, d) equiv -> (((c, a) union, b) union, (c, d) union) equiv = fun e -> trans (disj_morphism e refl) disj_assoc let lemma2 : type a c d u v. (a * c, u) equiv -> (a * d, v) equiv -> (a * (c, d) union, (u, v) union) equiv = fun e1 e2 -> trans (disj_morphism e2 e1) conj_distrib let lemma3 : type a b c d e f. (a * b, c) equiv -> (d * b, e) equiv -> ((c, e) union, f) equiv -> ((a, d) union * b, f) equiv = fun e1 e2 e3 -> trans e3 (trans (disj_morphism e2 e1) (trans (disj_morphism conj_comm conj_comm) (trans conj_distrib conj_comm))) let lemma4 : type a b c d e. (a, c) equiv -> (b, d) equiv -> ((c, d) union, e) equiv -> ((a, b) union, e) equiv = fun e1 e2 e3 -> trans e3 (disj_morphism e2 e1) let lemma5 : type a b c d e. (a, c) equiv -> (b, d) equiv -> (c * d, e) equiv -> ((a * b), e) equiv = fun e1 e2 e3 -> trans e3 (conj_morphism e2 e1)

Note that I only needed the previous primitives to prove these lemmas (and as such to define my functions), so we can even make the type `equiv`

abstract, provided that we are giving a complete set of primitives (which is not the case here). Although I’m not sure what it would buy us…

Anyway. That’s my solution! What’s yours?

Nice.

I spent bunch of time last week trying to write a solution using your initial definition of equiv type. I just got bunch of crazy type errors and I gave up.

So instead of my solution, here is your solution again but with a small tweak.

I used definition of equivalence from your last post (adding necessary variants). This gives you a proof tree instead of a conversion function as a proof.

I’m including just the parts different than your code. (I defined or_ and and_ types, I thought it might be easier to read). This works with ‘a atom=int or ‘a atom = ‘a or being abstract type but only in 4.01. In 4.00.1 it doesn’t compile.

type (‘a,’b) or_ = Or_

type (‘a,’b) and_ = And_

type ‘a atom = ‘a (* or = int to get better examples display *)

type (‘a, ‘b) equiv =

| Refl : (‘a, ‘a) equiv

| Sym : (‘a, ‘b) equiv -> (‘b, ‘a) equiv

| Trans : (‘a, ‘b) equiv * (‘b, ‘c) equiv -> (‘a, ‘c) equiv

| AssocA : (((‘a, ‘b) and_, ‘c) and_, (‘a, (‘b, ‘c) and_) and_) equiv

| AssocO : (((‘a, ‘b) or_, ‘c) or_, (‘a, (‘b, ‘c) or_) or_) equiv

| DistribA : ((‘a, (‘b, ‘c) or_) and_, ((‘a,’b) and_, (‘a,’c) and_) or_) equiv

| DistribO : ((‘a, (‘b, ‘c) and_) or_, ((‘a, ‘b) or_, (‘a, ‘c) or_) and_) equiv

| LiftOr : (‘a1,’a2) equiv * (‘b1,’b2) equiv -> ((‘a1,’b1) or_, (‘a2,’b2) or_) equiv

| LiftAnd : (‘a1,’a2) equiv * (‘b1, ‘b2) equiv -> ((‘a1,’b1) and_, (‘a2,’b2) and_) equiv

| CommA : ((‘a,’b) and_, (‘b,’a) and_) equiv

| CommO : ((‘a,’b) or_, (‘b,’a) or_) equiv

let lemma0 : type a b c d. ((a,b) and_, c) equiv -> (((d,a) and_,b) and_, (d,c) and_) equiv =

fun e -> Sym (Trans (Sym (LiftAnd (Refl,e)), Sym AssocA))

let lemma1 : type a b c d. ((a, b) or_, d) equiv ->

(((c, a) or_, b) or_, (c, d) or_) equiv =

fun e -> Sym (Trans (Sym (LiftOr (Refl,e)), Sym AssocO))

let lemma2 : type a c d u v. ((a,c) and_, u) equiv -> ((a,d) and_, v) equiv ->

((a, (c, d) or_) and_, (u, v) or_) equiv =

fun e1 e2 -> Sym (Trans (Sym (LiftOr (e1,e2)), Sym DistribA))

let lemma3 : type a b c d e f. ((a,b)and_, c) equiv -> ((d,b)and_, e) equiv ->

((c, e) or_, f) equiv -> (((a, d) or_, b) and_, f) equiv =

fun e1 e2 e3 ->

let e1 : ((b,a)and_,c) equiv = Sym (Trans ((Sym e1), CommA)) in

let e2 : ((b,d)and_,e) equiv = Sym (Trans ((Sym e2), CommA)) in

let t1 : (((b,a)and_,(b,d)and_)or_, ((a,d)or_,b)and_) equiv =

Trans (Sym DistribA, CommA)

in

Sym (Trans (Sym e3, Trans (Sym (LiftOr(e1,e2)), t1)))

let lemma4 : type a b c d e. (a, c) equiv -> (b, d) equiv ->

((c, d) or_, e) equiv -> ((a, b) or_, e) equiv =

fun e1 e2 e3 ->

Trans (LiftOr(e1,e2), e3)

let lemma5 : type a b c d e. (a, c) equiv -> (b, d) equiv ->

((c,d) and_, e) equiv -> ((a,b) and_, e) equiv =

fun e1 e2 e3 -> Trans (LiftAnd(e1,e2), e3)

There are bunch of Syms in the solution, that can be fixed by flipping the definitions in the equiv type.

# dnf (And (Or (X 1, X 2), X 3));;

- : ((‘_a, ‘_b) or_, ‘_c) and_ dsj =

Dsj (Or (And (1, X 3), Conj (And (2, X 3))),

Trans (LiftAnd (Trans (LiftOr (Refl, Refl), Refl), Refl),

Sym

(Trans (Sym Refl,

Trans

(Sym

(LiftOr (Sym (Trans (Sym Refl, CommA)),

Sym (Trans (Sym Refl, CommA)))),

Trans (Sym DistribA, CommA))))))

Sorry for the format, but I don’t know how to format code in comments.

Actually, it’s easy to eliminate all Syms without changing the equiv type.

In that case last example is

# dnf (And (Or (X 1, X 2), X 3));;

- : ((‘_a, ‘_b) or_, ‘_c) and_ dsj =

Dsj (Or (And (1, X 3), Conj (And (2, X 3))),

Trans (LiftAnd (Trans (LiftOr (Refl, Refl), Refl), Refl),

Trans

(Trans (Trans (CommA, DistribA),

LiftOr (Trans (CommA, Refl), Trans (CommA, Refl))),

Refl)))

p.s. it would be nice to be able to edit comments :)

Thanks a bunch Milan, this is great!

As for the question of whether you want to make equiv abstract, that could buy you some efficiency in runtime. You could just define primitives in the mli and just have implementation of all primitives be essentially no-op, returning (None : Obj.magic) or something similar.

When you just have type equivalence (in OCaml sense) you can even avoid Obj.magic and still pay almost no runtime cost (I don’t think that would work here because we have boolean algebra equivalence which compiler can’t deduce on it’s own, but I don’t really understand the whole thing).

For example, look at the implementation in Jane Street’s Core.

https://github.com/janestreet/core_kernel/blob/master/lib/type_equal.ml