On Fri, 26 Mar 2004 09:46:53 +0100, Robert Will
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.