Beta Reduction and the Consequences of Evaluation Order

The lambda calculus has one rewrite rule. A term of the form (λx. M) N is a redex, and it reduces to M[x := N]. Everything the system computes is a sequence of applications of that rule. There is no arithmetic, no branching, no recursion primitive; the rule is the whole engine, and the entire expressive power of the calculus comes from the fact that this one rule can be applied in many places, in many orders, and sometimes not at all.

The freedom is the difficulty. A term can contain several redexes at once, and the choice of which to reduce first can determine whether the term reaches a value, how much work is done on the way, and whether the reduction terminates. This is not a theoretical curiosity; it is the same choice a compiler makes when it decides whether to evaluate an argument before passing it, and the consequences are the ones visible in the semantics of real languages.

The rule, its variants, and what counts as a value

Beta reduction is usually presented alongside two auxiliary rules. The full relation on terms is the compatible closure of these:

(λx. M) N      →β  M[x := N]
λx. M          →α  λy. M[x := y]        (y not free in M)
λx. M x        →η  M                    (x not free in M)

Alpha conversion is the renaming already described; it changes no computation and exists only to keep substitution well defined. Eta conversion is an extensionality principle: a function that immediately applies itself to an argument is the same function as the one that does not bother. Beta reduction is the only rule that does work.

The compatible closure is what lets reduction happen anywhere. If M → M', then M N → M' N, P M → P M', and λx. M → λx. M'. A term is in normal form when it contains no beta redex, and a term has a normal form when some sequence of reductions ends in one. The central fact is that the order of reductions determines whether that sequence exists.

A value is the syntactic category of terms that cannot reduce further under the strategy in use. Under full beta reduction, a normal form that is an application cannot exist: if M N is normal then M is normal, and a normal M in function position would have to be a lambda, which would make M N a redex. So the normal forms of the pure calculus are lambdas whose bodies are normal, plus the open terms built from variables applied to normal arguments. A call-by-value strategy takes a narrower category for its values: a lambda, or a variable. Neither has to be closed, but an application is never a value even when both of its parts are.

Four strategies and their costs

The strategies differ in which redex they pick when several are available. Writing → for one step and ↠ for zero or more:

Normal order. Reduce the leftmost-outermost redex: of all redexes in the term, take the one whose lambda lies furthest left in the left-to-right reading of the syntax tree. Operationally that means the function position of an application is reduced before its argument, and an application is reduced before any redex inside its two parts. This strategy is normalising: if a term has a normal form, normal order reaches it. The cost is duplicated work, because an argument substituted into a body used k times is reduced k times.

Applicative order. Reduce the leftmost-innermost redex, so arguments are reduced before the function is applied. This corresponds to call-by-value when restricted to closed terms. It is not normalising: (λx. λy. y) Ω, where Ω = (λx. x x)(λx. x x), has the normal form λy. y, but applicative order reduces Ω forever and never applies the outer function.

Call-by-name. Do not reduce the argument; substitute it unevaluated, and reduce the body. This is normal order restricted so that reduction never happens inside a lambda body, which is what an interpreter does when it returns a closure instead of normalising.

Call-by-value. Reduce the argument to a value before substituting it. This is applicative order with the additional requirement that the argument be a value, not merely normal. It is the strategy of nearly every mainstream language, because it makes the cost of an argument predictable and gives a clean notion of effect ordering.

The divergence example is the standard discriminator. Ω is the standard term with no normal form: it reduces to itself in one step, since (λx. x x)(λx. x x) → (λx. x x)(λx. x x). Now consider the constant function applied to it:

(λx. y) Ω

Under normal order the head redex is the whole application, so it reduces in one step to y, and the Ω is discarded without ever being touched. Under applicative order the argument Ω is reduced before the function is applied, and the reduction diverges. Same term, same rule, different outcome: one terminates in a single step and the other does not terminate at all.

The reverse case is the reason call-by-value is popular anyway. Under normal order, (λx. p x x) E substitutes the unevaluated E twice, so whatever work E represents happens twice; under call-by-value E is reduced once and the value is substituted. For terms where arguments are used more than once and their evaluation has cost, call-by-value does less work. Plotkin’s 1975 paper formalised both strategies as calculi and showed that they are not equivalent: the same term can converge under one and diverge under the other. Neither is simply better, and the choice is a property of the language rather than of the calculus.

