# Exponential Automatic Amortized Resource Analysis

arXiv: https://arxiv.org/abs/2002.09519 · HTML: https://mlsanity.com/paper/2002.09519/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 21 Feb 2020.

## Built on by (most cited first, 1 of 1)

- [A Machine Learning-based Approach for Solving Recurrence Relations and its use in Cost Analysis of Logic Programs](https://mlsanity.com/paper/2405.06972/) (2024)

## Abstract (arXiv)

Automatic amortized resource analysis (AARA) is a type-based technique for inferring concrete (non-asymptotic) bounds on a program's resource usage. Existing work on AARA has focused on bounds that are polynomial in the sizes of the inputs. This paper presents and extension of AARA to exponential bounds that preserves the benefits of the technique, such as compositionality and efficient type inference based on linear constraint solving. A key idea is the use of the Stirling numbers of the second kind as the basis of potential functions, which play the same role as the binomial coefficients in polynomial AARA. To formalize the similarities with the existing analyses, the paper presents a general methodology for AARA that is instantiated to the polynomial version, the exponential version, and a combined system with potential functions that are formed by products of Stirling numbers and binomial coefficients. The soundness of exponential AARA is proved with respect to an operational cost semantics and the analysis of representative example programs demonstrates the effectiveness of the new analysis.