From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id 7A0B87F927 for ; Tue, 10 Jun 2014 21:52:23 +0200 (CEST) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of jonikelee@gmail.com) identity=pra; client-ip=209.85.216.181; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="jonikelee@gmail.com"; x-sender="jonikelee@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of jonikelee@gmail.com designates 209.85.216.181 as permitted sender) identity=mailfrom; client-ip=209.85.216.181; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="jonikelee@gmail.com"; x-sender="jonikelee@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-qc0-f181.google.com) identity=helo; client-ip=209.85.216.181; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="jonikelee@gmail.com"; x-sender="postmaster@mail-qc0-f181.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AooDAD5hl1PRVdi1nGdsb2JhbABYFoNJq0IGmRIBgQoWDwEBAQEBBg0JCRQohAMBAQEEEiYIARscAgMMBgULDQkWDwkDAgECAQ8CEQEFARwTBgIBAR6ICwEDEQUIogBqjRmDD5NdChknDWSEYxEBBQyFSoZRHIINFoQrAQOQboc8gXqBQoU0hlaECEGFCFABAQE X-IPAS-Result: AooDAD5hl1PRVdi1nGdsb2JhbABYFoNJq0IGmRIBgQoWDwEBAQEBBg0JCRQohAMBAQEEEiYIARscAgMMBgULDQkWDwkDAgECAQ8CEQEFARwTBgIBAR6ICwEDEQUIogBqjRmDD5NdChknDWSEYxEBBQyFSoZRHIINFoQrAQOQboc8gXqBQoU0hlaECEGFCFABAQE X-IronPort-AV: E=Sophos;i="4.98,1010,1392159600"; d="scan'208";a="66616994" Received: from mail-qc0-f181.google.com ([209.85.216.181]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 10 Jun 2014 21:52:22 +0200 Received: by mail-qc0-f181.google.com with SMTP id x3so2917669qcv.40 for ; Tue, 10 Jun 2014 12:52:21 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=message-id:date:from:user-agent:mime-version:to:subject:references :in-reply-to:content-type:content-transfer-encoding; bh=Ac0mXjmknKBlOyLh4F4QK/RrS13CYiVrlbrCreJ4dKA=; b=aBsYJjsR++quPoR6YGY50b40Lj8IQf70+hOe5gId+Bm/H5H2y+zJi8xOPEpDwLaiZu 8UNrocq5oTe395q3TxSvg1SqMe1dJAbCjjwHIZj6yK3N/1VGs1lbKV3d8389AZAnNs/W FVNpGs6JNtNf8qAFT5FPOqniSxCQ7a/4W+B8emHYWBxFPzzHvDBmc4ub0gipNg/4GtCz kUCRQ7azagxFHJ3BDo0hCwyetk1fIBW1PXLmcf+bH0tsCK3XP9rXlWQ1E3jlq0EfwRwo SMYRo4Hg4DXpAKNWrOfDU4+aiwUtN6nAAJkVuc1SPzR4ULTAMBJDidioc/klyQvND2sD hnHQ== X-Received: by 10.140.25.166 with SMTP id 35mr16340837qgt.103.1402429941795; Tue, 10 Jun 2014 12:52:21 -0700 (PDT) Received: from [10.0.2.15] (c-24-61-84-156.hsd1.ma.comcast.net. [24.61.84.156]) by mx.google.com with ESMTPSA id r14sm14335538qga.4.2014.06.10.12.52.20 for (version=TLSv1 cipher=ECDHE-RSA-RC4-SHA bits=128/128); Tue, 10 Jun 2014 12:52:21 -0700 (PDT) Message-ID: <539761F4.8000308@gmail.com> Date: Tue, 10 Jun 2014 15:52:20 -0400 From: Jonathan User-Agent: Mozilla/5.0 (X11; Linux i686; rv:24.0) Gecko/20100101 Thunderbird/24.5.0 MIME-Version: 1.0 To: caml-list@inria.fr References: <539753C4.6060707@hars.de> In-Reply-To: <539753C4.6060707@hars.de> Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Subject: Re: [Caml-list] Why AVL-tree? On 06/10/2014 02:51 PM, Florian Hars wrote: > Am 10.06.2014 20:19, schrieb jonikelee@gmail.com: >> Any further information or source pointers you can give me would be >> greatly >> appreciated. > > This may prove to be of interest to you: > > http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.2.6890 > > (Or the version on one of the authors' page: > https://www.lri.fr/~filliatr/ftp/publis/fpp.ps.gz ) > > - Florian. > Thanks for the links. I see that those are the origin of the FSets in Coq. The code I generated for AVL trees and "gap" trees doesn't carry around the height for each node at runtime (although the proofs do - but it gets fully erased in the extracted OCaml code, leaving just a small enumeration type), nor perform any height computations at runtime. There is a claim in the above paper that they carry around the height on each node for "greater efficiency". I wonder what that claim refers to. Possibly the fact that they relax the AVL "delta" (the difference between sibling subtree heights) to be greater than 1. Is that what was meant by "2-imbalance AVL trees" in this thread? -- Jonathan