Operational semantics


Operational semantics is a category of formal programming language semantics in which certain desired properties of a program, such as correctness, safety or security, are verified by constructing proofs from logical statements about its execution and procedures, rather than by attaching mathematical meanings to its terms. Operational semantics are classified in two categories: structural operational semantics formally describe how the individual steps of a computation take place in a computer-based system; by opposition natural semantics describe how the overall results of the executions are obtained. Other approaches to providing a formal semantics of programming languages include axiomatic semantics and denotational semantics.
The operational semantics for a programming language describes how a valid program is interpreted as sequences of computational steps.
These sequences then are the meaning of the program.
In the context of functional programs, the final step in a terminating
sequence returns the value of the program.
Perhaps the first formal incarnation of operational semantics was the use of the lambda calculus to define the semantics of LISP. Abstract machines in the tradition of the SECD machine are also closely related.

History

The concept of operational semantics was used for the first time in defining the semantics of Algol 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 computer
which performs the set of actions which constitute the elaboration of that program.

The first use of the term "operational semantics" in its present meaning is attributed to
Dana Scott.
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 to
semantics, but if the plan is to be any good, the operational aspects cannot
be completely ignored.

Approaches

introduced the structural operational semantics, Robert Hieb and Matthias Felleisen the reduction contexts, and Gilles Kahn the natural semantics.

Small-step semantics

Structural operational semantics

Structural operational semantics was introduced by Gordon Plotkin in 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 and inductive, view on operational semantics. An SOS specification defines the behavior of a program in terms of a transition relation. SOS specifications take the form of a set of inference 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 in [|Plotkin81] and [|Hennessy90], and other textbooks. Let range over programs of the language, and let range over states. If we have expressions, values and locations, then a memory update command would have semantics:
Informally, the rule says that "if the expression in state reduces to value, then the program will update the state with the assignment ".
The semantics of sequencing can be given by the following three rules:
Informally, the first rule says that,
if program in state finishes in state, then the program in state will reduce to the program in state.
The second rule says that
if the program in state can reduce to the program with state, then the program in state will reduce to the program in state.
The semantics is structural, because the meaning of the sequential program, is defined by the meaning of and the meaning of.
If we also have Boolean expressions over the state, ranged over by, then we can define the semantics of the while command:
Such a definition allows formal analysis of the behavior of programs, permitting the study of relations between programs. Important relations include simulation preorders and bisimulation.
These are especially useful in the context of concurrency theory.
Thanks to its intuitive look and easy-to-follow structure,
SOS has gained great popularity and has become a de facto standard in defining
operational semantics. As a sign of success, the original report on SOS has attracted more than 1000 citations according to the CiteSeer ,
making it one of the most cited technical reports in Computer Science.

Reduction semantics

Reduction semantics are an alternative presentation of operational semantics using so-called reduction contexts. The method was introduced by Robert Hieb and Matthias Felleisen in 1992 as a technique for formalizing an equational theory for control and state. For example, the grammar of a simple call-by-value lambda calculus and its contexts can be given as:
The contexts include a hole where a term can be plugged in.
The shape of the contexts indicate where reduction can occur.
To describe a semantics for this language, axioms or reduction rules are provided:
This single axiom is the beta rule from the lambda calculus. The reduction contexts show how this rule composes
with more complicated terms. In particular, this rule can trigger for the argument position of an
application like because there is a context
that matches the term. In this case, the contexts uniquely decompose terms so that only one reduction is possible
at any given step. Extending the axiom to match the reduction contexts gives the compatible closure. Taking the
reflexive, transitive closure of this relation gives the reduction relation for this language.
The technique is useful for the ease in which reduction contexts can model state or control constructs. In addition, reduction semantics have been used to model object-oriented languages, contract systems, and other language features.

Big-step semantics

Natural semantics

Big-step structural operational semantics is also known under the names natural semantics, relational semantics and evaluation semantics. Big-step operational semantics was introduced under the name natural semantics by Gilles Kahn when presenting Mini-ML, a pure dialect of the ML language.
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.
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.

Comparison

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 and often directly correspond to an efficient implementation of an interpreter for the language Both can lead to simpler proofs, for example when proving the preservation of correctness under some program transformation.
The main disadvantage of big-step semantics is that non-terminating computations do not have an inference tree, making it impossible to state and prove properties about such computations.
Small-step semantics give more control of 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 proving type soundness of a type system against an operational semantics.