A reduction trace makes the difference concrete

Take the term

(λf. λx. f (f x)) (λy. y) z

which applies the Church numeral two to the identity and then to z. Normal order reduces the outermost redex first, substituting the identity for f:

(λf. λx. f (f x)) (λy. y) z
→ (λx. (λy. y) ((λy. y) x)) z
→ (λy. y) ((λy. y) z)
→ (λy. y) z
→ z

Four steps. Call-by-value takes a different route to the same place: it evaluates the function position (λf. λx. f (f x)) (λy. y) first, since the argument (λy. y) is already a value, then applies the resulting λx. … to z, and finally reduces the two inner applications of the identity. That is also four steps. The strategies diverge in cost, not in result, when the argument is used once and is already a value.

Change the term to use the argument zero times:

(λf. λx. x) Ω z

Normal order: the head redex reduces immediately, f is discarded, and the result is λx. x applied to z, giving z in two steps. Call-by-value: Ω is reduced first and diverges. The strategies are not interchangeable, and this term is the standard witness.

The reverse asymmetry is shown by a term whose argument is cheap but used twice:

(λf. f f) ((λy. y) (λy. y))

Normal order substitutes the unreduced argument and applies it to itself, so the reduction (λy. y)(λy. y) happens twice. Call-by-value evaluates it once and substitutes the value. For a larger argument the difference is a factor of the number of uses, which is why call-by-value with sharing (call-by-need) is the usual compromise: evaluate at most once, on demand.

Strong normalisation and the terms that fail it

A term is strongly normalising if every reduction sequence from it terminates. The simply typed lambda calculus has this property: every well-typed term is strongly normalising, which is the content of the strong normalisation theorem for the simply typed system. The untyped calculus does not. Ω is the standard counterexample, and Y = λf. (λx. f (x x))(λx. f (x x)) is the general-purpose one, since Y f reduces to f (Y f) and hence to an infinite regress for any f that uses its argument.

The distinction has practical weight. In a total language, the type checker can reject non-terminating programs, and the evaluator can use any strategy it likes without risk of divergence. In an untyped or partially typed setting, the strategy is part of the language’s meaning, because it decides which programs produce answers. Languages that claim to be call-by-value and also to have a fixed-point operator are making a choice about which programs diverge, and the choice is observable.

There is also a notion of weak normalisation: every term has a normal form, but some reduction sequences do not reach it. The untyped calculus is not weakly normalising either, but some typed systems are only weakly normalising, and the difference matters for implementations that choose a strategy. Under a normalising strategy, weak normalisation suffices to guarantee that evaluation terminates; under an arbitrary strategy it does not.

Where the redex is not where the work is

The compatible closure hides an important subtlety. Reducing under a binder, λx. M → λx. M', is a legitimate beta step in the pure calculus, but an interpreter that returns a closure never performs it. The body stays unevaluated until the closure is applied, at which point the substitution happens and reduction continues. So the pure calculus’s notion of normal form, which requires the body to be reduced, does not correspond to any value an interpreter produces.

This is why the pure calculus distinguishes full normalisation from weak head normal form. A term is in weak head normal form if the outermost position is not a redex: it is a lambda, or a variable applied to arguments that are not themselves reducible in a way that exposes the head. Interpreters produce weak head normal forms. Proof assistants and anything that prints a result need full normal forms, which requires an additional traversal into the body. The difference in cost is the difference between evaluating a program and evaluating it plus all of the code it would have run if called, and for a recursive definition that difference is the difference between terminating and not.

Implementations of normalisation therefore have to be explicit about which notion they compute. A type checker comparing types needs full normal forms; a runtime applying a function needs weak head normal forms; a compiler doing partial evaluation may need something in between, normalising only the positions it can see. The Church-Rosser theorem establishes that the choice of redex does not change the normal form when one exists, which is what makes any of these strategies sound as implementations of the same calculus. The machines that realise the strategies are described in the CEK and Krivine machines, and the terms that make the difference observable are the ones built from Church encodings.