The Coq mailing list

[Jason Hu <fdhzs2010 AT hotmail.com>]

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. One very, if not the most, important problem of locally nameless representation and PHOAS is that they prevents you from counting the sizes or depths of derivations. Recall that, on paper, all proof trees are finite and their depths and sizes are countable. However, with locally nameless representation and PHOAS, you will find that the derivation of a universal quantification is over a meta-level dependent function. This function has larger cardinal than natural numbers so you will not be able to count the depth or size of it or even give it a upper bound. Just to give a more concrete example, with locally nameless representation, you might have the following premise in your derivation of universal quantification:

 

forall x, x \notin L -> G, x |- open t x : open P x

 

where L is some finite name store which an arbitrary name must avoid. Open is the operation in locally nameless representation which replaces the de Bruijn index 0 with x. Notice that the type of this premise does not prevent you from implementing this type as follows:

 

if x == “var1” then …

else if x == “var2” then …

else …

 

That is, even though it makes no sense to do so, this premise can do enough inspection of x, so that the resulting G, x |- open t x : open P x has a different size for every x.  I feel that to make locally nameless representation as “faithful” as de Bruijn indices, some sort of extra naturality conditions should be required to prevent the proof body from doing inspection of variables like the one above. In this sense, PHOAS seems in a better situation but I haven’t work with PHOAS so I am not sure how far it will go.

 

Thanks,

Jason Hu

 

From: Ian Shillito
Sent: Monday, October 11, 2021 9:47 PM
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Formalization of the syntax of first-order logic: binders

 

Hi Wilayat, Pierre and Carlos, 

 

Thank you all for your suggestions and references. I will have a look at them and figure out which one is the most convenient for me.

 

At least, what I gather from these suggestions is that there is no canonical way to formalize the syntax of FO on which the community unanimously agrees (if this phenomenon ever happens...). 

 

Best,

Ian

From: coq-club-request AT inria.fr <coq-club-request AT inria.fr> on behalf of Carlos Olarte <carlos.olarte AT gmail.com>
Sent: Monday, 11 October 2021 11:12 PM
To: coq-club AT inria.fr <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Formalization of the syntax of first-order logic: binders

 

Hi Ian,

 We have formalized first-order logics using both PHOAS
https://aus01.safelinks.protection.outlook.com/?url="https%3A%2F%2Fgithub.com%2Fmeta-logic%2Fcoq-ll%2F&amp;data=04%7C01%7Cian.shillito%40anu.edu.au%7C24ab8bbed1a8469d235408d98cb0789a%7Ce37d725cab5c46249ae5f0533e486437%7C0%7C0%7C637695512876278861%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&amp;sdata=eoxTwkT737xLNJmEGUtdoFL8XtcXaTNSm7NcojbTVd0%3D&amp;reserved=0

 and de Bruijn style (with Hybrid, a two-level system)
https://aus01.safelinks.protection.outlook.com/?url="https%3A%2F%2Fgithub.com%2Fmeta-logic%2Fcoq-fll&amp;data=04%7C01%7Cian.shillito%40anu.edu.au%7C24ab8bbed1a8469d235408d98cb0789a%7Ce37d725cab5c46249ae5f0533e486437%7C0%7C0%7C637695512876288817%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&amp;sdata=DJyjDZpM02xfIYwkJA4CiVhgN3wr6CCwVKM%2BySSl8eM%3D&amp;reserved=0

Best regards,
Carlos.





On Mon, Oct 11 2021 at 11:35:44 AM +0200, Pierre Courtieu
<Pierre.Courtieu AT cnam.fr> wrote:
> Hi,
> Third possibility: PHOAS, although I don't know if it is interesting
> in your setting.
> See https://aus01.safelinks.protection.outlook.com/?url="http%3A%2F%2Fadam.chlipala.net%2Fpapers%2FPhoasICFP08&amp;data=04%7C01%7Cian.shillito%40anu.edu.au%7C24ab8bbed1a8469d235408d98cb0789a%7Ce37d725cab5c46249ae5f0533e486437%7C0%7C0%7C637695512876288817%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&amp;sdata=uOzADtspq6d2nm55a4B2BT5b7uhwM0uRhQMxrc%2BA%2F7M%3D&amp;reserved=0.
> Pierre
>
> P.
>
> Le lun. 11 oct. 2021 à 10:54, Wilayat Khan <wilayatk AT gmail.com> a
> écrit :
>>
>>  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://aus01.safelinks.protection.outlook.com/?url="https%3A%2F%2Fwww.ps.uni-saarland.de%2Fautosubst%2F&amp;data=04%7C01%7Cian.shillito%40anu.edu.au%7C24ab8bbed1a8469d235408d98cb0789a%7Ce37d725cab5c46249ae5f0533e486437%7C0%7C0%7C637695512876288817%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&amp;sdata=Ol%2F%2BMpFi7M0XMTs6vP2C3tV2wSiI%2BVmFk0m0fVUAM6c%3D&amp;reserved=0" put
>>> in action in
>>> https://aus01.safelinks.protection.outlook.com/?url="https%3A%2F%2Fwww.ps.uni-saarland.de%2Fextras%2Ffol-completeness%2F&amp;data=04%7C01%7Cian.shillito%40anu.edu.au%7C24ab8bbed1a8469d235408d98cb0789a%7Ce37d725cab5c46249ae5f0533e486437%7C0%7C0%7C637695512876288817%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&amp;sdata=PYt%2F4BRldHXQWuS7aZyDdhR9jWWdq9pB%2BlFbienzWeE%3D&amp;reserved=0)
>>>  locally nameless (https://aus01.safelinks.protection.outlook.com/?url="https%3A%2F%2Fgithub.com%2Fplclub%2Flngen&amp;data=04%7C01%7Cian.shillito%40anu.edu.au%7C24ab8bbed1a8469d235408d98cb0789a%7Ce37d725cab5c46249ae5f0533e486437%7C0%7C0%7C637695512876288817%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&amp;sdata=Z%2BEKGm1WFm7qxVePW6yhTc0MJ26r5NXeejrDIxXTzP4%3D&amp;reserved=0" 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