Denotational semantics is one of those topics that tends to scare away people. The truth is that there are areas of denotational semantics that are very complicated but the basics are straightforward enough that anyone who isn’t afraid of mathematics should have no problem with it. I’m going to be using denotational semantics in future posts to suggest insights into programming languages so it seems like a good idea to try to make the topic accessible.

The basic idea behind denotational semantics is pretty simple: you define a function that maps phrases to their meaning based on the meanings of their parts. Let’s start with a simple language as an example. The language BC (for Bad Calculator) is a language of simple mathematical expressions. The syntax of BC is as follows:

expr ::= number-literal | expr + expr | - expr | ( expr )

This says that a phrase in BC is either a number literal (like 100 or 2.3) or it is two expressions joined by a “+” operator, or it is a single expression prefixed by “-”, or it is an expression in parentheses.

In denotational semantics, we like to be careful about specifying types of functions. It helps to avoid confusion. So we need a type for these syntactic objects to express the type of the denotational function. Let’s use Now, the meaning of a BC expression is a number, so we’ll use for the type of numbers and the type of the denotational function is. Let’s call this meaning functionso we write the function name and type like this:

You read this “ is a function mapping to ” or “ has type to ”.

The next step is to define what the function does. In regular mathematics it is common to use notation like this to define a function

For our purposes, we will modify that notation in several ways. First, we will leave off the parentheses and write:

Second, write multiple-clause functions like this:

where

Notice that we bring back the parentheses when they are needed for grouping and we have two different ways to pick out the right clause to use. One way is to provide a literal argument as in and the other way is to use a where clause.

Finally, we can’t really use phrases of BC directly in a notation like this. How would we describe the phrase “expr + expr”? We can’t very well write

expr + expr ...

Because that would be too confusing. We need to put some sort of quotes around the BC phrase:

“expr + expr” ...

That would work, but it’s a little wordy for us mathematical types. So we combine the quotes with the function name. Instead of using as the function name we use double square brackets and we would write the above as

[[ expr + expr ]] ...

This is read: “the meaning of a phrase ‘expr + expr’ is ...”.

One more problem with that form though. When we write the actual rule, we are going to have to distinguish between the first expression and the second one. This is usually done by providing subscripts:

[[ expr1 + expr2 ]] ...

Then in the “...” part we can tell them apart.

So here is the first clause of our meaning function:

[[ expr1 + expr2 ]] [[ expr1 ]] [[ expr2 ]]

We read this as: “the meaning of “expr + expr” is the meaning of the first expression plus the meaning of the second expression”. Doesn’t sound very revolutionary does it? But it really is saying something. We could have defined “expr + expr” to be anything; we didn’t have to use the standard definition of the plus symbol. When we get to more complicated languages, the meanings will get more interesting.

The next clause in our definition is similar

[[ -expr ]] [[ expr ]]

Again, this just says that the meaning of the negation sign is what you would expect.

A slightly more interesting clause is

[[ ( expr ) ]] [[ expr ]]

This says that a parenthesized expression just means what the expression means. It may be obvious, but this is the first definition that basically just throws away syntax. The parenthesis do not affect the semantics; they only affect the parsing of the phrase.

For atomic phrases (phrases with no parts) we will usually just punt and assume the existence of a function to define them as in

[[ number-literal ]] read(number-literal)

We read this as: “the meaning of a number-literal is the result of calling the function read on that literal”. The function read won’t be defined here but it should be obvious what it does. It just takes a phrase that looks like a number such as “44” or “36.5” and returns the number that it represents.

So here is the full definition of the meaning function on BC:

[[ number-literal ]] read(number-literal)

[[ expr1 + expr2 ]] [[ expr1 ]] [[ expr2 ]]

[[ -expr ]] [[ expr ]]

[[ ( expr ) ]] [[ expr ]]

OK, that’s all I’m going to write for this post until I find out if there is any way to post Google Docs with equations in Blogger.

Let’s expand our definition of BC to include names. We will expand the definition of a BC expression to include a let expression:

expr ::= let name=expr in expr

With this new syntax, we can write an expression like this in BC: