Re: [Caml-list] Specification of the choose function on sets

[Gabriel Scherer <gabriel.scherer@gmail.com>]

For the record, we had the same discussion for the Batteries
library, raised by Cedric "rixed" Cellier, and we decided to
add "any" functions to the Map and Set module that drop the
requirement of being deterministic with respect to set
rebalancing, and are a bit faster. (Note that "choose" is already
relatively fast in practice as its O(log(size))).

  https://github.com/ocaml-batteries-team/batteries-included/pull/751

On Tue, Jun 20, 2017 at 11:19 AM, Martin Riener <martin.riener@inria.fr> wrote:
> Hello Bruno,
>
>
> I'm far from being an expert in ocaml, but that's my explanation so for:
> The specification comes from Hilbert's epsilon operator, which picks an
> unspecified element from a set (for details, see e.g. [1]). Since
> epsilon is a function (of the set), it must always return the same
> element. An example which comes to mind is to have a quick check for the
> inequality of sets:
>
> let ineq s1 s2 =
>  if (S.choose s1 <> S.choose s2) then
>    false
>  else
>    not (
>     (S.for_all (fun x -> S.mem x s1) s2) &&
>     (S.for_all (fun x -> S.mem x s2) s1)
>    )
>
> I hope that helps,
> cheers, Martin
>
> [1] https://plato.stanford.edu/entries/epsilon-calculus/
>
> On 06/20/2017 07:46 AM, Bruno Guillaume wrote:
>> Dear Ocamlers,
>>
>> In a context not directly related to OCaml, I want to define the semantics of a “choose” function on a set.
>> In the doc of Set.Make, for the “choose" function, it is said:
>>
>> “but equal elements will be chosen for equal sets.”
>>
>> What is the rationale behind this specification? Do you have examples where this specific requirement is needed?
>>
>> Thanks,
>>
>> Bruno
>>
>