examples/huffman_with_two_queues.mlw

   1
   2 (** Huffman coding with two queues (instead of a priority queue)
   3
   4   Huffman coding is an algorithm to build a prefix code given a frequency
   5   for each symbol. See https://en.wikipedia.org/wiki/Huffman_coding
   6
   7   Huffman coding is typically implemented with a priority queue.
   8   We pick up the two trees with the smallest frequencies frequencies,
   9   we build a new tree with the sum of the frequencies, we put it
  10   back in the priority queue, until there is a single tree.
  11
  12   However, when the initial list of frequencies is sorted,
  13   we can implement the algorithm in a simpler (and more efficient way),
  14   using two (regular) queues instead of a priority queue.
  15   See http://www.staff.science.uu.nl/~leeuw112/huffman.pdf
  16
  17   In the following, we implement and prove the core of this algorithm,
  18   using a sorted list of integers as input and its sum as output
  19   (we do not build Huffman trees here). The key here is to prove that the
  20   two queues remain sorted.
  21
  22   Author: Jean-Christophe Filliâtre (CNRS)
  23   Thanks to Judicaël Courant for pointing this paper out.
  24 *)
  25
  26 use int.Int
  27 use seq.Seq
  28 use seq.SortedInt
  29 use seq.Sum
  30
  31 function last (s: seq int) : int = s[length s - 1]
  32
  33 lemma add_last:
  34   forall s: seq int, x.
  35   length s > 0 -> sorted s -> last s <= x -> sorted (snoc s x)
  36 lemma sorted_tail:
  37   forall s. sorted s -> length s >= 1 -> sorted s[1 .. ]
  38 lemma sorted_tail_tail:
  39   forall s. sorted s -> length s >= 2 -> sorted s[2 .. ]
  40
  41 let huffman_coding (s: seq int) : int
  42   requires { length s > 0 }
  43   requires { sorted s }
  44   ensures  { result = sum s }
  45 = let ref x = s in
  46   let ref y = empty in
  47   while length x + length y >= 2 do
  48     invariant { length x + length y > 0 }
  49     invariant { sum x + sum y = sum s }
  50     invariant { sorted x } invariant { sorted y }
  51     invariant { length x >= 2 -> length y >= 1 -> last y <= x[0] + x[1] }
  52     invariant { length x >= 1 -> length y >= 2 -> last y <= x[0] + y[0] }
  53     invariant {                  length y >= 2 -> last y <= y[0] + y[1] }
  54     variant   { length x + length y }
  55     if length y = 0 then begin
  56       y <- snoc y (x[0] + x[1]);
  57       x <- x[2 .. ]
  58     end else if length x = 0 then begin
  59       y <- snoc y[2 .. ] (y[0] + y[1]);
  60     end else begin (* both non-empty *)
  61       if x[0] <= y[0] then
  62         if length x >= 2 && x[1] <= y[0] then begin
  63           y <- snoc y (x[0] + x[1]);
  64           x <- x[2 .. ]
  65         end else begin
  66           y <- snoc y[1 .. ] (x[0] + y[0]);
  67           x <- x[1 .. ]
  68         end
  69       else
  70         if length y >= 2 && y[1] <= x[0] then begin
  71           y <- snoc y[2 .. ] (y[0] + y[1]);
  72         end else begin
  73           y <- snoc y[1 .. ] (x[0] + y[0]);
  74           x <- x[1 .. ]
  75         end
  76     end
  77   done;
  78   if length x > 0 then x[0] else y[0]