patternMinor
Denotational semantics of expressions with side effects
Viewed 0 times
denotationalsemanticswithsideeffectsexpressions
Problem
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 for
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 for
Solution
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.
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.
Context
StackExchange Computer Science Q#43115, answer score: 5
Revisions (0)
No revisions yet.