The goal of automatic resource bound analysis is to statically infer symbolic bounds on the resource consumption of the evaluation of a program. A longstanding challenge for automatic resource analysis is the inference of bounds that are functions of complex custom data structures. This article builds on type-based automatic amortized resource analysis (AARA) to address this challenge. AARA is based on the potential method of amortized analysis and reduces bound inference to standard type inference with additional linear constraint solving, even when deriving non-linear bounds. A key component of AARA is resource functions that generate the space of possible bounds for values of a given type while enjoying necessary closure properties. Existing work on AARA defined such functions for many data structures such as lists of lists but the question of whether such functions exist for arbitrary data structures remained open. This work answers this questions positively by uniformly constructing resource polynomials for algebraic data structures defined by regular recursive types. These functions are a generalization of all previously proposed polynomial resource functions and can be seen as a general notion of polynomials for values of a given recursive type. A resource type system for FPC, a core language with recursive types, demonstrates how resource polynomials can be integrated with AARA while preserving all benefits of past techniques. The article also proposes the use of new techniques useful for stating the rules of this type system and proving it sound. First, multivariate potential annotations are stated in terms of free semimodules, substantially abstracting details of the presentation of annotations and the proofs of their properties. Second, a logical relation giving semantic meaning to resource types enables a proof of soundness by a single induction on typing derivations.

翻译：自动资源边界分析的目标是静态推断程序求值过程中资源消耗的符号上界。如何为复杂自定义数据结构推断边界函数，一直是该领域长期面临的挑战。本文基于类型化自动摊销资源分析（AARA）方法应对这一挑战。AARA基于摊销分析的势能方法，将边界推断问题转化为标准类型推断与线性约束求解的组合，即便在推导非线性边界时亦能如此。其核心构件是资源函数，该函数在保持必要闭包性质的同时，为给定类型的值生成可能的边界空间。现有AARA工作已为列表的列表等多种数据结构定义了此类函数，但关于任意数据结构是否存在此类函数的问题始终悬而未决。本研究通过为正则递归类型定义的代数数据结构统一构造资源多项式，给出了肯定回答。这些函数是此前所有多项式资源函数的泛化形式，可视为给定递归类型值的多项式通解。针对支持递归类型的核心语言FPC，本文构建了资源类型系统，展示了如何将资源多项式与AARA框架整合，同时保留过往技术的全部优势。本文还提出若干新技术用于定义该类型系统的规则并证明其可靠性：其一，采用自由半模表示多元势能标注，显著抽象了标注呈现方式及其性质证明的细节；其二，通过为资源类型赋予语义含义的逻辑关系，实现了基于类型推导单次归纳的可靠性证明框架。