Automated Expected Amortised Cost Analysis of Probabilistic Data Structures
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2022
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866916269935034368 |
|---|---|
| author | Leutgeb, Lorenz Moser, Georg Zuleger, Florian |
| author_facet | Leutgeb, Lorenz Moser, Georg Zuleger, Florian |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2206_03537 |
| institution | arXiv |
| publishDate | 2022 |
| record_format | arxiv |
| spellingShingle | Automated Expected Amortised Cost Analysis of Probabilistic Data Structures Leutgeb, Lorenz Moser, Georg Zuleger, Florian Logic in Computer Science Data Structures and Algorithms Programming Languages 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. |
| title | Automated Expected Amortised Cost Analysis of Probabilistic Data Structures |
| topic | Logic in Computer Science Data Structures and Algorithms Programming Languages |
| url | https://arxiv.org/abs/2206.03537 |