arxiv: 2605.12091 · v1 · submitted 2026-05-12 · 💻 cs.PL

Recognition: 2 theorem links

· Lean Theorem

Automated Amortised Analysis of Skew Heaps and Leftist Heaps (Extended Version)

Armin Walch , Georg Moser , Berry Schoenmakers , Florian Zuleger

Authors on Pith no claims yet

Pith reviewed 2026-05-13 04:28 UTC · model grok-4.3

classification 💻 cs.PL

keywords amortised analysisskew heapsleftist heapstype inferencepotential functionsfunctional programmingresource analysisautomated verification

0 comments

The pith

A generic type system enables automated amortised analysis of skew heaps and leftist heaps using arbitrary potential functions.

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

The paper develops a type inference approach with a generic type system for analyzing the amortized costs of purely functional data structures, specifically skew heaps and weight- and rank-biased leftist heaps. This generalizes earlier methods by supporting arbitrary potential functions instead of hard-coded ones. The system incorporates new techniques including path-sensitive reasoning, encoding of data structure invariants, and template parameters for piecewise potential functions. These extensions allow the inference of precise and optimal cost bounds in a modular way. A sympathetic reader would care because it reduces the manual effort required to prove resource bounds for complex data structures.

Core claim

By developing a generic type system and extending the type inference algorithm with path sensitivity, data structure invariants, and templates for piecewise potentials, the approach supports the encoding and use of all known potential functions for skew heaps and leftist heaps, thereby confirming the known amortized bounds through fully automated analysis.

What carries the argument

The generic type system, which permits arbitrary classes of potential functions and is implemented in a modular way, combined with enhancements to the inference algorithm for handling invariants and templates.

If this is right

Optimal amortized bounds can be inferred automatically for skew heaps.
Both weight-biased and rank-biased variants of leftist heaps can be analyzed automatically.
The known manual bounds for these structures are reproduced by the automated system.
Modular reasoning becomes possible for data structures with complex invariants.
The method extends previous type-based analyses to a broader class of potential functions.

Where Pith is reading between the lines

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

This could enable rapid experimentation with novel potential functions via the template mechanism.
The path-sensitive analysis might help with other data structures involving conditional behaviors.
Future extensions could target additional functional data structures beyond heaps.

Load-bearing premise

The generic type system correctly encodes the required data-structure invariants and potential function templates for skew and leftist heaps without introducing unsound approximations.

What would settle it

If the implemented system fails to derive the known optimal bounds when applied to the standard definitions of skew heaps or leftist heaps, or if it produces unsound bounds, the claim would be falsified.

Figures

Figures reproduced from arXiv: 2605.12091 by Armin Walch, Berry Schoenmakers, Florian Zuleger, Georg Moser.

**Figure 1.** Figure 1: Amortised cost of meld and delete_min operations for leftist heaps, for different potential functions Φ, inferred by our prototype implementation. – We have developed a generic type system for amortised cost analysis that on the one hand can be instantiated to obtain the previous ATLAS tool and on the other hand easily generalizes to new classes of potential functions. – We extend the existing type inferen… view at source ↗

**Figure 2.** Figure 2: Purely functional leftist heap implementation with three different balanc [PITH_FULL_IMAGE:figures/full_fig_p005_2.png] view at source ↗

**Figure 3.** Figure 3: Abstract syntax of our (first-order) core language. Expressions are de [PITH_FULL_IMAGE:figures/full_fig_p007_3.png] view at source ↗

**Figure 4.** Figure 4: Evaluation rules for the big-step cost semantics. [PITH_FULL_IMAGE:figures/full_fig_p008_4.png] view at source ↗

**Figure 5.** Figure 5: Syntax-directed type rules. 4.2 Well-Typed Programs A program P is a finite set of function definitions. Our analysis computes, for each function f(x) = e ∈ P, two sets of signatures: F(f) and F cf(f). We write x: α as shorthand for the sequence of bindings x1 : α1, . . . , xn : αn. For each costed signature x: α|Ψ → ν : β|Φ ∈ F(f), we require the type judgement x: α|Ψ ⊢ e: β|Φ to hold. These signatures ac… view at source ↗

**Figure 6.** Figure 6: Structural type rules. types and potential functions; our extensions are highlighted in grey . While the syntax-directed rules involve only equality constraints—ensuring that potential and cost are always preserved—we also require a set of structural rules. In contrast they can modify or discard potential and may, in principle, be applied at any point in the type derivation. Example Derivation. To develop… view at source ↗

