Many terms have a type in this framework. But also many terms do not have a type. Certainly, there is no type for the auto-application. But also there is no type for this term Y. We do not have time here to discuss in depth what this term does, but we may just say that this term Y is the term that is able to compute fixed points. Anyway, a very important property that we get from types is the so-called normalisation property. Any term that has a type normalises. That means that any term in this framework has a normal form. However, only few functions are definable in this typed framework. So, while in the untyped case we got all Turing computable functions, here we have only few functions.

---