h t t p s : / / h o m e p a g e s . i n f . e d . a c . u k / g d p / p u b l i c a t i o n s / O r i g i n s _ S O S . p d f

Ingest: The Origins of Structural Operational Semantics

Type: types/ingest-report.md

Classification

This is a first-person historical retrospective by the method's originator. It accompanied the 2004 journal publication of his 1981 Aarhus lecture notes on SOS. It reports what he built, what influenced him, what worked and what did not: recursion was "clumsy", the PASCAL lecture "did not get very far", and static semantics "went very smoothly". It has no experiments or new formal results. It is closer to a practitioner report than to a scientific paper or a conceptual essay. The author says it is a reconstruction "based on (possibly faulty) memory". Author: Gordon D. Plotkin (Edinburgh, LFCS), the originator of Structural Operational Semantics and of PCF. He is a primary witness, and an interested one.

Summary

Plotkin traces Structural Operational Semantics (SOS) to his dissatisfaction with abstract interpreting machines. He names the Vienna school's VDL machine for PL/I and Landin's SECD machine. The machines' "grand state" buried semantic ideas in tree-traversal detail, so he concluded that such machines "do not scale up well when used as a human-oriented method of specification for real languages". Rule systems were the alternative, drawing on Smullyan's formal systems and Barendregt's rule-based axiomatisation of λ-calculus reduction. Rule-based operational semantics then grew through PCF, Milner's SIL teaching rules and his labelled-transition semantics for CCS, and work on parallelism and nondeterminism. Plotkin's turning point was a realisation: papers proved denotational semantics adequate relative to an operational semantics that was already simple and elementary. So operational semantics could be taken "seriously as a specification method" in its own right. The 1981 Aarhus lectures rest on two ideas. First, SOS is like an abstract machine with only the configuration content needed to explain the semantics. The rules make syntactic exploration "implicit rather than drearily explicit", while machines remain important for implementation. Second, the rules are syntax-directed: behaviour is defined structurally (primitive-recursively in the syntax), not compositionally as in denotational semantics. The account also records several points of context. Scott asked "what is operational about it?", and the term came from the Scott–Strachey denotational/operational distinction. Kahn's big-step "natural semantics" in TYPOL executed rules as Horn clauses in Prolog. The notes deliberately had no theoretical framework ("a theory could come later: once we had the data!"). Plotkin also proposes an unpublished diagrammatic rule notation that shows the flow of control directly.

Quotes

The operational semantics of PCF is given by a system of rules for a relation which one would now view as a smallstep call-by-name transition relation; the connection to a variant call-by-name SECD machine is mentioned but not given. --- kb/sources/.snapshots/plotkin-origins-of-sos.md @ sha256:03d678b27f5e834bfc020379b8f4dea7efcdc135ea55172a488768b92958082d — PCF discussion

Connections Found

The source's main role is term anchor and boundary marker. At ingestion, the KB used "unique operational semantics" as its symbolic-form criterion in representational form, inviting confusion with the programming-language (PL) sense. This historical use is not Plotkin's definition. Plotkin's operational semantics is a mathematical rule system that specifies a transition relation, and it is distinct from any implementation. That earlier KB criterion was broader: fixed rules "implemented by a parser, interpreter, runtime, schema, validator", with formal semantics "sufficient but not necessary". These two notions compare on the axis of what fixes an artifact's consequences, and they should not be read into each other. Scott's question shows that the boundary of "operational" was contested from the start. The same caution applies to operationalism. That ingest compares with this one on the axis of what "operational" names. In Bridgman's sense, operations fix the meaning of an empirical concept by a measurement procedure. In Plotkin's sense, rules fix a program's meaning by a transition relation over syntax. Neither means making knowledge usable for a defined task and executor. At most, SOS is the limiting case where the executor is a formal transition system and the task is fully specified.

