基于类型的对数摊还复杂度分析
计算机科学中的逻辑
2023-03-06 v2 编程语言
摘要
我们引入了一种新颖的摊还资源分析，其构建于类型与效应系统之中。我们的分析以物理学家的摊还分析方法表述，且基于势函数。该类型系统利用对数势函数，是首个展现*对数摊还复杂度*的此类系统。通过我们的方法，我们旨在对自调整数据结构（如伸展树）进行自动化分析，此类结构迄今仅在文献中被手动分析。特别地，我们实现了一个半自动化原型，一旦类型标注固定，它便能成功分析*伸展*的 zig-zig 情形。
引用
@article{arxiv.2101.12029,
title = {Type-Based Analysis of Logarithmic Amortised Complexity},
author = {Martin Hofmann and Lorenz Leutgeb and Georg Moser and David Obwaller and Florian Zuleger},
journal= {arXiv preprint arXiv:2101.12029},
year = {2023}
}
备注
35 pages. arXiv admin note: text overlap with arXiv:1807.08242