arxiv: 2605.09411 · v1 · submitted 2026-05-10 · 💻 cs.PL

Recognition: 2 theorem links

· Lean Theorem

Persistent Amortised Analysis, Operationally

Anton Lorenzen

Authors on Pith no claims yet

Pith reviewed 2026-05-12 02:23 UTC · model grok-4.3

classification 💻 cs.PL

keywords amortised analysispersistent data structuresthunksoperational semanticscall-by-value lambda calculusfunctional programmingdebits and credits

0 comments

The pith

Credit-based amortised analysis can be sound for persistent data structures when credits are stored only on thunks.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

Amortised analysis aims to prove combined time bounds for sequences of operations on data structures, but persistence breaks traditional credit-based methods because previous versions can be reused. The paper develops an operational semantics for call-by-value lambda calculus with thunks to model this setting precisely. It demonstrates that standard credit-based analysis produces incorrect bounds in persistent use, yet the method works correctly if credits are confined to thunks. It also supplies a formal semantics for the debit-based alternative. Sympathetic readers care because this resolves a point of confusion in proving efficiency for functional persistent structures.

Core claim

Contrary to folklore, credit-based amortised analysis is sound in a persistent setting provided that credits are only stored on thunks. This is shown using an operational semantics of call-by-value lambda calculus with thunks, which also establishes that the traditional approach fails without this restriction and provides a semantics for the debit-based method.

What carries the argument

Operational semantics for call-by-value lambda calculus with thunks that models sharing and cost under persistence.

If this is right

Traditional credit-based amortised analysis fails to give correct bounds for persistent data structures.
Restricting credits to thunks makes credit-based analysis sound for persistent use.
A formal semantics can be given to debit-based amortised analysis.
Amortised analysis becomes applicable to persistent functional data structures under these conditions.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

This approach may simplify time-bound proofs for some persistent structures by avoiding the need for debits.
The semantics could serve as a basis for mechanized verification of amortised analyses in theorem provers.
Similar restrictions might apply to other cost analyses in lazy or memoized evaluation settings.

Load-bearing premise

The operational semantics chosen for the lambda calculus with thunks accurately represents the cost and sharing in actual persistent data structures.

What would settle it

An example persistent data structure where storing credits only on thunks still produces an unsound time bound, or empirical measurements showing the semantics does not match real execution costs.

read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The paper shows credits work for persistent amortized analysis if restricted to thunks and supplies the first operational semantics for Okasaki's debit method.

read the letter

The core contribution is a formal clarification that the folklore claim about credits failing in persistent settings is not quite right. Credits remain sound when stored only on thunks, and the paper gives an operational account of both the failure case and the debit approach inside a call-by-value lambda calculus with thunks. This is the main new piece: neither the restricted-credit result nor the debit semantics appear in the cited prior work. The argument proceeds directly from the defined operational rules, so there is no circularity or self-referential accounting. The proofs are stated explicitly, which makes the technique more accessible and checkable than the original informal presentation. The paper does a clean job of separating the cases and showing where traditional credits break under persistence while the thunk-restricted version holds. One soft spot is the modeling choice itself. The semantics must accurately reflect sharing, forcing costs, and thunk creation in actual persistent structures; if real implementations like those in Haskell carry extra memoization or version-management overhead not present in the model, the soundness result stays internal to the calculus. That is a standard limitation for operational models rather than a flaw in the execution. The work is aimed at researchers in programming languages and verified functional data structures who need precise foundations for amortized bounds. A reader already working on cost analysis or persistent libraries would get direct value from the definitions and the separation of concerns. It deserves a serious referee because the formalization is substantive, the claims are grounded, and the clarification addresses a technique that has been used without this level of detail.

Referee Report

0 major / 1 minor

Summary. The paper sets up an operational semantics for call-by-value lambda calculus with thunks, formally demonstrates that traditional credit-based amortised analysis yields unsound bounds under persistent usage, shows that restricting credits to thunks restores soundness, and provides a formal semantics for Okasaki's debit-based approach, thereby challenging the folklore that credits cannot be used for persistent amortised analysis.

