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

We now review a third way to specify the semantics of a programming language:\
denotational semantics. A denotational semantics directly specifies the meaning
of programs as a mathematical object. If an operational semantics corresponds to
an idealized interpreter and a Hoare logic corresponds to an idealized verifier,
then a denotational semantics corresponds to an idealized compiler:\ a compiler
that translates the source program not to assembly language but directly to
mathematics.

The core of this chapter is modeled closely after Chapter~11 of \emph{Concrete
Semantics:\ With Isa\-belle\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}--\li{then}--\li{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 many useful
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/LoVe/LoVe11_DenotationalSemantics_DemoMaster.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 by the equation
%
\[\hbox{\tabletsmall\li$r₁ ◯ r₂ = {ac | ∃b, (Prod.fst ac, b) ∈ r₁ ∧ (b, Prod.snd ac) ∈ r₂}$}\]
%
The definition is perhaps easier to relate to when expressed as
\[\hbox{\tabletsmall\li$r₁ ◯ r₂ = {(a, c) | ∃b, (a, b) ∈ r₁ ∧ (b, c) ∈ r₂}$}\]
%
Unfortunately, Lean cannot process that form, since it requires the left part of
a comprehension to be a single variable.

The semantics of an \li{if}--\li{then}--\li{else} statement 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 | ab ∈ r ∧ P (Prod.fst ab)}$}\]
%
A more intuitive definition would have been
%
\[\hbox{\li$r ⇃ P = {(a, b) | (a, b) ∈ r ∧ P a}$}\]
%
but again this is not supported by Lean. Note two degenerate cases:
If \li{P := (fun _ ↦ True)}, then \li{r ⇃ P = r}, and if \li{P := (fun _ ↦ False)},
then \li$r ⇃ P = ∅$.

The difficulties arise when we try to define the semantics of \li{while} loops.
We would like to write
%
\begin{lstlisting}
| Stmt.whileDo B S      =>
  ((denote S ◯ denote (Stmt.whileDo B S)) ⇃ B)
  ∪ (Id ⇃ (fun s ↦ ¬ B s))
