The Lambda Calculus

A function is a rule: it takes an input and produces an output. In the 1930s, Alonzo Church asked: what if that's all you have? Could you build all of computation from that single idea? He called his answer the lambda calculus, a system built entirely from functions. It turns out that's enough.

Three rules#

Lambda calculus has exactly three kinds of expression.

• A variable: just a name, like $x$, standing for some value not yet specified.
• An abstraction, the lambda calculus word for a function definition: $\lambda x.e$ says "given $x$, produce $e$." The lambda marks where the input goes.
• An application, the word for a function call: two expressions written side by side, the function and then its input.

That is the entire language. Everything you want to compute has to be built from these three rules.

One operation: beta reduction#

Computation happens through a single operation, beta reduction. When you apply a function to an argument, you substitute the argument for the variable everywhere in the body (renaming bound variables where needed so nothing gets captured).

The simplest case is the identity function: $(\lambda x.x)a$ says "given anything, return that thing," and substituting gives back $a$.

Here is a richer case. Every function takes exactly one input, so a function that needs two takes the first and returns a new function that takes the second. Apply $\lambda x.\lambda y.x$ to $a$ and the outer function captures its argument, producing $\lambda y.a$: a function that ignores its own input and always returns the captured value. A constant function, built by substitution.

That is all computation is here. Build a function, apply it, substitute, one step at a time.

Numbers from nothing#

Lambda calculus has no numbers, so you build them from functions. Church's idea: a numeral takes a function $f$ and a starting value $x$, and the number is the repetition, how many times $f$ wraps around $x$.

$$0=\lambda f.\lambda x.x1=\lambda f.\lambda x.fx2=\lambda f.\lambda x.f\left(fx\right)$$

This might feel like a trick. It is, and a remarkably useful one, because now arithmetic is definable. The successor function wraps one more application around a numeral: $\lambda n.\lambda f.\lambda x.f\left(nfx\right)$. Addition chains two numerals together: $\lambda m.\lambda n.\lambda f.\lambda x.mf\left(nfx\right)$, so if one numeral applies $f$ twice and the other three times, the result applies it five times. Multiplication composes: $\lambda m.\lambda n.\lambda f.m\left(nf\right)$, applying $f$ three times, done twice, is six applications.

Run two plus three and every step is a single substitution, ending at $\lambda f.\lambda x.f\left(f\right(f\left(f\right(fx\left)\right)\left)\right)$. Five applications of $f$. Two times three reduces, by composing, to six applications. We built zero, successor, addition, and multiplication from nothing but functions. No numbers were presupposed.

Church numerals are unary: a thousand means a thousand nested applications. There is a more compact encoding that counts in binary, with three constructors: zero, double, and double-plus-one. Five is one-zero-one in binary, so start at zero, double-plus-one to get one, double to get two, double-plus-one to get five. Three layers deep instead of five, and for large numbers the binary encoding is exponentially smaller.

Booleans are choices#

Booleans work the same way. True takes two arguments and picks the first; false takes two and picks the second:

$$\text{true}=\lambda x.\lambda y.x\text{false}=\lambda x.\lambda y.y$$

A boolean doesn't store true or false. It is the act of choosing. An if-then-else is just application: hand the boolean two branches and it chooses. The connectives are single functions; "and" hands the question to the first boolean, so that if it picks true the answer is the second boolean, and if it picks false the answer is false no matter what. Every piece of data, every operation: functions all the way down.

Pause and try: define or and not as lambda terms.

"Or" can hand the question to the first boolean: if $p$ is true the answer is true, and conveniently $p$ itself is true in that branch, so $\text{or}=\lambda p.\lambda q.ppq$. If $p$ picks the first argument it returns $p$ (true); otherwise it returns $q$, which decides.

"Not" swaps the branches: $\text{not}=\lambda p.\lambda x.\lambda y.pyx$. Applied to true, it picks $y$ where true would pick $x$, giving false. Check both on the definitions above by substitution; each takes two or three reduction steps.

Recursion without names#

One thing remains: repetition. How do you write factorial, $n$ times $n-1$ all the way down, when there are no names to call?

Here is the trick: instead of naming your function and calling that name, pass the function to itself as an argument. Write factorial with an extra variable, and wherever it would call itself, call that variable instead. Then hand the function a copy of itself. It receives itself, calls itself through the variable, and the recursion unfolds.

The Y combinator packages this into a single expression:

$$Y=\lambda f.(\lambda x.f(xx\left)\right)(\lambda x.f(xx\left)\right)$$

It takes any almost-recursive function and wires up the self-application automatically, producing a fixed point: calling it is the same as unfolding one more step. Recursion is not a feature you need to add. It emerges from self-application; lambda calculus could compute recursive functions all along.

Two roads to one boundary#

In 1936, the same year Turing published his paper on Turing machines, Church published his own answer to the Entscheidungsproblem using lambda calculus. They arrived at the same conclusion by completely different routes. One model is a mechanical device, tape, head, states, transitions. The other is pure symbolic manipulation, variables, abstraction, substitution. Yet they compute exactly the same class of functions; Turing himself proved it in an appendix to his own paper. Two utterly different formalizations of "what is computable," invented independently, arriving at the same boundary: this is part of what makes the Church-Turing thesis so compelling. Every model agrees; that is the point.

And the boundary is real here too, because not every reduction terminates. Consider omega: apply $\lambda x.xx$ to itself. One beta step gives back the same expression, and the next, and the next. It loops forever. Now consider $\lambda x.xxx$ applied to itself: each step produces one more copy, the term grows every time, and it never stops. Church proved in 1936 that no lambda term can decide whether an arbitrary term will halt. It is the lambda-calculus twin of Turing's halting problem, reached independently and published just before Turing's paper.

The legacy#

Lambda calculus could have remained a curiosity of mathematical logic. It didn't. In 1958, John McCarthy borrowed its notation, and its central idea of functions as values, for Lisp, a language where programs are expressions and computation is evaluation. Every functional language since, ML, Haskell, Scheme, Erlang, Clojure, carries this DNA.

The influence goes deeper. Add types to lambda calculus and the structure of programs mirrors the structure of mathematical proofs. That connection, the Curry-Howard correspondence, gave rise to proof assistants like Coq, Agda, and Lean, where writing verified software and proving theorems are the same activity.

If you remember three things#

1. Three kinds of expression, variables, abstraction, and application, plus one operation, beta reduction, suffice to define all of computation.
2. Data is encoded as behavior: a number is "apply $f$ this many times," a boolean is the act of choosing a branch, and recursion emerges from self-application via the Y combinator.
3. Lambda calculus and Turing machines, invented independently in 1936, compute exactly the same functions and hit the same undecidable boundary, which is why the Church-Turing thesis is about computation itself, not about any one model.