<p>The semantics of a language can be specified either by <a href="https://en.wikipedia.org/wiki/Denotational_semantics" rel="noreferrer">denotational semantics</a> or <a href="https://en.wikipedia.org/wiki/Operational_semantics" rel="noreferrer">operational semantics</a>. These are sometimes summarised as:</p>
<ul>
<li>Denotational semantics specify the &quot;meaning&quot; of terms in the language,</li>
<li>Operational semantics specify what happens when those terms when executed.</li>
</ul>
<p>The latter seems straightforward, and there are obvious reasons why we would want to specify what programs in our language do when we run them ─ such a specification in some sense tells you how to implement the language.</p>
<p>But what does it mean to mathematically specify what a program <em>means</em>, as opposed to what happens when you run it? And is such a specification useful for language designers or implementors?</p>

<semantics><denotational-semantics>
What are denotational semantics, and what are they useful for?
<h1>You could have invented denotational semantics!</h1>
<p>Suppose you want to know if some property about a program or a programming language holds. For example, you might wish to know whether a static analysis you’ve come up with provides a runtime guarantee. You could just write some tests to verify it empirically, but you can’t exhaustively test all possible cases, so this isn’t enough to say for certain there aren’t corner cases where it fails.</p>
<p>The only way to be completely certain is to <em>prove</em> your property, and this necessarily means you are entering the realm of mathematical reasoning. Proofs can be done to varying degrees of formality, but even an informal proof requires some structured plan of attack. Broadly speaking, there are two routes you might take:</p>
<ul>
<li><p>You could choose to phrase your property entirely <em>syntactically</em>. You can define the syntax of your language and define syntactic rules (like typechecking judgments and reduction rules) for analyzing and transforming its terms. Then you can perform proofs about what invariants these syntactic manipulations preserve.</p>
<p>One example of this technique is proving type soundness via progress and preservation. You can prove that it’s always possible to reduce a well-typed term until it reaches some value (progress) and that this reduction doesn’t change the expression’s type (preservation). These are mathematical statements about the language’s symbol-manipulation rules, but they refrain from assigning any particular <em>meaning</em> to the symbols. They just prove properties about what the typechecker and evaluator happen to do.</p>
<p>This syntactic approach is known as <a href="https://en.wikipedia.org/wiki/Operational_semantics" rel="noreferrer"><strong>operational semantics</strong></a> because the analysis is performed on a model of the language’s actual operational mechanisms: typechecking judgments correspond to a typechecker, and reduction rules correspond to an evaluator.</p>
</li>
<li><p>A second approach would be to phrase your property <em>semantically</em>. You could say that numbers in your programming language <em>mean</em> (correspond to) mathematical numbers, and a lambda term <em>means</em> a mathematical function. That is, for each term in your language, you can map its syntax onto some mathematical concept that reflects its structure.</p>
<p>An immediate advantage of doing this is that we already know lots of properties about mathematical structures. If your mapping from syntactic terms to mathematical objects is an <em>adequate</em> model for your language—that is, equivalences in your denotational model imply equivalences in an operational model and vice versa—you can now reason about your programs entirely in terms of the realm of mathematical objects! This lets you get away from worrying about nitty-gritty syntactic details that are otherwise uninteresting bookkeeping.</p>
<p>For example, in purely a syntactic approach, <code>(x + y) + z</code> is a different term from <code>x + (y + z)</code>, and you cannot simply treat them as interchangeable. However, if numbers in your language really do work just like mathematical numbers, then you can work in the language of mathematics, and the distinction ceases to exist.</p>
<p>Since this approach chooses to interpret the syntactic terms of the programming language by giving them some mathematical meaning, or <em>denotation</em>, we call this approach <a href="https://en.wikipedia.org/wiki/Denotational_semantics" rel="noreferrer"><strong>denotational semantics</strong></a>.</p>
</li>
</ul>
<p>One way to think about denotational semantics is that it does some work up front to translate terms of a programming language into a domain-specific language for doing reasoning: mathematics. In this sense, it’s not entirely unlike the way a compiler desugars a source language into a simpler IR that is easier to work with. However, instead of simply mapping terms into a smaller, simpler grammar, we’re mapping them into a mathematical domain.</p>
<h2>A brief illustration</h2>
<p>Suppose we want to provide a denotational semantics for the following extremely simple arithmetic language:
<span class="math-container">$$\begin{array}{rcl}
\mathit{expr} \hskip{-10mu}&amp;::=&amp;\hskip{-10mu} \mathsf{zero}\\
&amp;|&amp;\hskip{-10mu} \mathsf{succ}(\mathit{expr})\\
&amp;|&amp;\hskip{-10mu} \mathsf{add}(\mathit{expr}, \mathit{expr})\\
&amp;|&amp;\hskip{-10mu} \mathsf{mul}(\mathit{expr}, \mathit{expr})
\end{array}
$$</span>
(Here, <span class="math-container">$\mathsf{succ}$</span> is the <a href="https://en.wikipedia.org/wiki/Successor_function" rel="noreferrer">successor function</a>.)</p>
<p>First, we need to pick a mathematical domain to map these syntactic terms into. Since this language represents arithmetic on natural numbers, we’ll choose ℕ, the set of natural numbers, as our mathematical domain.</p>
<p>Next, we need to actually define the mapping from syntactic terms to our domain. To do this, we traditionally use the notation <span class="math-container">$⟦x⟧$</span> to mean “the denotation of <span class="math-container">$x$</span>”. (The <span class="math-container">$⟦\,⟧$</span> brackets themselves are usually called “double square brackets” or “white brackets”.) For our language, we could therefore define our semantics this way:
<span class="math-container">$$\begin{aligned}
⟦\,\mathsf{zero}\,⟧ &amp;:= 0 \\
⟦\,\mathsf{succ}(x)\,⟧ &amp;:= ⟦\,x\,⟧ + 1 \\
⟦\,\mathsf{add}(x,y)\,⟧ &amp;:= ⟦\,x\,⟧ + ⟦\,y\,⟧ \\
⟦\,\mathsf{mul}(x,y)\,⟧ &amp;:= ⟦\,x\,⟧ × ⟦\,y\,⟧
\end{aligned}
$$</span>
Assuming this is, in fact, an adequate model for our language, we can now prove things about <em>programs</em> by taking advantage of facts we already know about <em>mathematics</em>. For example, we can prove that
<span class="math-container">$$
\mathsf{add}(x,y) ≡ \mathsf{add}(y,x)
$$</span>
via the argument
<span class="math-container">$$\begin{aligned}
⟦\,\mathsf{add}(x,y)\,⟧ &amp;= ⟦\,x\,⟧ + ⟦\,y\,⟧\\
&amp;= ⟦\,y\,⟧ + ⟦\,x\,⟧ \\ &amp;= ⟦\,\mathsf{add}(y,x)\,⟧
\end{aligned}$$</span>
which uses the commutativity of addition on natural numbers. If we were to prove the same property using operational semantics, we’d need to make an inductive argument about the language’s evaluator, which would be significantly more involved!</p>
<p>Denotational semantics of real programming languages is, of course, significantly more involved, but a full discussion is well outside the scope of this answer. However, the essential process is the same: select a domain, map each of the terms of your language onto that domain, and then write proofs that take advantage of the structure of the domain.</p>
<h2>The choice of domain</h2>
<p>For many languages, the interpretation of its terms may seem “obvious”. For example, it might seem like numbers in the programming language “ought” to be mapped onto mathematical numbers, and functions “ought” to be mapped onto mathematical functions. However, in practice, this is often <em>not</em> the most useful approach, for a few reasons:</p>
<ul>
<li><p>Programming language concepts often do <em>not</em> correspond precisely to the mathematical concepts we informally think of them as. For example, mathematical natural numbers satisfy the following property:
<span class="math-container">$$
\forall\, n ∈ ℕ.\: n + 1 &gt; 0
$$</span>
However, fixed-size unsigned integers in programming languages do not! Therefore, natural numbers are not a semantically valid interpretation for fixed-size unsigned integers. Instead, the more complicated domain of integers modulo <span class="math-container">$2^n$</span> must be used.</p>
</li>
<li><p>Some expressions in a programming language might not correspond to <em>any</em> value in the mathematical sense, such as <code>exit(-1)</code>. In these cases, it may be useful to map expressions of this sort onto some token value in the target domain, often notated as <span class="math-container">$⊥$</span> or <span class="math-container">$↯$</span>.</p>
</li>
<li><p>Imperative features like mutable state require some additional structure to model mathematically. There are often many different ways to represent that structure, and which one is the most useful may depend on what properties you’re trying to prove.</p>
</li>
<li><p>Capturing recursive functions or other potentially-unbounded structures can be mathematically challenging, so much so that we have an entirely separate question dedicated to it: <a href="https://langdev.stackexchange.com/questions/1953/how-can-i-understand-a-recursive-function-in-terms-of-denotational-semantics">How can we define a denotational semantics for recursive functions?</a></p>
</li>
<li><p>In some cases, there may be structure in your language you explicitly <em>don’t</em> want to preserve. For example, there may be expressions that are distinguishable within your language, but they are interchangeable from the perspective of the property you’re trying to prove. Therefore, you may choose to map several different values in your source language onto the same object in your mathematical domain, which is a form of <a href="https://en.wikipedia.org/wiki/Abstract_interpretation" rel="noreferrer">abstract interpretation</a>.</p>
</li>
</ul>
<p>Sometimes, finding the most useful domain to interpret your syntax in is actually the hardest part of proving something using denotational semantics! Indeed, this reflects the idea that denotational semantics is about “getting into the right language” to be able to prove something.</p>

