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} -- 1.0 --> table 'a {size} {0}
  val do_insert ['a] : forall {size num : Nat} {num < size}, table 'a {size} {num} ->> 'a -- 1.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} ->> 'a -- 1.0 --> do_delete 'a {size} {num}
  val copy ['a] : forall {size num size' num' : Nat}, table 'a {size} {num} ->> table 'a {size'} {num'} -- $num --> 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}
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 := ite (2 * num >= size) (2 * num - size) (size / 2 - num)
             == ite (2 * num >= size) (2 * num) (size / 2) - ite (2 * num >= size) size num 
*)
datatype some_output_and_cost_constraint 'a {size num : Nat} {acost cost : Time} =
         SomeOutputAndCostConstaint
           {size' num' : Nat}
           {cost + ite (2 * num' >= size') ($(2 * num')) ($size' / 2) + ite (2 * num >= size) $size $num <= ite (2 * num >= size) ($(2 * num)) ($size / 2) + 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} {23.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 2.0 + ite (num == size) ($num + 9.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))
                  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} (x : 'a) (table : table 'a {size} {num}) =
    let
      val LE _ = table_num_le_size table
      val @DoDelete {_ _ num' _} table' = do_delete table x
      val num' = num table'
      val size = size table'
    in
      AmortizedComp
        (fn () return some_output_and_cost_constraint 'a {size} {num} {23.0} {} =>
           case lt_dec (nat_mult (nat_4, num'), size) return using ite (4 * num' < size) (5.0 + $num') 0.0 of
               Lt =>
               let
                 val new_table = alloc (floor_half size)
                 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 20.0 =
    case is_insert of
        true => insert x table
      | false => delete x 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 48.0 * $n + 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 + 49.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 + 48.0 * $n
end

end