54
$\begingroup$

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

Improve this question
$\endgroup$
3

5 Answers 5

Reset to default
35
$\begingroup$

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.

Improve this answer
$\endgroup$
9
  • 3
    $\begingroup$ Church made the claim that lambda calculus captures the intuitive notation of computable function before Turing's paper, that is why it is called Church's Thesis. The idea of capturing the general notion of computable functions goes further back (e.g. Godel's general recursive functions), and Church was trying to capture it. $\endgroup$
    – Kaveh
    Nov 18, 2011 at 0:48
  • 6
    $\begingroup$ I think it's misleading to say that the equivalence of the models is a complete accident. It seems to me that Church and Turing set out to capture related notions, even if it was not immediately obvious that the notions were in fact related. Would you say it's "complete accident" that Riemann integration and anti-differentiation are closely related? $\endgroup$
    – Sasho Nikolov
    Nov 18, 2011 at 1:07
  • 1
    $\begingroup$ @Kaveh: According to Seldin (2006) The logic of Church and Curry, the aims and syntax of the lambda calculus were developed in the period 1928 to 1929, well before Church was aware of the general notion of recursive function. My answer would benefit from a timeline, but I don't have time to assemble that right now. $\endgroup$
    – Charles Stewart
    Nov 23, 2011 at 9:05
  • 1
    $\begingroup$ @Charles: Church was at Göttingen 1927-1928. He was surely aware of what was going on about recursive function theory and Hilbert's program. Ackermann's result about a non-primitive recursive function is from the same year. Church was trying to build a foundation for math. All of this happened before Turing's paper. See this. Kleene proved the equivalence of general recursive functions and $\lambda$-definable function before Turing's work. Your last paragraph is misleading since it gives the feeling that they were $\endgroup$
    – Kaveh
    Nov 23, 2011 at 10:02
  • 1
    $\begingroup$ @Charles, as I wrote I agree that Church's original motivation was to build a foundation (something like Frege's system) (AFAIK), but he also considered it as computation model before Turing's work. I don't think the answer needs to be deleted, revising the second paragraph should make it fine. (the reason I commented is that I feel that in recent times people undervalue Church's work w.r.t. computability.) $\endgroup$
    – Kaveh
    Nov 23, 2011 at 14:32
31
$\begingroup$

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

Improve this answer
$\endgroup$
8
  • 4
    $\begingroup$ We do have $T_EX$ markup now. $\endgroup$
    – András Salamon
    Aug 29, 2010 at 18:51
  • $\begingroup$ Andrej, the Wikipedia article uses different order of parameters that you are using, the second argument is the input and the third is the code of halting computation, the first argument is the code of the machine. I guess you are stating CT, I edited it based on vDT88. $\endgroup$
    – Kaveh
    Nov 18, 2011 at 1:08
  • $\begingroup$ One more thing, it seems that for realizability you give $f$ as a code of TM and expect a $\lambda$-term, but wouldn't it be more natural to give $f$ also as a $\lambda$-term and then the identity function would work? (I can ask it as a separate question if you prefer.) $\endgroup$
    – Kaveh
    Nov 18, 2011 at 1:24
  • $\begingroup$ @Kaveh: I think it was the other way around, but I also wonder why is it not natural to also have an output of the same type as the input in the case of lambda calculus. $\endgroup$
    – Abel Molina
    Nov 18, 2011 at 6:50
  • 2
    $\begingroup$ Would something like a realizer fo the statement "every $f : \mathbb{R} \to \mathbb{R}$ is continuous" do? Or how about a realizer for "the Cantor space $2^\mathbb{N}$ and the Baire space $\mathbb{N}^\mathbb{N}$ are homeomorphic"? $\endgroup$
    – Andrej Bauer
    Nov 19, 2011 at 0:19
14
$\begingroup$

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.

Improve this answer
$\endgroup$
7
$\begingroup$

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.

Improve this answer
$\endgroup$
6
$\begingroup$

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.

Improve this answer
$\endgroup$

Your Answer

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

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