Fwd: [Caml-list] Balancing algorithm of Set/Map implementation

[Julien Signoles <julien.signoles@gmail.com>]

[-- Attachment #1: Type: text/plain, Size: 1432 bytes --]

Sorry miss the Cc-ing to the caml list.

---------- Forwarded message ----------
From: Julien Signoles <julien.signoles@gmail.com>
Date: 2010/5/14
Subject: Re: [Caml-list] Balancing algorithm of Set/Map implementation
To: Yoriyuki Yamagata <yoriyuki.y@gmail.com>


Hello,

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

[-- Attachment #2: Type: text/html, Size: 2079 bytes --]