Typable Fragments of Polynomial Automatic Amortized Resource Analysis

TL;DR

This paper explores classes of programs that can be automatically analyzed for resource bounds using polynomial AARA, linking typability to PTIME complexity and providing syntactic conditions for multivariate cases.

Contribution

It identifies program classes analyzable by type-based polynomial AARA and establishes a connection between typability and PTIME complexity, with syntactic criteria for multivariate analysis.

Findings

Univariate polynomial AARA typability coincides with PTIME.

A sufficient condition for typability involves polynomial-time sub-expressions.

Syntactic restrictions enable multivariate polynomial AARA typability.

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.