Operational Semantics

A Tiny Example Language

We’ll start very simply, with a language that just has integers, addition and subtraction, and print statements. Programs look like this:

print(8 - (3 + 21) + 34);
print(55 - 3 + 2);

The concrete syntax can be given by this grammar:

Program = Stmt+
Stmt    = "print" "(" Exp ")" ";"
Exp     = (Exp ("+" | "-"))? Term
Term    = num | "(" Exp ")"
num     = digit+

When defining a semantics we don’t care about concrete syntax, only abstract syntax. So here is the abstract syntax of this tiny language, which is all we care about from here on:

n: Nml
e: Exp = n | e + e | e - e
s: Stm = print e
p: Pro = program s+

Need Practice?

For the example program in this section, give both the parse tree and the abstract syntax tree.

Concrete Operational Semantics

A concrete operational semantics is given to a language by mapping language constructs to operations on a virtual machine—a machine whose operation is “obvious.”

Stack machines are pretty well understood! Let’s make up a stack machine. The machine has a stack for execution and allows you to store integers in named cells. The instructions are:

When doing a concrete operational semantics, we just show the instruction sequence for each abstract syntactic form. That way, every program in our language will be translated to a unique instruction sequence. We assume this machine is sooooooooo simple that the meaning of instruction sequences is well understood. Therefore showing how to translate programs into machine instruction sequences suffices to define the semantics of the language. We will define the translation function, $T$, by cases on the abstract syntax forms:

The cool brackets $[\![$ and $]\!]$ distinguish syntactic forms, such as numerals and plus-expressions, from regular mathematical values, such as numbers.

Let’s see how it works for a trivial program:

$\begin{array}{l} T[\![\mathtt{program}\;\mathtt{print}\;8 + 13]\!] \\ \;\;\;\; = T[\![\mathtt{print}\;8 + 13]\!] \\ \;\;\;\; = T[\![8 + 13]\!] \;•\; \mathsf{PRINT} \\ \;\;\;\; = T[\![8]\!] \;•\; T[\![13]\!] \;•\; \mathsf{ADD} \;•\; \mathsf{PRINT} \\ \;\;\;\; = \mathsf{PUSH}\;8 \;•\; T[\![13]\!] \;•\; \mathsf{ADD} \;•\; \mathsf{PRINT} \\ \;\;\;\; = \mathsf{PUSH}\;8 \;•\; \mathsf{PUSH}\;13 \;•\; \mathsf{ADD} \;•\; \mathsf{PRINT} \\ \;\;\;\; = (\mathsf{PUSH}\;8, \mathsf{PUSH}\;13) \;•\; \mathsf{ADD} \;•\; \mathsf{PRINT} \\ \;\;\;\; = (\mathsf{PUSH}\;8, \mathsf{PUSH}\;13, \mathsf{ADD}) \;•\; \mathsf{PRINT} \\ \;\;\;\; = (\mathsf{PUSH}\;8, \mathsf{PUSH}\;13, \mathsf{ADD}, \mathsf{PRINT}) \end{array}$

The execution of this program on the “machine” unfolds as follows:

                // stack is (), output is ()
PUSH 8          // stack is [8], output is ()
PUSH 13         // stack is [8, 13], output is ()
ADD             // stack is [21], output is ()
PRINT           // stack is (), output is [21]

So the meaning of our program is the one element integer list $[21]$.

The translation of the example program from the beginning of this section is:

// print(8 - (3 + 21) + 34);
// print(55 - 3 + 2);

PUSH 8 
PUSH 3 
PUSH 21
ADD
SUB     
PUSH 34
ADD
PRINT
PUSH 55
PUSH 3 
SUB
PUSH 2 
ADD
PRINT   

Execute the program on the virtual machine. The output should be $[18, 54]$.

Structural Operational Semantics

Rather than specifying a machine with its own instruction set, we can simply define rules that show how a computation proceeds without the separate machine. Yep, we are going to abstract away the abstract machine!

For the tiny language, evaluating expressions eventually produces a number, executing statements keeps appending to “standard output,” and the execution of a program involves executing its statements, starting with the empty output to eventually produce its final output.

Here is the basic idea:

For each syntactic construct, the “machine” is in some configuration, which is either (1) the construct along with some other supporting data like a memory, input, output, or some such thing, or (2) some kind of “result”. The first kind of configuration is called an intermediate configuration.

In our example language:

• For expressions, the intermediate configuration is an expression; the terminal configuration is a number.
• For statements, the intermediate configuration is a statement plus the output-so-far; the terminal configuration is an output.
• For programs, the intermediate configuration is a program plus the output-so-far; the terminal configuration is an output.

This is best developed live, in a video or on a whiteboard.

To apply the semantics, we find the $o$ that the “starting configuration” $ [\![\mathtt{program}\;s_1 \cdots s_n]\!], ()$ will end up in. We can show the computation with a proof tree:

How much work was that?

That was a lot of work for a tiny language. Did you know there is another way to do this stuff, that does not involve nitty gritty computation details? There is. It is called natural semantics. Coming up...right now.

Natural Semantics

The semantics we’ve just seen, structural operational semantics, is often called small-step operational semantics. There’s another approach, known as, you guessed it, big-step operational semantics, also called natural semantics.

A motivation for, and details of, natural semantics, can be found in any good textbook on semantics. But we can learn it by just jumping right in. Here is the natural semantics for the tiny language we’ve been working with:

We’ll derive this in class. Did you find it easier going?

Structural Operational Semantics vs. Natural Semantics

It might take time to really internalize the difference. Here are two things that may help. First, a summary table:

SOS	Natural
Break computations down into individual “steps”	Concerned only with the final result of evaluating a construct
Aka: “small-step”, “transitional”, “reduction”	Aka: “big-step”, “relational”, “evaluation”
Uses $\rightarrow$	Uses $\Rightarrow$ or $\Downarrow$
Transitions between configurations, e.g., $ e,m \rightarrow e',m$	Complete evaluation of constructs, e.g., $ e,m \Rightarrow x$
Gordon Plotkin, 1981	Gilles Kahn, 1987

Second, here is a fantastic and detailed slide deck from a University of Illinois class that does an excellent job of describing both methods.

Operational Semantics for Astro

Let’s scale up just a little bit. Remember Astro? Here is the abstract syntax:

Several new features appear in Astro that were not in the trivial language:

• Identifiers, which stand for variables and functions
• Unary negation
• Binary multiplication, division, remainder, and exponentiation
• Assignment statements and print statements
• Function calls
• Variables can be read-only (RO) or read-write (RW)
• Semantic rules that completely separate variables and functions
• Semantic rules about the number of arguments matching the number of parameters
• A “standard library” of built-in variables (π, read-only), and functions (sin, cos, sqrt, and hypot)
• Astro programs can crash. Every syntactivally correct program in the trivial language had a meaning; they always ran to completion. In Astro, some programs fail to run, either due to the use of identifiers that have never been previously assigned, the attempt to write to a read-only variable, the attempt to invoke a number as a function, or a (run-time) division by zero.

Concrete Operational Semantics

We’ll have to scale up the machine a bit to support Astro:

Natural Semantics

To get started, we think through the kinds of reduction relations we need. Since we have identifiers that are bound to entities, we need a place to store the entities. This is usually called a store or a memory. Expressions have to be evaluated in the context of a memory, and will produce a number:

$\Longrightarrow_E\;\subseteq (\mathsf{Exp} \times \mathsf{Mem}) \times \mathbb{R}$

Statements read and modify this memory and the program’s output. We’ll create the type abbreviation $\mathsf{Output}=\mathbb{R}^*$ to make the specification a little more transparent:

$\Longrightarrow_S\;\subseteq (\mathsf{Stm} \times \mathsf{Mem} \times \mathsf{Output}) \times (\mathsf{Mem} \times \mathsf{Output})$

Programs are executed to produce a list of output values:

$\Longrightarrow_P\;\subseteq \mathsf{Pro} \times \mathsf{Output}$

There are four things an identifier can stand for: (1) a numeric variable, (2) a function (something that is called from an expression), or (3) nothing at all. Numeric variables not only have a numeric value, but we also have to track whether they are read-only or read-write. And for functions, we have to keep track of not only their “value” (a lambda expression, woohoo), but how many parameters they are declared with, since we can only call them with the exact same number of arguments! This means that our memory is a function with the following type:

$\begin{array} l\mathsf{Ide} \rightarrow (\\ \;\;\;\; \{\mathsf{UNDEF}\} \;\cup \\ \;\;\;\; (\{\mathsf{NUM}\} \times \mathbb{R} \times \{\mathsf{RO},\mathsf{RW}\}) \;\cup \\ \;\;\;\; (\{\mathsf{FUN}\} \times (\mathbb{R}^* \rightarrow \mathbb{R}) \times \mathbb{N})) \end{array}$

Now we are ready to give the natural semantics. We start slow, with expressions. Some of these are rather detailed, so much class time will be spent in showing where the rules come from.

where $o_0$, the initial output, is defined to be the empty sequence, and the initial memory $m_0$ is our “standard library”:

How did we handle errors?

We took a simple approach to error handling here. Programs that are illegal, either because they violate static constraints (e.g., using an identifier bound to the wrong type of entity), or failed at run time (e.g., divide by zero), just simply cannot be derived by the semantic rules.

We”re not that interested, then, in what kind of “error” a program exhibits. What we care about is: if the program is legal, what is its meaning?

How bad was that? Of course, it takes practice to get used to.

Structural Operational Semantics

An exercise for you.

Operational Semantics for Bella

The programming language Bella has its own formal specification. It adds a bunch of very interesting features to Astro:

• Logical (and, or, not) and relational (equality and inequality) operators. As in early versions of C though, “booleans” are really numbers.
• Actual variable declarations. In Astro, like Python, variables come into existence the first time they are assigned to. Bella requires a syntactically distinct declaration form (with the let keyword). All variables must be declared before being used.
• A while statement.
• A conditional expression.
• User-declared functions! Bella programmers can declare their own functions. Within the body of the function, parameters shadow variables of the same name, if any.

Here’s the abstract syntax, copied from the specification:

Natural Semantics

The natural semantics of Bella is fully explained in the specification, so head over there to continue your operational semantics study.

Structural Operational Semantics

Try it!

Concrete Operational Semantics

It should be really fun to extend the virtual machine we’ve been playing with above to have new instructions that can handle Bella.

Some Interesting Language Features

Rather than jumping in to a new language, let’s go one feature at a time, and think, how might we extend Bella to have this feature?”

If Statements

The ubiquitous if-statement might look like this in a Bella program:

if x >= 3 {
   print(y);
   y = sqrt(y);
} else {
   y = y ** 2;
}

and in the abstract syntax appear as:

s: Statement = ... | if e b b

The (natural semantics) rules should be straightforward:

For SOS we need to compute in smaller steps, bringing our tests down to a single number:

Parallel Assignment

Many languages have what they call parallel assignment, which might look like:

x, y = e1, e2

Natural semantics for Bella (in which identifiers must be bound before they can appear anywhere, including assignment statements):

Swap

Swapping is similar to parallel assignment, but (in most languages) requires that both identifiers already be bound to read-write variables. Of course, that kind of behavior can vary from language to language, but that’s what we will assume here. The concrete syntax might look like:

x, y = y, x

with the following abstract syntax:

s: Statement = ... | swap i i

Natural semantics:

And SOS:

Repeat-Until

What about something like this? You know, kinda like the while-statement except the body is executed at least once. And a truthy condition stops the loop.

repeat {
   print(y);
   y = sqrt(y);
} until y < 1;

Abstract syntax:

s: Statement = ... | repeat b e

Semantics:

Repeat-N-Times

More mainstream languages need this beauty:

repeat n*2 {
   print(0);
}

Yep that’s right. Just execute a block a certain number of times, without having to introduce a stupid iterator variable. Abstract syntax:

s: Statement = ... | dotimes e b

For the semantics, we, as language designers, have to determine whether we want to evaluate the number of times to do the loop just once, or re-evaluate it each time. Let’s say we evaluate it only once, before we even think about doing the loop body:

For-Loops

Sometimes, your definite iteration will need a iterator variable. Here’s a common form that we can add to Bella:

for i = x to y*8 {
   print(i);
   y = y / 2;
}

with abstract syntax:

s: Statement = ... | for i e e b

Again, as language designers, we have some choices to make:

