Relationship between Turing Machine and Lambda calculus?

Question

Is there a relationship between the Turing Machine and the Lambda calculus - or did they just happen to arise about the same time?

Answer 1

The lambda calculus is older than Turing's machine model, apparently dating from the period 1928-1929 (Seldin 2006), and was invented to encapsulate the notion of a schematic function that Church needed for a foundational logic he devised. It was not invented to capture the general notion of computable function, and indeed a weaker typed version would have served his purposes better.

It seems to be incidental to the purpose of that the calculus Church invented turned out to be Turing complete, although later Church used the lambda calculus as his foundation for what he called the effectively computable functions (1936), which Turing appealed to in his paper.

Church's simple theory of types (1940) provides a more moderate, typed theory of functions that suffices to express the syntax of higher-order logic but does not express all recursive functions. This theory can be seen as being more in tune with Church's original motivation.

References

• Church (1936). An unsolvable problem in elementary number theory. American Journal of Mathematics 58:345—363.
• Church (1940). A formulation of the simple theory of types. Journal of Symbolic Logic 5(2):56—68.
• Seldin (2006). The logic of Curry and Church. In Handbook of the History of Logic, vol.5: Logic from Russell to Church, p. 819—874. North-Holland: Amsterdam.

Note This answer is substantially revised due to objections by Kaveh and Sasho. I recommend the Wikipedia timeline that Kaveh suggested, History of the Church–Turing thesis, which has some choice quotes from seminal articles.

Answer 2

I would just like to point out that while the lambda calculus and Turing machines both compute the same class of number-theoretic functions, they are not precisely equivalent in every way imaginable. For example, in realizability theory there are statements which can be realized by a Turing machine but not by lambda calculus. One such statement is the formal Church's thesis, which states:

$$\forall f : \mathbf{nat} \to \mathbf{nat} \ \exists e \ \forall n \ \exists k \ \big( \mathbf{T}(e, n, k) \land \mathbf{U}(k,f(n)) \big)$$

Here $\mathbf{T}$ is Kleene's T predicate. A realizer for this statement would be a program $c$ that accepts a (representation of) map $f$ and outputs (a representation of) $e$ with the desired property. In the Turing machine model the map $f$ is represented by the code of a Turing machine that computes $f$, so the program $c$ is just (the code of a Turing machine computing) the identity function. However, if we use the lambda calculus, then $c$ is supposed to compute a numeral representing a Turing machine out of a lambda term representing a function $f$. This cannot be done (I can explain why, if you ask it as a separate question).

Answer 3

They are related both mathematically and historically.

The lambda calculus was developed in 1928 - 1929 by Alonzo Church (published in 1932).

The Turing machine was developed in 1935 - 1937 by Alan Turing (published in 1937).

Alan Turing was Alonzo Church's Ph.D. student at Princeton from 1936 - 1938.

Turing machines and the lambda calculus are equivalent in computational power: each can efficiently simulate the other.

Answer 4

Entscheidungsproblem is one of the famous 23 problems proposed by mathematician David Hilbert.

In 1936 and 1937 Alonzo Church and Alan Turing respectively, published independent papers showing that it is impossible to decide algorithmically whether statements in arithmetic are true or false, and thus a general solution to the Entscheidungsproblem is impossible.

This was done by Alonzo Church in 1936 with the concept of "effective calculability" based on his λ calculus and by Alan Turing in the same year with his concept of Turing machines. It was later recognized that these are equivalent models of computation. - Wikipedia

So lambda calculus and Turing machines not just closely related but they are equivalent models of computation.

You may also like tor read The Annotated Turing: A Guided Tour Through Alan Turing's Historic Paper on Computability and the Turing Machine by Charles Petzold. This book captures ome interesting information about the topic.

Answer 5

Turing machines and Lambda Calculus are two models that capture the notion of algorithm (mechanical computation). Lambda calculus was invented by Church to perform computations with functions. It is the basis of functional programming languages. Basically, every problem that is computable (decidable) by Turing machines is also computable using Lambda calculus. So, they are two equivalent models of computation (up to polynomial factors) and both try to capture the power of any mechanical computation.