Denotational semantics of expressions with side effects

Question

I'm doing revision for a module on programming language semantics and I'm having trouble understanding the introduction of side-effects in expressions.

We assume a standard syntax for arithmetic expression, with the four usual operations, plus the unary prefix and postfix operator $\texttt{++}$, defined as in language C, applicable to variables only as in $\texttt{V++}$, and assigment statement $\texttt{V:=E}$.

We have seen how to define the denotation function $[\![\texttt{E}]\!]_{\mathrm{Exp}}$ when we have to evaluate an expression $\texttt{E}$ without side-effect, to return a value resulting from that evaluation.

In order to give a denotational semantics for expressions with side-effects, we need to change the type of the denotation function $[\![\texttt{E}]\!]_{\mathrm{Exp}}$ for expressions $\texttt{E}$, so that it returns both the value of the expression and the state as modified by the side-effects. I.e., we want to define a denotation function

$[\![\texttt{E}]\!]_{\mathrm{Exp}} : State → Int×State$

by induction on the form of expressions $\texttt{E}$. For example, in the case $\texttt{E}$ has the form $\texttt{E1+E2}$, we define:

$[\![\texttt{E1+E2}]\!]_{\mathrm{Exp}}(S) = (n_1 + n_2, S_2)$

where $(n_1, S_1) = [\![\texttt{E1}]\!]_{\mathrm{Exp}}(S)$

and $(n_2, S_2) = [\![\texttt{E2}]\!]_{\mathrm{Exp}}(S_1)$

This says first evaluate the leftmost expression $\texttt{E1}$, giving the integer value $n_1$ and updated state $S_1$, then evaluate $\texttt{E2}$ in that updated state, giving the integer value $n_2$ and updated state $S_2$; the value of the expression is $n_1 + n_2$, and evaluation has the side effect of updating the state to $S_2$.

However this does not show when side effects actually take place, and I do not know how to write the denotation function for expressions that do produce side-effects. Can you tell me how to complete the inductive definition of $[\![\texttt{E}]\!]_{\mathrm{Exp}}$, including the case where $\texttt{E}$ is of the form $\texttt{V++}$?

Then, how should one change the definition of the denotation function $[\![\texttt{V:=E}]\!]_{\mathrm{Pgm}}$ for the assignment statement, to take account of the changes in the definition of $[\![\texttt{E}]\!]_{\mathrm{Exp}}$, which it necessarily uses?

Are there other changes that would need to be made to the denotational semantics of the language?

Answer 1

Since the question does not fully describe the language, I assume the simpler case when the $\texttt{++}$ operator applies only to variables given by an identifier, for example: $\texttt{foo++}$. Short of having more examples of the way you write denotational semantic, I have to improvise a bit. In particular, I avoid lambda notation since I do not know whether you are using it, but I would prefer using it.

Other arithmetic binary operators (substraction, multiplication) are similar to the $\texttt{E1+E2}$ case described in the question, and are explained similarly.

The simplest case is that of an expression which is only a lone variable $\texttt V$:

$[\![\texttt{V}]\!]_\mathrm{Exp}(S)= (S(\texttt V), S)$

What it says is to get the value $S(\texttt V)$ associated to the variable $\texttt V$ in the state $S$ and to return that value, of course, but associated with the state $S$ unchanged, since the type of the denotation function requires such a pair as result.

Then we complement as follow for the prefix and postfix $\texttt{++}$ operator the definition of the semantic function $Exp$ for expression $\texttt E$, when $\texttt E$ has the form $\texttt{V++}$ or $\texttt{++V}$, i.e., when it is a variable.

$[\![\texttt{V++}]\!]_\mathrm{Exp}(S)= (S(\texttt V), S1)$
where $S1(v_1)=\;\; \text{ if } v_1=\texttt V \;\text{ then } S(\texttt V)+1 \;\text{ else } S(v1)$

The value returned is the same as in the case of the variable $\texttt V$ alone. However, the state $S$ has to be changed to a new state $S1$ where the value corresponding to $\texttt V$ is incremented by $1$, the rest of the state being unchanged.

$[\![\texttt{++V}]\!]_\mathrm{Exp}(S)= (S(\texttt V)+1, S1)$
where $S1(v_1)=\;\;\text{ if }v_1=\texttt V \;\text{ then }S(\texttt V)+1\;\text{ else }S(v_1)$

This case is identical to the previous one, except for the fact that the value returned is also incremented by one, i.e. is the value provided by the state $S$ for $\texttt V$, but incremented by $1$. But the state $S1$ returned is the same as in the previous case.

For the assignment statement, it would be easier if the question included the definition of $[\![\texttt{V:=E}]\!]_\mathrm{Pgm}$ that is supposed to be modified. I am guessing, trying to be in accordance with what little information you give.

I suppose the result should be something like:

$\mathrm{[\![\texttt P]\!]_{Pgm} : State \to State}$

$[\![\texttt{V:=E}]\!]_\mathrm{Pgm}(S)= S2$
where $S2(v_1)=\;\; \text{ if } v_1=\texttt V \;\text{ then } n \;\text{ else } S1(v_1)$
and $(n,S1)= [\![\texttt E]\!]_\mathrm{Exp}(S)$

What this says in the first line is that the denotation of a statement is a function that takes a state as argument, and returns another state. The role of a statement is to modify the state.

Then the denotation function for the assignment statement $\texttt{V:=E}$ will first evaluate the expression $\texttt E$ in the environment $S$ provided as argument. This returns a value $n$ and a new environment $S1$ which may be different from $S$ if there have been side-effects while evaluating $\texttt E$. Then this environment $S1$ is modified into an environment $S2$ which associate the value $n$ to the variable $\texttt V$, and is otherwise identical to $S1$. This environment $S2$ is the one produced by execution of the assignment statement.

Other changes are probably necessary to fully account for side-effects in the language. But I cannot know exactly what because the question does not provide enough details about other language features. There are many ways to write denotational semantics, and it depends on the whole of the language and the way features interact.

The version given above is a bit simplified, assuming that $\texttt V$ is the actual variable name. I chose this simpler version because you do not provide examples of denotational semantics without side-effects, and I was not sure what presentation to choose. But there are other ways to present that.