\chapter{Denotational Semantics}
\label{chap:denotational-semantics}

We review a third way to specify the semantics of a programming language:
denotational semantics. Denotational semantics directly specifies the
meaning of programs as a mathematical object. If operational semantics
corresponds to an idealized interpreter and Hoare logic corresponds to an
idealized verifier, then denotational semantics corresponds to an idealized
compiler.

The core of this chapter is modeled closely after Chapter~11 of \emph{Concrete
Semantics:\ With Isabelle\slash HOL}~\cite{nipkow-klein-2014}.

\section{Compositionality}
\label{sec:compositionality}

A \emph{denotational semantics} defines the meaning of each program as a
mathematical object. Abstractly, it can be viewed as a function
%
\[\hbox{\lic{⟦ ⟧}~\lic{:}~\text{syntax}~\lic{→}~\text{semantics}}\]
%
A key property of denotational semantics is \emph{compositionality}: The
meaning of a compound statement should be defined in terms of the
meaning of its components. Consider the straightforward definition
%
\[\hbox{\lic$⟦S⟧ = {(s, t) | (S, s) ⟹ t}$}\]
%
in terms of the big-step semantics (\li{⟹}). Actually, because Lean supports
only variables on the left-hand side of the vertical bar, we must write
%
\[\hbox{\lic$⟦S⟧ = {st | (S, prod.fst st) ⟹ prod.snd st}$}\]
%
This definition specifies the desired semantics, but it does not qualify
as a denotational semantics due to lack of compositionality: The meaning of
the compound statements (sequential composition, \li{if then else}, and
\li{while}) is given directly, without using the denotation of their components.

A fully compositional definition allows us to reason equationally about
programs, which is often more convenient than using the introduction,
elimination, and inversion principles of~\li{⟹}. In essence, we want
structurally recursive equations of the form
%
\begin{center}
\begin{tabular}{@{}r@{}l@{}}
\li|⟦S ; T⟧| & \li| = … ⟦S⟧ … ⟦T⟧ …| \\
\li|⟦if b then S else T⟧| & \li| = … ⟦S⟧ … ⟦T⟧ …| \\
\li|⟦while b do S⟧| & \li| = … ⟦S⟧ …|
\end{tabular}
\end{center}
%
with no occurrences of \li{S} and \li{T} in the right-hand sides except
as arguments to \li{⟦ ⟧}.

An evaluation function for arithmetic expressions
%
\[
\hbox{\lic{eval}}~\hbox{\lic{:}}~\underbrace{\hbox{\lic{aexp}}}_\text{syntax}~
\hbox{\lic{→}}~\underbrace{\hbox{\lic{(string → ℤ) → ℤ}}}_\text{semantics}
\]
%
satisfying equations such as
\[
\hbox{\li{eval (aexp.add e₁ e₂) env = eval e₁ env + eval e₂ env}}
\]
is a denotational semantics, because the semantics of \li{aexp.add}
\hbox{\li{e₁ e₂}} is defined in terms of the semantics of \li{e₁} and of~\li{e₂}.

Denotational semantics are a natural match for arithmetic expressions but also
functional programs. Now we want a convenient denotational semantics for
imperative programs. Because of \li{while} loops, which are not guaranteed to
terminate, we need to develop some additional mathematical notions to reach the
point where we can formulate the desired semantics.

\section{A Relational Denotational Semantics}
\label{sec:a-relational-denotational-semantics}

Denotational semantics for deterministic languages are normally given as a
\relax{function} from prestate to poststate, but \relax{relations} are more
general and more convenient to manipulate. We present a relational denotational
semantics.

A denotational semantics of a program will be a mathematical object of type
\li{set (state × state)}.
The relational approach was also used for the big-step semantics, which took
the form of a predicate of type \li{state → state → Prop}. These two types are
isomorphic, but \li{set α}, defined as \li{α → Prop}, supports convenient
operations and notations, such as \li{∅}, \li{∪}, \li{∩}, \li{∈}, and
\li${… | …}$ (Section~\ref{sec:nondeterminism}).

Our semantics is called \li{denote}, with \li{⟦}\,\li{⟧} as syntactic sugar. We
start with the first four equations of the definition, keeping \li{while} for
later:
%
\lstinputlisting[linerange=denote_first_lines-q]{../lean/love10_denotational_semantics_demo_master.lean}

The \li{skip} statement is interpreted as the identity relation over
states---i.e., the set of all tuples of the form \li{(s, s)}. This captures
the desired semantics of \li{skip}: The poststate is always identical to the
prestate.

