指数自动摊销资源分析
Exponential Automatic Amortized Resource Analysis
摘要：
自动摊销资源分析（AARA）是一种基于类型的技术，用于推断程序资源使用的具体（非渐近）界限。AARA的现有工作集中在输入大小为多项式的边界上。本文提出并扩展AARA的指数界，保留了该技术的优点，如组合性和有效的类型推断的基础上线性约束求解。一个关键的想法是使用第二类斯特林数作为潜在的功能，发挥相同的作用，多项式AARA中的二项式系数的基础。为了形式化与现有的分析的相似性，本文提出了一种通用的方法AARA，实例化的多项式版本，指数版本，并与潜在的功能，由斯特林数和二项式系数的产品形成的组合系统。指数AARA的合理性证明了相对于操作成本语义和代表性的例子程序的分析表明了新的分析的有效性。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