Significance. If the results hold, the work supplies a precise formal foundation for persistent amortised analysis, clarifies the conditions under which credit-based methods remain valid, and renders Okasaki's debit technique more accessible to a wider audience through explicit operational rules and stated proofs rather than informal arguments. The explicit model and low circularity in the derivations constitute a clear strength.

minor comments (1)

The manuscript would benefit from a brief discussion of how the chosen thunk semantics aligns with or abstracts from memoization overheads in concrete implementations such as Haskell, even if only to delimit the scope of the formal result.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive review, clear summary of our contributions, and recommendation to accept the paper. We are pleased that the formal operational semantics and clarification of credit-based analysis for persistent structures were viewed as strengthening the foundation of Okasaki's approach.

Circularity Check

0 steps flagged

No significant circularity; claims derived from independent operational semantics

full rationale

The paper first defines an operational semantics for call-by-value lambda calculus with thunks, then uses that semantics to exhibit a counterexample showing traditional credit-based analysis fails under persistence, proves soundness for credits restricted to thunks, and gives a formal account of Okasaki's debits. All steps follow from the stated reduction rules and cost model rather than tautologically equating to fitted parameters, self-definitions, or prior self-citations. The central results are therefore independent of the conclusions they reach.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The work rests on standard definitions of operational semantics and no fitted parameters or new postulated entities.

axioms (1)

standard math Standard operational semantics rules for call-by-value lambda calculus extended with thunks
These rules form the foundation for all subsequent claims about costs and persistence.

pith-pipeline@v0.9.0 · 5516 in / 1007 out tokens · 70532 ms · 2026-05-12T02:23:30.011705+00:00 · methodology

discussion (0)

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

IndisputableMonolith/Cost/FunctionalEquation.lean washburn_uniqueness_aczel unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

We define the soundness and persistence of a reasoning principle in terms of the operational semantics of call-by-value lambda calculus with thunks... credit passing style... debit semantics
IndisputableMonolith/Foundation/ArrowOfTime.lean z_monotone_absolute echoes

?

echoes
ECHOES: this paper passage has the same mathematical shape or conceptual pattern as the Recognition theorem, but is not a direct formal dependency.

An accessible cost model is a cost model equipped with a preorder ⊑ on heaps such that Γ⊑∆ iff Γ:e⇓n ∆:v

What do these tags mean?

matches: The paper's claim is directly supported by a theorem in the formal canon.
supports: The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends: The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses: The paper appears to rely on the theorem as machinery.
contradicts: The paper's claim conflicts with a theorem or certificate in the canon.
unclear: Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

33 extracted references · 33 canonical work pages

[1]

2004 , publisher =

Semantics of types for mutable state , author =. 2004 , publisher =

work page 2004
[2]

Proceedings of the ACM on Programming Languages , volume =

Snapshottable Stores , author =. Proceedings of the ACM on Programming Languages , volume =. 2024 , publisher =. doi:10.1145/3674637 , timestamp =

work page doi:10.1145/3674637 2024
[3]

Proceedings of the seventh international conference on Functional programming languages and computer architecture , pages =

Parallelism in sequential functional languages , author =. Proceedings of the seventh international conference on Functional programming languages and computer architecture , pages =. 1995 , timestamp =. doi:10.1145/224164.224210 , _bib2doi_selected =

work page doi:10.1145/224164.224210 1995
[4]

2008 , publisher =

Nils Anders Danielsson , title =. 2008 , publisher =. doi:10.1145/1328438.1328457 , booktitle =

work page doi:10.1145/1328438.1328457 2008
[5]

[FL93] Joel Friedman and Nathan Linial

Making Data Structures Persistent , journal =. 1989 , issn =. doi:10.1016/0022-0000(89)90034-2 , author =

work page doi:10.1016/0022-0000(89)90034-2 1989
[6]

Journal of the ACM (JACM) , volume =

Fully persistent lists with catenation , author =. Journal of the ACM (JACM) , volume =. 1994 , publisher =. doi:10.1145/185675.185791 , _bib2doi_selected =

