IMP: A While Language

Everything so far has been expression-shaped: a term computes a value and has no lasting effect on the world. Real imperative programs are different — they mutate state. Assigning X := X + 1 does not "return" anything; it changes the value stored at X, and the next command sees the change. To give a semantics to that, we need one new ingredient: an explicit notion of the machine's memory.

IMP is the canonical toy imperative language — a "while language" — used to teach exactly this, following Glynn Winskel's textbook. It is deliberately minimal: integer variables, arithmetic and boolean expressions, assignment, sequencing, a conditional, and a single loop. Yet that single \mathsf{while} makes it Turing-complete, so IMP is rich enough to compute anything computable and to exhibit the one phenomenon expressions could not: non-termination. IMP will be our running example for the rest of the course — the same language gets a denotational and an axiomatic (Hoare-logic) semantics later, and it is illuminating to watch three very different accounts describe one language.

Syntax: expressions, booleans, commands

IMP has three syntactic categories. Arithmetic expressions and boolean expressions are pure (they read the state but never change it); commands are where the effects live.

a \;::=\; n \mid X \mid a_0 + a_1 \mid a_0 - a_1 \mid a_0 \times a_1 b \;::=\; \mathsf{true} \mid \mathsf{false} \mid a_0 = a_1 \mid a_0 \le a_1 \mid \lnot b \mid b_0 \wedge b_1 c \;::=\; \mathsf{skip} \mid X := a \mid c_0 \mathbin{;} c_1 \mid \mathsf{if}\ b\ \mathsf{then}\ c_0\ \mathsf{else}\ c_1 \mid \mathsf{while}\ b\ \mathsf{do}\ c

Here X ranges over locations (program variables) and n over integer literals. The whole language fits on one line each — and that economy is the point: every metatheorem we prove about IMP is short enough to do by hand, yet the lessons transfer directly to full languages.

The store \sigma

The missing ingredient is the store (or state) \sigma: a function from locations to integers,

\sigma \;:\; \mathbf{Loc} \to \mathbb{Z}.

So \sigma(X) is "the current contents of variable X". The one operation we need is update: write \sigma[X \mapsto n] for the store that agrees with \sigma everywhere except at X, where its value is n:

\big(\sigma[X \mapsto n]\big)(Y) \;=\; \begin{cases} n & \text{if } Y = X,\\ \sigma(Y) & \text{if } Y \neq X. \end{cases}

This is a mathematical update — it builds a new function, it does not "mutate" anything — which is precisely why the semantics stays clean and easy to reason about. Expressions are evaluated against a store: \langle a, \sigma\rangle \Downarrow n and \langle b, \sigma\rangle \Downarrow t, with the obvious rules (a location reads its value, \langle X,\sigma\rangle \Downarrow \sigma(X); operators evaluate their operands and combine).

Big-step rules for commands

A command does not produce a value — it transforms one store into another. So its big-step judgment has the shape

\langle c, \sigma\rangle \;\Downarrow\; \sigma'

read "running command c in store \sigma terminates in store \sigma'". Six rules define it. \mathsf{skip} does nothing; assignment evaluates its expression and updates the store; sequencing threads the store through:

\dfrac{\;}{\,\langle \mathsf{skip}, \sigma\rangle \Downarrow \sigma\,}\ \text{\small Skip}\qquad\dfrac{\,\langle a, \sigma\rangle \Downarrow n\,}{\,\langle X := a, \sigma\rangle \Downarrow \sigma[X \mapsto n]\,}\ \text{\small Assign} \dfrac{\,\langle c_0, \sigma\rangle \Downarrow \sigma' \qquad \langle c_1, \sigma'\rangle \Downarrow \sigma''\,}{\,\langle c_0 \mathbin{;} c_1, \sigma\rangle \Downarrow \sigma''\,}\ \text{\small Seq}

Look how Seq passes \sigma' — the store produced by c_0 — into c_1. That threading is the meaning of "one statement after another". The conditional evaluates its guard, then the chosen branch:

