1. Verified Analysis of Random Binary Tree Structures
- Author
-
Manuel Eberl, Max W. Haslbeck, and Tobias Nipkow
- Subjects
Automated theorem proving ,Theoretical computer science ,Computational Theory and Mathematics ,Artificial Intelligence ,Computer science ,Binary search tree ,Proof assistant ,Probabilistic analysis of algorithms ,Data structure ,Software ,Random binary tree ,Quicksort ,Treap - Abstract
This work is a case study of the formal verification and complexity analysis of some famous probabilistic algorithms and data structures in the proof assistant Isabelle/HOL. In particular, we consider the expected number of comparisons in randomised quicksort, the relationship between randomised quicksort and average-case deterministic quicksort, the expected shape of an unbalanced random Binary Search Tree, the randomised binary search trees described by Martínez and Roura, and the expected shape of a randomised treap. The last three have, to our knowledge, not been analysed using a theorem prover before and the last one is of particular interest because it involves continuous distributions.
- Published
- 2020
- Full Text
- View/download PDF