Small-Step (Structural) Operational Semantics
A programming language is not really defined until we can say, with mathematical precision,
what a program does. Operational semantics answers that question by describing
computation as a sequence of elementary moves — like watching a Turing machine or a calculator tick
forward one key-press at a time. In the small-step (or structural) style, due
to Gordon Plotkin, we define a single relation
e \;\longrightarrow\; e'
read "the term e takes one step of computation to
e'". Running a program is then just following the arrow as far as it goes:
e \to e_1 \to e_2 \to \dots until you reach something that cannot move. The
beauty of the method is that the whole dynamics of a language is captured by a handful of
inference rules, each so simple you could check it by hand.
We will pin the idea down on a tiny language of arithmetic and boolean expressions — small enough to fit
in your head, rich enough to show every phenomenon that matters: values, reduction under a
strategy, stuck terms, multi-step reduction, and determinism.
The language
Our terms are numbers, the two booleans, addition, multiplication, and a conditional. Written as a
grammar:
e \;::=\; n \mid \mathsf{true} \mid \mathsf{false} \mid e_1 + e_2 \mid e_1 \times e_2 \mid \mathsf{if}\ e_1\ \mathsf{then}\ e_2\ \mathsf{else}\ e_3
Among all terms, some are already finished — there is nothing left to compute. We call
these the values, and single them out with their own grammar:
v \;::=\; n \mid \mathsf{true} \mid \mathsf{false}
A value is the goal of evaluation. Everything else — a term with an operator still waiting to fire — is a
redex-containing expression that ought to be able to step. (As we will see, "ought to" hides a
subtlety: some non-values are stuck.)
Two flavours of rule: computation and congruence
Every small-step rule is one of two kinds, and telling them apart is the single most clarifying idea in
the subject.
A computation rule (Plotkin's β-style rule, sometimes an "axiom") does real
work: it fires an operator whose operands are already values. Our arithmetic has one such rule per
operator, plus two for the conditional:
\dfrac{\;}{\,n_1 + n_2 \;\longrightarrow\; n_3\,}\;\;(n_3 = n_1 + n_2)\qquad\text{\small E-Add}
\dfrac{\;}{\,n_1 \times n_2 \;\longrightarrow\; n_3\,}\;\;(n_3 = n_1 \cdot n_2)\qquad\text{\small E-Mul}
\dfrac{\;}{\,\mathsf{if}\ \mathsf{true}\ \mathsf{then}\ e_2\ \mathsf{else}\ e_3 \;\longrightarrow\; e_2\,}\ \text{\small E-IfTrue}\qquad\dfrac{\;}{\,\mathsf{if}\ \mathsf{false}\ \mathsf{then}\ e_2\ \mathsf{else}\ e_3 \;\longrightarrow\; e_3\,}\ \text{\small E-IfFalse}
A congruence rule (also called a structural or search rule) does no
arithmetic at all. It says: "I cannot fire the top-level operator yet, because a sub-term is not a value.
So step inside that sub-term instead." These rules are what make the semantics
structural — computation reaches down into the syntax tree.
\dfrac{\,e_1 \longrightarrow e_1'\,}{\,e_1 + e_2 \;\longrightarrow\; e_1' + e_2\,}\ \text{\small E-Add-L}\qquad\dfrac{\,e_2 \longrightarrow e_2'\,}{\,v_1 + e_2 \;\longrightarrow\; v_1 + e_2'\,}\ \text{\small E-Add-R}
\dfrac{\,e_1 \longrightarrow e_1'\,}{\,\mathsf{if}\ e_1\ \mathsf{then}\ e_2\ \mathsf{else}\ e_3 \;\longrightarrow\; \mathsf{if}\ e_1'\ \mathsf{then}\ e_2\ \mathsf{else}\ e_3\,}\ \text{\small E-If}
Look hard at E-Add-R: its left operand is a value v_1,
not an arbitrary e_1. That single choice encodes the evaluation strategy.
Because E-Add-L can only fire while the left operand is not a value, and E-Add-R can only fire
once it is, the two rules together force left-to-right evaluation. Multiplication
gets the mirror-image pair E-Mul-L and E-Mul-R, and the conditional evaluates only its guard (E-If) — never
its branches — until the guard is decided.
Reduction as a chain
Put the rules to work on (1+2)\times(3+4). At each moment, exactly one rule
applies — the semantics walks the term down to a value. Reveal the chain step by step; each
arrow is one use of \longrightarrow, annotated with the rule that fired.
Notice how the congruence rules E-Mul-L and E-Mul-R merely
navigate — they carry the arrow down into a sub-term — while E-Add and
E-Mul are the only steps that actually compute a number. Every reduction sequence is
this interleaving: search down to a redex, fire it, repeat.
Multi-step reduction \longrightarrow^{*}
One step is rarely enough. We define multi-step reduction
\longrightarrow^{*} as the reflexive–transitive closure of
\longrightarrow — the smallest relation closed under these three rules:
\dfrac{\;}{\,e \longrightarrow^{*} e\,}\ \text{\small(refl)}\qquad\dfrac{\,e \longrightarrow e'\,}{\,e \longrightarrow^{*} e'\,}\ \text{\small(incl)}\qquad\dfrac{\,e \longrightarrow^{*} e' \quad e' \longrightarrow^{*} e''\,}{\,e \longrightarrow^{*} e''\,}\ \text{\small(trans)}
In words: any term reaches itself in zero steps; one step is a (short) reduction; and reductions compose.
So e \longrightarrow^{*} v means "e evaluates fully
to the value v", and that is exactly what we mean by "running the program to
completion". We say e is in normal form when no step applies
to it — e \not\longrightarrow.
Values versus stuck terms
Here is where the tiny language earns its keep. A term in normal form is one that cannot step. The
good normal forms are the values — 7, \mathsf{true}.
But look at
\mathsf{true} + 2.
It is not a value. Yet no rule applies: E-Add needs two numbers and
\mathsf{true} is not one; E-Add-L needs the left operand to
step, but \mathsf{true} is already a value and cannot; E-Add-R
needs the right operand to step, but 2 is a value too. The term is
stuck: a normal form that is not a value.
- A term e is stuck iff it is in normal form
(e \not\longrightarrow) and is not a value.
- Stuck terms are precisely the run-time errors: "\mathsf{true} is not a
number", "add a function to an integer", "call a non-function". A type system exists
to prove a well-typed program never gets stuck — the famous slogan "well-typed programs do not go
wrong."
This is a crucial payoff of the small-step style, and one we could not even state without it:
being stuck is a property of the reduction arrow, visible only because we watch computation move one step
at a time.
The stepper, in code
The whole semantics is a single recursive function: given a term, return the term after one step, or
null if it is already a normal form. The structure of the code mirrors the rules exactly —
computation rules are the base cases, congruence rules are the recursive ones. A driver then follows the
arrow, printing the reduction sequence.
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): boolean => e.tag === "num" || e.tag === "bool";
// One step of e -> e' , or null if e is a normal form (value OR stuck).
function step(e: Term): Term | null {
switch (e.tag) {
case "add":
case "mul": {
// Computation rule: both operands are numbers -> fire the operator.
if (e.l.tag === "num" && e.r.tag === "num") {
const n = e.tag === "add" ? e.l.n + e.r.n : e.l.n * e.r.n;
return { tag: "num", n };
}
// Congruence -L: left operand not yet a value -> step it.
if (!isValue(e.l)) {
const l = step(e.l);
return l ? { ...e, l } : null;
}
// Congruence -R: left is a value, step the right.
const r = step(e.r);
return r ? { ...e, r } : null;
}
case "if": {
if (e.c.tag === "bool") return e.c.b ? e.t : e.e; // E-IfTrue / E-IfFalse
const c = step(e.c); // E-If: step the guard
return c ? { ...e, c } : null;
}
default:
return null; // num / bool: already a value
}
}
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)}`;
}
}
// Follow the arrow to a normal form, printing each step, then say why we stopped.
function run(e: Term): void {
console.log(show(e));
let cur: Term = e;
let next: Term | null;
while ((next = step(cur)) !== null) { cur = next; console.log("-> " + show(cur)); }
console.log(isValue(cur) ? " (value: done)" : " (STUCK: normal form, not a value)");
}
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) } });
console.log("---");
// if true then 10 else 20 — the guard is a value, so E-IfTrue fires immediately.
run({ tag: "if", c: { tag: "bool", b: true }, t: num(10), e: num(20) });
console.log("---");
// A STUCK term: true + 2 reaches a normal form that is NOT a value.
run({ tag: "add", l: { tag: "bool", b: true }, r: num(2) });
The last example prints (true + 2) and then stops — step returned
null on a non-value. That halt is the stuck state: the operational semantics has
detected a run-time type error, purely by running out of applicable rules.
Determinism
Our rules were carefully arranged so that from any term at most one rule applies. That gives the
cornerstone metatheorem of this language:
- If e \longrightarrow e' and e \longrightarrow e'',
then e' = e''.
- Consequently every term has at most one normal form, and
\longrightarrow^{*} is a partial function from terms to values —
"running the program" has a single well-defined answer (when it has one at all).
The proof is a short induction on the derivation of e \longrightarrow e'. The
key observations: the value restriction on E-Add-R (and E-Mul-R) means E-Add-L and E-Add-R can
never both fire on the same term; and a computation rule and a congruence rule never overlap, because a
computation rule requires operands that are values (which cannot themselves step). Not every
language is deterministic — concurrent and nondeterministic calculi deliberately allow several steps —
but for a sequential expression language, determinism is exactly what we want.
In 1981 Gordon Plotkin circulated a set of lecture notes at Aarhus University titled
"A Structural Approach to Operational Semantics" — forever after abbreviated SOS.
Before SOS, the meaning of a language was usually given by an interpreter written in some
metalanguage, or by heavyweight denotational domain theory. Plotkin's insight was that you could specify
a language's dynamics with the same lightweight inference rules logicians use for proof systems:
computation becomes a derivation, and the syntax tree itself drives the search for the next redex — hence
structural. The notes went unpublished for a quarter of a century (finally appearing in the
Journal of Logic and Algebraic Programming in 2004) yet became one of the most cited documents
in all of programming-language theory. Almost every semantics you will meet — this course included — is
written in Plotkin's notation.
Beginners routinely collapse two very different situations into one word, "done". Evaluation
stops for two reasons, and only one of them is success:
- Success: the term reduced to a value (7,
\mathsf{true}). Nothing more to do — this is the answer.
- Failure: the term reduced to a stuck normal form
(\mathsf{true} + 2). No rule applies, but it is not an answer — it
is a run-time error frozen in place.
"Cannot step" is not the definition of a value. Values are defined by their own grammar; stuck
terms are the non-values that happen to be normal forms. A third possibility — never stopping at all
(divergence) — cannot arise in this terminating language, but it looms large the moment we add
recursion, and small-step semantics is the tool that lets us see it: an infinite chain
e \to e_1 \to e_2 \to \cdots that never reaches a normal form.