Operational semantics

Operational semantics defines meaning in terms of computation steps. A program is represented by a configuration, commonly a term paired with an environment, store, or control state, and execution is described by a transition relation between configurations.¹ In small-step semantics, each transition models one elementary reduction, so a sequence of transitions exposes the intermediate states of evaluation. In big-step semantics, also called natural semantics, a judgment relates an initial expression directly to its final value or result.

The distinction affects what a specification can express. Small-step rules naturally represent divergence, interleaving, exceptions, and individual machine actions; big-step rules are often shorter for terminating computations but may not distinguish failure from nontermination without additional judgments.² Both styles can describe expressions, commands, functional languages, imperative stores, and abstract machines.

Inference rules provide the executable-looking grammar of an operational semantics. A rule has premises above a line and a conclusion below it, such as reducing the left operand of an addition before reducing the right, or selecting a branch after a Boolean condition becomes true. This method is often called structural operational semantics, because rules follow the syntactic structure of programs and can be extended construct by construct.¹

Evaluation contexts offer another way to state where the next reduction may occur, separating the choice of evaluation order from the rules for individual operations. A language specification can thereby make call-by-value, call-by-name, short-circuiting, sequencing, mutation, and exception propagation explicit. Formal rules also expose ambiguities: if two rules apply to the same configuration, the language may be nondeterministic unless additional restrictions establish determinism.

Operational semantics supplies the foundation for proving that language implementations behave as intended. A typical type-safety argument combines progress, which says that a well-typed program is either finished or can take a step, with preservation, which says that a step does not invalidate its type.³ Related results establish determinism, termination for selected fragments, compiler correctness, and correspondence between source programs and lower-level machines.

The same rules can guide implementation. An interpreter may follow big-step judgments directly, while a reducer or abstract machine can execute small-step transitions. Mechanized developments in systems such as Coq and Isabelle represent syntax, judgments, and proofs inside a proof assistant, reducing errors in metatheory and allowing definitions to be tested or extracted into executable code.²⁵

Operational semantics also describes behavior that is not naturally summarized by a final value. In concurrency, labeled transitions can record communication actions and support reasoning about interleavings, bisimulation, and observational equivalence. For interactive or reactive programs, the relevant meaning may be an execution trace, a set of possible traces, or a relation between externally visible actions rather than termination.

Small-step systems are especially useful for modeling unusual control features, including exceptions, continuations, coroutines, nondeterministic choice, resource exhaustion, and low-level memory operations. The K Framework turns executable semantic rules into language definitions and analysis tools, illustrating how operational descriptions can serve simultaneously as specifications, interpreters, and testing infrastructure.⁴ A specification may also deliberately permit stuck states to represent undefined behavior, then use separate safety conditions to prove that valid programs never reach them.

Configuration

A formal representation of the current computational state, such as an expression together with an environment and store.

Small-step semantics

A semantics in which each rule describes one elementary transition during execution.

Big-step semantics

A semantics that relates an initial program directly to a final value, state, or result.

Evaluation context

A syntactic context identifying the subexpression selected for the next reduction.

Bisimulation

A relation used to show that two transition systems exhibit matching observable behavior.