\end{lstlisting}
%
but this is ill-founded due to the recursive call on \hbox{\li{Stmt.whileDo}}
\hbox{\li{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 ⇃ (fun 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/LoVe/LoVe11_DenotationalSemantics_DemoMaster.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};
for example, if \li{f := Nat.}\allowbreak\li{succ}, then there exists no
value \li{X} such that \li{X = Nat.succ X}.
There may also be several fixpoints; for example, if
\li{f := (fun x ↦ x)}), then any \li{X} is a solution of
\li{X = (fun x ↦ x) 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, where \li{X : ℕ → Prop}:
%
\[\hbox{\lic{X = (fun n : ℕ ↦ n = 0 ∨ (∃m : ℕ, n = m + 2 ∧ X m))}}\]
%
This equation is the $\beta$-reduced variant of an equation with the right
format:
%
\[\tabletsmall\hbox{\lic{X =}}~\overbrace{\hbox{\lic{(fun (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 = (fun P ↦ P) X}}\]
for \li{X : ℕ → Prop}.
The least fixpoint is \li{fun _ ↦ False} and the greatest fixpoint is
\li{fun _ ↦ True}. By convention, we have \hbox{\li{False}} \hbox{\li{< True}} and
thus \li{(fun _ ↦ False) <} \li{(fun _ ↦ True)}. Similarly, \li{∅ < @Set.univ α} for
any inhabited type \li{α}.

For the semantics of \li{while} loops, \li{X} will have type
\hbox{\li{Set (State}} \hbox{\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}? Whereas the
greatest fixpoint would also allow cyclic and diverging executions, the least
fixpoint allows only finite (but possibly unbounded) executions. Hence we choose
the least fixpoint.

\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{fun x ↦ x}, the constant
function \li{fun _ ↦ 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 α}, with \li{⊆} as the partial order:
%
\[\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
%
\[\hbox{\li$⋂ X = {a | ∀A, A ∈ X → a ∈ A}$}\]
%
If \li{X} is a finite set \li${A₁, …, Aₙ}$, then \li{⋂ X = A₁ ∩ ⋯ ∩ Aₙ}.

\pagebreak[2]

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,
  antisymmetric, and transitive 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 ∈ A};

\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}[.
The infimum of a set is a generalization of the notion of minimal element.

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{fun 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 nonexamples of complete lattices: \li{ℕ}, \li{ℤ}, \li{ℚ},
and \li{ℝ} with respect to \li{≤}. The issue is that there is no greatest
element to assign to \li{⨅ ∅}. Another nonexample is \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=CompleteLattice-q]{../lean/LoVe/LoVe11_DenotationalSemantics_DemoMaster.lean}
%
The type \li{Set α} is an instance of the type class:
%
\lstinputlisting[linerange=Set.CompleteLattice-q]{../lean/LoVe/LoVe11_DenotationalSemantics_DemoMaster.lean}

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

Using complete lattices, we can define the least fixpoint operator:
%
\[\hbox{\li$lfp f = ⨅ {x | f x ≤ x}$}\]
%
In Lean:
%
\lstinputlisting[linerange=lfp-q]{../lean/LoVe/LoVe11_DenotationalSemantics_DemoMaster.lean}

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/LoVe/LoVe11_DenotationalSemantics_DemoMaster.lean}

To validate our definition, we can prove the following connection between the
denotational and the big-step semantics:
%
\lstinputlisting[linerange=denote_iff_BigStep-q]{../lean/LoVe/LoVe11_DenotationalSemantics_DemoMaster.lean}
%
For the proof, we refer to Chapter~11 of
\emph{Concrete Semantics:\ With Isa\-belle\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=DenoteEquiv_def-q]{../lean/LoVe/LoVe11_DenotationalSemantics_DemoMaster.lean}
%
We write \li{S₁ ~ S₂} as an abbreviation for \li{DenoteEquiv S₁ S₂}. It is
easy to see 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=DenoteEquiv_congrs-q]{../lean/LoVe/LoVe11_DenotationalSemantics_DemoMaster.lean}
%
A \emph{congruence rule} is a theorem that lifts an equivalence relation over
some context (here, \li{~} over sequential composition,
\li{if}--\li{then}--\li{else}, and \li{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=DenoteEquiv_simple_equivs-q]{../lean/LoVe/LoVe11_DenotationalSemantics_DemoMaster.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 theorem:

\lstinputlisting[linerange=DenoteEquiv.ite_seq_while-q]{../lean/LoVe/LoVe11_DenotationalSemantics_DemoMaster.lean}
%
The theorem gives us a convenient way to expand or contract one iteration of a
loop. The second \li{apply} invokes the theorem \li{lfp_eq} \li{:} \li{lfp f = f (lfp f)},
stating that \li{lfp} is a fixpoint.
%
The last step applies a theorem to convince Lean that \li{lfp}'s
argument is monotone. That theorem's proof is fairly monotonous:
%
\lstinputlisting[linerange=Monotone_while_lfp_arg-q]{../lean/LoVe/LoVe11_DenotationalSemantics_DemoMaster.lean}

\section{A Simpler Approach Based on an Inductive Predicate}

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}. Most of this section was dedicated to the
construction of an \li{lfp} operator. Could we have used an inductive predicate
instead and saved ourselves this work?

The answer is yes. First, recall that the types \li{Set (State × State)} and
\li{State} \li{→} \li{State → Prop} are equivalent representations of binary
relations in Lean. So we can build the following \hbox{\li{Awhile}} predicate, which
resembles the reflexive transitive closure but stops when the given condition
\li{B} turns false:

\lstinputlisting[linerange=awhile-q]{../lean/LoVe/LoVe11_DenotationalSemantics_DemoMaster.lean}
%
With this operator, the definition of the definitional semantics becomes

\lstinputlisting[linerange=denote_awhile_def_line-q]{../lean/LoVe/LoVe11_DenotationalSemantics_DemoMaster.lean}

\vskip-.25\topsep

\noindent\hbox{}\kern\leftmargin\phantom{\li{xxxxx}}\strut\smash{$\vdots$}

\vskip-.5\topsep

\lstinputlisting[linerange=denote_awhile_last_line-q]{../lean/LoVe/LoVe11_DenotationalSemantics_DemoMaster.lean}

The \li{Awhile} predicate's introduction rules closely resembles the \li{while}
rules of the big-step operational semantics. Behind their different fa\c{c}ades,
operational and denotational semantics are not so dissimilar after all.
