binomial_heap.mlw 8.67 KB
Newer Older
1

2
3
4
(** Binomial heaps (Jean Vuillemin, 1978).

    Purely applicative implementation, following Okasaki's implementation
5
    in his book "Purely Functional Data Structures" (Section 3.2).
6
7
8
9
10
11
12
13
14
15

    Author: Jean-Christophe Filliâtre (CNRS)
*)

module BinomialHeap

  use import int.Int
  use import list.List
  use import list.Length
  use import list.Reverse
16
17
18
  use import list.Append

  (** The type of elements, together with a total pre-order *)
19
20
21

  type elt

22
  val predicate le elt elt
23
  clone relations.TotalPreOrder with type t = elt, predicate rel = le, axiom .
24

25
26
27
  (** Trees.

      These are arbitrary trees, not yet constrained
28
      to be binomial trees. Field `rank` is used later to store the rank
29
30
      of the binomial tree, for access in constant time. *)

31
  type tree = {
32
        elem: elt;
33
    children: list tree;
34
        rank: int;
35
36
  }

37
38
39
40
41
42
  function size (l: list tree) : int =
    match l with
    | Nil                     -> 0
    | Cons { children = c } r -> 1 + size c + size r
    end

43
44
45
46
47
48
49
  let lemma size_nonnneg (l: list tree)
    ensures { size l >= 0 }
  = let rec auxl (l: list tree) ensures { size l >= 0 } variant { l }
    = match l with Nil -> () | Cons t r -> auxt t; auxl r end
    with auxt (t: tree) ensures { size t.children >= 0 } variant { t }
    = match t with { children = c } -> auxl c end in
    auxl l
50
51
52

  (** Heaps. *)

53
  (* `e` is no greater than the roots of the trees in `l` *)
54
55
56
57
58
59
60
61
62
63
64
  predicate le_roots (e: elt) (l: list tree) =
    match l with
    | Nil      -> true
    | Cons t r -> le e t.elem && le_roots e r
    end

  lemma le_roots_trans:
    forall x y l. le x y -> le_roots y l -> le_roots x l

  predicate heaps (l: list tree) =
    match l with
65
66
    | Nil                               -> true
    | Cons { elem = e; children = c } r -> le_roots e c && heaps c && heaps r
67
68
    end

69
  lemma heaps_append:
70
    forall h1 [@induction] h2. heaps h1 -> heaps h2 -> heaps (h1 ++ h2)
71
72
73
  lemma heaps_reverse:
    forall h. heaps h -> heaps (reverse h)

74
  (** Number of occurrences of a given element in a list of trees. *)
75
76
77
78
79
80
81
82
83

  function occ (x: elt) (l: list tree) : int =
    match l with
    | Nil      -> 0
    | Cons { elem = y; children = c } r ->
       (if x = y then 1 else 0) + occ x c + occ x r
    end

  let rec lemma occ_nonneg (x: elt) (l: list tree)
84
    variant { size l }
85
86
    ensures { 0 <= occ x l }
  = match l with
87
88
    | Nil                     -> ()
    | 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
95
96
97
98
99

  lemma occ_reverse:
    forall x l. occ x l = occ x (reverse l)

  predicate mem (x: elt) (l: list tree) =
    occ x l > 0

100
101
102
103
104
105
106
107
108
  let rec lemma heaps_mem (l: list tree)
    requires { heaps l }
    variant  { size l }
    ensures  { forall x. le_roots x l -> forall y. mem y l -> le x y }
  = match l with
    | Nil                     -> ()
    | Cons { children = c } r -> heaps_mem c; heaps_mem r
    end

109
  (** Binomial tree of rank `k`. *)
110
111
112

  predicate has_order (k: int) (l: list tree) =
    match l with
