Beta reduction

We keep pouring from one empty vessel into another, and now it is β-reduction's turn. Reduction, precisely — not conversion, since there can be no expansion here: there is only reduction. In general, the whole operational semantics of the λ-calculus is a single rewriting rule, nothing more.

A function call in any language is a special case of β-reduction.

A term of the form $(\lambda x.\,M)\,N$ is called a redex. Reduction may be applied to any redex anywhere in a term. The notation $\to_\beta$ denotes a single β-reduction step, $\twoheadrightarrow_\beta$ — zero or more steps, and $=_\beta$ — the equivalence generated by reduction. A normal form, or NF, is a term with no redexes: there is nothing left to compute. The result of a program is meant to be exactly a normal form.

If we forbid reduction under a λ — not looking inside the body of an abstraction — we get a weaker notion: weak normal form. In it every redex is burned away except those hidden under a λ. For instance, $\lambda x.\,(\lambda y.\,y)\,z$ is already in weak normal form, even though it has not yet reached the ordinary NF $\lambda x.\,z$. It is to this form (more precisely, the weak head one, WHNF) that real languages evaluate: they do not touch the body of a function until it is called — more on that in the section on reduction strategies.

This is how infinite structures live in Haskell: they are evaluated to weak head form, but not all the way.

nats = [1..]        -- an infinite list 1 : 2 : 3 : …
-- already in WHNF: the outer constructor (:) is known, the tail is an unevaluated thunk;
-- there is no full NF — reaching it would mean building the whole list
take 3 nats         -- [1,2,3]: we take only the beginning, and it all works

Examples of β-reductions:

But, as always, there are subtleties, and the main one is that far from every term reduces to a normal form. Above, in Haskell, I already gave the example of an infinite list, but this is not about that one. The term $\Omega$ reduces to itself — the computation never terminates:

And the fun does not stop there: it can happen that the order in which redexes are evaluated decides whether the algorithm loops or not. In lazy languages this is all over the place, but the compiler usually sorts it out on its own, unless we impose our own will on it. In short, it only gets more interesting from here.