[Coq-Club] What Coq function definition `Definition Term := forall

[Alex Meyer]

I am reading about mechanization of linear logic in Coq
http://www.cs.cmu.edu/~iliano/projects/metaCLF2/inc/dl/papers/lsfa17.pdf and
https://github.com/brunofx86/LL and I have trouble to understand the the function definition Term(and other function definitions involving forall) from
https://github.com/brunofx86/LL/blob/master/FOLL/LL/SyntaxLL.v:


Definition Term := forall T:Type, term T. (* type for terms *)
Definition AProp := forall T:Type, aprop T. (* type for atomic propositions *)


Why we need forall construction in function definition, what additional meaning it gives? Is is creating some kind of set - i.e. - that function returns set of results - one result for each type.

I asked this question on stackoverflow:

https://stackoverflow.com/questions/51017013/what-coq-function-definition-definition-term-forall-t-type-term-t-means

and received one answer there but I would like to get more elaborate answer, I still does not understand this this construction. Maybe there is some good and exact reference in literature?

[ikdc]

[Carlos Olarte]

Dear Alex,
We used PHOAS [4] to encode the binders of (first order) linear logic.
The 'forall T' construction is needed to avoid exotic terms (Ie, terms that
do not correspond to any syntax)

Roughly, since the construction is parametric on any Type, an inhabitant of
Term or Aprop cannot do pattern matching on the input and generate
(structurally) different formulas.

This link from Adam Chilipala's book is quite useful to understand the
technique.

http://adam.chlipala.net/cpdt/html/Hoas.html

Best
Carlos

Looks like a PHOAS construction; see
http://adam.chlipala.net/papers/PhoasICFP08/ for details.
(Reference [4] in the paper you linked.)
I am reading about mechanization of linear logic in Coq
http://www.cs.cmu.edu/~iliano/projects/metaCLF2/inc/dl/papers/lsfa17.pdf and
https://github.com/brunofx86/LL and I have trouble to understand the the
function definition Term(and other function definitions involving forall)
from
Definition Term := forall T:Type, term T. (* type for terms *)
Definition AProp := forall T:Type, aprop T. (* type for atomic propositions *)
Why we need forall construction in function definition, what additional
meaning it gives? Is is creating some kind of set - i.e. - that function
returns set of results - one result for each type.
https://stackoverflow.com/questions/51017013/what-coq-function-definition-definition-term-forall-t-type-term-t-means
and received one answer there but I would like to get more elaborate
answer, I still does not understand this this construction. Maybe there is
some good and exact reference in literature?

[Alex Meyer]

Now I am reading http://adam.chlipala.net/cpdt/html/Hoas.html and the presentation is almost clear. But I am stuck with the estimation, that the following is the exotic term:

Example exotic_prop := Forall<http://adam.chlipala.net/cpdt/html/Hoas.html#Forall> (fun b : bool<http://coq.inria.fr/distrib/8.3pl2/stdlib/Coq.Init.Datatypes.html#bool> => if b then true_prop<http://adam.chlipala.net/cpdt/html/Hoas.html#true_prop> else false_prop<http://adam.chlipala.net/cpdt/html/Hoas.html#false_prop>).

Why it is called exotic terms, whats wrong with it? It is not so obvious for newbie..

________________________________
No: coq-club-***@inria.fr <coq-club-***@inria.fr> Carlos Olarte <***@gmail.com> vàrdà
Nosþtïts: svºtdiena, 2018. gada 1. jþlijs 10:19:51
Kam: coq-***@inria.fr
Tºma: Re: [Coq-Club] What Coq function definition `Definition Term := forall T: Type, term T.` means?

Dear Alex,
We used PHOAS [4] to encode the binders of (first order) linear logic. The 'forall T' construction is needed to avoid exotic terms (Ie, terms that do not correspond to any syntax)

Roughly, since the construction is parametric on any Type, an inhabitant of Term or Aprop cannot do pattern matching on the input and generate (structurally) different formulas.

This link from Adam Chilipala's book is quite useful to understand the technique.

http://adam.chlipala.net/cpdt/html/Hoas.html

Best
Carlos

On Sun, 1 Jul 2018 at 03:03 ikdc <***@mit.edu<mailto:***@mit.edu>> wrote:
Looks like a PHOAS construction; see http://adam.chlipala.net/papers/PhoasICFP08/ for details.

(Reference [4] in the paper you linked.)

On Jun 30, 2018 20:24, Alex Meyer <***@outlook.lv<mailto:***@outlook.lv>> wrote:

I am reading about mechanization of linear logic in Coq
http://www.cs.cmu.edu/~iliano/projects/metaCLF2/inc/dl/papers/lsfa17.pdf and
https://github.com/brunofx86/LL and I have trouble to understand the the function definition Term(and other function definitions involving forall) from
https://github.com/brunofx86/LL/blob/master/FOLL/LL/SyntaxLL.v:


Definition Term := forall T:Type, term T. (* type for terms *)
Definition AProp := forall T:Type, aprop T. (* type for atomic propositions *)


Why we need forall construction in function definition, what additional meaning it gives? Is is creating some kind of set - i.e. - that function returns set of results - one result for each type.

I asked this question on stackoverflow:

https://stackoverflow.com/questions/51017013/what-coq-function-definition-definition-term-forall-t-type-term-t-means

and received one answer there but I would like to get more elaborate answer, I still does not understand this this construction. Maybe there is some good and exact reference in literature?

[Ralf Jung]

Hi Alex,

Now I am reading http://adam.chlipala.net/cpdt/html/Hoas.html and the
presentation is almost clear. But I am stuck with the estimation, that the
Example exotic_prop := Forall
<http://adam.chlipala.net/cpdt/html/Hoas.html#Forall> (fun b : bool
<http://coq.inria.fr/distrib/8.3pl2/stdlib/Coq.Init.Datatypes.html#bool> => if b then true_prop
<http://adam.chlipala.net/cpdt/html/Hoas.html#true_prop> else false_prop
<http://adam.chlipala.net/cpdt/html/Hoas.html#false_prop>).
Why it is called exotic terms, whats wrong with it? It is not so obvious for newbie..

Indeed I have been wondering the same at first. I am very used to shallow
embeddings where this is normal.
However, this is supposed to be a deep embedding that faithfully represents the
following on-paper definition:

Prop \ni P, Q ::=
t = u
| ~P
| P /\ Q
| P \/ Q
| forall x, P
| exists x, P

In that grammar, it is impossible to write

Forall (fun b : bool => if b then 1 = 1 else ~(1 = 1))

So this being possible in Coq shows that the grammar is not adequately modeled.
Essentially, the problem is that this definition accidentally pulls in the
entire expressiveness of Coq.

Kind regards,
Ralf

--------------------------------------------------------------------------------
*Nosūtīts:* svētdiena, 2018. gada 1. jūlijs 10:19:51
*Tēma:* Re: [Coq-Club] What Coq function definition `Definition Term := forall
T: Type, term T.` means?
 
Dear Alex,
 We used PHOAS [4] to encode the binders of (first order) linear logic.  The
'forall T' construction is needed to avoid exotic terms (Ie, terms that do not
correspond to any syntax) 
Roughly, since the construction is parametric on any Type, an inhabitant of Term
or Aprop cannot do pattern matching on the input and generate (structurally)
different formulas. 
This link from Adam Chilipala's book is quite useful to understand the technique. 
http://adam.chlipala.net/cpdt/html/Hoas.html
Best 
Carlos 
Looks like a PHOAS construction;
see http://adam.chlipala.net/papers/PhoasICFP08/ for details.
(Reference [4] in the paper you linked.)
I am reading about mechanization of linear logic in Coq
http://www.cs.cmu.edu/~iliano/projects/metaCLF2/inc/dl/papers/lsfa17.pdf and
https://github.com/brunofx86/LL and I have trouble to understand the the
function definition |Term|(and other function definitions
involving |forall|) from
|Definition Term := forall T:Type, term T. (* type for terms *)
Definition AProp := forall T:Type, aprop T. (* type for atomic
propositions *) |
Why we need |forall| construction in function definition, what
additional meaning it gives? Is is creating some kind of set - i.e. -
that function returns set of results - one result for each type.
https://stackoverflow.com/questions/51017013/what-coq-function-definition-definition-term-forall-t-type-term-t-means
and received one answer there but I would like to get more elaborate
answer, I still does not understand this this construction. Maybe there
is some good and exact reference in literature?