Amortized analysis is a program cost analysis technique for data structures in which the cost of operations is specified in aggregate, under the assumption of continued sequential use. Typically, amortized analyses are presented inductively, in terms of finite sequences of operations. We give an alternative coinductive formulation and prove that it is equivalent to the standard inductive definition. We describe a classic amortized data structure, the batched queue, and outline a coinductive proof of its amortized efficiency in $\textbf{calf}$, a dependent type theory for cost analysis.

翻译：摊还分析是一种针对数据结构进行程序开销分析的技术，其中操作的成本是在持续顺序使用的假设下以聚合方式指定的。通常，摊还分析基于有限的操作序列以归纳形式呈现。我们给出了一种替代的余归纳表述，并证明其与标准归纳定义等价。我们描述了一种经典的摊还数据结构——批处理队列，并概述了在$\textbf{calf}$（一种用于成本分析的依赖类型理论）中对其摊还效率进行余归纳证明的框架。