Sorry miss the Cc-ing to the caml list. ---------- Forwarded message ---------- From: Julien Signoles Date: 2010/5/14 Subject: Re: [Caml-list] Balancing algorithm of Set/Map implementation To: Yoriyuki Yamagata Hello, 2010/5/14 Yoriyuki Yamagata > 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