Automatic Amortized Resource Analysis with Regular Recursive Types
Automatic Amortized Resource Analysis with Regular Recursive Types
复制标题
DOI：
10.1109/lics56636.2023.10175720
复制
发表时间：
2023-04
期刊：
影响因子：
--
通讯作者：
Jessie Grosen;David M. Kahn;Jan Hoffmann
中科院分区：
文献类型：
--
作者：
Jessie Grosen;David M. Kahn;Jan Hoffmann
自动资源约束分析的目的是静态地推断出程序评估的资源消耗符号界限。自动资源分析的长期挑战是界限的推断，这些界限是复杂的自定义数据结构的功能。本文以基于类型的自动摊销资源分析（AARA）为基础，以应对这一挑战。 AARA基于摊销分析的潜在方法，并将与标准类型推断的结合推断使用其他线性约束求解，即使在推导非线性界限时也是如此。这样的界限来自资源函数，这些功能是数据结构大小的基本功能的线性组合，这些函数满足了某些闭合属性。在许多数据结构（例如列表）的AARA定义的资源函数上进行了自我提出的工作，但是是否暂时打开了此类功能是否存在于任意的功能数据结构。这项工作是通过统一构建由常规递归类型定义的代数数据结构的资源多项式来积极回答了这个问题的。这些功能是对所有先前提出的多项式资源函数的概括，可以看作是给定递归类型值的多项式的一般概念。 FPC的资源类型系统是一种具有递归类型的核心语言，展示了如何将资源多项式与AARA集成，同时保留了过去技术的所有好处。本文还建议使用新技术可简洁地说明这种类型系统的规则，并证明其与小步骤的语义相反。首先，多元潜在注释是根据自由半模型来说明的，大量抽象的注释介绍及其性质证明的细节。其次，逻辑关系为资源类型提供语义含义，可以通过单个诱导派生来证明声音证明。
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. Such bounds come from resource functions, which are linear combinations of basic functions of data structure sizes that fulfill certain closure properties.Previous work on AARA defined resource functions for many data structures such as lists of lists, but left open whether such functions exist for arbitrary data structures. This work answers this question 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 succinctly and proving it sound against a small-step cost semantics. 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.