1
$\begingroup$

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

$\endgroup$
9
$\begingroup$

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))
$\endgroup$
  • 1
    $\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$ – Andrew Polonsky Apr 16 '17 at 18:01
6
$\begingroup$

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

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.