\dfrac{\,\langle b, \sigma\rangle \Downarrow \mathsf{true} \qquad \langle c_0, \sigma\rangle \Downarrow \sigma'\,}{\,\langle \mathsf{if}\ b\ \mathsf{then}\ c_0\ \mathsf{else}\ c_1, \sigma\rangle \Downarrow \sigma'\,}\ \text{\small If-True}\qquad\dfrac{\,\langle b, \sigma\rangle \Downarrow \mathsf{false} \qquad \langle c_1, \sigma\rangle \Downarrow \sigma'\,}{\,\langle \mathsf{if}\ b\ \mathsf{then}\ c_0\ \mathsf{else}\ c_1, \sigma\rangle \Downarrow \sigma'\,}\ \text{\small If-False}

The while rule — the one that ties a knot

The loop needs two rules. If the guard is false, the loop is over and the store is unchanged. If it is true, run the body once, then run the whole loop again in the new store:

\dfrac{\,\langle b, \sigma\rangle \Downarrow \mathsf{false}\,}{\,\langle \mathsf{while}\ b\ \mathsf{do}\ c, \sigma\rangle \Downarrow \sigma\,}\ \text{\small While-False} \dfrac{\,\langle b, \sigma\rangle \Downarrow \mathsf{true} \quad \langle c, \sigma\rangle \Downarrow \sigma' \quad \langle \mathsf{while}\ b\ \mathsf{do}\ c, \sigma'\rangle \Downarrow \sigma''\,}{\,\langle \mathsf{while}\ b\ \mathsf{do}\ c, \sigma\rangle \Downarrow \sigma''\,}\ \text{\small While-True}

Stare at While-True: the command \mathsf{while}\ b\ \mathsf{do}\ c appears in its own third premise. The rule is self-referential, and that is exactly how a finite rule captures an unbounded number of iterations — the derivation tree grows one nested \mathsf{while} deeper for every trip around the loop. A loop that runs k times has a derivation k While-True's tall, capped by one While-False. And a loop that never stops? Then there is no finite derivation at all — precisely the big-step blind spot: non-termination shows up as the absence of a proof of \langle c, \sigma\rangle \Downarrow \sigma'.

A loop, unrolled

Run \mathsf{while}\ X \le 2\ \mathsf{do}\ X := X + 1 from the store \{X \mapsto 0\}. Each pass tests the guard, and if it holds, executes the body and re-enters the loop in the updated store. Reveal the trace step by step — this is the chain of stores that the nested While-True derivations describe.

Three passes each fire While-True (guard true, body bumps X), and the fourth test 3 \le 2 is false, firing While-False and leaving the final store \{X \mapsto 3\}. Had the guard been, say, 0 \le X — always true — the chain would never end, and no derivation of \Downarrow \sigma' would exist.

An interpreter for IMP

The six command rules translate into a single exec function threading a store; expression rules become evalA / evalB. The store is an immutable map, updated functionally with the spread operator — exactly \sigma[X \mapsto n]. We run the classic example: factorial via a while loop.

type AExp = | { tag: "num"; n: number } | { tag: "loc"; x: string } | { tag: "add"; l: AExp; r: AExp } | { tag: "sub"; l: AExp; r: AExp } | { tag: "mul"; l: AExp; r: AExp }; type BExp = | { tag: "bool"; b: boolean } | { tag: "eq"; l: AExp; r: AExp } | { tag: "le"; l: AExp; r: AExp } | { tag: "not"; e: BExp } | { tag: "and"; l: BExp; r: BExp }; type Com = | { tag: "skip" } | { tag: "assign"; x: string; a: AExp } | { tag: "seq"; c0: Com; c1: Com } | { tag: "if"; b: BExp; c0: Com; c1: Com } | { tag: "while"; b: BExp; c: Com }; type Store = { [loc: string]: number }; // ⟨a, σ⟩ ⇓ n function evalA(a: AExp, s: Store): number { switch (a.tag) { case "num": return a.n; case "loc": return s[a.x] ?? 0; // unset locations read as 0 case "add": return evalA(a.l, s) + evalA(a.r, s); case "sub": return evalA(a.l, s) - evalA(a.r, s); case "mul": return evalA(a.l, s) * evalA(a.r, s); } } // ⟨b, σ⟩ ⇓ t function evalB(b: BExp, s: Store): boolean { switch (b.tag) { case "bool": return b.b; case "eq": return evalA(b.l, s) === evalA(b.r, s); case "le": return evalA(b.l, s) <= evalA(b.r, s); case "not": return !evalB(b.e, s); case "and": return evalB(b.l, s) && evalB(b.r, s); } } // ⟨c, σ⟩ ⇓ σ′ (returns the final store) function exec(c: Com, s: Store): Store { switch (c.tag) { case "skip": return s; // Skip case "assign": return { ...s, [c.x]: evalA(c.a, s) }; // Assign: σ[X↦n] case "seq": return exec(c.c1, exec(c.c0, s)); // Seq: thread the store case "if": return evalB(c.b, s) ? exec(c.c0, s) : exec(c.c1, s); case "while": // While return evalB(c.b, s) ? exec(c, exec(c.c, s)) : s; // true: body then loop again; false: done } } // Builders const num = (n: number): AExp => ({ tag: "num", n }); const loc = (x: string): AExp => ({ tag: "loc", x }); const asg = (x: string, a: AExp): Com => ({ tag: "assign", x, a }); const seq = (...cs: Com[]): Com => cs.reduce((c0, c1) => ({ tag: "seq", c0, c1 })); // Y := 1; while ¬(X = 0) do (Y := Y × X; X := X − 1) const factorial: Com = seq( asg("Y", num(1)), { tag: "while", b: { tag: "not", e: { tag: "eq", l: loc("X"), r: num(0) } }, c: seq(asg("Y", { tag: "mul", l: loc("Y"), r: loc("X") }), asg("X", { tag: "sub", l: loc("X"), r: num(1) })) }, ); const start: Store = { X: 5, Y: 0 }; console.log("start: σ =", JSON.stringify(start)); const final = exec(factorial, start); console.log("final: σ =", JSON.stringify(final)); // { X: 0, Y: 120 } console.log(`5! computed by the while loop = ${final["Y"]}`);

The loop ran five times, threading the store through each iteration, and left Y = 120 with X = 0. Every case of exec is one big-step rule read as a recursive equation — the while case even calls exec(c, …) on itself, mirroring the self-reference of While-True.

Determinism and (non)termination

That word partial is unavoidable, and it is not a defect of our rules: by the halting problem, no total rule set could decide in advance whether an arbitrary \mathsf{while} loop terminates. Non-termination is a genuine feature of any Turing-complete language, and IMP wears it honestly: a diverging loop simply has no derivation, so \mathcal{C}\llbracket c \rrbracket(\sigma) is undefined there. When we give IMP a denotational semantics later, this partial function is exactly the object we will construct as a least fixed point; when we give it a Hoare-logic semantics, termination becomes a separate proof obligation. Same language, three lenses.

IMP owes its fame to Glynn Winskel's 1993 textbook The Formal Semantics of Programming Languages, where it is the thread running through the whole book: first an operational semantics (the rules above), then a denotational one, then an axiomatic (Hoare logic) one, with theorems proving all three agree. That triangulation — one small language seen operationally, denotationally, and axiomatically — is the single most valuable exercise in the subject, because it shows these are not rival theories but three views of one meaning. IMP is deliberately just past the edge of triviality: drop the \mathsf{while} and it is a decidable calculator; keep it and you have a Turing-complete language whose metatheory still fits in a lecture. Almost every modern proof assistant (Coq's Software Foundations, Isabelle's Concrete Semantics) formalises IMP as its first serious case study.

Two related traps snare beginners. First, \sigma[X \mapsto n] is a mathematical function update, not an in-place edit of a shared object: it denotes a store that differs from \sigma at one point. In the interpreter we honour this with { ...s, [c.x]: n } — a fresh map — never by writing s[c.x] = n onto a shared object, which would let earlier stores be corrupted by later commands. Second, the effect of one command reaches the next only through the store threaded by Seq: read the rule and you will see \sigma' flowing out of c_0 and into c_1. There is no hidden global mutable variable; the store is passed explicitly, everywhere. Get either wrong and your semantics will "work" on straight-line code but give nonsense the moment a loop reuses a store.