Persistent Amortised Analysis, Operationally
For researchers and practitioners in data structures and programming languages, this work resolves a long-standing folklore about the unsoundness of credit-based amortised analysis under persistence, providing a clearer theoretical foundation.
This paper clarifies the formal foundations of Okasaki's persistent amortised analysis by providing an operational semantics for call-by-value lambda calculus with thunks, showing that credit-based analysis is sound when credits are stored only on thunks, and formalizing Okasaki's debit-based approach.
Amortised analysis is a technique for proving a combined time bound for a batch of operations on a data structure, even if some of those operations are expensive. But the traditional method of amortised analysis yields incorrect time bounds when the data structure is used persistently. Persistence allows operations to be performed on previous versions of the data structure, which prevents us from amortising expensive restructuring work. In his seminal book, Chris Okasaki showed how to extend amortised analysis to persistent usage. His method works by extending the data structure with thunks and performing the analysis with debits rather than credits. His argument, that credits are unsound for analysing persistent usage, has become folklore. In this paper, we provide a new perspective on the role of debits in Okasaki's work. First, we set up an operational semantics of call-by-value lambda calculus with thunks, and show formally that traditional amortised analysis does not work in a persistent setting. Then we show that, contrary to the folklore, credit-based amortised analysis can be sound in a persistent setting as long as credits are only stored on thunks. Finally, we provide a formal semantics for Okasaki's debit-based approach. Our paper clarifies the formal foundation of Okasaki's work and makes it accessible to a wider audience.