work page doi:10.1145/185675.185791 1994
[7]

International Workshop on Aliasing, Confinement and Ownership in object-oriented programming (IWACO) , year =

Heap monotonic typestates , author =. International Workshop on Aliasing, Confinement and Ownership in object-oriented programming (IWACO) , year =

work page
[8]

Proceedings of the ACM on Programming Languages , volume =

Keep your laziness in check , author =. Proceedings of the ACM on Programming Languages , volume =. 2018 , publisher =. doi:10.1145/3236797 , timestamp =

work page doi:10.1145/3236797 2018
[9]

Proceedings of the ACM on Programming Languages , volume =

Call-by-need is clairvoyant call-by-value , author =. Proceedings of the ACM on Programming Languages , volume =. 2019 , publisher =. doi:10.1145/3341718 , timestamp =

work page doi:10.1145/3341718 2019
[10]

Type-Based Cost Analysis for Lazy Functional Languages , ty =

Jost, Steffen and Vasconcelos, Pedro and Florido, M. Type-Based Cost Analysis for Lazy Functional Languages , ty =. Journal of Automated Reasoning , number =. 2017 , timestamp =. doi:10.1007/s10817-016-9398-9 , id =

work page doi:10.1007/s10817-016-9398-9 2017
[11]

2000 , publisher =

Simple Confluently Persistent Catenable Lists , author =. 2000 , publisher =. doi:10.1137/S0097539798339430 , timestamp =

work page doi:10.1137/s0097539798339430 2000
[12]

Proceedings of the 2nd ACM SIGPLAN workshop on Functional high-performance computing , pages =

LVars: lattice-based data structures for deterministic parallelism , author =. Proceedings of the 2nd ACM SIGPLAN workshop on Functional high-performance computing , pages =. 2013 , timestamp =. doi:10.1145/2502323.2502326 , _bib2doi_selected =

work page doi:10.1145/2502323.2502326 2013
[13]

Proceedings of the 20th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages , series =

Launchbury, John , title =. Proceedings of the 20th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages , series =. 1993 , location =. doi:10.1145/158511.158618 , timestamp =

work page doi:10.1145/158511.158618 1993
[14]

Information and computation , volume =

Modelling environments in call-by-value programming languages , author =. Information and computation , volume =. 2003 , publisher =. doi:10.1016/S0890-5401(03)00088-9 , _bib2doi_selected =

work page doi:10.1016/s0890-5401(03)00088-9 2003
[15]

Proceedings of the ACM on Programming Languages , volume =

Reasoning about the garden of forking paths , author =. Proceedings of the ACM on Programming Languages , volume =. 2021 , publisher =. doi:10.1145/3473585 , timestamp =

work page doi:10.1145/3473585 2021
[16]

Proceedings of the 18th ACM SIGPLAN International Haskell Symposium , year =

Lightweight Testing of Persistent Amortized Time Complexity in the Credit Monad , author =. Proceedings of the 18th ACM SIGPLAN International Haskell Symposium , year =. doi:10.1145/3759164.3759351 , timestamp =

work page doi:10.1145/3759164.3759351
[17]

Proceedings of the ACM on Programming Languages , number =

First-Order Laziness , author =. Proceedings of the ACM on Programming Languages , number =. 2025 , publisher =. doi:10.1145/3747530 , timestamp =

work page doi:10.1145/3747530 2025
[18]

Moerman, M

Ravichandhran Madhavan and Sumith Kulal and Viktor Kuncak , title =. 2017 , publisher =. doi:10.1145/3009837.3009874 , booktitle =

work page doi:10.1145/3009837.3009874 2017
[19]

Time credits and time receipts in Iris , author =. Programming Languages and Systems: 28th European Symposium on Programming, ESOP 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6--11, 2019, Proceedings 28 , pages =. 2019 , organization =. doi:10.1007/978-3-030-17184-1_1 ,...

work page doi:10.1007/978-3-030-17184-1_1 2019
[20]

