tree_height.mlw 7.09 KB
Newer Older
1 2 3 4 5 6

(** Computing the height of a tree in CPS style
    (author: Jean-Christophe Filliâtre) *)

module HeightCPS

7 8 9 10
  use int.Int
  use int.MinMax
  use bintree.Tree
  use bintree.Height
11

12
  let rec height_cps (t: tree 'a) (k: int -> 'b) : 'b
Mário Pereira's avatar
Mário Pereira committed
13
    variant { t }
14
    ensures { result = k (height t) }
Mário Pereira's avatar
Mário Pereira committed
15
  = match t with
16 17
    | Empty -> k 0
    | Node l _ r ->
18 19
        height_cps l (fun hl ->
        height_cps r (fun hr ->
20 21 22
        k (1 + max hl hr)))
    end

23 24 25
  let height (t: tree 'a) : int
    ensures { result = height t }
  = height_cps t (fun h -> h)
26 27 28

end

29 30 31 32
(** with a while loop, manually obtained by compiling out recursion *)

module Iteration

33 34 35 36 37 38 39
  use int.Int
  use int.MinMax
  use list.List
  use bintree.Tree
  use bintree.Size
  use bintree.Height
  use ref.Ref
40 41 42 43 44

  type cont 'a = Id | Kleft (tree 'a) (cont 'a) | Kright int (cont 'a)

  type what 'a = Argument (tree 'a) | Result int

