Operational Semantics

Origin. Gordon Plotkin, "A Structural Approach to Operational Semantics", Aarhus technical report DAIMI FN-19 (1981), reprinted in the Journal of Logic and Algebraic Programming (2004). The point of structural operational semantics is that the transition relation is defined by inference rules following the syntax, so a program's behaviour is derived from its parts. Gilles Kahn's natural semantics (1987) is the big-step counterpart. Felleisen and Hieb (1992) recast reduction with evaluation contexts, and Wright and Felleisen (1994) turned the whole apparatus into the standard syntactic proof of type soundness.

Models. Meaning is how a program runs, not what it denotes. A configuration ⟨e, σ⟩ pairs a term with whatever state it needs, and the rules define a transition relation on configurations — the least relation closed under the rules, so every property is provable by rule induction. Small-step semantics exposes the intermediate states and therefore divergence, nondeterminism and interleaving; big-step semantics relates a term directly to its value and is closer to an interpreter. Both are syntactic: no domains, no mathematical objects standing for programs.

Formalism.

Small-step (structural): e → e' (one step reduction) e →* e' (many steps)

Big-step (natural): e ⇓ v (e evaluates to v)

Rules (small-step): E-App1: e₁ → e₁' ────────────── e₁ e₂ → e₁' e₂

E-App2: e₂ → e₂' ────────────── v₁ e₂ → v₁ e₂'

E-Beta: (λx.e) v → e[v/x]

Rules (big-step): E-App: e₁ ⇓ λx.e e₂ ⇓ v₂ e[v₂/x] ⇓ v ───────────────────────────────────── e₁ e₂ ⇓ v

Evaluation contexts: E ::= □ | E e | v E | ... E[e] → E[e'] if e → e'.

Call-by-value: Reduce arguments before substitution. Values don't reduce.

Call-by-name: Substitute unreduced arguments. Lazy evaluation variant.

Stuck terms: A configuration that is not a value and has no transition. Type soundness is the claim that no well-typed program reaches one.

Contextual equivalence: e ≃ e′ iff for every closing context C, C[e] and C[e′] both diverge or both converge. Defined from the transition relation alone; the standard notion of program equality here.

Rule formats: Constraints on the shape of rules, imposed so that results hold for every language defined in the format. GSOS and tyft/tyxt guarantee that bisimilarity is a congruence.

Symbols.

Symbol	Unicode	Name	Meaning
→	U+2192	Step	One small-step reduction
→*	—	Steps	Reflexive transitive closure of →
⇓	U+21D3	Downwards double arrow / Evaluates	Big-step: e ⇓ v
□	U+25A1	White square / Hole	The position in an evaluation context where reduction happens
⟨ ⟩	—	Configuration	⟨e, σ⟩ pairs a term with a state
σ	U+03C3	Sigma	The store or environment component of a configuration
E	—	Evaluation context	A term with one hole, marking the next redex
≃	U+2243	Asymptotically equal to	Contextual equivalence

Metatheory. Wright and Felleisen (1994) gave the argument that made the style dominant: type soundness follows from progress (a well-typed term is a value or takes a step) and preservation (a step keeps the type), both proved by induction on typing derivations, with no denotational model anywhere. Small-step and big-step agree on terminating programs — e ⇓ v exactly when e →* v — but only the small-step relation separates divergence from getting stuck, since in big-step form both are simply the absence of a derivation. When the rules are read as defining a labelled transition system, rule formats decide the algebraic properties: Bloom, Istrail and Meyer's GSOS format (1995) and the tyft/tyxt format of Groote and Vaandrager (1992) guarantee that strong bisimilarity is a congruence for every operator so defined. Negative premises require stratification for the relation to exist at all.

Applies to. Language specification. Type soundness. Mechanized proofs. Compiler verification. Semantics comparison.

Limitations. The semantics is intensional. It fixes an evaluation order and a term representation, so it assigns no meaning to a program independent of how the program is written, and equality of programs has to be recovered as contextual equivalence — whose quantification over all contexts makes it hard to establish directly, which is why logical relations and applicative bisimulation exist. Big-step semantics cannot distinguish divergence from a stuck state, so type soundness in that style needs coinductive rules or explicit error configurations. Rules do not compose: adding state, exceptions or continuations forces every existing rule to be revisited to thread the new component, the propagation problem that modular and monadic variants of SOS were designed to remove. And nothing in the method guarantees that a denotational model matching the semantics exists or is fully abstract.