<p><a href="https://en.wikipedia.org/wiki/Denotational_semantics" rel="noreferrer">Denotational semantics</a> 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 <a href="https://langdev.stackexchange.com/a/2021/89">this answer</a>), 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.</p>
<p>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 <em>don't</em> produce values and only have side-effects.</p>
<p>So, how can denotational semantics be defined for imperative statements or other side-effectful terms? What mathematical objects could they correspond with?</p>
<p>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.</p>

<semantics><side-effects><denotational-semantics>
How can denotational semantics be defined for imperative statements?
CC BY-SA 4.0
2023-08-02T16:47:05.533Z
related https://cs.stackexchange.com/q/43115/29390
coredump
<h1>Statements as Functions</h1>
<p>As suggested in <a href="https://langdev.stackexchange.com/users/1356">coredump</a>'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).</p>
<p>For example, consider this toy Python function:</p>
<pre class="lang-py prettyprint-override"><code>def f(x):
    y = x + 1
    y = x * y
    return y
</code></pre>
<p>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</p>
<blockquote>
<p><code>⟦y = x + 1⟧ = λ(x, y). (x, x + 1)</code></p>
</blockquote>
<p>where the function takes in the old values of <code>x</code> and <code>y</code> as inputs and produces their new values as outputs.  If we further define</p>
<blockquote>
<p><code>⟦y = x * y⟧ = λ(x, y). (x, x * y)</code></p>
</blockquote>
<p>and</p>
<blockquote>
<p><code>⟦return y⟧ = λ(x, y). y</code>,</p>
</blockquote>
<p>then we can give denotational semantics for <code>f</code> by composing its statements:</p>
<blockquote>
<p><code>⟦f⟧ = ⟦return y⟧ ∘ ⟦y = x * y⟧ ∘ ⟦y = x + 1⟧ = λx. x² + x</code></p>
</blockquote>
<p>Or, if it's easier to see in Python (please assume Python 2 here, since Python 3 got rid of tuple destructuring in <code>lambda</code> parameters), we have essentially translated the original program to</p>
<pre class="lang-py prettyprint-override"><code>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))))
</code></pre>
<p>which is something we could pretty directly write in a pure functional language using <code>let</code>s.</p>
<p>(If this desugaring looks familiar, that's probably because you've seen it with <code>do</code> 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 <code>do</code> notation and a continuation monad.)</p>
<p>Now, of course, this does start to blur the line with small-step operational semantics, where we also explicate a &quot;before&quot; and &quot;after&quot; 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.</p>
<h1>Compositionality</h1>
<p>As <a href="https://langdev.stackexchange.com/users/172/">David Young</a> 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.</p>
<p>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: <code>State → (State, Value)</code>.</p>
<p>Regarding side-effects on mutable variables, in the extreme, a <code>State</code> includes a partial map from variable names to values of type <code>Value</code>, and <code>Value</code> 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.</p>
<p>Alternatively, if we want to have a little more type safety, we can make the variable storage in <code>State</code> a partial dependent product that maps variables to values of the appropriate types, and read <code>Value</code> in <code>State → (State, Value)</code> 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 <code>⟦print('Hello, World!')⟧</code> would be <code>State → (State, Unit)</code> since a print statement does not return anything meaningful, whereas <code>⟦exit(0)⟧</code> might have type <code>State → (State, Bottom)</code> since execution cannot continue past this call.</p>
<p>Of course, <code>State</code> 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, <a href="https://langdev.stackexchange.com/users/89/">kaya3 - support the strike</a>, mentions in the comments, that's where you would track things like terminal output since writing just <code>⟦print('Hello, World!')⟧ = λs.(s, ())</code> would elide the <code>print</code> function's effect.</p>

CC BY-SA 4.0
2023-08-02T19:04:21.907Z
2023-08-03T19:48:43.413Z
2023-08-03T19:48:43.413Z
Wheelwright
CC BY-SA 4.0
2023-08-02T19:27:04.327Z
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.
David Young
CC BY-SA 4.0
2023-08-02T19:28:33.527Z
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"
David Young
CC BY-SA 4.0
2023-08-02T19:34:34.877Z
@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…
Wheelwright
CC BY-SA 4.0
2023-08-02T21:16:58.703Z
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?
David Young
CC BY-SA 4.0
2023-08-02T22:55:40.783Z
@kaya3-supportthestrike Actually, you can think of IO actions in that way! This is [how Haskell implements `IO` internally](https://hackage.haskell.org/package/ghc-prim-0.10.0/docs/src/GHC.Types.html#line-244). You need to expand your picture of "state" to a representation of [the entire physical world](https://hackage.haskell.org/package/ghc-prim-0.10.0/docs/src/GHC.Prim.html#line-4945). 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!
David Young
# How can denotational semantics be defined for imperative statements?
Posted by: username_0 on 2023-08-02
[Denotational semantics](https://en.wikipedia.org/wiki/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](https://langdev.stackexchange.com/a/2021/89)), 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.
**Tags:** semantics side-effects denotational-semantics
> **Comments:**
> **username_1**: related https://cs.stackexchange.com/q/43115/29390  
---
## 1 answers
### Answer by username_2 on 2023-08-02. Score: 9 | Accepted answer
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.
> **Comments:**
> **username_3** (2023-08-02): 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.  
> **username_3** (2023-08-02): 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"  
> **username_2** (2023-08-02): @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…  
> **username_3** (2023-08-02): 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?  
> **username_3** (2023-08-02): @kaya3-supportthestrike Actually, you can think of IO actions in that way! This is [how Haskell implements `IO` internally](https://hackage.haskell.org/package/ghc-prim-0.10.0/docs/src/GHC.Types.html#line-244). You need to expand your picture of "state" to a representation of [the entire physical world](https://hackage.haskell.org/package/ghc-prim-0.10.0/docs/src/GHC.Prim.html#line-4945). 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!  
---