The source is evidence for the lineage paragraph of any symbolic program with LLM calls is a select/call program, and it also sharpens that paragraph. The note says small-step operational semantics "represents execution as transitions over machine configurations" and that abstract-machine compilation reifies control state. Plotkin separates these two lines. SOS does use configurations (for example, statement-plus-state pairs), but it keeps them minimal and leaves control implicit in syntax-directed rules. Abstract machines reify control in large configurations, and Plotkin keeps them for implementation. The lemma's explicit control state follows the abstract-machine and defunctionalization line, not SOS proper. "Machine configurations" is therefore the wrong description of SOS.

The source compares with statecharts and programs differ in what they show, not in what they can compute on the axis of which structure a representation shows natively. SECD/VDL machines and SOS rules specify the same languages. Plotkin chose between them by what a human reader must reconstruct, not by expressive power. His diagrammatic notation goes one step further and shows the flow of control "rather than having to compute it by looking at the rules". This is an independent, earlier instance of that note's thesis from language semantics.

The source is moderate evidence for prompting changes failure diagnosis with the semantic reference: there, formal semantics is a plausible ideal for programming languages even when practice falls short. SOS made rule-based specification teachable and robust across "a very wide range of language constructs". Yet the real-language attempt stalled at PASCAL blocks, and the notes were never revised for publication.

Extractable Value

  1. Operational semantics is a specification of a transition relation, not execution by an executor -- this separates three things: having a precise operational meaning (SOS rules), having an implementation that executes it (abstract machines, TYPOL's Prolog interpretation), and operationalizing knowledge for a task and executor. Plotkin keeps the first two apart even when the rules are executable. This gives a precedent for not equating "operational" with "executed" or "automated". [quick-win]
  2. Executable specification is a separate move from specification -- TYPOL showed that rules read as Horn clauses yield an interpreter "for free". Efficient execution remained an open question, separate from the specification. This is a clean data point for distinguishing specification from executability: a fully formal artifact becomes executable only when a consumer is attached, and that consumer's efficiency is a further problem. [quick-win]
  3. Correct the select/call lemma's lineage sentence -- SOS uses minimal configurations and implicit control. Reified control in large configurations is the abstract-machine and defunctionalization line. The lemma uses the latter, so the sentence should attribute the explicit K there and cite this source for the contrast. [quick-win]
  4. Representation choice by reader burden at equal semantic content -- the rejection of machines rests on human-oriented specification (machine states "too big", detail "burying essential semantical ideas"), not on capability. Machines are kept for implementation. This is a historical precedent for the statecharts note, and possibly a scope sentence for it: explicit state is chosen for analysis and implementation, implicit control for human specification. [experiment]
  5. Anchor for the KB's "unique operational semantics" criterion -- the KB's earlier symbolic-form criterion borrowed the PL term. This source fixes its origin (Scott–Strachey) and its original scope (a mathematical specification method). It marks where that implementation-anchored sense departed from the PL sense. [just-a-reference]
  6. Structural, not compositional -- SOS behaviour is defined by structural recursion over syntax but is not a function of the parts' meanings. This distinction could matter wherever the KB argues about whether an instruction's meaning composes from its parts. No current note needs it. [just-a-reference]

Limitations (our opinion)

This is a single participant's reconstruction, written about 23 years after the events by the person whose method won. Its account of why abstract machines failed as specifications is a retrospective rationale. The VDL group's own "small state" work, which Plotkin admits he learned of only while writing, shows that the machine line was also reducing configuration size. So the decisive difference may be the use of rules, as Plotkin himself says, rather than machines as such. The scaling claim ("do not scale up well ... for real languages") is not tested against SOS. By the author's own report, the SOS treatment of PASCAL also "did not get very far", and recursion was clumsy. So the source does not show that rules scale to full real languages; later work (for example, the Definition of Standard ML) would be needed for that, and this ingest does not establish it. The text is a pdftotext capture. Rule layouts and the diagrammatic notation are garbled, so claims about the diagrams' exact form need the original PDF rather than this text extraction. The source says nothing about automation, executors in the human-factors sense, or decision autonomy. Its bearing is limited to disambiguating "operational" and to the specification/execution split.

Use this source to check the lineage sentence in the select/call program note: distinguish syntax-directed transition rules from the abstract-machine line that makes control state explicit.