Operational Semantics

Definition

Operational semantics defines the meaning of programs by specifying how they execute step by step. It models program execution as transitions between configurations - abstract states containing program fragments, environments, or memory.

Styles of Operational Semantics

Small-step (Structural Operational Semantics)

Computation is broken into atomic transitions:

(2 + 3) → 5
(2 + 3) * 4 → 5 * 4 → 20

Useful for modeling concurrency, interleaving, and partial execution.

Big-step (Natural Semantics)

Describes evaluation in terms of final results:

(2 + 3) * 4 ⇓ 20

Often clearer for reasoning about terminating programs.

Formal Rules

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

Expr ::= n | Expr + Expr

We can write:

n1 + n2 → n3      (where n3 = n1 + n2)

Evaluation trace:

(1 + 2) + 3 → 3 + 3 → 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

• Free Monad: Encodes operational rules as an AST of instructions.
• CPS: Makes control flow explicit by turning "rest of the program" into a continuation.
• Defunctionalization: Turns continuations into explicit state transitions, directly resembling operational semantics.
• Dependent Types: Can enrich operational rules with proofs (e.g., stack safety, gas bounds).

In Practice

Operational semantics is how interpreters are built:

• The EVM can be viewed as a large-step state transition system.
• Small-step rules directly resemble match arms in a Rust interpreter.

(n1 + n2) → n3

can be read as Rust code:

#![allow(unused)]
fn main() {
match expr {
    Add(Box::new(Num(n1)), Box::new(Num(n2))) => Num(n1 + n2),
    _ => expr,
}
}

To think about

Thinking about programming in operational ways or using an imperative style—even with a proof—does not enable us to gain deep insights

Operational thinking (implementation first) prevent us to express and improve ideas