6
$\begingroup$

In the pre-history of dependent type theory, Per Martin Löf introduced a calculus that is in some sense the simplest dependent type theory and the most general form of impredicative polymorphism. It is often referred to as Type:Type because the kind Type is itself of type Type. Unfortunately, it is inconsistent as a logic. This was discovered by Girard in his famous dissertation [1], who managed to express the Burali-Forti paradox in Type:Type. Various people have analysed, generalised and simplified Girard's analysis, see e.g. [2, 3]. This analysis seems to involve showing that non-terminating terms can be typed.

I have a question about non-termination: do we get non-normalisation at the level of types? By that I mean, is there a type $T$ such that the reduction relation $\rightarrow$ used, explicitly or implicitly, to define equality of types, gives rise to an infinite reduction sequence $$ T \rightarrow T' \rightarrow T'' \rightarrow \cdots? $$

[1] J.-Y.. Girard, Une extension de l'interpretation fonctionelle de Gödel a l'analyse.

[2] T. Coquand, A New Paradox in Type Theory.

[3] A. J. C. Hurkens, A Simplification of Girard's Paradox.

Improve this question
$\endgroup$

1 Answer 1

Reset to default
6
$\begingroup$

Short answer: yes.

Long answer: For $\mathrm{Type}:\mathrm{Type}$, non-termination at the type level is trivial. You can take a constant $X:\mathrm{False}\rightarrow \mathrm{Type}$. Then if you take the inconsistent term $\bot : \mathrm{False}$ you have $$ X\ \bot : \mathrm{Type}$$ Which is non-terminating at the type level. You might complain that this has a head normal form, which isn't what usually leads to inconsistency in type theory. In this case you can remember that $$ \mathrm{False}\equiv \forall X.\ X$$ and so $$ \bot\ \mathrm{Type}:\mathrm{Type}$$

Which has no head-normal form. In general, in this system the types and terms are so intertwined that the non-termination always seeps at the type level.

However, there is another system, called $U^-$, also described by Girard in his thesis, which was discovered to be inconsistent by Coquand (A New Paradox in Type Theory). This system is terminating at the type level, as it only has $\mathrm{system}\ F$ types at the kind level, and we know that terms are normalizing in that system (also a result of Girard!).

This means that non-termination at the type level is not necessary for having an inconsistent pure type system (a fact that I found out somewhat painfully after having proven an open question while depending on this fact).

Improve this answer
$\endgroup$
7
  • $\begingroup$ This is super interesting @cody, as I'm in fact trying to compare type theories where types may diverge with type theories where they don't. I wasn't really aware of $U^-$. $\endgroup$
    – Martin Berger
    Dec 18, 2013 at 20:58
  • 2
    $\begingroup$ It's an interesting subject! The thing is that usually what is more interesting is the equational theory at the type level. Normalization (confluence + termination) can give you good properties, but at the term level, you are really interested in termination, as this corresponds to cut-elimination (and implies consistency). There is some interesting work around this theme by Dowek and Werner: lix.polytechnique.fr/~werner/publis/moduloJSL.pdf $\endgroup$
    – cody
    Dec 19, 2013 at 9:38
  • 2
    $\begingroup$ It might be of interest that there is a dependently typed version of deduction modulo, $\lambda\Pi$-modulo. Here is a paper which briefly describes it: who.rocq.inria.fr/Gilles.Dowek/Publi/pts.pdf $\endgroup$
    – cody
    Dec 19, 2013 at 16:07
  • 1
    $\begingroup$ Cody, do you know if reduction modulo is implemented in real provers, interactive or automated? For me as an outsider it's a bit hard to work out exactly what rule systems are being use in which working provers. $\endgroup$
    – Martin Berger
    Dec 31, 2013 at 10:38
  • 1
    $\begingroup$ Well I do know that there is a nifty implementation of $\lambda\Pi$-modulo: rocq.inria.fr/deducteam/Dedukti Other than that, you might want to have a look at the really nice CoqMT system, that has similar motivations: pierre-yves.strub.nu/coqmt $\endgroup$
    – cody
    Dec 31, 2013 at 15:02

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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