0
$\begingroup$

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

$\endgroup$
2
$\begingroup$

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.

$\endgroup$
5
  • $\begingroup$ 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? $\endgroup$ – neinoa Apr 26 at 13:38
  • $\begingroup$ @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? $\endgroup$ – Martin Berger Apr 26 at 16:43
  • $\begingroup$ @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? $\endgroup$ – neinoa Apr 26 at 17:37
  • $\begingroup$ @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. $\endgroup$ – Martin Berger Apr 26 at 17:57
  • $\begingroup$ @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. $\endgroup$ – Martin Berger Apr 26 at 17:58

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.