13
$\begingroup$

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.

Improve this question
$\endgroup$
2
  • $\begingroup$ 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 can only type normalising programs, while the untyped $\lambda$-calculus contains non-normalising terms. $\endgroup$
    – Martin Berger
    Jan 10, 2012 at 12:10
  • $\begingroup$ I was thinking about System F and simple typed lambda calculus. By function, I mean turing-computable function. $\endgroup$
    – Timothy Zacchari
    Jan 10, 2012 at 12:31

6 Answers 6

Reset to default
16
$\begingroup$

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

Improve this answer
$\endgroup$
2
  • $\begingroup$ 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? $\endgroup$
    – cody
    Jan 18, 2012 at 19:43
  • 3
    $\begingroup$ 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. $\endgroup$
    – Neel Krishnaswami
    Jan 20, 2012 at 6:17
11
$\begingroup$

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, which can compute any computable function, just like the untyped lambda calculus.

Improve this answer
$\endgroup$
10
$\begingroup$

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.

Improve this answer
$\endgroup$
7
  • $\begingroup$ For some reason I'd had it in my head that you could do Ackermann in System F... $\endgroup$
    – Rob Simmons
    Jan 11, 2012 at 0:08
  • $\begingroup$ @Rob, as I understand, Andrej doesn't say that is not the case. $\endgroup$
    – Kaveh
    Jan 11, 2012 at 1:36
  • 1
    $\begingroup$ 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. $\endgroup$
    – Andrej Bauer
    Jan 11, 2012 at 12:53
  • $\begingroup$ 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.) $\endgroup$
    – Rob Simmons
    Jan 11, 2012 at 15:57
  • $\begingroup$ 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. $\endgroup$
    – Francisco Mota
    Jan 20, 2012 at 1:53
6
$\begingroup$

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.

Improve this answer
$\endgroup$
3
  • 5
    $\begingroup$ 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.) $\endgroup$
    – Neel Krishnaswami
    Jan 11, 2012 at 16:51
  • 2
    $\begingroup$ @ Neel. A slighly better translation would be Definable Functions in the $\lambda$-calculus with Types. You can download it here, 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? $\endgroup$
    – Martin Berger
    Jan 12, 2012 at 13:06
  • $\begingroup$ @Marting: Thanks! I'm living in Germany now, so this is a nice extra incentive to practice my German. :) $\endgroup$
    – Neel Krishnaswami
    Jan 12, 2012 at 15:37
4
$\begingroup$

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.

Improve this answer
$\endgroup$
0
$\begingroup$

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

Improve this answer
$\endgroup$
5
  • $\begingroup$ 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. $\endgroup$
    – Kaveh
    Jan 23, 2012 at 4:59
  • $\begingroup$ 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. $\endgroup$
    – Charles
    Jan 23, 2012 at 10:31
  • $\begingroup$ 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. $\endgroup$
    – lambda.xy.x
    Sep 10, 2015 at 17:46
  • $\begingroup$ @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? $\endgroup$
    – Martijn
    Jan 18, 2017 at 16:34
  • $\begingroup$ You are probably thinking classically about sets and function spaces over them. Think e.g. about finite binary strings and computable functions over them. $\endgroup$
    – Kaveh
    Jan 18, 2017 at 21:50

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.