L6) SOS for Dummies

understanding structural operational semantics

How to precisely describe what a program does, step by step, without ambiguity? Structural Operational Semantics (SOS) answers this question with a mathematical elegance that revolutionized the definition of programming languages.

Where does SOS fit in?

In L5, we saw three ways to give meaning to a program:

Operational: “how it executes” ← this is the subject of this article
Denotational: “what mathematical function it computes”
Axiomatic: “what properties it guarantees”

SOS (Structural Operational Semantics) is the most widespread formalism of operational semantics. Invented by Gordon Plotkin in 1981, it has become the de facto standard for defining programming languages. Other approaches exist within operational semantics (Kahn’s natural semantics, abstract machines), but SOS dominates due to its systematicity. It uses the L4 (AST, Abstract Syntax Tree) as a starting structure and defines rules to transform it step by step.

Why is it important?

When writing an interpreter or a compiler, a precise specification of the language’s behavior is needed. “The if instruction executes the block if the condition is true” — this is vague. What does “true” mean? What exactly happens? In what order?

SOS provides a rigorous framework to answer these questions. It describes execution as a series of transitions between configurations, governed by inference rules.

For the BP2SC project (BP3 to SuperCollider transpiler, see B7), SOS is particularly relevant: BP3 (Bol Processor 3, see I2) is a grammar language with five execution modes — ORD (ordered), RND (weighted random), LIN (linear), SUB (complete substitution), SUB1 (single substitution) —, conditional flags, and stochastic weights (probabilities associated with rules). Specifying all of this in prose would be a nightmare. With SOS, each behavior becomes a formal, testable, and unambiguous rule.

The idea in one sentence

SOS describes the execution of a program as a sequence of transitions between configurations, where each transition is justified by an inference rule.

The three ingredients of SOS

1. Configurations

A configuration captures the complete state of the program at a given moment. It typically contains:

The expression (or instruction) currently being evaluated
The environment (variable-value bindings)
The memory (state of mutable variables)
Optionally: time, inputs/outputs, etc.

Standard notation:

⟨e, σ⟩

⟨ and ⟩: mathematical angle brackets delimiting a tuple (an ordered group of elements)
e: the expression to be evaluated
σ (sigma, lowercase Greek letter): the state (environment + memory)

Concrete example:

⟨x + 1, {x ↦ 5}⟩

Full reading: “evaluate the expression x + 1 in a state where x is 5″.

Decoding the notation {x ↦ 5}:

The curly braces {...} represent a set or a dictionary

The arrow ↦ (read “is associated with” or “maps to”) indicates a correspondence

{x ↦ 5} means “a state where variable x is associated with the value 5”

A more complex state: {x ↦ 5, y ↦ 10, counter ↦ 0}

2. Transitions

A transition represents an execution step: moving from one configuration to another.

Notation:

⟨e, σ⟩ ⟹ ⟨e', σ'⟩

Symbol-by-symbol decoding:

⟨e, σ⟩: initial configuration (expression e in state σ)

⟹: transition arrow (read “transforms into” or “reduces to”)

⟨e', σ'⟩: resulting configuration

