Operational Semantics: Execution and Computation Models

Introduction

Operational semantics defines the meaning of a program by specifying how it executes. Rather than assigning abstract mathematical meanings (denotational) or stating properties (axiomatic), operational semantics describes the concrete steps a program takes during execution. This approach is intuitive, directly implementable, and particularly useful for understanding program behavior and proving properties about execution.

This article explores the foundations of operational semantics, including transition systems, evaluation rules, and practical applications.

Historical Context

Operational semantics emerged from work in the 1970s and 1980s, particularly through the contributions of Gordon Plotkin and others. Plotkin’s structural operational semantics (SOS) provided a systematic framework for defining execution rules. This approach has become the standard method for specifying programming language semantics in practice.

Core Concepts

Transition Systems

A transition system models computation as a sequence of state transitions:

Definition: A transition system is a tuple (S, →) where:

• S: A set of states (configurations)
• → ⊆ S × S: A transition relation (s → s’ means we can move from s to s')

Execution: An execution is a sequence of states s₀ → s₁ → s₂ → … where s₀ is an initial state.

Termination: A state s is terminal if there is no s’ such that s → s'.

Configurations

A configuration represents the current state of computation:

Components:

• Current expression/statement being evaluated
• Current environment (variable bindings)
• Current store (memory state)
• Call stack (for function calls)

Example: For evaluating 2 + 3:

Configuration: ⟨2 + 3, σ⟩
where σ is the current state

Evaluation Relations

An evaluation relation specifies how expressions and statements are evaluated:

Notation:

• ⟨e, σ⟩ ⇓ v means “expression e in state σ evaluates to value v”
• ⟨s, σ⟩ → ⟨s’, σ’⟩ means “statement s in state σ transitions to s’ in state σ'”

Structural Operational Semantics (SOS)

Structural Operational Semantics provides a systematic way to define evaluation rules using inference rules.

Inference Rules

Format:

Premise₁  Premise₂  ...  Premiseₙ
─────────────────────────────────
        Conclusion

Interpretation: If all premises are true, then the conclusion is true.

Evaluation Rules for Expressions

Atomic Values:

─────────────────
⟨n, σ⟩ ⇓ n

(A number evaluates to itself)

Variables:

─────────────────
⟨x, σ⟩ ⇓ σ(x)

(A variable evaluates to its value in the state)

Binary Operations:

⟨e₁, σ⟩ ⇓ v₁    ⟨e₂, σ⟩ ⇓ v₂
─────────────────────────────────
⟨e₁ + e₂, σ⟩ ⇓ v₁ + v₂

(Evaluate both operands, then apply the operation)

Conditional:

⟨b, σ⟩ ⇓ true    ⟨e₁, σ⟩ ⇓ v
──────────────────────────────
⟨if b then e₁ else e₂, σ⟩ ⇓ v

⟨b, σ⟩ ⇓ false    ⟨e₂, σ⟩ ⇓ v
───────────────────────────────
⟨if b then e₁ else e₂, σ⟩ ⇓ v

Evaluation Rules for Statements

Skip:

─────────────────
⟨skip, σ⟩ → ⟨σ⟩

(Skip does nothing, returns the state unchanged)

Assignment:

⟨e, σ⟩ ⇓ v
──────────────────────────
⟨x := e, σ⟩ → ⟨σ[x ↦ v]⟩

(Evaluate the expression, update the state)

Sequence:

⟨s₁, σ⟩ → ⟨σ'⟩    ⟨s₂, σ'⟩ → ⟨σ''⟩
──────────────────────────────────────
⟨s₁; s₂, σ⟩ → ⟨σ''⟩

(Execute first statement, then second)

If Statement:

⟨b, σ⟩ ⇓ true    ⟨s₁, σ⟩ → ⟨σ'⟩
──────────────────────────────────
⟨if b then s₁ else s₂, σ⟩ → ⟨σ'⟩

While Loop:

⟨b, σ⟩ ⇓ false
──────────────────────────────────
⟨while b do s, σ⟩ → ⟨σ⟩

⟨b, σ⟩ ⇓ true    ⟨s, σ⟩ → ⟨σ'⟩    ⟨while b do s, σ'⟩ → ⟨σ''⟩
──────────────────────────────────────────────────────────────
⟨while b do s, σ⟩ → ⟨σ''⟩

Evaluation Strategies

Different evaluation strategies lead to different operational semantics:

Eager Evaluation (Strict)

Evaluate arguments before applying functions:

⟨e₁, σ⟩ ⇓ v₁    ⟨e₂, σ⟩ ⇓ v₂
─────────────────────────────────
⟨f(e₁, e₂), σ⟩ ⇓ ⟦f⟧(v₁, v₂)

Characteristics:

• All arguments evaluated
• Predictable performance
• May evaluate unnecessary expressions

Lazy Evaluation

Delay evaluation until needed:

⟨e₁, σ⟩ ⇓ λx. e    ⟨e₂, σ⟩ ⇓ v₂    ⟨e[x ↦ v₂], σ⟩ ⇓ v
──────────────────────────────────────────────────────────
⟨e₁(e₂), σ⟩ ⇓ v

Characteristics:

• Arguments passed unevaluated
• Avoids unnecessary computation
• More complex to reason about

Call-by-Value vs Call-by-Name

Call-by-Value: Evaluate arguments, pass values

⟨e₁, σ⟩ ⇓ λx. e    ⟨e₂, σ⟩ ⇓ v
──────────────────────────────────
⟨e₁(e₂), σ⟩ ⇓ ⟨e[x ↦ v], σ⟩

Call-by-Name: Pass unevaluated expressions

⟨e₁, σ⟩ ⇓ λx. e
──────────────────────────────────
⟨e₁(e₂), σ⟩ ⇓ ⟨e[x ↦ e₂], σ⟩

Big-Step vs Small-Step Semantics

Big-Step Semantics (Natural Semantics)

Describes complete evaluation from start to finish:

Notation: ⟨e, σ⟩ ⇓ v (e evaluates to v in one big step)

Advantages:

• Concise and intuitive
• Directly implementable as interpreter
• Easier to reason about termination

Disadvantage:

• Difficult to express non-terminating computations
• Hard to reason about intermediate states

Small-Step Semantics (Structural Operational Semantics)

Describes individual computation steps:

Notation: ⟨e, σ⟩ → ⟨e’, σ’⟩ (one step of computation)

Advantages:

• Handles non-termination naturally
• Captures intermediate states
• Useful for debugging and analysis

Disadvantage:

• More verbose
• Requires multiple steps for complete evaluation

Relationship: Big-step evaluation is the transitive closure of small-step:

⟨e, σ⟩ ⇓ v iff ⟨e, σ⟩ →* ⟨v, σ'⟩

Practical Example: Simple Imperative Language

Language:

e ::= n | x | e₁ + e₂ | e₁ * e₂
b ::= true | false | e₁ = e₂ | e₁ < e₂ | ¬b | b₁ ∧ b₂
s ::= skip | x := e | s₁; s₂ | if b then s₁ else s₂ | while b do s

Small-Step Semantics:

Arithmetic:
⟨n, σ⟩ → n
⟨x, σ⟩ → σ(x)
⟨e₁ + e₂, σ⟩ → ⟨e₁', σ⟩ + e₂  if ⟨e₁, σ⟩ → ⟨e₁', σ⟩
⟨v₁ + e₂, σ⟩ → ⟨v₁ + e₂', σ⟩  if ⟨e₂, σ⟩ → ⟨e₂', σ⟩
⟨v₁ + v₂, σ⟩ → v₁ + v₂

Statements:
⟨skip, σ⟩ → σ
⟨x := e, σ⟩ → σ[x ↦ v]  if ⟨e, σ⟩ →* v
⟨s₁; s₂, σ⟩ → ⟨s₁', σ'⟩; s₂  if ⟨s₁, σ⟩ → ⟨s₁', σ'⟩
⟨skip; s₂, σ⟩ → ⟨s₂, σ⟩

Applications

Language Implementation

Operational semantics directly guides interpreter implementation:

def eval_expr(e, state):
    if isinstance(e, int):
        return e
    elif isinstance(e, str):  # variable
        return state[e]
    elif e[0] == '+':
        return eval_expr(e[1], state) + eval_expr(e[2], state)
    # ... more cases

Program Verification

Prove properties about program execution:

Example: Prove that x := 5; y := x + 1 results in y = 6

⟨x := 5; y := x + 1, σ⟩ 
→ ⟨y := x + 1, σ[x ↦ 5]⟩
→ σ[x ↦ 5, y ↦ 6]

Equivalence Checking

Prove two programs are equivalent:

Example: x := 5; y := x ≡ x := 5; y := 5

Both evaluate to the same final state.

Debugging and Tracing

Small-step semantics enables step-by-step execution:

• Debuggers use small-step semantics
• Trace execution for analysis
• Identify where errors occur

Advanced Topics

Concurrency

For concurrent programs, extend transition systems:

⟨s₁, σ⟩ → ⟨s₁', σ'⟩
──────────────────────────────
⟨s₁ ∥ s₂, σ⟩ → ⟨s₁' ∥ s₂, σ'⟩

(Either process can take a step)

Exception Handling

Add exception states:

⟨e, σ⟩ → exception
──────────────────────────────
⟨try e catch h, σ⟩ → ⟨h, σ⟩

Non-Determinism

Allow multiple possible transitions:

⟨e, σ⟩ → ⟨e₁', σ'⟩  or  ⟨e, σ⟩ → ⟨e₂', σ'⟩

Glossary

Big-Step Semantics: Evaluation relation describing complete computation from start to finish

Configuration: The current state of computation (expression, environment, store)

Evaluation Relation: A relation specifying how expressions and statements are evaluated

Inference Rule: A rule with premises and conclusion used to define evaluation

Operational Semantics: Defining meaning through execution steps

Small-Step Semantics: Transition relation describing individual computation steps

State: An assignment of values to variables

Structural Operational Semantics (SOS): Systematic framework for defining evaluation rules

Terminal State: A state with no outgoing transitions

Transition System: A set of states with a transition relation

Practice Problems

Problem 1: Define small-step semantics for 2 + 3 * 4 and show the evaluation steps.

Solution:

⟨2 + 3 * 4, σ⟩ 
→ ⟨2 + 12, σ⟩  (evaluate 3 * 4)
→ ⟨14, σ⟩      (evaluate 2 + 12)

Problem 2: Write operational semantics rules for a repeat-until loop: repeat s until b.

Solution:

⟨s, σ⟩ → ⟨σ'⟩    ⟨b, σ'⟩ ⇓ false    ⟨repeat s until b, σ'⟩ → ⟨σ''⟩
──────────────────────────────────────────────────────────────────
⟨repeat s until b, σ⟩ → ⟨σ''⟩

⟨s, σ⟩ → ⟨σ'⟩    ⟨b, σ'⟩ ⇓ true
──────────────────────────────────
⟨repeat s until b, σ⟩ → ⟨σ'⟩

Problem 3: Prove that while false do s is equivalent to skip.

Solution:

⟨while false do s, σ⟩ → ⟨σ⟩  (by while rule with false condition)
⟨skip, σ⟩ → ⟨σ⟩
Both evaluate to the same state, so they're equivalent.

Related Resources

• Operational Semantics: https://en.wikipedia.org/wiki/Operational_semantics
• Structural Operational Semantics: https://en.wikipedia.org/wiki/Structural_operational_semantics
• Semantics of Programming Languages: “Semantics of Programming Languages” by Carl Gunter
• Formal Semantics: https://plato.stanford.edu/entries/formal-semantics/
• Programming Language Semantics: https://en.wikipedia.org/wiki/Semantics_(computer_science)
• Transition Systems: https://en.wikipedia.org/wiki/Transition_system
• Evaluation Strategy: https://en.wikipedia.org/wiki/Evaluation_strategy
• Call-by-Value vs Call-by-Name: https://en.wikipedia.org/wiki/Evaluation_strategy
• Formal Methods: https://plato.stanford.edu/entries/formal-methods/
• Program Verification: https://en.wikipedia.org/wiki/Program_verification
• Compiler Design: https://en.wikipedia.org/wiki/Compiler
• Interpreter Pattern: https://en.wikipedia.org/wiki/Interpreter_pattern
• Abstract Syntax Tree: https://en.wikipedia.org/wiki/Abstract_syntax_tree
• Type Systems: https://plato.stanford.edu/entries/type-theory/
• Lambda Calculus: https://plato.stanford.edu/entries/lambda-calculus/

Conclusion

Operational semantics provides a concrete, intuitive way to specify and reason about program execution. By defining evaluation rules that describe how programs compute step-by-step, operational semantics bridges the gap between informal program understanding and formal mathematical reasoning.

The flexibility of operational semantics—supporting both big-step and small-step approaches, handling various evaluation strategies, and extending to concurrent and exceptional programs—makes it the most widely used approach for specifying programming language semantics in practice.

Understanding operational semantics is essential for language designers, compiler developers, and anyone involved in formal verification. It provides the foundation for implementing interpreters, proving program properties, and understanding the precise behavior of programming languages.