Jean-Christophe Filliatre wrote:

> > I  have not  found a  method to  implement a  set with  an efficient
> > element removal  operation. To  my knowledge, the  implementation of
> > set based on  balanced tree is efficient for  union, difference etc,
> > but  does  not seem  to  be  reasonably  efficient for  deleting  an
> > element. Besides, the tree-based implementation of set requires that
> > the elements  have an  ordered type, it  is not  clear to me  how to
> > extend these techniques  to build a set of  unordered elements, say,
> > set of sets.
>
> Ocaml sets come with a comparison function, so that you can build sets
> of sets. See   http://caml.inria.fr/ocaml/htmlman/manual053.html.
>
> If you can  manage with sets of integers,  you could consider Patricia
> trees  instead  of  balanced  trees,  as  suggested  in  that  article
> http://www.cs.columbia.edu/~cdo/papers.html#ml98maps
>
> As  I already  wrote,  Okasaki's  book is  marvelous,  and gives  many
> different implementations  of efficient datastructures,  together with
> tools to analyze theire complexity.

Thanks for the suggestion, it sounds to be interesting to consider the ocaml
comparison function on sets to build sets of sets.

For the deletion operation, I've contacted Okasaki, who has also proposed
balanced tree and Patricia tree, as well as the above paper and the following one:
http://www-swiss.ai.mit.edu/~adams/BB/index.html

The deletion operation described in these papers will rebuild a tree. Therefore,
it does not seem to be comparably efficient with those implementations in
imperative languages.

Best regards.

Gang Chen