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.
翻译:我们提出了一个与物理学家的摊还资源分析方法合作的新方法,我们称之为量子物理学家的方法。这些原则使得能够更精确地分析非单质消耗的资源,如堆叠。这种方法取自其两个主要特征,即世界观和资源隧道,与量子叠加和量子隧道类似。我们使用量子物理学家的方法扩展自动摊还资源分析(AARA)类型系统,从而能够根据树深度得出资源界限。我们这样做,我们还引入了剩余环境,用于线型系统中的簿记。我们随后通过将OCaml标准图书馆的Set模块的功能捆绑在一起来评估这一新类型系统的性能。与AARA的标准图书馆的“Set ” 模块相比,我们的新系统有了更紧凑的边框,只有中度的顶端。