Abstract: |
This work is a formalisation of the Randomised Binary Search
Trees introduced by MartÃnez and Roura, including definitions and
correctness proofs. Like randomised treaps, they
are a probabilistic data structure that behaves exactly as if elements
were inserted into a non-balancing BST in random order. However,
unlike treaps, they only use discrete probability distributions, but
their use of randomness is more complicated. |
BibTeX: |
@article{Randomised_BSTs-AFP,
author = {Manuel Eberl},
title = {Randomised Binary Search Trees},
journal = {Archive of Formal Proofs},
month = oct,
year = 2018,
note = {\url{http://isa-afp.org/entries/Randomised_BSTs.html},
Formal proof development},
ISSN = {2150-914x},
}
|