Verified analysis of random binary tree structures. (English) Zbl 1468.68288

Eberl, Manuel; Haslbeck, Max W.; Nipkow, Tobias

Avigad, Jeremy (ed.) et al., Interactive theorem proving. 9th international conference, ITP 2018, held as part of the federated logic conference, FloC 2018, Oxford, UK, July 9–12, 2018. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10895, 196-214 (2018).

Summary: 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, and the expected shape of a Treap. The last two 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.
For the entire collection see [Zbl 1391.68001].

MSC:

68V15	Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
68P05	Data structures
68P10	Searching and sorting
68W20	Randomized algorithms
68W40	Analysis of algorithms

Software:

PRISM; Amortized Complexity; Isar; QuickSort Cost; Ergodic theory; Archive Formal Proofs; Isabelle/HOL; Random BSTs; Treaps; Density Compiler; HOL; Root Balanced Tree; Coq; CryptHOL; Isabelle