Document Open Access Logo

Persistent Amortised Analysis, Operationally

Author Anton Lorenzen

PDF

File

Thumbnail PDF
PDF
LIPIcs.ICALP.2026.185.pdf
  • Filesize: 1.08 MB
  • 22 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Data structures design and analysis
  • Software and its engineering → Functional languages
  • Theory of computation → Invariants
Keywords
  • Lazy Data Structures
  • Amortised Analysis

Metrics

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 Get BibTex

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) https://doi.org/10.4230/LIPIcs.ICALP.2026.185

Author Details

Anton Lorenzen
  • University of Edinburgh, UK

Acknowledgements

I am grateful to Kengo Hirata, François Pottier, Wouter Swierstra, and Kim Worrall for their helpful feedback, and to the participants of the AUTOSARD Mid-Term Workshop 2025 for inspiring discussions. Any remaining errors are my own.

References

  1. Amal Jamil Ahmed. Semantics of types for mutable state. Princeton University, 2004. Google Scholar
  2. Clément Allain, Basile Clément, Alexandre Moine, and Gabriel Scherer. Snapshottable stores. Proceedings of the ACM on Programming Languages, 8(ICFP):338-369, 2024. URL: https://doi.org/10.1145/3674637.
  3. Guy Blelloch and John Greiner. Parallelism in sequential functional languages. In Proceedings of the seventh international conference on Functional programming languages and computer architecture, pages 226-237, 1995. URL: https://doi.org/10.1145/224164.224210.
  4. Nils Anders Danielsson. Lightweight semiformal time complexity analysis for purely functional data structures. In George C. Necula and Philip Wadler, editors, Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, San Francisco, California, USA, January 7-12, 2008, POPL '08, pages 133-144, New York, NY, USA, 2008. ACM. URL: https://doi.org/10.1145/1328438.1328457.
  5. James R. Driscoll, Neil Sarnak, Daniel Dominic Sleator, and Robert Endre Tarjan. Making data structures persistent. J. Comput. Syst. Sci., 38(1):86-124, 1989. URL: https://doi.org/10.1016/0022-0000(89)90034-2.
  6. James R Driscoll, Daniel DK Sleator, and Robert E Tarjan. Fully persistent lists with catenation. Journal of the ACM (JACM), 41(5):943-959, 1994. URL: https://doi.org/10.1145/185675.185791.
  7. Manuel Fähndrich and K Rustan M Leino. Heap monotonic typestates. In International Workshop on Aliasing, Confinement and Ownership in object-oriented programming (IWACO), 2003. Google Scholar
  8. Kenneth Foner, Hengchu Zhang, and Leonidas Lampropoulos. Keep your laziness in check. Proceedings of the ACM on Programming Languages, 2(ICFP):1-30, 2018. URL: https://doi.org/10.1145/3236797.
  9. Harrison Grodin and Robert Harper. Amortized analysis via coalgebra. Electronic Notes in Theoretical Informatics and Computer Science, 4, 2024. URL: https://doi.org/10.46298/entics.14797.
  10. Jennifer Hackett and Graham Hutton. Call-by-need is clairvoyant call-by-value. Proceedings of the ACM on Programming Languages, 3(ICFP):1-23, 2019. URL: https://doi.org/10.1145/3341718.
  11. Jan Hoffmann, Klaus Aehlig, and Martin Hofmann. Multivariate amortized resource analysis. ACM Transactions on Programming Languages and Systems (TOPLAS), 34(3):1-62, 2012. URL: https://doi.org/10.1145/2362389.2362393.
  12. Jan Hoffmann and Steffen Jost. Two decades of automatic amortized resource analysis. Mathematical Structures in Computer Science, 32(6):729-759, 2022. URL: https://doi.org/10.1017/S0960129521000487.
  13. Martin Hofmann and Steffen Jost. Type-based amortised heap-space analysis. In European Symposium on Programming, pages 22-37. Springer, 2006. URL: https://doi.org/10.1007/11693024_3.
  14. Steffen Jost, Pedro Vasconcelos, Mário Florido, and Kevin Hammond. Type-based cost analysis for lazy functional languages. Journal of Automated Reasoning, 59(1):87-120, 2017. URL: https://doi.org/10.1007/s10817-016-9398-9.
  15. Haim Kaplan, Chris Okasaki, and Robert Endre Tarjan. Simple confluently persistent catenable lists. SIAM J. Comput., 30(3):965-977, 2000. URL: https://doi.org/10.1137/S0097539798339430.
  16. Lindsey Kuper and Ryan R Newton. Lvars: lattice-based data structures for deterministic parallelism. In Proceedings of the 2nd ACM SIGPLAN workshop on Functional high-performance computing, pages 71-84, 2013. URL: https://doi.org/10.1145/2502323.2502326.
  17. John Launchbury. A natural semantics for lazy evaluation. In Proceedings of the 20th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '93, pages 144-154, 1993. URL: https://doi.org/10.1145/158511.158618.
  18. Paul-Blain Levy, John Power, and Hayo Thielecke. Modelling environments in call-by-value programming languages. Information and computation, 185(2):182-210, 2003. URL: https://doi.org/10.1016/S0890-5401(03)00088-9.
  19. Yao Li, Li-yao Xia, and Stephanie Weirich. Reasoning about the garden of forking paths. Proceedings of the ACM on Programming Languages, 5(ICFP):1-28, 2021. URL: https://doi.org/10.1145/3473585.
  20. Anton Lorenzen. Lightweight testing of persistent amortized time complexity in the credit monad. In Proceedings of the 18th ACM SIGPLAN International Haskell Symposium, 2025. URL: https://doi.org/10.1145/3759164.3759351.
  21. Anton Lorenzen. Persistent amortised analysis, operationally, 2026. URL: https://arxiv.org/abs/2605.09411.
  22. Anton Lorenzen, Daan Leijen, Wouter Swierstra, and Sam Lindley. First-order laziness. Proceedings of the ACM on Programming Languages, 9(ICFP), 2025. URL: https://doi.org/10.1145/3747530.
  23. Ravichandhran Madhavan, Sumith Kulal, and Viktor Kuncak. Contract-based resource verification for higher-order functions with memoization. In Giuseppe Castagna and Andrew D. Gordon, editors, Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, pages 330-343. ACM, 2017. URL: https://doi.org/10.1145/3009837.3009874.
  24. Glen Mével, Jacques-Henri Jourdan, and François Pottier. Time credits and time receipts in iris. In 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 3-29. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-17184-1_1.
  25. Chris Okasaki. Purely Functional Data Structures. Cambridge University Press, 1998. Google Scholar
  26. Alexandre Pilkiewicz and François Pottier. The essence of monotonic state. In Proceedings of the 7th ACM SIGPLAN Workshop on Types in Language Design and Implementation, pages 73-86, 2011. URL: https://doi.org/10.1145/1929553.1929565.
  27. Juliette Ponsonnet and François Pottier. Verified Persistent Catenable Deques. In JFLA 2026 - 37es Journées Francophones des Langages Applicatifs, volume JFLA 2026 - 37es Journées Francophones des Langages Applicatifs, Oberbronn, France, January 2026. Marie Kerjean and Yannick Zakowski. URL: https://hal.science/hal-05427954.
  28. François Pottier, Armaël Guéneau, Jacques-Henri Jourdan, and Glen Mével. Thunks and debits in separation logic with time credits. Proceedings of the ACM on Programming Languages, 8(POPL):1482-1508, 2024. URL: https://doi.org/10.1145/3632892.
  29. Neil Sarnak and Robert Endre Tarjan. Planar point location using persistent search trees. Commun. ACM, 29(7):669-679, July 1986. URL: https://doi.org/10.1145/6138.6151.
  30. Daniel Selsam, Simon Hudon, and Leonardo de Moura. Sealing pointer-based optimizations behind pure functions. Proceedings of the ACM on Programming Languages, 4(ICFP):1-20, 2020. URL: https://doi.org/10.1145/3408997.
  31. Hugo Simoes, Pedro Vasconcelos, Mário Florido, Steffen Jost, and Kevin Hammond. Automatic amortised analysis of dynamic memory allocation for lazy functional programs. In Proceedings of the 17th ACM SIGPLAN international conference on Functional programming, pages 165-176, 2012. URL: https://doi.org/10.1145/2364527.2364575.
  32. Robert Endre Tarjan. Amortized computational complexity. SIAM Journal on Algebraic Discrete Methods, 6(2):306-318, 1985. URL: https://doi.org/10.1137/0606031.
  33. Jean Vuillemin. A data structure for manipulating priority queues. Communications of the ACM, 21(4):309-315, 1978. URL: https://doi.org/10.1145/359460.359478.
  34. Li-yao Xia, Laura Israel, Maite Kramarz, Nicholas Coltharp, Koen Claessen, Stephanie Weirich, and Yao Li. Story of your lazy function’s life: A bidirectional demand semantics for mechanized cost analysis of lazy programs. Proc. ACM Program. Lang., 8(ICFP), August 2024. URL: https://doi.org/10.1145/3674626.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact