English version
Accueil     À propos     Téléchargement     Ressources     Contactez-nous    

Ce site est rarement mis à jour. Pour les informations les plus récentes, rendez-vous sur le nouveau site OCaml à l'adresse ocaml.org.

Browse thread
Balancing algorithm of Set/Map implementation
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ 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>


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