leftist_heap.mlw 5.74 KB
Newer Older
1 2 3 4 5 6 7 8 9

(** Leftist heaps (Clark Allan Crane, 1972 && Donald E. Knuth, 1973).

    Purely applicative implementation, following Okasaki's implementation
    in his book "Purely Functional Data Structures" (Section 3.1).

    Author: Mário Pereira (Université Paris Sud)
*)

10 11 12 13 14 15 16 17 18 19 20
module Heap

  use import int.Int

  type elt
  predicate le elt elt

  clone relations.TotalPreOrder with type t = elt, predicate rel = le

  type heap

21
  val function size heap : int
22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73

  function occ elt heap : int

  predicate mem (x: elt) (h: heap) = occ x h > 0

  function minimum heap : elt

  predicate is_minimum (x: elt) (h: heap) =
    mem x h && forall e. mem e h -> le x e

  axiom min_def:
    forall h. 0 < size h -> is_minimum (minimum h) h

  val empty () : heap
    ensures { size result = 0 }
    ensures { forall x. occ x result = 0 }

  val is_empty (h: heap) : bool
    ensures { result <-> size h = 0 }

  val merge (h1 h2: heap) : heap
    ensures { forall x. occ x result = occ x h1 + occ x h2 }
    ensures { size result = size h1 + size h2 }

  val insert (x: elt) (h: heap) : heap
    ensures { occ x result = occ x h + 1 }
    ensures { forall y. y <> x -> occ y h = occ y result }
    ensures { size result = size h + 1 }

  val find_min (h: heap) : elt
    requires { size h > 0 }
    ensures  { result = minimum h }

  val delete_min (h: heap) : heap
    requires { size h > 0 }
    ensures  { let x = minimum h in occ x result = occ x h - 1 }
    ensures  { forall y. y <> minimum h -> occ y result = occ y h }
    ensures  { size result = size h - 1 }

end

module TreeRank

  type tree 'a = E | N int (tree 'a) 'a (tree 'a)

end

module Size

  use import TreeRank
  use import int.Int

74
  let rec function size (t: tree 'a) : int = match t with
75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104
    | E -> 0
    | N _ l _ r -> 1 + size l + size r
    end

  lemma size_nonneg: forall t: tree 'a. 0 <= size t
  lemma size_empty: forall t: tree 'a. 0 = size t <-> t = E

end

module Occ

  use import TreeRank
  use import int.Int

  function occ (x: 'a) (t: tree 'a) : int = match t with
    | E -> 0
    | N _ l e r -> (if x = e then 1 else 0) + occ x l + occ x r
    end

  lemma occ_nonneg:
    forall x:'a, t. 0 <= occ x t

  predicate mem (x: 'a) (t: tree 'a) =
    0 < occ x t

end

module LeftistHeap

  type elt
105
  val predicate le elt elt
106 107 108 109 110 111 112 113 114 115 116
  clone relations.TotalPreOrder with type t = elt, predicate rel = le

  use import TreeRank
  use export Size
  use export Occ
  use import int.Int
  use import int.MinMax

  type t = tree elt

  (* [e] is no greater than the root of [h], if any *)
117
  let predicate le_root (e: elt) (h: t) = match h with
118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143
    | E -> true
    | N _ _ x _ -> le e x
    end

  lemma le_root_trans:
    forall x y h. le x y -> le_root y h -> le_root x h

  (* [h] is a heap *)
  predicate is_heap (h: t) = match h with
    | E -> true
    | N _ l x r -> le_root x l && is_heap l && le_root x r && is_heap r
    end

  function minimum t : elt
  axiom minimum_def: forall l x r s. minimum (N s l x r) = x

  predicate is_minimum (x: elt) (h: t) =
    mem x h && forall e. mem e h -> le x e

  let rec lemma root_is_miminum (h: t) : unit
    requires { is_heap h && 0 < size h }
    ensures  { is_minimum (minimum h) h }
    variant  { h }
  = match h with
    | E -> absurd
    | N _ l _ r ->
144 145
       match l with E -> root_is_miminum l | _ -> () end;
       match r with E -> root_is_miminum r | _ -> () end
146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171
    end

  function rank (h: t) : int = match h with
    | E -> 0
    | N _ l _ r -> 1 + min (rank l) (rank r)
    end

  predicate leftist (h: t) = match h with
    | E -> true
    | N s l _ r ->
       s = rank h &&
       leftist l && leftist r &&
       rank l >= rank r
    end

   predicate leftist_heap (h: t) =
    is_heap h && leftist h

  let empty () : t
    ensures { size result = 0 }
    ensures { forall x. occ x result = 0 }
    ensures { leftist_heap result }
  = E

  let is_empty (h: t) : bool
    ensures { result <-> size h = 0 }
172
  = match h with E -> true | N _ _ _ _ -> false end
173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235

  let rank (h: t) : int
    requires { leftist_heap h }
    ensures  { result = rank h }
  = match h with
    | E -> 0
    | N r _ _ _ -> r
    end

  let make_n (x: elt) (l r: t) : t
    requires { leftist_heap r && leftist_heap l }
    requires { le_root x l && le_root x r }
    ensures  { leftist_heap result }
    ensures  { minimum result = x }
    ensures  { size result = 1 + size l + size r }
    ensures  { occ x result = 1 + occ x l + occ x r }
    ensures  { forall y. x <> y -> occ y result = occ y l + occ y r }
  = if rank l >= rank r then N (rank r + 1) l x r
    else N (rank l + 1) r x l

  let rec merge (h1 h2: t) : t
    requires { leftist_heap h1 && leftist_heap h2 }
    ensures  { size result = size h1 + size h2 }
    ensures  { forall x. occ x result = occ x h1 + occ x h2 }
    ensures  { leftist_heap result }
    variant  { size h1 + size h2 }
  = match h1, h2 with
    | h, E | E, h -> h
    | N _ l1 x1 r1, N _ l2 x2 r2 ->
       if le x1 x2 then make_n x1 l1 (merge r1 h2)
       else make_n x2 l2 (merge h1 r2)
    end

  let insert (x: elt) (h: t) : t
    requires { leftist_heap h }
    ensures  { leftist_heap result }
    ensures  { occ x result = occ x h + 1 }
    ensures  { forall y. x <> y -> occ y result = occ y h }
    ensures  { size result = size h + 1 }
  = merge (N 1 E x E) h

  let find_min (h: t) : elt
    requires { leftist_heap h }
    requires { 0 < size h }
    ensures  { result = minimum h }
  = match h with
    | E -> absurd
    | N _ _ x _ -> x
    end

  let delete_min (h: t) : t
    requires { 0 < size h }
    requires { leftist_heap h }
    ensures  { occ (minimum h) result = occ (minimum h) h - 1 }
    ensures  { forall x. x <> minimum h -> occ x result = occ x h }
    ensures  { size result = size h - 1 }
    ensures  { leftist_heap result }
  = match h with
    | E -> absurd
    | N _ l _ r -> merge l r
    end

end