Typable Fragments of Polynomial Automatic Amortized Resource Analysis
Abstract
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.
Cite
@article{arxiv.2010.16353,
title = {Typable Fragments of Polynomial Automatic Amortized Resource Analysis},
author = {Long Pham and Jan Hoffmann},
journal= {arXiv preprint arXiv:2010.16353},
year = {2020}
}
Comments
This is the full version of our CSL 2021 paper