Semantics

Syntax vs. Semantics

The semantics of a language assigns a meaning to each utterance of the language. But where does this meaning come from? How it is assigned? It appears an inescapable fact that semantics is driven by the underlying structure of the utterances, not to each individual character. It is the arrangement of the characters that gives a program its particular meaning. The arrangement. The syntax. Generally semantics is given by mapping syntactic structures to their meaning.

Why Study Semantics?

I asked ChatGPT in late 2022.

Informal Semantic Descriptions

The traditional way to assign meanings to programs is with natural language. These descriptions, to be fair, try to be super precise. Let’s see an example. We’ll attempt an informal semantics of the language Astro we saw previously, when we covered Syntax. As a refresher, here’s the abstract syntax of the language:

$ \begin{array}{lcl} n: \mathsf{Nml} & & \\ i: \mathsf{Ide} & & \\ e: \mathsf{Exp} & = & n \mid i \mid -e \mid e+e \mid e-e \mid e\,\mathtt{*}\,e \mid e\,/\,e \mid e\,\mathtt{\%}\,e \mid e\,\mathtt{**}\,e \mid i\;e^*\\ s: \mathsf{Stm} & = & i = e \mid \mathtt{print}\;e\\ p: \mathsf{Pro} & = & \mathtt{program}\;s^+\\ \end{array}$

Let’s attempt a semantics in plain English (any other would do just as well), trying to be precise:

• A program executes its statements in order, generating a list of output values.
• Before the program begins, the following identifiers are bound like so:
  • The identifier π is bound to the number $\pi$.
  • The identifier sqrt is bound to the function that returns the square root of its sole argument, which must evaluate to a number.
  • The identifier sin is bound to to the function that returns the sine of its sole argument, which must evaluate to a number
  • The identifier cos is bound to to the function that returns the cosine of its sole argument, which must evaluate to a number
  • The identifier hypot is bound to to the function of two numeric arguments, $x$ and $y$ that returns $\sqrt{x^2+y^2}$
• The identifier π is a read-only identifier. All other identifiers are not read-only; we call them writable.
• An assignment statement evaluates its right hand side, an expression, then binds the identifier on its left hand side to this new numeric value; however the identifier must not have been previously assigned to, or if it had been, the identifier must be writable and bound to a number (not a function).
• A print statement evaluates its argument, then writes it to standard output.
• The unary and binary operator expressions evaluate their operands then do the obvious corresponding mathematical operation.
• A call expression evaluates its arguments, then calls the function bound to the identifier with these argument values. If the identifier was unbound or bound to a number (instead of a function), that is an error.
• An expression that is an identifier produces the value bound to that identifier, which must have been previously bound to a number (not a function).

Well that that was long-winded and who knows if we even caught everything?

In fact, the informal semantics above are terrible! There is so much imprecision! To get started, what does it be to be “bound”? What is “previously”? Let’s try to find more problems. There are quite a few!

And can you imagine doing this for a real language? It would take hundreds and hundreds of pages? Right? Right.

Well, it looks like we want a formal semantics. But what would that even look like? How do we formalize meaning?

Approaches to Formal Semantics

Let’s think of some ways we could capture the meaning of a program formally. Some things come to mind:

• We can show the effects of executing each construct on an abstract machine. (Operational)
• We can define functions that assign meanings in the form of mathematical objects to each construct. (Denotational)
• We can provide a formal logic allowing us to infer execution properties of programs via formal proof. (Axiomatic)

We can also mix elements of various approaches.

An Operational Approach

Let’s try to build a semantics for Astro, giving a set of rules which may be seen as simulating the execution of a program on some kind of abstract “machine.” For Astro, programs evaluate to the list of numbers they output. For example, the program:

x = 5;
print(sqrt(5 * 13 + 35));
print(3);
x = x + 21;
print(x / 8);

“evaluates to” the sequence $[10, 3, 3.25]$. So we want to define the relation $\Longrightarrow_P$ such that:

$p \Longrightarrow_P o$

means that program $p$ produces output $o$, where $o \in \mathbb{R}^*$ The evaluation relation for programs must be defined in terms of its constituent statements and its constituent expressions. But hmmm, we know that we want 3+2 to evaluate to $5$, but how do we evaluate x+3? It depends on what x is bound to, hence expressions must be evaluated in a context that contains a mapping from identifiers to the entities they are bound to. This mapping is called a memory (in the US, or a store in the UK). So we will write the evaluation relation for expressions as:

$e,m \Longrightarrow_E x$

meaning that in the context of memory $m$, expression $e$ evaluates to $x$. For statements, we notice that statements can both read and write memory, and they can append to the output. So:

$s,m,o \Longrightarrow_S (m', o')$

means that, if the context of memory $m$ with the output is currently $o$, then the execution of $s$ produces a new memory $m'$ and new output $o'$. Now we can define the operational semantics of Astro as follows (for brevity, dropping the subscripts on the evaluation relations since they can be inferred from context):

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

We’ve been able to capture the notion of the memory formally! In a memory, identifiers are bound to values that have one of four forms:

• $\mathsf{UNDEF}$, a value representing a value not being bound to anything. These can be nasty and require care in handling. But they are convenient. To handle it properly, we need to make sure our semantics never allows this value to be produced when evaluating an expression. But we did do this right above, check it out!
• $(\mathsf{NUM}, \mathit{value}, \mathit{access})$ for variables that are meant to hold numbers. Variables we create ourselves will be mutable, denoted $\mathsf{RW}$, for read-write; pre-defined variables like π will be immutable, denoted $\mathsf{RO}$ for read-only.
• $(\mathsf{FUN}, \mathit{value}, \mathit{numparams})$ for functions that will be called in expressions. These functions can take in any number of numeric parameters and always return a single number. Again, that is the language design. You might have designed it differently. In Astro, a call to a function that takes in $n$ parameters MUST receive $n$ arguments. The semantics enforces this.

