Amortized Analysis via Coalgebra

Abstract

Amortized analysis is a technique for analyzing the efficiency of operations on a data structure in which cost is studied in aggregate: rather than considering the cost of a single operation in isolation, one bounds the total cost encountered throughout multiple operations in sequence. Traditionally, amortized analysis is 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. In addition to simplifying the precise definition of amortized analysis, this perspective also generalizes the technique to other settings and incorporates type- and category-theoretic intuition.