Splitting Hairs

It is often claimed that the formal derivation of an algorithm hand-in-hand with its specification is too hard to do, so that it is only viable for toy examples. I have found, as Dijkstra repeatedly has, that discipline and restraint in the drive to "just code" are key to succeeding. As an example, I'll show the creation from scratch of a program I didn't know before.

Aside: You'll have to believe me on this, but I first attempted to code this program without paying attention to the logic; it had a bug. Instead of trying to paper over it with some fix or other, I started from scratch. Apart from some minor omissions, due more to inattention to the predicates than anything else, it worked on the first try.

This program generates the partitions of an integer n in reverse lexicographical (or colex) order. As I did before, I choose to write it in imperative OCaml, with each generated value being fed to a continuation; this allows straightforward translation to many other languages without the need to fake or build functional features in. The first question I must answer is what is an adequate logical description of a partition? "Adequate" here means the weakest (that is, least constraining) predicate that completely defines a partition.

I'll keep the partition of n as an array v of monotonically non-increasing, positive values that sum to n. The predicate that characterizes a partition is:

P ≡ ⟨∑ i : 0 ≤ i < n : v.i⟩ = n ∧ ⟨∀ i, j : 0 < i < j < n : v.i ≥ v.j > 0⟩

That is a mouthful, and —more worryingly— is over-constrained. Any partition might have less than n elements; in fact most will. The standard operating procedure is to change a constant by a variable and parameterize the predicate by it, call it l. In the process, I'll split the predicate in two:

S.l ≡ ⟨∑ i : 0 ≤ i < l : v.i⟩ = n
T.l ≡ ⟨∀ i, j : 0 < i < j < l : v.i ≥ v.j > 0⟩

so that P.l ≡ S.l ∧ T.l. Now v.0 = n ∧ l = 1 immediately satisfy P.l, and so I can begin with a program scheme:

let part_iter n (f : int array -> int -> unit) =
  let v = Array.make n 0
  and l = ref 1 in
  v.(0) <- n;
  (* P.l *)
  f v !l;
  Generate the partitions in colex order
  (* P.n *)

The kernel of the code must change both v and l stepwise, such that the last partition is found when l = n; this will be our stopping condition:

let part_iter n (f : int array -> int -> unit) =
  let v = Array.make n 0
  and l = ref 1 in
  v.(0) <- n;
  (* P.l *)
  f v !l;
  while !l != n do
    Advance v and l to the next partition in colex order
    (* P.l *)
    f v !l
  done
  (* P.n *)

Think of the partition as a row of piles of stones or marbles, in non-increasing order. To respect the colex order, the change must be done as far to the right as possible, and must be a decrement of the last pile that can be so altered, under invariance of T.l:

let part_iter n (f : int array -> int -> unit) =
  let v = Array.make n 0
  and l = ref 1 in
  v.(0) <- n;
  (* P.l *)
  f v !l;
  while !l != n do
    let j = ref (!l - 1) in
    while v.(!j) == 1 do v.(!j) <- 0; decr j done;
    v.(!j) <- v.(!j) - 1;
    Restore S.l under invariance of T.l
    (* P.l *)
    f v !l
  done
  (* P.n *)

The inner loop picks up the singleton piles that cannot possibly be decremented, until finding one pile that can. Or rather, picking up singleton piles is decrementing them; if OCaml had repeat… until loops, the inner loop could be written more compactly as:

let j = ref !l in
repeat decr j; v.(!j) <- v.(!j) - 1 until v.(!j) != 0;
Restore S.l…

In order to keep the partition to sum to n, the l - j picked-up stones must be added back under invariance of T.l:

let part_iter n (f : int array -> int -> unit) =
  let v = Array.make n 0
  and l = ref 1 in
  v.(0) <- n;
  (* P.l *)
  f v !l;
  while !l != n do
    let j = ref (!l - 1) in
    while v.(!j) == 1 do v.(!j) <- 0; decr j done;
    v.(!j) <- v.(!j) - 1;
    let s = ref (!l - !j) in
    incr j;
    while !s != 0 do
      Add back s under invariance of T.l
    done;
    (* S.j *)
    l := !j;
    (* P.l *)
    f v !l
  done
  (* P.n *)

Invariance of T.l means that we must not add more stones than the previous pile has:

let part_iter n (f : int array -> int -> unit) =
  let v = Array.make n 0
  and l = ref 1 in
  v.(0) <- n;
  (* P.l *)
  f v !l;
  while !l != n do
    let j = ref (!l - 1) in
    while v.(!j) == 1 do v.(!j) <- 0; decr j done;
    v.(!j) <- v.(!j) - 1;
    let s = ref (!l - !j) in
    incr j;
    while !s != 0 do
      v.(!j) <- min v.(!j - 1) !s;
      s := !s - v.(!j);
      incr j
    done;
    (* S.j *)
    l := !j;
    (* P.l *)
    f v !l
  done
  (* P.n *)

That's it. On a personal note, I'm not so much proud that I could write this program, but rather that I've learned enough of Dijkstra's discipline to put it to effective use.

Aside: Now that I read it, I don't think the sarcastic overtones of the title are in the spirit of this article. I chose it at the beginning as a pun on integer partitions; someone may construe it as a disparaging remark on the level of attention to detail needed to formally derive programs. If so, their loss; to me, the confidence gained by such hair-splitting is reassuring.