# Proof that the calculus of constructions extended with recursive types isn't strongly normalizing?

What is the proof that the calculus of constructions, extended with recursive types (i.e., Fix at the type-level) isn't strongly normalizing?

With general recursive types you can define the type

type T = T -> T


With that type you can type self-application -- and in fact, every term of the untyped lambda calculus, including any of the well-known fixed-point operators. For example, the Y operator:

Y = \f:T. (\x:T. f (x x)) (\x:T. f (x x))

• It even suffices to have type $T = T \to A$ for some other type $A$. Then $Y I_A = \Omega$ will have type $A$. Of course, this is all because of the negative occurrence of $T$ in type $T \to A$. – Andrew Polonsky Apr 16 '17 at 18:01

Here is a slightly more explicit version of what Andreas said.

The term $(\lambda x . x x) (\lambda x . x x)$ is not normalizing because it has exactly one $\beta$-redex, and when we reduce it we get back to the same term. But this term has the type $T$ for any type $T$ satisfying $T = T \to T$.