Control Flow and Semantics §

These three notions — state, skip, composition — are the foundation on which every other control-flow rule builds: if and while are just different ways of choosing which sequence of assignments to run.

The state: think of $\sigma$ as a table with one row per variable currently in scope. There is exactly one cell per binding; assignment overwrites the cell’s content, it never creates a second cell. (Where those cells live physically — stack frame or heap — is covered in Memory Management.)

Assignment: $\sigma[x := v]$ is defined pointwise: it agrees with $\sigma$ on every variable except $x$, where it maps $x \mapsto v$. All other bindings are untouched — this is what makes assignment local.

Skip: $\text{skip}$ leaves the state unchanged: $\sigma \vdash \text{skip} \to \sigma$. It is the identity element of sequencing: $S; \text{skip}$ and $\text{skip}; S$ behave exactly like $S$. This is why a for loop with an empty body is legal and means “repeat the condition test only”.

Composition: $S_1; S_2$ is evaluated left to right:

$\frac{\sigma \vdash S_1 \to \sigma' \quad \sigma' \vdash S_2 \to \sigma''}{\sigma \vdash S_1; S_2 \to \sigma''}$

Specific example: take the program $x := 3;\; y := x + 1$ starting from the empty state $\sigma_0 = \{\}$:

1. Evaluate $x := 3$: the state becomes $\sigma_1 = \sigma_0[x := 3] = \{x \mapsto 3\}$.
2. Evaluate $y := x + 1$ in $\sigma_1$: look up $x$ (yields 3), compute 4, and the state becomes $\sigma_2 = \sigma_1[y := 4] = \{x \mapsto 3,\; y \mapsto 4\}$.

The order matters: had the program been $y := x + 1;\; x := 3$, the lookup of $x$ in step 2 would fail (or yield a default), which is why sequencing is not commutative.

Authoritative source: The Formal Semantics of Programming Languages (Winskel, 1993) — chapters 1–3 build everything from exactly these rules.

Conditionals and loops are derived rules: each one selects which sequence of assignments (the primitive from the previous section) to run, and how many times.

Short-circuit evaluation: $a \&\& b$ evaluates $b$ only if $a$ is true; $a \|\| b$ evaluates $b$ only if $a$ is false. This is a semantic choice, not a syntactic one.

The for loop desugared: the C-style for (init; cond; update) body is syntactic sugar for:

init;
while (cond) {
  body;
  update;
}

“Bounded” means the loop’s lifetime is controlled by three explicit parts: init runs once before the first test, cond is checked before every iteration, and update runs after each iteration. This contrasts with an unbounded while where the programmer must manage the counter manually.

Loop invariants: a predicate $P$ that holds before and after each iteration. Proving $P$ holds at loop exit (when $b$ is false) establishes the loop’s postcondition.

Tail position and tail recursion: a call is in tail position when no operation is pending after it — the caller’s frame has nothing left to do, so it can be discarded before the call executes. A function whose recursive calls are all in tail position is tail-recursive and can be compiled to a loop. Whether a runtime actually performs this tail-call optimization is a property of the implementation, not the language semantics; the mechanism (stack frames, stack overflow) is covered in Memory Management.

Lexical scope (static): a variable’s scope is determined by its textual position. $let x = 1; let f = () => x; let x = 2; f() // returns 1$.

Dynamic scope: a variable’s scope is determined by the call stack. Rare in modern languages (Scheme’s dynamic-wind, R5RS+; Common Lisp uses unwind-protect instead).

The difference is easiest to see when the same program is resolved both ways:

Closures: $let makeCounter = () => { let n = 0; return () => { n++; return n; }; }; let c = makeCounter(); c(); // 1, c(); // 2$. The inner function captures the mutable cell for $n$. The environment cell is shared: every call to c() mutates the same cell.

Hoisting: in JavaScript, variable declarations (var) and function declarations are moved to the top of their scope before execution. let and const are hoisted but not initialized (temporal dead zone).

Connection to the formal model: this is the state-and-assignment model of the sequencing section with one addition — an environment layer mapping names to cells, so that two names may share one cell (closures) or one name may denote different cells in different scopes (let per iteration).

Authoritative source: ECMAScript Language Specification — Lexical Environments.

Composition: $(g \circ f)(x) = g(f(x))$, type $(A \to B) \to (B \to C) \to (A \to C)$. Composition is associative — $h \circ (g \circ f) = (h \circ g) \circ f$ — which is why pipelines of transformations can be regrouped freely.

Partial application: fixing one argument of $f: A \times B \to C$ yields $f': A \to (B \to C)$.

Currying: $f: A \times B \to C$ is equivalent to $f': A \to (B \to C)$. $f(a, b) = f'(a)(b)$. Currying is what makes partial application uniform: every function of several arguments is secretly a function of one argument returning a function.

Specific example: with add = a => b => a + b, the partially applied add(3) is the function $b \mapsto 3 + b$, and map(add(3), [1, 2, 3]) yields [4, 5, 6] — no new machinery needed, just composition of an existing function with map.

Recursion schemes: catamorphisms (folds) and anamorphisms (unfolds) generalize recursion over inductive data types. A left fold (the default reduce in Python, JavaScript, and Haskell’s foldl):

$\text{foldl}(f, z, [a_1, \ldots, a_n]) = f(\ldots f(f(z, a_1), a_2) \ldots, a_n)$

A right fold (Haskell’s foldr):

$\text{foldr}(f, z, [a_1, \ldots, a_n]) = f(a_1, f(a_2, \ldots f(a_n, z) \ldots))$

The left fold is strict in the accumulator; the right fold can be lazy and may terminate on infinite lists.

Authoritative source: Haskell Report, section on folds.

Global picture: each layer adds one degree of dependency. Functor: the function is total and independent per element. Applicative: the shape of the computation is fixed in advance (all arguments known up front). Monad: the shape may depend on intermediate results — which is why monads can model effects like exceptions (stop early) and state (thread $\sigma$ through).

Specific example: parsing two integers where the second parse depends on the first requires a monad (>>=); parsing two independent integers needs only an applicative (<*>), which is why applicative parsers can be parallelized and monadic ones generally cannot.

Where to go next: the practical, pattern-level uses of these abstractions (Option chaining, Result propagation, promise chaining as a monad) with worked code are treated in Design Patterns; this page fixes only the type signatures and the progression.

Authoritative source: Applicative Programming with Effects (McBride & Paterson, 2008) and Monads for Functional Programming (Wadler, 1995).

Call-by-value (strict / eager): arguments are fully evaluated before the function body executes. This is the strategy of C, Java, Python, and most imperative languages. Side effects in arguments are visible to the callee.

Call-by-name (lazy): arguments are substituted unevaluated into the body and evaluated only when needed. This can avoid unnecessary computation but may re-evaluate the same expression multiple times.

Call-by-need (lazy with memoization): like call-by-name, but each argument is evaluated at most once and the result is cached. Haskell’s default strategy. This gives the efficiency of strict evaluation with the laziness of call-by-name.

A concrete comparison: take $f(x) = x + x$ and call it with a side-effecting argument — a counter increment:

let counter = 0;
function inc() { counter++; return counter; }
function f(x) { return x + x; }
f(inc());

The comparison, rendered as raw HTML (LaTeXMarkdown does not render pipe tables):

Call-by-name is the only strategy where the argument’s side effect happens twice — and it happens interleaved with the body’s execution rather than before it, which is why call-by-name programs with effects are notoriously hard to reason about. Call-by-need restores the “evaluated once” guarantee while keeping laziness.

Evaluation order: even in strict languages, the order in which arguments are evaluated is often unspecified (C) or left-to-right (Java, Python). This matters when arguments have side effects.

Short-circuit vs. full evaluation: $a \&\& b$ and $a \|\| b$ are inherently non-strict in their second operand — a special case of call-by-name embedded in an otherwise strict language.

The choice of strategy interacts with the type system (see Language Theory) and with the compiler’s code generation (see Compilation): a lazy language requires the runtime to allocate thunks (unevaluated expressions) on the heap.

Authoritative source: Report on the Algorithmic Language Haskell 2010 — semantics of lazy evaluation.

try / catch / finally:

try {
  S;            // may throw
} catch (e: T) {
  H;            // handler for type T
} finally {
  C;            // cleanup, runs whether or not an exception was thrown
}

The finally block runs on normal completion, on exception, and on non-local exit (e.g., return inside try). This makes it the canonical place for resource cleanup.

Non-local exits: return, break, continue, and exceptions all transfer control out of the current frame without executing the remaining statements. The key semantic question is: which cleanup code runs? In most languages, finally blocks and destructors run in reverse order of entry as the stack unwinds.

Interaction with scope: an exception does not “break” scope — it triggers the same cleanup (variable deallocation, finally blocks) that a normal return would, but the control transfer target is the handler, not the caller.

Scheme’s dynamic-wind (R5RS+) and Common Lisp’s unwind-protect provide explicit before/after guards that run on any exit (normal or exceptional), making the cleanup contract explicit rather than implicit.

Checked vs. unchecked exceptions: Java distinguishes checked (must be declared or caught) from unchecked (runtime) exceptions. C++ uses noexcept specifications. Python has no checked exceptions. The choice affects the type system and the compiler’s code generation.