**Figure 7.** Figure 7: Constraints defining C Lsol,p Match(Q, Q′ , P, R,(Γ, x:T),(Γ, t:T, u:T)), where x = dom(Γ), xi ∈ dom(Γ) and [p] denotes the Iverson bracket for predicate p, i.e. [p] = 1 if p holds and [p] = 0. where C = C1 ∪ C2 ∪ CLsol,p Match(Q, Q′ , P, R,(Γ, x:T),(Γ, t:T, u:T)). Note that we omit a: B from the typing context in the node case because Lsol,p is only defined on trees — the elements themselves do not carry … view at source ↗

**Figure 8.** Figure 8: Constraint generating functions for Lpw where x = dom(Γ), y = z = dom(∆) and x1, x2 ⊆ x. x, ¯ y¯ denote (possibly empty) sequences of variables. Expert Knowledge. To support the optimal golden-ratio bound for skew heaps and weight-biased leftist heaps, we generalise Lemma 1 and obtain the following result. Lemma 5. Let a, b > 0. Then, (a + b) log2 (x + y) ⩾ a log2 x + b log2 y + 1 for all x, y > 0 if and o… view at source ↗

**Figure 9.** Figure 9: Constraint generating functions for Lrank, where xi ∈ dom Γ and yi ∈ dom(∆). 6.3 Rank Potential For the analysis of rank-biased leftist heaps we introduce the following template language, whose constraint generators are given in [PITH_FULL_IMAGE:figures/full_fig_p019_9.png] view at source ↗

**Figure 10.** Figure 10: Template language agnostic constraint generating functions. [PITH_FULL_IMAGE:figures/full_fig_p025_10.png] view at source ↗

**Figure 11.** Figure 11: Constraint generating functions for Llog, where x = dom(Γ) and y = dom(∆) [PITH_FULL_IMAGE:figures/full_fig_p026_11.png] view at source ↗

**Figure 12.** Figure 12: Constraint generating functions for Lsol,p, where x = dom(Γ) and xi ∈ dom(Γ). [p] denotes the Iverson bracket for predicate p, i.e. [p] = 1 if p holds and [p] = 0. Lemma 8. Ψmix(Γ, ∆) = X b̸=0,a̸=0∨c̸=0 q(ax,by,c) log2 (a|x| + b|y| + c) = X b̸=0,a̸=0∨c̸=0 X d̸=0∨e̸=0 p (b,d,e) (ax,c) log2 (a|x| + b|y| + c) = X b̸=0,d̸=0∨e̸=0 X a̸=0∨c̸=0 p (b,d,e) (ax,c) log2 (a|x| + b|y| + c) ⩾ X b̸=0,d̸=0∨e̸=0 p ′(b,d,e)… view at source ↗

**Figure 13.** Figure 13: Partial type derivation of meld, showcasing potential “borrowing”. Lifting of Iverson Terms. The next interesting step lifts the potential [|t| > |u|+|y|−1] through the let-bound recursive call meld u y to the binding variable z, in order to pay [|t| > |z|] to construct the result node. We remember that T-Let has the obligation Ψmix(Γ, ∆) ⩾ Ω(x: α, ∆), concerning terms that mix variables from the binding … view at source ↗

read the original abstract

We study the fully automated amortised analysis of purely functional data structures like skew heaps, as well as weight- and rank-biased leftist heaps. For that we generalise earlier works on automated amortised resource analysis by developing a type inference based approach with a generic type system. This allows for modular reasoning and the inference of precise and optimal cost bounds. More specifically, we extend the work on the ATLAS system by Leutgeb et al. which was developed to cover the analysis of splay trees and some closely related data structures. To enable the analysis of skew heaps, however, and the even more challenging (amortised) analysis of leftist heaps, we have developed a range of new techniques for type-based automated analysis. By introducing a generic type system we allow for arbitrary (classes of) potential functions, compared to the use of hard-coded potential functions in ATLAS, which we have implemented in Haskell in an entirely modular way. We have also greatly enhanced the existing type inference algorithm by extensions in multiple directions, including path-sensitive reasoning, data structure invariants, and template parameters for piecewise defined potential functions. We show how our newly developed system supports the use of all known potential functions for analysing skew heaps and leftist heaps, confirming the known bounds.

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

This paper generalizes the ATLAS type system to automate amortized analysis for skew heaps and leftist heaps, recovering the known bounds.

read the letter

