Stream: Miscellaneous

Topic: Does Coq follow a context-free grammar?

Roman Bars (Apr 24 2021 at 14:06):

Are the valid type definitions in Coq a context-free grammar? What about valid definitions of closed terms of types in Type 0? Has anybody written this down in detail?

Li-yao (Apr 24 2021 at 15:12):

Do you mean the kind of grammar found in the reference manual? https://coq.inria.fr/distrib/current/refman/language/core/inductive.html

Paolo Giarrusso (Apr 26 2021 at 14:49):

The parser is ultimately LL(1), but there must be some extra state...

Paolo Giarrusso (Apr 26 2021 at 14:51):

For instance, because imports change the grammar, so you can't produce a real AST with a CFG parser

Pierre-Marie Pédrot (Apr 26 2021 at 14:51):

@Roman Bars are you talking about parsing of the syntax itself, or are you making a theoretical statement about the strength of the logic?

Pierre-Marie Pédrot (Apr 26 2021 at 14:52):

in the first case, the parsing engine is Turing-complete, although most fragments we use fit into a LL(1+ε) grammar

Paolo Giarrusso (Apr 26 2021 at 14:52):

(... In the sense that C is LR(1) but actually context sensitive)

Pierre-Marie Pédrot (Apr 26 2021 at 14:52):

in the second case, although I am not a specialist, this is probably not true

Pierre-Marie Pédrot (Apr 26 2021 at 14:54):

You can encode complex statements in the type-checking algorithm thanks to conversion, and it goes farther than CFG

Pierre-Marie Pédrot (Apr 26 2021 at 14:55):

(I wouldn't be surprised if System F type-checking is already not encodable in CFG, since it captures second-order arithmetic which has a crazy ordinal)

Paolo Giarrusso (Apr 26 2021 at 15:25):

I thought "typing is context-sensitive" was obvious folklore, even for STLC?

Pierre-Marie Pédrot (Apr 26 2021 at 15:27):

That's stuff from the 70's I vaguely heard about but have no practical knowledge of.

Paolo Giarrusso (Apr 26 2021 at 15:30):

IIUC, even if a complete argument might take a while, "type-checking is context-sensitive because it's sensitive to the context" encapsulates the complete answer accurately.

Pierre-Marie Pédrot (Apr 26 2021 at 15:31):

Proof. reflexivity. Qed.

Roman Bars (Apr 26 2021 at 18:26):

Paolo Giarrusso said:

I thought "typing is context-sensitive" was obvious folklore, even for STLC?

When you say context-sensitive do you mean context-sensitive in the sense of Chomsky or do you mean not context-free?

Paolo Giarrusso (Apr 27 2021 at 09:38):

Good question, @Roman Bars . I was thinking of Chomsky but the only obvious part is "beyond context free" so I should retract the rest.
I have seen parsing and typing described as "context-free" and "context-sensitive" in the literature, but it was taken for granted and not the main point. They might have known better, or not.

Last updated: Jun 01 2023 at 12:01 UTC