The semantics of assignment is the set of tuples where the second component
reflects the result of the assignment.

The semantics of sequential composition is elegantly expressed as a relational
composition \li{◯}, which is defined such that
%
\[\hbox{\tabletsmall\li$r₁ ◯ r₂ = {ac | ∃b, (prod.fst ac, b) ∈ r₁ ∧ (b, prod.snd ac) ∈ r₂}$}\]

The semantics of \li{if then else} is given as the union of the semantics of the
two branches, restricted to include only the tuples whose
first component makes the Boolean condition true or false, depending on the
branch. The restriction operator is defined by
%
\[\hbox{\li$r ⇃ p = {ab | p (prod.fst ab) ∧ ab ∈ r}$}\]

The difficulties arise when we try to define the semantics of \li{while} loops.
We would like to write
%
\begin{lstlisting}
| (stmt.while b S)  :=
  ((denote S ◯ denote (stmt.while b S)) ⇃ b)
  ∪ (Id ⇃ (λs, ¬ b s))
\end{lstlisting}
%
but this is ill-founded due to the recursive call on \li{stmt.while b S}. We
need something else. What we are looking for on the right-hand side is some
term \li{X} that satisfies the equation
%
\[\hbox{\li{X = ((denote S ◯ X) ⇃ b) ∪ (Id ⇃ (λs, ¬ b s))}}\]
%
We are looking for what mathematicians call a fixpoint. The next four sections
are concerned with building an operator \li{lfp} that computes the fixpoint for
a given equation. Using \li{lfp}, we will be able to define the
semantics of \li{while} loops by
%
\lstinputlisting[linerange=denote_last_line-q]{../lean/love10_denotational_semantics_demo_master.lean}

\section{Fixpoints}
\label{sec:fixpoints}

A \emph{fixpoint} (or \emph{fixed point}) of \li{f} is a solution for \li{X}
in the equation
\[\hbox{\li{X = f X}}\]
In general, fixpoints may not exist at all for some \li{f} (e.g., \li{f := nat.succ}),
or there may be several fixpoints (e.g., \li{f := (λx, x)}).
Under some conditions on \li{f}, a unique \emph{least fixpoint} and a
unique \emph{greatest fixpoint} are guaranteed to exist.

Consider the following fixpoint equation, with \li{X : ℕ → Prop}:
%
\[\hbox{\lic{X = (λn : ℕ, n = 0 ∨ (∃m : ℕ, n = m + 2 ∧ X m))}}\]
%
This equation is the $\beta$-reduced variant of an equation with the right
format:
%
\[\hbox{\lic{X =}}~\overbrace{\hbox{\lic{(λ(p : ℕ → Prop) (n : ℕ), n = 0 ∨ (∃m : ℕ, n = m + 2 ∧ p m))}}}^{\smash{\textstyle\texttt{f}}}~\hbox{\lic{X}}\]
%
A solution is \li{X := even}, the predicate that characterizes the even natural
numbers. Recall that we proved the inversion rule
%
\[\hbox{\lic{even n ↔ n = 0 ∨ (∃m : ℕ, n = m + 2 ∧ even m)}}\]
%
in Section~\ref{sec:elimination}.
It turns out that \li{even} is the only fixpoint. In general,
the least and greatest fixpoint may be different. Consider the equation
\[\hbox{\li{X = (λp, p) X}}\]
for \li{X : ℕ → Prop}.
The least fixpoint is \li{λ_, False} and the greatest fixpoint is
\hbox{\li{λ_}\verb|,|} \hbox{\li{True}.} By convention, we have \li{False < True} and
thus \hbox{\li{(λ_, False) < (λ_, True)}.} Similarly, \li{∅ < @set.univ α} for
any inhabited type \li{α}.

For the semantics of \li{while} loops, \li{X} will have type
\li{set (state} \li{× state)} of relations between states, and \li{f} will
correspond to either taking one extra iteration of the loop (if the condition
\li{b} is true) or the identity (if \li{b} is false).

