We’ll start very simply, with a language that just has integers, addition and subtraction, and print statements. We’ll call the language PlusMinusLang. Programs look like this:
print(8 - (3 + 21) + 34);
print(55 - 3 + 2);
The concrete syntax can be given by this analytic grammar:
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:
Need Practice?
For the example program in this section, give both the parse tree and the abstract syntax tree.
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:
| Instruction | Description |
|---|---|
| PUSH $n$ | Push the value of the literal $n$ |
| ADD | Pop twice then push first popped value plus second popped value |
| SUB | Pop twice then push first popped value minus second popped value |
| Print contents of top of stack to standard output then pop |
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 so simple that the meaning of instruction sequences is well understood. (This is a recurring theme in foundations!) 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]\!] \\ \quad = T[\![\mathtt{print}\;8 + 13]\!] \\ \quad = T[\![8 + 13]\!] \,\mathtt{+\!+}\, [\mathsf{PRINT}] \\ \quad = T[\![8]\!] \,\mathtt{+\!+}\, T[\![13]\!] \,\mathtt{+\!+}\, [\mathsf{ADD}] \,\mathtt{+\!+}\, [\mathsf{PRINT}] \\ \quad = [\mathsf{PUSH}\;8] \,\mathtt{+\!+}\, T[\![13]\!] \,\mathtt{+\!+}\, [\mathsf{ADD}] \,\mathtt{+\!+}\, [\mathsf{PRINT}] \\ \quad = [\mathsf{PUSH}\;8] \,\mathtt{+\!+}\, [\mathsf{PUSH}\;13] \,\mathtt{+\!+}\, [\mathsf{ADD}] \,\mathtt{+\!+}\, [\mathsf{PRINT}] \\ \quad = [\mathsf{PUSH}\;8, \mathsf{PUSH}\;13] \,\mathtt{+\!+}\, [\mathsf{ADD}] \,\mathtt{+\!+}\, [\mathsf{PRINT}] \\ \quad = [\mathsf{PUSH}\;8, \mathsf{PUSH}\;13, \mathsf{ADD}] \,\mathtt{+\!+}\, [\mathsf{PRINT}] \\ \quad = [\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]$.
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:
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.
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. Where little steps in SOS are given with the relation $\longrightarrow$, natural semantics uses $\Longrightarrow$ or $\Downarrow$ to signify that a construct is completely evaluated or executed to its final configuration.
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?
Let’s take a closer look at how SOS and Natural Semantics compare. First, a little 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.
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:
π, read-only), and functions (sin, cos, sqrt, and hypot)We are going to look at the three styles of operations semantics for Astro.
We’ll have to scale up the machine a bit to support Astro:
| Instruction | Description |
|---|---|
| PUSH $n$ | Push the value of the literal $n$ |
| LOAD $v$ | Push the value in memory location $v$, crashing if $v$ is not in memory |
| STORE $v$ | Pop into memory location $v$ |
| NEG | Pop then push the negation of the popped value |
| SIN | Pop then push the sine of the popped value |
| COS | Pop then push the cosine of the popped value |
| SQRT | Pop then push the square root of the popped value |
| ADD | Pop twice then push first popped value plus second popped value |
| SUB | Pop twice then push first popped value minus second popped value |
| MUL | Pop twice then push first popped value times second popped value |
| DIV | Pop twice then push first popped value divided by second popped value, crashing if the second popped value is 0 |
| REM | Pop twice then push the remainder of first popped value divided by second popped value |
| POW | Pop twice then push first popped value raised to the power of the second popped value |
| HYPOT | Pop twice then push the hypotenuse of the two popped values |
| Print contents of top of stack to standard output then pop |
For example, the Astro program:
x = 9 * 35 ** π;
print(3 / hypot(1-cos(x), 13));
is:
PUSH 9
PUSH 35
PUSH π
POW
MUL
STORE x
PUSH 3
PUSH 1
LOAD x
COS
SUB
PUSH 13
HYPOT
DIV
PRINT
For a concrete semantics, we give the translation to the little stack language. We could define a formal translation function as we did above for PlusMinusLang, but we can also give it in Python:
import math
def check(condition, message):
if not condition:
raise ValueError(message)
initial_env = {
"π": { "kind": "CONST", "value": math.pi },
"sqrt": { "kind": "FUN", "arity": 1 },
"sin": { "kind": "FUN", "arity": 1 },
"cos": { "kind": "FUN", "arity": 1 },
"hypot": { "kind": "FUN", "arity": 2 }}
def t(node, env):
match node:
case int(n) | float(n):
return [f"PUSH {n}"]
case str(x):
check(x in env, f"Uninitialized {x}")
check((kind := env[x]["kind"]) in ("CONST", "VAR"), "Not a variable")
return [f"LOAD {x}" if kind == "VAR" else f"PUSH {env[x]['value']}"]
case ("neg", e):
return t(e, env) + ["NEG"]
case ("add", e1, e2):
return t(e1, env) + t(e2, env) + ["ADD"]
case ("sub", e1, e2):
return t(e1, env) + t(e2, env) + ["SUB"]
case ("mul", e1, e2):
return t(e1, env) + t(e2, env) + ["MUL"]
case ("div", e1, e2):
return t(e1, env) + t(e2, env) + ["DIV"]
case ("rem", e1, e2):
return t(e1, env) + t(e2, env) + ["REM"]
case ("pow", e1, e2):
return t(e1, env) + t(e2, env) + ["POW"]
case ("call", f, args):
check(f in env, f"Unknown {f}")
check(env[f]["kind"] == "FUN", f"{f} is not a function")
check(len(args) == env[f]["arity"], f"Wrong number of args for {f}")
return [i for arg in args for i in t(arg, env)] + [f.upper()]
case ("assign", i, e):
check(i not in env or env[i]["kind"] == "VAR", f"{i} is not assignable")
return t(e, env) + [f"STORE {i}"], {**env, i: {"kind": "VAR"}}
case ("print", exp):
return t(exp, env) + ["PRINT"], env
case ("program", statements):
code, e = [], env
for s in statements:
c, e = t(s, e)
code += c
return code
case _:
raise ValueError("Malformed program")
# Quick check: print the translation of a small program
program = ("program", [
("assign", "x", ("mul", 9, ("pow", 35, "π"))),
("print", ("div", 3, ("call", "hypot", [
("sub", 1, ("call", "cos", ["x"])), 13])))])
print('\n'.join(t(program, initial_env)))
Let’s run it:
$ python3 astro_concrete.py PUSH 9 PUSH 35 PUSH 3.141592653589793 POW MUL STORE x PUSH 3 PUSH 1 LOAD x COS SUB PUSH 13 HYPOT DIV PRINT
Exactly what we expected.
The Astro language specification contains a natural semantics specification in which static and dynamic aspects of the language are mashed together.
In our notes on Semantics, a two-part natural semantics was given.
You may wish to review both specifications now.
An exercise for you.
The programming language Bella has its own formal specification. It adds a bunch of very interesting features to Astro:
let keyword). All variables must be declared, not just assigned to, before being used.while statement.Bella was just complex enough that we did not even try to build an “all-in-one” semantics; instead the language definition itself is given with separate static and dynamic semantics.
The language definition presents a natural semantics. A structural operational and concrete operational semantics are left for you as an exercise.
Bella is a very simple language. To learn more about operational semantics, we are going to grow the language, little by little, giving the semantics for each new feature as they are introduced.
We’ll stay with natural semantics, unless otherwise specified.
In OG Bella, all expressions evaluate to numbers, with the literal $\textsf{true}$ being represented as 1 and $\textsf{false}$ as 0. Relational and logical operators cast their results to numbers as well. We can do better by allowing variables to hold numbers, booleans, and functions. We can then provided sensible typing for operators, restrict the test of a while-statement to have Boolean type, pass functions as arguments, return functions from functions, and just overall keep things separated by type.
TODO show example code
Naturally, we’d like to do all of our type checking in the statics.
This is not a trivial change. It even requires a change to the syntax, as our function parameters will need to carry type annotations. (Strictly speaking, they don’t have to if we adopted a more sophisticated type inference system which is well beyond the scope of these notes.) In the abstract syntax we add a new category $\textsf{Type}$ and change the function declaration to include type annotations for each parameter.
The static semantics has enough changes to warrant a full rewrite:
The dynamic semantics changes rather little. Here are the rules that change:
TODO
The ubiquitous if-statement might look like this in a Bella program:
if x >= 3 {
print(y);
y = sqrt(y);
} else {
y = y ** 2;
}
Abstract syntax:
$s: \textsf{Statement} = \ldots \mid \texttt{if}\;e\;b\;b$
Static semantics. The test expression must have Boolean type. As in the while statement, any changes to the context within the arms are not reflected outside the if-statement—variables declared in the inner blocks are local to their respective inner block. From the outside, the if-statement leaves the context unchanged.
Dynamic semantics. Only one arm is executed:
For SOS we need to compute in smaller steps, bringing our tests down to a single number:
Many languages have what they call parallel assignment, which might look like:
x, y = e1, e2
with the following abstract syntax:
$s: \textsf{Statement} = \ldots \mid i, i = e, e$
Static semantics. The two variables and the two expressions must all share the same type, and the two variables must be mutable. The context does not change because no new variables are introduced:
Dynamic semantics, The expressions are evaluated first and afterwards the memory is updated:
let x, y = e1, e2). Such a construct would indeed produce a new context in the static semantics.
The repeat-until statement exists in a handful of modern languages. The body is executed at least once, and a true condition stops the loop.
repeat {
print(y);
y = sqrt(y);
} until y < 1;
Abstract syntax:
$s: \textsf{Statement} = \ldots \mid \texttt{repeat}\;b\;e$
Static Semantics. The test must have boolean type and local variables declared in the inner block stay in the inner block.
Dynamic Semantics. The inner block must be executed at least once:
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 useless iterator variable. Abstract syntax:
$s: \textsf{Statement} = \ldots \mid \texttt{dotimes}\;e\;b$
Static semantics. The expression specifying the number of times to repeat must have numeric type. As with other blocks, any changes to the context within the block are local to the block and do not affect the outside context.
Dynamic 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:
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: \textsf{Statement} = \ldots \mid \texttt{for}\;i\;e\;e\;b$
Again, as language designers, we have some choices to make:
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:
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: \textsf{Statement} = \ldots \mid \texttt{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.
Let’s add a new type for homogenous lists, with a list literal of the form [e_1, e_2, \ldots, e_n] and a list-indexing expression of the form e_1[e_2].
TODO
TODO
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.
To make things more interesting, let’s extend Bella by separating numbers and booleans, adding indexable lists, and allowing variables to hold different types of values, including functions, The extended language will be called Bella 2 (so original, sorry). Here’s the abstract syntax:
Rather than carrying around type checks at run time, we can perform type checking at compile time, that is, static typing. Checking types during compilation generally gives us more confidence about the program’s correctness, and by catching errors before the program is run, software development is cheaper (at least when humans are doing the programming).
With static checking, we write the semantics in two parts: a static semantics that enforces the compile-time rules, including type checking, but also access checking and argument-length checking. If the program “passes” the static semantics, that is, if the program has a static meaning, it will not encounter type errors at run time. We then define our dynamic semantics under the assumption we have a statically checked program.
This simplifies the dynamic semantics quite a bit.
It is a wonderful example of the engineering discipline of separation of concerns.
The static semantics evaluates each of the syntactic constructs in a context, $\Gamma$, which maps identifiers to their types and other relevant compile-time information, in our case, its access attribute (read-only or read-write). In the static semantics:
We’ll present the static semantics here and discuss in class.
The dynamic semantics assumes the program is statically legal, and therefore the dynamic semantic definition is now free of all the noisy types, read-write checks, undeclared variable checks, and so on. It’s a bit cleaner and easier to read:
The only run-time errors are division by zero and array index out of bounds.
TODO
TODO UNDER CONSTRUCTION
Concurrency is about things happening “at the same time.” The usual model is interleaved computation. For example:
x, y = 1, 2;
par {
x = y + 5 * y; // t0:=y, t1:=y, t2:=5*t1, t3:=t0+t2, x:=t3
y = x + 8; // t4:=x, t5:=t4+8, y:=t5
}
print x;
print y;
can have multiple results! One of which is [12,20]. Another is [54,9]. There are even more!
Determine all of the other possibilities.
Let’s add a new syntactic construct to execute two statements concurrently:
$s: \textsf{Statement} = \ldots \mid \texttt{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:
Here are some good papers and other references:
Here are some questions useful for your spaced repetition learning. Many of the answers are not found on this page. Some will have popped up in lecture. Others will require you to do your own research.
We’ve covered: