Operational semantics
Encyclopedia
In computer science
, operational semantics is a way to give meaning to computer program
s in a mathematically rigorous way. Operational semantics are classified into two categories: structural operational semantics (or small-step semantics) formally describe how the individual steps of a computation
take place in a computer-based system. By opposition natural semantics (or big-step 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. (In general there can be many return values for a single program,
because the program could be nondeterministic
, 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.)
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 first use of the term "operational semantics" in its present meaning is attributed to
Dana Scott (Plotkin04).
What follows is a quote from Scott's seminal paper on formal semantics,
in which he mentions the "operational" aspects of semantics.
Perhaps the first formal incarnation of operational semantics was the use of the lambda calculus
to define the semantics of LISP
by [].
Abstract machines in the tradition of the SECD machine
are also closely related.
introduced the structural operational semantics, Robert Hieb and Matthias Felleisen
the reduction contexts , and Gilles Kahn
the natural semantics.
in (Plotkin81) as a logical means to defining 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 (set of) transition relation
(s). SOS specifications take the form of a set of inference rules which 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 (e.g. functions from memory locations to values). If we have expressions (ranged over by 
), 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 
.
(You can think of this as formalizing "You can run
, and then run 
using the resulting memory store.)
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 
.
(You can think of this as formalizing the principle for an optimizing compiler:
"You are allowed to transform
as if it were stand-alone, even if it is just the
first part of a program.")
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 preorder
s 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 (so-called Aarhus
report) on SOS (Plotkin81) has attracted more than 1000 citations according to the CiteSeer http://citeseer.ist.psu.edu/673965.html,
making it one of the most cited technical reports in Computer Science
.
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 (i.e., a term can be plugged into) a term.
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 (e.g., continuations). In addition, reduction semantics have been used to model object-oriented languages, contract systems
, and other language features.
Computer science
Computer science or computing science is the study of the theoretical foundations of information and computation and of practical techniques for their implementation and application in computer systems...
, operational semantics is a way to give meaning to computer program
Computer program
A computer program is a sequence of instructions written to perform a specified task with a computer. A computer requires programs to function, typically executing the program's instructions in a central processor. The program has an executable form that the computer can use directly to execute...
s in a mathematically rigorous way. Operational semantics are classified into two categories: structural operational semantics (or small-step semantics) formally describe how the individual steps of a computation
Computation
Computation is defined as any type of calculation. Also defined as use of computer technology in Information processing.Computation is a process following a well-defined model understood and expressed in an algorithm, protocol, network topology, etc...
take place in a computer-based system. By opposition natural semantics (or big-step semantics) describe how the overall results of the executions are obtained. Other approaches to providing a formal semantics of programming languages
Formal semantics of programming languages
In programming language theory, semantics is the field concerned with the rigorous mathematical study of the meaning of programming languages and models of computation...
include axiomatic semantics
Axiomatic semantics
Axiomatic semantics is an approach based on mathematical logic to proving the correctness of computer programs. It is closely related to Hoare logic....
and denotational semantics
Denotational semantics
In computer science, denotational semantics is an approach to formalizing the meanings of programming languages by constructing mathematical objects which describe the meanings of expressions from the languages...
.
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. (In general there can be many return values for a single program,
because the program could be nondeterministic
Nondeterministic algorithm
In computer science, a nondeterministic algorithm is an algorithm that can exhibit different behaviors on different runs, as opposed to a deterministic algorithm. There are several ways an algorithm may behave differently from run to run. A concurrent algorithm can perform differently on different...
, 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.)
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. (Algol68, Section 2)
The first use of the term "operational semantics" in its present meaning is attributed to
Dana 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 to
semantics, but if the plan is to be any good, the operational aspects cannot
be completely ignored. (Scott70)
Perhaps the first formal incarnation of operational semantics was the use of the lambda calculus
Lambda calculus
In mathematical logic and computer science, lambda calculus, also written as λ-calculus, is a formal system for function definition, function application and recursion. The portion of lambda calculus relevant to computation is now called the untyped lambda calculus...
to define the semantics of LISP
Lisp
A lisp is a speech impediment, historically also known as sigmatism. Stereotypically, people with a lisp are unable to pronounce sibilants , and replace them with interdentals , though there are actually several kinds of lisp...
by [].
Abstract machines in the tradition of the SECD machine
SECD machine
The SECD machine is a highly influential virtual machine and abstract machine intended as a target for functional programming language compilers. The letters stand for Stack, Environment, Code, Dump, the internal registers of the machine...
are also closely related.
Approaches
Gordon PlotkinGordon Plotkin
Gordon D. Plotkin, FRS, FRSE is a Scottish computer scientist.Gordon Plotkin is best-known for his introduction of structural operational semantics and his work on denotational semantics. In particular, his notes on A Structural Approach to Operational Semantics of 1981 were very influential...
introduced the structural operational semantics, Robert Hieb and Matthias Felleisen
Matthias Felleisen
Matthias Felleisen is a computer science professor and an author of German background.Felleisen is currently a Trustee Professor in the College of Computer and Information Science at Northeastern University in Boston, Massachusetts. In the past he has taught at Rice University after receiving his...
the reduction contexts , and Gilles Kahn
Gilles Kahn
Gilles Kahn was a French computer scientist. He notably introduced Kahn process networks as a model for parallel processing....
the natural semantics.
Structural operational semantics
Structural operational semantics (also called structured operational semantics or small-step semantics) was introduced by Gordon PlotkinGordon Plotkin
Gordon D. Plotkin, FRS, FRSE is a Scottish computer scientist.Gordon Plotkin is best-known for his introduction of structural operational semantics and his work on denotational semantics. In particular, his notes on A Structural Approach to Operational Semantics of 1981 were very influential...
in (Plotkin81) as a logical means to defining 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 (set of) transition relation
State transition system
In theoretical computer science, a state transition system is an abstract machine used in the study of computation. The machine consists of a set of states and transitions between states, which may be labeled with labels chosen from a set; the same label may appear on more than one transition...
(s). SOS specifications take the form of a set of inference rules which 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 (e.g. functions from memory locations to values). If we have expressions (ranged over by ), 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 .(You can think of this as formalizing "You can run
, and then run using the resulting memory store.)
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 .(You can think of this as formalizing the principle for an optimizing compiler:
"You are allowed to transform
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
, 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
Relation (mathematics)
In set theory and logic, a relation is a property that assigns truth values to k-tuples of individuals. Typically, the property describes a possible connection between the components of a k-tuple...
between programs. Important relations include simulation preorder
Simulation preorder
In theoretical computer science a simulation preorder is a relation between state transition systems associating systems which behave in the same way in the sense that one system simulates the other....
s and bisimulation
Bisimulation
In theoretical computer science a bisimulation is a binary relation between state transition systems, associating systems which behave in the same way in the sense that one system simulates the other and vice-versa....
.
These are especially useful in the context of concurrency theory
Concurrency (computer science)
In computer science, concurrency is a property of systems in which several computations are executing simultaneously, and potentially interacting with each other...
.
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 (so-called Aarhus
report) on SOS (Plotkin81) has attracted more than 1000 citations according to the CiteSeer http://citeseer.ist.psu.edu/673965.html,
making it one of the most cited technical reports in Computer Science
Computer science
Computer science or computing science is the study of the theoretical foundations of information and computation and of practical techniques for their implementation and application in computer systems...
.
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 FelleisenMatthias Felleisen
Matthias Felleisen is a computer science professor and an author of German background.Felleisen is currently a Trustee Professor in the College of Computer and Information Science at Northeastern University in Boston, Massachusetts. In the past he has taught at Rice University after receiving his...
in 1992 as a technique for formalizing an equational theory for control
Control flow
In computer science, control flow refers to the order in which the individual statements, instructions, or function calls of an imperative or a declarative program are executed or evaluated....
and state
Program state
One of the key concepts in computer programming is the idea of state, essentially a snapshot of the measure of various conditions in the system. Most programming languages require a considerable amount of state information in order to operate properly - information which is generally hidden from...
. For example, the grammar of a simple call-by-value lambda calculus
Lambda calculus
In mathematical logic and computer science, lambda calculus, also written as λ-calculus, is a formal system for function definition, function application and recursion. The portion of lambda calculus relevant to computation is now called the untyped 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 (i.e., a term can be plugged into) a term.
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 (e.g., continuations). In addition, reduction semantics have been used to model object-oriented languages, contract systems
Design by contract
Design by contract , also known as programming by contract and design-by-contract programming, is an approach to designing computer software...
, and other language features.
Natural semantics
Natural semantics (or big-step semantics) ...See also
- Algebraic semanticsAlgebraic semanticsAn programming language theory, the algebraic semantics of a programming language is a form of axiomatic semantics based on algebraic laws for describing and reasoning about program semantics in a formal manner....
- Axiomatic semanticsAxiomatic semanticsAxiomatic semantics is an approach based on mathematical logic to proving the correctness of computer programs. It is closely related to Hoare logic....
- Denotational semanticsDenotational semanticsIn computer science, denotational semantics is an approach to formalizing the meanings of programming languages by constructing mathematical objects which describe the meanings of expressions from the languages...
- Interpreter semantics
- Formal semantics of programming languagesFormal semantics of programming languagesIn programming language theory, semantics is the field concerned with the rigorous mathematical study of the meaning of programming languages and models of computation...