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

hi, On Mon, 22 Mar 2004, JP Bernardy wrote:

--- Robert Will 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