coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Formalization of the syntax of first-order logic: binders

From: Ian Shillito <Ian.Shillito AT anu.edu.au>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Formalization of the syntax of first-order logic: binders
Date: Wed, 13 Oct 2021 22:26:27 +0000
Accept-language: en-AU, en-US
Arc-authentication-results: i=1; mx.microsoft.com 1; spf=pass smtp.mailfrom=anu.edu.au; dmarc=pass action=none header.from=anu.edu.au; dkim=pass header.d=anu.edu.au; arc=none
Arc-message-signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-AntiSpam-MessageData-ChunkCount:X-MS-Exchange-AntiSpam-MessageData-0:X-MS-Exchange-AntiSpam-MessageData-1; bh=puVnmipzutlj4l7rBkTfhPnqzXeh0G3QuJOx0q9looQ=; b=oUwGGY8kXt00lvnxB1kecBYrUXvSKPXaVUSnAuA+/J0FXUERsT1h+wn+UrLwh+y/DBOlrXeQKH9WF6SpCzcO79jyRx6xiTAhup3U78IsE8lXE2rVKY7KPExHw3J25mGRI83dzX7UJaEi60f/azQ+eNo9T87jQe5VWD9mQD6k0qvIYkm0sFEMigK7zPrTd6iLfRpjxH6Q8VZpIM+AXUBtkSHxRD4t3WEsK0xDofoHfwGONi9jcevTo1woXTIf3PcwRdZmsvVHT5CvtcUgWxXP637rG151lmnGk08teVaPQY6ipp8GEcJs07vryS0eLWsv6qCYjBqqHpzsIFFL+Y01Dw==
Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=cMbFFm/TYf1ce6b1CbnybOcK6qTZwI7wy/5OGlWBJqW9i7PH/GF1dOHI7W54lE77M5zrhZTra8vXcWU5tJcgMhZole6WvZiY6dbxFhe6jQp899rq2qMxidugoqOF1y6l/Q9ONLlhqf/HJeoiQaPvj+QJceJUEWmJPRKJnOGmqMsVzAyi2EsXedwrh2pDxkTwTLwa9xhGn+yywHp4QtP8ZoS8spgjZWhY/X63DsmYJUrnv8dUcmYZi9NLr0l96QwF4UAXOQorixTQvo1qNaXqre4Ikxz0g2x/sOU08C9XNPeRMGzExiPWLKs/T3Sza5CaZ0cKhZDkO2QL0TR7AQViUQ==
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=Ian.Shillito AT anu.edu.au; spf=Pass smtp.mailfrom=Ian.Shillito AT anu.edu.au; spf=Pass smtp.helo=postmaster AT AUS01-ME3-obe.outbound.protection.outlook.com
Ironport-hdrordr: A9a23:j7vwY6P798k7t8BcT4n255DYdb4zR+YMi2TDiHoddfUFSKalfp6V98jzjSWE8Ar5K0tQ4uxoWZPwDU80kKQY3WB/B8bHYOCLggqVxcRZnPLfKl7bamLDH4xmpMBdmsFFYbWeY2SSz/yKhjVQeOxQo+VvhZrY4Ns2uE0dLz2CBZsB0y5JTiKgVmFmTghPApQ0ULCG4NBcmjamcXMLKuymG3gsRYH41pz2vaOjRSRDKw8s6QGIgz/twqX9CQKk0hAXVC4K6as+8FLCjxfy6syYwrGGI17npizuBqZt6Z7cI+h4dYixYw8uW3LRYzOTFcZcsnu5zXYISa+UmQ8XeZL30m0d1oxImg7slyeO0FXQMkDboUkTwmX/x1GVm2burPrwWS8zActEiYVFRAHU8VAhutZL0K8j5RPki7NHSRnanC76/bHzJmNXv1vxrnw4neEJiXtDFYMYdb9KtIQauFhYCZEaAUvBmcga+cRVfbfhDcxtABqnhrHizxpS6c3pWm52EgaNQ0AEtMDQ2z9KnGphx09dwMAEhH8P+J80VpEBvo3/Q+5VvaALStVTYbN2Be8HT8fyAmvRQQjUOGbXJVj8DqkIN3/Etpay6rQo4+OhfoAO0fIJ6d/8eUIdsXR3d1PlCMWI0pEO+hfRQH+lVTCo0c1a74gRgMyKeFMqC1z2dLkKqbrsnxwyOLyrZx+DAuMiPxa4FxqRJW9g5XyPZ6Vv
Ironport-phdr: A9a23:JJTRuhwkSa/vXoTXCzL5zVBlVkEcU1XcAAcZ59Idhq5Udez7ptK+ZhSZtKwm0QCBdL6YwsoMs/DRvaHkVD5Iyre6m1dGTqZxUQQYg94dhQ0qDZ3NI0T6KPn3c35yR5waBxdq8H6hLEdaBtv1aUHMrX2u9z4SHQj0ORZoKujvFYPekdi72/q29pHObAlFhDiwaq5uIRurqgncqtMYipZ4JKYrzRvJrHpIe+BIym5tOFmegRXy6Nqu8ZB66yhftO4v+MBGUaXhYqQ3VqdYAyg8M2A0/8Lkqx/ORhaS63QGU2UWlh1IAxXZ7Bz/Q5z8vDf2uvZ71SKHO8D9ULI6Vim476pzSBHmljoJNyI3/m/UhMx/jr5Urx26qhNl34LYfJuYOOZicq7fe94RWGpPXtxWVyxEGo6ybJEAD+wcNuhFr4n9pl8OrR+/BQmwA+Pk1zhFiHzs0q08yegvDAHG3A0kH9IKsXTUsNL1ObwIXuCz0anE1yvMYO5L2Tvn8ofIbwksrPeRVr1/bcTf01MgFx/ZjlqOs4zlOSuY2vgOvmWa8+duWuKihmEkpgx+rDWi2tsghInHiI8Jyl7J6yp3zZsoKNC6SkN3fMOpHIZeuSyeKYd7TN0vT3xmtSs817YIt5m7fC0Qx5QmwR7Sc+eHc4mH4hL7UOaeOzF4iGhieLKliBa+6U+gyvDgVsmw11ZKqSlFnsPQuXAK0hzf8smHSv1n/kegwzmDzQ7T6vtCLEsplqTbM4Ysz7EsmpYJrEjPAi37lF/rgKOKdUgo4PWk5/job7n+uJORNpN4hw/7P6gzhsCwHeU1Pw0TU2SH/Omwyb3u8lD8TbhPk/E7nK/Uu43AK8sBvK62GQpV354j6xmhCzem18wVkGUJI1xYZB6LkpHlNVbBLv32FPu/hE+jnylxy/DBI73hHo7CLn/ekLfnYLlx8VZcyBA0zdBD+Z1bFq0BIPP0Wk/3rtDYCQI5MxCww+bgD9V91ZkSVn6IAq+cKK/SsFmI6fwzI+SUa4IZpCzxJ+U56/Psl3M1hEMRcKqz0ZcKdHy1EexqI0CDbnrthtcBH30Kvg07TOHyi1ONSzhTa2yvUaI85zE7DIamDYbfRoCqm7GOxiG7HoBMam9YF1+MDG3keJ+ZW/sUciKdPtdhkiAYVbimU4IuyRautBbjx7V7KurU5zYXuIn41Nl14u3TjQs9+SZ1D8SbyWGNTnt7knkGRz8sj+hDphk3wVCalKN8nvZwFNpJ5voPXB1wfcrXyPU/ANTvUCrAeM2IQRCoWIP1Lys2S4cQytlGWEZ8H9GjkheLiwujBfkul72PAJ0o9YrV2WW3KspgjX/bgvpyx2I6S9dCYDX1zpV08BLeUtahe6qxnqC3M6kQwWjE6TXapYJvlGhla1YpFIDoBjUYbEaQqsnl7ETfSbPoEa4gLgZK1c+FLO1Nd8HtilJFAvzkPYaHC4pUs262GFCFyq7KZZe4Iw0g
Suggested_attachment_session_id: e1f56faa-8f18-c29c-47dd-8fac10b4f792

