论文标题
自动化的概率数据结构的预期摊销成本分析
Automated Expected Amortised Cost Analysis of Probabilistic Data Structures
论文作者
论文摘要
在本文中，我们介绍了自我调整数据结构的第一个完全自动化的预期摊销成本分析，即随机张开树，随机的张开堆和随机的粘堆堆，到目前为止，在文献中只对其进行了（半）手动分析。我们的分析被称为一阶功能编程语言的类型和效应系统，并支持对离散分布，非确定性选择和滴答操作员进行采样。后者允许对细粒成本模型进行规范。我们根据两个不同但相关的打字规则陈述了两个合理定理，这些规则以不同终止计算的成本为不同。最后，我们提供了一个原型实施，能够完全自动分析上述案例研究。
In this paper, we present the first fully-automated expected amortised cost analysis of self-adjusting data structures, that is, of randomised splay trees, randomised splay heaps and randomised meldable heaps, which so far have only (semi-) manually been analysed in the literature. Our analysis is stated as a type-and-effect system for a first-order functional programming language with support for sampling over discrete distributions, non-deterministic choice and a ticking operator. The latter allows for the specification of fine-grained cost models. We state two soundness theorems based on two different -- but strongly related -- typing rules of ticking, which account differently for the cost of non-terminating computations. Finally we provide a prototype implementation able to fully automatically analyse the aforementioned case studies.
