The Coq mailing list

[Ralf Jung <jung AT mpi-sws.org>]

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
> 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..

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



> 
> --------------------------------------------------------------------------------
> *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
>  
> <mailto: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
>     
> <mailto: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?
> 
>