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

Dylan Thurston dpt at lotus.bostoncoop.net
Mon Mar 22 14:05:56 EST 2004

On Mon, Mar 22, 2004 at 05:41:52AM -0800, JP Bernardy wrote:
> Can you derive a counter-example from the
> demonstration bug?

Counter-example of what?  The claim is that there's a bug in the proof
that concatenating trees (the concat3 function in Adams' paper) is
efficient; do you want a pair of trees that take a long time to
concatenate with that algorithm, or do you want counterexamples to the

To tell the truth, after looking at the tech report
( http://www.swiss.ai.mit.edu/~adams/BB/92-10.ps.gz ), I don't
see a proof that concat3 is efficient, so I don't see how there can be
a bug in the (missing) proof.  Robert Will, can you clarify which
claim in the paper is faulty?

	Dylan Thurston

More information about the Libraries mailing list