Weight-Balanced Trees

Kazu Yamamoto
created: 2011.1.25
modified: 2011.2.1

Weight-Balanced Trees(or binary search trees of bounded balance) are binary search trees which can be used to implement sets and finite maps (key-value store). This structure is widely used in functional languages. For instance, Haskell uses this for Data.Set and Data.Map. MIT/GNU Scheme and slib provides wttree.


The original weight balanced tree is invested by Nievergelt and Reingold in 1972. Its weight is "size + 1". The balance algorithm has two parameters, delta and gamma. They defined <delta,gamma> = <1 + sprt 2, sqrt 2>. This algorithm and this parameter does not have bugs. That is, the balance of a tree is always maintained. However, since these parameter are not integer, implementation cost is high.

In 1991, Adams created a variant of weight balanced tree for the programming competition organized by Appel. Its weight is purely "size". He defined (delta,gamma) = (3 or larger, 1) in his SML implementations and papers. The pair (delta,gamma) of "wttree.scm" is (5,1).

While Campbell was re-implementing "wttree.scm" in 2010, he found a balancing bug. In some cases, the delete operation on a given balanced tree breaks its balance. He also found Data.Map of Haskell is buggy and made a bug report. To our tests, only (3,2) and (4,2) are valid. So, all parameter choices by Adams are buggy.

We (Mr. Hirai and me) mathematically proved in Coq that <3,2> is one and only one interger solution for the original weight balanced tree (not Adams's one).