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 72A2680161 for ; Tue, 20 Jun 2017 18:52:52 +0200 (CEST) Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=gabriel.scherer@gmail.com; spf=Pass smtp.mailfrom=gabriel.scherer@gmail.com; spf=None smtp.helo=postmaster@mail-io0-f170.google.com Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of gabriel.scherer@gmail.com) identity=pra; client-ip=209.85.223.170; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="gabriel.scherer@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of gabriel.scherer@gmail.com designates 209.85.223.170 as permitted sender) identity=mailfrom; client-ip=209.85.223.170; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="gabriel.scherer@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-io0-f170.google.com) identity=helo; client-ip=209.85.223.170; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="postmaster@mail-io0-f170.google.com"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3A3xogYh8RTMs1Z/9uRHKM819IXTAuvvDOBiVQ1KB2?= =?us-ascii?q?0ekcTK2v8tzYMVDF4r011RmSDNqds6oMotGVmpioYXYH75eFvSJKW713fDhBt/?= =?us-ascii?q?8rmRc9CtWOE0zxIa2iRSU7GMNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1?= =?us-ascii?q?Ifn+FpLPg8it2e2//5/ebx9UiDahfLh/MAi4oQLNu8cMnIBsMLwxyhzHontJf+?= =?us-ascii?q?RZ22ZlLk+Nkhj/+8m94odt/zxftPw9+cFAV776f7kjQrxDEDsmKWE169b1uhTF?= =?us-ascii?q?UACC+2ETUmQSkhpPHgjF8BT3VYr/vyfmquZw3jSRMNboRr4oRzut86ZrSAfpiC?= =?us-ascii?q?gZMT457HrXgdF0gK5CvR6tuwBzz4vSbYqINvRxY7ndcMsYSmpPXshfWS9PDJ6i?= =?us-ascii?q?YYQTAOQMJvpYr5DnqlcSsReyGQuhCeXywTFInH/22qg63vwgHw7cxwMgBdMOv2?= =?us-ascii?q?rQrN7oKakdTeC1w7fSzTrddfNdxDDw6IfSfR86u/GMXKx/cc7LxUk0CwzFjkuf?= =?us-ascii?q?qZb7MDOPzekNvG2b4PBhVeKrkWIotwZxoj22y8oql4LHiIUVylXe+iV4xoY4Pd?= =?us-ascii?q?K4SE9nYd6kDZtfrDuWOJdxQsMnW21oozo6xacAuZ61eygK0okoywTBZPOaboiF?= =?us-ascii?q?5A/oWuWJITpgmn5pZLayiwyx/EWg0OHwSNe43VhQoiZYkNTAqnYA3AHJ5MedUP?= =?us-ascii?q?ty5EKh1C6P1w/N7uFEJlg5la/BJJ4gxr48j5sTsUPfEiPvlkX6ka2belk+9uin?= =?us-ascii?q?7OTnZbrmppuCOINulg7+NaEultS+AeQ+LAcOQ3CW9fqg2LDn50H0Q7VHguconq?= =?us-ascii?q?XHvp3WP9kXq6ylDwNN14Ys8Re/DzOo0NQCmnkHKUpIeB2dgIfyIVHOIe73DfOl?= =?us-ascii?q?j1S3jDhrx+7JPqf/DZXXNXXDn7Lhcqx8605Y0gY80ddf55dMBrEbPP3zQlPxtM?= =?us-ascii?q?DfDhIhNgy02efnB8t71owAQ2KCGa6YMKLXsVCT/OIgOfOAZI4TuDbnKvgq/eTi?= =?us-ascii?q?jXEjmVUFZ6mmwYMXaGykHvRhO0iWfWDjgtIFEWsTugo+TffqiEGZXD5IZ3eyWr?= =?us-ascii?q?o86SshBIKnC4fDXIGtj6ab0Ce1BJ0FLlxBX3WFC2vpcc2+WvoKZTjadspoiCAF?= =?us-ascii?q?U/67SoIn2AuGtQngyrMhIPCCqQMCspe2+9F//ezekVkJ/jx5FcmHmzWCRmtun2?= =?us-ascii?q?4MASQ93K1lrFZVxVKK0Kw+iPtdQ48Ar8hVWxs3YMaPh9dxDMr/D0eYJo+E?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0AhAQBdUklZf6rfVdFdHAEBBAEBCgEBF?= =?us-ascii?q?wEBBAEBCgEBhA+BDQeDZIoZkX+JG4xdghEshXgCgl8HPxgBAQEBAQEBAQEBARI?= =?us-ascii?q?BAQkLCwgmMYIzJAGCQQECAyMEGQEbDw4BAwwGBQsNAgImAgIiAREBBQEcBhMIi?= =?us-ascii?q?gsBAxUQnzE/jAiBbBgFARyDCQWDXgoZJw1Wg0ABAQEBAQEBAwEBAQEBAQEZAgE?= =?us-ascii?q?FEnmFYYUEhDI3gxKCYQWeYYIWhR2ML5IOk0UUH4EVH4FCMCEjXhmEZQ8cggIkN?= =?us-ascii?q?olZAQEB?= X-IPAS-Result: =?us-ascii?q?A0AhAQBdUklZf6rfVdFdHAEBBAEBCgEBFwEBBAEBCgEBhA+?= =?us-ascii?q?BDQeDZIoZkX+JG4xdghEshXgCgl8HPxgBAQEBAQEBAQEBARIBAQkLCwgmMYIzJ?= =?us-ascii?q?AGCQQECAyMEGQEbDw4BAwwGBQsNAgImAgIiAREBBQEcBhMIigsBAxUQnzE/jAi?= =?us-ascii?q?BbBgFARyDCQWDXgoZJw1Wg0ABAQEBAQEBAwEBAQEBAQEZAgEFEnmFYYUEhDI3g?= =?us-ascii?q?xKCYQWeYYIWhR2ML5IOk0UUH4EVH4FCMCEjXhmEZQ8cggIkNolZAQEB?= X-IronPort-AV: E=Sophos;i="5.39,364,1493676000"; d="scan'208";a="229048737" Received: from mail-io0-f170.google.com ([209.85.223.170]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 20 Jun 2017 18:52:51 +0200 Received: by mail-io0-f170.google.com with SMTP id y77so88502416ioe.3; Tue, 20 Jun 2017 09:52:51 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-transfer-encoding; bh=hI7OzhK+y3yamDGL7liEvHZ6ypm2Jfw2Oi0LqPWNbi8=; b=PLLpVYW8c4ZOyYk8AXdGSzHKSzB4KWoqGp/sRdu57geLjw/rFnH9X/s9mLo0sAUK2F nfaVGyk+Uqo1TzEj3qZ8orLbuURldYeDq5/bWWdaXA9aMAjN+7F/SdRLzloN4KRky04e Y3xJA4Jwug64z48xGbYlpbN12aqBxq3q0JMbWfdL6zwN0Kk/njt16jxuZIvUbnUi7pgN u4owZtJYc7XbDUkrHdztg7HzHyfmVSo8HMgNb0bY2f9YRU7drFK3IhuvYh1KSbPVdeeR SBOtITnxL5Azn9bHxGks3EbkJF2ZcM6sgCca81nv/H2ANjho3TDZG3/p7emy2nl6kQL/ z1kA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:mime-version:in-reply-to:references:from:date :message-id:subject:to:cc:content-transfer-encoding; bh=hI7OzhK+y3yamDGL7liEvHZ6ypm2Jfw2Oi0LqPWNbi8=; b=M+uKagw4NMMOiLH54CL4VcTOGTTqW5f3j2kYfcyoZITVJg9Hx7kQxugFvvH7/zvFST t5s/Da50rDEdBh24377w7EvkuerJwMU/3bX/H+mcYl593vs4h0P930nwOEAJL+ph6Avz 30BAGqGkMF5Qp4eprRXvvek64+pJJ5G8BpukSJY+jcTK5/kD5J4HAZo0E/IAOXszppmj /js/ZmvZfppx/io+FyCxuUcMLHnz9eRlFMXIxYijcbAP4jkrUKFJSnWrXq0Nxm01O6KL ivZPIKbNwgED8JzjjfXTa7GfY8U98June888RdfGoxhQ4ki9FFhQf6nt3TLQCVOi2Hlz 4yjg== X-Gm-Message-State: AKS2vOy/PGBHtIYwE04u8Jjnfke+3LlAVENl+m/ZQ9m6XIopOoPkkF85 HQI2NumjnI3DOxU9VV6crfKq9p03Nq+c X-Received: by 10.107.170.99 with SMTP id t96mr28409263ioe.113.1497977569681; Tue, 20 Jun 2017 09:52:49 -0700 (PDT) MIME-Version: 1.0 Received: by 10.79.36.132 with HTTP; Tue, 20 Jun 2017 09:52:09 -0700 (PDT) In-Reply-To: <36cdaad0-efa4-a4f3-4d14-46985a5f1101@inria.fr> References: <36cdaad0-efa4-a4f3-4d14-46985a5f1101@inria.fr> From: Gabriel Scherer Date: Tue, 20 Jun 2017 12:52:09 -0400 Message-ID: To: Martin Riener Cc: caml users Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Subject: Re: [Caml-list] Specification of the choose function on sets 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 wr= ote: > 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, >> >> In a context not directly related to OCaml, I want to define the semanti= cs of a =E2=80=9Cchoose=E2=80=9D function on a set. >> In the doc of Set.Make, for the =E2=80=9Cchoose" function, it is said: >> >> =E2=80=9Cbut equal elements will be chosen for equal sets.=E2=80=9D >> >> What is the rationale behind this specification? Do you have examples wh= ere this specific requirement is needed? >> >> Thanks, >> >> Bruno >> >