Authoritative source: R5RS Scheme — control features (dynamic-wind).

Operational semantics defines meaning as a sequence of state transitions:

• Big-step (natural) semantics: $\sigma \vdash e \Downarrow v$ — expression $e$ in state $\sigma$ evaluates in one (possibly compound) step to value $v$.
• Small-step (structural) semantics: $\sigma \vdash e \to e'$ — one atomic transition. The reflexive-transitive closure $\to^*$ gives the full evaluation. Small-step makes it easier to reason about intermediate states and to define concurrency.

Denotational semantics maps each syntactic construct to a mathematical object (usually a function between domains):

• A command denotes a function from state to state: $\llbracket S \rrbracket : \Sigma \to \Sigma$.
• An expression denotes a function from environment to value: $\llbracket e \rrbracket : \Gamma \to V$.
• The key property is compositionality: the denotation of a compound expression is determined solely by the denotations of its parts.

Axiomatic semantics (Hoare logic) specifies meaning as pre/postcondition triples: $\{P\} \; S \; \{Q\}$ means “if $P$ holds before $S$ and $S$ terminates, then $Q$ holds after.” This is the basis for formal verification.

The two primitive rules, formally:

$\sigma \vdash \text{skip} \to \sigma \qquad \frac{\sigma \vdash S_1 \to \sigma' \quad \sigma' \vdash S_2 \to \sigma''}{\sigma \vdash S_1; S_2 \to \sigma''}$

skip is the identity on state; $S_1; S_2$ composes by evaluating $S_1$ to a state $\sigma'$, then $S_2$ in $\sigma'$. Every other rule (if, while, exceptions) is defined on top of these.

Worked example: take the tiny program $x := 3;\; y := x + 1$ from the empty state $\sigma_0 = \{\}$.

(a) Big-step derivation — one judgment per compound command, bottom-up:

$\frac{\sigma_0 \vdash x := 3 \Downarrow \sigma_1 \qquad \sigma_1 \vdash y := x + 1 \Downarrow \sigma_2}{\sigma_0 \vdash x := 3;\; y := x + 1 \Downarrow \sigma_2}$

where $\sigma_1 = \{x \mapsto 3\}$ and $\sigma_2 = \{x \mapsto 3,\; y \mapsto 4\}$. The premise on the left is discharged by the assignment axiom $\sigma \vdash x := 3 \Downarrow \sigma[x := 3]$; the right premise needs the expression sub-derivation $\sigma_1 \vdash x + 1 \Downarrow 4$ before the assignment axiom applies.

(b) Small-step derivation — a linear trace of atomic transitions on configurations $\langle S, \sigma \rangle$:

$\langle x := 3;\; y := x + 1,\; \sigma_0 \rangle$
$\to \langle y := x + 1,\; \{x \mapsto 3\} \rangle$
$\to \langle \text{skip},\; \{x \mapsto 3,\; y \mapsto 4\} \rangle$
$\to \{x \mapsto 3,\; y \mapsto 4\}$

Each arrow is one rule application: the sequencing rule exposes $x := 3$ first, the assignment axiom fires, then the same happens for $y := x + 1$, and finally the skip rule terminates the trace.

(c) Denotational mapping — no states are “reached”; the program is a function:

$\llbracket x := 3 \rrbracket = \lambda \sigma.\; \sigma[x := 3]$
$\llbracket S_1; S_2 \rrbracket = \llbracket S_2 \rrbracket \circ \llbracket S_1 \rrbracket$
$\llbracket x := 3;\; y := x + 1 \rrbracket\, \sigma_0 = \sigma_0[x := 3][y := 4] = \{x \mapsto 3,\; y \mapsto 4\}$

The three frameworks agree on the outcome ($\sigma_2$), but they expose different information: the big-step derivation shows why the result holds, the small-step trace shows each intermediate state (essential for concurrency), and the denotation shows the program as a composable function, enabling algebraic laws such as $\llbracket S; \text{skip} \rrbracket = \llbracket S \rrbracket$.

The three approaches are equivalent in expressive power for sequential programs but differ in what they make easy to reason about: operational → execution traces; denotational → algebraic laws; axiomatic → correctness proofs.

Authoritative source: The Formal Semantics of Programming Languages (Winskel, 1993).

Problem: Explain why the following JavaScript code prints 3, 3, 3 and not 0, 1, 2:

for (var i = 0; i < 3; i++) {
  setTimeout(() => console.log(i), 100);
}

for (let i = 0; i < 3; i++) {
  setTimeout(() => console.log(i), 100);
}
// prints 0, 1, 2

for (var i = 0; i < 3; i++) {
  (function(j) { setTimeout(() => console.log(j), 100); })(i);
}
// prints 0, 1, 2