8
$\begingroup$

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

$\endgroup$

migrated from cstheory.stackexchange.com May 26 '12 at 13:06

This question came from our site for theoretical computer scientists and researchers in related fields.

9
$\begingroup$

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

  1. computable syntax and rules of evaluation, and
  2. 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 $\lambda$-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 $\lambda$-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 $\lambda$-calculus, or Martin-Lof type theory, or the Calculus of constructions. (Exercise: if you could implement the normalization procedure, you could implement eval above.)

$\endgroup$
  • $\begingroup$ I'm afraid I can not parse your second explanatory sentence: Any programming language with 1. and 2. verifies what? I assume you wanted to say that no such language can exist... $\endgroup$ – cody May 26 '12 at 19:24
  • $\begingroup$ Sorry, messed up the text. It should read fine now. $\endgroup$ – Andrej Bauer May 26 '12 at 19:26
  • $\begingroup$ Cool, did not think of this. See here for the background of this answer. $\endgroup$ – Raphael May 27 '12 at 11:44
4
$\begingroup$

I find that merijn's answer handles the first part of your question quite well. I shall try to answer the second part: why finding functions that are computable but not representable in the polymorphic $\lambda$-calculus requires "standing on ones head".

I'm afraid it requires some explanation of the concepts that you are not interested in. A partial recusive function is a $\lambda$-term which represents a function from $\mathbb{N}$ to $\mathbb{N}\cup\{\bot\}$. A $\lambda$-term $t$ applied to the representative of a natural number $n$ is sent to $\bot$ if and only if $t\ n$ does not have a normal form. If no number is sent to $\bot$ we say that the function is total. Now the idea is that no logical theory $T$ can prove that a term $t$ represents a total function for each total function $t$, there are always "blind spots" where $t$ terminates on all input $n$, but the statement

$$ \forall n, t\ n\ \mbox{terminates}$$

is undecidable in $T$. If the above statement is provable in $T$, we say that the function represented by $t$ is provably total. That not all total functions are provably total in $T$ is a consequence of (a variant of) the Godel Incompleteness Theorem for $T$.

Now the point is that the vast majority program we concretely wish to write (list sorting, graph traversal, operating systems) are not only total functions, but are provably total in reasonable logical systems, like Peano Arithmetic.

Now for the polymorphic $\lambda$-calculus. It can be shown that the terms one can type in this calculus are exactly the terms which represent the functions provably total in Second Order Peano Arithmetic. Second Order Peano Arithmetic is much, much more powerful than ordinary Peano Arithmetic.

This means by the above explanations that there are terms which are total but not provably total, but such functions are extremely rare, as they are already rare for Peano Arithmetic (and so much rarer in the second-order theory). Hence the "standing on your head" statement.

$\endgroup$
  • 2
    $\begingroup$ You are missing conditions on your theory $T$, namely consistency and that the set of axioms is recursive, otherwise we can take as $T$ a theory whose set of axioms includes "$f$ terminates" for every $f$ that terminates. $\endgroup$ – Andrej Bauer May 26 '12 at 18:33
  • $\begingroup$ Thanks for those precisions, Andrej. A more complete explanation would probably also detail what we require of our theory, namely that the theory can at least express what it means to terminate (arithmetic with multiplication is sufficient, but I tend to favor slightly more expressive systems). $\endgroup$ – cody May 26 '12 at 19:20
  • $\begingroup$ Right, I think it's just fair to point out that there are some technical conditions missing, so the interested readers can go look them up. $\endgroup$ – Andrej Bauer May 26 '12 at 19:26
3
$\begingroup$

I'm finding it a bit hard to concisely write down the proof, but I hope this explanation provides you enough intuition to see why simple typed terms cannot represent all untyped terms.

The simply typed lambda calculus is strongly normalising. Every $\beta$ reduction will bring us closer to normal form. When the function $f :: \alpha \rightarrow \beta \rightarrow \gamma$ is applied to a value of type $\alpha$ it will $\beta$ reduce to a function of type $\beta \rightarrow \gamma$. Given a finite number of arguments it takes a finite number of reduction steps to reach $\beta$-normal form , in which there are no further possible reductions.

To contrast this with the untyped lambda calculus. One of the more famous UTLC combinators is the $Y$-combinator:

$Y = λf.(λx.f\; (x\; x))\; (λx.f\;(x\;x))$

When we try to reduce the $Y$-combinator the following happens:

$$λf.(λx.f\; (x\; x))\; (λx.f\;(x\;x))\; g$$ $$(λx.g\;(x\;x))\;(λx.g\;(x\;x))$$ $$g\;((λx.g\;(x\;x))\;(λx.g\;(x\;x)))$$ $$g\;(g\;((λx.g\;(x\;x))\;(λx.g\;(x\;x))))$$

No matter what functions we pass in, we get stuck in an infinite sequence of reductions! If we would try to pin a STLC type on the UTLC $Y$-combinator, we quickly find this impossible, because the function application doesn't shrink the type as is required in the STLC. The $Y$-combinator is clearly computable (it represents, using recursion, the concept of an infinite loop), yet it cannot be represented in the STLC, as all STLC terms are strongly normalising.

$\endgroup$
  • $\begingroup$ This argument has very little to do with the fact that not all total number-theoretic functions are representable in the type $\lambda$-calculus, which is what the question is about. In what sense is the $Y$ combinator a total function? $\endgroup$ – Andrej Bauer May 26 '12 at 18:35
  • $\begingroup$ @AndrejBauer The question ends with "I am looking for a simple explanation as to why certain computable functions cannot be represented by a typed term". How does my answer not cover this? The $Y$-combinator is an example of a computable function that cannot be represented by a simply typed term, and I hope my explanation was coherent enough to explain why it cannot be represented by a simply typed term. $\endgroup$ – merijn May 26 '12 at 18:55
  • $\begingroup$ Well, if you are going to interpret the question as asking for an example of a partial function which is not definable in the simply typed $\lambda$-calculus, then any such function will do (and the question is nonsense). For example, the one that is undefined everywhere. It is not definable in the simply typed $\lambda$-calculus either. The question is about total functions, as I read it. $\endgroup$ – Andrej Bauer May 26 '12 at 19:18

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.