Reading the paper An Introduction to the Lambda Calculus, I came across a paragraph I didn't really understand, on page 34 (my italics):Within each of the two paradigms there are several versions of typed  lambda calculus. In many important systems, especially those a la  Church, it is the case that terms that do have a type always possess a  normal form. By the unsolvability of the halting problem this  implies that not all computable functions can be represented by a  typed term, see Barendregt (1990), Theorem 4.2.15. This is not so bad  as it sounds, because in order to find such computable functions that  cannot be represented, one has to stand on one's head. For example in  2, the second order typed lambda calculus, only those partial  recursive functions cannot be represented that happen to be total,  but not provably so in mathematical analysis (second order  arithmetic).I am familiar with most of these concepts, but not the concept of a partial recursive function, nor the concept of a provably total function. However, this is not what I am interested in learning.I am looking for a simple explanation as to why certain computable functions cannot be represented by a typed term, as well as to why such functions can only be found 'by standing on one's head.'
Simple explanation as to why certain computable functions cannot be represented by a typed term?
computability;logic;lambda calculus;type theory