Type-Based Analysis of Logarithmic Amortised Complexity

TL;DR

This paper presents a type-based, potential method for analyzing logarithmic amortised complexity, enabling automated analysis of self-adjusting data structures like splay trees.

Contribution

It introduces the first type system with logarithmic potential functions for automated amortised complexity analysis.

Findings

Successfully analyzed splay tree splaying operation

First to automate logarithmic amortised analysis

Prototype implementation demonstrates practical applicability

Abstract

We introduce a novel amortised resource analysis couched in a type-and-effect system. Our analysis is formulated in terms of the physicist's method of amortised analysis, and is potential-based. The type system makes use of logarithmic potential functions and is the first such system to exhibit *logarithmic amortised complexity*. With our approach we target the automated analysis of self-adjusting data structures, like splay trees, which so far have only manually been analysed in the literature. In particular, we have implemented a semi-automated prototype, which successfully analyses the zig-zig case of *splaying*, once the type annotations are fixed.