The prime (apostrophe ') indicates “the new value after transformation”

e' (read “e prime”) = new expression

σ' (read “sigma prime”) = new state

Full reading: “the configuration (expression e, state sigma) reduces in one step to (expression e prime, state sigma prime)”.

Two transition styles:

Style	Notation	Meaning
Small-step	`⟨e, σ⟩ → ⟨e', σ'⟩`	A single execution step
Big-step	`⟨e, σ⟩ ⇓ v`	Complete evaluation to a value

Analogy: cooking recipe

Small-step: like following a recipe instruction by instruction. “Break the eggs” → “beat” → “add flour” → … → final dish. You see each step.

Big-step: like directly saying “this recipe yields a chocolate cake”. You only see the final result, not the intermediate steps.

The arrow ⇓ (read “evaluates to” or “yields”) indicates a complete evaluation, while → indicates a single micro-step.

Small-step is more detailed (you see each micro-step), big-step is more compact (you jump directly to the result).

3. Inference rules

An inference rule has the form:

    premise₁    premise₂    ...
    ─────────────────────────────── (RuleName)
              conclusion

It reads: “if all premises are true, then the conclusion is true”.

Anatomy of an inference rule:

Horizontal line: separates the hypotheses (above) from the conclusion (below). It represents the logical implication “if… then…”.

Premises (above): conditions that must be satisfied to apply the rule. Multiple premises are implicitly linked by “and”.

Conclusion (below): what can be affirmed if all premises are true.

(RuleName): label allowing this rule to be referenced.

Indices (₁, ₂): typographical indices to distinguish elements. e₁ is read “e one” or “e subscript 1”.

A rule without premises (nothing above the bar) is an axiom: it is always applicable.

Example — Addition:

    ⟨e₁, σ⟩ ⇓ n₁    ⟨e₂, σ⟩ ⇓ n₂
    ───────────────────────────── (Add)
       ⟨e₁ + e₂, σ⟩ ⇓ n₁ + n₂

Complete decoding of this rule:

e₁, e₂: two arbitrary expressions (free variables of the rule)

n₁, n₂: the numerical values resulting from the evaluation

σ: the state (the same for both sub-expressions)

⇓: “evaluates completely to”

The + to the left of ⇓ is the syntactic operator (in the program)

The + to the right of ⇓ is mathematical addition (on numbers)

Reading in English: “If expression e1 evaluates to n1 in state sigma, AND if expression e2 evaluates to n2 in that same state sigma, THEN expression e1 + e2 evaluates to the sum n1 + n2.”

Let’s explain step by step

Example 1: A mini-language of expressions

Let’s define the SOS of an ultra-simple language with numbers, additions, and multiplications.

Syntax:

e ::= n | e + e | e * e

How to read this BNF (Backus-Naur Form) notation:

e: name of the syntactic category (here, “expression”)

::=: “is defined as” or “can be”

|: “or” (alternative separator)

n: a literal number (1, 42, -7…)

e + e: an addition of two expressions

e * e: a multiplication of two expressions

Reading: “An expression (e) is either a number (n), or an addition (e + e), or a multiplication (e * e).”
The definition is recursive: an expression can contain other expressions.

Configurations:

⟨e⟩  (no state, pure expressions)

Rules (big-step):

    ───────── (Num)
    ⟨n⟩ ⇓ n


    ⟨e₁⟩ ⇓ n₁    ⟨e₂⟩ ⇓ n₂
    ─────────────────────── (Add)
       ⟨e₁ + e₂⟩ ⇓ n₁ + n₂


    ⟨e₁⟩ ⇓ n₁    ⟨e₂⟩ ⇓ n₂
    ─────────────────────── (Mul)
       ⟨e₁ * e₂⟩ ⇓ n₁ × n₂

Derivation of (2 + 3) * 4:

        ⟨2⟩ ⇓ 2    ⟨3⟩ ⇓ 3
        ─────────────────── (Add)
           ⟨2 + 3⟩ ⇓ 5            ⟨4⟩ ⇓ 4
        ─────────────────────────────────── (Mul)
                ⟨(2 + 3) * 4⟩ ⇓ 20

We construct a derivation tree: each node is a rule application, the leaves are axioms (rules without premises like (Num)).

Application to BP3

SOS is the ideal tool to formalize BP3’s mechanisms: five execution modes (ORD, RND, LIN, SUB, SUB1), conditional flags, decremental weights. Each behavior becomes a precise, testable, and unambiguous inference rule.

This application is detailed in the B series:

B3 — Derivation Rules — SOS formalization of the five modes
B4 — Flags and Weights — cross-cutting mechanisms (Flag-Cond, Weight-Dec)
B7 — From BP3 to SuperCollider — translation of SOS rules into SuperCollider patterns

Structure of a complete SOS specification

A complete SOS specification for any language comprises five components:

1. Abstract syntax

The language grammar, typically in BNF or EBNF (Extended BNF, see L3):

Program ::= Instruction+
Instruction ::= Assignment | Loop | Conditional
Expression ::= Number | Variable | Expression Op Expression

2. Semantic domains

The mathematical sets used:

Value = Int | Bool | ...
State = Variable → Value

3. Configurations

The complete state of the program at a given moment:

C = ⟨instruction, state⟩
C_final when the instruction is completely evaluated

4. Transition relation

⟹ ⊆ C × C

Decoding: This mathematical notation means:

⟹ is the transition relation (the set of all possible transitions)

⊆ means “is a subset of” or “is included in”

C × C is the Cartesian product of C by itself: the set of all pairs (configuration before, configuration after)

Reading: “The transition relation is a set of pairs of configurations”

5. Inference rules

The rules that define how to move from one configuration to another (like those seen in the examples above).

In practice: To see these five components applied to a concrete language (BP3, a language of musical grammars), consult the B series, starting with B3.

Small-step vs Big-step: which style to choose?

Aspect	Small-step	Big-step
Granularity	A micro-step	Complete evaluation
Non-termination	Detectable (no transition)	Invisible (rule inapplicable)
Concurrency	Natural (interleaving)	Difficult
Implementation	Close to an interpreter	Close to a recursive evaluator

The choice depends on the language:

Small-step is preferable when the language has mutable state, potentially infinite loops, or time advancing between steps.
Big-step is more concise for purely functional languages without side effects.

Properties of SOS rules

Well-designed SOS rules have several important properties:

Determinism (or lack thereof)

Deterministic rule: for a given configuration, at most one rule applies.

Non-deterministic rule: multiple rules can apply (free or probabilistic choice).

A language can mix the two: some constructs are deterministic, others introduce non-determinism (choice, concurrency, stochasticity).

Progress

Progress property: if a configuration is not final, at least one rule applies.

Without this property, a program can “get stuck” in a non-final state — a sign of error in the specification or in the program.

Termination

Question: does the derivation always reach a final configuration?

SOS does not guarantee termination. A recursive definition without a stopping condition loops indefinitely. It is up to the language or program designer to ensure it, for example by introducing counters, termination conditions, or mechanisms like decremental weights (see B4).

Confluence

Confluence property: if multiple derivation paths are possible, they all lead to the same final result.

A non-deterministic language is generally not confluent: two executions can produce different results. Depending on the context, non-confluence can be a desired property (concurrency, stochasticity) or a defect to be corrected.

Key takeaways

Configuration: complete program state (expression + environment + memory).
Transition: an execution step, denoted ⟨e, σ⟩ ⟹ ⟨e', σ'⟩.
Inference rule: “if the premises are true, the conclusion is true”. Premises above, conclusion below.
Compositionality: the behavior of a composite expression depends on the behavior of its sub-expressions.
Small-step vs big-step: two complementary styles — small-step for details, big-step for conciseness.
Key properties: determinism, progress, termination, confluence — to be checked for any SOS specification.

Glossary

Axiom: an inference rule without premises (conclusion always true). Example: ⟨n⟩ ⇓ n is an axiom because a number always evaluates to itself.
Big-step: semantics where a transition (denoted ⇓) completely evaluates an expression to its final value.
BNF (Backus-Naur Form): notation for describing language syntax. e ::= n | e + e means “e is either n, or e + e”.
Concatenation: joining strings end-to-end. Denoted · (middle dot). "abc" · "def" = "abcdef".
Configuration: instantaneous program state, denoted ⟨e, σ⟩. Contains the current expression and the memory state.
Derivation: a proof tree showing how a transition is justified by the rules.
Non-terminal: a symbol that can be rewritten according to the grammar rules. Opposite of terminal.
Premise: a condition required to apply a rule (above the horizontal bar).
Prime: apostrophe (') indicating “the new value”. σ' = “sigma prime” = new state.
Cartesian product: A × B = set of all pairs (a, b) with a in A and b in B.
Inference rule: a logical schema of the form “premises imply conclusion”, separated by a horizontal bar.
Small-step: semantics where each transition (denoted →) represents a single execution step.
SOS: Structural Operational Semantics — a formal framework introduced by Plotkin in 1981 to define programming languages.
Stochastic: that follows a probability distribution. A stochastic system can produce different results with each execution.
Terminal: a symbol that can no longer be rewritten (leaf of the derivation). Example: a number, a language keyword.
Σ (uppercase sigma): summation symbol. Σwᵢ = w₁ + w₂ + … + wₙ.

Prerequisites: L5, L4
Reading time: 12 min
Tags: #SOS #operational-semantics #inference-rules #formalism

Next article: L7 — Denotational Semantics — when a program becomes a mathematical function