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

<p>$$\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)$$</p>

<p>Here $\mathbf{T}$ is <a href="http://en.wikipedia.org/wiki/Kleene%27s_T_predicate">Kleene's T predicate</a>. 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).</p>

CC BY-SA 3.0
2011-11-18T01:08:04.647Z
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.
Kaveh
CC BY-SA 3.0
2011-11-18T01:24:43.750Z
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.)
Kaveh
CC BY-SA 3.0
2011-11-18T06:50:23.660Z
@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.
Abel Molina
CC BY-SA 3.0
2011-11-18T07:13:13.133Z
You are right, it is the other way around: "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."
Kaveh
CC BY-SA 3.0
2011-11-18T09:47:27.497Z
@Abel: If I understand you correctly, then what you're suggesting becomes a truism in the realizability model: every function that is realized is realized. For an interesting observation, you should have a statement whose realizers convert realizers for functions to some other representation (such as to codes of Turing machines).
Andrej Bauer
CC BY-SA 3.0
2011-11-18T21:04:51.943Z
@Andrej. Very true. But the statement in the Turing Machine model seems kind of like a truism as well. Is it possible to obtain an interesting statement in the Turing Machine model? (i.e. a statement in which c is computing between two different kind of representations).
Abel Molina
CC BY-SA 3.0
2011-11-19T00:19:45.823Z
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"?
Andrej Bauer
CC BY-SA 2.5
2010-08-29T18:51:48.040Z
We do have $T_EX$ markup now.
András Salamon
CC BY-SA 3.0
2010-08-28T21:11:28.483Z
2011-11-18T01:16:47.263Z
2011-11-18T01:16:47.263Z
Andrej Bauer
<p>They are related both mathematically and historically.</p>

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

<p>The Turing machine was developed in 1935 - 1937 by Alan Turing (published in 1937).</p>

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

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

CC BY-SA 2.5
2010-08-28T23:11:34.000Z
2010-08-28T23:11:34.000Z
Matt Might
<p>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.</p>

CC BY-SA 2.5
2010-08-26T12:14:07.297Z
2010-08-26T12:14:07.297Z
Mohammad Al-Turkistany
<p><a href="http://en.wikipedia.org/wiki/Entscheidungsproblem">Entscheidungsproblem</a> is one of the famous 23 problems proposed by mathematician David Hilbert.</p>

<blockquote>
  <p>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.</p>
  
  <p>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</p>
</blockquote>

<p>So <strong>lambda calculus and Turing machines</strong> not just closely related but they are <strong>equivalent models of computation</strong>. </p>

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

CC BY-SA 2.5
2010-08-26T13:06:59.980Z
2010-08-26T13:06:59.980Z
Pratik Deoghare
<p>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.</p>

<p>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 <em>effectively computable</em> functions (1936), which Turing appealed to in his paper.</p>

<p>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.</p>

<h3>References</h3>

<ul>
<li>Church (1936).  An unsolvable problem in elementary number theory.  <em>American Journal of Mathematics</em> 58:345—363. </li>
<li>Church (1940).  <a href="http://www.classes.cs.uchicago.edu/archive/2007/spring/32001-1/papers/church-1940.pdf">A formulation of the simple theory of types</a>.  <em>Journal of Symbolic Logic</em> 5(2):56—68. </li>
<li>Seldin (2006). <a href="http://people.uleth.ca/~jonathan.seldin/CCL.pdf">The logic of Curry and Church</a>.  In <em>Handbook of the History of Logic, vol.5: Logic from Russell to Church</em>, p. 819&mdash;874.  North-Holland: Amsterdam.</li>
</ul>

<p><strong>Note</strong> This answer is substantially revised due to objections by Kaveh and Sasho.  I recommend the Wikipedia timeline that Kaveh suggested, <a href="http://en.wikipedia.org/wiki/History_of_the_Church%E2%80%93Turing_thesis">History of the Church–Turing thesis</a>, which has some choice quotes from seminal articles.</p>