Which fixpoint should we use for the semantics of \li{while}? A program should
be prohibited from looping infinitely. Each time a loop is executed, it must
terminate after some number~\li{n} of iterations. Let \li{f}$^\texttt{n}$ denote
the \li{n}-fold composition of \li{f}, corresponding to performing at most
\li{n}~iterations. We have \li{X = f}$^\texttt{n}$\li{(∅)} in this case.
If we do not know the value of \li{n} ahead of time, we can always take
%
\[\hbox{\li{X = f}$^\texttt{0}$\li{(∅) ∪ f}$^\texttt{1}$\li{(∅) ∪ f}$^\texttt{2}$\li{(∅) ∪ ⋯}}\]
%
By Kleene's fixpoint theorem,%
\footnote{\url{https://en.wikipedia.org/wiki/Kleene_fixed-point_theorem}}
such an \li{X} is equal to the least fixpoint \li{lfp f}. The
greatest fixpoint would also allow cyclic and diverging executions, which we
want to rule out.

Incidentally, Lean's inductive predicates correspond to least fixpoints, but
they are built into Lean's logic (the calculus of inductive constructions),
without using a fixpoint operator like \li{lfp}.

\section{Monotone Functions}
\label{sec:monotone-functions}

We claimed above that the least and greatest fixpoints are guaranteed to exist
under some conditions on \li{f}. It is time to make this more precise.
Let \li{α} and \li{β} be arbitrary types, each equipped with a partial order
\li{≤}. The function \li{f : α → β} is \emph{monotone} if
\hbox{\li{a ≤ b →}} \li{f a ≤ f b} for all \li{a}, \li{b}.
The function \li{f : set α → set α} admits least and greatest fixpoints if
\li{f} is monotone.

Many operations on sets (e.g., union \li{∪}), relations (e.g., composition
\li{◯}), and functions (e.g., the identity function \li{λx, x}, the constant
function \li{λ_, k}, composition \li{∘}) are monotone or preserve monotonicity.
Of course, not all functions are monotone. Here is an example of a nonmonotone
function \li{f} on \li{set α}:
%
\[\text{\li{f A = (if A = ∅ then set.univ else ∅)}}\]
%
If \li{α} is inhabited, we have \li{∅ ⊆} \verb|set.univ| but
\li{f ∅ = set.univ ⊈ ∅ =} \li{f set.univ}.

\section{Complete Lattices}
\label{sec:complete-lattices}

To define \li{lfp} for sets (including relations), we need two operations:\
subset \hbox{\li{⊆ :}} \li{set α → set α → Prop} and
big intersection \li{⋂ : set (set α) → set α}, which can be defined as follows:
%
\[\hbox{\li$⋂ 𝒜 = {a | ∀A, A ∈ 𝒜 → a ∈ A}$}\]
%
If \li{𝒜} is a finite set \li${A₁, …, Aₙ}$, then \li{⋂ 𝒜 = A₁ ∩ ⋯ ∩ Aₙ}.

We can define \li{lfp} more generally so that it works not only with sets but
with any instance of the algebraic structure called a complete lattice. A
\emph{complete lattice} \li{α} is an ordered type for which each \li{set α} has
an infimum, also called \emph{greatest lower bound}. A complete lattice
consists of
%
\begin{itemize}
\item[1.] a partial order \li{≤ : α → α → Prop} (i.e., a reflexive, transitive, and
  antisymmetric binary predicate);

\item[2.] an operator \li{⨅ : set α → α}, called the \emph{infimum}.
\end{itemize}
%
The \li{⨅} operator satisfies the following two conditions:
%
\begin{itemize}
\item[1.] \li{⨅ A} is a lower bound of \li{A}:
  \li{⨅ A ≤ b} for all \li{b ∈ s};

\item[2.] \li{⨅ A} is a greatest lower bound:
  \li{b ≤ ⨅ A} for all \li{b} such that \li{∀a, a ∈ A → b ≤ a}.
\end{itemize}
%
Together, conditions 1 and 2 ensure that \li{⨅ A} is the unique greatest
lower bound.

The lattice operators \li{≤} and \li{⨅} generalize \li{⊆ : set α → set α →} \li{Prop}
and \li{⋂ :} \li{set (set α) → set α}. Be aware that \li{⨅ A} need not be in
\li{A}. For example, an open interval ]\textit{a},
\textit{b}[ over \li{ℝ} has infimum \textit{a}~$\notin$ ]\textit{a}, \textit{b}[.

Here are some examples of complete lattices:
%
\begin{itemize}
\item \li{set α} with respect to \li{⊆} and \li{⋂} for
  all types \li{α};

\item \li{Prop} with respect to \li{→} and \li{λA, ∀a ∈ A, a};

\item \li|enat := ℕ ∪ {∞}| with respect to \li{≤} and a suitable infimum
  operator;

\item \li|ereal := ℝ ∪ {- ∞, ∞}| with respect to \li{≤} and a suitable infimum
  operator.
\end{itemize}

If \li{α} is a complete lattice, then \li{β → α} is also a complete lattice.
If \li{α} and \li{β} are complete lattices, then \li{α × β} is also a complete
lattice.
In both cases, \li{≤} and \li{⨅} are defined componentwise.

Here are some \emph{non}examples of complete lattices: \li{ℕ}, \li{ℤ}, \li{ℚ},
and \li{ℝ} with respect to \li{≤}. The issue is that there is no greatest
element, which \li{⨅ ∅} must be. Another nonexample: \li$erat := ℚ ∪$ \hbox{\li${- ∞, ∞}$,}
because \li$⨅ {q | 2 < q * q} = sqrt 2$ is not in \li{erat}.

In Lean, it is natural to represent complete lattices using type classes:
%
\lstinputlisting[linerange=complete_lattice-q]{../lean/love10_denotational_semantics_demo_master.lean}
%
The type \li{set α} is an instance of the type class:
%
\lstinputlisting[linerange=set.complete_lattice-q]{../lean/love10_denotational_semantics_demo_master.lean}

\section{Least Fixpoint}
\label{section:least-fixpoint}

With complete lattices in place, we can define the least fixpoint operator:
%
\[\hbox{\li$lfp f = ⨅ {x | f x ≤ x}$}\]
%
The Knaster--Tarski theorem,%
\footnote{\url{https://en.wikipedia.org/wiki/Knaster-Tarski_theorem}}
which we briefly mentioned in Section~\ref{sec:introductory-examples},
gives us the following properties for any monotone function \li{f} on a
complete lattice:
%
\begin{itemize}
\item \li{lfp f} is a fixpoint: \li{lfp f = f (lfp f)};

\item \li{lfp f} is smaller than any other fixpoint: \li{X = f X → lfp f ≤ X}.
\end{itemize}

\section{A Relational Denotational Semantics, Continued}
\label{sec:a-relational-denotational-semantics-continued}

With \li{lfp}, we can fulfill our promise and complete the definition of the
denotational semantics of WHILE programs:
%
\lstinputlisting[linerange=denote_last_line-q]{../lean/love10_denotational_semantics_demo_master.lean}

To validate our definition, we can prove the following connection between the
denotational and the big-step semantics:
%
\lstinputlisting[linerange=denote_iff_big_step-q]{../lean/love10_denotational_semantics_demo_master.lean}
%
For the proof, we refer to Chapter~11 of
\emph{Concrete Semantics:\ With Isabelle\slash HOL}~\cite{nipkow-klein-2014}
or to the demonstration file accompanying this chapter.

\section{Application to Program Equivalence}
\label{sec:application-to-program-equivalence}

Based on the denotational semantics, we introduce a notion of program
equivalence. Two programs are equivalent if they have the same semantics:
%
\lstinputlisting[linerange=denote_equiv_def-q]{../lean/love10_denotational_semantics_demo_master.lean}
%
We write \li{S₁ ~ S₂} as an abbreviation for \li{denote_equiv S₁ S₂}. It is
obvious from the definition that \li{~} is an equivalence relation.

Program equivalence can be used to replace a subprogram in a larger program
with another subprogram if they have the same semantics. This is
achieved by the following congruence rules:
%
\lstinputlisting[linerange=denote_equiv_congrs-q]{../lean/love10_denotational_semantics_demo_master.lean}
%
A \emph{congruence rule} is a lemma that lifts an equivalence relation over
some context (here, \li{~} over \li{;;}\,, \li{stmt.ite}, and \li{stmt.while}).

Notice how the denotational semantics leads to short proofs by rewriting. This
should not be surprising, given that it is designed to be equational and
compositional. If we had used the big-step semantics as the basis for program
equivalence instead, these proofs would have been much more complicated.

We can now prove simple programs equivalent by equational reasoning:
%
\lstinputlisting[linerange=denote_equiv_simple_equivs-q]{../lean/love10_denotational_semantics_demo_master.lean}

We defined the semantics of \li{while} using the \li{lfp} operator, but who
knows whether monotonicity---which guarantees the existence of a least
fixpoint---is met? To quell such doubts, we prove the following lemma:

\lstinputlisting[linerange=denote_equiv.ite_seq_while-q]{../lean/love10_denotational_semantics_demo_master.lean}
%
The lemma gives us a convenient way to expand or contract one iteration of a
loop. The second \li{apply} invokes the lemma \li{lfp_eq} \li{:} \li{lfp f = f (lfp f)},
stating that \li{lfp} is a fixpoint. The rest of the proof is fairly
monotonous: It is all about convincing Lean that \li{lfp}'s argument is
monotone.
