Lambda Calculus

Three rules. No numbers, no loops, no memory. And yet every computation that can be performed at all.

In 1936, two men with very different temperaments answered the same question in two utterly different ways. Alan Turing imagined an infinite tape and a little machine crawling over it, reading and writing symbols. Alonzo Church, his doctoral supervisor at Princeton, wrote down something stranger: a notation with no machines, no memory, no tape. Just functions. Functions making functions. Functions feeding functions to functions. He called it the lambda calculus.

It looks like a child's toy and turns out to be one of the deepest pieces of mathematics of the twentieth century. Every functional programming language in use today — Haskell, OCaml, Lisp, even the bits of JavaScript you used last Tuesday — is, under a thin layer of syntax, a dialect of it. The word “lambda” you may have typed in Python is named after Church's λ. And, most surprisingly, his system and Turing's turned out to compute exactly the same things.

The smallest language anyone has invented

How much grammar do you need to describe every computation in the universe? Church's answer was: three rules.

There are exactly three kinds of expression in the pure lambda calculus.

A variable is a name: x, y, z.

An abstraction is what programmers would call an anonymous function. You write it with a λ, the bound variable, a dot, and the body. So λx. x is “the function that takes an argument and returns it” — the identity. λx. λy. x takes two arguments and returns the first. That's it. No return, no braces, no types.

An application is the act of handing an argument to a function. You just write them side by side: (λx. x) y. This means “apply the identity to y.”

And one rewriting rule, called beta reduction: when an abstraction meets an argument, substitute the argument into the body. So (λx. x) y becomes y. That is the entire calculation step. That is the entire calculator.

That picture, in a precise sense, is what computers do. They reduce expressions. The chip in front of you is, philosophically, doing nothing but very fast beta reduction on a vast and well-organised expression.

Encoding the universe

A skeptical reader will object: this is fine for toy substitutions, but the world is made of numbers and lists and booleans and loops. The lambda calculus has none of those. Where do they come from?

Church's audacious answer was: build them out of functions.

Take the number 3. Church represented it as “a function that, given another function and a starting value, applies the function three times.” In symbols: λf. λx. f (f (f x)). The number 2 is λf. λx. f (f x). Zero is λf. λx. x — apply nothing. These are Church numerals. They are not numbers in any sense your calculator would recognise; they are little programs that act like the number they encode.

Addition? Adding two Church numerals is itself just a lambda expression that takes two such repeat-functions and stitches them together. Multiplication too. So is the predecessor function — a surprisingly intricate construction by Stephen Kleene, dreamed up, the story goes, in a dentist's chair.

True and false are just two-argument functions: λa. λb. a returns the first thing, λa. λb. b returns the second. From those, if-then-else is trivial: it is just applying the boolean to the two branches. Pairs are functions of one argument that take a picker. Lists are chains of pairs. Recursion is achieved by an expression of breathtaking strangeness called the Y combinator — a function that, when applied to a function, returns the fixed point that lets a definition refer to itself, all without ever giving anything a name.

There are no numbers, no truths, no choices — only functions. And yet everything that can be computed, can be computed here.

You can encode the whole of arithmetic, logic, data structures and control flow with nothing but variables, abstractions, and the act of substitution. It feels like a magic trick. It is not. It is what mathematicians mean when they call something expressive.

The same machine, in disguise

Within a year of Church publishing his calculus, Turing had finished his paper on the machine that bears his name. The two systems looked nothing alike. Church's was algebraic, almost calligraphic. Turing's was mechanical, with a head crawling along a tape. One looked like pure thought; the other like an unbuilt factory.

Then Turing proved they were equivalent. Any function computable by a Turing machine is expressible as a lambda term, and the other way around. The proof is a delight: he shows how to encode the state-and-tape of a Turing machine as a lambda expression, and how to encode a lambda term as a sequence of moves on a tape. Two completely independent attempts to formalise “computation” had arrived at the same shore from opposite directions.

That convergence is what gave Church and Turing the nerve to propose what is now called the Church–Turing thesis: any function that can be effectively computed at all can be computed by either system. The fact that two such different formalisms collapsed into one is the strongest evidence anyone has ever produced for that thesis. It is the ground every other claim in computer science stands on.

Why a 1936 sketch still runs your code

Lambda calculus's particular gift is that it stayed close to the surface of programming. When John McCarthy designed Lisp in 1958, he reached straight into Church's notation; Lisp's lambda keyword is the original article. Decades later, when Robin Milner designed ML, then again when Simon Peyton Jones and others helped build Haskell, the calculus was right there, barely concealed. The reason functional languages can express so much in so little — map, filter, fold, first-class functions, closures — is that they are already most of the way to being pure lambdas.

It also gave us the modern theory of types. When Bertrand Russell's paradox forced Church to add typing rules to keep his calculus consistent, he stumbled into a system that mathematicians now recognise as the same thing as constructive logic — an extraordinary correspondence known as Curry–Howard, in which every program is a proof and every proof is a program. The whole field of type theory, and a good fraction of the proof assistants used to verify modern software, descend from that single move.

So a thread runs from a Princeton blackboard in 1936, through Lisp in 1958, through ML and Haskell, to the “lambda” you typed in Python last week. The same three rules. The same act of substitution. A whole edifice of computer science rests on a notation so small you can fit it on a postcard — and that, perhaps, is the point. The simplest things, taken seriously enough, end up holding the most weight.