Lawrence Paulson
2018-10-19 15:16:36 UTC
I'm happy to announce another AFP entry contributed by Manuel Eberl: Randomised Binary Search Trees
"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."
It's a wonderful demonstration of what can be done with the libraries now our disposal, including probability theory and a number of theories related to the analysis of algorithms.
It is now online at https://www.isa-afp.org/entries/Randomised_BSTs.html
Larry Paulson
"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."
It's a wonderful demonstration of what can be done with the libraries now our disposal, including probability theory and a number of theories related to the analysis of algorithms.
It is now online at https://www.isa-afp.org/entries/Randomised_BSTs.html
Larry Paulson