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

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

[Bruno Guillaume]

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

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

[Martin Riener]

[-- Attachment #1.1: Type: text/plain, Size: 1146 bytes --]

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
> 


[-- Attachment #2: OpenPGP digital signature --]
[-- Type: application/pgp-signature, Size: 819 bytes --]

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

[Gabriel Scherer]

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
>>
>