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?

Sadowski

en.wikipedia.org/wiki/Church-Turing_thesis is a good starting point. – Reconnoitre

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.

Bursary

Answer 2

All these foundational languages have been introduced in a era preceding the advent of computers. The whole point of the research consisted in charcterizing a class of (numerical) functions that looked "intuitively" computable, in algorithmic sense, and not necessarily by an automatic device. Now, it turns out that lambda calculus and Turing machines, as well as many others computational models like combinatory logic, Post systems, generalized recursive functions, and so on, precisely express the same class of computable functions. This motivated Church's thesis.

I agree with you that Turing machines (like random access machines) have a more architectural flavour with respect to other models. In fact, this is what convinced Goedel, who was at first a bit skeptical, of the validity of Church's thesis.

I also agree with you that lambda calculus cannot supersede Turing machines as a theoretical model of computation: there is nothing evident to gain in such an operation.

At the same time, lambda calculus is fun, while turing machines are deadly boring. It is fun, precisely because it is at the extreme opposite of Turing Machines. I think one could reasonably argue that it is the highest level model of computation that has been ever conceived (and probably that will ever be). This is why it is a challenging and instructive language for every programmer.

Gertudegerty