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?
Do you mean the kind of grammar found in the reference manual? https://coq.inria.fr/distrib/current/refman/language/core/inductive.html
The parser is ultimately LL(1), but there must be some extra state...
For instance, because imports change the grammar, so you can't produce a real AST with a CFG parser
@Roman Bars are you talking about parsing of the syntax itself, or are you making a theoretical statement about the strength of the logic?
in the first case, the parsing engine is Turing-complete, although most fragments we use fit into a LL(1+ε) grammar
(... In the sense that C is LR(1) but actually context sensitive)
in the second case, although I am not a specialist, this is probably not true
You can encode complex statements in the type-checking algorithm thanks to conversion, and it goes farther than CFG
(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)
I thought "typing is context-sensitive" was obvious folklore, even for STLC?
That's stuff from the 70's I vaguely heard about but have no practical knowledge of.
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.
Proof. reflexivity. Qed.
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?
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