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

[Daan Leijen]

On Fri, 26 Mar 2004 09:46:53 +0100, Robert Will <robertw at stud.tu-ilmenau.de> wrote:

> The precondition-problem is not easy to fix.  However, I ackknowledge that
> your balancing-checks are really good evidence for the correctness of the
> algorithm.  (I didn't notice them first, because you checked via an
> external function, not in a smart constructor.  And I looked only there.)
>
> Well, having mathematically unproven code is a common thing and should
> indeed be no problem.  It's just that I personnally prefer algorithms that
> I understand, i.e. I know why they are correct.  For Adam's algorithm this
> is not the case, and I think other people would have serious problems,
> too, when explaining "under what (pre)condition does 'balance' produce a
> correctly balanced tree?" and "why does 'join' always observe that
> precondition?".

I agree with this and I will take a close look at your proofs. It would
be good to flesh out the true pre-conditions to Adams' "join" operation
and show that these are fullfilled in DData/Data.FiniteMap.

All the best,
  Daan.