Randomised Binary Search Trees


Title: Randomised Binary Search Trees
Author: Manuel Eberl
Submission date: 2018-10-19

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.

  author  = {Manuel Eberl},
  title   = {Randomised Binary Search Trees},
  journal = {Archive of Formal Proofs},
  month   = oct,
  year    = 2018,
  note    = {\url{https://isa-afp.org/entries/Randomised_BSTs.html},
            Formal proof development},
  ISSN    = {2150-914x},
License: BSD License
Depends on: Monad_Normalisation, Random_BSTs