AI 中文总结
该研究在Calf中综合物理学家和银行家对摊销分析的视角，提出断裂和粘合定理，构造类型运算符，定义Giralf理论，并用推理算法实现Calf程序成本分析自动化。
AI 中文摘要
摊销分析可以从物理学家的视角构建，便于在依赖类型理论中使用势函数进行人工验证，也可以从银行家的视角构建，便于在子结构类型理论中使用类型级信用注释进行自动推理。在这项工作中，我们在Calf（一种依赖类型理论成本验证工具）中综合了这些观点。从物理学家的视角，我们提出了一个断裂和粘合定理，使每种类型都包含一个抽象函数和一个势函数的融合。通过构造，两种这样的类型之间的每个程序都必须保留抽象以促进行为的模块化，并保留势以促进成本的模块化。结合银行家的视角，我们综合构造了用于信用和借记的类型运算符。然后我们定义了Giralf，一种用于使用信用和借记进行编程的分级子结构依赖类型理论，其语义被解释为Calf的子语言。最后，我们采用一种推理算法将一类有限的Calf程序转换为Giralf对应程序，从而实现Calf中常见算法成本分析的自动化。
英文摘要
Amortized analysis can be framed from the physicist's view, amenable to manual verification in dependent type theory using potential functions, and the banker's view, amenable to automated inference in substructural type theory using type-level credit annotations. In this work, we synthesize these perspectives in Calf, a dependent type theory cost verification. From the physicist's view, we present a fracture and gluing theorem that renders every type as containing a fusion of an abstraction function and a potential function. By construction, every program between two such types must preserve abstraction, to facilitate modularity of behavior, and conserve potential, to facilitate modularity of cost. Incorporating the banker's view, we synthetically construct type operators for credits and debits. We then define Giralf, a graded substructural dependent type theory for programming with credits and debits, which is semantically interpreted as a sub-language of Calf. Finally, we adapt an inference algorithm to transform a limited class of Calf programs into Giralf counterparts, automating the cost analysis of common algorithms in Calf.
