examples/tree_height.mlw

   1
   2 (** Computing the height of a tree in CPS style
   3     (author: Jean-Christophe Filliâtre) *)
   4
   5 module HeightCPS
   6
   7   use int.Int
   8   use int.MinMax
   9   use bintree.Tree
  10   use bintree.Height
  11
  12   let rec height_cps (t: tree 'a) (k: int -> 'b) : 'b
  13     variant { t }
  14     ensures { result = k (height t) }
  15   = match t with
  16     | Empty -> k 0
  17     | Node l _ r ->
  18         height_cps l (fun hl ->
  19         height_cps r (fun hr ->
  20         k (1 + max hl hr)))
  21     end
  22
  23   let height (t: tree 'a) : int
  24     ensures { result = height t }
  25   = height_cps t (fun h -> h)
  26
  27 end
  28
  29 (** with a while loop, manually obtained by compiling out recursion *)
  30
  31 module Iteration
  32
  33   use int.Int
  34   use int.MinMax
  35   use list.List
  36   use bintree.Tree
  37   use bintree.Size
  38   use bintree.Height
  39   use ref.Ref
  40
  41   type cont 'a = Id | Kleft (tree 'a) (cont 'a) | Kright int (cont 'a)
  42
  43   type what 'a = Argument (tree 'a) | Result int
  44
  45   let predicate is_id (k: cont 'a) =
  46     match k with Id -> true | _ -> false end
  47
  48   let predicate is_result (w: what 'a) =
  49     match w with Result _ -> true | _ -> false end
  50
  51   function evalk (k: cont 'a) (r: int) : int =
  52     match k with
  53     | Id         -> r
  54     | Kleft  l k -> evalk k (1 + max (height l) r)
  55     | Kright x k -> evalk k (1 + max x r)
  56     end
  57
  58   function evalw (w: what 'a) : int =
  59     match w with
  60     | Argument t -> height t
  61     | Result   x -> x
  62     end
  63
  64   function sizek (k: cont 'a) : int =
  65     match k with
  66     | Id         -> 0
  67     | Kleft  t k -> 3 + 4 * size t + sizek k
  68     | Kright _ k -> 1 + sizek k
  69     end
  70
  71   lemma sizek_nonneg: forall k: cont 'a. sizek k >= 0
  72
  73   function sizew (w: what 'a) : int =
  74     match w with
  75     | Argument t -> 1 + 4 * size t
  76     | Result   _ -> 0
  77     end
  78
  79   lemma helper1: forall t: tree 'a. 4 * size t >= 0
  80   lemma sizew_nonneg: forall w: what 'a. sizew w >= 0
  81
  82   let height1 (t: tree 'a) : int
  83     ensures { result = height t }
  84   =
  85     let w = ref (Argument t) in
  86     let k = ref Id in
  87     while not (is_id !k && is_result !w) do
  88       invariant { evalk !k (evalw !w) = height t }
  89       variant   { sizek !k + sizew !w }
  90       match !w, !k with
  91       | Argument Empty,        _ -> w := Result 0
  92       | Argument (Node l _ r), _ -> w := Argument l; k := Kleft r !k
  93       | Result _, Id             -> absurd
  94       | Result v, Kleft r k0     -> w := Argument r; k := Kright v k0
  95       | Result v, Kright hl k0   -> w := Result (1 + max hl v); k := k0
  96       end
  97     done;
  98     match !w with Result r -> r | _ -> absurd end
  99
 100 end
 101
 102 (** Computing the height of a tree with an explicit stack
 103     (code: Andrei Paskevich / proof: Jean-Christophe Filliâtre) *)
 104
 105 module HeightStack
 106
 107   use int.Int
 108   use int.MinMax
 109   use list.List
 110   use bintree.Tree
 111   use bintree.Size
 112   use bintree.Height
 113
 114   type stack 'a = list (int, tree 'a)
 115
 116   function heights (s: stack 'a) : int =
 117     match s with
 118     | Nil            -> 0
 119     | Cons (h, t) s' -> max (h + height t) (heights s')
 120     end
 121
 122   function sizes (s: stack 'a) : int =
 123     match s with
 124     | Nil            -> 0
 125     | Cons (_, t) s' -> size t + sizes s'
 126     end
 127
 128   lemma sizes_nonneg: forall s: stack 'a. sizes s >= 0
 129
 130   let rec height_stack (m: int) (s: stack 'a) : int
 131     requires { m >= 0 }
 132     variant  { sizes s, s }
 133     ensures  { result = max m (heights s) }
 134   = match s with
 135     | Nil                     -> m
 136     | Cons (h, Empty) s'      -> height_stack (max m h) s'
 137     | Cons (h, Node l _ r) s' -> height_stack m (Cons (h+1,l) (Cons (h+1,r) s'))
 138    end
 139
 140   let height1 (t: tree 'a) : int
 141     ensures { result = height t }
 142   = height_stack 0 (Cons (0, t) Nil)
 143
 144 end
 145
 146 (** Computing the height of a tree with a small amount of memory:
 147     Stack size is only proportional to the logarithm of the tree size.
 148     (author: Martin Clochard) *)
 149
 150 module HeightSmallSpace
 151
 152   use int.Int
 153   use int.MinMax
 154   use int.ComputerDivision
 155   use option.Option
 156   use bintree.Tree
 157   use bintree.Size
 158   use bintree.Height
 159
 160   (** Count number of leaves in a tree. *)
 161   function leaves (t: tree 'a) : int = 1 + size t
 162
 163   (** `height_limited acc depth lim t`:
 164        Compute the `height t` if the number of leaves in `t` is at most `lim`,
 165          fails otherwise. `acc` and `depth` are accumulators.
 166          For maintaining the limit within the recursion, this routine
 167          also send back the difference between the number of leaves and
 168          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          of the recursive call for that child and make a recursive tail-call
 173          for the other child, using the computed difference in order to
 174          update `lim`. Since non-tail-recursive calls halve the limit,
 175          the space complexity is logarithmic in `lim`.
 176        Note that as is, this has a degenerate case:
 177          if the small child is extremely small, we may waste a lot
 178          of computing time on the large child to notice it is large,
 179          while in the end processing only the small child until the
 180          tail-recursive call. Analysis shows that this results in
 181          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          in increasing order (see process_small_child subroutine), until
 184          one succeed or maximal limits both fails. This way,
 185          the time spent by a single phase of the algorithm is representative
 186          of the size of the processed set of nodes.
 187          Time complexity: open
 188    *)
 189   let rec height_limited (acc depth lim: int) (t:tree 'a) : option (int,int)
 190     requires { 0 < lim /\ 0 <= acc }
 191     returns  { None -> leaves t > lim
 192       | Some (res,dl) -> res = max acc (depth + height t)
 193                          /\ lim = leaves t + dl /\ 0 <= dl }
 194     variant { lim }
 195   = match t with
 196     | Empty -> Some (max acc depth,lim-1)
 197     | Node l _ r ->
 198       let rec process_small_child (limc: int) : option (int,int,tree 'a)
 199         requires { 0 <= limc < lim }
 200         returns  { None -> leaves l > limc /\ leaves r > limc
 201           | Some (h,sz,rm) -> height t = 1 + max h (height rm)
 202                               /\ leaves t = leaves rm + sz
 203                               /\ 0 < sz <= limc }
 204         variant { limc }
 205       = if limc = 0 then None else
 206         match process_small_child (div limc 2) with
 207         | (Some _) as s -> s
 208         | None -> match height_limited 0 0 limc l with
 209         | Some (h,dl) -> Some (h,limc-dl,r)
 210         | None -> match height_limited 0 0 limc r with
 211         | Some (h,dl) -> Some (h,limc-dl,l)
 212         | None -> None
 213         end end end
 214       in
 215       let limc = div lim 2 in
 216       match process_small_child limc with
 217       | None -> None
 218       | Some (h,sz,rm) ->
 219         height_limited (max acc (depth + h + 1)) (depth+1) (lim-sz) rm
 220       end
 221     end
 222
 223   use ref.Ref
 224
 225   let height (t: tree 'a) : int
 226     ensures { result = height t }
 227   = let lim = ref 1 in
 228     while true do
 229       invariant { !lim > 0 }
 230       variant { leaves t - !lim }
 231       match height_limited 0 0 !lim t with
 232       | None -> lim := !lim * 2
 233       | Some (h,_) -> return h
 234       end
 235     done; absurd
 236
 237
 238 end