Big-Step (Natural) Semantics
Small-step
semantics shows a computation ticking forward one move at a time. Sometimes,
though, we do not care about the intermediate scenery — we only want to know the final answer.
Big-step semantics (also called natural semantics or evaluation
semantics) captures exactly that: a single relation
e \;\Downarrow\; v
read "the term e evaluates to the value
v". Where small-step gave us e \to e_1 \to \cdots \to v,
big-step jumps straight from the whole expression to its result. The relation is defined by inference
rules whose premises evaluate the sub-expressions and whose conclusion assembles the answer — so
a proof that e \Downarrow v is a derivation tree mirroring the
shape of e itself.
We keep the same little language of numbers, booleans, +,
\times and \mathsf{if}, so we can hold the two
styles side by side and watch them agree — and, crucially, watch where big-step goes blind.
The evaluation rules
A value evaluates to itself — the axioms at the leaves of every derivation:
\dfrac{\;}{\,n \Downarrow n\,}\ \text{\small B-Num}\qquad\dfrac{\;}{\,\mathsf{true} \Downarrow \mathsf{true}\,}\ \text{\small B-True}\qquad\dfrac{\;}{\,\mathsf{false} \Downarrow \mathsf{false}\,}\ \text{\small B-False}
To evaluate a sum, evaluate both operands to numbers and add — the premises sit above the line,
the conclusion below:
\dfrac{\,e_1 \Downarrow n_1 \qquad e_2 \Downarrow n_2\,}{\,e_1 + e_2 \;\Downarrow\; n_3\,}\;\;(n_3 = n_1 + n_2)\qquad\text{\small B-Add}
\dfrac{\,e_1 \Downarrow n_1 \qquad e_2 \Downarrow n_2\,}{\,e_1 \times e_2 \;\Downarrow\; n_3\,}\;\;(n_3 = n_1 \cdot n_2)\qquad\text{\small B-Mul}
The conditional evaluates its guard, then only the chosen branch. Note there are two rules — one
for each way the guard can come out — and the losing branch is never evaluated at all:
\dfrac{\,e_1 \Downarrow \mathsf{true} \qquad e_2 \Downarrow v\,}{\,\mathsf{if}\ e_1\ \mathsf{then}\ e_2\ \mathsf{else}\ e_3 \;\Downarrow\; v\,}\ \text{\small B-IfTrue}\qquad\dfrac{\,e_1 \Downarrow \mathsf{false} \qquad e_3 \Downarrow v\,}{\,\mathsf{if}\ e_1\ \mathsf{then}\ e_2\ \mathsf{else}\ e_3 \;\Downarrow\; v\,}\ \text{\small B-IfFalse}
There is no congruence rule here — nothing like small-step's E-Add-L. The recursion into
sub-terms is baked into the premises of each rule, not spun out as separate structural steps.
That is exactly why big-step is often more compact to write and more convenient for building an
interpreter.
A derivation tree
A single judgment e \Downarrow v is justified by a tree of rule
applications: the conclusion sits at the bottom, its premises stacked above it, all the way up to axioms
at the leaves. Here is the full derivation of (1+2)\times(3+4) \Downarrow 21.
Reveal it from the leaves down to the root — that is the order in which the sub-expressions are actually
evaluated.
Read the tree as a proof: the two axioms 1\Downarrow 1 and
2\Downarrow 2 justify 1+2\Downarrow 3 by
B-Add; symmetrically 3+4\Downarrow 7; and those two results
justify the root (1+2)\times(3+4)\Downarrow 21 by B-Mul. The
shape of the derivation is the shape of the syntax tree — that structural correspondence is the
signature of natural semantics.
The evaluator, in code
Big-step semantics translates almost verbatim into a recursive interpreter: one function
evaluate that, given a term, returns its value. Each rule becomes one branch;
recursion into a premise becomes a recursive call. The absence of a value — because a term is stuck —
becomes a thrown error, since no rule applies.
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 };
type Value = { tag: "num"; n: number } | { tag: "bool"; b: boolean };
// e ⇓ v : return the value, or throw if no rule applies (a stuck term).
function evaluate(e: Term): Value {
switch (e.tag) {
case "num": return e; // B-Num
case "bool": return e; // B-True / B-False
case "add":
case "mul": {
const l = evaluate(e.l), r = evaluate(e.r); // evaluate BOTH premises
if (l.tag !== "num" || r.tag !== "num")
throw new Error(`stuck: cannot ${e.tag} non-numbers`);
const n = e.tag === "add" ? l.n + r.n : l.n * r.n;
return { tag: "num", n }; // B-Add / B-Mul
}
case "if": {
const c = evaluate(e.c); // evaluate the guard
if (c.tag !== "bool") throw new Error("stuck: if-guard is not a boolean");
return c.b ? evaluate(e.t) : evaluate(e.e); // B-IfTrue / B-IfFalse
}
}
}
const num = (n: number): Term => ({ tag: "num", n });
const show = (v: Value) => v.tag === "num" ? String(v.n) : String(v.b);
// (1 + 2) * (3 + 4) ⇓ 21
console.log("result =", show(evaluate(
{ tag: "mul", l: { tag: "add", l: num(1), r: num(2) }, r: { tag: "add", l: num(3), r: num(4) } })));
// if false then 10 else 20 ⇓ 20 (then-branch never evaluated)
console.log("result =", show(evaluate(
{ tag: "if", c: { tag: "bool", b: false }, t: num(10), e: num(20) })));
// A STUCK term: true + 2 has NO derivation, so evaluate throws.
try { evaluate({ tag: "add", l: { tag: "bool", b: true }, r: num(2) }); }
catch (err) { console.log("no ⇓ derivation ->", (err as Error).message); }
The third case is the whole point of this page. There is simply no rule whose conclusion matches
\mathsf{true}+2 \Downarrow v, so no derivation exists, and the interpreter can
only fail. Big-step reports "there is no value" — but it cannot tell you why.
The blind spot: stuck and diverging look identical
Small-step and big-step agree on every terminating, well-behaved program (see the theorem below). They
part ways on the two pathological cases, and this is the deepest lesson of the page.
| Situation | Small-step \to | Big-step \Downarrow |
|---|
| Success | e \to^{*} v | e \Downarrow v |
| Stuck (run-time error) | e \to^{*} e', e' stuck, not a value | no derivation of e \Downarrow v |
| Divergence (loops forever) | infinite chain e \to e_1 \to e_2 \to \cdots | no derivation of e \Downarrow v |
Look at the right-hand column. Both failure modes show up as "no finite derivation
exists" — big-step cannot distinguish a program that crashed from one that runs forever.
Small-step keeps them apart effortlessly: a stuck term is a finite chain ending at a non-value,
while divergence is an infinite chain. (Our terminating toy language never diverges, but the
moment we add recursion,
it can — and then this distinction is everything.) This is the classic reason theorists reach for
small-step when reasoning about non-termination, safety, or type soundness.
The two styles agree
- For every term e and value v:
e \Downarrow v iff e \to^{*} v.
- Read left to right: any big-step evaluation can be "unrolled" into a small-step sequence. Read right
to left: any small-step run to a value can be "folded" into a big-step derivation.
The \Rightarrow direction is an induction on the big-step derivation
(each premise's small-step run is stitched in front of the others using the congruence rules). The
\Leftarrow direction is an induction on the length of the small-step
sequence, with a key lemma: if e \to e' and
e' \Downarrow v, then e \Downarrow v. Determinism of
\Downarrow (each e has at most one
v) then follows from the determinism of \to. On
terminating programs the two accounts are genuinely interchangeable — pick whichever makes your proof
shorter.
The name natural semantics comes from Gilles Kahn and his group at INRIA in the late 1980s.
Their point was that the derivation trees of \Downarrow look exactly like
proofs in natural deduction — premises above a line, conclusion below — the proof format Gerhard
Gentzen introduced in the 1930s precisely because it mirrored "natural" mathematical reasoning. Kahn even
built a tool, Centaur/Typol, that took such rules as input and generated a working
interpreter and type-checker. So when you write a big-step rule you are, quite literally, doing proof
theory: a program's execution is a proof that it produces its answer.
The single most important caveat about big-step semantics: e \Downarrow v is a
relation about success. Its failure — the absence of any v —
lumps together two utterly different fates:
- the program got stuck (a type error like \mathsf{true}+2),
which is a finite failed search for a rule; and
- the program diverges (an infinite regress of recursive premises), which is an
infinite tree that is not a derivation at all.
If your metatheory needs to say "well-typed programs never crash, though they may loop" — the
precise statement of type safety — plain big-step cannot express it, because it cannot see the difference.
Use small-step (or an enriched big-step with an explicit "goes-wrong" answer, or a coinductive
\Downarrow^{\infty} relation for divergence) instead. Reaching for big-step to
prove a soundness theorem about non-termination is the classic trap.