Turing Machines and Lambda Calculus equivalence

Question

I am wondering can anyone explain to me in general terms, some proofs of the equivalence of Lambda calculus and turing machines and the general method of the proof. In as plain terms as possible.

Answer 1

In very basic terms, you just prove two things:

1. For any lambda term, there is a Turing machine which computes the same thing
2. For any Turing machine, there is a lambda term which computes the same thing

Of course there's some handwaving involved here, since you also need to account for operational differences in input/output, but we're not getting into that here.

In practice, the above two theorems are proven constructively, that is, by actually giving a mechanical way of turning one into the other. So basically you are giving two compilers, along with a proof of their correctness.

To get a good intuition, think of the analogous theorem of equivalence between the lambda calculus and register machines. In that setting, handwaving away the finiteness of a real computer, an interpreter for the untyped lambda calculus is the proof for one direction. And here I mean a real, tangible program that you can run; e.g. by removing the typechecker from the compiler of a functional programming language (which is bound to have some typed version of the lambda calculus embedded in it.

So next time you run GHC, think of this theorem!

Answer 2

I believe that Gate logic(Hardware), Lambda Calculus(Math/Abstraction) and Turing Machines(abstract Images) are the same operation from a different perspective. Gate Logic are the bits/current that get shifted. You can implement it yourself by hand (experiment kits, breadboard, hardware) or use a logic gate simulator(software) to test it. Lambda Calculus is a formal and mathematical concept to prove that the operation that you do mechanically, will always have the same output/result. Turing Machines are just a more abstract way to explain this, without Math nor Gates. Telling your grandma the Von-Neumann Architecture, leaving Math, electrical and software engineering in the lab. In gate logic, you will create a latch that will hold a bit/state depending on inputs. In lambda calculus, each bit is a symbol and the lambda itself is the symbol for transition/reduction. In Turing machines, the bits are the registers. I have learned this with Principia Mathematica, Tractatus-Logico Philosophicus and the Lambda Calculus: The shortest explanations are the worst because most abstract. You will need time to look at the trees for them to become a forest.