45
  let predicate is_id (k: cont 'a) =
46 47
    match k with Id -> true | _ -> false end

48
  let predicate is_result (w: what 'a) =
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 74 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
    match w with Result _ -> true | _ -> false end

  function evalk (k: cont 'a) (r: int) : int =
    match k with
    | Id         -> r
    | Kleft  l k -> evalk k (1 + max (height l) r)
    | Kright x k -> evalk k (1 + max x r)
    end

  function evalw (w: what 'a) : int =
    match w with
    | Argument t -> height t
    | Result   x -> x
    end

  function sizek (k: cont 'a) : int =
    match k with
    | Id         -> 0
    | Kleft  t k -> 3 + 4 * size t + sizek k
    | Kright _ k -> 1 + sizek k
    end

  lemma sizek_nonneg: forall k: cont 'a. sizek k >= 0

  function sizew (w: what 'a) : int =
    match w with
    | Argument t -> 1 + 4 * size t
    | Result   _ -> 0
    end

  lemma helper1: forall t: tree 'a. 4 * size t >= 0
  lemma sizew_nonneg: forall w: what 'a. sizew w >= 0

  let height1 (t: tree 'a) : int
    ensures { result = height t }
  =
    let w = ref (Argument t) in
    let k = ref Id in
    while not (is_id !k && is_result !w) do
      invariant { evalk !k (evalw !w) = height t }
      variant   { sizek !k + sizew !w }
      match !w, !k with
      | Argument Empty,        _ -> w := Result 0
      | Argument (Node l _ r), _ -> w := Argument l; k := Kleft r !k
      | Result _, Id             -> absurd
      | Result v, Kleft r k0     -> w := Argument r; k := Kright v k0
      | Result v, Kright hl k0   -> w := Result (1 + max hl v); k := k0
      end
    done;
    match !w with Result r -> r | _ -> absurd end

end

102 103 104 105 106
(** Computing the height of a tree with an explicit stack
    (code: Andrei Paskevich / proof: Jean-Christophe Filliâtre) *)

module HeightStack

107 108 109 110 111 112
  use int.Int
  use int.MinMax
  use list.List
  use bintree.Tree
  use bintree.Size
  use bintree.Height
113 114 115 116 117 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 144

  type stack 'a = list (int, tree 'a)

  function heights (s: stack 'a) : int =
    match s with
    | Nil            -> 0
    | Cons (h, t) s' -> max (h + height t) (heights s')
    end

  function sizes (s: stack 'a) : int =
    match s with
    | Nil            -> 0
    | Cons (_, t) s' -> size t + sizes s'
    end

  lemma sizes_nonneg: forall s: stack 'a. sizes s >= 0

  let rec height_stack (m: int) (s: stack 'a) : int
    requires { m >= 0 }
    variant  { sizes s, s }
    ensures  { result = max m (heights s) }
  = match s with
    | Nil                     -> m
    | Cons (h, Empty) s'      -> height_stack (max m h) s'
    | Cons (h, Node l _ r) s' -> height_stack m (Cons (h+1,l) (Cons (h+1,r) s'))
   end

  let height1 (t: tree 'a) : int
    ensures { result = height t }
  = height_stack 0 (Cons (0, t) Nil)

end
145 146 147 148 149 150 151

(** Computing the height of a tree with a small amount of memory:
    Stack size is only proportional to the logarithm of the tree size.
    (author: Martin Clochard) *)

module HeightSmallSpace

152 153 154 155 156 157 158
  use int.Int
  use int.MinMax
  use int.ComputerDivision
  use option.Option
  use bintree.Tree
  use bintree.Size
  use bintree.Height
159 160 161 162

  (** Count number of leaves in a tree. *)
  function leaves (t: tree 'a) : int = 1 + size t

163 164 165
  (** `height_limited acc depth lim t`:
       Compute the `height t` if the number of leaves in `t` is at most `lim`,
         fails otherwise. `acc` and `depth` are accumulators.
166 167 168
         For maintaining the limit within the recursion, this routine
         also send back the difference between the number of leaves and
         the limit in case of success.
169
       Method: find out one child with number of leaves at most `lim/2` using
170
         recursive calls. If no such child is found, the tree has at
171
         least `lim+1` leaves, hence fails. Otherwise, accumulate the result
172 173
         of the recursive call for that child and make a recursive tail-call
         for the other child, using the computed difference in order to
174 175
         update `lim`. Since non-tail-recursive calls halve the limit,
         the space complexity is logarithmic in `lim`.
176 177 178 179 180 181
       Note that as is, this has a degenerate case:
         if the small child is extremely small, we may waste a lot
         of computing time on the large child to notice it is large,
         while in the end processing only the small child until the
         tail-recursive call. Analysis shows that this results in
         super-polynomial time behavior (recursion T(N) = T(N/2)+T(N-1))
182
       To mitigate this, we perform recursive calls on all `lim/2^k` limits
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
         in increasing order (see process_small_child subroutine), until
         one succeed or maximal limits both fails. This way,
         the time spent by a single phase of the algorithm is representative
         of the size of the processed set of nodes.
         Time complexity: open
   *)
  let rec height_limited (acc depth lim: int) (t:tree 'a) : option (int,int)
    requires { 0 < lim /\ 0 <= acc }
    returns  { None -> leaves t > lim
      | Some (res,dl) -> res = max acc (depth + height t)
                         /\ lim = leaves t + dl /\ 0 <= dl }
    variant { lim }
  = match t with
    | Empty -> Some (max acc depth,lim-1)
    | Node l _ r ->
      let rec process_small_child (limc: int) : option (int,int,tree 'a)
        requires { 0 <= limc < lim }
        returns  { None -> leaves l > limc /\ leaves r > limc
          | Some (h,sz,rm) -> height t = 1 + max h (height rm)
                              /\ leaves t = leaves rm + sz
                              /\ 0 < sz <= limc }
        variant { limc }
      = if limc = 0 then None else
        match process_small_child (div limc 2) with
        | (Some _) as s -> s
        | None -> match height_limited 0 0 limc l with
        | Some (h,dl) -> Some (h,limc-dl,r)
        | None -> match height_limited 0 0 limc r with
        | Some (h,dl) -> Some (h,limc-dl,l)
        | None -> None
        end end end
      in
      let limc = div lim 2 in
      match process_small_child limc with
      | None -> None
      | Some (h,sz,rm) ->
        height_limited (max acc (depth + h + 1)) (depth+1) (lim-sz) rm
      end
    end

223
  use ref.Ref
224 225 226 227 228 229 230 231 232 233 234 235 236 237 238

  let height (t: tree 'a) : int
    ensures { result = height t }
  = let lim = ref 1 in
    while true do
      invariant { !lim > 0 }
      variant { leaves t - !lim }
      match height_limited 0 0 !lim t with
      | None -> lim := !lim * 2
      | Some (h,_) -> return h
      end
    done; absurd


end