Browse thread
Balancing algorithm of Set/Map implementation
-
Yoriyuki Yamagata
- Julien Signoles
- Daniel_Bünzli
- Goswin von Brederlow
- Stanisław T. Findeisen
[
Home
]
[ Index:
by date
|
by threads
]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: | 2010-05-14 (08:09) |
From: | Julien Signoles <julien.signoles@g...> |
Subject: | Fwd: [Caml-list] Balancing algorithm of Set/Map implementation |
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