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: Wilayat Khan <wilayatk AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Formalization of the syntax of first-order logic: binders
Date: Mon, 11 Oct 2021 13:53:43 +0500
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=wilayatk AT gmail.com; spf=Pass smtp.mailfrom=wilayatk AT gmail.com; spf=None smtp.helo=postmaster AT mail-vk1-f182.google.com
Ironport-hdrordr: A9a23:C9GYGK7X7V/8k8aD8APXwMfXdLJyesId70hD6qkRc20yTiX8raqTdZsgpH3JYVoqOE3I+urwW5VoI0mskKKdiLN5VdzCYOCMghrNEGgN1/qE/9QiIUHDHyxmuJuIv5IQNDQ4NzZHsfo=
Ironport-phdr: A9a23:PsxXyR9KXsET6v9uWd28ngc9DxPPW53KNwIYoqAql6hJOvz6uci4ZAqOvL4w0xfgZsby07p8ke3YsqTtCyQrwK2qlzQ8SqFKTAIPks4MngYtU4avAEz/K+P2PWRhRJwRHFBq8GumPkdLBc3we0PdomGo7T4VBx7zKRd5Kv76F4LMk8i7zeS/94DcbwhIhje2fK9/IgixoQjNrMcdnJFsKrw2yhvHo3tIf/pZyGZ1Ll+NnBjy+9m98od7/ytfp/wu+chAUb7nf6sjVrxXEC4mM2Eu68L1sxTIUBaC6WEdUmUSlRpIHhTF4RTnVZr/rif2quxw0zScMMbrT747RC6i4r9kRx/miigJNzA3/mLKhMJukK1WuwiuqwBlzoPOfI2ZKPhzc6XAdt0aX2pBWcNRWjRBDYO9a4sAFeoAMvxEr4LgolUOrQGxBQ+xD+7oxD5Ih3v20rc60us7DQHG3xctH90LsHvOrdX1ML0eXvyyzKnN1DjOae5d1jjh5obSaB8hve2MUqxqccrX0UQiGB3Jg1SOpILrIT6Y1+sDvmiU4udgWu+hhHIqph9yrzWx28shlInEi4IXx13H6Cl13Ig4K928RUN4btCpEpVeuieHPIV4RcMiRntnuCc8yrAepJ67eikKxI08xxHFcfOHaYyI7QjlVOmMOzt3mWxqdKqwhxaz7UigyvD8WdKu3FlWqSpFl9/BvW0O2RzL8sWLVOdx80O71TuM1w3f8P9ILV4pmabBNpIswaA8m5wOukrZBCD2gl/5jKqOe0Uk5Oeo7+Pnb63jppCGNo90jhjyMrotmsCiGOg4PBUCUmuF9eim273j+kr5QLpOjvIoiKXWrJfaJcEDqq64BQ9azJoj5g6hAzu61NkUh3oKIVJfdB6ZkYTlJkvCLO37APuhm1islS1kx/HCPr3vGJXNKX3Dna/vfLZ8705T0goywspD55JXEbwBL/fzVVXwtNzcFBM2Lwu0w+P/BNVnyoweQX6PArOeMK7KrVCI4fsvL/CQa48RpTbyMOMo5+XujH88gV8SZ7Ol3ZoRaHCiH/RpOV+VYXT2goRJLWBftQ0nCefulVeqUDhJZn/0UbhvyCs8DdeZDIPKV4mxyJ+B1SHzSoJXYmlXA0yPOXjtfoSAHfwLbXTBcYdajjUYWO35GMca3ha0uVqio1KIBuXR8ywc85nk0YosjwUyvRQ79DgxEcfElm/UHzsykWQPSDs7mqt4pB4lor9m+ad9iv1cU9dU4qEROjo=

Hi Ian

In the past, I have used both in formalising Android type system. In locally nameless representation, bound variables are represented with de Bruijn indices. You might be interested to have a look at our paper, in particular the Section II-D and Coq formalization.

Best,

Wilayat

On Mon, Oct 11, 2021 at 1:42 PM Ian Shillito <Ian.Shillito AT anu.edu.au> wrote:

Hi all,

I am about to start the formalisation of a proof of completeness for an extension of first-order intuitionistic logic. As a consequence I need to find a way to formalise the quantifiers of the FO syntax, and thus formalise binders.

It seems that there are already some approaches in the literature using:

de Bruijn indices (https://www.ps.uni-saarland.de/autosubst/ put in action in https://www.ps.uni-saarland.de/extras/fol-completeness/)
locally nameless (https://github.com/plclub/lngen could be used here?)

Are there arguments for using the one over the other? Are there other approaches? Do you have any experience to share about the formalisation of FO syntax?

Thanks in advance for your comments and thoughts!

Best,

Ian

[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