Operational semantics is a category offormal programming languagesemantics in which certain desired properties of aprogram, such as correctness, safety or security, areverified by constructingproofs from logical statements about itsexecution and procedures, rather than by attaching mathematical meanings to its terms (denotational semantics). Operational semantics are classified in two categories:structural operational semantics (orsmall-step semantics) formally describe how theindividual steps of acomputation take place in a computer-based system; by oppositionnatural semantics (orbig-step semantics) describe how theoverall results of the executions are obtained. Other approaches to providing aformal semantics of programming languages includeaxiomatic semantics anddenotational semantics.

The operational semantics for aprogramming language describes how a valid program is interpreted as sequences of computational steps. These sequences thenare the meaning of the program. In the context offunctional programming, the final step in a terminating sequence returns the value of the program. (In general there can be many return values for a single program, because the program could benondeterministic, and even for a deterministic program there can be many computation sequences since the semantics may not specify exactly what sequence of operations arrives at that value.)

Perhaps the first formal incarnation of operational semantics was the use of thelambda calculus to define the semantics ofLisp.^[1]Abstract machines in the tradition of theSECD machine are also closely related.

The concept of operational semantics was used for the first time in defining the semantics ofAlgol 68.The following statement is a quote from the revised ALGOL 68 report:

The meaning of a program in the strict language is explained in terms of a hypothetical computerwhich performs the set of actions that constitute the elaboration of that program. (Algol68, Section 2)

The first use of the term "operational semantics" in its present meaning is attributed toDana Scott (Plotkin04).What follows is a quote from Scott's seminal paper on formal semantics,in which he mentions the "operational" aspects of semantics.

It is all very well to aim for a more ‘abstract’ and a ‘cleaner’ approach tosemantics, but if the plan is to be any good, the operational aspects cannotbe completely ignored. (Scott70)

Gordon Plotkin introduced the structural operational semantics,Matthias Felleisen and Robert Hieb the reduction semantics,^[2] andGilles Kahn the natural semantics.

Structural operational semantics (SOS, also calledstructured operational semantics orsmall-step semantics) was introduced byGordon Plotkin in (Plotkin81) as a logical means to define operational semantics. The basic idea behind SOS is to define the behavior of a program in terms of the behavior of its parts, thus providing a structural, i.e., syntax-oriented andinductive, view on operational semantics. An SOS specification defines the behavior of a program in terms of a (set of)transition relation(s). SOS specifications take the form of a set ofinference rules that define the valid transitions of a composite piece of syntax in terms of the transitions of its components.

For a simple example, we consider part of the semantics of a simple programming language; proper illustrations are given inPlotkin81 andHennessy90, and other textbooks. Let${\displaystyle C_1,C_2}$ range over programs of the language, and let${\displaystyle s}$ range over states (e.g. functions from memory locations to values). If we have expressions (ranged over by${\displaystyle E}$), values(${\displaystyle V}$) and locations (${\displaystyle L}$), then a memory update command would have semantics:

${\displaystyle \frac{⟨E,s⟩\Rightarrow V}{⟨L:=E,s⟩⟶(s\uplus (L\mapsto V))}}$

Informally, the rule says that "if the expression${\displaystyle E}$ in state${\displaystyle s}$ reduces to value${\displaystyle V}$,then the program${\displaystyle L:=E}$ will update the state${\displaystyle s}$ with the assignment${\displaystyle L=V}$".

The semantics of sequencing can be given by the following three rules:

1.${\displaystyle \frac{⟨C_1,s⟩⟶s^{\prime }}{⟨C_1;C_2,s⟩⟶⟨C_2,s^{\prime }⟩}}$

2.${\displaystyle \frac{⟨C_1,s⟩⟶⟨C_1^{\prime },s^{\prime }⟩}{⟨C_1;C_2,s⟩⟶⟨C_1^{\prime };C_2,s^{\prime }⟩}}$

3.${\displaystyle \frac{}{⟨\mathbf{s}\mathbf{k}\mathbf{i}\mathbf{p},s⟩⟶s}}$

