DROPS

Document

Track B: Automata, Logic, Semantics, and Theory of Programming

DOI: 10.4230/LIPIcs.ICALP.2026.185

Persistent Amortised Analysis, Operationally

Authors: Anton Lorenzen

Published in: LIPIcs, Volume 374, 53rd International Colloquium on Automata, Languages, and Programming (ICALP 2026)

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, amortised analysis in a persistent setting can be performed purely in terms of credits without using debits at all. Finally, we provide a formal semantics for Okasaki’s original debit-based approach.

Cite as

Anton Lorenzen. Persistent Amortised Analysis, Operationally. In 53rd International Colloquium on Automata, Languages, and Programming (ICALP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 374, pp. 185:1-185:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{lorenzen:LIPIcs.ICALP.2026.185,
  author =	{Lorenzen, Anton},
  title =	{{Persistent Amortised Analysis, Operationally}},
  booktitle =	{53rd International Colloquium on Automata, Languages, and Programming (ICALP 2026)},
  pages =	{185:1--185:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-428-4},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{374},
  editor =	{Bhattacharya, Sayan and Nanongkai, Danupon and Benedikt, Michael and Puppis, Gabriele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2026.185},
  URN =		{urn:nbn:de:0030-drops-265736},
  doi =		{10.4230/LIPIcs.ICALP.2026.185},
  annote =	{Keywords: Lazy Data Structures, Amortised Analysis}
}

Document

DOI: 10.4230/LIPIcs.ITP.2021.16

A Natural Formalization of the Mutilated Checkerboard Problem in Naproche

Authors: Adrian De Lon, Peter Koepke, and Anton Lorenzen

Published in: LIPIcs, Volume 193, 12th International Conference on Interactive Theorem Proving (ITP 2021)

Abstract

Naproche is an emerging natural proof assistant that accepts input in a controlled natural language for mathematics, which we have integrated with LaTeX for ease of learning and to quickly produce high-quality typeset documents. We present a self-contained formalization of the Mutilated Checkerboard Problem in Naproche, following a proof sketch by John McCarthy. The formalization is embedded in detailed literate style comments. We also briefly describe the Naproche approach.

Cite as

Adrian De Lon, Peter Koepke, and Anton Lorenzen. A Natural Formalization of the Mutilated Checkerboard Problem in Naproche. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 16:1-16:11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{delon_et_al:LIPIcs.ITP.2021.16,
  author =	{De Lon, Adrian and Koepke, Peter and Lorenzen, Anton},
  title =	{{A Natural Formalization of the Mutilated Checkerboard Problem in Naproche}},
  booktitle =	{12th International Conference on Interactive Theorem Proving (ITP 2021)},
  pages =	{16:1--16:11},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-188-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{193},
  editor =	{Cohen, Liron and Kaliszyk, Cezary},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.16},
  URN =		{urn:nbn:de:0030-drops-139112},
  doi =		{10.4230/LIPIcs.ITP.2021.16},
  annote =	{Keywords: checkerboard, formalization, formal mathematics, controlled language}
}

Search Results

Documents authored by Lorenzen, Anton

Persistent Amortised Analysis, Operationally

Abstract

Cite as

A Natural Formalization of the Mutilated Checkerboard Problem in Naproche

Abstract

Cite as

Thanks for your feedback!

Could not send message