We study the fully automated amortised analysis of purely functional data structures like skew heaps, as well as weight- and rank-biased leftist heaps. For that we generalise earlier works on automated amortised resource analysis by developing a type inference based approach with a generic type system. This allows for modular reasoning and the inference of precise and optimal cost bounds. More specifically, we extend the work on the ATLAS system by Leutgeb et al. which was developed to cover the analysis of splay trees and some closely related data structures. To enable the analysis of skew heaps, however, and the even more challenging (amortised) analysis of leftist heaps, we have developed a range of new techniques for type-based automated analysis. By introducing a generic type system we allow for arbitrary (classes of) potential functions, compared to the use of hard-coded potential functions in ATLAS, which we have implemented in Haskell in an entirely modular way. We have also greatly enhanced the existing type inference algorithm by extensions in multiple directions, including path-sensitive reasoning, data structure invariants, and template parameters for piecewise defined potential functions. We show how our newly developed system supports the use of all known potential functions for analysing skew heaps and leftist heaps, confirming the known bounds.

翻译：我们研究纯函数式数据结构（如倾斜堆以及权重偏向和秩偏向的左偏堆）的完全自动化摊销分析。为此，我们通过开发基于类型推断的通用类型系统，拓展了早期关于自动摊销资源分析的研究工作，从而实现模块化推理以及精确且最优代价边界的推断。具体而言，我们扩展了Leutgeb等人针对ATLAS系统的工作，该系统最初设计用于分析伸展树及若干紧密相关的数据结构。为支持倾斜堆的分析以及更具挑战性的左偏堆（摊销）分析，我们开发了一系列基于类型的自动分析新技术。通过引入通用类型系统，我们允许使用任意（类别的）势函数（相较于ATLAS中硬编码的势函数），并以完全模块化的方式在Haskell中实现。我们还在多个方向上对现有类型推断算法进行了重大增强，包括路径敏感推理、数据结构不变量以及分段定义势函数的模板参数。我们展示了新开发的系统如何支持所有已知用于分析倾斜堆和左偏堆的势函数，并验证了已知的代价边界。