Informally, the first rule says that,if program${\displaystyle C_1}$ in state${\displaystyle s}$ finishes in state${\displaystyle s^{\prime }}$, then the program${\displaystyle C_1;C_2}$ in state${\displaystyle s}$ will reduce to the program${\displaystyle C_2}$ in state${\displaystyle s^{\prime }}$.(You can think of this as formalizing "You can run${\displaystyle C_1}$, and then run${\displaystyle C_2}$using the resulting memory store.)The second rule says thatif the program${\displaystyle C_1}$ in state${\displaystyle s}$ can reduce to the program${\displaystyle C_1^{\prime }}$ with state${\displaystyle s^{\prime }}$, then the program${\displaystyle C_1;C_2}$ in state${\displaystyle s}$ will reduce to the program${\displaystyle C_1^{\prime };C_2}$ in state${\displaystyle s^{\prime }}$.(You can think of this as formalizing the principle for an optimizing compiler:"You are allowed to transform${\displaystyle C_1}$ as if it were stand-alone, even if it is just thefirst part of a program.")The semantics is structural, because the meaning of the sequential program${\displaystyle C_1;C_2}$, is defined by the meaning of${\displaystyle C_1}$ and the meaning of${\displaystyle C_2}$.

If we also have Boolean expressions over the state, ranged over by${\displaystyle B}$, then we can define the semantics of thewhile command:${\displaystyle \frac{⟨B,s⟩\Rightarrow \mathbf{t}\mathbf{r}\mathbf{u}\mathbf{e}}{⟨\mathbf{w}\mathbf{h}\mathbf{i}\mathbf{l}\mathbf{e}B\mathbf{d}\mathbf{o}C,s⟩⟶⟨C;\mathbf{w}\mathbf{h}\mathbf{i}\mathbf{l}\mathbf{e}B\mathbf{d}\mathbf{o}C,s⟩}\frac{⟨B,s⟩\Rightarrow \mathbf{f}\mathbf{a}\mathbf{l}\mathbf{s}\mathbf{e}}{⟨\mathbf{w}\mathbf{h}\mathbf{i}\mathbf{l}\mathbf{e}B\mathbf{d}\mathbf{o}C,s⟩⟶s}}$

Such a definition allows formal analysis of the behavior of programs, permitting the study ofrelations between programs. Important relations includesimulation preorders andbisimulation.These are especially useful in the context ofconcurrency theory.

Thanks to its intuitive look and easy-to-follow structure,SOS has gained great popularity and has become a de facto standard in definingoperational semantics. As a sign of success, the original report (so-called Aarhusreport) on SOS (Plotkin81) has attracted more than 1000 citations according to the CiteSeer[1],making it one of the most cited technical reports inComputer Science.

Reduction semantics is an alternative presentation of operational semantics. Its key ideas were first applied to purely functionalcall by name andcall by value variants of thelambda calculus byGordon Plotkin in 1975^[3] and generalized to higher-order functional languages with imperative features byMatthias Felleisen in his 1987 dissertation.^[4] The method was further elaborated by Matthias Felleisen and Robert Hieb in 1992 into a fullyequational theory forcontrol andstate.^[2] The phrase “reduction semantics” itself was first coined by Felleisen andDaniel P. Friedman in a PARLE 1987 paper.^[5]

Reduction semantics are given as a set ofreduction rules that each specify a single potential reduction step. For example, the following reduction rule states that an assignment statement can be reduced if it sits immediately beside its variable declaration:

${\displaystyle \mathbf{l}\mathbf{e}\mathbf{t}\mathbf{r}\mathbf{e}\mathbf{c}x=v_1\mathbf{i}\mathbf{n}x\leftarrow v_2;e⟶\mathbf{l}\mathbf{e}\mathbf{t}\mathbf{r}\mathbf{e}\mathbf{c}x=v_2\mathbf{i}\mathbf{n}e}$

To get an assignment statement into such a position it is “bubbled up” through function applications and the right-hand side of assignment statements until it reaches the proper point. Since intervening${\displaystyle \mathbf{l}\mathbf{e}\mathbf{t}}$ expressions may declare distinct variables, the calculus also demands an extrusion rule for${\displaystyle \mathbf{l}\mathbf{e}\mathbf{t}}$ expressions. Most published uses of reduction semantics define such “bubble rules” with the convenience of evaluation contexts. For example, the grammar of evaluation contexts in a simplecall by value language can be given as

${\displaystyle E::=[]|vE|Ee|x\leftarrow E|\mathbf{l}\mathbf{e}\mathbf{t}\mathbf{r}\mathbf{e}\mathbf{c}x=v\mathbf{i}\mathbf{n}E|E;e}$

where${\displaystyle e}$ denotes arbitrary expressions and${\displaystyle v}$ denotes fully-reduced values. Each evaluation context includes exactly one hole${\displaystyle []}$ into which a term is plugged in a capturing fashion. The shape of the context indicates with this hole where reduction may occur. To describe “bubbling” with the aid of evaluation contexts, a single axiom suffices:

${\displaystyle E[x\leftarrow v;e]⟶x\leftarrow v;E[e]\text{(lift assignments)}}$

This single reduction rule is the lift rule from Felleisen and Hieb's lambda calculus for assignment statements. The evaluation contexts restrict this rule to certain terms, but it is freely applicable in any term, including under lambdas.

Following Plotkin, showing the usefulness of a calculus derived from a set of reduction rules demands (1) a Church-Rosser lemma for the single-step relation, which induces an evaluation function, and (2) a Curry-Feys standardization lemma for the transitive-reflexive closure of the single-step relation, which replaces the non-deterministic search in the evaluation function with a deterministic left-most/outermost search. Felleisen showed that imperative extensions of this calculus satisfy these theorems. Consequences of these theorems are that the equational theory—the symmetric-transitive-reflexive closure—is a sound reasoning principle for these languages. However, in practice, most applications of reduction semantics dispense with the calculus and use the standard reduction only (and the evaluator that can be derived from it).

Reduction semantics are particularly useful given the ease by which evaluation contexts can model state or unusual control constructs (e.g.,first-class continuations). In addition, reduction semantics have been used to modelobject-oriented languages,^[6]contract systems, exceptions, futures, call-by-need, and many other language features. A thorough, modern treatment of reduction semantics that discusses several such applications at length is given by Matthias Felleisen, Robert Bruce Findler and Matthew Flatt inSemantics Engineering with PLT Redex.^[7]

Big-step structural operational semantics is also known under the namesnatural semantics,relational semantics andevaluation semantics.^[8] Big-step operational semantics was introduced under the namenatural semantics byGilles Kahn when presenting Mini-ML, a pure dialect ofML.

One can view big-step definitions as definitions of functions, or more generally of relations, interpreting each language construct in an appropriate domain. Its intuitiveness makes it a popular choice for semantics specification in programming languages, but it has some drawbacks that make it inconvenient or impossible to use in many situations, such as languages with control-intensive features or concurrency.^[9]

A big-step semantics describes in a divide-and-conquer manner how final evaluation results of language constructs can be obtained by combining the evaluation results of their syntactic counterparts (subexpressions, substatements, etc.).

There are a number of distinctions between small-step and big-step semantics that influence whether one or the other forms a more suitable basis for specifying the semantics of a programming language.

Big-step semantics have the advantage of often being simpler (needing fewer inference rules) and often directly correspond to an efficient implementation of an interpreter for the language (hence Kahn calling them "natural".) Both can lead to simpler proofs, for example when proving the preservation of correctness under someprogram transformation.^[10]

The main disadvantage of big-step semantics is that non-terminating (diverging) computations do not have an inference tree, making it impossible to state and prove properties about such computations.^[10]

Small-step semantics give more control over the details and order of evaluation. In the case of instrumented operational semantics, this allows the operational semantics to track and the semanticist to state and prove more accurate theorems about the run-time behaviour of the language. These properties make small-step semantics more convenient when provingtype soundness of a type system against an operational semantics.^[10]

• Algebraic semantics
• Axiomatic semantics
• Denotational semantics
• Formal semantics of programming languages

• Gilles Kahn. "Natural Semantics".Proceedings of the 4th Annual Symposium on Theoretical Aspects of Computer Science. Springer-Verlag. London. 1987.
• Gordon D. Plotkin.A Structural Approach to Operational Semantics. (1981) Tech. Rep. DAIMI FN-19, Computer Science Department, Aarhus University, Aarhus, Denmark. (Reprinted with corrections in J. Log. Algebr. Program. 60-61: 17-139 (2004), (preprint).
• Gordon D. Plotkin. The Origins of Structural Operational Semantics. J. Log. Algebr. Program. 60-61:3-15, 2004. (preprint).
• Dana S. Scott. Outline of a Mathematical Theory of Computation, Programming Research Group, Technical Monograph PRG–2, Oxford University, 1970.
• Adriaan van Wijngaarden et al. Revised Report on the Algorithmic LanguageALGOL 68. IFIP. 1968.[2]
• Matthew Hennessy. Semantics of Programming Languages. Wiley, 1990.available online.

• Media related toOperational semantics at Wikimedia Commons

• Operational semantics
• Formal specification languages
• Logic in computer science
• Programming language semantics

• Articles with short description
• Short description matches Wikidata
• Commons category link from Wikidata