Persistent Amortised Analysis, Operationally

TL;DR

This paper revisits amortised analysis for persistent data structures, demonstrating that credit-based methods can be sound if credits are stored on thunks, and clarifies Okasaki's debit-based approach through formal semantics.

Contribution

It provides a formal semantics for Okasaki's debit-based amortised analysis and shows credit-based analysis can be sound in persistence when credits are stored on thunks.

Findings

Traditional amortised analysis fails in persistent settings.

Credit-based analysis can be sound if credits are stored on thunks.

Provides formal semantics for Okasaki's debit-based approach.

Abstract

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.