We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:

Download:

Current browse context:

cs.LO

Change to browse by:

References & Citations

DBLP - CS Bibliography

Bookmark

(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Computer Science > Logic in Computer Science

Title: Automated Expected Amortised Cost Analysis of Probabilistic Data Structures

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.
Comments: 39 pages
Subjects: Logic in Computer Science (cs.LO); Data Structures and Algorithms (cs.DS); Programming Languages (cs.PL)
Cite as: arXiv:2206.03537 [cs.LO]
  (or arXiv:2206.03537v1 [cs.LO] for this version)

Submission history

From: Georg Moser [view email]
[v1] Tue, 7 Jun 2022 19:12:25 GMT (55kb,D)

Link back to: arXiv, form interface, contact.