Evaluation Order and Strategies
A term with several redexes offers several next steps, and β-reduction does not tell us which to take.
A reduction strategy is a policy that resolves the choice — a deterministic function
picking the redex to contract at each step. It might seem a technicality, but the choice is
momentous: on the very same term, one strategy can terminate with an answer while another loops
forever. Every programming language bakes in such a policy — it is the difference between
Haskell's
laziness and ML's strictness — so understanding strategies is understanding what your
language actually does when it runs a program.
Normal order versus applicative order
Two strategies anchor the spectrum. Both scan the term for redexes; they differ in which they
prefer.
-
Normal order contracts the leftmost-outermost redex first — the
one whose \lambda is furthest out and furthest left. Intuitively:
evaluate the function before the argument, passing arguments in unevaluated.
-
Applicative order contracts the leftmost-innermost redex first —
it fully reduces a function's arguments before applying the function. Intuitively:
evaluate arguments first, like almost every mainstream language does at a call site.
The distinction is exactly whether you reduce the operand of an application before or after firing the
outer redex. It sounds symmetric. It is not — as the next card's picture makes vivid.
When the choice decides termination
Consider (\lambda x.\, y)\ \Omega, where
\Omega = (\lambda z.\, z\ z)(\lambda z.\, z\ z) is our non-terminating term.
The outer function \lambda x.\, y ignores its argument. Watch what
each strategy does:
Normal order fires the outer redex immediately: since
x does not occur in the body, \Omega is discarded
unevaluated and we reach the normal form y in one step.
Applicative order insists on reducing the argument
\Omega to a value first — but \Omega never
finishes, so the whole computation diverges though a perfectly good answer sat one step away. Same term,
opposite fates.
Leftmost-outermost is normalising
The example is not a coincidence — normal order is optimal for termination. This is one of the
deepest facts in the subject, the standardisation/normalisation
theorem.
-
If a term M has a β-normal form, then the
leftmost-outermost (normal-order) reduction of M is
guaranteed to reach it.
-
More strongly, every reduction M \twoheadrightarrow_\beta N can be
reordered into a standard reduction that contracts redexes left-to-right; normal order is
the strategy that always follows this standard order.
In words: if any strategy can find the answer, normal order will. Applicative order carries no
such guarantee — it can dive into a doomed subterm and never surface. So why does anyone use applicative
order? Because when a term does normalise under both, applicative order often does less
work: it evaluates each argument once, whereas normal order re-evaluates an argument once per use.
Termination versus efficiency — the classic trade-off, and the seed of call-by-need.
The three practical strategies
Real languages restrict reduction: they never reduce under an unapplied
\lambda (a function body is evaluated only when called), stopping at
weak head normal form. Within that discipline, three strategies dominate.
Call-by-name (CBN) passes arguments unevaluated and substitutes them into the body,
re-evaluating on each use. Its small-step rules — where reduction happens only at the head — are:
\dfrac{}{(\lambda x.\, M)\ N \to M[x := N]} \qquad
\dfrac{M \to M'}{M\ N \to M'\ N}
Call-by-value (CBV) evaluates the argument to a value
V (here, an abstraction) before substituting. It adds an evaluation rule for
the operand and restricts β to values:
\dfrac{}{(\lambda x.\, M)\ V \to M[x := V]} \qquad
\dfrac{M \to M'}{M\ N \to M'\ N} \qquad
\dfrac{N \to N'}{V\ N \to V\ N'}
Call-by-need is CBN made efficient: the argument is still passed unevaluated, but the
first time it is forced its value is memoised (shared via a thunk) so later uses are free. It
has the termination behaviour of CBN and, on the terms both handle, the work profile of CBV — the best
of both, and the semantics of lazy languages like Haskell.
A strategy-parametric reducer
Below, one reducer takes a strategy: "normal" picks the leftmost-outermost
redex, "applicative" reduces operands first. Run it on
(\lambda x.\, y)\,\Omega to see normal order return y while
applicative order exhausts its fuel, and on a shared-work term to see the step counts differ.
type Term =
| { tag: "var"; name: string }
| { tag: "abs"; param: string; body: Term }
| { tag: "app"; fn: Term; arg: Term };
const v = (name: string): Term => ({ tag: "var", name });
const lam = (param: string, body: Term): Term => ({ tag: "abs", param, body });
const app = (fn: Term, arg: Term): Term => ({ tag: "app", fn, arg });
function freeVars(t: Term): Set<string> {
switch (t.tag) {
case "var": return new Set([t.name]);
case "app": return new Set([...freeVars(t.fn), ...freeVars(t.arg)]);
case "abs": { const s = freeVars(t.body); s.delete(t.param); return s; }
}
}
function fresh(b: string, avoid: Set<string>): string { let n = b; while (avoid.has(n)) n += "'"; return n; }
function subst(M: Term, x: string, N: Term): Term {
switch (M.tag) {
case "var": return M.name === x ? N : M;
case "app": return app(subst(M.fn, x, N), subst(M.arg, x, N));
case "abs": {
if (M.param === x) return M;
if (!freeVars(N).has(M.param)) return lam(M.param, subst(M.body, x, N));
const y2 = fresh(M.param, new Set([...freeVars(N), ...freeVars(M.body), x]));
return lam(y2, subst(subst(M.body, M.param, v(y2)), x, N));
}
}
}
const isNF = (t: Term): boolean => step(t, "normal") === null;
// One step under the chosen strategy, or null if normal.
function step(t: Term, strat: "normal" | "applicative"): Term | null {
if (t.tag === "abs") { const b = step(t.body, strat); return b ? lam(t.param, b) : null; }
if (t.tag === "app") {
if (strat === "applicative") {
// reduce operator, then operand, THEN fire the redex (innermost-first)
const f = step(t.fn, strat); if (f) return app(f, t.arg);
const a = step(t.arg, strat); if (a) return app(t.fn, a);
if (t.fn.tag === "abs") return subst(t.fn.body, t.fn.param, t.arg);
return null;
} else {
// normal order: fire the outer redex FIRST (outermost-first)
if (t.fn.tag === "abs") return subst(t.fn.body, t.fn.param, t.arg);
const f = step(t.fn, strat); if (f) return app(f, t.arg);
const a = step(t.arg, strat); if (a) return app(t.fn, a);
return null;
}
}
return null;
}
function show(t: Term): string {
switch (t.tag) {
case "var": return t.name;
case "abs": return `λ${t.param}. ${show(t.body)}`;
case "app": {
const f = t.fn.tag === "abs" ? `(${show(t.fn)})` : show(t.fn);
const a = t.arg.tag === "var" ? show(t.arg) : `(${show(t.arg)})`;
return `${f} ${a}`;
}
}
}
function run(t: Term, strat: "normal" | "applicative", fuel = 100) {
let cur = t, n = 0;
for (; n < fuel; n++) { const nx = step(cur, strat); if (!nx) return { term: cur, steps: n, done: true }; cur = nx; }
return { term: cur, steps: n, done: false };
}
const omega = lam("z", app(v("z"), v("z")));
const OMEGA = app(omega, omega);
const konst = app(lam("x", v("y")), OMEGA); // (λx.y) Ω
const no = run(konst, "normal", 30), ao = run(konst, "applicative", 30);
console.log("normal order :", show(no.term), `done=${no.done} steps=${no.steps}`);
console.log("applicative order :", show(ao.term), `done=${ao.done} steps=${ao.steps}`);
// Shared work: (λx. x x) ((λw. w) a) — both terminate, different step counts.
const dup = app(lam("x", app(v("x"), v("x"))), app(lam("w", v("w")), v("a")));
const nd = run(dup, "normal"), ad = run(dup, "applicative");
console.log("dup normal :", show(nd.term), `steps=${nd.steps}`); // argument reduced twice
console.log("dup applicative :", show(ad.term), `steps=${ad.steps}`); // argument reduced once
Normal order returns y; applicative order dies on \Omega. And on
the duplicating term both reach a a, but applicative order — evaluating the argument once,
up front — beats normal order, which copies the redex and reduces it twice. Call-by-need would match
applicative's count and normal order's termination, by sharing the single evaluation.
Pure laziness — call-by-need — sounds ruinously slow: pass everything unevaluated and you seem doomed to
re-compute. The trick is sharing. A lazy runtime represents an unevaluated argument as
a thunk: a suspended computation with a slot for its result. The first time the thunk is forced
it runs, overwrites itself with the value, and every later use reads the value for free. So an argument
is evaluated at most once — never (if unused, like \Omega above) or
exactly once (if used, however many times). This is why Haskell can define
take 5 [1..] over an infinite list, bind expensive values that may never be
needed, and tie recursive knots that a strict language cannot. Graph reduction — reducing a shared
graph rather than a tree — is the implementation of the call-by-need lambda calculus, and it is
why "lazy" is a performance strategy, not just a semantic one.
It is tempting to file this as "applicative = fast, normal = safe" and move on. Both halves mislead.
Applicative order can be catastrophically slower — infinitely so — because it may evaluate an
argument the function was going to throw away, as with (\lambda x.\, y)\,\Omega.
And normal order is not merely a slow tax: it is the only pure strategy guaranteed to find a
normal form when one exists. The genuine cost of normal order is duplicated work, not
non-termination — and call-by-need pays exactly that cost off by memoisation.
A second trap: do not equate "call-by-value" with "evaluates the whole term to normal form." CBV (and
CBN, and call-by-need) stop at weak head normal form — they never reduce under an
unapplied \lambda. So a program can return a function
\lambda x.\, ((\lambda y.\, y)\, x) with an unreduced redex inside its
body, and that is the correct, finished value at runtime even though it is not the mathematical
β-normal form.