基于量子物理学家方法的自动摊还资源分析
编程语言
2021-06-29 v1
摘要
我们提出了一种使用物理学家摊还资源分析方法的新方法，称之为量子物理学家方法。这些原理允许对如栈这类非单调消耗的资源进行更精确的分析。该方法因其两个主要特征——世界观和资源隧道——而得名，它们的行为分别类似于量子叠加和量子隧道。我们利用量子物理学家方法扩展了自动摊还资源分析（AARA）类型系统，从而能够基于树深度推导资源界限。在此过程中，我们还引入了剩余上下文，以辅助线性类型系统中的簿记。随后，我们通过界定OCaml标准库Set模块中函数的栈使用来评估这一新类型系统的性能。与最先进的AARA实现相比，我们的新系统以仅适度的开销推导出了更紧的界限。
引用
@article{arxiv.2106.13936,
title = {Automatic Amortized Resource Analysis with the Quantum Physicist's Method},
author = {David M Kahn and Jan Hoffmann},
journal= {arXiv preprint arXiv:2106.13936},
year = {2021}
}