Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Automated Expected Amortised Cost Analysis of Probabilistic Data Structures

Lorenz Leutgeb, Georg Moser, Florian Zuleger

TL;DR

This work presents the first fully-automated framework for computing expected amortised costs of probabilistic self-adjusting data structures via a specialized type-and-effect system. It introduces a probabilistic functional language with sampling, non-determinism, and ticking cost annotations, and proves two soundness theorems corresponding to different ticking strategies. The ATLAS prototype automatically infers tight logarithmic bounds for randomised Meldable Heaps, Splay Trees, and a probabilistic BST, outperforming or matching known manual analyses and enabling exploration of parameter knobs like rotation probability and tick costs. The results demonstrate practical impact by enabling automated cost analyses for sophisticated data structures, with potential extensions to additional probabilistic data structures and connections to established cost-calculus frameworks.

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.

Automated Expected Amortised Cost Analysis of Probabilistic Data Structures

TL;DR

This work presents the first fully-automated framework for computing expected amortised costs of probabilistic self-adjusting data structures via a specialized type-and-effect system. It introduces a probabilistic functional language with sampling, non-determinism, and ticking cost annotations, and proves two soundness theorems corresponding to different ticking strategies. The ATLAS prototype automatically infers tight logarithmic bounds for randomised Meldable Heaps, Splay Trees, and a probabilistic BST, outperforming or matching known manual analyses and enabling exploration of parameter knobs like rotation probability and tick costs. The results demonstrate practical impact by enabling automated cost analyses for sophisticated data structures, with potential extensions to additional probabilistic data structures and connections to established cost-calculus frameworks.

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.
Paper Structure (28 sections, 8 theorems, 56 equations, 20 figures, 3 tables)

This paper contains 28 sections, 8 theorems, 56 equations, 20 figures, 3 tables.

Table of Contents

  1. Introduction
  2. Overview of Our Approach and Results
  3. Introductory Example
  4. Overview of Benchmarks and Results
  5. Randomised Meldable Heaps.
  6. Randomised Splay Trees.
  7. Probabilistic Analysis of Binary Search Trees.
  8. Probabilistic Functional Language
  9. Operational Semantics
  10. Type-and-Effect System for Expected Cost Analysis
  11. Resource Functions
  12. Typing Rules
  13. Soundness Theorems
  14. Implementation and Evaluation
  15. Implementation.
  16. ...and 13 more sections

Key Result

theorem 1

Let $\mathsf{P}$ be a program and $\sigma$ a substitution. Then, Moreover, if $e\sigma$ almost-surely terminates, we can choose $c=c'$ in both cases.

Figures (20)

  • Figure 1: function
  • Figure 2: Partial Type Derivation for Function
  • Figure 3: Partial function of Randomised Meldable Heaps
  • Figure 4: Partial function of Randomised Splay Trees (zigzig-case)
  • Figure 5: function of a Binary Search Tree with randomized comparison
  • ...and 15 more figures

Theorems & Definitions (12)

  • theorem 1: Equivalence
  • definition 1
  • definition 2
  • lemma 1
  • theorem 2: Soundness Theorem for $\ruletick$
  • corollary 1
  • theorem 3: Soundness Theorem for $\ruletickast$
  • lemma 2
  • theorem 3: Soundness Theorem for $\ruletick$
  • proof
  • ...and 2 more