Verified Analysis of Random Binary Tree Structures

Autor:	Manuel Eberl, Max W. Haslbeck, Tobias Nipkow
Rok vydání:	2020
Předmět:	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
Zdroj:	Journal of Automated Reasoning. 64:879-910
ISSN:	1573-0670 0168-7433
DOI:	10.1007/s10817-020-09545-0
Popis:	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.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_________::579381b7e0e2d94998c94b10575e5f0c https://doi.org/10.1007/s10817-020-09545-0 Zobrazit plný text záznamu Full text from SpringerLink