Even the original paper (1973) describing trees of bounded balance had
a bug! I think it is fair to describe maintaining balance in BBSTs as
"subtle".
Some ideas that might help:
1. http://www.brics.dk/BRICS/ALCOM-FT/TR/ALCOMFT-TR-01-167.html
2. This seems like a place where calling in a theorem prover might be
appropriate:
(a) The operations are tricky
(b) The data structure is very important
(c) Coq has done similar work before:
http://www.lri.fr/~filliatr/fsets/ (The performance suffered, but I
think all of that can be alleviated with Coq's updated extraction
mechanism. Pragmas necessary for performance would still need to be
inserted after extraction.)
On Tue, Aug 3, 2010 at 4:59 PM, Daniel Peebles
Deletion in Data.Map does not always preserve the balance of a tree.