Notice that a memory is a member of the following set:

$\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}$

That looks pretty formal, right? And while we’re at it, the relations themselves are also typed:

$\begin{array}{l} \Longrightarrow_P \subseteq \mathsf{Pro} \times \mathsf{Output} \\ \Longrightarrow_S \subseteq (\mathsf{Stm} \times \mathsf{Mem} \times \mathsf{Output}) \times (\mathsf{Mem} \times \mathsf{Output}) \\ \Longrightarrow_E \subseteq (\mathsf{Exp} \times \mathsf{Mem}) \times \mathbb{R} \end{array}$

where $\mathsf{Output}$ is just $\mathbb{R}^*$.

More about operational semantics

We’ve only given a very brief introduction. There’s so much more. There are many styles of operational semantics, and for the style we’ve presented here, you’ll find both “big-step” and “small-step” flavors. Much more to come.

A Denotational Approach

Let’s try something else. For each abstract syntax form, we’ll give a function mapping the form to its meaning, a mathematical object known as a denotation:

Think of $\bot$ for now as some kind of error thing. And any function application that has $\bot$ as an argument will automatically return $\bot$. We need to go into some pretty deep and gnarly and difficult mathematics to actually justify it. More on this later in the course. And oh, wait until you see what we need to do to justify recursive definitions. Get your inner mathematician ready.

We left a LOT out.

There is a great deal more to denotational semantics that what is shown here, but this gets us started. Entire books have been written on denotational semantics alone. There are many mathematical difficulties involved that need to be handled, particularly surrounding recursion. There is so much to cover.

It can be tough going mathematically, which is probably why operational semantics is a bit more popular.

Methodologies

Here are some methodologies that have evolved in the world of formal semantics:

Mathematics of Meaning

In the sneak peaks above you’ve just been given a taste of what formal semantic definitions look like.

How can we be sure they are truly formal, or truly unambiguous? What kind of mathematical objects work to covey the meaning of programs in a programming language? If your approach to semantics is super algebraic, you might want to check out Category Theory. But mostly, it’s the Lambda Calculus that everyone learns and knows and uses mostly.

We’ll study the Lambda Calculus pretty soon.

Resources

Where are some places to learn about semantics? Wikipedia is a good place to start:

• Semantics
• Semantics in Computer Science

There are a few books that cover formal semantics:

• Glynn Winskel, The Formal Semantics of Programming Languages, 1993.
• Hanne Riis Nielson and Flemming Nielson, Semantics with Applications, 1999.
• Kenneth Slonneger and Barry L. Kurtz, Formal Syntax and Semantics of Programming Languages, 1995.
• Matthew Hennessy, The Semantics of Programming Languages, Wiley, 1990.
• David Schmidt, Denotational Semantics, 1986.
• Carl A. Gunter, Semantics of Programming Languages, MIT Press, 1992.
• Michael J. C. Gordon, The Denotational Description of Programming Languages, Springer, 1979.

Also, I have course notes coming up for Operational, Denotational, and Axiomatic semantics. We’ll get to them soon.

Context, Again

Let’s revisit context once again.

What would you say about this Astro program?

print(x);

The grammar permits it, but the contextual constraint requiring all variables to have been previously assigned is violated. The program is illegal. The same goes for similar violations in many popular programming languages, such as:

• Use of undeclared identifiers
• Redeclaration of identifiers within a scope (unless overloading permitted)
• Use of an identifier where it may not have been initialized (only in some languages)
• Assignment to a read-only variable
• Modification of an immutable object
• Using an entity improperly (violating access controls, configuration attributes, etc.)
• Failure to call a private method
• Failure to use a local variable
• Match or switch not exhaustive
• Function in which all paths do not have an explicit return
• Wrong number of arguments passed to a function
• Passing r-values to reference parameters

But are these syntactically illegal or semantically illegal? We saw earlier you can say either:

In the semantics definitions for Astro above, we handled all the contextual rules in the semantics. In fact we completely conflated the static and dynamic semantics, mashing them both together in a single set of rules. In practice, you might see two sets of rules, one that just checks the contextual constraints, and the second defining the run-time behavior, under the assumption that the constraints have already been checked.

The terminology “static semantics” and “dynamic semantics” is in line with the two computer science terms:

You may have heard the terms “static” and “dynamic” in the context of type systems. Many people speak of a statically-typed language as one in which type checking is done prior to program execution and a dynamically typed language as one in which type checking is done during program execution. In reality, most languages do a little of both, but one or the other usually predominates.

Semantics in Practice

Formal semantics, and formal methods in general (e.g., proofs of correctness) seem to be underused in practice, except in certain life-critical domains. But the benefit of studying formal semantics leads to much more rigorous approaches to software correctness and security, a very good thing indeed.

Applying semantic rules at compile-time is part of what’s known as static analysis. During static analysis we look for outright errors, of course, but we also look for suspect practices that have the potential for errors or security vulnerabilities. This latter part of static analysis is necessarily outside the code of formal semantics, but it is an extremely important pragmatic issue that requires the developer’s full attention. To learn more about this area of static analysis, browse the following:

• List of (potential) Java bugs detectable by FindBugs™
• List of (potential) Java bugs detectable by PMD
• List of (potential) JavaScript bugs detectable by PMD
• The rules of ESLint

Summary