What is the proof that the calculus of constructions, extended with recursive types (i.e., Fix at the type-level) isn't strongly normalizing?
Add a comment
|
2 Answers
$\begingroup$
$\endgroup$
1
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))
answered Apr 16, 2017 at 15:21
-
2$\begingroup$ 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$. $\endgroup$ Apr 16, 2017 at 18:01
$\begingroup$
$\endgroup$
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$.
answered Apr 16, 2017 at 17:15