113
114
115
116
    | Nil ->
        k = 0
    | Cons { rank = k'; children = c } r ->
        k' = k - 1 && has_order (k-1) c && has_order (k-1) r
117
118
    end

119
  predicate binomial_tree (t: tree) =
120
121
    t.rank = length t.children &&
    has_order t.rank t.children
122

123
124
125
126
127
  lemma has_order_length:
    forall l k. has_order k l -> length l = k

  (** Binomial heaps. *)

128
129
  type heap = list tree

130
131
  (** A heap `h` is a list of binomial trees in strict increasing order of
      ranks, those ranks being no smaller than `m`. *)
132

133
134
135
  predicate inv (m: int) (h: heap) =
    match h with
    | Nil -> true
136
    | Cons t r -> let k = t.rank in m <= k && binomial_tree t && inv (k + 1) r
137
138
    end

139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
  lemma inv_trans:
    forall m1 m2 h. m1 <= m2 -> inv m2 h -> inv m1 h

  let lemma inv_reverse (t: tree)
    requires { binomial_tree t }
    ensures  { inv 0 (reverse t.children) }
  = let rec aux (k: int) (l: list tree) (acc: list tree)
      requires { has_order k l }
      requires { inv k acc }
      variant  { k }
      ensures  { inv 0 (reverse l ++ acc) }
    = match l with
      | Nil -> ()
      | Cons t r ->
          assert { binomial_tree t };
          aux (k-1) r (Cons t acc)
      end in
    match t with
    | { rank = k; children = c } -> aux k c Nil
    end

  (** Heap operations. *)
161
162
163

  let empty () : heap
    ensures { heaps result }
164
    ensures { inv 0 result }
165
    ensures { forall e. not (mem e result) }
166
167
    =
    Nil
168
169

  let is_empty (h: heap) : bool
170
    ensures { result <-> h = Nil }
171
  = match h with Nil -> true | _ -> false end
172
173
174
175
176
177

  let get_min (h: heap) : elt
    requires { heaps h }
    requires { h <> Nil }
    ensures  { mem result h }
    ensures  { forall x. mem x h -> le result x }
178
    =
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
    match h with
      | Nil      -> absurd
      | Cons t l ->
          let rec aux (m: elt) (l: list tree) : elt
            requires { heaps l }
            variant  { l }
            ensures  { result = m || mem result l }
            ensures  { le result m }
            ensures  { forall x. mem x l -> le result x }
          = match l with
          | Nil             -> m
          | Cons {elem=x} r -> aux (if le x m then x else m) r
          end in
          aux t.elem l
    end

195
  let function link (t1 t2: tree) : tree =
196
197
198
199
200
    if le t1.elem t2.elem then
      { elem = t1.elem; rank = t1.rank + 1; children = Cons t2 t1.children }
    else
      { elem = t2.elem; rank = t2.rank + 1; children = Cons t1 t2.children }

201
202
  let rec add_tree (t: tree) (h: heap)
    requires { heaps (Cons t Nil) }
203
    requires { binomial_tree t }
204
    requires { heaps h }
205
    requires { inv (rank t) h }
206
207
    variant  { h }
    ensures  { heaps result }
208
    ensures  { inv (rank t) result }
209
210
211
212
213
214
215
216
    ensures  { forall x. occ x result = occ x (Cons t Nil) + occ x h }
    =
    match h with
    | Nil ->
        Cons t Nil
    | Cons hd tl ->
        if rank t < rank hd then
          Cons t h
217
218
        else begin
          assert { rank t = rank hd };
219
          add_tree (link t hd) tl
220
        end
221
222
223
224
    end

  let add (x: elt) (h: heap) : heap
    requires { heaps h }
225
    requires { inv 0 h }
226
    ensures  { heaps result }
227
    ensures  { inv 0 result }
228
229
    ensures  { occ x result = occ x h + 1 }
    ensures  { forall e. e <> x -> occ e result = occ e h }
230
    =
231
    add_tree { elem = x; rank = 0; children = Nil } h
232

233
  let rec merge (ghost k: int) (h1 h2: heap)
234
    requires { heaps h1 }
235
    requires { inv k h1 }
236
    requires { heaps h2 }
237
238
    requires { inv k h2 }
    variant  { h1, h2 }
239
    ensures  { heaps result }
240
    ensures  { inv k result }
241
    ensures  { forall x. occ x result = occ x h1 + occ x h2 }
242
243
244
245
246
247
248
249
250
251
252
    =
    match h1, h2 with
    | Nil, _ -> h2
    | _, Nil -> h1
    | Cons t1 tl1, Cons t2 tl2 ->
        if rank t1 < rank t2 then
          Cons t1 (merge (rank t1 + 1) tl1 h2)
        else if rank t2 < rank t1 then
          Cons t2 (merge (rank t2 + 1) h1 tl2)
        else
          add_tree (link t1 t2) (merge (rank t1 + 1) tl1 tl2)
253
254
    end

255
  let rec extract_min_tree (ghost k: int) (h: heap) : (tree, heap)
256
    requires { heaps h }
257
    requires { inv k h }
258
259
    requires { h <> Nil }
    variant  { h }
260
    ensures  { let t, h' = result in
261
262
               heaps (Cons t Nil) && heaps h' && inv k h' &&
               le_roots t.elem h && binomial_tree t &&
263
               forall x. occ x h = occ x (Cons t Nil) + occ x h' }
264
265
    =
    match h with
266
267
268
    | Nil ->
        absurd
    | Cons t Nil ->
269
        t, Nil
270
    | Cons t tl ->
271
272
        let t', tl' = extract_min_tree (rank t + 1) tl in
        if le t.elem t'.elem then t, tl else t', Cons t tl'
273
274
275
276
    end

  let rec extract_min (h: heap) : (elt, heap)
    requires { heaps h }
277
    requires { inv 0 h }
278
279
    requires { h <> Nil }
    variant  { h }
280
    ensures  { let e, h' = result in
281
               heaps h' && inv 0 h' &&
282
283
               occ e h' = occ e h - 1 &&
               forall x. x <> e -> occ x h' = occ x h }
284
    =
285
286
    let t, h' = extract_min_tree 0 h in
    t.elem, merge 0 (reverse t.children) h'
287

288
  (** Complexity analysis. *)
289
290
291

  use import int.Power

292
293
294
295
296
297
298
  let rec lemma has_order_size (k: int) (l: list tree)
    requires { has_order k l }
    variant  { size l }
    ensures  { size l = power 2 k - 1 }
  = match l with
    | Nil -> ()
    | Cons { children = c } r -> has_order_size (k-1) c; has_order_size (k-1) r
299
300
301
    end

  lemma binomial_tree_size:
302
303
304
305
306
307
308
309
310
311
312
313
314
    forall t. binomial_tree t -> size t.children = power 2 t.rank - 1

  let rec lemma inv_size (k: int) (l: list tree)
    requires { 0 <= k }
    requires { inv k l }
    variant  { l }
    ensures  { size l >= power 2 (k + length l) - power 2 k }
  = match l with
    | Nil -> ()
    | Cons _ r -> inv_size (k+1) r
    end

  (** Finally we prove that the number of binomial trees is O(log n) *)
315

316
317
  lemma heap_size:
    forall h. inv 0 h -> size h >= power 2 (length h) - 1
318
319

end