The main thing to know is that the authors extend automated amortized analysis beyond splay trees to skew heaps and both weight- and rank-biased leftist heaps. They do this by replacing the hardcoded potentials in the earlier ATLAS work with a generic type system that accepts arbitrary classes of potential functions, then adding path-sensitive rules, explicit data-structure invariants, and template parameters for piecewise potentials. The Haskell implementation is reported to infer the standard textbook bounds on the canonical examples without manual intervention. The stress-test note confirms the argument stays internally consistent and introduces no hidden approximations. What the paper does well is keep the extension modular and targeted: the new features directly address the invariants that make leftist heaps harder than splay trees, and the results line up with the potentials already in the literature. The work is confirmatory rather than discovery-oriented, which is fine for an automation paper but limits how far it moves the frontier. The soft spots are modest. Because the potentials are taken from prior manual analyses, the main claim rests on faithful encoding rather than new bound discovery; a referee might ask for more detail on how the template parameters avoid over-approximation in the piecewise cases. No load-bearing soundness gaps appear in the description. This paper is for researchers working on type-based resource analysis or on functional data structures that rely on these heaps. A reader who needs concrete evidence that the extended inference can discharge the required invariants will get value from it. The technical extensions are non-trivial and the examples are reproducible in principle, so the paper deserves a serious referee. I would send it to peer review.

Referee Report

0 major / 3 minor

Summary. The manuscript presents a generic type system for amortised resource analysis of purely functional data structures, generalizing the ATLAS system to support arbitrary classes of potential functions in a modular Haskell implementation. It extends the type inference algorithm with path-sensitive reasoning, data-structure invariants, and template parameters for piecewise-defined potentials. The system is applied to skew heaps and both weight-biased and rank-biased leftist heaps, recovering all known potential functions from the literature and confirming the textbook amortised bounds without manual intervention or post-hoc adjustments.

Significance. If the claims hold, the work meaningfully advances automated amortised analysis by handling data structures whose invariants and potentials are more intricate than those covered by prior hard-coded systems. The modular design, explicit side conditions preserving standard accounting, and reported success on canonical examples constitute concrete strengths; the provision of an implementation and falsifiable example outcomes aids reproducibility.

minor comments (3)

The description of how template parameters interact with the path-sensitive rules (around the extensions to the inference algorithm) would benefit from a small worked example using one of the leftist-heap potentials to illustrate the side conditions.
A compact table summarizing the recovered bounds versus the textbook bounds for each heap variant and each potential function would improve readability and make the confirmation claim easier to verify at a glance.
The paper should explicitly state in the main text (rather than only in the implementation section) that the potential-function templates are taken directly from the literature without fitting or approximation inside the tool.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive assessment of our manuscript, the accurate summary of its contributions, and the recommendation for minor revision. No specific major comments were raised in the report.

Circularity Check

0 steps flagged

No significant circularity

full rationale

The paper generalises the ATLAS system by introducing a generic type system parameterised over arbitrary classes of potential functions taken from the existing literature on skew and leftist heaps. It extends the type inference algorithm with path-sensitive rules, data-structure invariants, and template parameters, then reports that the resulting implementation successfully encodes and discharges the known potentials and invariants to recover the textbook amortised bounds. Because the potential functions themselves are external inputs rather than fitted or redefined inside the derivation, and the central result is verification of pre-existing bounds on canonical examples, no step reduces to its own inputs by construction.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The approach rests on the existence of suitable potential functions for the heaps and on the soundness of the underlying type system for amortized analysis; no new free parameters or invented entities are mentioned in the abstract.

axioms (1)

domain assumption The type system correctly encodes the data-structure invariants and potential functions used in prior manual analyses of skew and leftist heaps.
The abstract claims the system supports all known potential functions, which presupposes that those functions can be represented inside the generic type system.

pith-pipeline@v0.9.0 · 5529 in / 1269 out tokens · 60871 ms · 2026-05-13T04:28:31.984520+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/Constants/AlphaDerivationExplicit.lean phi_golden_ratio 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.

the exact bound for meld has been shown to be log_ϕ(|x|+|y|), where ϕ denotes the golden ratio [13]
IndisputableMonolith/Cost/FunctionalEquation.lean washburn_uniqueness_aczel 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.

Φϕ(t) + 105/163 log2(|t|+|u|) − 105/163 log2|t| + Φϕ(u)

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

29 extracted references · 29 canonical work pages

[1]

Journal of Experimental Algorithmics (JEA)3, 2–es (1998).https://doi.org/10

Cho, S., Sahni, S.: Weight-biased leftist trees and modified skip lists. Journal of Experimental Algorithmics (JEA)3, 2–es (1998).https://doi.org/10. 1145/297096.297111

work page arXiv 1998
[2]

MIT press (2022)

Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: Introduction to al- gorithms. MIT press (2022)

