binomial_heap.mlw 8.67 KB
 Jean-Christophe Filliâtre committed Mar 31, 2016 1 `````` `````` Jean-Christophe Filliâtre committed Apr 03, 2016 2 3 4 ``````(** Binomial heaps (Jean Vuillemin, 1978). Purely applicative implementation, following Okasaki's implementation `````` Jean-Christophe Filliâtre committed Apr 03, 2016 5 `````` in his book "Purely Functional Data Structures" (Section 3.2). `````` Jean-Christophe Filliâtre committed Mar 31, 2016 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 `````` Jean-Christophe Filliâtre committed Apr 03, 2016 16 17 18 `````` use import list.Append (** The type of elements, together with a total pre-order *) `````` Jean-Christophe Filliâtre committed Mar 31, 2016 19 20 21 `````` type elt `````` Guillaume Melquiond committed Jun 16, 2016 22 `````` val predicate le elt elt `````` Andrei Paskevich committed Jun 14, 2018 23 `````` clone relations.TotalPreOrder with type t = elt, predicate rel = le, axiom . `````` Jean-Christophe Filliâtre committed Mar 31, 2016 24 `````` `````` Jean-Christophe Filliâtre committed Apr 03, 2016 25 26 27 `````` (** Trees. These are arbitrary trees, not yet constrained `````` Guillaume Melquiond committed Jun 13, 2018 28 `````` to be binomial trees. Field `rank` is used later to store the rank `````` Jean-Christophe Filliâtre committed Apr 03, 2016 29 30 `````` of the binomial tree, for access in constant time. *) `````` Jean-Christophe Filliâtre committed Mar 31, 2016 31 `````` type tree = { `````` Jean-Christophe Filliâtre committed Apr 03, 2016 32 `````` elem: elt; `````` Jean-Christophe Filliâtre committed Mar 31, 2016 33 `````` children: list tree; `````` Jean-Christophe Filliâtre committed Apr 03, 2016 34 `````` rank: int; `````` Jean-Christophe Filliâtre committed Mar 31, 2016 35 36 `````` } `````` Jean-Christophe Filliâtre committed Apr 03, 2016 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 `````` Jean-Christophe Filliâtre committed Apr 03, 2016 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 `````` Jean-Christophe Filliâtre committed Apr 03, 2016 50 51 52 `````` (** Heaps. *) `````` Guillaume Melquiond committed Jun 13, 2018 53 `````` (* `e` is no greater than the roots of the trees in `l` *) `````` Jean-Christophe Filliâtre committed Mar 31, 2016 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 `````` Jean-Christophe Filliâtre committed Apr 01, 2016 65 66 `````` | Nil -> true | Cons { elem = e; children = c } r -> le_roots e c && heaps c && heaps r `````` Jean-Christophe Filliâtre committed Mar 31, 2016 67 68 `````` end `````` Jean-Christophe Filliâtre committed Apr 03, 2016 69 `````` lemma heaps_append: `````` Guillaume Melquiond committed Jan 12, 2018 70 `````` forall h1 [@induction] h2. heaps h1 -> heaps h2 -> heaps (h1 ++ h2) `````` Jean-Christophe Filliâtre committed Mar 31, 2016 71 72 73 `````` lemma heaps_reverse: forall h. heaps h -> heaps (reverse h) `````` Jean-Christophe Filliâtre committed Apr 03, 2016 74 `````` (** Number of occurrences of a given element in a list of trees. *) `````` Jean-Christophe Filliâtre committed Mar 31, 2016 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) `````` Jean-Christophe Filliâtre committed Apr 03, 2016 84 `````` variant { size l } `````` Jean-Christophe Filliâtre committed Mar 31, 2016 85 86 `````` ensures { 0 <= occ x l } = match l with `````` Jean-Christophe Filliâtre committed Apr 03, 2016 87 88 `````` | Nil -> () | Cons { children = c } r -> occ_nonneg x c; occ_nonneg x r `````` Jean-Christophe Filliâtre committed Mar 31, 2016 89 `````` end `````` Jean-Christophe Filliâtre committed Apr 03, 2016 90 91 `````` lemma occ_append: `````` Guillaume Melquiond committed Jan 12, 2018 92 `````` forall l1 [@induction] l2 x. occ x (l1 ++ l2) = occ x l1 + occ x l2 `````` Jean-Christophe Filliâtre committed Mar 31, 2016 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 `````` Jean-Christophe Filliâtre committed Apr 03, 2016 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 `````` Guillaume Melquiond committed Jun 13, 2018 109 `````` (** Binomial tree of rank `k`. *) `````` Jean-Christophe Filliâtre committed Mar 31, 2016 110 111 112 `````` predicate has_order (k: int) (l: list tree) = match l with `````` Jean-Christophe Filliâtre committed Apr 03, 2016 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 `````` Jean-Christophe Filliâtre committed Mar 31, 2016 117 118 `````` end `````` Jean-Christophe Filliâtre committed Apr 01, 2016 119 `````` predicate binomial_tree (t: tree) = `````` Jean-Christophe Filliâtre committed Apr 01, 2016 120 121 `````` t.rank = length t.children && has_order t.rank t.children `````` Jean-Christophe Filliâtre committed Mar 31, 2016 122 `````` `````` Jean-Christophe Filliâtre committed Apr 03, 2016 123 124 125 126 127 `````` lemma has_order_length: forall l k. has_order k l -> length l = k (** Binomial heaps. *) `````` Jean-Christophe Filliâtre committed Mar 31, 2016 128 129 `````` type heap = list tree `````` Guillaume Melquiond committed Jun 13, 2018 130 131 `````` (** A heap `h` is a list of binomial trees in strict increasing order of ranks, those ranks being no smaller than `m`. *) `````` Jean-Christophe Filliâtre committed Apr 03, 2016 132 `````` `````` Jean-Christophe Filliâtre committed Apr 01, 2016 133 134 135 `````` predicate inv (m: int) (h: heap) = match h with | Nil -> true `````` Jean-Christophe Filliâtre committed Apr 01, 2016 136 `````` | Cons t r -> let k = t.rank in m <= k && binomial_tree t && inv (k + 1) r `````` Jean-Christophe Filliâtre committed Apr 01, 2016 137 138 `````` end `````` Jean-Christophe Filliâtre committed Apr 03, 2016 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. *) `````` Jean-Christophe Filliâtre committed Mar 31, 2016 161 162 163 `````` let empty () : heap ensures { heaps result } `````` Jean-Christophe Filliâtre committed Apr 01, 2016 164 `````` ensures { inv 0 result } `````` Jean-Christophe Filliâtre committed Mar 31, 2016 165 `````` ensures { forall e. not (mem e result) } `````` Jean-Christophe Filliâtre committed Apr 01, 2016 166 167 `````` = Nil `````` Jean-Christophe Filliâtre committed Mar 31, 2016 168 169 `````` let is_empty (h: heap) : bool `````` Jean-Christophe Filliâtre committed Apr 01, 2016 170 `````` ensures { result <-> h = Nil } `````` Guillaume Melquiond committed Jun 16, 2016 171 `````` = match h with Nil -> true | _ -> false end `````` Jean-Christophe Filliâtre committed Mar 31, 2016 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 } `````` Jean-Christophe Filliâtre committed Apr 01, 2016 178 `````` = `````` Jean-Christophe Filliâtre committed Mar 31, 2016 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 `````` Guillaume Melquiond committed Jun 16, 2016 195 `````` let function link (t1 t2: tree) : tree = `````` Jean-Christophe Filliâtre committed Apr 03, 2016 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 } `````` Jean-Christophe Filliâtre committed Mar 31, 2016 201 202 `````` let rec add_tree (t: tree) (h: heap) requires { heaps (Cons t Nil) } `````` Jean-Christophe Filliâtre committed Apr 01, 2016 203 `````` requires { binomial_tree t } `````` Jean-Christophe Filliâtre committed Mar 31, 2016 204 `````` requires { heaps h } `````` Jean-Christophe Filliâtre committed Apr 01, 2016 205 `````` requires { inv (rank t) h } `````` Jean-Christophe Filliâtre committed Mar 31, 2016 206 207 `````` variant { h } ensures { heaps result } `````` Jean-Christophe Filliâtre committed Apr 01, 2016 208 `````` ensures { inv (rank t) result } `````` Jean-Christophe Filliâtre committed Mar 31, 2016 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 `````` Jean-Christophe Filliâtre committed Apr 01, 2016 217 218 `````` else begin assert { rank t = rank hd }; `````` Jean-Christophe Filliâtre committed Mar 31, 2016 219 `````` add_tree (link t hd) tl `````` Jean-Christophe Filliâtre committed Apr 01, 2016 220 `````` end `````` Jean-Christophe Filliâtre committed Mar 31, 2016 221 222 223 224 `````` end let add (x: elt) (h: heap) : heap requires { heaps h } `````` Jean-Christophe Filliâtre committed Apr 01, 2016 225 `````` requires { inv 0 h } `````` Jean-Christophe Filliâtre committed Mar 31, 2016 226 `````` ensures { heaps result } `````` Jean-Christophe Filliâtre committed Apr 01, 2016 227 `````` ensures { inv 0 result } `````` Jean-Christophe Filliâtre committed Mar 31, 2016 228 229 `````` ensures { occ x result = occ x h + 1 } ensures { forall e. e <> x -> occ e result = occ e h } `````` Jean-Christophe Filliâtre committed Apr 01, 2016 230 `````` = `````` Jean-Christophe Filliâtre committed Apr 01, 2016 231 `````` add_tree { elem = x; rank = 0; children = Nil } h `````` Jean-Christophe Filliâtre committed Mar 31, 2016 232 `````` `````` Jean-Christophe Filliâtre committed Apr 01, 2016 233 `````` let rec merge (ghost k: int) (h1 h2: heap) `````` Jean-Christophe Filliâtre committed Mar 31, 2016 234 `````` requires { heaps h1 } `````` Jean-Christophe Filliâtre committed Apr 01, 2016 235 `````` requires { inv k h1 } `````` Jean-Christophe Filliâtre committed Mar 31, 2016 236 `````` requires { heaps h2 } `````` Jean-Christophe Filliâtre committed Apr 01, 2016 237 238 `````` requires { inv k h2 } variant { h1, h2 } `````` Jean-Christophe Filliâtre committed Mar 31, 2016 239 `````` ensures { heaps result } `````` Jean-Christophe Filliâtre committed Apr 01, 2016 240 `````` ensures { inv k result } `````` Jean-Christophe Filliâtre committed Mar 31, 2016 241 `````` ensures { forall x. occ x result = occ x h1 + occ x h2 } `````` Jean-Christophe Filliâtre committed Apr 01, 2016 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) `````` Jean-Christophe Filliâtre committed Mar 31, 2016 253 254 `````` end `````` Jean-Christophe Filliâtre committed Apr 01, 2016 255 `````` let rec extract_min_tree (ghost k: int) (h: heap) : (tree, heap) `````` Jean-Christophe Filliâtre committed Mar 31, 2016 256 `````` requires { heaps h } `````` Jean-Christophe Filliâtre committed Apr 01, 2016 257 `````` requires { inv k h } `````` Jean-Christophe Filliâtre committed Mar 31, 2016 258 259 `````` requires { h <> Nil } variant { h } `````` Andrei Paskevich committed Jun 11, 2017 260 `````` ensures { let t, h' = result in `````` Jean-Christophe Filliâtre committed Apr 01, 2016 261 262 `````` heaps (Cons t Nil) && heaps h' && inv k h' && le_roots t.elem h && binomial_tree t && `````` Jean-Christophe Filliâtre committed Mar 31, 2016 263 `````` forall x. occ x h = occ x (Cons t Nil) + occ x h' } `````` Jean-Christophe Filliâtre committed Apr 01, 2016 264 265 `````` = match h with `````` Jean-Christophe Filliâtre committed Mar 31, 2016 266 267 268 `````` | Nil -> absurd | Cons t Nil -> `````` Andrei Paskevich committed Jun 11, 2017 269 `````` t, Nil `````` Jean-Christophe Filliâtre committed Mar 31, 2016 270 `````` | Cons t tl -> `````` Andrei Paskevich committed Jun 11, 2017 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' `````` Jean-Christophe Filliâtre committed Mar 31, 2016 273 274 275 276 `````` end let rec extract_min (h: heap) : (elt, heap) requires { heaps h } `````` Jean-Christophe Filliâtre committed Apr 01, 2016 277 `````` requires { inv 0 h } `````` Jean-Christophe Filliâtre committed Mar 31, 2016 278 279 `````` requires { h <> Nil } variant { h } `````` Andrei Paskevich committed Jun 11, 2017 280 `````` ensures { let e, h' = result in `````` Jean-Christophe Filliâtre committed Apr 01, 2016 281 `````` heaps h' && inv 0 h' && `````` Jean-Christophe Filliâtre committed Mar 31, 2016 282 283 `````` occ e h' = occ e h - 1 && forall x. x <> e -> occ x h' = occ x h } `````` Jean-Christophe Filliâtre committed Apr 01, 2016 284 `````` = `````` Andrei Paskevich committed Jun 11, 2017 285 286 `````` let t, h' = extract_min_tree 0 h in t.elem, merge 0 (reverse t.children) h' `````` Jean-Christophe Filliâtre committed Apr 01, 2016 287 `````` `````` Jean-Christophe Filliâtre committed Apr 03, 2016 288 `````` (** Complexity analysis. *) `````` Jean-Christophe Filliâtre committed Apr 01, 2016 289 290 291 `````` use import int.Power `````` Jean-Christophe Filliâtre committed Apr 03, 2016 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 `````` Jean-Christophe Filliâtre committed Apr 01, 2016 299 300 301 `````` end lemma binomial_tree_size: `````` Jean-Christophe Filliâtre committed Apr 03, 2016 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) *) `````` Jean-Christophe Filliâtre committed Apr 01, 2016 315 `````` `````` Jean-Christophe Filliâtre committed Apr 03, 2016 316 317 `````` lemma heap_size: forall h. inv 0 h -> size h >= power 2 (length h) - 1 `````` Jean-Christophe Filliâtre committed Mar 31, 2016 318 319 `````` end``````