dynamic-table.timl

(* Dynamic table (amortized analysis) *)

(* This file showcases how to use TiML, more specifically the [some_output_and_cost_constraint] and [amortized_comp] datatypes below, to conduct amortized complexity analysis. *)
(* A dynamic table [1] (like the ``vector'' container in C++'s STL) is a dynamically allocated buffer that enlarges itself when the load factor becomes too high after an insertion, and shrinks itself when the load factor becomes too low after a deletion. *)

(* [1] T. H. Cormen, C. Stein, R. L. Rivest, and C. E. Leiserson.
Introduction to Algorithms. McGraw-Hill Higher Education,
2nd edition, 2001. *)

(* The main functions are [insert_delete_seq_from_good_start] and [insert_delete_seq_from_empty]. *)

functor DynamicTable (T : sig
(* num: the number of existing elements in the table 
   size: the capacity (the maximal possible number of elements) *)
  type table 'a  {Nat} {Nat}
  (* Requirement: for any table, num is not larger than capacity *)
  val table_num_le_size ['a] : forall {size num : Nat}, table 'a {size} {num} -- 1.0 --> Basic.le {num} {size}
  val alloc ['a] : forall {size : Nat}, nat {size} * 'a -- 1.0 --> table 'a {size} {0}
  val do_insert ['a] : forall {size num : Nat} {num < size}, table 'a {size} {num} ->> 'a -- 2.0 --> table 'a {size} {num + 1}
  datatype do_delete 'a {num size : Nat} = DoDelete {num' : Nat} {num = num' \/ num = num' + 1} of table 'a {size} {num'} --> do_delete 'a {size} {num}
  val do_delete ['a] : forall {size num : Nat}, table 'a {size} {num} -- 2.0 --> do_delete 'a {size} {num}
  val copy ['a] : forall {size num size' num' : Nat}, table 'a {size} {num} ->> table 'a {size'} {num'} -- 4.0 * $num + 5.0 --> table 'a {size'} {num min size'}
  val num ['a] : forall {size num : Nat}, table 'a {size} {num} -- 1.0 --> nat {num}
  val size ['a] : forall {size num : Nat}, table 'a {size} {num} -- 1.0 --> nat {size}
  val any_value ['a] : forall {size num : Nat} {size > 0}, table 'a {size} {num} -- 1.0 --> 'a
end) = struct

open T
open Basic
open List
open Nat

(* Common pattern for cost constraint :
     cost + post_potential <= acost + pre_potential
   (acost: amortized cost)
 *)
(* potential := 4 * ite (2 * num >= size) (2 * num - size) (size / 2 - num)
             == 4 * ite (2 * num >= size) (2 * num) (size / 2) - 4 * ite (2 * num >= size) size num 
 *)
(* the "4" factor is because of the "4" factor in "copy"'s time *)
datatype some_output_and_cost_constraint 'a {size num : Nat} {acost cost : Time} =
         SomeOutputAndCostConstaint
           {size' num' : Nat}
           {cost + 4.0 * ite (2 * num' >=? size') ($(2 * num')) ($size' / 2) + 4.0 * ite (2 * num >=? size) $size $num <= 4.0 * ite (2 * num >=? size) ($(2 * num)) ($size / 2) + 4.0 * ite (2 * num' >=? size') $size' $num' + acost}
         of table 'a {size'} {num'} --> some_output_and_cost_constraint 'a {size} {num} {acost} {cost}

(* An amortized computation is a closure (or "computation") whose cost is constrainted by the input and output capas in some manner.
   Note that the actual [cost] is existentially introduced and not visible from the type.
 *)
datatype amortized_comp 'a {size num : Nat} {acost : Time} =
         AmortizedComp {cost : Time} of
         (unit -- cost --> some_output_and_cost_constraint 'a {size} {num} {acost} {cost}) --> amortized_comp 'a {size} {num} {acost}

(* When num reaches capacity, do re-allocation and copying *)
fun insert ['a] {size num : Nat} (x : 'a) (table : table 'a {size} {num}) =
    AmortizedComp
      (fn () return some_output_and_cost_constraint 'a {size} {num} {38.0} {} =>
          let
            val LE _ = table_num_le_size table
            val num = num table
            val size = size table
          in
            case eq_dec (num, size) return using 3.0 + ite (num =? size) (4.0 * $num + 15.0) 1.0 of
                Neq =>
                SomeOutputAndCostConstaint (do_insert table x)
              | Eq =>
                let
                  val new_table = alloc (nat_max (nat_mult (size, nat_2), nat_1), x)
                  val new_table = copy table new_table
                in
                  SomeOutputAndCostConstaint (do_insert new_table x)
                end
          end
      )

(* When num' falls below capacity/4, do re-allocation and copying *)
fun delete ['a] {size num : Nat} (table : table 'a {size} {num}) =
    let
      val LE _ = table_num_le_size table
      val @DoDelete {_ _ num' _} table' = do_delete table
      val num' = num table'
      val size = size table'
    in
      AmortizedComp
        (fn () return some_output_and_cost_constraint 'a {size} {num} {38.0} {} =>
           case lt_dec (nat_mult (nat_4, num'), size) return using ite (4 * num' <? size) (13.0 + 4.0 * $num') 0.0 of
               Lt =>
               let
                 val init = any_value table'
                 val new_table = alloc (floor_half size, init)
                 val new_table = copy table' new_table
               in
                 SomeOutputAndCostConstaint new_table
               end
             | Ge =>
               SomeOutputAndCostConstaint table'
        )
    end

fun insert_or_delete ['a] {size num : Nat} (is_insert : bool, x : 'a) (table : table 'a {size} {num}) return using 38.0 =
    if is_insert then
      insert x table
    else
      delete table

datatype some_table 'a =
         SomeTable {size num : Nat} of table 'a {size} {num} --> some_table 'a

fun insert_delete_seq ['a] {n size num : Nat} (xs : list (bool * 'a) {n}) (table : table 'a {size} {num}) return some_table 'a using 81.0 * $n + 4.0 * ite (2 * num >=? size) ($(2 * num - size)) ($size / 2 - $num) =
    case xs of
        Nil => SomeTable table
      | Cons (x, xs) =>
        let
          val AmortizedComp f = insert_or_delete x table
          val SomeOutputAndCostConstaint table = f ()
          val table = insert_delete_seq xs table
        in
          table
        end
          
absidx T_insert_delete_seq_from_good_start : BigO (fn n => $n) with
fun insert_delete_seq_from_good_start ['a] {n size num : Nat} {ite (2 * num >=? size) ($(2 * num - size)) ($size / 2 - $num) <= $n} (xs : list (bool * 'a) {n}) (table : table 'a {size} {num}) return some_table 'a using T_insert_delete_seq_from_good_start n =
    insert_delete_seq xs table using 2.0 + 85.0 * $n
end
          
absidx T_insert_delete_seq_from_empty : BigO (fn n => $n) with
fun insert_delete_seq_from_empty ['a] {n : Nat} (xs : list (bool * 'a) {n}) (table : table 'a {0} {0}) return some_table 'a using T_insert_delete_seq_from_empty n =
    insert_delete_seq xs table using 2.0 + 81.0 * $n
end

end

structure ArrayTable = struct

open Basic
open Array
       
datatype table 'a {size : Nat} {num : Nat} =
         Table {num <= size} of array 'a {size} * nat {num} --> table 'a {size} {num}
                                     
fun table_num_le_size ['a] {size num : Nat} (t : table 'a {size} {num}) return le {num} {size} using 1.0 =
  let                                          
    val Table _ = t
  in
    LE
  end
    
fun alloc ['a] {size : Nat} (size : nat {size}, init : 'a) return table 'a {size} {0} using 1.0 =
  Table (array (size, init), #0)
        
fun do_insert ['a] {size num : Nat} {num < size} (t : table 'a {size} {num}) (x : 'a) return table 'a {size} {num + 1} using 2.0 =
  let
    val Table (a, num) = t
    val () = update (a, num, x) 
  in
    Table (a, num #+ #1)
  end
  
datatype do_delete 'a {num size : Nat} = DoDelete {num' : Nat} {num = num' \/ num = num' + 1} of table 'a {size} {num'} --> do_delete 'a {size} {num}
                                                                                                 
fun do_delete ['a] {size num : Nat} (t : table 'a {size} {num}) return do_delete 'a {size} {num} using 2.0 =
  let
    val Table (a, num) = t
  in
    DoDelete (Table (a, bounded_minus (num, #1)))
  end
  
fun copy ['a] {size num size' num' : Nat} (s : table 'a {size} {num}) (t : table 'a {size'} {num'}) return table 'a {size'} {num min size'} using 4.0 * $num + 5.0 =
  let
    val Table (a, num) = s
    val Table (a', num') = t
    val size' = length a'
    val num'' = nat_min (num, size')
    (* val nat {num''} = num'' *)
    idx num'' = num min size'
    fun loop {i | i <= num''} (i : nat {i}) =
      ifdec i #>= num'' then ()
      else update (a', i, sub (a, i)); loop (i #+ #1) using 4.0 * $(num'' - i)
    val () = loop #0
  in
    Table (a', num'')
  end
  
fun num ['a] {size num : Nat} (t : table 'a {size} {num}) return nat {num} using 1.0 =
  let
    val Table (_, num) = t
  in
    num
  end
    
fun size ['a] {size num : Nat} (t : table 'a {size} {num}) return nat {size} using 1.0 =
  let
    val Table (a, _) = t
  in
    length a
  end
                     
fun any_value ['a] {size num : Nat} {size > 0} (t : table 'a {size} {num}) return using 1.0 =
  let
    val Table (a, _) = t
  in
    sub (a, #0)
  end
        
end

structure ArrayDynamicTable = DynamicTable (ArrayTable)