The Coq mailing list

[Alex Meyer <alex153 AT outlook.lv>]

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 (fun b : bool => if b then true_prop else false_prop).

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

---

No: coq-club-request AT inria.fr <coq-club-request AT inria.fr> Carlos Olarte <carlos.olarte AT gmail.com> vārdā
Nosūtīts: svētdiena, 2018. gada 1. jūlijs 10:19:51
Kam: coq-club AT 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 <ikdc AT 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 <alex153 AT 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?