CC BY-SA 4.0
2023-07-04T23:34:40.640Z
2023-08-11T18:34:53.273Z
2023-08-11T18:34:53.273Z
Alexis King
CC BY-SA 4.0
2023-07-18T12:54:05.430Z
Could you recommend some reference to learn about denotational semantics?
Pablo H
CC BY-SA 4.0
2023-07-27T19:34:35.210Z
@PabloH A classic reference is the book *"The Formal Semantics of Programming Languages: An Introduction"* by Glynn Winskel. I've also found the book *"Semantics of Programming Languages: Structures and Techniques"* by Carl A. Gunter helpful. Another good one is the strangely titled, but influential paper [*"A type-theoretical alternative to ISWIM, CUCH, OWHY"*](https://www.cs.cmu.edu/~crary/819-f09/Scott93.pdf) by Dana Scott, who is one of the originators of denotational semantics.
David Young
CC BY-SA 4.0
2023-07-27T19:36:19.370Z
@PabloH Another one is what I believe is the original paper on denotational semantics [*"Towards A Mathematical Semantics For Computer Languages"*](https://www.cs.cmu.edu/~crary/819-f09/Scott71.pdf) by Scott and Strachey. It begins with a description of the fundamental ideas and goals of denotational semantics.
David Young
CC BY-SA 4.0
2023-07-27T20:04:50.713Z
A good starting point would be to at least read the introduction to that last paper I mentioned (the one by Scott and Strachey), since it provides important background. It also describes the distinction between syntax and semantics (as an example, they contrast numerals with numbers). Then, the books would be good. The other paper by Scott describes a specific denotational semantics (one which is close to the one I describe in [my answer here](https://langdev.stackexchange.com/a/1954/172), though more fleshed out and with more features).
David Young
CC BY-SA 4.0
2024-01-08T22:19:30.023Z
"adequate model for your language—that is, equivalences in your denotational model imply equivalences in an operational model and vice versa"

Adequacy means that terms with different termination behavior are not equal under denotational semantics. That's cool, but often you actually care about *observational equivalence* of expressions, e.g., expressions are equal when their termination behavior coincides *in all syntactic contexts*.
Sebastian Graf
CC BY-SA 4.0
2024-01-08T22:22:24.800Z
The definitional equivalence relation on most denotational domains is however much *finer* than observational equivalence, to the point that it becomes impossible to prove useful theorems that hold observationally. E.g., it is often possible to poke at denotations of two obs. equivalent expressions with domain elements outside the range of the semantics such that you can tell them apart. Finding an equivalence relation that is as coarse as observational equivalence is called the "full abstraction" problem. I know this because I underestimated the gravity of it for the proofs I were conducting
Sebastian Graf
CC BY-SA 4.0
2023-08-15T21:35:02.520Z
I don't agree with this answer. It makes an artificial distinction between "mathematical concept"  and operational semantics. But the structures you use to define operational semantics  (such as labelled transition systems) are themselves perfectly mathematical. Moreover, for almost all programming languages, whether C++ or Rust or Haskell, or X86 semantics there is no known denotational semantics in the the answer of the question.
Martin Berger
CC BY-SA 4.0
2023-08-15T21:36:10.310Z
I'd say that the spirit of denotational semantics is that proofs tend to look more compositional, at least on the surface.
Martin Berger
# What are denotational semantics, and what are they useful for?
Posted by: username_0 on 2023-07-04
The semantics of a language can be specified either by [denotational semantics](https://en.wikipedia.org/wiki/Denotational_semantics) or [operational semantics](https://en.wikipedia.org/wiki/Operational_semantics). These are sometimes summarised as:

* Denotational semantics specify the "meaning" of terms in the language,
* Operational semantics specify what happens when those terms when executed.

The latter seems straightforward, and there are obvious reasons why we would want to specify what programs in our language do when we run them ─ such a specification in some sense tells you how to implement the language.

But what does it mean to mathematically specify what a program *means*, as opposed to what happens when you run it? And is such a specification useful for language designers or implementors?
**Tags:** semantics denotational-semantics
---
## 1 answers
### Answer by username_1 on 2023-07-04. Score: 19 | Accepted answer
# You could have invented denotational semantics!

Suppose you want to know if some property about a program or a programming language holds. For example, you might wish to know whether a static analysis you’ve come up with provides a runtime guarantee. You could just write some tests to verify it empirically, but you can’t exhaustively test all possible cases, so this isn’t enough to say for certain there aren’t corner cases where it fails.

The only way to be completely certain is to *prove* your property, and this necessarily means you are entering the realm of mathematical reasoning. Proofs can be done to varying degrees of formality, but even an informal proof requires some structured plan of attack. Broadly speaking, there are two routes you might take:

* You could choose to phrase your property entirely *syntactically*. You can define the syntax of your language and define syntactic rules (like typechecking judgments and reduction rules) for analyzing and transforming its terms. Then you can perform proofs about what invariants these syntactic manipulations preserve.

  One example of this technique is proving type soundness via progress and preservation. You can prove that it’s always possible to reduce a well-typed term until it reaches some value (progress) and that this reduction doesn’t change the expression’s type (preservation). These are mathematical statements about the language’s symbol-manipulation rules, but they refrain from assigning any particular *meaning* to the symbols. They just prove properties about what the typechecker and evaluator happen to do.

  This syntactic approach is known as [**operational semantics**](https://en.wikipedia.org/wiki/Operational_semantics) because the analysis is performed on a model of the language’s actual operational mechanisms: typechecking judgments correspond to a typechecker, and reduction rules correspond to an evaluator.
* A second approach would be to phrase your property *semantically*. You could say that numbers in your programming language *mean* (correspond to) mathematical numbers, and a lambda term *means* a mathematical function. That is, for each term in your language, you can map its syntax onto some mathematical concept that reflects its structure.

  An immediate advantage of doing this is that we already know lots of properties about mathematical structures. If your mapping from syntactic terms to mathematical objects is an *adequate* model for your language—that is, equivalences in your denotational model imply equivalences in an operational model and vice versa—you can now reason about your programs entirely in terms of the realm of mathematical objects! This lets you get away from worrying about nitty-gritty syntactic details that are otherwise uninteresting bookkeeping.

  For example, in purely a syntactic approach, `(x + y) + z` is a different term from `x + (y + z)`, and you cannot simply treat them as interchangeable. However, if numbers in your language really do work just like mathematical numbers, then you can work in the language of mathematics, and the distinction ceases to exist.

  Since this approach chooses to interpret the syntactic terms of the programming language by giving them some mathematical meaning, or *denotation*, we call this approach [**denotational semantics**](https://en.wikipedia.org/wiki/Denotational_semantics).

One way to think about denotational semantics is that it does some work up front to translate terms of a programming language into a domain-specific language for doing reasoning: mathematics. In this sense, it’s not entirely unlike the way a compiler desugars a source language into a simpler IR that is easier to work with. However, instead of simply mapping terms into a smaller, simpler grammar, we’re mapping them into a mathematical domain.

## A brief illustration

Suppose we want to provide a denotational semantics for the following extremely simple arithmetic language:
$$\begin{array}{rcl}
\mathit{expr} \hskip{-10mu}&::=&\hskip{-10mu} \mathsf{zero}\\
&|&\hskip{-10mu} \mathsf{succ}(\mathit{expr})\\
&|&\hskip{-10mu} \mathsf{add}(\mathit{expr}, \mathit{expr})\\
&|&\hskip{-10mu} \mathsf{mul}(\mathit{expr}, \mathit{expr})
\end{array}
$$
(Here, $\mathsf{succ}$ is the [successor function](https://en.wikipedia.org/wiki/Successor_function).)

First, we need to pick a mathematical domain to map these syntactic terms into. Since this language represents arithmetic on natural numbers, we’ll choose ℕ, the set of natural numbers, as our mathematical domain.

Next, we need to actually define the mapping from syntactic terms to our domain. To do this, we traditionally use the notation $⟦x⟧$ to mean “the denotation of $x$”. (The $⟦\,⟧$ brackets themselves are usually called “double square brackets” or “white brackets”.) For our language, we could therefore define our semantics this way:
$$\begin{aligned}
⟦\,\mathsf{zero}\,⟧ &:= 0 \\
⟦\,\mathsf{succ}(x)\,⟧ &:= ⟦\,x\,⟧ + 1 \\
⟦\,\mathsf{add}(x,y)\,⟧ &:= ⟦\,x\,⟧ + ⟦\,y\,⟧ \\
⟦\,\mathsf{mul}(x,y)\,⟧ &:= ⟦\,x\,⟧ × ⟦\,y\,⟧
\end{aligned}
$$
Assuming this is, in fact, an adequate model for our language, we can now prove things about *programs* by taking advantage of facts we already know about *mathematics*. For example, we can prove that
$$
\mathsf{add}(x,y) ≡ \mathsf{add}(y,x)
$$
via the argument
$$\begin{aligned}
⟦\,\mathsf{add}(x,y)\,⟧ &= ⟦\,x\,⟧ + ⟦\,y\,⟧\\
&= ⟦\,y\,⟧ + ⟦\,x\,⟧ \\ &= ⟦\,\mathsf{add}(y,x)\,⟧
\end{aligned}$$
which uses the commutativity of addition on natural numbers. If we were to prove the same property using operational semantics, we’d need to make an inductive argument about the language’s evaluator, which would be significantly more involved!

Denotational semantics of real programming languages is, of course, significantly more involved, but a full discussion is well outside the scope of this answer. However, the essential process is the same: select a domain, map each of the terms of your language onto that domain, and then write proofs that take advantage of the structure of the domain.

## The choice of domain

For many languages, the interpretation of its terms may seem “obvious”. For example, it might seem like numbers in the programming language “ought” to be mapped onto mathematical numbers, and functions “ought” to be mapped onto mathematical functions. However, in practice, this is often *not* the most useful approach, for a few reasons:

* Programming language concepts often do *not* correspond precisely to the mathematical concepts we informally think of them as. For example, mathematical natural numbers satisfy the following property:
  $$
  \forall\, n ∈ ℕ.\: n + 1 > 0
  $$
  However, fixed-size unsigned integers in programming languages do not! Therefore, natural numbers are not a semantically valid interpretation for fixed-size unsigned integers. Instead, the more complicated domain of integers modulo $2^n$ must be used.
* Some expressions in a programming language might not correspond to *any* value in the mathematical sense, such as `exit(-1)`. In these cases, it may be useful to map expressions of this sort onto some token value in the target domain, often notated as $⊥$ or $↯$.
* Imperative features like mutable state require some additional structure to model mathematically. There are often many different ways to represent that structure, and which one is the most useful may depend on what properties you’re trying to prove.
* Capturing recursive functions or other potentially-unbounded structures can be mathematically challenging, so much so that we have an entirely separate question dedicated to it: [How can we define a denotational semantics for recursive functions?](https://langdev.stackexchange.com/questions/1953/how-can-i-understand-a-recursive-function-in-terms-of-denotational-semantics)
* In some cases, there may be structure in your language you explicitly *don’t* want to preserve. For example, there may be expressions that are distinguishable within your language, but they are interchangeable from the perspective of the property you’re trying to prove. Therefore, you may choose to map several different values in your source language onto the same object in your mathematical domain, which is a form of [abstract interpretation](https://en.wikipedia.org/wiki/Abstract_interpretation).

Sometimes, finding the most useful domain to interpret your syntax in is actually the hardest part of proving something using denotational semantics! Indeed, this reflects the idea that denotational semantics is about “getting into the right language” to be able to prove something.
> **Comments:**
> **username_2** (2023-07-18): Could you recommend some reference to learn about denotational semantics?  
> **username_3** (2023-07-27): @PabloH A classic reference is the book *"The Formal Semantics of Programming Languages: An Introduction"* by Glynn Winskel. I've also found the book *"Semantics of Programming Languages: Structures and Techniques"* by Carl A. Gunter helpful. Another good one is the strangely titled, but influential paper [*"A type-theoretical alternative to ISWIM, CUCH, OWHY"*](https://www.cs.cmu.edu/~crary/819-f09/Scott93.pdf) by Dana Scott, who is one of the originators of denotational semantics.  
> **username_3** (2023-07-27): @PabloH Another one is what I believe is the original paper on denotational semantics [*"Towards A Mathematical Semantics For Computer Languages"*](https://www.cs.cmu.edu/~crary/819-f09/Scott71.pdf) by Scott and Strachey. It begins with a description of the fundamental ideas and goals of denotational semantics.  
> **username_3** (2023-07-27): A good starting point would be to at least read the introduction to that last paper I mentioned (the one by Scott and Strachey), since it provides important background. It also describes the distinction between syntax and semantics (as an example, they contrast numerals with numbers). Then, the books would be good. The other paper by Scott describes a specific denotational semantics (one which is close to the one I describe in [my answer here](https://langdev.stackexchange.com/a/1954/172), though more fleshed out and with more features).  
> **username_5** (2023-08-15): I don't agree with this answer. It makes an artificial distinction between "mathematical concept"  and operational semantics. But the structures you use to define operational semantics  (such as labelled transition systems) are themselves perfectly mathematical. Moreover, for almost all programming languages, whether C++ or Rust or Haskell, or X86 semantics there is no known denotational semantics in the the answer of the question.  
> **username_5** (2023-08-15): I'd say that the spirit of denotational semantics is that proofs tend to look more compositional, at least on the surface.  
> **username_4** (2024-01-08): "adequate model for your language—that is, equivalences in your denotational model imply equivalences in an operational model and vice versa"

Adequacy means that terms with different termination behavior are not equal under denotational semantics. That's cool, but often you actually care about *observational equivalence* of expressions, e.g., expressions are equal when their termination behavior coincides *in all syntactic contexts*.  
> **username_4** (2024-01-08): The definitional equivalence relation on most denotational domains is however much *finer* than observational equivalence, to the point that it becomes impossible to prove useful theorems that hold observationally. E.g., it is often possible to poke at denotations of two obs. equivalent expressions with domain elements outside the range of the semantics such that you can tell them apart. Finding an equivalence relation that is as coarse as observational equivalence is called the "full abstraction" problem. I know this because I underestimated the gravity of it for the proofs I were conducting  
---