CC BY-SA 3.0
2011-11-18T00:48:53.197Z
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.
Kaveh
CC BY-SA 3.0
2011-11-18T01:07:17.877Z
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?
Sasho Nikolov
CC BY-SA 3.0
2011-11-23T09:05:02.537Z
@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.
Charles Stewart
CC BY-SA 3.0
2011-11-23T09:08:07.290Z
@Sasha: I mean accident in the sense of being unintended.  When Riemann did his work on grounding integration, he was well aware of the relationship between integration and differentiation.
Charles Stewart
CC BY-SA 3.0
2011-11-23T10:02:13.853Z
@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](http://en.wikipedia.org/wiki/History_of_the_Church%E2%80%93Turing_thesis). 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
Kaveh
CC BY-SA 3.0
2011-11-23T10:12:40.570Z
not considering $\lambda$-calculus as a model capturing the notion of computability before Turing's paper, that is not the case.
Kaveh
CC BY-SA 3.0
2011-11-23T10:40:56.960Z
@Charles, we can also ask it on MO or FOM.
Kaveh
CC BY-SA 3.0
2011-11-23T14:32:58.133Z
@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.)
Kaveh
CC BY-SA 3.0
2016-11-13T21:20:43.153Z
It's amusing, if nothing else, to note Church's 1932 comment of the lambda calculus: "There may, indeed, be other applications of the system than its use as a logic."
OJFord
CC BY-SA 3.0
2010-08-26T13:24:59.047Z
2011-11-24T21:28:29.747Z
2011-11-24T21:28:29.747Z
Charles Stewart
<p>Is there a relationship between the Turing Machine and the Lambda calculus - or did they just happen to arise about the same time?</p>

CC BY-SA 3.0
2011-11-18T19:01:37.827Z
related: [Realizability theory: difference in power between Lambda calculus and Turing Machines](http://cstheory.stackexchange.com/questions/1117/realizability-theory-difference-in-power-between-lambda-calculus-and-turing-mac)
Kaveh
CC BY-SA 3.0
2017-07-04T15:37:26.737Z
This is a nice question!
Tayfun Pay
CC BY-SA 2.5
2010-08-26T12:15:58.513Z
Can you elaborate your question? Both models have the same computational power (both are able the express the family of recursive functions), that is, they're Turing complete. See: http://en.wikipedia.org/wiki/Turing_completeness
Joel Rybicki
<computability><lambda-calculus><turing-machines>
Relationship between Turing Machine and Lambda calculus?
hawkeye
# Relationship between Turing Machine and Lambda calculus?

(Asked by: username_0 on 2010-08-26)

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

**Tags:** computability, lambda-calculus, turing-machines
> **Comments:**
> **username_3**: Can you elaborate your question? Both models have the same computational power (both are able the express the family of recursive functions), that is, they're Turing complete. See: http://en.wikipedia.org/wiki/Turing_completeness  
> **username_1**: related: [Realizability theory: difference in power between Lambda calculus and Turing Machines](http://cstheory.stackexchange.com/questions/1117/realizability-theory-difference-in-power-between-lambda-calculus-and-turing-mac)  
> **username_2**: This is a nice question!  

---

## 5 answers

### Answer by username_10 on 2010-08-26. Score: 35 | Accepted answer

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](http://www.classes.cs.uchicago.edu/archive/2007/spring/32001-1/papers/church-1940.pdf). *Journal of Symbolic Logic* 5(2):56—68.
* Seldin (2006). [The logic of Curry and Church](http://people.uleth.ca/~jonathan.seldin/CCL.pdf). 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](http://en.wikipedia.org/wiki/History_of_the_Church%E2%80%93Turing_thesis), which has some choice quotes from seminal articles.

> **Comments:**
> **username_1**: 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.  
> **username_11**: 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?  
> **username_10**: @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.  
> **username_10**: @Sasha: I mean accident in the sense of being unintended.  When Riemann did his work on grounding integration, he was well aware of the relationship between integration and differentiation.  
> **username_1**: @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](http://en.wikipedia.org/wiki/History_of_the_Church%E2%80%93Turing_thesis). 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  
> **username_1**: not considering $\lambda$-calculus as a model capturing the notion of computability before Turing's paper, that is not the case.  
> **username_1**: @Charles, we can also ask it on MO or FOM.  
> **username_1**: @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.)  
> **username_12**: It's amusing, if nothing else, to note Church's 1932 comment of the lambda calculus: "There may, indeed, be other applications of the system than its use as a logic."  

---

### Answer by username_4 on 2010-08-28. Score: 31

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](http://en.wikipedia.org/wiki/Kleene%27s_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).

> **Comments:**
> **username_6**: We do have $T_EX$ markup now.  
> **username_1**: 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.  
> **username_1**: 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.)  
> **username_5**: @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.  
> **username_1**: You are right, it is the other way around: "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."  
> **username_4**: @Abel: If I understand you correctly, then what you're suggesting becomes a truism in the realizability model: every function that is realized is realized. For an interesting observation, you should have a statement whose realizers convert realizers for functions to some other representation (such as to codes of Turing machines).  
> **username_5**: @Andrej. Very true. But the statement in the Turing Machine model seems kind of like a truism as well. Is it possible to obtain an interesting statement in the Turing Machine model? (i.e. a statement in which c is computing between two different kind of representations).  
> **username_4**: 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"?  

---

### Answer by username_7 on 2010-08-28. Score: 14

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 by username_9 on 2010-08-26. Score: 7

[Entscheidungsproblem](http://en.wikipedia.org/wiki/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 by username_8 on 2010-08-26. Score: 6

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.


---

