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 <pumpkingod@gmail.com> wrote:
Deletion in Data.Map does not always preserve the balance of a tree.