Automatic Amortized Resource Analysis with the Quantum Physicist's Method

TL;DR

This paper introduces the quantum physicist's method, an extension of Automatic Amortized Resource Analysis, which improves resource bounds estimation for non-monotonically consumed resources like stacks using concepts inspired by quantum physics.

Contribution

The paper presents a novel extension to AARA incorporating worldviews and resource tunneling, enabling more precise resource analysis for complex data structures.

Findings

Derives tighter resource bounds compared to existing AARA methods.

Successfully applies the method to bound stack use in OCaml's Set module.

Maintains moderate computational overhead in analysis.

Abstract

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.