论文标题
多项式自动摊销资源分析的典型片段
Typable Fragments of Polynomial Automatic Amortized Resource Analysis
论文作者
论文摘要
作为用于资源分析的全自动技术，自动摊销资源分析（AARA）可能会因资源分析的不确定性而无法返回程序的最差成本范围。对于不熟悉AARA技术细节的程序员来说，很难预测是否可以在AARA中成功分析程序。在此问题的激励下，本文确定了可以在类型的多项式AARA中分析的程序类。首先，显示在单变量多项式AARA中键入的函数集与复杂性类Ptime一致。其次，本文为特征性提供了足够的条件，即公理上要求给定程序的每个子表达都是多项式时间。事实证明，这种情况意味着在某些句法限制下，多元多项式AARA中的特异性。
Being a fully automated technique for resource analysis, automatic amortized resource analysis (AARA) can fail in returning worst-case cost bounds of programs, fundamentally due to the undecidability of resource analysis. For programmers who are unfamiliar with the technical details of AARA, it is difficult to predict whether a program can be successfully analyzed in AARA. Motivated by this problem, this article identifies classes of programs that can be analyzed in type-based polynomial AARA. Firstly, it is shown that the set of functions that are typable in univariate polynomial AARA coincides with the complexity class PTIME. Secondly, the article presents a sufficient condition for typability that axiomatically requires every sub-expression of a given program to be polynomial-time. It is proved that this condition implies typability in multivariate polynomial AARA under some syntactic restrictions.
