Automated Expected Amortised Cost Analysis of Probabilistic Data Structures

TL;DR

This paper introduces the first fully automated expected amortised cost analysis for probabilistic self-adjusting data structures like splay trees and heaps, using a type-and-effect system with a prototype implementation.

Contribution

It presents a novel automated analysis method for probabilistic data structures, including a type system and soundness theorems, with a working prototype.

Findings

Successfully analyzed randomized splay trees and heaps automatically

Developed a type-and-effect system for cost analysis with probabilistic features

Provided soundness proofs for the analysis approach

Abstract

In this paper, we present the first fully-automated expected amortised cost analysis of self-adjusting data structures, that is, of randomised splay trees, randomised splay heaps and randomised meldable heaps, which so far have only (semi-) manually been analysed in the literature. Our analysis is stated as a type-and-effect system for a first-order functional programming language with support for sampling over discrete distributions, non-deterministic choice and a ticking operator. The latter allows for the specification of fine-grained cost models. We state two soundness theorems based on two different -- but strongly related -- typing rules of ticking, which account differently for the cost of non-terminating computations. Finally we provide a prototype implementation able to fully automatically analyse the aforementioned case studies.