文章基本信息

标题：Typable Fragments of Polynomial Automatic Amortized Resource Analysis
本地全文：下载
作者：Long Pham ; Jan Hoffmann
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2021
卷号：183
页码：34:1-34:19
DOI：10.4230/LIPIcs.CSL.2021.34
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：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.
关键词：Resource consumption; Quantitative analysis; Amortized analysis; Typability