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 mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id 665D87EF21 for ; Sun, 15 Jun 2014 16:01:40 +0200 (CEST) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of jonikelee@gmail.com) identity=pra; client-ip=209.85.216.180; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="jonikelee@gmail.com"; x-sender="jonikelee@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of jonikelee@gmail.com designates 209.85.216.180 as permitted sender) identity=mailfrom; client-ip=209.85.216.180; receiver=mail2-smtp-roc.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 (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-qc0-f180.google.com) identity=helo; client-ip=209.85.216.180; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="jonikelee@gmail.com"; x-sender="postmaster@mail-qc0-f180.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: ArMBAO6mnVPRVdi0lGdsb2JhbABag1+DRqZ+AQaCV5ZNAYEAFg8BAQEBBwsLCRIqhAMBAQEDARIRFQgBGxIKAgMMBgULAwoCAgUEEgsCAgkDAgECAQ8CEQEFAQoSBgEMBgIBAQ4QiAsBAwkIBQikTWqLJ4Fygw+SPAoZJwMKZYUZEQEFDIEehDmGcIE/a4J3gUwBA4RjBYwYh0qBeYFDhTeGXoQPQYUMUIEC X-IPAS-Result: ArMBAO6mnVPRVdi0lGdsb2JhbABag1+DRqZ+AQaCV5ZNAYEAFg8BAQEBBwsLCRIqhAMBAQEDARIRFQgBGxIKAgMMBgULAwoCAgUEEgsCAgkDAgECAQ8CEQEFAQoSBgEMBgIBAQ4QiAsBAwkIBQikTWqLJ4Fygw+SPAoZJwMKZYUZEQEFDIEehDmGcIE/a4J3gUwBA4RjBYwYh0qBeYFDhTeGXoQPQYUMUIEC X-IronPort-AV: E=Sophos;i="5.01,481,1400018400"; d="scan'208";a="80154326" Received: from mail-qc0-f180.google.com ([209.85.216.180]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 15 Jun 2014 16:01:11 +0200 Received: by mail-qc0-f180.google.com with SMTP id r5so2869548qcx.11 for ; Sun, 15 Jun 2014 07:01:10 -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=K4lhEPfTIbkl/qOPLOcptsQnXFzb1yNLOU2ZVMswO0w=; b=fk13hgqKCQgD0UT6ZhVDjx6n32WNMFM+piLuYA9u7OrJl1Yr8Xa8PIgrLg23P9tWrC Sv3EyuKntTi+rqEowipUVskr2hNGn5QlbiZiv89/WloAI0ESOOgaBydaCT0kEslW6YFn 3fjQ2eWS4RE4V9iCgq8vu6oUSQ2e2eIXWvNZEU6S/W9yM8idv+9pYQlWWAUZSZmwF2Kv gjRxnTNBC4TwTuA1H2CLbwSHNuTZ6QIs0z+Xy9xLZnfj4D3Q7IRlViTFtRs+3KDm8OiA /LHucVCKnXBYmTAxa88ZK1FnIC9jv3dTD7xLhyEt0SXNAWj73aR3mdV5HQ15WGCQPxuk HuCg== X-Received: by 10.224.123.202 with SMTP id q10mr13860737qar.79.1402840870584; Sun, 15 Jun 2014 07:01:10 -0700 (PDT) Received: from [10.0.2.15] (c-66-30-197-186.hsd1.ma.comcast.net. [66.30.197.186]) by mx.google.com with ESMTPSA id j5sm16753368qai.34.2014.06.15.07.01.09 for (version=TLSv1 cipher=ECDHE-RSA-RC4-SHA bits=128/128); Sun, 15 Jun 2014 07:01:09 -0700 (PDT) Message-ID: <539DA724.3080405@gmail.com> Date: Sun, 15 Jun 2014 10:01:08 -0400 From: Jonathan User-Agent: Mozilla/5.0 (X11; Linux i686; rv:24.0) Gecko/20100101 Thunderbird/24.6.0 MIME-Version: 1.0 To: Lukasz Stafiniak , Caml References: <538CAD12.2040104@inria.fr> In-Reply-To: Content-Type: text/plain; charset=UTF-8; format=flowed Content-Transfer-Encoding: 7bit Subject: Re: [Caml-list] Why AVL-tree? On 06/15/2014 12:51 AM, Lukasz Stafiniak wrote: > Here is a 2-imbalance AVL trees example from InvarGenT: > https://github.com/lukstafi/invargent/blob/master/examples/avl_tree.gadt > and the (inferred) types: > https://github.com/lukstafi/invargent/blob/master/examples/avl_tree.gadti.target > > Regards, > Lukasz Thank you for those links, Lukasz. I see from them that there is a difference between 2-imbalance AVL trees and gap trees. In 2-imbalance AVL trees, as with standard AVL trees, the parent height is always 1 + the maximum child height. In gap trees, a parent's height can in some cases be 2 above the height of both children, even though the childrens' heights never differ by more than 1. I am wondering how important this difference is. For example, with gap trees, there is at most one rebalancing needed per insertion or deletion operation. My understanding of standard AVL trees is that they may require O(logN) rebalancings per insertion or deletion. Do you know how the 2-imbalance property addition changes this rebalancing requirement for AVL trees? Thanks again, Jonathan > > On Tue, Jun 10, 2014 at 11:19 AM, wrote: > >> I am coming here from the Coq mailing list, because of a link posted there >> about this e-mail thread. I have been working on Coq-verified and fully >> proof-erased versions of AVL and red-black trees, as well as a variant I >> didn't know existed before, until I read about "2-imbalance AVL trees" in >> this >> thread. >> >> The github address for my development is: >> >> https://github.com/jonleivent/mindless-coding >> >> and the "gaptree" development there may be the same as your "2-imbalance" >> AVL >> trees, though I can't be sure without more of an explanation (or maybe >> just a >> pointer to the source code) for the 2-imbalance AVL trees. >> >> Any further information or source pointers you can give me would be greatly >> appreciated. >> >> Thanks >> --Jonathan >> >> -- >> Caml-list mailing list. Subscription management and archives: >> https://sympa.inria.fr/sympa/arc/caml-list >> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners >> Bug reports: http://caml.inria.fr/bin/caml-bugs >>