Problem Detail: 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.
Asked By : Martin Berger
Answered By : cody
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).
Best Answer from StackOverflow
Question Source : http://cs.stackexchange.com/questions/19065 Ask a Question Download Related Notes/Documents
