Skew 堆和 Leftist 堆的自动摊销分析（扩充版）

我们研究纯函数式数据结构（如 skew 堆以及重量偏向和秩偏向的 leftist 堆）的完全自动摊销分析。为此，我们通过开发一种基于类型推断的通用方法来概括化早前关于自动摊销资源分析的工作，构建一个通用的类型系统。这使得能够进行模块化推理，并推断出精确且最优的成本界限。更具体地说，我们扩展了 Leutgeb 等人开发的 ATLAS 系统的工作，该系统用于覆盖 splay 树及其相关数据结构的分析。然而，为了实现对 skew 堆的分析，以及对更具挑战性的（摊销）leftist 堆的分析，我们在多个方向上开发了一系列新技术进行类型基自动分析。通过引入通用类型系统，我们允许任意（类）潜在函数的使用，与 ATLAS 中硬编码潜在函数的使用相比，这些工作已在 Haskell 中以完全模块化的方式实现。我们还大大增强了现有的类型推断算法，通过多个方向的扩展，包括路径敏感推理、数据结构不变量以及分段定义潜在函数的模板参数。我们展示了我们新开发的系统支持对分析 skew 堆和 leftist 堆的所有已知潜在函数，确认了已知界限。