A topic in the Open Knowledge Graph — a free, open map of 15,290 topics and the order to learn them in.
Operational semantics defines the meaning of programs by specifying how they execute, step by step. Small-step (structural) operational semantics defines a transition relation that reduces a program configuration by one computational step at a time, making evaluation order and intermediate states explicit. Big-step (natural) operational semantics defines a relation that maps a program directly to its final result, abstracting away intermediate steps. Both are formalized as inference rules that inductively define the evaluation relation. Operational semantics provides the rigorous mathematical foundation upon which Hoare logic, type soundness proofs, and abstract interpretation are built -- without a formal definition of what programs mean, reasoning about program correctness is informal at best.
Programming languages need precise definitions of what their programs mean. Informal English descriptions are ambiguous -- does `x++ + x++` in C evaluate left-to-right, right-to-left, or is it undefined? Operational semantics answers such questions by defining a mathematical relation that specifies exactly how programs execute. There are two main styles, both formalized as sets of inference rules.
Small-step operational semantics (also called structural operational semantics or SOS, after Plotkin's 1981 framework) defines a transition relation `->` on configurations. A configuration pairs a program fragment with a state (variable assignments, heap, etc.). Each rule specifies one atomic computation step. For example, the rule for addition says: if both operands are integer values n1 and n2, then `n1 + n2 -> n` where n is their sum. If the left operand is not yet a value, a congruence rule says `e1 + e2 -> e1' + e2` whenever `e1 -> e1'`, specifying left-to-right evaluation order. Full program execution is the reflexive-transitive closure `->*` of the single-step relation: starting from the initial configuration, repeatedly apply transition rules until no rule applies (the program is stuck or has produced a final value).
Big-step operational semantics (also called natural semantics, after Kahn's 1987 formulation) defines an evaluation relation `=>` that maps a configuration directly to a final value. The rule for addition says: if `e1 => n1` and `e2 => n2`, then `e1 + e2 => n1 + n2`. The derivation tree for a big-step judgment mirrors the recursive call structure of an interpreter. Big-step semantics is often more concise and intuitive for deterministic, terminating languages -- it reads almost like a recursive interpreter specification. However, it cannot naturally express non-termination (there is simply no derivation for a diverging program) or distinguish stuck programs from diverging ones. It also struggles with concurrency and interleaving, where intermediate states matter.
The choice between small-step and big-step depends on what you need to reason about. Small-step is essential when intermediate states are observable or important: concurrency (interleaving of steps from different threads), type soundness proofs (progress: "well-typed programs can always take a step"), and reasoning about non-termination. Big-step is preferred for simple languages or when you only care about input-output behavior. Many formalizations use both: big-step for the deterministic core language, small-step for the concurrency and control-flow extensions. The two styles can be shown equivalent for terminating, deterministic programs: if `e =>* v` in big-step, then `e ->* v` in small-step, and vice versa.
Operational semantics is not just a theoretical exercise -- it is the foundation on which formal verification rests. Hoare logic's soundness theorem is stated with respect to the operational semantics: `{P} C {Q}` means that for all states sigma satisfying P, if `(C, sigma) ->* (skip, sigma')`, then sigma' satisfies Q. Abstract interpretation's soundness is proved by showing the abstract transfer functions over-approximate the concrete transitions defined by the operational semantics. Type soundness (via progress and preservation) is entirely a statement about the operational transition relation. Without a formal semantics, verification is informal reasoning about an informal object -- operational semantics makes it rigorous mathematics about a mathematical object. This is why Plotkin's SOS framework is one of the most cited papers in programming language theory: it gave the field its mathematical foundation.