Balancing weight-balanced trees
Balancing weight-balanced trees
复制标题
平衡重量平衡树
DOI：
10.1017/s0956796811000104
复制
发表时间：
2011
影响因子：
1.1
通讯作者：
Kazuhiko Yanamoto
中科院分区：
文献类型：
--
作者：
Yoichi Hirai;Kazuhiko Yanamoto
权重平衡树（Weight-Balanced Tree，WBT）是一种二叉查找树，它的平衡是基于每个节点中子树的大小。虽然在函数式编程语言中广泛使用变体WBT算法上的纯函数式实现，但在某些情况下，许多现有实现在删除后不能保持平衡。困难在于选择一对有效的旋转参数：一个用于标准平衡，另一个用于选择单旋转或双旋转。本文确定了原始WBT算法中插入和删除旋转参数的精确有效范围，其中存在且仅存在一个整数解。合理的范围证明使用证明助理Coq。完备性证明使用有效的算法生成反例树。对于两个特定的参数对，我们还在Coq中证明了集合运算也保持平衡。由于原始WBT和变体WBT之间的差异很小，因此很容易将基于变体WBT的现有错误实现更改为具有合理解决方案的认证原始WBT。
A weight-balanced tree (WBT) is a binary search tree, whose balance is based on the sizes of the subtrees in each node. Although purely functional implementations on a variant WBT algorithm are widely used in functional programming languages, many existing implementations do not maintain balance after deletion in some cases. The difficulty lies in choosing a valid pair of rotation parameters: one for standard balance and the other for choosing single or double rotation. This paper identifies the exact valid range of the rotation parameters for insertion and deletion in the original WBT algorithm where one and only one integer solution exists. Soundness of the range is proved using a proof assistant Coq. Completeness is proved using effective algorithms generating counterexample trees. For two specific parameter pairs, we also proved in Coq that set operations also maintain balance. Since the difference between the original WBT and the variant WBT is small, it is easy to change the existing buggy implementations based on the variant WBT to the certified original WBT with a rational solution.