Lambda Calculus
Advanced Logic Computation
Most of mathematics describes things that exist — numbers, shapes, probabilities. The lambda calculus (λ-calculus) describes something different: computation itself. It is a tiny formal system invented by the logician Alonzo Church in the 1930s, and it is famous for a wild claim: with almost nothing in it, it can compute anything any computer can compute.
Everything is a function
Lambda calculus has exactly three kinds of expression:
No numbers. No strings. No if. No loops. No names that
stick around. Just variables, nameless functions, and feeding one to
another — forever.
λx.M reads as "a function that takes x and gives M."
So λx.x is "takes x, gives x" — the function that returns
whatever you hand it. Mathematicians call it the identity
function.
The one rule
Computation in λ-calculus is a single rewrite rule. When a function meets an argument —
That's it. That rule is called β-reduction, and the entire field is what falls out of applying it over and over. Try it:
Why anyone cares
- 1936: Church used λ-definability to prove some questions have no mechanical answer — weeks before Alan Turing reached the same result with his machines. The two definitions turned out to be exactly equivalent.
- Every functional feature since — anonymous
functions, closures,
map— is a descendant of λ. - It's still the best proof that a handful of rules, applied relentlessly, is all a computer is.
The road ahead
- Syntax — how to read λ-terms without drowning in parentheses
- Reduction — the one rule, done slowly and correctly
- Church numerals — numbers conjured from thin air
- Booleans & pairs — true, false, if, and data structures
- Recursion — loops without loops, and the Y combinator
How many kinds of expression does λ-calculus have?
λx.x is…
Reduce: (λx.x) y → ___
The name of the single computation rule is…
Next: lambda syntax · Back: modular arithmetic