If a type system can assign a type to λ x . x x, or to the non-terminating (λx . x x) (λ x . x x), then is that system inconsistent as a consequence? Is every type under that system inhabited? Can you prove false?
$\begingroup$
$\endgroup$
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
6
Certainly, assigning a type to $\lambda x. x\ x$ is not enough for inconsistency: in system $F$, we can derive $$ \lambda x.x\ x:(\forall X.X)\rightarrow (\forall X.X)$$
in a pretty straightforward way (this is a good exercise!). However, $(\lambda x.x\ x)(\lambda x.x\ x)$ cannot be well typed in this system, assuming $\omega$-consistency of 2nd order arithmetic, as this implies that all such well-typed terms are normalizing.
Furthermore, system $F$ is consistent. This follows from either normalization, as one can show that any term of type $\forall X.X$ cannot have a normal form, or a much simpler argument, in which each type is assigned a set, either $\varnothing$ or $\{\varnothing\}$ and it can be shown that all derivable types are assigned $\{\varnothing\}$, and $\forall X.X$ is assigned $\varnothing$ (and is therefore not derivable).
The latter argument can be carried out in first-order arithmetic. The fact that $\lambda x.x\ x$ can be well-typed in a consistent system can be seen as somewhat disturbing, and is a consequence of the systems' impredicativity. It shouldn't come as a surprise that some people question the trustworthiness of impredicative systems of logic. However, no inconsistencies have been found so far in such systems.
On the other hand, to be able to make the more general assertion that $(\lambda x.x\ x)(\lambda x.x\ x)$ cannot be well-typed in a consistent system, you need to have enough "logical structure" in your type system to be able to clearly define consistency. Then you need to show that a term without a head normal form (like the one above) can have any type, which is also not obvious!
More details can be found in my answer to a related question: https://cstheory.stackexchange.com/a/31321/3984
-
4$\begingroup$ From reading those answers I see you obviously have a great understanding of the matter. I'd like to learn more, but I'm not sure where to look for. I've glanced through the TAPL book and it doesn't mention any of that, so I'm not sure this is a Type Theory subject. Could you point me what CS/math areas are related to this question, and perhaps a few books/articles? Thank you very much. $\endgroup$ Commented Oct 23, 2016 at 15:42
-
2$\begingroup$ I'm not sure that these questions are an "area of research" per se, more like a few fun questions which would have been answered long ago if there was some serious effort from experts. It's definitely a type theory subject, and the theory of Pure Type Systems has the advantage of make the problem definite and constrained. I'd probably recommend the Coquand-Herbelin paper from the other thread. $\endgroup$– codyCommented Oct 23, 2016 at 17:34
-
3$\begingroup$ Similar questions have been asked, for example here and here. I'd add Barendregt's "lambda calculi with types" to the list. $\endgroup$– codyCommented Oct 23, 2016 at 19:28
-
1$\begingroup$ What's the syntax here? I expected to see $ \lambda x : (\forall X . X) . \Lambda Y . x [Y \to Y] \; (x [Y])$ for a term of type $(\forall X . X) \to (\forall X . X)$. $\endgroup$ Commented Oct 24, 2016 at 11:49
-
1$\begingroup$ @AndrejBauer it's the "implicit" syntax, where there are no annotations on the $\lambda$s, and type abstractions and applications are omitted. You could also give: $\lambda x:(\forall X.X). x[(\forall X.X)\rightarrow(\forall X.X)]\ x$ if you like. Type inference is undecidable here but this is somewhat orthogonal to the question. Things are of course not so clear when you have dependent types, but there are versions of e.g. the CoC with implicit quantifications (Miquel's Calculus of Implicit Constructions), so the question remains relevant. $\endgroup$– codyCommented Oct 24, 2016 at 13:36