Email Gateway (Aug 22 2022 at 18:39): Email Gateway (Aug 22 2022 at 18:39):From: Lawrence Paulson <lp15@cam.ac.uk>
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
Last updated: Nov 21 2024 at 12:39 UTC