Amortized Analysis via Coalgebra
Harrison Grodin, Robert Harper
TL;DR
The paper reframes amortized analysis as a coalgebraic cost analysis within the category of writer monad algebras, showing that potentials correspond to generalized coalgebra morphisms and that cost-boundedness can be captured by a simple amortization equation $\costof{\specCoalg}(d) = \costof{\implCoalg}(d) + \Phi(\behof{\implCoalg}(d)) - \Phi(d)$. It extends this view to lax (colax) settings in bicategories to accommodate upper bounds, and to endoprofunctors to handle multi-input/output operations, including randomized and expected amortization via suitable monads. The framework supports splitting/combining potentials through monoidal structure and profunctors, enabling composition of amortized data structures and translation between signatures via indexed categories; this yields practical constructions such as queues from stacks and buffers from printing, all within a uniform, abstract theory. The authors also report mechanization in Calf and discuss connections to prior work, along with directions for future exploration such as nonrepresentable carriers and double-categorical extensions, highlighting the significance of a unified, effect-aware, coalgebraic account of amortized cost across data-structure paradigms.
Abstract
Amortized analysis is a cost analysis technique for data structures in which cost is studied in aggregate: rather than considering the maximum cost of a single operation, one bounds the total cost encountered throughout a session. Traditionally, amortized analysis has been phrased inductively, quantifying over finite sequences of operations. Connecting to prior work on coalgebraic semantics for data structures, we develop the alternative perspective that amortized analysis is naturally viewed coalgebraically in a category of cost algebras, where a morphism of coalgebras serves as a first-class generalization of potential function suitable for integrating cost and behavior. Using this simple definition, we consider amortization of other sample effects, non-commutative printing and randomization. To support imprecise amortized upper bounds, we adapt our discussion to the bicategorical setting, where a potential function is a colax morphism of coalgebras. We support algebraic and coalgebraic operations simultaneously by using coalgebras for an endoprofunctor instead of an endofunctor, combining potential using a monoidal structure on the underlying category. Finally, we compose amortization arguments in the indexed category of coalgebras to implement one amortized data structure in terms of others.