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

[Martin Riener <martin.riener@inria.fr>]

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