2026-07-26T02:22:24Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:13468 2024-03-06T10:52:09Z ddc:004 open_access

Typable Fragments of Polynomial Automatic Amortized Resource Analysis Pham, Long Hoffmann, Jan Resource consumption Quantitative analysis Amortized analysis Typability 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Long Pham and Jan Hoffmann 2021 Is Part Of LIPIcs, Volume 183, 29th EACSL Annual Conference on Computer Science Logic (CSL 2021) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CSL.2021.34 urn:nbn:de:0030-drops-134681 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.34 eng https://creativecommons.org/licenses/by/3.0/legalcode