Based on the Church Turing Thesis, we conjecture that Turing Machines are the "correct," model of computation. It is well known that they are equivalent to the Lambda Calculus, another model of computation. Based on Why do we believe the Church-Turing Thesis? and other questions on this site, it seems clear that the equivalence between TMs and LC is well known. However, I have not been able to find an answer better than "Show LC is equivalent to the \mu-recursive functions." I'm looking for a proof of this equivalence. A more in depth sketch than "Use \mu-recursive functions," or a link to a paper/article would be appreciated. Thanks.
Add a comment |
1 Answer
$\begingroup$ $\endgroup$
I don't know whether this answer is satisfactory for you, but in the book by Odifreddi Classical Recursion Theory, it is proven (Thm. 1.7.12) that for a function $f: \mathbb{N}^k \to \mathbb{N}$ is equivalent to be:
- Turing-computable;
- recursive;
- $\lambda$-definable.
A function $f: \mathbb{N}^k \to \mathbb{N}$ is $\lambda$-definable if there is a $\lambda$-term $F$ such that $$f(x_1, \ldots, x_k) = x \iff F \bar{x}_1 \cdots \bar{x}_k \twoheadrightarrow_\beta \bar{x}$$ where $\bar{n}$ is the Church's numeral $\lambda fx.f\cdots(fx)$ for the number $n$.
It is easier to prove 1. $\iff$ 2. $\iff$ 3. rather than $1. \iff$ 3.
The proof of 2. $\implies$ 3. is mainly due to Church ("A set of postulates for the foundation of logic", 1933), and relies on the encoding of initial functions, iteration, composition, etc. in $\lambda$-calculus. To the direction 3. $\implies$ 2. contributed Church and Kleene ("Lambda-definability and recursiveness", 1936).
