What it means lambda calculus is equivalent to turing machine

Question

I'm trying to wrap my head around lambda calculus, and how it relates to language, compiler and binary code. What it actually means that lambda calculus is equivalent to turing machine, and where it actually manifest itself?

I don't understand how lambda calculus could supersede turing machine as a theoretical model of computation. Turing machine is about sequential instructions to mutate the state, lambda calculus is about expressions evaluating to something. It is more abstract, like a programming language of it's own, not the model of how to practically compute something, make things happen. Or let's put it this way: lambda calculus is like the road map, and turing machine like a model of car. How are these two considered equivalent? Would it be possible to run software on hardware without implementing turing machine?

How does for example, a lisp compiler and language relates to lambda calculus? In which layer is the lambda calculus implemented? Is the implementation pure in the terms of definition of lambda calculus? Where and how the theory behind lambda calculus transforms syntax into a running binary? For example, in lambda calculus numbers are encoded as special functions applied to some other function n times. Yet in syntax we use number literals. Where all these axioms are used?

Answer 1

In computability theory, equivalence between two theoretical models of computation means that they can solve the same set of problems. Anything you can compute in a Turing Machine, you can compute using Lambda Calculus, and vice versa.

How do we prove this? It is sufficient to say that if we can model a Turing Machine in lambda calculus, than clearly lambda calculus can compute everything a Turing Machine can. And if we can solve lambda calculus on a Turing Machine, then the reverse holds true as well.

Both of these are possible, and so the models are said to be equivalent.

In practice of course, one model may easily be more practical for certain use cases. Computers today are based on the RAM state model, which in turn lends the basis of it's theory from the idea of a Turing Machine. Lambda calculus is indeed quite abstract, and it doesn't lend it's self as easily to implementation in physical hardware. The two models however both exist in the same computation class, and they can solve the same problems, and are therefor referred to as equivalent.