work page 2022
[3]

PhD thesis, Computer Science, Stanford University, CA (1972)

Crane, C.A.: Linear Lists and Priority Queues as Balanced Binary Trees. PhD thesis, Computer Science, Stanford University, CA (1972). Automated Amortised Analysis of Skew Heaps and Leftist Heaps 21

work page 1972
[5]

Palgrave (2003)

Gibbons, J., de Moor, O.: The Fun of Programming. Palgrave (2003)

work page 2003
[6]

ACM Transactions on Algorithms (TALG)11(4), 1–26 (2015).https : / / doi

Haeupler, B., Sen, S., Tarjan, R.E.: Rank-balanced trees. ACM Transactions on Algorithms (TALG)11(4), 1–26 (2015).https : / / doi . org / https : //doi.org/10.1145/2689412

work page doi:10.1145/2689412 2015
[7]

In: Proceedings of the 38th annual ACM SIGPLAN-SIGACT sym- posium on Principles of programming languages, pp

Hoffmann, J., Aehlig, K., Hofmann, M.: Multivariate amortized resource analysis. In: Proceedings of the 38th annual ACM SIGPLAN-SIGACT sym- posium on Principles of programming languages, pp. 357–370 (2011).https: //doi.org/10.1145/1926385.1926427

work page doi:10.1145/1926385.1926427 2011
[8]

Hoffmann, J., Hofmann, M.: Amortized resource analysis with polynomial potential: A static inference of polynomial bounds for functional programs. In: Programming Languages and Systems: 19th European Symposium on Programming, ESOP 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-...

work page 2010
[9]

Hofmann, M., Jost, S.: Static prediction of heap space usage for first-order functionalprograms.ACMSIGPLANNotices38(1),185–197(2003).https: //doi.org/10.1145/640128.604148

work page doi:10.1145/640128.604148 2003
[10]

Mathematical Structures in Computer Science32(6), 794–826 (2022)

Hofmann, M., Leutgeb, L., Obwaller, D., Moser, G., Zuleger, F.: Type-based analysis of logarithmic amortised complexity. Mathematical Structures in Computer Science32(6), 794–826 (2022)

work page 2022
[11]

In: Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp

Jost, S., Hammond, K., Loidl, H.-W., Hofmann, M.: Static determination of quantitative resource usage for higher-order programs. In: Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp. 223–236 (2010).https://doi.org/10.1145/ 1706299.1706327

work page arXiv 2010
[12]

Kahn, D.M., Hoffmann, J.: Exponential automatic amortized resource anal- ysis. In: Foundations of Software Science and Computation Structures: 23rd International Conference, FOSSACS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25–30, 2020, Proceedings 23, pp. 359–380 (2020).htt...

work page doi:10.1007/978-3-030-45231-5_19 2020
[13]

Information Processing Letters37(5), 265–271 (1991)

Kaldewaij, A., Schoenmakers, B.: The derivation of a tighter bound for top- down skew heaps. Information Processing Letters37(5), 265–271 (1991). https://doi.org/10.1016/0020-0190(91)90218-7

work page doi:10.1016/0020-0190(91)90218-7 1991
[14]

Addison Wesley Longman Publishing Co., Inc., USA (1998)

Knuth, D.E.: The art of computer programming, volume 3: (2nd ed.) sorting and searching. Addison Wesley Longman Publishing Co., Inc., USA (1998)

work page 1998
[15]

In: Computer Aided Verifica- tion: 33rd International Conference, CAV 2021, Virtual Event, July 20–23, 22 A

Leutgeb, L., Moser, G., Zuleger, F.: ATLAS: automated amortised complex- ity analysis of self-adjusting data structures. In: Computer Aided Verifica- tion: 33rd International Conference, CAV 2021, Virtual Event, July 20–23, 22 A. Walch et al. 2021, Proceedings, Part II 33, pp. 99–122 (2021).https://doi.org/10. 1007/978-3-030-81688-9_5

work page 2021
[16]

In: International Conference on Computer Aided Verification, pp

Leutgeb, L., Moser, G., Zuleger, F.: Automated expected amortised cost analysis of probabilistic data structures. In: International Conference on Computer Aided Verification, pp. 70–91 (2022).https : / / doi . org / 10 . 1007/978-3-031-13188-2_4

work page 2022
[17]

Journal of Auto- mated Reasoning62, 367–391 (2019).https://doi.org/10.1007/s10817- 018-9459-3

Nipkow, T., Brinkop, H.: Amortized complexity verified. Journal of Auto- mated Reasoning62, 367–391 (2019).https://doi.org/10.1007/s10817- 018-9459-3