Hi Jason, Alan and Dominik,

Jason: thank you for your detailed explanation. The phenomenon you describe is indeed one I would like to avoid, as I intend to do some work on the proof theoretical aspect of the logic I am considering. De Bruijn indices seem to be the way to go!

Alan: I will have a look at your comparison. This sounds very interesting.

Dominik: thanks for the pointer! 🙂

Thank you all for your contributions!

Best,

Ian

From: coq-club-request AT inria.fr <coq-club-request AT inria.fr> on behalf of Dominik Kirst <dominik.kirst AT cs.uni-saarland.de>
Sent: Wednesday, 13 October 2021 2:38 AM
To: coq-club AT inria.fr <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Formalization of the syntax of first-order logic: binders

Just to add one more option: there is also Olivier Laurent’s anti-locally-nameless approach.

https://popl21.sigplan.org/details/CPP-2021/17/An-Anti-Locally-Nameless-Approach-to-Formalizing-Quantifiers

Best,

Dominik

On 12. Oct 2021, at 09:04, Alan Schmitt <alan.schmitt AT polytechnique.org> wrote:

On 2021-10-12 02:13, Jason Hu <fdhzs2010 AT hotmail.com> writes:

I would like to add that IMO, de Bruijn indices reflect the paper
proof the most faithfully, among the three methods mentioned here and
probably others.

We compared several methods (locally nameless, nominal, weak HOAS, and
full de Bruijn) in a completely different setting (a process calculus
with two kinds of binders and scope extrusion), and we found the most
concise method was de Bruijn, although they each have some advantages
and drawbacks. The work is available at
https://hal.inria.fr/hal-02536463v2/file/jar.pdf

Best,

Alan

[Coq-Club] Formalization of the syntax of first-order logic: binders, Ian Shillito, 10/11/2021
- Re: [Coq-Club] Formalization of the syntax of first-order logic: binders, Wilayat Khan, 10/11/2021
  - Re: [Coq-Club] Formalization of the syntax of first-order logic: binders, Pierre Courtieu, 10/11/2021
    - Re: [Coq-Club] Formalization of the syntax of first-order logic: binders, Carlos Olarte, 10/11/2021
      - Re: [Coq-Club] Formalization of the syntax of first-order logic: binders, Ian Shillito, 10/12/2021
        
        RE: [Coq-Club] Formalization of the syntax of first-order logic: binders, Jason Hu, 10/12/2021
        
        RE: [Coq-Club] Formalization of the syntax of first-order logic: binders, Alan Schmitt, 10/12/2021
        
        Re: [Coq-Club] Formalization of the syntax of first-order logic: binders, Dominik Kirst, 10/12/2021
        Re: [Coq-Club] Formalization of the syntax of first-order logic: binders, Ian Shillito, 10/14/2021