Weight-Balanced Trees

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.

History

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.

• Nievergelt J. and Reingold E.M., "Binary search trees of bounded balance", Proceedings of the fourth annual ACM symposium on Theory of computing, pp 137--142, 1972

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).

• Adams S., Implementing sets efficiently in a functional language, Technical Report CSTR 92-10, University of Southampton, 1992

• Adams S., "Efficient sets: a balancing act, Journal of Functional Programming", Vol 3, No 4, pp 553--562, 1993

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).

Fixes

• In Dec 2010, slib incorporated our patch. (wttree.scm in slib 3b3 or earlier has this bug.)
• In Jan 2011, MIT/GNU Scheme incorporated our patch. (wttree.scm in MIT/GNU Scheme 9.0.1 or earlier has this bug.)
• Data.Map in the container package 0.3.0.0 or earlier has this bug. We would propose to incorporate our patch.

Resources

• Balancing Weight-Balanced Trees, Journal of Functional Programming. Volume 21, Issue 03, pp 287-307. (The old title is "Balance Condition on Weight-Balanced Trees".)
• Our proof in Coq
• Our code for algorithm implementation, tests, Omega Solver, and benchmarks are available on github.
• Our fixes for MIT/GNU Scheme and slib are also available on github. To demonstrate Adams's implementation is buggy and our patch fixes the bug, we implemented a test framework like QuickCheck.
• The valid area of <delta,gamma> for the original weight balanced tree is illustrated.