<p>A nice example is given by Godelization: in lambda calculus, the only thing you can do with a function is to apply it. As a result, there is no way to write a closed function of type $(\mathbb{N} \to \mathbb{N}) \to \mathbb{N}$, which takes a function argument and returns a Godel code for it. </p>

<p>Adding this as an axiom to Heyting arithmetic is usually called "the constructive Church thesis", and is a strongly anti-classical axiom. Namely, it is consistent to add it to HA, but not to Peano arithmetic! (Basically, it is a classical fact that every Turing machine halts or not, and there is no computable function that can witness this fact.) </p>

CC BY-SA 3.0
2012-01-18T19:43:48.970Z
I don't understand how this is consistent with an extensional theory: take f and g extensionally equal, but with different implementations and therefore different godel codes. Does your function return the same number for f and g?
cody
CC BY-SA 3.0
2012-01-20T06:17:40.453Z
It's not consistent with extensionality! However, in HA $\forall$ and $\exists$ are logical connectives, not functions/records. So they have to be realizable but their  realizers don't have to be extensional. Andrej Bauer is an expert on this stuff, so if you ask a question you're sure to get a good answer.
Neel Krishnaswami
CC BY-SA 3.0
2012-01-10T17:47:11.647Z
2012-01-10T17:47:11.647Z
Neel Krishnaswami
<p>The untyped $\lambda$-calculus posseses general recursion in the form of the $Y$ combinator. Simply-typed $\lambda$-calculus does not. Thus, any function that requires general recursion is a candidate, for example the Ackermann function. (I am skipping some details on how precisely we represent the natural numbers in each system, but essentially any reasonable approach will do.)</p>

<p>Of course, you can always extend the simply-typed $\lambda$-calculus to match the power of $Y$, but then you're changing the rules of the game.</p>

CC BY-SA 3.0
2012-01-11T00:08:12.667Z
For some reason I'd had it in my head that you could do Ackermann in System F...
Rob Simmons
CC BY-SA 3.0
2012-01-11T01:36:21.700Z
@Rob, as I understand, Andrej doesn't say that is not the case.
Kaveh
CC BY-SA 3.0
2012-01-11T12:53:02.037Z
I suppose I said that the Ackermann function can be programmed in the untyped $\lambda$-calculus (because every computable function can), but no the simply typed $\lambda$-calculus. I said nothing about System F.
Andrej Bauer
CC BY-SA 3.0
2012-01-11T15:57:47.577Z
Oh, right, I was just being dumb. (Because the question was pretty ambiguous between talking about System F and talking about STLC, I picked the stronger system and forgot about the simpler question.)
Rob Simmons
CC BY-SA 3.0
2012-01-20T01:53:44.393Z
The Ackermann function in $\lambda$-calculus is $\lambda m.m(\lambda f n.n f(f \underline{1}))~\mathsf{suc}$. According to a type inferencer I built this semester, it has simple type: $(((((f \to e) \to f \to e) \to h) \to ((((f \to e) \to f \to e) \to h)$ $\to h \to g) \to g) \to (((b \to c) \to a \to b) \to (b \to c) \to a \to c) \to d) \to d$, which is atrocious, but possibly correct. The problem with STS isn't Ackermann -- it's, for example, simulating a Turing machine. You simply can't do that without the $Y$ combinator.
Francisco Mota
CC BY-SA 3.0
2012-01-20T02:04:38.417Z
Hmm. I tried passing $\underline{2}$ as the first argument to the function, and the type inferencer fails. I can pass $\underline{1}$ just fine, though, and I can pass any number for the second argument. So, it's possible to represent the Ackermann function ... it's just not possible to run $\mathsf{ack}~\underline{m}~\underline{n}$ for $m \geq 2$. ...
Francisco Mota
CC BY-SA 3.0
2012-01-20T13:30:40.347Z
You should either have a builtin type `nat` with primitive recursion, or encode numbers as iterators of type `(o -> o) -> (o -> o)` where `o` is some basic type. So even though your $\lambda$-exprression for Ackermann does the right thing, it cannot be typed in the right way. Of course, in the untyped $\lambda$-calculus types do not impose any limitations and everything works. By the way, you can plug in your program into ocaml and Haskell, too. They will compute the same type.
Andrej Bauer
CC BY-SA 3.0
2012-01-10T23:45:54.830Z
2012-01-10T23:45:54.830Z
Andrej Bauer
<p>The simplest answer is given by the fact that typed lambda calculi correspond to logics (simply typed lambda calculus -> predicate logic; system f -> second-order logic) and consistent logics cannot prove their own consistency.</p>

