NyaOJ

题目描述

本题考察在定理证明器中对程序的时间复杂度进行证明。

为了对程序的时间消耗进行建模，本题通过 Tick Monad 使用一个自然数对一段计算的方法的时间进行度量（可以理解为"步数"），tick 用来标记一定的时间消耗。比如，如果希望以函数调用次数为时间度量，可以在每次函数调用前插入 tick 1。

本题考虑使用两个列表来模拟队列的算法。该算法的思想是把队列的数据存储在两个列表 outq 和 inq 中：

入队操作总是在 inq 的头部添加元素，而出队操作总是在 outq 的头部取出元素。当进行出队操作但是 outq 为空时，需要先将 inq 进行翻转并移动其中元素到 outq 中。

这样实现的队列操作的均摊时间复杂度是常数，即从空队列开始执行 $n$ 个队列操作的时间复杂度为 $O(n)$ 。

Queue.empty a：返回一个队列元素类型为 a 的空队列
Queue.in_to_out q：把 q.inq 进行翻转并移动其中元素到 q.outq 中
Queue.enq q x：将元素 x 入队到 q 中
Queue.deq q：从 q 中出队一个元素，若队列为空则返回 none
Queue.seq_op_queue q ops：从队列 q 开始依次执行 ops 中的操作，其中操作如果是 none 则表示出队，是 some x 则表示入队
Queue.seq_op_queue_from_empty ops：从空队列开始依次执行 ops 中的操作

(150 分) 试证明定理 seq_op_queue_from_empty_cost：从空队列开始执行 $n$ 个操作的时间复杂度的上界为 $2n$ 。

theorem seq_op_queue_from_empty_cost {α : Type} (ops : List (Option α)) :
    (seq_op_queue_from_empty ops ()).2 ≤ 2 * ops.length

使用势能法 (potential method) 进行均摊分析。可以定义势能函数为入队栈的大小。

总计: 150 分