functional-queue.timl

(* Functional queue (amortized analysis) *)

(* Functional queues are queues implemented with two stacks. 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. *)

(* The main functions are [enqueue_dequeue_seq_from_good_start] and [enqueue_dequeue_seq_from_empty]. *)

structure FunctionalQueue = struct

open Basic
open List

datatype queue 'a {s1 s2 : Nat} =
         Queue of list 'a {s1} * list 'a {s2} --> queue 'a {s1} {s2}

(* Common pattern for cost constraint :
     cost + post_potential <= acost + pre_potential
   (acost: amortized cost)
 *)
(* potential := s1 *)
datatype some_output_and_cost_constraint 'a {s1 s2 : Nat} {acost cost : Time} =
         SomeOutputAndCostConstraint
           {s1' s2' : Nat}
           {cost + $s1' <= $s1 + acost}
         of queue 'a {s1'} {s2'} --> some_output_and_cost_constraint 'a {s1} {s2} {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 {s1 s2 : Nat} {acost : Time} =
         AmortizedComp
           {cost : Time} 
         of (unit -- cost --> some_output_and_cost_constraint 'a {s1} {s2} {acost} {cost}) --> amortized_comp 'a {s1} {s2} {acost}

(* enqueue is implemented by pushing to stack 1 *)                                
fun do_enqueue ['a] {s1 s2 : Nat} (q : queue 'a {s1} {s2}, x : 'a) =
    case q return queue 'a {s1 + 1} {s2} of
        Queue (l1, l2) => Queue (x :: l1, l2)

(* dequeue is implemented by poping from stack 2; when stack 2 is empty, dump all elements from stack 1 to stack2, reversing order naturally *)
fun do_dequeue ['a] {s1 s2 : Nat} (q : queue 'a {s1} {s2}) return queue 'a {ite (s2 =? 0) 0 s1} {ite (s2 =? 0) (s1 - 1) (s2 - 1)} using ite (s2 =? 0) ($s1 + 1.0) 0.0 =
    case q of
        Queue (l1, l2) =>
        case l2 of
            hd :: tl => Queue (l1, tl)
          | [] =>
            let
              val l2 = rev_append (l1, [])
            in
              case l2 of
                  hd :: tl => Queue ([], tl)
                | [] => Queue ([], [])
            end

fun enqueue ['a] {s1 s2 : Nat} (q : queue 'a {s1} {s2}, x : 'a) return amortized_comp 'a {s1} {s2} {2.0} =
    AmortizedComp
      (fn () =>
          SomeOutputAndCostConstraint (do_enqueue (q, x)))

fun dequeue ['a] {s1 s2 : Nat} (q : queue 'a {s1} {s2}) return amortized_comp 'a {s1} {s2} {2.0} =
    AmortizedComp
      (fn () =>
          SomeOutputAndCostConstraint (do_dequeue q))

datatype operation 'a =
         OPush of 'a --> operation 'a
         | OPop of operation 'a

fun enqueue_or_dequeue ['a] {s1 s2 : Nat} (q : queue 'a {s1} {s2}, opr : operation 'a) =
    case opr of
        OPush x => enqueue (q, x)
      | OPop => dequeue q

datatype some_queue 'a =
         SomeQueue {s1 s2 : Nat} of queue 'a {s1} {s2} --> some_queue 'a

fun enqueue_dequeue_seq ['a] {s1 s2 cnt : Nat} (q : queue 'a {s1} {s2}, oprs : list (operation 'a) {cnt}) return some_queue 'a using 6.0 * $cnt + $s1 =
    case oprs of
        [] => SomeQueue q
      | hd :: tl =>
        let
          val AmortizedComp f = enqueue_or_dequeue (q, hd)
          val SomeOutputAndCostConstraint q = f ()
        in
          enqueue_dequeue_seq (q, tl)
        end

absidx T_enqueue_dequeue_seq_from_good_start : BigO (fn n => $n) with
fun enqueue_dequeue_seq_from_good_start ['a] {s1 s2 cnt : Nat} {s1 <= cnt} (q : queue 'a {s1} {s2}, oprs : list (operation 'a) {cnt}) return some_queue 'a using T_enqueue_dequeue_seq_from_good_start cnt =
    enqueue_dequeue_seq (q, oprs)
end

absidx T_enqueue_dequeue_seq_from_empty : BigO (fn n => $n) with
fun enqueue_dequeue_seq_from_empty ['a] {cnt : Nat} (q : queue 'a {0} {0}, oprs : list (operation 'a) {cnt}) return some_queue 'a using T_enqueue_dequeue_seq_from_empty cnt =
    enqueue_dequeue_seq (q, oprs)
end

end