Reading the paper An Introduction to the Lambda Calculus, I came across a paragr

Question

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

Explanation / Answer

Given that you do not want to learn precise concepts, here is an intuitive explanation. In the discussion below "function" always refers to a function mapping natural numbers to natural numbers (possibly undefined at some arguments).

Any programming language which has

computable syntax and rules of evaluation, and
implements every total computable function

necessarily implements some partial functions.

To see this, suppose it were the case that every definable function in this language were total. Because the language has computable syntax, we can enumerate all definitions of functions (just enumerate all strings and filter out those that cause syntactic errors). Because the rules of evaluation are computable, the second assumption allows us to conclude that in our language we can define the total function eval(n,m) which evaluates the n-th definable function on m (essentially this is an mini-interpreter written in the language itself). But then the function

? k . (1 + eval(k,k))

is a total definable function which is different from every total definable function, a contradiction.

The simply typed ?-calculus satisfies the first condition and it defines only total functions. Therefore it does not satisfy the second condition.

As far as "standing on your head" is concerned, for a strongly-normalizing ?-calculus it is fairly easy to provide a total function which is not definable in the calculus, namely the normalization procedure itself. It is not very important how fancy your strongly normalizing calculus is, it could be the polymorphic ?-calculus, or Martin-Lof type theory, or the Calculus of constructions. (Exercise: if you could implement the normalization procedure, you could implement eval above.)

Related Questions

Navigate

• Browse (All)
• Browse R
• Subjects

Integrity-first tutoring: explanations and feedback only — we do not complete graded work. Learn more.