semantics.tex

% TODO: goal synonymous with conclusion??!

\def\prod{\mathrel{::=}}
\def\altn{\mathrel{\mid}}
\def\NT#1{\textsf{#1}}
\def\TT#1{\texttt{#1}}
\def\Nat{\mathbb{N}}

\def\Expression{\NT{Expression}}
\def\Add{\oplus}
\def\PUSH{\TT{PUSH}\;}
\def\ADD{\TT{ADD}}
\def\nil{\TT{[]}}
\def\Instruction{\NT{Instruction}}
\def\Code{\NT{Code}}
\def\Stack{\NT{Stack}}
\def\Machine{\NT{Machine}}
\def\compile{\textit{compile}}

\def\Eval{\Downarrow}
\def\Step{\mapsto}
\def\StepS{\Step^\star}
\def\Exec{\rightarrowtail}
\def\ExecS{\Exec^\star}

\chapter{Semantics for Compiler Correctness}\label{ch:semantics}

In the context of computer science, the primary focus of \textit{semantics}
is the study of the meaning of programming languages. Having
a mathematically rigorous definition of a language allows us to reason about
programs written in the language in a precise manner. In this chapter, we
begin by reviewing different ways of giving a formal semantics to
a language, and various techniques for proving properties of these
semantics. We conclude by presenting a compiler for a simple expression
language, exploring what it means for this compiler to be correct, and how
this may be proved.

