Verified Analysis of Random Binary Tree Structures
Verified Analysis of Random Binary Tree Structures
复制标题
DOI：
10.1007/s10817-020-09545-0
复制
发表时间：
2020-02-08
期刊：
影响因子：
--
通讯作者：
Nipkow, Tobias
中科院分区：
文献类型：
--
作者：
Eberl, Manuel;Haslbeck, Max W.;Nipkow, Tobias
这项工作是对证明助手Isabelle/Hol中一些著名概率算法和数据结构的正式验证和复杂性分析的案例研究。特别是，我们考虑了随机QuickSort中的比较数量，随机QuickSort和平均案例确定性QuickSort之间的关系，不平衡的随机二进制搜索树的预期形状，由Martinez和Roura描述的随机二进制搜索树以及随机TREAP的预期形状。据我们所知，最后三个之前没有使用定理供奉献者对最后一个进行分析，而最后一个则特别感兴趣，因为它涉及持续的分布。
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 Martinez 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.