1998 , publisher =

Okasaki, Chris , title =. 1998 , publisher =

work page 1998
[21]

Proceedings of the 7th ACM SIGPLAN Workshop on Types in Language Design and Implementation , pages =

The essence of monotonic state , author =. Proceedings of the 7th ACM SIGPLAN Workshop on Types in Language Design and Implementation , pages =. 2011 , timestamp =. doi:10.1145/1929553.1929565 , _bib2doi_selected =

work page doi:10.1145/1929553.1929565 2011
[22]

2026 , month =

Ponsonnet, Juliette and Pottier, Fran. 2026 , month =

work page 2026
[23]

Proceedings of the ACM on Programming Languages , volume =

Thunks and Debits in Separation Logic with Time Credits , author =. Proceedings of the ACM on Programming Languages , volume =. 2024 , publisher =. doi:10.1145/3632892 , timestamp =

work page doi:10.1145/3632892 2024
[24]

1986 , month = jul, journal =

Neil Sarnak and Robert Endre Tarjan , title =. 1986 , issue_date =. doi:10.1145/6138.6151 , journal =

work page doi:10.1145/6138.6151 1986
[25]

Proceedings of the ACM on Programming Languages , volume =

Sealing pointer-based optimizations behind pure functions , author =. Proceedings of the ACM on Programming Languages , volume =. 2020 , publisher =. doi:10.1145/3408997 , timestamp =

work page doi:10.1145/3408997 2020
[26]

SIAM Journal on Algebraic Discrete Methods , volume =

Amortized computational complexity , author =. SIAM Journal on Algebraic Discrete Methods , volume =. 1985 , publisher =. doi:10.1137/0606031 , _bib2doi_finished =

work page doi:10.1137/0606031 1985
[27]

Communications of the ACM , volume =

A data structure for manipulating priority queues , author =. Communications of the ACM , volume =. 1978 , publisher =. doi:10.1145/359460.359478 , _bib2doi_selected =

work page doi:10.1145/359460.359478 1978
[28]

Xia, Li-yao and Israel, Laura and Kramarz, Maite and Coltharp, Nicholas and Claessen, Koen and Weirich, Stephanie and Li, Yao , title =. Proc. ACM Program. Lang. , month =. 2024 , issue_date =. doi:10.1145/3674626 , timestamp =

work page doi:10.1145/3674626 2024
[29]

Electronic Notes in Theoretical Informatics and Computer Science , volume =

Amortized Analysis via Coalgebra , author =. Electronic Notes in Theoretical Informatics and Computer Science , volume =. 2024 , publisher =. doi:10.46298/entics.14797 , _bib2doi_selected =

work page doi:10.46298/entics.14797 2024
[30]

European Symposium on Programming , pages =

Type-based amortised heap-space analysis , author =. European Symposium on Programming , pages =. 2006 , organization =. doi:10.1007/11693024_3 , _bib2doi_selected =

work page doi:10.1007/11693024_3 2006
[31]

ACM Transactions on Programming Languages and Systems (TOPLAS) , volume =

Multivariate amortized resource analysis , author =. ACM Transactions on Programming Languages and Systems (TOPLAS) , volume =. 2012 , publisher =. doi:10.1145/2362389.2362393 , _bib2doi_selected =

work page doi:10.1145/2362389.2362393 2012
[32]

Mathematical Structures in Computer Science , volume =

Two decades of automatic amortized resource analysis , author =. Mathematical Structures in Computer Science , volume =. 2022 , publisher =. doi:10.1017/S0960129521000487 , _bib2doi_selected =

work page doi:10.1017/s0960129521000487 2022
[33]

Proceedings of the 17th ACM SIGPLAN international conference on Functional programming , pages =

Automatic amortised analysis of dynamic memory allocation for lazy functional programs , author =. Proceedings of the 17th ACM SIGPLAN international conference on Functional programming , pages =. 2012 , timestamp =. doi:10.1145/2364527.2364575 , _bib2doi_selected =

work page doi:10.1145/2364527.2364575 2012