Prove that turing machines and the lambda calculus are equivalent

It is known that a turing machine and the lambda calculus are equivalent in power. I now want to try to prove this myself. I think proving that the lambda calculus is at least as powerful as a turing machine should be relatively easy, by trying to simulate a turing machine in lambda calculus. This should be possible by storing the tape as a list with some encoding, and encoding a transition function as a lambda term.

However, I'm having trouble with proving that a turing machine is at least as powerful as lambda calculus. Any pointers on how to start trying?

• You just need to show how a Turing machine can evaluate $\lambda$-terms. If you already know that, could you try to ask a more specific question so we can work out what part you need help with? – David Richerby Jun 30 '14 at 11:26
• I know how to simulate a turing machine using lambda calculus. I'm not sure, however, how to evaluate lambda -terms with a turing machine. – user19775 Jun 30 '14 at 11:41
• Build a Turing machine that acts as an interpreter for the lambda calculus. You should be able to find lots of resources in books and on the web for how to build an interpreter for the lambda calculus. For instance, see Structure and Interpretation of Computer Programs by Abelson and Sussman. – D.W. Jun 30 '14 at 16:31
• Do you know how to build an interpreter for the lambda-calculus? – D.W. Jun 30 '14 at 20:05
• Start by figuring out whether you know how to build a lambda calculus interpreter, without regard to Turing machines. In other words, see if you can work out an algorithm or pseudocode to do it. If yes, then the only question remaining is how to translate that into a Turing machine. But first figure out which part you are having trouble with: are you having trouble with the first part (how to build an interpreter for the lambda-calculus) or the second part (how to turn the pseudocode for such an interpreter into a Turing machine). – D.W. Jul 1 '14 at 4:25