Skip to content

Instantly share code, notes, and snippets.

@mamonu
Created April 24, 2016 00:44
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save mamonu/47a2d3e37aec1fa693927e47387ad9ca to your computer and use it in GitHub Desktop.
Save mamonu/47a2d3e37aec1fa693927e47387ad9ca to your computer and use it in GitHub Desktop.
What is Lambda Calculus by Robert Harper, Professor of CS at Carnegie Mellon

There are two important models of computation, the lambda calculus and all the others.

The "others" are all "machine models" that differ from one another in uninteresting ways; they are all based on the idea of a program acting on data by modification. So a TM consists of a program (the finite control) acting on the data (the so-called tape).
A RAM consists of a program (machine language) acting on the data (in memory). And so on.
The machine-based models are inherently imperative, and offer no notion of composition of programs from parts.
It's all "first-order"; programs are not data, data does not contain programs.
(Yes, I am aware of encodings, but those are not programs, those are representations of programs as data.)

The lambda calculus is the sole "language model". It is markedly different from machine models because it is based on one of the most important inventions of the human mind, the concept of a variable in mathematics (which is not at all related to the concept of a "variable", a misnomer for "assignables" in imperative programming languages and machine models).

A variable is given meaning by substitution, which captures the concept of composition of a whole from parts.
There is no separation of program from data; the lambda calculus is inherently "higher order".
And it does not rely in any way on modification of storage or data, giving rise to much greater flexibility in programming.
And the lambda calculus is utterly trivial to define, it has variables, functions, and applications, that's it.

The sole virtue of the machine models is their psychological motivation as given by Turing shortly after Church defined computation using the lambda calculus. Turing's formulation makes clear that computation is a faculty of the human mind, and that we externalize it using computers. This view gave rise to the field of Artificial Intelligence, in which Turing was interested from the start. The machine models have no practical uses at all.
There is no such thing as software development using Turing machines, because there cannot be --- there is no notion of composition, so no libraries, no shared code, no reuse, no abstraction, nothing. It's worthless from a practical viewpoint.

The lambda calculus, however, has launched a thousand ships.
It is based on the mathematical concept of a variable, properly so-called, and has given rise to many, many serious programming languages, largely because it inherently supports composition.
It also provides a much richer concept of computation that extends to higher order, and that does not mandate mutation.

In the long run the only model that matters is the lambda calculus. Church got it right from the get-go, before the machine models existed, and it has not changed since (but for one detail that he later dropped, the requirement that all variables introduced actually be used---it is cleaner to think of a term that does not involve a variable x as being vacuously dependent on x, much as a univariate polynomial is "automatically" a multivariate polynomial.)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment