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

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

This chapter is inspired by Chapter~11 of \emph{Concrete
Semantics: With Isabelle\slash HOL}~\cite{nipkow-klein-2014}, whose reading
is recommended.

\section{Motivation}

A \emph{denotational semantics} defines the meaning of each program as a
mathematical object and can be seen as a function
%
\[\hbox{\li{⟦ ⟧ : syntax → 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. This compositionality makes it possible to reason equationally
about programs. The compositionality requirement disqualifies the trivial
definition
%
\[\hbox{\li{⟦S⟧ =} \verb|{|\li{st | (S, st.1) ⟹ st.2}\verb|}|}\]
%
in terms of the big-step semantics \li{ ⟹} because that semantics is not
compositional: The semantics of a while loop is given in terms of itself,
not of its loop body.

In essence, we want structurally recursive equations of the form

\begin{lstlisting}
⟦S ; S'⟧              = … ⟦S⟧ … ⟦S'⟧ …
⟦if b then S else S'⟧ = … ⟦S⟧ … ⟦S'⟧ …
⟦while b do S⟧        = … ⟦S⟧ …
\end{lstlisting}

An evaluation function such as \li{eval : aexp → ((var → ℤ) → ℤ)} on arithmetic expressions
is a denotational semantics. Now we want the same for imperative programs.
We need to develop some mathematical notions to reach the point where we can
formulate the denotational semantics.

\section{A Relational Denotational Semantics}

Denotational semantics for deterministic languages are normally given as a
\emph{function} from prestate to poststate, but we find \emph{relations} more
convenient to manipulate. Hence we present a relational denotational
semantics, following \emph{Concrete Semantics} \cite{nipkow-klein-2014}. The
relational approach was also used for the big-step semantics, which took the
form of a predicate of type \li{state → state → Prop}. In contrast, a
denotational semantics of a program will be a mathematical object of type
\li{set (state × state)}.

To a mathematician working informally, \li{state → state → Prop} and
\li{set (state} \li{×} \li{state)} are ``the same,'' since there is a
one-to-one correspondence between predicates on pairs and subsets of the
cartesian product. To a type theorist, \li{state → state → Prop} and
\li{set} \li{(state × state)} are ``the same'' up to currying, since
\li{set α = α → Prop} by definition. So why make this distinction? One reason
is the different perspective afforded by the different structures. Another is
for efficiency of notation or of computation. The final reason is that many
systems of formal logic enforce a strict separation between predicates and
their arguments, making it formally nonsensical to even ask whether
\li{state → state →} \li{Prop} and \li{set (state × state)} are ``the same.''

We call our denotational semantics \li{den}, with \li{⟦}\,\li{⟧} as syntactic
sugar. Let us first study the first four equations of the definition,
keeping the \li{while} case for later:
%
\lstinputlisting[linerange=den_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. Recall that if \li{x} is a pair, then
\li{x.1} and \li{x.2} give access to its first and second components.

The semantics of sequential composition is elegantly expressed as a relational
composition \li{◯}, which is defined such that
\li$r₁ ◯ r₂ = {x | ∃y, (x.1, y) ∈ r₁ ∧ (y,$ \li$x.2) ∈ r₂}$.

The semantics of \li{ite} is the union of the behaviors of the two branches,
restricted to include only the tuples whose first component makes the Boolean
condition true or false, according to the branch. The restriction operator
is defined as
\li$r ⇃ p = {x | p x.1 ∧ x ∈ r}$.

The difficulties arise when we try to define the \li{while} case. We would
like to write
%
\begin{lstlisting}
| (while b S)   :=
  ((den S ◯ den (while b S)) ⇃ b) ∪ (Id state ⇃ λs, ¬ b s))
\end{lstlisting}
%
but this is not well founded due to the unmodified recursive call to
\li{while b S}. So we need to write this differently. What we are looking for
is a solution for \li{X} in the equation
%
\begin{lstlisting}
X = ((den S ◯ X) ⇃ b) ∪ (Id state ⇃ λs, ¬ b s))
\end{lstlisting}
%
In other words, we are looking for a fixpoint. The rest of this chapter
is concerned with building a fixpoint operator \li{lfp} that will allow us to
define the \li{while} case as well:
%
\lstinputlisting[linerange=den_last_line-q]{../lean/love10_denotational_semantics_demo_master.lean}
%
The union and restriction operators are as for the \li{ite} case.

\section{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 many 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:
%
\[\hbox{\li{X = λn : ℕ, n = 0 ∨ ∃m : ℕ, n = m + 2 ∧ X m}}\]
%
This equation is the $\beta$-contracted version of an equation that has more
obviously the right format, with \li{X : ℕ → Prop} and
\li{f := (λ(p : ℕ → Prop) (n : ℕ), n = 0 ∨ ∃m : ℕ, n =} \li{m + 2 ∧ p m)}:
%
\[\hbox{\li{X = (λ(p : ℕ → Prop) (n : ℕ), n = 0 ∨ ∃m : ℕ, n = m + 2 ∧ p m) X}}\]
%
It turns out that this equation admits only one fixpoint. The fixpoint
equation uniquely specifies \li{X} as the set of even natural numbers.

In general, the least and greatest fixpoint may be different. Consider the
equation
\[\hbox{\li{X = (λx, x) X}}\]
where \li{X : ℕ → Prop}.
The least fixpoint of this equation is \li{λ_, False} and the greatest
fixpoint is \li{λ_, True}. Conventionally, we have that \li{False < True} and
thus \li{(λ_, False) <} \li{(λ_, True)}. Similarly, \li{∅ < @set.univ α} if
\li{α} is inhabited (i.e., if it contains at least one element).

Incidentally, Lean's inductive predicates correspond to least fixpoints, but
they are built into Lean's calculus of inductive constructions. We implicitly
made use of this observation when we defined the operational semantics as an
inductive data type.

For the semantics of programming languages:
%
\begin{itemize}
\item \li{X} will have type \li{set (state × state)}, representing relations
between states;

\item \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).
\end{itemize}

Which fixpoint should we use for the semantics of \li{while}? A program should
be prohibited from looping infinitely: Each time a loop is evaluated, it must
terminate after some number of iterations \li{n}. Let \li{f}$^\texttt{\itshape
n}$ denote the \texttt{\itshape n}-fold composition of \li{f}, corresponding
to performing at most \texttt{\itshape n}~iterations, then we have
\li{X = f}$^\texttt{\itshape n}$\li{(∅)} in this case. More generally, we
always have
\[\hbox{\li{X = f}$^\texttt{0}$\li{(∅) ∪ f}$^\texttt{1}$\li{(∅) ∪ f}$^\texttt{2}$\li{(∅) ∪ ⋯}}\]
Kleene's fixpoint theorem%
\footnote{\url{https://en.wikipedia.org/wiki/Kleene_fixed-point_theorem}}
states that the least fixpoint \li{lfp f} will produce the value of \li{X}
satisfying this equation. The greatest fixpoint would also consider cyclic and
diverging executions.

\section{Monotone Functions}

Let \li{α} and \li{β} be arbitrary types, each equipped with a partial order \li{≤}.
We say that the function \li{f : α → β} is \emph{monotone} if
\li{a ≤ b → f a ≤ f b} for all \li{a}, \li{b}.

Many operations on sets (e.g., \li{∪}), relations (e.g., \li{◯}), and
functions (e.g., \li{const}) are monotone.
The set of monotone functions is also well behaved: The identity function is
monotone, the composition of monotone functions is again monotone, and so
on.

All monotone functions \li{f : α → α}, where \li{α} is a ``complete lattice''
(introduced below), admit least and greatest fixpoints.

Here is an example of a nonmonotone function on sets:
%
\[\text{\li{f s =}}
  \begin{cases}
    \text{\li{s ∪}}~\hbox{\verb|{|a\verb|}|} & \text{if \li{a ∉ s}} \\
    \text{∅} & \text{otherwise}
  \end{cases}\]
%
Notice that \li{∅ ⊆} \verb|{|a\verb|}|
but \li{f ∅ = }\verb|{|\li{a}\verb|}| \li{⊈ ∅ = f} \verb|{|a\verb|}|.

\section{Complete Lattices}

To define the least fixpoint for sets, we only need one operation:\
intersection \li{⋂}. The same definition works in 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 a partial order \li{≤ : α → α → Prop} (i.e., reflexive, transitive, and
  antisymmetric);

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

\item \li{⨅s} is the greatest lower bound:
  \li{b ≤ ⨅s} for all \li{b} such that \li{∀x ∈ s, b ≤ x}.
\end{itemize}

We are justified in writing ``\emph{the} greatest lower bound'': If \li{α} is
a partial order, for any \li{s : set α} there is at most one \li{a : α}
satisfying both conditions on the infimum.

Warning: \li{⨅s} is not necessarily an element of \li{s}. For example, an open
interval ]\textit{a}, \textit{b}[ has infimum \textit{a}, which is not in
]\textit{a}, \textit{b}[.

Here are some examples of complete lattices:
%
\begin{itemize}
\item \li|enat := ℕ ∪ {∞}|;

\item \li|ereal := ℝ ∪ {- ∞, ∞}|;

\item \li{set α} is a complete lattice with respect to \li{⊆} and \li{⋂} for
  all types \li{α};

\item \li{Prop} is a complete lattice with respect to \li{→} and \li{∀}, i.e.,
  \li{⨅s := ∀p ∈ s, p}.
\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{ℚ},
\li{ℝ}. The issue is that there is no largest element, which the infimum for
\li{∅} must be. Another nonexample:
\li{erat := ℚ ∪ }\verb|{|\li{- ∞, ∞}\verb|}|. The issue is that
\li{⨅}\verb|{|\li{q | 2 < q * q}\verb|}| \li{= sqrt 2} is not in \li{ℚ}.

Finally, we define
%
\[\hbox{\li{lfp f  :=  ⨅}\verb|{|\li{x | f x ≤ x}\verb|}|}\]

The Knaster--Tarski theorem%
\footnote{\url{https://en.wikipedia.org/wiki/Knaster-Tarski_theorem}}
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}

With \li{lfp}, we can complete the definition of the denotational semantics,
as announced:
%
\lstinputlisting[linerange=den_last_line-q]{../lean/love10_denotational_semantics_demo_master.lean}

\section{A Relational Denotational Semantics, Continued}

The proof of the pudding is in the eating. We defined the semantics of
\li{while} in terms of the \li{lfp} operator, but perhaps monotonicity---which
guarantees the existence of a least fixpoint---is not met. To quell such
doubts, we prove the lemma

\lstinputlisting[linerange=den_while-q]{../lean/love10_denotational_semantics_demo_master.lean}
%
The lemma gives us a convenient way to unfold one iteration of a loop. The first
proof step expands the least fixpoint, exploiting definitional
equality to recognize the semantics of an \li{ite} hiding in the semantics of
a \li{while}. The rest of the proof is all about proving monotonicity of the
body of the fixpoint operator.

Another important result is the connection between the denotational and the
big-step semantics:

\lstinputlisting[linerange=den_eq_bigstep-q]{../lean/love10_denotational_semantics_demo_master.lean}
%
Its proof is beyond the scope of this course. We refer to Chapter~11 of
\emph{Concrete Semantics: With Isabelle\slash HOL}~\cite{nipkow-klein-2014}
or to the Lean files accompanying this book.