work page doi:10.1007/s10817- 2019
[18]

Cambridge University Press (1998)

Okasaki, C.: Purely functional data structures. Cambridge University Press (1998)

work page 1998
[19]

Cambridge University Press (1998)

Reynolds, J.C.: Theories of programming languages. Cambridge University Press (1998)

work page 1998
[20]

In: Proceedings of the 29th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp

Rondon, P.M., Kawaguci, M., Jhala, R.: Liquid types. In: Proceedings of the 29th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 159–169 (2008).https : / / doi . org / 10 . 1145 / 1379022.1375602

work page arXiv 2008
[21]

PhD thesis, Math & CS, TU Eindhoven, Netherlands (1992)

Schoenmakers, B.: Data Structures and Amortized Complexity in a Func- tional Setting. PhD thesis, Math & CS, TU Eindhoven, Netherlands (1992)

work page 1992
[22]

Informa- tion processing letters61(5), 279–284 (1997).https://doi.org/10.1016/ s0020-0190(97)00028-8

Schoenmakers, B.: A tight lower bound for top-down skew heaps. Informa- tion processing letters61(5), 279–284 (1997).https://doi.org/10.1016/ s0020-0190(97)00028-8

work page 1997
[23]

In: Principles of Verification:CyclingtheProbabilisticLandscape:EssaysDedicatedtoJoost- Pieter Katoen on the Occasion of His 60th Birthday, Part I, pp

Schoenmakers, B.: Amortized Analysis of Leftist Heaps. In: Principles of Verification:CyclingtheProbabilisticLandscape:EssaysDedicatedtoJoost- Pieter Katoen on the Occasion of His 60th Birthday, Part I, pp. 73–84. Springer (2024).https://doi.org/10.1007/978-3-031-75783-9_3

work page doi:10.1007/978-3-031-75783-9_3 2024
[24]

In: Proceedings of the 17th ACM SIGPLAN international conference on Functional programming, pp

Simoes, H., Vasconcelos, P., Florido, M., Jost, S., Hammond, K.: Automatic amortised analysis of dynamic memory allocation for lazy functional pro- grams. In: Proceedings of the 17th ACM SIGPLAN international conference on Functional programming, pp. 165–176 (2012).https://doi.org/10. 1145/2398856.2364575

work page arXiv 2012
[25]

Sleator and Robert E

Sleator, D.D., Tarjan, R.E.: Self-adjusting binary search trees. Journal of the ACM (JACM)32(3), 652–686 (1985).https : / / doi . org / 10 . 1145 / 3828.3835

work page arXiv 1985
[26]

SIAM Journal on Com- puting15(1), 52–69 (1986).https://doi.org/10.1137/0215004

Sleator, D.D., Tarjan, R.E.: Self-adjusting heaps. SIAM Journal on Com- puting15(1), 52–69 (1986).https://doi.org/10.1137/0215004

work page doi:10.1137/0215004 1986
[27]

SIAM Journal on Alge- braic Discrete Methods6(2), 306–318 (1985).https://doi.org/10.1137/ 0606031

Tarjan, R.E.: Amortized computational complexity. SIAM Journal on Alge- braic Discrete Methods6(2), 306–318 (1985).https://doi.org/10.1137/ 0606031

work page 1985
[28]

Vasconcelos, P., Jost, S., Florido, M., Hammond, K.: Type-based allocation analysis for co-recursion in lazy functional languages. In: Programming Lan- guages and Systems: 24th European Symposium on Programming, ESOP 2015, Held as Part of the European Joint Conferences on Theory and Prac- tice of Software, ETAPS 2015, London, UK, April 11-18, 2015, Procee...

work page doi:10.1007/978- 2015
[29]

209–228 (2013).https://doi.org/10

Vazou,N.,Rondon,P.M.,Jhala,R.:Abstractrefinementtypes.In:European Symposium on Programming, pp. 209–228 (2013).https://doi.org/10. 1007/978-3-642-37036-6_13

work page 2013
[30]

borrowing

Wang, D., Kahn, D.M., Hoffmann, J.: Raising expectations: automating ex- pected cost analysis with types. Proceedings of the ACM on Programming Languages4(ICFP), 1–31 (2020).https://doi.org/10.1145/3408992 24 A. Walch et al. Table 2: Exact cost bounds ofmeldanddelete_minfor skew and leftist heaps. Potentialmeld delete_min skew heap Φ[t<u] log2(|y|+|x| −1)...

work page doi:10.1145/3408992 2020