examples/binomial_heap.mlw

   1
   2 (** Binomial heaps (Jean Vuillemin, 1978).
   3
   4     Purely applicative implementation, following Okasaki's implementation
   5     in his book "Purely Functional Data Structures" (Section 3.2).
   6
   7     Author: Jean-Christophe Filliâtre (CNRS)
   8 *)
   9
  10 module BinomialHeap
  11
  12   use int.Int
  13   use list.List
  14   use list.Length
  15   use list.Reverse
  16   use list.Append
  17
  18   (** The type of elements, together with a total pre-order *)
  19
  20   type elt
  21
  22   val predicate le elt elt
  23   clone relations.TotalPreOrder with type t = elt, predicate rel = le, axiom .
  24
  25   (** Trees.
  26
  27       These are arbitrary trees, not yet constrained
  28       to be binomial trees. Field `rank` is used later to store the rank
  29       of the binomial tree, for access in constant time. *)
  30
  31   type tree = {
  32         elem: elt;
  33     children: list tree;
  34         rank: int;
  35   }
  36
  37   function size (l: list tree) : int =
  38     match l with
  39     | Nil                     -> 0
  40     | Cons { children = c } r -> 1 + size c + size r
  41     end
  42
  43   let lemma size_nonnneg (l: list tree)
  44     ensures { size l >= 0 }
  45   = let rec auxl (l: list tree) ensures { size l >= 0 } variant { l }
  46     = match l with Nil -> () | Cons t r -> auxt t; auxl r end
  47     with auxt (t: tree) ensures { size t.children >= 0 } variant { t }
  48     = match t with { children = c } -> auxl c end in
  49     auxl l
  50
  51   (** Heaps. *)
  52
  53   (* `e` is no greater than the roots of the trees in `l` *)
  54   predicate le_roots (e: elt) (l: list tree) =
  55     match l with
  56     | Nil      -> true
  57     | Cons t r -> le e t.elem && le_roots e r
  58     end
  59
  60   lemma le_roots_trans:
  61     forall x y l. le x y -> le_roots y l -> le_roots x l
  62
  63   predicate heaps (l: list tree) =
  64     match l with
  65     | Nil                               -> true
  66     | Cons { elem = e; children = c } r -> le_roots e c && heaps c && heaps r
  67     end
  68
  69   lemma heaps_append:
  70     forall h1 [@induction] h2. heaps h1 -> heaps h2 -> heaps (h1 ++ h2)
  71   lemma heaps_reverse:
  72     forall h. heaps h -> heaps (reverse h)
  73
  74   (** Number of occurrences of a given element in a list of trees. *)
  75
  76   function occ (x: elt) (l: list tree) : int =
  77     match l with
  78     | Nil      -> 0
  79     | Cons { elem = y; children = c } r ->
  80        (if x = y then 1 else 0) + occ x c + occ x r
  81     end
  82
  83   let rec lemma occ_nonneg (x: elt) (l: list tree)
  84     variant { size l }
  85     ensures { 0 <= occ x l }
  86   = match l with
  87     | Nil                     -> ()
  88     | Cons { children = c } r -> occ_nonneg x c; occ_nonneg x r
  89     end
  90
  91   lemma occ_append:
  92     forall l1 [@induction] l2 x. occ x (l1 ++ l2) = occ x l1 + occ x l2
  93
  94   lemma occ_reverse:
  95     forall x l. occ x l = occ x (reverse l)
  96
  97   predicate mem (x: elt) (l: list tree) =
  98     occ x l > 0
  99
 100   let rec lemma heaps_mem (l: list tree)
 101     requires { heaps l }
 102     variant  { size l }
 103     ensures  { forall x. le_roots x l -> forall y. mem y l -> le x y }
 104   = match l with
 105     | Nil                     -> ()
 106     | Cons { children = c } r -> heaps_mem c; heaps_mem r
 107     end
 108
 109   (** Binomial tree of rank `k`. *)
 110
 111   predicate has_order (k: int) (l: list tree) =
 112     match l with
 113     | Nil ->
 114         k = 0
 115     | Cons { rank = k'; children = c } r ->
 116         k' = k - 1 && has_order (k-1) c && has_order (k-1) r
 117     end
 118
 119   predicate binomial_tree (t: tree) =
 120     t.rank = length t.children &&
 121     has_order t.rank t.children
 122
 123   lemma has_order_length:
 124     forall l k. has_order k l -> length l = k
 125
 126   (** Binomial heaps. *)
 127
 128   type heap = list tree
 129
 130   (** A heap `h` is a list of binomial trees in strict increasing order of
 131       ranks, those ranks being no smaller than `m`. *)
 132
 133   predicate inv (m: int) (h: heap) =
 134     match h with
 135     | Nil -> true
 136     | Cons t r -> let k = t.rank in m <= k && binomial_tree t && inv (k + 1) r
 137     end
 138
 139   lemma inv_trans:
 140     forall m1 m2 h. m1 <= m2 -> inv m2 h -> inv m1 h
 141
 142   let lemma inv_reverse (t: tree)
 143     requires { binomial_tree t }
 144     ensures  { inv 0 (reverse t.children) }
 145   = let rec aux (k: int) (l: list tree) (acc: list tree)
 146       requires { has_order k l }
 147       requires { inv k acc }
 148       variant  { k }
 149       ensures  { inv 0 (reverse l ++ acc) }
 150     = match l with
 151       | Nil -> ()
 152       | Cons t r ->
 153           assert { binomial_tree t };
 154           aux (k-1) r (Cons t acc)
 155       end in
 156     match t with
 157     | { rank = k; children = c } -> aux k c Nil
 158     end
 159
 160   (** Heap operations. *)
 161
 162   let empty : heap = Nil
 163     ensures { heaps result }
 164     ensures { inv 0 result }
 165     ensures { forall e. not (mem e result) }
 166
 167   let is_empty (h: heap) : bool
 168     ensures { result <-> h = Nil }
 169   = match h with Nil -> true | _ -> false end
 170
 171   let get_min (h: heap) : elt
 172     requires { heaps h }
 173     requires { h <> Nil }
 174     ensures  { mem result h }
 175     ensures  { forall x. mem x h -> le result x }
 176     =
 177     match h with
 178       | Nil      -> absurd
 179       | Cons t l ->
 180           let rec aux (m: elt) (l: list tree) : elt
 181             requires { heaps l }
 182             variant  { l }
 183             ensures  { result = m || mem result l }
 184             ensures  { le result m }
 185             ensures  { forall x. mem x l -> le result x }
 186           = match l with
 187           | Nil             -> m
 188           | Cons {elem=x} r -> aux (if le x m then x else m) r
 189           end in
 190           aux t.elem l
 191     end
 192
 193   let function link (t1 t2: tree) : tree =
 194     if le t1.elem t2.elem then
 195       { elem = t1.elem; rank = t1.rank + 1; children = Cons t2 t1.children }
 196     else
 197       { elem = t2.elem; rank = t2.rank + 1; children = Cons t1 t2.children }
 198
 199   let rec add_tree (t: tree) (h: heap)
 200     requires { heaps (Cons t Nil) }
 201     requires { binomial_tree t }
 202     requires { heaps h }
 203     requires { inv (rank t) h }
 204     variant  { h }
 205     ensures  { heaps result }
 206     ensures  { inv (rank t) result }
 207     ensures  { forall x. occ x result = occ x (Cons t Nil) + occ x h }
 208     =
 209     match h with
 210     | Nil ->
 211         Cons t Nil
 212     | Cons hd tl ->
 213         if rank t < rank hd then
 214           Cons t h
 215         else begin
 216           assert { rank t = rank hd };
 217           add_tree (link t hd) tl
 218         end
 219     end
 220
 221   let add (x: elt) (h: heap) : heap
 222     requires { heaps h }
 223     requires { inv 0 h }
 224     ensures  { heaps result }
 225     ensures  { inv 0 result }
 226     ensures  { occ x result = occ x h + 1 }
 227     ensures  { forall e. e <> x -> occ e result = occ e h }
 228     =
 229     add_tree { elem = x; rank = 0; children = Nil } h
 230
 231   let rec merge (ghost k: int) (h1 h2: heap)
 232     requires { heaps h1 }
 233     requires { inv k h1 }
 234     requires { heaps h2 }
 235     requires { inv k h2 }
 236     variant  { h1, h2 }
 237     ensures  { heaps result }
 238     ensures  { inv k result }
 239     ensures  { forall x. occ x result = occ x h1 + occ x h2 }
 240     =
 241     match h1, h2 with
 242     | Nil, _ -> h2
 243     | _, Nil -> h1
 244     | Cons t1 tl1, Cons t2 tl2 ->
 245         if rank t1 < rank t2 then
 246           Cons t1 (merge (rank t1 + 1) tl1 h2)
 247         else if rank t2 < rank t1 then
 248           Cons t2 (merge (rank t2 + 1) h1 tl2)
 249         else
 250           add_tree (link t1 t2) (merge (rank t1 + 1) tl1 tl2)
 251     end
 252
 253   let rec extract_min_tree (ghost k: int) (h: heap) : (tree, heap)
 254     requires { heaps h }
 255     requires { inv k h }
 256     requires { h <> Nil }
 257     variant  { h }
 258     ensures  { let t, h' = result in
 259                heaps (Cons t Nil) && heaps h' && inv k h' &&
 260                le_roots t.elem h && binomial_tree t &&
 261                forall x. occ x h = occ x (Cons t Nil) + occ x h' }
 262     =
 263     match h with
 264     | Nil ->
 265         absurd
 266     | Cons t Nil ->
 267         t, Nil
 268     | Cons t tl ->
 269         let t', tl' = extract_min_tree (rank t + 1) tl in
 270         if le t.elem t'.elem then t, tl else t', Cons t tl'
 271     end
 272
 273   let rec extract_min (h: heap) : (elt, heap)
 274     requires { heaps h }
 275     requires { inv 0 h }
 276     requires { h <> Nil }
 277     variant  { h }
 278     ensures  { let e, h' = result in
 279                heaps h' && inv 0 h' &&
 280                occ e h' = occ e h - 1 &&
 281                forall x. x <> e -> occ x h' = occ x h }
 282     =
 283     let t, h' = extract_min_tree 0 h in
 284     t.elem, merge 0 (reverse t.children) h'
 285
 286   (** Complexity analysis. *)
 287
 288   use int.Power
 289
 290   let rec lemma has_order_size (k: int) (l: list tree)
 291     requires { has_order k l }
 292     variant  { size l }
 293     ensures  { size l = power 2 k - 1 }
 294   = match l with
 295     | Nil -> ()
 296     | Cons { children = c } r -> has_order_size (k-1) c; has_order_size (k-1) r
 297     end
 298
 299   lemma binomial_tree_size:
 300     forall t. binomial_tree t -> size t.children = power 2 t.rank - 1
 301
 302   let rec lemma inv_size (k: int) (l: list tree)
 303     requires { 0 <= k }
 304     requires { inv k l }
 305     variant  { l }
 306     ensures  { size l >= power 2 (k + length l) - power 2 k }
 307   = match l with
 308     | Nil -> ()
 309     | Cons _ r -> inv_size (k+1) r
 310     end
 311
 312   (** Finally we prove that the number of binomial trees is O(log n) *)
 313
 314   lemma heap_size:
 315     forall h. inv 0 h -> size h >= power 2 (length h) - 1
 316
 317 end