(*<*) theory tmpl12 imports Complex_Main begin (*>*) text {* \ExerciseSheet{12}{14.~7.~2017} *} text \ \Exercise{Balanced Queues} Consider locale \Queue\ in file \Thys/Amortized_Examples\. A call of \deq (xs,[])\ requires the reversal of \xs\, which may be very long. We can reduce that impact by shifting \xs\ over to \ys\ whenever \length xs > length ys\. This does not improve the amortized complexity (in fact it increases it by 1) but reduces the worst case complexity of individual calls of \deq\. Modify locale \Queue\ as follows:\ locale Queue begin type_synonym 'a queue = "'a list * 'a list" definition "init = ([],[])" fun balance :: "'a queue \ 'a queue" where "balance(xs,ys) = (if size xs \ size ys then (xs,ys) else ([], ys @ rev xs))" fun enq :: "'a \ 'a queue \ 'a queue" where "enq a (xs,ys) = balance (a#xs, ys)" fun deq :: "'a queue \ 'a queue" where "deq (xs,ys) = balance (xs, tl ys)" text \Again, we count only the newly allocated list cells.\ fun t_balance :: "'a queue \ nat" where "t_balance (xs,ys) = (if size xs \ size ys then 0 else size xs + size ys)" fun t_enq :: "'a \ 'a queue \ nat" where "t_enq a (xs,ys) = 1 + t_balance (a#xs, ys)" fun t_deq :: "'a queue \ nat" where "t_deq (xs,ys) = t_balance (xs, tl ys)" text \ \<^item> Start over with showing functional correctness. Hint: You will require an invariant. \ fun invar :: "'a queue \ bool" (*<*) where "invar (xs,ys) \ undefined" (*>*) fun abs :: "'a queue \ 'a list" (*<*) where "abs (xs,ys) = undefined" (*>*) lemma [simp]: "invar init" (*<*) sorry (*>*) lemma [simp]: "invar q \ invar (enq x q)" (*<*) sorry (*>*) lemma [simp]: "invar q \ invar (deq q)" (*<*) sorry (*>*) lemma [simp]: "abs init = []" (*<*) sorry (*>*) lemma [simp]: "invar q \ abs (enq x q) = x#abs q" (*<*) sorry (*>*) lemma [simp]: "invar q \ abs (deq q) = butlast (abs q)" (*<*) sorry (*>*) text \ \<^item> Next, define a suitable potential function \\\, and prove that the amortized complexity of \enq\ is \ \ 3\ and of \deq\ is \ \ 0\. \ fun \ :: "'a queue \ int" (*<*) where "\ (xs,ys) = undefined" (*>*) lemma \_non_neg: "\ t \ 0" sorry lemma \_init: "\ init = 0" sorry lemma a_enq: " t_enq a q + \(enq a q) - \ q \ 3" sorry lemma a_deq: " t_deq q + \(deq q) - \ q \ 0" sorry text \Finally, show that a sequence of enqueue and dequeue operations requires linear cost in its length: \ (*<*) (* Establish abstraction boundary *) lemmas [simp del] = \.simps enq.simps deq.simps t_enq.simps t_deq.simps (*>*) datatype 'a opr = ENQ 'a | DEQ fun execute :: "'a queue \ 'a opr list \ 'a queue" where "execute q [] = q" | "execute q (ENQ x#ops) = execute (enq x q) ops" | "execute q (DEQ#ops) = execute (deq q) ops" text \Count only list cell allocations! \ fun t_execute :: "'a queue \ 'a opr list \ nat" where "t_execute q _ = undefined" lemma t_execute_aux: "t_execute q ops \ 3*length ops + \ q - \ (execute q ops)" sorry lemma t_execute: "t_execute init ops \ 3*length ops" sorry end (*<*) end (*>*)