The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 06/10/2014 09:18 AM, Frédéric Blanqui wrote:

Hi! You may be interested by this message:

https://sympa.inria.fr/sympa/arc/caml-list/2014-06/msg00013.html

That is very interesting!

The crucial entry in that thread is apparently:

https://sympa.inria.fr/sympa/arc/caml-list/2014-06/msg00009.html

where it says:

"Note that OCaml's balanced trees are not exactly what is usually
called AVL, as the imbalance between different branches can be at most
2 (+1 on one side and -1 on the other) instead of just 1 as the
traditional definition assumes."

which suggests that the 2-imbalance AVL trees OCaml uses are what I've been calling gap trees, or are at least very similar.  Does the OCaml team have a more precise definition?  Do they store the imbalance information on the parent node (as with AVL trees, which would take 2 bits per node) or in the child nodes (as with gap trees, which take 1 bit per node, but require additional leaf-handling rules)?

Also, from:

https://sympa.inria.fr/sympa/arc/caml-list/2014-06/msg00010.html

"As for performance of insert/lookup operations, Jean-Christophe
Filliâtre has measurements showing that OCaml's 2-imbalance AVL trees
perform better than red-black trees. It all depends on your ratio of
insertions to lookups, of course. But the 2-imbalance trick makes a
big difference with textbook AVL trees."

Which, if 2-imbalance AVL trees are gap trees, confirms my suspicion.

I also had not heard about 1-2 brother trees before.  Maybe I will implement them as well.

Also, maybe I should investigate the set operations (union, intersection, difference, etc).

Also, the OCaml team apparently has some tree testing and benchmarking code.  Might they be willing to share that?

Thanks very much for that link, Frédéric!

-- Jonathan