<p>Generally, there will be one context-free grammar for <em>both</em> types and terms, and judgements will be used to identify those expressions which are types and which expressions are terms of a particular type.</p>
<p>This has been written down many, many times. For a pretty typical example, you could look at Abel, Coquand and Dybjer's LICS 2007 paper, <a href="http://www2.tcs.ifi.lmu.de/%7Eabel/lics07.pdf" rel="nofollow noreferrer"><em>Normalization by Evaluation for Martin-Löf Type Theory with Typed Equality Judgements</em></a>.</p>

CC BY-SA 4.0
2021-04-26T13:38:28.197Z
Will all the strings produced by this grammar be typeable? Can't I write something like $a\to b$ where $a$ and $b$ are both terms?
neinoa
CC BY-SA 4.0
2021-04-26T16:43:59.570Z
@neinoa We separate syntax and type checking, because while syntactic properties can be expressed in a CFG, the properties you check with types are too strong for CFGs. That's already a problem for languages like Java.  Here are some example properties: Identifiers declared before use?  Types correctly
declared before use?  Inheritance relationships make sense? 
Classes and variables defined only once?  Methods defined only
once?  Private methods and members only used within the
defining class?
Martin Berger
CC BY-SA 4.0
2021-04-26T17:37:54.180Z
@MartinBerger but then I could also declare my formal language to be all finite sequences of $\Pi, \Sigma, \mathbf{0}, \mathbf{1}$ etc. and just typecheck that right? Is there say a context-sensitive grammar that is guaranteed to generate typeable things?
neinoa
CC BY-SA 4.0
2021-04-26T17:57:41.890Z
@neinoa Yes, that't a viable approach. It's called generate-and-filter. It tends not to be very effective, since almost all finite sequences over the alphabet $\{\Pi, \Sigma, ...\}$ are not typable. I imagine that typable terms have asymptotic density 0. However, you can 'read typing rules backwards' and generate only typable terms.
Martin Berger
CC BY-SA 4.0
2021-04-26T17:58:00.043Z
@neinoa I don't know the exact computational power needed for
type-checking MLTT, and how it relates to CSGs. There is usually
some mismatch between first-order approaches, such as
Chomsly-style grammars, and higher-order approaches.
Martin Berger
CC BY-SA 4.0
2021-04-26T13:16:51.603Z
2021-04-26T13:16:51.603Z
Neel Krishnaswami
<p>Are the terms and the types of Martin-Löf type theory described by context-free grammars? Have such grammars been written down somewhere?</p>

<reference-request><fl.formal-languages><type-theory><context-free>
Reference for context-free grammar for Martin-Löf type theory
neinoa
# Reference for context-free grammar for Martin-Löf type theory

(Asked by: username_0 on 2021-04-26)

Are the terms and the types of Martin-Löf type theory described by context-free grammars? Have such grammars been written down somewhere?

**Tags:** reference-request, fl.formal-languages, type-theory, context-free


---

## 1 answers

### Answer by username_1 on 2021-04-26. Score: 2

Generally, there will be one context-free grammar for *both* types and terms, and judgements will be used to identify those expressions which are types and which expressions are terms of a particular type.

This has been written down many, many times. For a pretty typical example, you could look at Abel, Coquand and Dybjer's LICS 2007 paper, [*Normalization by Evaluation for Martin-Löf Type Theory with Typed Equality Judgements*](http://www2.tcs.ifi.lmu.de/%7Eabel/lics07.pdf).

> **Comments:**
> **username_0**: Will all the strings produced by this grammar be typeable? Can't I write something like $a\to b$ where $a$ and $b$ are both terms?  
> **username_2**: @username_0 We separate syntax and type checking, because while syntactic properties can be expressed in a CFG, the properties you check with types are too strong for CFGs. That's already a problem for languages like Java.  Here are some example properties: Identifiers declared before use?  Types correctly declared before use?  Inheritance relationships make sense?  Classes and variables defined only once?  Methods defined only once?  Private methods and members only used within the defining class?  
> **username_0**: @MartinBerger but then I could also declare my formal language to be all finite sequences of $\Pi, \Sigma, \mathbf{0}, \mathbf{1}$ etc. and just typecheck that right? Is there say a context-sensitive grammar that is guaranteed to generate typeable things?  
> **username_2**: @username_0 Yes, that't a viable approach. It's called generate-and-filter. It tends not to be very effective, since almost all finite sequences over the alphabet $\{\Pi, \Sigma, ...\}$ are not typable. I imagine that typable terms have asymptotic density 0. However, you can 'read typing rules backwards' and generate only typable terms.  
> **username_2**: @username_0 I don't know the exact computational power needed for type-checking MLTT, and how it relates to CSGs. There is usually some mismatch between first-order approaches, such as Chomsly-style grammars, and higher-order approaches.  

---