• Should we evaluate the loop-ending value just once, or each time we begin a new iteration?
• Do we execute the loop body when the iterator is equal to the end value or not? (That is, do the loops have inclusive or exclusive upper bounds? Are they “through” or “up to”?)
• Should the iterator variable be local to the loop, or should it belong to the declared variable set of the containing scope? If local, should it be read-only? If global, does the statement add the variable to the set or must it already exist? And then if it should add, what if it was already there? And also, if global, it would have to be read-write, or maybe not?

Let’s choose to evaluate the bounds once at the beginning, and to make the loop variable local to the body and read-only. This gives us the semantic rules:

Nondeterminism

Many languages have a select statement, whose job is to randomly pick one of its arms to execute. The simplest form is to have exactly two arms:

select {
   print(0);
} or {
   y = y / 2;
   print(1);
}

with abstract syntax:

s: Statement = ... | select b b

The semantics are simple, but interesting. We have multiple rules that can fire for a given select statement. But that’s just fine. It’s what we want. The program has multiple possible executions. The semantics tells us all of them.

Concurrency

Concurrency is about things happening “at the same time.” The usual model is interleaved computation. For example:

TODO

can have multiple results:

TODO

Let’s add a new syntactic construct to execute two statements concurrently:

s: Statement = ... | par s s

Here, natural semantics is not sufficient; it can only say that we can execute the first statement and then the second, or the second and then the first. But an SOS can specify interleaved execution quite easily:

Types

Now for one of biggest topics: types.

In OG Bella, variables could only hold numeric values. “Boolean” expressions like x>=y just evaluate to either 0 or 1, so boolean values did not exist. 0 was “falsy” and 1 was “truthy.” Expressions never produced anything but numbers! This is far from a modern programming language.

Strong Typing

Let’s extend Bella to be much more expressive: we’ll allow expressions to not only evaluate to numbers or booleans, but functions as well. And we’ll add lists. But with added power comes some responsibilities: we should do typechecking so we don’t multiply functions, call numbers, perform a not operation on a number, or other such dreadful things. We want to make it so that any misuse of expressions—that is the use of an expression of one type in a context that requires a different type—generate an error. We want strong typing.

Before we show the semantics, let’s look at lists. They should look like this in Bella programs:

a = [10, 20, 30];
b = [false, true, true, false];
if (b[0) {
  print(a[2]);
}

which in the abstract syntax will admit two new forms:

e: Exp = ... | e[e] | [e*]

So now for the semantics. Expression evaluation in OG Bella always produced a number. Now it will produce a more general value:

Now what are values? There is a value for each kind of type (respectively, number, boolean, list, user-defined function, intrinsic function). So we’re gonna say:

Now we need a memory to store the entities bound to each identifier:

Here’s the semantics:

Static Types

The semantics above strongly suggested type checking was done at run time. Now suppose we wanted to extend that extension of Bella so that all type checking could be done at compile time. Many (most?) programmers love languages that check types during compilation since it gives them a bit more confidence about the program’s correctness. Others my not like the lack of flexibility. Whatever your preference may be, static typing is a thing we should explore.

With static types, the language itself should have some changes. We will:

• Add new keywords number, boolean,

The static semantics will show what each construct “means” relative to a context. A context maps identifiers to things we know about them at compile time, rather than run time. We don’t care about values, then, but we do care about types and access (read-only or read-write). A context is then:

When analyzing an expression in a context, we want to generate a type for it. When analyzing statements (which may include declarations, we will produce a new context. Programs simply are ok or not ok. Formally the relation types are:

TODO: explain the relations

A possible static semantics is:

A nice benefit of doing the static semantics only is that we can now write the dynamic semantics under the assumption that the program has already been typechecked. This means our memory needs to only store values (since the read-only and number-of-parameter settings has already been handled in the static semantics. We’ve done that “break a large problem down into smaller ones” thing! Here is the Bella dynamic-semantics-only:

Learning More

Here are some good papers and other references:

• Wikipedia Operational Semantics
• The OG paper by Gordon Plotkin where he created SOS
• The OG paper by Gilles Kahn introducing Natrual Semantics
• A very deep 133-page book chapter with 200+ references entirely on SOS
• Notes from a class at Cornell
• Notes from a class at Oregon Statement
• Lecture notes from New Mexico State
• Harvard notes on big-step semantics
• Harvard notes on small-step semantics
• Harvard notes on large-step semantics
• A presentation on an SOS for JavaScript

Summary