<p>With general recursive types you can define the type</p>

<pre><code>type T = T -&gt; T
</code></pre>

<p>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:</p>

<pre><code>Y = \f:T. (\x:T. f (x x)) (\x:T. f (x x))
</code></pre>

CC BY-SA 3.0
2017-04-16T18:01:35.297Z
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
CC BY-SA 3.0
2017-04-16T15:21:31.003Z
2017-04-16T15:21:31.003Z
Andreas Rossberg
<p>Here is a slightly more explicit version of what Andreas said.</p>

<p>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$.</p>

CC BY-SA 3.0
2017-04-16T17:15:08.943Z
2017-04-16T17:15:08.943Z
Andrej Bauer
<p>What is the proof that the calculus of constructions, extended with recursive types (i.e., Fix at the type-level) isn't strongly normalizing?</p>

<type-theory><lambda-calculus><normalization>
Proof that the calculus of constructions extended with recursive types isn't strongly normalizing?
MaiaVictor
# Proof that the calculus of constructions extended with recursive types isn't strongly normalizing?

(Asked by: username_0 on 2017-04-16)

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

**Tags:** type-theory, lambda-calculus, normalization

---

## 2 answers

### Answer by username_1 on 2017-04-16. Score: 11

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))

> **Comments:**
> **username_2**: 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$.  

---

### Answer by username_3 on 2017-04-16. Score: 7

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$.


---

