# How can denotational semantics be defined for imperative statements?

Denotational semantics associate each term in a program with some mathematical object representing the meaning of that term. When I see denotational semantics explained (e.g. in this answer), this is usually done for expressions; naturally, an expression in a programming language can correspond with a mathematical expression, and the correspondence is quite direct: the value of the expression in the programming language, when it's evaluated, would match the value of the mathematical expression it corresponds with.

However, for this to work, the behaviour of the expression in the programming language must be sufficiently similar to the behaviour of a mathematical expression. That is, it results in a value when it is evaluated, and evaluating it has no other observable behaviour (i.e. no side-effects). So this correspondence makes perfect sense for expressions in a pure-functional language, but the same correspondence wouldn't apply if one was trying to define denotational semantics for statements in an imperative language, which generally don't produce values and only have side-effects.

So, how can denotational semantics be defined for imperative statements or other side-effectful terms? What mathematical objects could they correspond with?

It occurs to me that the abstract syntax tree (AST) of the program could be seen as a mathematical object, such that terms in the program correspond with the AST nodes representing them. However, this just moves the problem somewhere else instead of solving it, since it would still be necessary to define the semantics for the AST nodes.

• Aug 2, 2023 at 16:47

# Statements as Functions

As suggested in coredump's comments, we generally interpret imperative statements as syntactic sugar for a function application. Side-effects are represented as usual in pure functional languages: the function takes additional arguments representing the current state and returns additional results representing the updated state (these details possibly wrapped up and hidden behind something like a state monad depending on your preferred mathematical representation).

For example, consider this toy Python function:

def f(x):
y = x + 1
y = x * y
return y


Under denotational semantics, we could desugar each of the three statements in its body as lambdas. Setting aside some technical issues that I will get into at the end of the answer, that could look something like

⟦y = x + 1⟧ = λ(x, y). (x, x + 1)

where the function takes in the old values of x and y as inputs and produces their new values as outputs. If we further define

⟦y = x * y⟧ = λ(x, y). (x, x * y)

and

⟦return y⟧ = λ(x, y). y,

then we can give denotational semantics for f by composing its statements:

⟦f⟧ = ⟦return y⟧ ∘ ⟦y = x * y⟧ ∘ ⟦y = x + 1⟧ = λx. x² + x

Or, if it's easier to see in Python (please assume Python 2 here, since Python 3 got rid of tuple destructuring in lambda parameters), we have essentially translated the original program to

increment = lambda (x, y): (x, x + 1)
multiply = lambda (x, y): (x, x * y)
return_y = lambda (x, y): y
f = lambda x: return_y(multiply(increment((x, None))))


which is something we could pretty directly write in a pure functional language using lets.

(If this desugaring looks familiar, that's probably because you've seen it with do notation in languages like Haskell, which makes sense to be the same, since the mutable variables can be thought of in terms of state monads. Similarly, more complicated statements, like loops, can be desugared in the same way you would desugar a loop written using do notation and a continuation monad.)

Now, of course, this does start to blur the line with small-step operational semantics, where we also explicate a "before" and "after" state and give a formula relating them. The main difference is one of perspective: in denotational semantics we are literally thinking of a statement as a mathematical object, and we are free to manipulate it like any other function, whereas in operational semantics we more or less ignore that the statement can be thought of this way and instead focus on how it tells us to change the program state.

# Compositionality

As David Young mentions in the comments, one issue that I've swept under the rug is how to decide on the signatures for these functions. For instance, do we curry the functions? How do we order the parameters and return values? Should the functions return values that we know by static analysis are unmodified? Etc.

No particular approach is wrong per se, in the sense that they will all give us correct results, but there is a convention to give every statement's interpretation the same signature: State → (State, Value).

Regarding side-effects on mutable variables, in the extreme, a State includes a partial map from variable names to values of type Value, and Value is a union type covering all possible values that can be stored in program variables. That means that every statement has the exact same signature, and we can compose them freely.

Alternatively, if we want to have a little more type safety, we can make the variable storage in State a partial dependent product that maps variables to values of the appropriate types, and read Value in State → (State, Value) as a placeholder for whatever type the statement returns, often the unit or bottom type since most statements have no return value. So, for example, the type of ⟦print('Hello, World!')⟧ would be State → (State, Unit) since a print statement does not return anything meaningful, whereas ⟦exit(0)⟧ might have type State → (State, Bottom) since execution cannot continue past this call.

Of course, State may contain other kinds of state needed to represent other language-relevant side-effects. (Alternatively, you could think of each kind of state as tracked by a separate state monad.) As the OP, kaya3 - support the strike, mentions in the comments, that's where you would track things like terminal output since writing just ⟦print('Hello, World!')⟧ = λs.(s, ()) would elide the print function's effect.

• This is definitely on the right track, but there is a difference from the usual approach. Usually, you represent the state as something like a partial mapping from variable names to values. For example, with the approach here you can't give the denotation of ⟦y = x * y⟧ without knowing other stuff about the code beyond what was given to ⟦-⟧ (which is not usually how you want a denotational semantics to work, since this goes against compositionality). You also can't use that denotation without knowing how much state is being used. Aug 2, 2023 at 19:27
• So, the usual approach would be for the denotation of a command to be a function with "type" State -> (State, Value), where State is a partial mapping from variable names to values and Value is whatever you're using to denote values. In the case of a command that does not give back a value, you can use the unit value. Then, all the denotations of all the commands have the "same shape" Aug 2, 2023 at 19:28
• @DavidYoung Indeed. I was trying sidestep those sorts of technical concerns to focus on what I see as the core idea, but perhaps it's better to address them. Give me a bit to edit the answer… Aug 2, 2023 at 19:34
• It's more of an issue than that, I'm afraid. The first thing isn't compositional, which is required for denotational semantics. Here, "compositional" means that the denotation of a term is determined exclusively by the denotations of its subterms. You usually define a semantics for an entire language: you want to define the semantic function for each kind of term. Imagine you want to define the denotation of assignments ⟦x = e⟧ = ... for an arbitrary variable x and an arbitrary expression e. But you don't know anything else about the program, due to compositionality. How do you do this? Aug 2, 2023 at 21:16
• @kaya3-supportthestrike Actually, you can think of IO actions in that way! This is how Haskell implements IO internally. You need to expand your picture of "state" to a representation of the entire physical world. In that case, print does update the state. You can't actually represent all the details of the universe in the computer, of course. But that doesn't stop you from treating it that way. And it works out! Aug 2, 2023 at 22:55