一句话：提出量子物理学家方法，扩展 AARA 类型系统，以更紧界分析栈等非单调资源。
论文提出“量子物理学家方法”（quantum physicist's method），用于改进摊销资源分析中的物理学家方法，从而更精确地分析非单调消耗的资源（如栈）。该方法包含 worldviews 与 resource tunneling，分别类比量子叠加与量子隧穿。作者将其用于扩展自动摊销资源分析（AARA）类型系统，使其能推导基于树深度的资源界，并引入 remainder contexts 以辅助线性类型系统的簿记。评估通过限制 OCaml 标准库 Set 模块函数的栈使用，与当前 AARA 实现相比，新系统以中等开销得到更紧的界。
We present a novel method for working with the physicist's method of amortized resource analysis, which we call the quantum physicist's method. These principles allow for more precise analyses of resources that are not monotonically consumed, like stack. This method takes its name from its two major features, worldviews and resource tunneling, which behave analogously to quantum superposition and quantum tunneling. We use the quantum physicist's method to extend the Automatic Amortized Resource Analysis (AARA) type system, enabling the derivation of resource bounds based on tree depth. In doing so, we also introduce remainder contexts, which aid bookkeeping in linear type systems. We then evaluate this new type system's performance by bounding stack use of functions in the Set module of OCaml's standard library. Compared to state-of-the-art implementations of AARA, our new system derives tighter bounds with only moderate overhead.
@article{paperbot1141,
title = {Automatic amortized resource analysis with the Quantum physicist’s method},
author = {David M. Kahn and Jan Hoffmann},
journal = {Proceedings of the ACM on Programming Languages},
volume = {5},
number = {ICFP},
year = {2021},
doi = {10.1145/3473581}
}