<p>So let's say that you have natural numbers (or a Church encoding of natural numbers) in your typed lambda calculus. It's possible to do a G&ouml;del numbering that assigns every term in System F to a unique natural number. Then, there is a function $f$ that takes any natural number (that corresponds to a well-typed term in System F) to another natural number (that corresponds to the normal form of that well-typed System F term) and does something else for any natural number that doesn't correspond to a well-typed term in System F (say, it returns zero). The function $f$ is computable, so it can be computed by the untyped lambda calculus but not the typed lambda calculus (because the latter would amount to a proof of the consistency of second-order logic <i>in</i> second-order logic, which would imply that second-order logic is inconsistent).</p>

<p>Caveat 1: If second-order logic <i>is</i> inconsistent, it <i>might</i> be possible to write $f$ in System F... and/or it <i>might</i> not be possible to write $f$ in the untyped lambda calculus - you could write something, but it might not always terminate, which is a criteria for "computable."</p>

<p>Caveat 2: Sometimes by "simply typed lambda calculus" people mean "simply typed lambda calculus with a fixed-point operator or recursive functions." This would be more-or-less <a href="http://en.wikipedia.org/wiki/Programming_Computable_Functions">PCF</a>, which can compute any computable function, just like the untyped lambda calculus.</p>

CC BY-SA 3.0
2012-01-10T15:19:37.373Z
2012-01-10T15:19:37.373Z
Rob Simmons
<p>The simply-typed lambda calculus is actually surprisingly weak.  For example, it can't recognize the regular language $\mathtt{a}^*$.  I've never found a precise characterization of the set of languages that STLC can recognize, though.</p>

CC BY-SA 3.0
2012-01-11T16:51:42.320Z
I think what is computable depends on the types you are looking at. When you represent naturals over the type $(p \to p) \to p \to p$, where $p$ is a base type, and take equality to be beta-equality, the definable functions are the extended polynomials (polynomials + if-then-else). IIRC, Schwichtenberg proved this, though I have never read his original paper (in German). (I think the paper name, translated, is "Definable Functions in Typed Lambda Calculi", 1976.)
Neel Krishnaswami
CC BY-SA 3.0
2012-01-12T13:06:18.650Z
@ Neel. A slighly better translation would be _Definable Functions in the $\lambda$-calculus with Types_. You can download it [here](http://epub.ub.uni-muenchen.de/4273), it's only two pages long. Is it know what happens at other types, with other notions of equality, or with other encodings of natural numbers?
Martin Berger
CC BY-SA 3.0
2012-01-12T15:37:14.837Z
@Marting: Thanks! I'm living in Germany now, so this is a nice extra incentive to practice my German. :)
Neel Krishnaswami
CC BY-SA 3.0
2012-01-11T15:20:02.223Z
2012-01-11T15:20:02.223Z
Sam Tobin-Hochstadt
<p>One vision of the limits of strongly normalizing calculi I like is the computability angle. In a strongly normalizing typed calculus, such as the core simply-typed lambda calculus, System F, or Calculus of Constructions, you have a proof that all terms eventually terminate.</p>

<p><em>If</em> this proof is constructive, you get a fixed algorithm to evaluate all terms with a guaranteed upper-bound on the computation time. Or you can also study the (not-necessarily-constructive) proof and extract an upper-bound from it -- which is likely to be <em>huge</em>, because those calculi are expressive.</p>

<p>This bounds gives you "natural" examples of function that cannot be typed in this fixed lambda-calculus : all arithmetic functions that are asymptotically superior to this bound.</p>

<p>If I remember correctly, terms typed in the simply-typed lambda-calculus can be evaluated in towers of exponential : <code>O(2^(2^(...(2^n)..)</code>; a function growing faster than all such towers won't be expressible in this calculi. System F corresponds to intuitionistic second-order logic, so the computability power is simply enormous. To seize the computability strength of even more powerful theories, we usually reason in terms of set theory and model theory (eg. what ordinals can be built) instead of computability theory.</p>

CC BY-SA 3.0
2012-01-11T09:40:30.810Z
2012-01-11T09:40:30.810Z
gasche
<p>If I understand your question correctly, I think a simple example is the term $\Delta = \lambda x. x x$, which takes a function and applies it to itself. You can define and reduce this function in the untyped lambda calculus (and in particular, you have $\Delta \Delta \to_\beta ~\Delta \Delta$, which is not normalizing), but you can't type $\Delta$, because that would mean finding a type $A$ such that $A = A \to A$. </p>

CC BY-SA 3.0
2012-01-23T04:59:09.187Z
We should be careful about what we mean by typed $\lambda$-calculus. Having a type $A$ s.t. $A\equiv A \to A$ is not strange.
Kaveh
CC BY-SA 3.0
2012-01-23T10:31:50.103Z
Yes, you're right, but I thought (maybe I'm wrong) that it was not possible to have such a type in the simply-typed lambda-calculus or System F, which are both strongly normalizing.
Charles
CC BY-SA 3.0
2015-09-10T17:46:57.437Z
I'm not sure if this argument holds: we not only need to show that $\Delta\Delta$ is not typeable, but that there is no typed lambda-term which is equivalent to $\Delta\Delta$. The easiest way to do this is by pointing to the fact that typed lambda calculus is strongly normalizing.
lambda.xy.x
CC BY-SA 3.0
2017-01-18T16:34:42.640Z
@Kaveh Why is having a type `A` such that `A \ident A \rightarrow A` not strange? It sounds absurd to me, what am I overlooking?
Martijn
CC BY-SA 3.0
2017-01-18T21:50:15.487Z
You are probably thinking classically about sets and function spaces over them. Think e.g. about finite binary strings and computable functions over them.
Kaveh
CC BY-SA 3.0
2012-01-20T00:24:26.437Z
2012-01-20T00:24:26.437Z
Charles
<p>I just want to know some examples of the functions that can be computed by the untyped lambda calculus but not by typed lambda calculi.</p>

<p>As I am a beginner, some reiteration of background information would be appreciated.</p>

<p>Thanks.</p>

<p>Edit: by typed lambda calculi, I was intending to know about System F and the simply-typed lambda calculus. By function, I mean any Turing-computable function. </p>

CC BY-SA 3.0
2012-01-10T12:10:12.357Z
Many typing disciplines exist for $\lambda$-calculi, and the answer to your request depends partly on which choice of typing discipline you have in mind. It also depends on what you mean by function. One example of a difference would be that typing disciplines such as [System F](http://en.wikipedia.org/wiki/System_F) can only type normalising programs, while the untyped $\lambda$-calculus contains non-normalising terms.
Martin Berger
CC BY-SA 3.0
2012-01-10T12:31:31.110Z
I was thinking about System F and simple typed lambda calculus. By function, I mean turing-computable function.
Timothy Zacchari
<pl.programming-languages><type-theory><lambda-calculus><computable-analysis>
Functions that typed lambda calculus cannot compute
Timothy Zacchari
# Functions that typed lambda calculus cannot compute

(Asked by: username_0 on 2012-01-10)

I just want to know some examples of the functions that can be computed by the untyped lambda calculus but not by typed lambda calculi.

As I am a beginner, some reiteration of background information would be appreciated.

Thanks.

Edit: by typed lambda calculi, I was intending to know about System F and the simply-typed lambda calculus. By function, I mean any Turing-computable function.

**Tags:** pl.programming-languages, type-theory, lambda-calculus, computable-analysis
> **Comments:**
> **username_1**: Many typing disciplines exist for $\lambda$-calculi, and the answer to your request depends partly on which choice of typing discipline you have in mind. It also depends on what you mean by function. One example of a difference would be that typing disciplines such as [System F](http://en.wikipedia.org/wiki/System_F) can only type normalising programs, while the untyped $\lambda$-calculus contains non-normalising terms.  
> **username_0**: I was thinking about System F and simple typed lambda calculus. By function, I mean turing-computable function.  

---

## 6 answers

### Answer by username_2 on 2012-01-10. Score: 17

A nice example is given by Godelization: in lambda calculus, the only thing you can do with a function is to apply it. As a result, there is no way to write a closed function of type $(\mathbb{N} \to \mathbb{N}) \to \mathbb{N}$, which takes a function argument and returns a Godel code for it.

Adding this as an axiom to Heyting arithmetic is usually called "the constructive Church thesis", and is a strongly anti-classical axiom. Namely, it is consistent to add it to HA, but not to Peano arithmetic! (Basically, it is a classical fact that every Turing machine halts or not, and there is no computable function that can witness this fact.)

> **Comments:**
> **username_3**: I don't understand how this is consistent with an extensional theory: take f and g extensionally equal, but with different implementations and therefore different godel codes. Does your function return the same number for f and g?  
> **username_2**: It's not consistent with extensionality! However, in HA $\forall$ and $\exists$ are logical connectives, not functions/records. So they have to be realizable but their  realizers don't have to be extensional. Andrej Bauer is an expert on this stuff, so if you ask a question you're sure to get a good answer.  

---

### Answer by username_4 on 2012-01-10. Score: 11

The untyped $\lambda$-calculus posseses general recursion in the form of the $Y$ combinator. Simply-typed $\lambda$-calculus does not. Thus, any function that requires general recursion is a candidate, for example the Ackermann function. (I am skipping some details on how precisely we represent the natural numbers in each system, but essentially any reasonable approach will do.)

Of course, you can always extend the simply-typed $\lambda$-calculus to match the power of $Y$, but then you're changing the rules of the game.

> **Comments:**
> **username_5**: For some reason I'd had it in my head that you could do Ackermann in System F...  
> **username_6**: @Rob, as I understand, Andrej doesn't say that is not the case.  
> **username_4**: I suppose I said that the Ackermann function can be programmed in the untyped $\lambda$-calculus (because every computable function can), but no the simply typed $\lambda$-calculus. I said nothing about System F.  
> **username_5**: Oh, right, I was just being dumb. (Because the question was pretty ambiguous between talking about System F and talking about STLC, I picked the stronger system and forgot about the simpler question.)  
> **username_7**: The Ackermann function in $\lambda$-calculus is $\lambda m.m(\lambda f n.n f(f \underline{1}))~\mathsf{suc}$. According to a type inferencer I built this semester, it has simple type: $(((((f \to e) \to f \to e) \to h) \to ((((f \to e) \to f \to e) \to h)$ $\to h \to g) \to g) \to (((b \to c) \to a \to b) \to (b \to c) \to a \to c) \to d) \to d$, which is atrocious, but possibly correct. The problem with STS isn't Ackermann -- it's, for example, simulating a Turing machine. You simply can't do that without the $Y$ combinator.  
> **username_7**: Hmm. I tried passing $\underline{2}$ as the first argument to the function, and the type inferencer fails. I can pass $\underline{1}$ just fine, though, and I can pass any number for the second argument. So, it's possible to represent the Ackermann function ... it's just not possible to run $\mathsf{ack}~\underline{m}~\underline{n}$ for $m \geq 2$. ...  
> **username_4**: You should either have a builtin type `nat` with primitive recursion, or encode numbers as iterators of type `(o -> o) -> (o -> o)` where `o` is some basic type. So even though your $\lambda$-exprression for Ackermann does the right thing, it cannot be typed in the right way. Of course, in the untyped $\lambda$-calculus types do not impose any limitations and everything works. By the way, you can plug in your program into ocaml and Haskell, too. They will compute the same type.  

---

### Answer by username_5 on 2012-01-10. Score: 11

The simplest answer is given by the fact that typed lambda calculi correspond to logics (simply typed lambda calculus -> predicate logic; system f -> second-order logic) and consistent logics cannot prove their own consistency.

So let's say that you have natural numbers (or a Church encoding of natural numbers) in your typed lambda calculus. It's possible to do a Gödel numbering that assigns every term in System F to a unique natural number. Then, there is a function $f$ that takes any natural number (that corresponds to a well-typed term in System F) to another natural number (that corresponds to the normal form of that well-typed System F term) and does something else for any natural number that doesn't correspond to a well-typed term in System F (say, it returns zero). The function $f$ is computable, so it can be computed by the untyped lambda calculus but not the typed lambda calculus (because the latter would amount to a proof of the consistency of second-order logic *in* second-order logic, which would imply that second-order logic is inconsistent).

Caveat 1: If second-order logic *is* inconsistent, it *might* be possible to write $f$ in System F... and/or it *might* not be possible to write $f$ in the untyped lambda calculus - you could write something, but it might not always terminate, which is a criteria for "computable."

Caveat 2: Sometimes by "simply typed lambda calculus" people mean "simply typed lambda calculus with a fixed-point operator or recursive functions." This would be more-or-less [PCF](http://en.wikipedia.org/wiki/Programming_Computable_Functions), which can compute any computable function, just like the untyped lambda calculus.


---

### Answer by username_8 on 2012-01-11. Score: 6

The simply-typed lambda calculus is actually surprisingly weak. For example, it can't recognize the regular language $\mathtt{a}^\*$. I've never found a precise characterization of the set of languages that STLC can recognize, though.

> **Comments:**
> **username_2**: I think what is computable depends on the types you are looking at. When you represent naturals over the type $(p \to p) \to p \to p$, where $p$ is a base type, and take equality to be beta-equality, the definable functions are the extended polynomials (polynomials + if-then-else). IIRC, Schwichtenberg proved this, though I have never read his original paper (in German). (I think the paper name, translated, is "Definable Functions in Typed Lambda Calculi", 1976.)  
> **username_1**: @ Neel. A slighly better translation would be _Definable Functions in the $\lambda$-calculus with Types_. You can download it [here](http://epub.ub.uni-muenchen.de/4273), it's only two pages long. Is it know what happens at other types, with other notions of equality, or with other encodings of natural numbers?  
> **username_2**: @Marting: Thanks! I'm living in Germany now, so this is a nice extra incentive to practice my German. :)  

---

### Answer by username_9 on 2012-01-11. Score: 4

One vision of the limits of strongly normalizing calculi I like is the computability angle. In a strongly normalizing typed calculus, such as the core simply-typed lambda calculus, System F, or Calculus of Constructions, you have a proof that all terms eventually terminate.

*If* this proof is constructive, you get a fixed algorithm to evaluate all terms with a guaranteed upper-bound on the computation time. Or you can also study the (not-necessarily-constructive) proof and extract an upper-bound from it -- which is likely to be *huge*, because those calculi are expressive.

This bounds gives you "natural" examples of function that cannot be typed in this fixed lambda-calculus : all arithmetic functions that are asymptotically superior to this bound.

If I remember correctly, terms typed in the simply-typed lambda-calculus can be evaluated in towers of exponential : `O(2^(2^(...(2^n)..)`; a function growing faster than all such towers won't be expressible in this calculi. System F corresponds to intuitionistic second-order logic, so the computability power is simply enormous. To seize the computability strength of even more powerful theories, we usually reason in terms of set theory and model theory (eg. what ordinals can be built) instead of computability theory.


---

### Answer by username_10 on 2012-01-20. Score: 0

If I understand your question correctly, I think a simple example is the term $\Delta = \lambda x. x x$, which takes a function and applies it to itself. You can define and reduce this function in the untyped lambda calculus (and in particular, you have $\Delta \Delta \to\_\beta ~\Delta \Delta$, which is not normalizing), but you can't type $\Delta$, because that would mean finding a type $A$ such that $A = A \to A$.

> **Comments:**
> **username_6**: We should be careful about what we mean by typed $\lambda$-calculus. Having a type $A$ s.t. $A\equiv A \to A$ is not strange.  
> **username_10**: Yes, you're right, but I thought (maybe I'm wrong) that it was not possible to have such a type in the simply-typed lambda-calculus or System F, which are both strongly normalizing.  
> **username_11**: I'm not sure if this argument holds: we not only need to show that $\Delta\Delta$ is not typeable, but that there is no typed lambda-term which is equivalent to $\Delta\Delta$. The easiest way to do this is by pointing to the fact that typed lambda calculus is strongly normalizing.  
> **username_12**: @Kaveh Why is having a type `A` such that `A \ident A \rightarrow A` not strange? It sounds absurd to me, what am I overlooking?  
> **username_6**: You are probably thinking classically about sets and function spaces over them. Think e.g. about finite binary strings and computable functions over them.  

---

