From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by yquem.inria.fr (Postfix) with ESMTP id E85C1BC57 for ; Fri, 14 May 2010 10:09:10 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AuADAHOi7EtKfVI2gGdsb2JhbACdH1sIFQEBFCQirEeCAIUFLohNAQEDBYULBA X-IronPort-AV: E=Sophos;i="4.53,227,1272837600"; d="scan'208";a="62821117" Received: from mail-ww0-f54.google.com ([74.125.82.54]) by mail4-smtp-sop.national.inria.fr with ESMTP; 14 May 2010 10:09:11 +0200 Received: by wwb18 with SMTP id 18so7587wwb.27 for ; Fri, 14 May 2010 01:09:10 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=domainkey-signature:mime-version:received:received:in-reply-to :references:date:message-id:subject:from:to:content-type; bh=qiZK7yuQi8oEyxsg+11JlAkUi5i3ZnBLfeFuSwPs9Wc=; b=K/C7VY72GuQqlDQ8eXcUhE207R0dRjUwPsC8g/gCJrjxtyraGW66/C1u1qoBNV6I/e rlfRJtIPOqXCzWKwzqdDWe8qS1Lq5Z7XQXuwOG2p+ula0H5SgLOJFP1OdITFVYiw/Jhu y7S3ffAAT1dwe4kNtSleQi4RdeAF98jvvcjIc= DomainKey-Signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :content-type; b=j0Trmb0ErTldWFPKMOZgVcFQnN4m72MxIlp3Fes5E7eywVGy34GH3TxnS7HZQmpkIP MHz0oMfnh1zd4EPK61aA4OpSsNwupigOmenEBYrWrCWlvnwPFZCAqYkPRcVnO6JZDNkD E01nnt+oEAS/VFvFkzojYvEDs5tbxNoRgRw54= MIME-Version: 1.0 Received: by 10.227.69.84 with SMTP id y20mr842313wbi.226.1273824550146; Fri, 14 May 2010 01:09:10 -0700 (PDT) Received: by 10.216.168.141 with HTTP; Fri, 14 May 2010 01:09:10 -0700 (PDT) In-Reply-To: References: Date: Fri, 14 May 2010 10:09:10 +0200 Message-ID: Subject: Fwd: [Caml-list] Balancing algorithm of Set/Map implementation From: Julien Signoles To: caml-list@inria.fr Content-Type: multipart/alternative; boundary=001636498d39d154d204868963b8 X-Spam: no; 0.00; signoles:01 signoles:01 yoriyuki:01 yamagata:01 yoriyuki:01 yamagata:01 unbalanced:01 ocaml:01 filliatre:01 letouzey:01 coq:01 coq:01 filliatre:01 letouzey:01 functors:01 --001636498d39d154d204868963b8 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable 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 comm= ent it. > > Some years ago, Jean-Christophe Filli=E2tre 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 answe= r your 2 questions. [1] Jean-Christophe Filli=E2tre and Pierre Letouzey. Functors for Proofs an= d 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 --001636498d39d154d204868963b8 Content-Type: text/html; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable 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 ag= o, I thought I have understand how it works.=A0 But now, I read it again an= d I'm less confident now.=A0 Could someone answer my questions?=A0
= 
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 f=
actor up to *2*, which is usually allowed only up to 1?




Maybe my question is naive one, but I would appreciate if your could co=
mment it.

Some years ago, Jean-Christo= phe Filli=E2tre and Pierre Letouzey formally proved within the Coq proof as= sistant (http://coq.inria= .fr) that this algorithm is correct. Explanations provided by their pap= er [1] should answer your 2 questions.

[1]=20 Jean-Christophe Filli=E2tre 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, Barcelon= a, Spain, April 2004.

Hope this helps,
Julien Signoles

--001636498d39d154d204868963b8--