2010/5/14 Yoriyuki Yamagata
<yoriyuki.y@gmail.com>
When I read the balancing function of stdlib's Set/Map several years ago, I thought I have understand how it works. But now, I read it again and I'm less confident now. Could someone answer my questions?
Is this code right? If r is Empty and lr and ll are huge trees,
doesn't it create a massively unbalanced tree?
Another question is that why OCaml implementation allows
a balancing factor up to *2*, which is usually allowed only up to 1?
Maybe my question is naive one, but I would appreciate if your could comment it.
Some years ago, Jean-Christophe Filliātre and Pierre Letouzey formally proved within the Coq proof assistant (
http://coq.inria.fr) that this algorithm is correct. Explanations provided by their paper [1] should answer your 2 questions.
[1]
Jean-Christophe Filliātre and Pierre Letouzey.
Functors for Proofs and Programs.
In
Proceedings of The European Symposium on Programming, volume
2986 of
Lecture Notes in Computer Science, pages 370-384, Barcelona,
Spain, April 2004.
Hope this helps,
Julien Signoles