Denotational recurrence extraction for amortized analysis
Joseph W. Cutler, Daniel R. Licata, Norman Danner

TL;DR
This paper extends denotational recurrence extraction techniques to support amortized analysis in functional programs, enabling more precise complexity bounds through a new language and logical relations.
Contribution
It introduces an affine-typed language with amortized annotations, a recurrence translation, and a denotational semantics for solving amortized recurrences.
Findings
Correctness of recurrence extraction for amortized analysis proven
Application to binary counters and splay trees demonstrated
Supports higher-order functions with formal guarantees
Abstract
A typical way of analyzing the time complexity of functional programs is to extract a recurrence expressing the running time of the program in terms of the size of its input, and then to solve the recurrence to obtain a big-O bound. For recurrence extraction to be compositional, it is also necessary to extract recurrences for the size of outputs of helper functions. Previous work has developed techniques for using logical relations to state a formal correctness theorem for a general recurrence extraction translation: a program is bounded by a recurrence when the operational cost is bounded by the extracted cost, and the output value is bounded, according to a value bounding relation defined by induction on types, by the extracted size. This previous work supports higher-order functions by viewing recurrences as programs in a lambda-calculus, or as mathematical entities in a denotational…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
