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 lemma1lemma5, 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 A, there exists a disjuctive normal form B such that A \Leftrightarrow B.

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

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?