\section{Semantics}%{{{%

\subsection{Natural Numbers and Addition}%{{{%

To unambiguously reason about what any given program means, we need to give
a mathematically rigorous definition of the language in which it is
expressed. To this end, let us consider the elementary language of natural
numbers and
addition~\cite{hutton04-exceptions,hutton06-calculating,hutton07-interruptions}.
\begin{align*}
	\Expression
		& \prod \Nat \eqTag{Exp-$\mathbb{N}$} \\
		& \altn \Expression \Add \Expression \eqTag{Exp-$\Add$}
\end{align*}
That is, an $\Expression$ is either simply a natural number, or a pair of
$\Expression$s, punctuated with the $\Add$ symbol to represent the
operation of addition. We will adhere to a naming convention of $m, n \in
\Nat$ and $a, b, e \in \Expression$.

Although seemingly simplistic, this language has sufficient structure to
illustrate two fundamental aspects of computation, namely that of sequencing
computations and combining their results. We shall shortly expand on this in
section \ref{sec:semantics-degenerate}.

%}}}%

\subsection{Denotational Semantics}%{{{%

% semantic brackets
\def\sb[#1]{[\![#1]\!]}

Denotational semantics attempts to give an interpretation of a source
language in some suitable existing formalism that we already understand.
More specifically, the denotation of a program is a representation of what
the program means in the vocabulary of the chosen formalism, which could be
the language of sets and functions, the $\lambda$-calculus, or perhaps one
of the many process calculi. Thus, to formally give a denotational semantics
for a language is to define a mapping from the source language into some
underlying semantic domain. For example, we can give the following semantics
for our earlier $\Expression$ language, denoted as a natural number:
\begin{align*}
	\sb[\anonymous] &: \Expression \rightarrow \Nat \\
	\sb[ m ] &= m \eqTag{denote-val} \\
	\sb[ a \Add b ] &= \sb[ a ] + \sb[ b ] \eqTag{denote-plus}
\end{align*}
Here, a numeric $\Expression$ is interpreted as just the number itself. The
expression $a \Add b$ is denoted by the sum of the denotations of its
sub-expressions $a$ and $b$; alternatively, we could say that the denotation
of the $\Add$ operator is the familiar $+$ on natural numbers. This
illustrates the essential compositional aspect of denotational semantics,
that the meaning of an expression is given in terms of the meaning of its
parts. The expression $\sb[(1 \Add 2) \Add (4 \Add 8)]$ say, has the
denotation $15$ by repeatedly applying the above definition:
\begin{align*}
	\sb[(1 \Add 2) \Add (4 \Add 8)]
		&= \sb[1 \Add 2] + \sb[4 \Add 8] \\
		&= (\sb[1] + \sb[2]) + (\sb[4] + \sb[8]) \\
		&= (1 + 2) + (4 + 8) \\
		&= 15
\end{align*}

%}}}%

\subsection{Big-Step Operational Semantics}%{{{%

The notion of big-step operational semantics is concerned with the overall
result of a computation. Formally, we define a relation ${\Eval} \subseteq
\Expression \times \Nat$ between $\Expression$s and their final values,
given below in a natural deduction style:
\begin{gather*}
\inferrule*{ }
	{m \Eval m} \eqTag{big-val} \\[2ex]
\inferrule*{a \Eval m \quad b \Eval n}%
	{a \Add b \Eval m + n} \eqTag{big-plus}
\end{gather*}
The first \eqName{big-val} rule says that a simple numeric $\Expression$
evaluates to the number itself. The second \eqName{big-plus} rule states
that, if $a$ evaluates to $m$ and $b$ evaluates to $n$, then $a \Add b$
evaluates to the sum $m + n$. Thus according to this semantics, we can show
that $(1 \Add 2) \Add (4 \Add 8) \Eval 15$ by the following derivation:
\begin{gather*}
\inferrule* [left=big-plus]
{
	\inferrule* [Left=big-plus]
	{
		\inferrule* [Left=big-val]
			{ }{1 \Eval 1}
		\and
		\inferrule*
			{ }{2 \Eval 2}
	}
	{1 \Add 2 \Eval 3}
	\and
	\inferrule*
	{
		\inferrule*
			{ }{4 \Eval 4}
		\and
		\inferrule*
			{ }{8 \Eval 8}
	}
	{4 \Add 8 \Eval 12}
}
{(1 \Add 2) \Add (4 \Add 8) \Eval 15}
\end{gather*}

\noindent For this simple language, the big-step operational semantics
happens to be essentially the same as the denotational semantics, expressed
in a different way. However, one advantage of a relational operational
semantics is that the behaviour can be non-deterministic, in the sense that
each expression could potentially evaluate to multiple distinct values. In
contrast, a denotational semantics deals with non-determinism in the source
language by mapping it to a potentially different notion of non-determinism
in the underlying formalism. For example, should we require our expression
language to be non-deterministic, we would need to switch the semantic
domain of the previous semantics to the power set of natural numbers, rather
than just the set of natural numbers.

%}}}%

\subsection{Small-Step Operational Semantics}\label{sec:small-step}%{{{%

Small-step semantics on the other hand is concerned with how a computation
proceeds as a sequence of steps. Both big-step and small-step semantics are
`operational' in the sense that the meaning of a program is understood
through how it operates to arrive at the result. However, in this case each
reduction step is made explicit, which is particularly apt when we wish to
consider computations that produce side-effects. Again we formally define
a relation ${\Step} \subseteq \Expression \times \Expression$, but between
pairs of $\Expression$s, rather than between expressions and their values:
\begin{gather*}
\inferrule*{ }%
	{m \Add n \Step m + n} \eqTag{small-plus} \\[2ex]
\inferrule*{b \Step b'}%
	{m \Add b \Step m \Add b'} \eqTag{small-right} \\[2ex]
\inferrule*{a \Step a'}%
	{a \Add b \Step a' \Add b} \eqTag{small-left}
\end{gather*}
The first rule \eqName{small-plus} deals with the case where the expressions
on both sides of $\Add$ are numerals: in a single step, it reduces to the
sum $m + n$. The second \eqName{small-right} rule applies when the left
argument of $\Add$ is a numeral, in which case the right argument can make
a single reduction, while \eqName{small-left} reduces the left argument of
$\Add$ if this is possible. There is no rule corresponding to a lone numeric
$\Expression$ as no further reductions are possible in this case.

As each ${\Step}$ step corresponds to a primitive computation, it will often
be more convenient to refer to it via its reflexive, transitive closure,
defined as follows:
\begin{gather*}
\inferrule*[right=small-nil]
{ }{a \StepS a}
\qquad\qquad
\inferrule*[right=small-cons]
{a \Step a' \and a' \StepS b}
{a \StepS b}
\end{gather*}
For example, the full reduction sequence of $(1 \Add 2) \Add (4 \Add 8)
\StepS 15$ would begin by evaluating the $1 \Add 2$ sub-expression,
\begin{gather*}
\inferrule* [left=small-left]
{
	\inferrule* [Left=small-plus]
	{ }{1 \Add 2 \Step 3}
}
{(1 \Add 2) \Add (4 \Add 8) \Step 3 \Add (4 \Add 8)}
\end{gather*}
followed by $4 \Add 8$,
\begin{gather*}
\inferrule* [left=small-right]
{
	\inferrule* [Left=small-plus]
	{ }{4 \Add 8 \Step 12}
}
{3 \Add (4 \Add 8) \Step 3 \Add 12}
\end{gather*}
before delivering the final result:
\begin{gather*}
\inferrule* [left=small-plus]
{ }{3 \Add 12 \Step 15}
\end{gather*}

%}}}%

\subsection{Modelling Sequential Computation with Monoids}\label{sec:semantics-degenerate}%{{{%

It would be perfectly reasonable to give a right-to-left, or even
a non-deterministic interleaved reduction strategy for the small-step
semantics of our $\Expression$ language. However, we enforce a left-to-right
order in order to model the sequential style of computation as found in the
definition of the $\mathsf{State}\;\alpha$ monad from \S\ref{sec:stm-state}.

In the case where the result type of monadic computations form a monoid,
such computations themselves can also be viewed as a monoid. Concretely,
suppose we are working in some monad $\mathsf{M}$ computing values of type
$\Nat$. Using the monoid of sums $(\Nat,\;+,\;0)$, the following definition
of $\circledast$:
\begin{align*}
	\phantom{a} \circledast \phantom{b} \quad:\quad
		&\mathsf{M} \Nat \rightarrow \mathsf{M} \Nat \rightarrow \mathsf{M} \Nat \\
	a \circledast b \quad=\quad 
		&a \bind \lambda m \rightarrow \\
		&b \bind \lambda n \rightarrow \\
		&\textit{return}\;(m + n)
\end{align*}
gives the monoid $(\mathsf{M}\;\Nat,\;\circledast,\;\textit{return}\;0)$. We can
easily verify that the identity and associativity laws hold for this monoid
via simple equational reasoning proofs, as we had done in
\S\ref{sec:stm-monad-prop}. Therefore, we can view monoids as a degenerate
model of monads.

The expression languages of this thesis only computes values of natural
numbers, so rather than work with monadic computations of type
$\mathsf{M}\;\Nat$, we may work directly with the underlying
$(\Nat,\;{+},\;0)$ monoid, since it shares the same monoidal structure. This
simplification allows us to avoid the orthogonal issues of variable binding
and substitution. By enforcing a left-to-right evaluation order for $\Add$
in our expression language to mirror that of the $\bind$ operator, we
are able to maintain a sequential order for computations, which is the key
aspect of the monads that we are interested in.

%}}}%

%\TODO{Are the proofs necessary? They're rather elementary.}
%%{{{%
%\begin{verbatim}
%  a * return 0
%={ defn of * }
%  a >>= \ m -> return 0 >>= \ n -> return (m . n)
%={ left-identity of >>= }
%  a >>= \ m -> (\ n -> return (m . n)) 0
%={ application }
%  a >>= \ m -> return (m . 0)
%={ right-identity of . }
%  a >>= \ m -> return m
%={ right-identity of >>= }
%  a
%\end{verbatim}
%%}}}%
%%{{{%
%\begin{verbatim}
%  return 0 * b
%={ defn of * }
%  return 0 >>= \ m -> b >>= \ n -> return (m . n)
%={ left-identity of >>= }
%  (\ m -> b >>= \ n -> return (m . n)) 0
%={ application }
%  b >>= \ n -> return (0 . n)
%={ left-identity of . }
%  b >>= \ n -> return n
%={ right-identity of >>= }
%  b
%\end{verbatim}
%%}}}%
%%{{{%
%\begin{verbatim}
%  (a * b) * c
%={ defn of * }
%  (a >>= \ l -> b >>= \ m -> return (l . m)) >>= \ lm ->
%  c >>= \ n ->
%  return (lm . n)
%={ associativity of >>=, twice }
%  a >>= \ l -> b >>= \ m -> (return (l . m) >>= \ lm ->
%  c >>= \ n ->
%  return (lm . n))
%={ substitute lm by left-id of >>= }
%  a >>= \ l ->
%  b >>= \ m ->
%  c >>= \ n ->
%  return ((l . m) . n)
%={ associativity of . }
%  a >>= \ l ->
%  b >>= \ m ->
%  c >>= \ n ->
%  return (l . (m . n))
%={ factor out (m . n)  }
%  a >>= \ l ->
%  b >>= \ m -> c >>= \ n -> (return (m . n) >>= \ mn ->
%  return (l . mn))
%={ associativity of >>=, twice }
%  a >>= \ l ->
%  (b >>= \ m -> c >>= \ n -> return (m . n)) >>= \ mn ->
%  return (l . mn)
%={ defn of * }
%  a * (b * c)
%\end{verbatim}
%%}}}%

%}}}%

\section{Equivalence Proofs and Techniques}%{{{%

Now that we have provided precise definitions for the semantics of the
language, we can proceed to show various properties of the $\Expression$
language in a rigorous manner. One obvious questions arises, on the matter
of whether the semantics we have given in the previous
section---denotational, big-step and small-step---agree in some manner.
This section reviews the main techniques involved.

\subsection{Rule Induction}%{{{%

\def\subExp{\sqsubset}

The main proof tool at our disposal is that of \emph{well-founded
induction}, which can be applied to any well-founded structure. For example,
we can show that the syntax of the $\Expression$ language satisfies the
condition of well-foundedness when paired with the following sub-expression
ordering:
\[
	a \subExp a \Add b \qquad b \subExp a \Add b \eqTag{Exp-$\subExp$}
\]
The partial order given by the transitive closure of $\subExp$ is
well-founded, since any $\subExp$-descending chain of expressions must
eventually end in a numeral at the leaves of the finite expression tree.
This particular ordering arises naturally from the inductive definition of
$\Expression$: the inductive case \eqName{Exp-$\Add$} allows us to build
a larger expression $a \Add b$ given two existing expressions $a$ and $b$,
while the base case \eqName{Exp-$\mathbb{N}$} constructs primitive
expressions out of any natural number. In this particular case, to give
a proof that some property $P(e)$ holds for all $e \in \Expression$, it
suffices by the well-founded induction principle to show instead that:
\[
	\forall b \in \Expression.\;
		(\forall a \in \Expression.\; a \subExp b \rightarrow P(a))
		\rightarrow P(b)
\]
More explicitly, we are provided with the hypothesis that $P(a)$ already
holds for all sub-expressions $a \subExp b$ when proving $P(b)$; in those
cases when $b$ has no sub-expressions, we must show that $P(b)$ holds
directly.

The application of well-founded induction to the structure of an inductive
definition is called \emph{structural induction}: to prove that a property
$P(x)$ holds for all members $x$ of an inductively defined structure $X$, it
suffices to initially show that $P(x)$ holds in all the base cases in the
definition of $X$, and that $P(x)$ holds in the inductive cases assuming
that $P(x')$ holds for any immediate substructure $x'$ of $x$.

Our earlier reduction rules ${\Eval}$ along with ${\Step}$ and its
transitive closure ${\StepS}$ are similarly inductively defined, and
therefore admits the same notion of structural induction. These instances
will be referred to as \emph{rule induction}.

%}}}%

\subsection{Proofs of Semantic Equivalence}\label{sec:semantic-equivalence}%{{{%

We shall illustrate the above technique with some examples.

\begin{theorem}\label{thm:denote-big}
Denotational semantics and big-step operational semantics coincide:
\[
	\forall e \in \Expression,\ m \in \Nat.\quad
		\sb[e] \equiv m \;\leftrightarrow\; e \Eval m
\]
\end{theorem}

\begin{proof}
We consider each direction of the $\leftrightarrow$ equivalence separately.
To show $\sb[e] \equiv m \rightarrow e \Eval m$, we ought to proceed by
induction on the definition of the $\sb[\anonymous]$ function. As it happens
to be structurally recursive on its argument, we may equivalently proceed by
structural induction on $e$, giving us two cases to consider:
\begin{description}
\item[Case $e \equiv n$:]%{{{%
Substituting $e$, this base case specialises to showing that:
\[
	\sb[n] \equiv m \rightarrow n \Eval m
\]
By \eqName{denote-val} in the definition of $\sb[\anonymous]$, the
hypothesis evaluates to $n \equiv m$. This allows us to substitute $m$ for
$n$ in the conclusion, which is trivially satisfied by instantiating
\eqName{big-val} with $m$ in the definition of ${\Eval}$.
%}}}%
\item[Case $e \equiv a \Add b$:]%{{{%
Substituting $e$ as before, we need to show that:
\[
	\sb[a \Add b] \equiv m \rightarrow a \Add b \Eval m
\]
Applying \eqName{denote-plus} once to the hypothesis, we obtain that $\sb[a]
+ \sb[b] \equiv m$. Substituting for $m$, the conclusion becomes $a \Add
b \Eval \sb[a] + \sb[b]$. Instantiate the induction hypothesis twice
with the trivial equalities $\sb[a] \equiv \sb[a]$ and $\sb[b] \equiv
\sb[b]$ to yield proofs of $a \Eval \sb[a]$ and $b \Eval \sb[b]$,
which are precisely the two antecedents required by \eqName{big-plus} to
obtain $a \Add b \Eval \sb[a] + \sb [b]$.
%}}}%
\end{description}

\noindent The second half of the proof requires us to show that $\sb[e]
\equiv m \leftarrow e \Eval m$. We may proceed by rule induction directly on
our assumed hypothesis of $e \Eval m$, which must match either
\eqName{big-val} or \eqName{big-plus} in the definition of $\Eval$:
\begin{description}
\item[Rule \eqName{big-val}:]%{{{%
Matching $e \Eval m$ with the consequent of \eqName{big-val}, we may
conclude that there exists an $n$ such that $e \equiv n$ and $m \equiv n$.
Substituting $n$ for $e$ and $m$ in $\sb[e] \equiv m$ and applying
\eqName{denote-val} once, the desired conclusion becomes $n \equiv n$, which
is trivially satisfied by the reflexivity of $\equiv$.
%}}}%
\item[Rule \eqName{big-plus}:]%{{{%
Again by matching $e \Eval m$ with the consequent of \eqName{big-plus},
there exists $a$, $b$, $n_a$ and $n_b$ where $e \equiv a \Add b$ and $m
\equiv n_a + n_b$, such that $a \Eval n_a$ and $b \Eval n_b$.
Substituting for $e$ and $m$, the conclusion becomes $\sb[a \Add b] \equiv
n_a + n_b$, which reduces to:
\[
	\sb[a] + \sb[b] \equiv n_a + n_b
\]
by applying \eqName{denote-plus} once. Instantiating the induction
hypothesis twice with $a \Eval n_a$ and $b \Eval n_b$ yields the
equalities $\sb[a] \equiv n_a$ and $\sb[b] \equiv n_b$ respectively, which
allows us to rewrite the conclusion as $\sb[a] + \sb[b] \equiv \sb[a]
+ \sb[b]$ by substituting $n_a$ and $n_b$. The desired result is now
trivially true by reflexivity of $\equiv$.
%}}}%
\end{description}

\noindent Thus we have shown both directions of the theorem.
\end{proof}

% premise, antecedent / consequent
% hypothesis / conclusion

\begin{theorem}\label{thm:big-small}
Big-step and small-step operational semantics coincide. That is,
\[
	\forall e \in \Expression,\ m \in \Nat.\quad
		e \Eval m \;\leftrightarrow\; e \StepS m
\]
\end{theorem}
\begin{proof}
We shall consider each direction separately as before. To show the forward
implication, we proceed by rule induction on the assumed $e \Eval m$
hypothesis:
\begin{description}
\item[Rule \eqName{big-val}:]%{{{%
There exists an $n$ such that $e \equiv n$ and $m \equiv n$, by matching $e
\Eval m$ with the consequent of \eqName{big-val}. Substituting $n$ for
both $e$ and $m$, we can readily conclude that $n \StepS n$ via
\eqName{small-nil}.
%}}}%
\item[Rule \eqName{big-plus}:]%{{{%
There exists $a$, $b$, $n_a$ and $n_b$ where $e \equiv a \Add b$ and $m
= n_a + n_b$, such that $a \Eval n_a$ and $b \Eval n_b$. After
substituting for $e$ and $m$, the desired conclusion becomes:
\[
	a \Add b \StepS n_a + n_b
\]
Instantiating the induction hypothesis with $a \Eval n_a$ and $b
\Eval n_b$ gives us evidence of $a \StepS n_a$ and $b
\StepS n_b$ respectively. With the former, we can apply $\anonymous
\Add b$ to each of the terms and \eqName{small-left} to obtain a proof of
$a \Add b \StepS n_a \Add b$, while with the latter, we obtain
$n_a \Add b \StepS n_a \Add n_b$ by applying $n_a \Add
\anonymous$ and \eqName{small-right}.

By the transitivity of $\StepS$, these two small-step reduction
sequences combine to give $a \Add b \StepS n_a \Add n_b$, to
which we need only append an instance of \eqName{small-plus} to arrive at
the conclusion.
%}}}%
\end{description}

%The converse implication $e \Eval m \leftarrow e \StepS m$ additionally
%requires lemma \ref{lem:small-sound}, which states that $e \Step e'
%\rightarrow e' \Eval m \rightarrow e \Eval m$; in other words, the reduct of
%a single step under the small-step semantics evaluates under the big-step
%semantics to the same value as the original expression.

\noindent We proceed by induction over the definition of $\StepS$ and using
an additional lemma that we state and prove afterwards. Given $e \StepS m$,
\begin{description}
\item[Rule \eqName{small-nil}:]%{{{%
If the reduction sequence is empty, then it follows that $e \equiv m$. In
this case, we can trivially satisfy the conclusion of $m \Eval m$ with
\eqName{big-val}.
%}}}%
\item[Rule \eqName{small-cons}:]%{{{%
For non-empty reduction sequences, there exists an $e'$ such that $e \Step
e'$ and $e' \StepS m$. Invoke lemma \ref{lem:small-sound} below with $e
\Step e'$ and $e' \Eval m$, where the latter is given by the induction
hypothesis, to obtain proof of $e \Eval m$.
%}}}%
\end{description}
Pending the proof of lemma \ref{lem:small-sound} below, we have thus shown
the equivalence of big- and small-step semantics for the $\Expression$
language.
\end{proof}

\begin{lemma}
\label{lem:small-sound}
A single small-step reduction preserves the value of expressions with
respect to the big-step semantics:
\[
	\forall e, e' \in \Expression,\ m \in \Nat.\quad
		e \Step e' \;\rightarrow\;
		e' \Eval m \;\rightarrow\; e \Eval m
\]
\end{lemma}
\begin{proof}
Assume the two premises $e \Step e'$ and $e' \Eval m$, and proceed by
induction on the structure of the first:
\begin{description}
\item[Rule \eqName{small-plus}:]%{{{%
There are $n_a$ and $n_b$ such that $e \equiv n_a \Add n_b$ and $e' \equiv
n_a + n_b$. As $e'$ is a numeric expression, the only applicable rule for
$e' \Eval m$ is \eqName{big-val}, which implies $m \equiv n_a + n_b$.
Thus the desired conclusion of $e \Eval m$---after substituting for $e$
and $m$---may be satisfied as follows:
\begin{gather*}
\inferrule* [Left=big-plus]
{
	\inferrule* [Left=big-val]
	{ }{n_a \Eval n_a}
	\and
	\inferrule*
	{ }{n_b \Eval n_b}
}{n_a \Add n_b \Eval n_a + n_b}
\end{gather*}
%}}}%
\item[Rule \eqName{small-right}:]%{{{%
There exists $n_a$, $b$ and $b'$ such that $b \Step b'$ with $e \equiv n_a
\Add b$ and $e' \equiv n_a \Add b'$. Substituting for $e'$, the second
assumption becomes $n_a \Add b' \Eval m$, with \eqName{big-plus} as
the only matching rule. This implies the existence of the premises $n_a
\Eval n_a$ and $b' \Eval n_b$,
\begin{gather*}
\inferrule*
{
	\inferrule*
	{ }{n_a \Eval n_a}
	\and
	\inferrule*
	{
		\vdots
	}{b' \Eval n_b}
}{n_a \Add b' \Eval n_a + n_b}
\end{gather*}
for some $n_b$ such that $m \equiv n_a + n_b$. Invoking the induction
hypothesis with $b \Step b'$ and the above derivation of $b' \Eval
n_b$, we obtain a proof of $b \Eval n_b$. The conclusion is satisfied
by the following derivation:
\begin{gather*}
\inferrule*
{
	\inferrule*
	{ }{n_a \Eval n_a}
	\and
	\inferrule* [Right=IH]
	{
		\vdots
	}{b \Eval n_b}
}{n_a \Add b \Eval n_a + n_b}
\end{gather*}
%}}}%
\item[Rule \eqName{small-left}:]%{{{%
This case proceeds in a similar manner to the previous rule, but with $a$,
$a'$ and $b$ such that $a \Step a'$, where $e \equiv a \Add b$ and $e'
\equiv a' \Add b$. Substituting for $e$ and $e'$ in the second assumption
and inspecting its premises, we observe that $a' \Eval n_a$ and $b
\Eval n_b$ for some $n_a$ and $n_b$ where $m \equiv n_a + n_b$:
\begin{gather*}
\inferrule*
{
	\inferrule*
	{
		\vdots
	}{a' \Eval n_a}
	\and
	\inferrule*
	{
		\vdots
	}{b \Eval n_b}
}{a' \Add b \Eval n_a + n_b}
\end{gather*}
Instantiating the induction hypothesis with $a \Step a'$ and $a'
\Eval n_a$ delivers evidence of $a \Eval n_a$. Reusing the second
premise of $b \Eval n_b$ verbatim, we can then derive the
conclusion of $a \Add b \Eval n_a + n_b$:
\begin{gather*}
\inferrule*
{
	\inferrule* [Left=IH]
	{
		\vdots
	}{a \Eval n_a}
	\and
	\inferrule*
	{
		\vdots
	}{b \Eval n_b}
}{a \Add b \Eval n_a + n_b}
\end{gather*}
%}}}%
\end{description}
This completes the proof of $e \Step e' \rightarrow e' \Eval m \rightarrow
e \Eval m$.
\end{proof}

%}}}%

%}}}%

\section{Compiler Correctness}%{{{%

Now that we have established the equivalence of our three semantics for the
expression language, we consider how this language may be compiled for
a simple stack-based machine, what it means for such a compiler to be
correct, and how this may be proved.

%We have given a high-level semantics for the $\Expression$ language in the
%previous sections, but in order to run any such program on a real processor,
%we need to translate, or \emph{compile} an expression to a sequence of
%instructions for some target machine. Given a definition of how the
%processor behaves, how do we ensure that the compiler is producing the
%correct instructions? When we talk of \emph{compiler correctness}, we mean
%that when executed on the target machine, a compiled program ought to
%deliver a result coinciding with what one would expect from the high-level
%semantics. In this section we define a simple stack-based virtual machine,
%along with a compiler for the $\Expression$ language, and demonstrate how we
%can prove a corresponding compiler correctness theorem.

\subsection{A Stack Machine and Its Semantics}\label{sec:stack-machine}%{{{%

\def\MS<#1,#2>{\langle #1 ,\; #2 \rangle}

Unlike the previously defined high-level semantics---which operate directly
on $\Expression$s themselves---real processors generally execute
a \emph{linear} sequences of instructions, each mutating the state of the
machine in some primitive way. In order to give such a low-level
implementation of our $\Expression$ language, we will make use of
a stack-based virtual machine.

Our stack machine has a stack of natural numbers as its sole form of
storage, and the state of the $\Machine$ at any point may be conveniently
represented as the pair of the currently executing $\Code$, along with the
current $\Stack$,
\begin{align*}
	\Machine & \prod \MS<\Code, \Stack> \\
	\Code & \prod \nil \altn \Instruction :: \Code \\
	\Stack & \prod \nil \altn \Nat :: \Stack
\end{align*}
where $\Code$ comprises a sequence of $\Instruction$s, and $\Stack$
a sequence of values.

Due to the simple nature of the $\Expression$ language, the virtual machine
only requires two $\Instruction$s, both of which operate on the top of the
stack:
\begin{align*}
	\Instruction & \prod \PUSH \Nat \altn \ADD
\end{align*}
The $\PUSH m$ instruction places the number $m$ on top of the current stack,
while $\ADD$ replaces the top two values with their sum. Formally, the
semantics of the virtual machine is defined by the $\Exec$ reduction
relation, given below:
\begin{gather*}
	\MS<\PUSH m :: c , \sigma>
	\Exec
	\MS<c , m :: \sigma>
		\eqTag{vm-push} \\[2ex]
	\MS<\ADD :: c , n :: m :: \sigma>
	\Exec
	\MS<c , m + n :: \sigma>
		\eqTag{vm-add}
\end{gather*}
As with the previous definition of $\StepS$, we shall write
$\ExecS$ for the transitive, reflexive closure of
$\Exec$:
\begin{gather*}
\inferrule*[right=vm-nil]
{ }{t \ExecS t}
\qquad\qquad
\inferrule*[right=vm-cons]
{a \Exec a' \and a' \ExecS b}
{a \ExecS b}
\end{gather*}

Informally, the difference between the semantics of a virtual machine versus
a small-step operational semantics is that the reduction rules for the
former is simply a collection of transition rules between pairs of states,
and does not make use of any premises.

%}}}%

\subsection{Compiler}\label{sec:compiler}%{{{%

Given an $\Expression$, a compiler in this context produces some $\Code$
that when executed according to the semantics of the virtual machine just
defined, computes the value of the $\Expression$, leaving the result on top
of the current stack. To avoid the need to define concatenation on
instruction sequences and the consequent need to prove various distributive
properties, the definition of $\compile$ below accepts an extra \emph{code
continuation} argument, to which the code for the expression being compiled
is prepended. To compile a top-level expression, we simply pass in the empty
sequence $\nil$. This both simplifies reasoning and results in more
efficient compilers~\cite{hutton07-haskell}. A numeric expression $m$ is
compiled to a $\PUSH m$ instruction, while $a \Add b$ involves compiling the
sub-expressions $a$ and $b$ in turn, followed by an $\ADD$ instruction:
\begin{align*}
	&\compile : \Expression \rightarrow \Code \rightarrow \Code \\
	&\compile\;m\;c = \PUSH m :: c \eqTag{compile-val} \\
	&\compile\;(a \Add b)\;c = \compile\;a\;(\compile\;b\;(\ADD :: c))
		\eqTag{compile-add}
\end{align*}
For example, $\compile\;((1 \Add 2) \Add (4 \Add 8))\;\nil$ produces
the code below,
\begin{gather*}
	\PUSH 1 :: \PUSH 2 :: \ADD :: \PUSH 4 :: \PUSH 8 :: \ADD :: \ADD :: \nil
\end{gather*}
which when executed with an empty initial stack, reduces as follows:
\begin{align*}
	&\MS<\PUSH 1 :: \PUSH 2 :: \ldots, \nil> \\
	&\Exec \MS<\PUSH 2 :: \ADD :: \ldots, 1 :: \nil> \\
	&\Exec \MS<\ADD :: \PUSH 4 :: \ldots, 2 :: 1 :: \nil> \\
	&\Exec \MS<\PUSH 4 :: \PUSH 8 :: \ldots, 3 :: \nil> \\
	&\Exec \MS<\PUSH 8 :: \ADD :: \ldots, 4 :: 3 :: \nil> \\
	&\Exec \MS<\ADD :: \ADD :: \nil, 8 :: 4 :: 3 :: \nil> \\
	&\Exec \MS<\ADD :: \nil, 12 :: 3 :: \nil> \\
	&\Exec \MS<\nil, 15 :: \nil>
\end{align*}

%}}}%

\subsection{Compiler Correctness}%{{{%

By compiler correctness, we mean that given an expression $e$ which
evaluates to $m$ according to a high-level semantics, compiling $e$ and
executing the resultant code on the corresponding virtual machine must
compute the same $m$. Earlier in the chapter, we had shown the equivalence
of our denotational, big-step, and small-step semantics. While we may freely
choose any of these as our high-level semantics, we shall adopt the big-step
semantics, as it makes our later proofs much shorter.

Using these ideas, the correctness of our compiler can now be formalised by
the following equivalence:
\begin{gather*}
	e \Eval m
	\quad\leftrightarrow\quad
	\MS<\compile\;e\;\nil, \sigma>
		\ExecS \MS<\nil, m :: \sigma>
\end{gather*}
%As $\Eval$ and $\ExecS$ are relations, we necessarily
%require the double implication:
The $\rightarrow$ direction corresponds to a notion of \emph{completeness},
and states that the machine must be able to compute any $m$ that the
big-step semantics permits. Conversely, the $\leftarrow$ direction
corresponds to \emph{soundness}, and states that the machine can only
produce values permitted by the big-step semantics. For this proof, we will
need to generalise the virtual machine on the right hand side to an
arbitrary code continuation and stack.
\begin{theorem}[Compiler Correctness]\label{thm:compiler-correct}
%The compiler and virtual machine semantics coincide with the earlier
%big-step semantics:
\begin{gather*}
	e \Eval m
	\quad\leftrightarrow\quad
	\forall c, \sigma.\
		\MS<\compile\;e\;c, \sigma>
			\ExecS \MS<c, m :: \sigma>
\end{gather*}
\end{theorem}

\begin{proof}
We shall consider each direction of the double implication separately. In
the forward direction, we assume $e \Eval m$ and proceed on its
structure:
\begin{description}
\item[Rule \eqName{big-val}:]%{{{%
There exists an $n$ such that $e \equiv n$ and $m \equiv n$. Substituting
$n$ for both $e$ and $m$, the conclusion becomes:
\begin{align*}
		\MS<\compile\;n\;c, \sigma>
			&\ExecS \MS<c, n :: \sigma> \quad{,} \\
	\textrm{or}\quad
		\MS<\PUSH n :: c, \sigma>
			& \ExecS \MS<c, n :: \sigma>
\end{align*}
by \eqName{compile-val} in the definition of \compile. The conclusion is
satisfied by simply applying \eqName{vm-cons} to \eqName{vm-push} and
\eqName{vm-nil}:
\[\inferrule* [Left=vm-cons]
{
	\inferrule* [Left=vm-push]
	{
	}{\MS<\PUSH n :: c, \sigma>
			\Exec \MS<c, n :: \sigma>}
	\and
	\inferrule* [Right=vm-nil]
	{ }{\MS<c, n :: \sigma>
		\ExecS \MS<c, n :: \sigma>}
}{\MS<\PUSH n :: c, \sigma>
			\ExecS \MS<c, n :: \sigma>}
\]
%}}}%
\item[Rule \eqName{big-plus}:]%{{{%
By matching the assumed $e \Eval m$ with the consequent of
\eqName{big-plus}, we see that there exists $a$, $b$, $n_a$ and $n_b$ where
$e \equiv a \Add b$ and $m \equiv n_a + n_b$, such that $a \Eval n_a$ and $b
\Eval n_b$. Substituting for $e$ and $m$, the conclusion becomes
\begin{gather*}
		\MS<\compile\;(a \Add b)\;c, \sigma>
			\ExecS \MS<c, n_a + n_b :: \sigma> \textrm{ , or} \\
		\MS<\compile\;a\;(\compile\;b\;(\ADD :: c)), \sigma>
			\ExecS \MS<c, n_a + n_b :: \sigma>
\end{gather*}
by expanding \compile. Instantiating the induction hypothesis with $a \Eval
n_a$ and $b \Eval n_b$ yields proofs of
\begin{gather*}
	\forall c_a, \sigma_a.\ \MS<\compile\;a\;c_a, \sigma_a> \ExecS \MS<c_a, n_a :: \sigma_a>
		\textrm{ , and} \\
	\forall c_b, \sigma_b.\ \MS<\compile\;b\;c_b, \sigma_b> \ExecS \MS<c_b, n_b :: \sigma_b>
\end{gather*}
respectively. Note that crucially, these two hypotheses are universally
quantified over $c$ and $\sigma$, written with distinct subscripts above to
avoid ambiguity. Now substitute $c_b = \ADD :: c$, $c_a = \compile\;b\;c_b$,
$\sigma_a = \sigma$, $\sigma_b = n_a :: \sigma_a$ and we obtain via the
transitivity of $\ExecS$:
\begin{align*}
	\forall c, \sigma.\
		&\MS<\compile\;a\;(\compile\;b\;(\ADD :: c)), \sigma> \\
	&\ExecS \MS<(\compile\;b\;(\ADD :: c), n_a :: \sigma> \\
	&\ExecS \MS<\ADD :: c, n_b :: n_a :: \sigma>
\end{align*}
A second application of transitivity to \eqName{vm-add} instantiated as
follows,
\begin{gather*}
	\MS<\ADD :: c, n_b :: n_a :: \sigma> \Exec \MS<c, n_a + n_b :: \sigma>
\end{gather*}
gives the required conclusion of:
\begin{align*}
	\forall c, \sigma.\
		&\MS<\compile\;a\;(\compile\;b\;(\ADD :: c)), \sigma>
			\Exec \MS<c, n_a + n_b :: \sigma>
\end{align*}
%}}}%
\end{description}

For the backward direction, we proceed on the structure of $e$:
\begin{description}
\item[Case $e \equiv n$:]%{{{%
Substituting $e$ with $n$, the base case becomes:
\begin{gather*}
	\forall c, \sigma.\
		\MS<\compile\;n\;c, \sigma>
			\ExecS \MS<c, m :: \sigma>
	\rightarrow n \Eval m
	\textrm{ , or} \\
	\forall c, \sigma.\
		\MS<\PUSH n :: c, \sigma>
			\ExecS \MS<c, m :: \sigma>
	\rightarrow n \Eval m
\end{gather*}
Assume the hypothesis and set both $c$ and $\sigma$ to $\nil$ to obtain
$\MS<\PUSH n :: [], []> \ExecS \MS<[], m :: []>$, which must be a single
reduction corresponding to \eqName{vm-push}. Therefore $m$ and $n$ must be
one and the same, and the conclusion of $n \Eval n$ is trivially satisfied
by \eqName{big-val}.
%}}}%
\item[Case $e \equiv a \Add b$:]%{{{%
Substituting $e$ with $a \Add b$ and expanding the definition of \compile,
we need to show that:
\begin{gather*}
	\forall c, \sigma.\
		\MS<\compile\;a\;(\compile\;b\;(\ADD :: c)), \sigma>
			\ExecS \MS<c, m :: \sigma>
	\rightarrow a \Add b \Eval m
\end{gather*}
Now, for both $a$ and $b$, we know that there exists $n_a$ and $n_b$ such
that:
\begin{gather*}
	\forall c_a, \sigma_a.\ \MS<\compile\;a\;c_a, \sigma_a>
		\ExecS \MS<c_a, n_a :: \sigma_a>
	\textrm{ , and} \\
	\forall c_b, \sigma_b.\ \MS<\compile\;b\;c_b, \sigma_b>
		\ExecS \MS<c_b, n_b :: \sigma_b>
\end{gather*}
Substituting for the subscripted $c_a$, $c_b$, $\sigma_a$ and $\sigma_b$ as
we had done in the \eqName{big-plus} case of the first half of this proof,
we obtain:
\begin{gather*}
	\forall c, \sigma.\
		\MS<\compile\;a\;(\compile\;b\;(\ADD :: c)), \sigma>
			\ExecS \MS<c, n_a + n_b :: \sigma>
\end{gather*}
Contrast this with the hypothesis:
\begin{gather*}
	\forall c, \sigma.\
		\MS<\compile\;a\;(\compile\;b\;(\ADD :: c)), \sigma>
			\ExecS \MS<c, m :: \sigma>
\end{gather*}
Since the $\Exec$ reduction relation is deterministic, it must be the case
that $m$ and $n_a + n_b$ are the same. Substituting in $n_a + n_b$ for $m$,
the conclusion becomes $a \Add b \Eval n_a + n_b$---an instance of
\eqName{big-plus}---whose premises of $a \Eval n_a$ and $b \Eval n_b$ are in
turn satisfied by instantiating the induction hypothesis with $\forall c_a,
\sigma_a.\ \MS<\compile\;a\;c_a, \sigma_a> \ExecS \MS<c_a, n_a :: \sigma_a>$
and $\forall c_b, \sigma_b.\ \MS<\compile\;b\;c_b, \sigma_b> \ExecS \MS<c_b,
n_b :: \sigma_b>$.

%\TODO{there's more to be said on the determinism of $\Exec$ here---in
%contrast with the non-det VMs later---just not sure what it is yet.}

%}}}%
\end{description}
This completes the proof of the compiler correctness theorem.
\end{proof}

%}}}%

%}}}%

\section{Conclusion}%{{{%

In this chapter, we have shown by example what it means to give the
semantics of simple language in denotational, big-step and small-step
styles. We justified the use of a monoidal model of natural numbers and
addition---with left-to-right evaluation order---as simplification of
monadic sequencing. We then proved the three given semantics to be
equivalent, and demonstrate the use of well-founded induction on the
structure of the reduction rules (that is, rule induction) and of the
syntax. Finally, we defined a stack-based virtual machine and a compiler for
running programs of the $\Expression$ language, and presented a proof of
compiler correctness.

%}}}%

% vim: ft=tex: