Beta Reduction
Advanced Logic Computation
Here is the entire engine of λ-calculus, and therefore — in a real sense — the entire engine of computing.
The rule
A term of the shape (λx.M) N is called a
redex — a reducible expression. Finding one
and rewriting it is one β-step. Keep going until no
redex remains and you have a normal form: an answer.
Slow motion
Nothing was "computed" in the arithmetic sense — the machine just rewrote symbols, and the answer fell out. Watch it happen live:
Which redex first? Order matters — sort of
Big terms can contain several redexes at once. Two classic strategies:
- Normal order — always reduce the leftmost-outermost redex. Patient, lazy, always finds the answer if one exists.
- Applicative order — reduce arguments first, then apply. Eager; faster when the argument is needed, wasteful when it isn't.
The Church–Rosser theorem guarantees the reassuring part: if two strategies both finish, they agree on the answer. Only whether you finish is at stake.
The trap: capture
Substitution has one subtle failure mode. Watch:
The incoming y was free — it belonged to whoever
wrote the term. Letting it fall under a λy kidnaps it into
a bound variable. The fix is α-renaming: bound
variables are dummies and may be renamed freely —
λy.x and λw.x are the same function — so we
rename before substituting.
λx.f x ≡ f — a function that just forwards
its argument is the function. You won't need it much, but
you'll meet it.
Your turn at the controls
Type any λ-term (use λ or \), or click through a preset:
(λx.λy.x) y reduces to ___ (α-renaming allowed)
A term with no redexes left is in…
Which order reduces the leftmost-outermost redex?
(λx.λy.y) a b → ___
Next: Church numerals · Back: lambda syntax