# To what does typing correspond in a Turing Machine?

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?

• 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. – Martin Berger Jul 8 '13 at 9:01
• 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? – BlueBomber Jul 8 '13 at 13:11
• @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. – 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.)