Operational Semantics
Operational semantics defines a program's meaning by specifying how it executes, using inference rules that describe the steps of computation.
Definition
Operational semantics specifies the meaning of a program as the sequence of computation steps it performs, given by inductively defined transition relations over program configurations.
Scope
This topic covers small-step (structural) and big-step (natural) operational semantics, in which transition or evaluation relations defined by syntax-directed inference rules describe how programs compute. It addresses reduction strategies, abstract machines, and how operational definitions support proofs of type soundness and program equivalence.
Core questions
- How do inference rules capture the steps of a computation?
- What is the difference between small-step and big-step semantics?
- How does operational semantics support soundness and equivalence proofs?
- How do abstract machines relate to rule-based operational definitions?
Key theories
- Structural operational semantics
- Plotkin defines execution by small-step transition rules structured by the syntax of the language, giving a compositional, syntax-directed account of how each construct computes.
- Natural (big-step) semantics
- Kahn's natural semantics relates a program directly to its final result through evaluation rules, abstracting away intermediate steps and easing certain proofs.
Clinical relevance
Operational semantics is the standard tool for specifying real language behavior and proving compilers and interpreters correct. Its rule-based style maps closely to implementations and underlies machine-checked language metatheory.
History
Operational ideas appeared in early interpreter-based definitions of languages. Plotkin's 1981 Aarhus notes established structural operational semantics as a rigorous, syntax-directed framework, and Kahn's 1987 natural semantics offered a big-step alternative. Together they became the dominant approach for defining and reasoning about programming languages.
Debates
- Small-step versus big-step formulations
- Semanticists choose between small-step semantics, which expose intermediate states and handle non-termination and concurrency naturally, and big-step semantics, which are concise but less suited to diverging or interleaved computation.
Key figures
- Gordon Plotkin
- Gilles Kahn
- Glynn Winskel
- Matthias Felleisen
Related topics
Seminal works
- plotkin1981
- kahn1987
- winskel1993
Frequently asked questions
- What is the difference between small-step and big-step semantics?
- Small-step semantics describes individual computation steps and the intermediate states between them, while big-step semantics relates a program directly to its final value, hiding the steps in between.
- Why is operational semantics useful for proving soundness?
- Because it makes the steps of execution explicit, it pairs naturally with the progress-and-preservation method, which reasons about how typing is maintained as a program takes each step.