I hope my question makes sense: Starting with the premise that the untyped $\lambda $ calculus is equivalent in power to a Turing machine, to what in a Turing machine does adding types to the $\lambda $ calculus correspond? Is there some kind of automaton analog to typing, whether static or dynamic?

  • 3
    $\begingroup$ I recommend that you give up on the simplistic idea that TMs correspond to $\lambda$-calculus. It's misleading. By the Church-Turing thesis you can find encodings between all reasonable computational frameworks. TMs don't correspond any more to $\lambda$-calculus than to Conway's game of life or to semi-Thue systems or to Prolog or .... We can find encodings between all these systems. The encodings have or lack properties (e.g. compositionality), and that may or may not be a good thing in a specific application. $\endgroup$ Jul 8 '13 at 9:01
  • 1
    $\begingroup$ If it is so misleading, then shouldn't people (especially professors) stop emphasizing it? It seems an important--indeed, foundational--result in computer science, so why shouldn't people seek and expect other connections between the two systems? $\endgroup$
    – BlueBomber
    Jul 8 '13 at 13:11
  • $\begingroup$ @BlueBomber, It is important/foundational for historical reasons: these were two of the primary proposed formalizations of computation (along with $\mu$-recursion) at a time when it wasn't known what the "correct" way to formalize computation would be. So, the discovery of the fact that each could simulate the other was a big deal. However, this doesn't necessarily mean that they have a more special connection than do any two other formalizations of computation. $\endgroup$
    – usul
    Jul 8 '13 at 19:26

I can't give you a direct answer for automatons, but for functions on numbers.

The untyped lambda calculus corresponds to $\mu$-recursive functions.

For typed systems, it naturally varies for different systems.

An interesting one is System F, also known as the polymorphic lambda calculus. There is a theorem that says that

A function (on natural numbers) is expressible in System F if and only if it can be proved in the second order Peano arithmetic that the function is total.

This means that in System F you can express basically all imaginable total functions.

There is a bit weaker system, Gödel's System T, for which there is a very similar theorem for first order Peano arithmetic. (However this system is not as nice as System F. In System F you can represent natural numbers, booleans etc. natively, while System T is constructed as the simply typed lambda calculus with externally added naturals and booleans. Also System F has type polymorphism, which makes it much more elegant in many cases.)

See also:


I'm going to say that typing doesn't correspond to anything for Turing Machines. Here's my reasoning: typing doesn't actually have to do with computation, and Turing Machines only model computations.

For the most part, the types of a program don't actually affect how that program runs. Rather, they're tools at compile time which are used for one of two reasons. One is to cause poorly typed programs not to compile. This is a purely compile-time operation, which doesn't affect how the resulting computation is carried out.

The second is to allow multiple functions to have the same name. This isn't really affecting the underlying computation, it's just letting us write programs in a way that's easier to understand.

Types aren't a tool of computation. They can be used for proofs, for understanding programs, for structuring them in ways that are easier to understand, but their presence doesn't change the fundamental way we perform the computation.


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.