Bug in Data.Map

[Milan Straka]

Hi,

> On August 4, 2010 05:33:15 Milan Straka wrote:
> > If the rebalancing is done in the case of broken balance, ie. in
> > sizeR > delta*sizeL, there is a simple counterexample (you will need
> > fixed-width font):
> >    2                                                          (A)
> > 1     5
> >      4 6
> >     3   7
> > 
> > and delete 1.
> 
> Urk.  I see where the problem is.  The first equation on page 27 gives the 
> state of things once they are out of balance in conjunction with Fig 6.
> 
>   n + alpha n + 1 = wx + 1
> 
> In other words, an element has been added to the right side (containing n + 
> alpha n + 1) items so it now contains one more item than w times the x items 
> on the left side.  The equalities and such that follow ensure a re-balance 
> will always fix this situation.
> 
> What they don't show, however, is what happens if things get out of balance in 
> by deleting an item from the left-hand side.  In this case, the right side can 
> windup exceed the left by anywhere up to w times (i.e., as in your example).  
> The required fix is to redo all the inequalities using
> 
>   n + alpha n + 1 = wx + e,
> 
> for e = 1, 2, ..., w (in most cases only e = w will also need checking).
> 
> Cheers!  -Tyson
> 
> PS:  In short, unless I'm missing something, Adam only gave a proof/conditions 
> for insertion.  The deletion case still needs to be done.

That is exactly the case. Actually, it is enough to consider deletions
only, when you write down the inequalities.

Another thing is that you have to solve several cases manually for small
trees (a bit more than with insertion), because for n=1 (and maybe for
n=2, I do not recall) some equations are not satisfied, but only for
non-integral numbers of vertices, which cannot happen.

I will write it down and post it somewhere.

Cheers,
Milan