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 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:

• Girard, Lafont and Taylor, Proofs and Types. Cambridge University Press, 1989, ISBN 0-521-37181-3.

• Is there an always-halting, limited model of computation accepting $R$ but not $RE$?

StackExchange Computer Science Q#13158, answer score: 4