Re: [Caml-list] Why AVL-tree?

[Jonathan <jonikelee@gmail.com>]

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