Evaluation Contexts
Look back at the small-step
rules and you will notice something a little wasteful. For every operator we wrote a
computation rule (the interesting one that actually fires) and one or two
congruence rules whose only job is to say "the redex is further inside — go step there". Those
congruence rules are pure bureaucracy: E-Add-L, E-Add-R, E-Mul-L, E-Mul-R, E-If … all repeating the same
idea. As a language grows, the congruence rules multiply and the real content — the handful of
reductions that do work — gets buried.
Evaluation contexts, due to Matthias Felleisen and Robert Hieb, cut cleanly through
this. The trick is to separate two concerns that the congruence rules had tangled together:
- Where to reduce next — captured once and for all by a grammar of contexts
with a single hole [\cdot]; and
- What the reduction does — a small set of primitive notions of reduction,
each firing an operator on values.
Snap the two back together with one rule, and the whole search apparatus of congruence rules
collapses into a single line. Better still, the context grammar becomes an explicit, readable
specification of the evaluation strategy.
The hole and the context grammar
An evaluation context E is a term with exactly one sub-term
replaced by a hole, written [\cdot]. Writing
E[e] means "plug the term e into the hole of
E". For our arithmetic-and-boolean language, the grammar of evaluation
contexts is:
E \;::=\; [\cdot] \;\mid\; E + e \;\mid\; v + E \;\mid\; E \times e \;\mid\; v \times E \;\mid\; \mathsf{if}\ E\ \mathsf{then}\ e\ \mathsf{else}\ e
Read this grammar as a set of instructions for finding the hole. The clause
E + e says "you may look inside the left operand of a sum"; the clause
v + E says "you may look inside the right operand — but only
once the left operand is already a value v". That single
value-restriction is the entire evaluation strategy in disguise: it forces left-to-right,
call-by-value order, exactly as the congruence rules did — but now stated once. Notice
also there is no clause letting the hole descend into the branches of an
\mathsf{if}: you may evaluate the guard, never a branch.
Notions of reduction, and the one rule that remains
Separately, we list the primitive reductions — the "real work", written with a plain
arrow \rightsquigarrow (a notion of reduction). Each fires an operator
whose operands are values:
n_1 + n_2 \;\rightsquigarrow\; n_3\ (n_3 = n_1{+}n_2)\qquad n_1 \times n_2 \;\rightsquigarrow\; n_3\ (n_3 = n_1{\cdot}n_2)
\mathsf{if}\ \mathsf{true}\ \mathsf{then}\ e_2\ \mathsf{else}\ e_3 \;\rightsquigarrow\; e_2 \qquad \mathsf{if}\ \mathsf{false}\ \mathsf{then}\ e_2\ \mathsf{else}\ e_3 \;\rightsquigarrow\; e_3
A term matching the left of some \rightsquigarrow is a redex.
Now the entire small-step relation is one rule — the context rule — that lifts a
primitive reduction to wherever the context says the hole is:
\dfrac{\,r \;\rightsquigarrow\; r'\,}{\,E[r] \;\longrightarrow\; E[r']\,}\qquad\text{\small (context rule)}
That is the whole dynamics. Every congruence rule we ever wrote is now a consequence of this
one rule plus the context grammar: to step e_1 + e_2 with
e_1 not a value, you decompose it as E[r] for
E = ([\cdot] + e_2) nested around the redex, fire
r \rightsquigarrow r', and plug back. The bureaucracy became a lemma.
Every step: a context and a redex
Watch what happens when we reduce (1+2)\times(3+4) the context way. At each
step we decompose the term into an evaluation context E (the spine
down to the hole) and the redex r sitting in that hole, fire
r \rightsquigarrow r', and plug r' back.
Read each row as E[r]: the boxed piece is the redex
r, and everything around it — the part shown with the hole
[\cdot] — is the context E. In the first row the
left operand 1+2 is not yet a value, so the grammar's
E+e clause sends the hole left; once it becomes the value
3, the v \times E clause lets the hole move right.
The strategy is not "decided by the rule engine" — it is read straight off the context grammar.
Unique decomposition — the property that makes it work
- Every closed term e is either a value, or can be
written as E[r] for a unique evaluation context
E and redex r (or is stuck: a non-value with no
such decomposition).
- Because the decomposition is unique, at most one primitive reduction can fire — so
\longrightarrow is deterministic, for free.
This is the payoff. In the rule-by-rule presentation, determinism was a theorem you proved by wrangling
overlapping rules. Here it falls out of a grammatical fact: the context grammar is unambiguous
about where the hole must go, so there is exactly one redex a term can offer next. Change the grammar and
you change the strategy — and, as long as the new grammar still decomposes uniquely, you get a new
deterministic semantics with no other edits.
Contexts in code: decompose, contract, plug
The context machinery is beautifully direct to implement. decompose walks the term
following the context grammar until it finds the redex, recording how to plug a result back;
contract is the notion of reduction \rightsquigarrow; and one
step is plug the contractum back into the same context. The driver prints the context
E (with its hole) and the redex r at every step.
type Term =
| { tag: "num"; n: number }
| { tag: "bool"; b: boolean }
| { tag: "add"; l: Term; r: Term }
| { tag: "mul"; l: Term; r: Term }
| { tag: "if"; c: Term; t: Term; e: Term };
const isValue = (e: Term) => e.tag === "num" || e.tag === "bool";
// A redex matches the left of some ↝ (operands are values of the right kind).
function isRedex(e: Term): boolean {
if (e.tag === "add" || e.tag === "mul") return e.l.tag === "num" && e.r.tag === "num";
if (e.tag === "if") return e.c.tag === "bool";
return false;
}
// The notion of reduction ↝ , applied to a redex.
function contract(e: any): Term {
if (e.tag === "add") return { tag: "num", n: e.l.n + e.r.n };
if (e.tag === "mul") return { tag: "num", n: e.l.n * e.r.n };
return e.c.b ? e.t : e.e; // if-true / if-false
}
function show(e: Term): string {
switch (e.tag) {
case "num": return String(e.n);
case "bool": return String(e.b);
case "add": return `(${show(e.l)} + ${show(e.r)})`;
case "mul": return `(${show(e.l)} * ${show(e.r)})`;
case "if": return `if ${show(e.c)} then ${show(e.t)} else ${show(e.e)}`;
}
}
type Decomp =
| { kind: "value" }
| { kind: "stuck" }
| { kind: "redex"; ctx: string; redex: Term; plug: (t: Term) => Term };
// Decompose e uniquely into E[redex], per the evaluation-context grammar.
function decompose(e: Term): Decomp {
if (isValue(e)) return { kind: "value" };
if (isRedex(e)) return { kind: "redex", ctx: "[.]", redex: e, plug: (t) => t };
if (e.tag === "add" || e.tag === "mul") {
const op = e.tag === "add" ? "+" : "*";
if (!isValue(e.l)) { // grammar: E op e
const d = decompose(e.l);
if (d.kind !== "redex") return { kind: "stuck" };
return { kind: "redex", redex: d.redex,
ctx: `(${d.ctx} ${op} ${show(e.r)})`,
plug: (t) => ({ ...e, l: d.plug(t) }) };
}
const d = decompose(e.r); // grammar: v op E
if (d.kind !== "redex") return { kind: "stuck" };
return { kind: "redex", redex: d.redex,
ctx: `(${show(e.l)} ${op} ${d.ctx})`,
plug: (t) => ({ ...e, r: d.plug(t) }) };
}
// if: the hole may only enter the guard
const d = decompose(e.c);
if (d.kind !== "redex") return { kind: "stuck" };
return { kind: "redex", redex: d.redex,
ctx: `if ${d.ctx} then ${show(e.t)} else ${show(e.e)}`,
plug: (t) => ({ ...e, c: d.plug(t) }) };
}
function run(e: Term): void {
let cur = e;
for (;;) {
const d = decompose(cur);
if (d.kind === "value") { console.log(`= ${show(cur)} (value)`); break; }
if (d.kind === "stuck") { console.log(`${show(cur)} (STUCK)`); break; }
console.log(`${show(cur)} = E[ ${show(d.redex)} ] with E = ${d.ctx}`);
cur = d.plug(contract(d.redex));
}
}
const num = (n: number): Term => ({ tag: "num", n });
// (1 + 2) * (3 + 4)
run({ tag: "mul", l: { tag: "add", l: num(1), r: num(2) }, r: { tag: "add", l: num(3), r: num(4) } });
The output narrates the strategy: E = ([.] * (3 + 4)) while the left operand is still being
reduced, then E = (3 * [.]) once it is a value, then E = [.] for the final
top-level multiply. The redex column is always the primitive reduction; the context
column is always the unique place the grammar put the hole.
Because the strategy lives entirely in the context grammar, you can change how a language evaluates by
editing that grammar and nothing else. Want right-to-left evaluation? Swap the
clauses to e + E and E + v. Want
call-by-name (don't evaluate an argument until it is used)? Drop the
v\ E clause for application so the hole never enters an argument position.
Want a language with exceptions? Add a clause and a
E[\mathsf{raise}\ v] \rightsquigarrow \mathsf{raise}\ v rule that lets an
exception "eat" its surrounding context up to the nearest handler — Felleisen's original motivation.
Evaluation contexts turned control operators (call/cc, generators,
\mathsf{try/catch}) from black magic into ordinary reduction rules. That is
why this style is often just called reduction semantics.
A tempting "simplification" is to write the context grammar with E + E instead
of the two clauses E + e and v + E. Resist it. With
E + E a term like (1+2) + (3+4) could be decomposed
two ways — hole in the left sum or hole in the right — so unique
decomposition fails, and with it determinism. The clause v + E (a
value to the left of the hole) is precisely what guarantees the left operand is finished before
the right one may be touched, giving exactly one legal decomposition. The value restriction is not a
stylistic nicety — it is the load-bearing wall. Drop it and the two operands become a nondeterministic
race.