From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id F2DFE80161 for ; Tue, 20 Jun 2017 17:20:06 +0200 (CEST) X-IronPort-AV: E=Sophos;i="5.39,364,1493676000"; d="asc'?scan'208";a="229038196" Received: from xover.htu.tuwien.ac.at (HELO [0.0.0.0]) ([128.130.95.22]) by mail3-relais-sop.national.inria.fr with ESMTP/TLS/DHE-RSA-AES128-SHA; 20 Jun 2017 17:20:06 +0200 To: caml-list@inria.fr References: From: Martin Riener Message-ID: <36cdaad0-efa4-a4f3-4d14-46985a5f1101@inria.fr> Date: Tue, 20 Jun 2017 17:19:53 +0200 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:52.0) Gecko/20100101 Thunderbird/52.1.0 MIME-Version: 1.0 In-Reply-To: Content-Type: multipart/signed; micalg=pgp-sha256; protocol="application/pgp-signature"; boundary="eVEx0iG92nntcu1pIEQlXhoI2aHmb2uT4" Subject: Re: [Caml-list] Specification of the choose function on sets This is an OpenPGP/MIME signed message (RFC 4880 and 3156) --eVEx0iG92nntcu1pIEQlXhoI2aHmb2uT4 Content-Type: multipart/mixed; boundary="DGRs9aITs33S3rijoNRSf0OVluomnQDuS"; protected-headers="v1" From: Martin Riener To: caml-list@inria.fr Message-ID: <36cdaad0-efa4-a4f3-4d14-46985a5f1101@inria.fr> Subject: Re: [Caml-list] Specification of the choose function on sets References: In-Reply-To: --DGRs9aITs33S3rijoNRSf0OVluomnQDuS Content-Type: text/plain; charset=utf-8 Content-Language: de-AT Content-Transfer-Encoding: quoted-printable 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 =3D 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, >=20 > In a context not directly related to OCaml, I want to define the semantic= s of a =E2=80=9Cchoose=E2=80=9D function on a set.=20 > In the doc of Set.Make, for the =E2=80=9Cchoose" function, it is said:=20 >=20 > =E2=80=9Cbut equal elements will be chosen for equal sets.=E2=80=9D >=20 > What is the rationale behind this specification? Do you have examples whe= re this specific requirement is needed? >=20 > Thanks, >=20 > Bruno >=20 --DGRs9aITs33S3rijoNRSf0OVluomnQDuS-- --eVEx0iG92nntcu1pIEQlXhoI2aHmb2uT4 Content-Type: application/pgp-signature; name="signature.asc" Content-Description: OpenPGP digital signature Content-Disposition: attachment; filename="signature.asc" -----BEGIN PGP SIGNATURE----- Version: GnuPG v2 iQIcBAEBCAAGBQJZST0lAAoJEP8NMgf63JCW1m0P/0Dw19YrOeII/nA6sHggU45z x3o2gg12/PBHWnXXAGvC0XIS7CsUx6XH92MuTpBSqFN+2jM0VNP3FjfNqEpYYeqF +8Q/xHDsZWYQ7+JgwQPr4imDXFxumCYETxganFOBvHkTLWzsqPF5NNxoS+HFpTV1 qVOOWBI/Icjkg3zZGPqBVC3244vHJ9zICjZ2xK2tSPEiSu8gNUSvEXSWcdahBamj oDJL38xu7m9pMm6iQI5UH0J/uhbzygXkpt/sBaIOjJPK8iPU9crSOeUAVQJAB6Xf 3yLva8lyHoAi9UNlWZy/WeB33ENSS8+WT3swT/CrkUszkxxkP6HXWVWgnc+5OWVX KW4q2+EamnLEpNfEEPf52q5scLIHft1Uwk2EqMUCM6PcWiF8JDPkfCYPW3QzGxpr BTF0Cc5hMyDRcLz2X4Nc4wMAZtm6e2fn4etW9Q3P7XH3uuS2veSuP2Ww2Gx5uvwx TcPLn/MTKE3ORIHR1HZl1KXYMPPGiWRskZobbhD6u9zRj1rlVjJ0Q1YLfYA6HXHy Dk7EBNy8pKXWArKtYdNqRo4nrpCSOf4neoYYeKCwWu1sH4yWNjYCLZG5+fyb6DyG ARe9onHSV7iW12ESJ+UCXlMrnsHuOJuT0DxKB+qBGmTeTyh370hSv7XjZtQXDvtr rrgbJNLhX6s+PuRam7Zx =gGW2 -----END PGP SIGNATURE----- --eVEx0iG92nntcu1pIEQlXhoI2aHmb2uT4--