Operational semantics

Definition

Operational semantics describes program behavior with evaluation judgments or transitions between configurations. A configuration may contain a program fragment together with an environment, store, continuation, or other abstract machine state.

The description is mathematical: it states which evaluations or transitions are valid. An interpreter or virtual machine may implement those rules, but a particular implementation is not itself the definition.

Styles of operational semantics

Small-step (structural operational semantics)

Computation is broken into atomic transitions:

$$\begin{array}{rl}2+3& \to 5\\ (2+3)\cdot 4& \to 5\cdot 4\to 20\end{array}$$

Useful for modeling concurrency, interleaving, and partial execution.

Big-step (natural semantics)

Describes evaluation in terms of final results:

$$(2+3)\cdot 4\Downarrow 20$$

Often clearer for reasoning about terminating programs.

Formal rules

Operational semantics is typically given with inference rules. For a simple arithmetic language:

$$E::=n\mid E+E$$

For left-to-right evaluation, three rules are needed:

$$\frac{E_1\to E_1^{\prime }}{E_1+E_2\to E_1^{\prime }+E_2}\frac{E_2\to E_2^{\prime }}{n+E_2\to n+E_2^{\prime }}{n}_1+n_2\to n_3\text{where }{n}_3=n_1+n_2$$

The first two rules select the next reducible subexpression. The third performs addition once both operands are values.

Evaluation trace:

$$(1+2)+3\to 3+3\to 6$$

Why it matters

• Provides a precise machine-like model of execution.
• Foundation for interpreters and virtual machines.
• Supports reasoning about correctness, resource use, and safety.

Relation to other concepts

• A free monad provides instruction syntax and sequencing. Operational rules can describe how a program in that representation evaluates.
• CPS makes the rest of a computation explicit as a continuation. Operational rules can describe how values pass to those continuations.
• Defunctionalization replaces a known family of functions with first-order data and an apply operation. Operational rules can describe the resulting explicit machine states.

These are objects and transformations that may be given an operational semantics. They are not operational semantics themselves.

In practice

Operational rules can guide an interpreter and provide a precise model against which to check it:

• The EVM can be modeled naturally as a small-step state transition system, while a terminating whole execution can also be related by a big-step judgment.
• Small-step rules often correspond closely to match arms in a Rust interpreter.

$$n_1+n_2\to n_3$$

The complete left-to-right relation above can be represented as Rust code:

enum Expr {
    Num(i64),
    Add(Box<Expr>, Box<Expr>),
}

fn step(expr: Expr) -> Option<Expr> {
    match expr {
        Expr::Num(_) => None,
        Expr::Add(left, right) => match (*left, *right) {
            (Expr::Num(a), Expr::Num(b)) => Some(Expr::Num(a + b)),
            (left @ Expr::Num(_), right) => step(right).map(|next| {
                Expr::Add(Box::new(left), Box::new(next))
            }),
            (left, right) => step(left).map(|next| {
                Expr::Add(Box::new(next), Box::new(right))
            }),
        },
    }
}

This function performs one transition. Repeated application produces the displayed trace; returning None means that the expression is already a value.

Operational and denotational questions

Operational rules can prove safety, progress, resource bounds, and correspondence with implementations. The limitation appears when operational machinery is chosen before the intended abstract meaning: implementation choices can become accidental semantic commitments.

Denotational Design does not reject operational semantics. It asks us to state the semantic domain, composition, and laws first, then relate the operational model to them.

The following clips motivate the danger of treating operational descriptions as the only source of insight.