Bug in the proof of Data.FiniteMap and DData.Map

[Robert Will]

hi,

On Mon, 22 Mar 2004, JP Bernardy wrote:
>
> --- Robert Will <robertw at stud.tu-ilmenau.de> wrote:
> >
> > both of the data structures are based on Adams' balancing algorithm
> > which contains a bug -- at least in its proof.  (Perhaps it is
> > correct, but I don't know anyone that knows if.)
>
> Can you derive a counter-example from the demonstration bug?

No, since obviously otherwise I *would* know that the algorithm is wrong,
but as I said, I don't and .... I don't know anyone that knows if.

If you want to know, you can add a smart constructor that checks the
balancing invariant.  (E.g. in 'bin' which should then be called
everywhere in place of 'Bin'.)  If this assertion never fails, there's
probably no bug.

To prove the correctness of the algorithm, by the way.... it suffices to
give a precondition for 'balance' (T' in Adams' paper) and prove that
'merge' (Adams' 'concat3') observes that precondition.  That's the bug in
Adams' proof.  Adams proved 'balanced' correct for the precondition that
that the balancing invariant is violated by at most one.  (size left <=
size right + 1 and v.v.)  This is observed by any other call to 'balance',
but not (?) from 'merge'.

> The current algorithm looks good enough for me,

Yeah, in DData it looks better than FiniteMap where they just disabled the
failing assertions.  Oh, perhaps the algorithm is wrong with respect to
the simple balancing invariant, but correct with respect to some more
complicated (amortised?) invariant.  That would explain Adams' failure
(and my reluctance) to proof it _and_ its good behaviour in practice.

> As a side note, I've re-implemented the "SpellCheck"
> test with DData, and it behaves ok.

As it does with many other applications...


Robert