\chapter{Operational Semantics}
\label{chap:operational-semantics}

In this and the next two chapters, we will see how to use Lean to specify the
syntax and semantics of programming languages and to reason about the semantics.

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

\section{Motivation}

A formal semantics helps specify and reason about the programming language
itself, and about individual programs. It can form the basis of verified
compilers, interpreters, verifiers, static analyses, type systems, etc.
Without formal proofs, semantics, compilers, interpreters, verifiers, static
analyses, type systems, etc., are almost always wrong.

Proof assistants are widely used in the area of programming language research.
For example, every year, about 10\%--20\% of papers presented at
POPL (Principles of Programming Languages) are partially or totally
formalized. This is possible because comparatively little machinery
(background libraries, tactics) is needed to get started, beyond inductive
types and predicates and recursive functions, which are provided by the
provers. The proofs tend to have lots of cases, which is a good match for
computers. Proof assistants are convenient to keep track of what needs to be
changed as we extend a programming language with more features.

\section{A Minimalistic Imperative Language}

\emph{WHILE}%
\footnote{Fans of backronyms might enjoy this one: Weak Hypothetical
  Imperative Language Example.}
is a minimalistic imperative language with the following grammar:

\begin{center}
\begin{tabular}{@{}l@{\enskip}r@{\enskip}l@{\qquad}l@{}}
\texttt{\itshape S} & \li|::=| & \li|skip|
  & \text{(no-op)} \\
& $\mid$ & \texttt{{\itshape x} := {\itshape a}}
  & \text{(assignment)} \\
& $\mid$ & \texttt{{\itshape S} ; {\itshape S}}
  & \text{(sequential composition)} \\
& $\mid$ & \li|if| \texttt{\itshape b} \li|then| \texttt{\itshape S} \li|else| \texttt{\itshape S}
  & \text{(conditional statement)} \\
& $\mid$ & \li|while| \texttt{\itshape b} \li|do| \texttt{\itshape p}
  & \text{(while loop)}
\end{tabular}
\end{center}
%
where \texttt{\itshape S} stands for a \emph{statement} (also called
\emph{command} or \emph{program}), \texttt{\itshape x} for a program variable,
\texttt{\itshape a} for an arithmetic expression, and \texttt{\itshape b} for
a Boolean expression.

In our grammar, we deliberately leave the syntax of arithmetic and Boolean
expressions unspecified. In Lean, we have the choice:
%
\begin{itemize}
\item We can use a type such as \li{aexp} from
  Section~\ref{sec:type-definitions} and similarly for Boolean expressions.

\item We can decide that an arithmetic expression is simply a function from
  states to natural numbers (e.g., \li{state → ℕ}) and a Boolean expression is
  simply a predicate over states (e.g., \li{state → Prop} or
  \li{state → bool}). A \emph{state} is a mapping from program variables to
  values. For example, the arithmetic expression \li{x + y + 1} would be
  represented by the function \li{λs : state, s "x" + s "y" + 1}, and the
  Boolean expression \li{a ≠ b} by the predicate \li{λs : state, s "a" ≠ s "b"}.
\end{itemize}

This corresponds to the difference between deep and shallow embeddings: A
\emph{deep embedding} of some syntax (expression, formula, program, etc.)
consists of an abstract syntax tree specified in the proof assistant (e.g.,
\li{aexp}) with a semantics. In contrast, a \emph{shallow embedding} simply
reuses the corresponding mechanisms from the logic (e.g., functions and
predicates).

A deep embedding allows us to reason explicitly about a program's syntax. A
shallow embedding is more leightweight, because we can use it directly,
without having to define a semantics (e.g., an \li{eval} function for
\li{aexp}).

We will use a deep embedding of programs (which we find interesting) and
a shallow embeddings of arithmetic and Boolean expressions (which we find
boring). Our Lean definition of programs follows:

\lstinputlisting[linerange=program-q]{../lean/love08_operational_semantics_demo_master.lean}
%
The infix operation \li{S ;; T} is provided as an alternative to \li{seq S T}.

The correspondence between the inductive type's constructors and the grammar
rules should be clear. Variables are represented by strings. The type
\li{state} is defined as \li{string → ℕ}, a mapping from variable names to
values. For simplicity, our program variables are all of type natural number,
and (somewhat unusually) all possible variable names exist in the state and
are assigned a value.

\section{Big-Step Semantics}

An \emph{operational semantics} corresponds to an idealized, abstract
interpreter. There are two main variants: big-step semantics and small-step
semantics. We will start by giving a big-step semantics to our WHILE language.

The traditional (and also the most readable) way to specify such a semantics
is through a formal system of derivation rules, in the style of the typing rules
presented in Sections \ref{sec:types-and-terms}~and~\ref{sec:dependent-types}.

In a \emph{big-step} (\emph{operational}) \emph{semantics} (also called
\emph{natural semantics}), judgments have the form \li{(S, s) ⟹ t} and the following intuitive
interpretation:
%
\begin{quote}
Starting in a state \li{s}, executing \li{S} terminates in the state \li{t}.
\end{quote}
%
In keeping with
the definition of WHILE programs, a state \li{s} is a function of type
\li{string → ℕ}. An example of a judgment follows:
%
\[\hbox{\li|(x := x + y; y := 0,  [x ↦ 3, y ↦ 5])  ⟹  [x ↦ 8, y ↦ 0]|}\]
%
We use the informal notation \li{[x ↦ 3, y ↦ 5]} to denote the function
\li{λvar, if var = "x" then 3 else if var = "y" then 5 else 0} and similarly
for \li{[x ↦ 8, y ↦ 0]}. Intuitively, the judgment should hold.

The derivation rules for big-step semantics judgments are given below.
The rules can be seen as an abstract interpreter for WHILE program.

\begin{gather*}
\prftree[r]{\textsc{Skip}}
  {\strut( \texttt{skip,}~ \texttt{\itshape s}) \Longrightarrow
  \texttt{\itshape s}}
\\[2\jot]
\prftree[r]{\textsc{Asn}}
  {\strut( \texttt{\itshape x}~\texttt{:=}~\texttt{{\itshape a},}~
  \texttt{\itshape s})
  \Longrightarrow \texttt{\itshape s}\{\texttt{\itshape x} \mapsto
  \texttt{{\itshape a}\;{\itshape s}}\}}
\\[2\jot]
\prftree[r]{\textsc{Seq}}
  {\strut(\texttt{{\itshape S}, {\itshape s}}) \Longrightarrow t}
  {\strut(\texttt{{\itshape T}, {\itshape t}}) \Longrightarrow u}
  {\strut(\texttt{{\itshape S}{;}\,{\itshape T}, {\itshape s}}) \Longrightarrow u}
\\[2\jot]
\prftree[r]{\textsc{If-True}\quad if \li{b s} is true}
  {\strut(\texttt{{\itshape S$_1$}, {\itshape s}}) \Longrightarrow t}
  {\strut(\texttt{if~{\itshape b}~then~{\itshape S$_1$}~else~{\itshape S$_2$}, {\itshape s}}) \Longrightarrow t}
\\[2\jot]
\prftree[r]{\textsc{If-False}\quad if \li{b s} is false}
  {\strut(\texttt{{\itshape S$_2$}, {\itshape s}}) \Longrightarrow t}
  {\strut(\texttt{if~{\itshape b}~then~{\itshape S$_1$}~else~{\itshape S$_2$}, {\itshape s}}) \Longrightarrow t}
\\[2\jot]
\prftree[r]{\textsc{While-True}\quad if \li{b s} is true}
  {\strut(\texttt{{\itshape S}, {\itshape s}}) \Longrightarrow t}
  {\strut(\texttt{while~{\itshape b}~do~{\itshape S}, {\itshape t}}) \Longrightarrow u}
  {\strut(\texttt{while~{\itshape b}~do~{\itshape S}, {\itshape s}}) \Longrightarrow u}
\\[2\jot]
\prftree[r]{\textsc{While-False}\quad if \li{b s} is false}
  {\strut(\texttt{while~{\itshape b}~do~{\itshape S}, {\itshape s}}) \Longrightarrow s}
\end{gather*}

Above, \li{a s} denotes the value of arithmetic expression \li{a} in state
\li{s}, and similarly for \li{b s}. Moreover, the syntax
$\texttt{\itshape s}\{\texttt{\itshape x} \mapsto \texttt{\itshape n}\}$
represents the state that is identical to \texttt{\itshape s} except that it
maps the variable~\texttt{\itshape x} to \texttt{\itshape n\/}. Formally:
\li|s{x ↦ n} = (λvar, if var = x then n else s var)|.
Exercise to the reader: Write the derivation tree
for the judgment \li|(x := x + y; y := 0,  [x ↦ 3, y ↦ 5])  ⟹  [x ↦ 8, y ↦ 0]|.

The derivation rules can be read intuitively. Consider \textsc{Seq} as an
example. The rule can be read as follows:
%
\begin{quote}
  If (1)~executing \texttt{\itshape S} in state \texttt{\itshape s} leads to
  state \texttt{\itshape t} and (2)~executing \texttt{\itshape T} in state
  \texttt{\itshape t} leads to state \texttt{\itshape u}, then
  executing the sequential composition \texttt{\itshape S; T} in state
  \texttt{\itshape s} leads to state \texttt{\itshape u}.
\end{quote}
%
The conditions (1) and (2) correspond to the two premises of \textsc{Seq}.

The most complicated rule is undoubtedly \textsc{While-True}. Intuitively, it
can be understood as follows:
%
\begin{quote}
  Assume the loop condition \texttt{\itshape b} is true in state
  \texttt{\itshape s\/}.
  If (1)~executing \texttt{\itshape S} in state~\texttt{\itshape s} leads to
  state \texttt{\itshape t} and (2)~executing the loop
  \texttt{while~{\itshape b}~do~{\itshape S}}
  from state \texttt{\itshape t} leads to state \texttt{\itshape u\/},
  then
  executing the loop \texttt{while~{\itshape b}~do~{\itshape S}} in
  state~\texttt{\itshape s} leads to state~\texttt{\itshape u\/}.
\end{quote}
%
Another way to think about \textsc{While-True} is in terms of sequential
composition. If the loop condition is true,
\texttt{while~{\itshape b}~do~{\itshape S}}
should be equivalent to
\texttt{{\itshape S}; while~{\itshape b}~do~{\itshape S}}.
The two premises of \textsc{While-True} correspond to the two premises of
the instance of the \textsc{Seq} rule for the statement
\texttt{{\itshape S}; while~{\itshape b}~do~{\itshape S}}.

In Lean, a big-step semantics judgment is represented by an inductive predicate
whose introduction rules correspond to the derivation rules above:

\lstinputlisting[linerange=big_step-q]{../lean/love08_operational_semantics_demo_master.lean}

Using an inductive predicate as opposed to a recursive function allows us to
cope with nontermination (e.g., a diverging \li{while}) and (for languages
richer than WHILE) nondeterminism. It also arguably provides a nicer syntax,
closer to the judgment rule syntax that is traditionally used in the
scientific literature.

We make ample use of implicit arguments, denoted by curly braces, for the
variables corresponding to the derivation rule's metavariables.

\section{Lemmas about the Big-Step Semantics}

Equipped with a big-step semantics, we can reason about concrete programs,
proving theorems relating final states with initial states. Perhaps more
interestingly, we can prove properties of the programming language, such as
equivalence proofs between program constructs and determinism.

We will take determinism as an example, stated thus: If \li{(S, s) ⟹ l}
and \li{(S, s) ⟹ r}, then \li{l = r}. Formally:

\lstinputlisting[linerange=big_step_unique-q]{../lean/love08_operational_semantics_demo_master.lean}

The proof is by rule induction over \li{(S, s) ⟹ l}, generalizing over \li{r}.
We give an informal proof sketch:

\begin{quote}
\textsc{Case} \textsc{Skip}: The only way to have \li{(skip, s) ⟹ l} or
\li{(skip, s) ⟹ r} is if \li{l = r = s}.

\medskip

\textsc{Case} \textsc{Asn}: Similar to \textsc{Skip}.

\medskip

\textsc{Case} \textsc{Seq}:
We have the hypotheses \li{(S, s) ⟹ t},
\li{(T, t) ⟹ l},
\li{(S, s) ⟹ t'},
and \li{(T, t') ⟹ r} and the induction hypotheses
\li|∀r : state, (S, s) ⟹ r → t = r| and
\li|∀r : state, (T, t) ⟹ r → l = r|. From the first induction hypothesis
together with \li{(S, s) ⟹ t'}, we derive \li{t =} \hbox{\li{t'}.} From the
second induction hypothesis together with \li{(T, t') ⟹ r}, we derive
\li{l = r}, as desired.

\medskip

\textsc{Case} \textsc{If-True}:
The only way to be in this case is if the condition \li{b s} is true.
As a result, \li{(if b then S₁ else S₂, s) ⟹ r} can only have been derived
using \textsc{If-True}; hence, \li{(S₁, s) ⟹ r}. The induction hypothesis is
\li{∀r : state,} \li{(S₁, s) ⟹ r → l = r}. We can apply \li{(S₁, s) ⟹ r} to
it to obtain the desired result \li{l = r}.

\medskip

\textsc{Case} \textsc{If-False}: Similar to \textsc{If-True}.

\medskip

\textsc{Case} \textsc{While-True}: Similar to \textsc{Seq}.

\medskip

\textsc{Case} \textsc{While-False}: Similar to \textsc{Skip}.
\end{quote}

When reasoning about an inductive predicate, it is often convenient to use
inversion rules
(Section~\ref{sec:introduction-elimination-induction-and-inversion}).
Accordingly, we define the following rules:

\lstinputlisting[linerange=big_step_skip_iff-q]{../lean/love08_operational_semantics_demo_master.lean}
\lstinputlisting[linerange=big_step_assign_iff-q]{../lean/love08_operational_semantics_demo_master.lean}
\lstinputlisting[linerange=big_step_seq_iff-q]{../lean/love08_operational_semantics_demo_master.lean}
\lstinputlisting[linerange=big_step_ite_iff-q]{../lean/love08_operational_semantics_demo_master.lean}
\lstinputlisting[linerange=big_step_while_iff-q]{../lean/love08_operational_semantics_demo_master.lean}
\lstinputlisting[linerange=big_step_while_true_iff-q]{../lean/love08_operational_semantics_demo_master.lean}
\lstinputlisting[linerange=big_step_while_false_iff-q]{../lean/love08_operational_semantics_demo_master.lean}

We add most of them to the simp set. We leave \li{big_step_while_true_iff} out
because it could make the simplifier loop due to the presence on the
right-hand side of a term that matches the left-hand side.

\section{Small-Step Semantics}

A limitation of big-step semantics is that they do not let us reason about
intermediate states. From a judgment \li{(S, s) ⟹ t}, all we see is the
initial state and the final state. This is for example too coarse-grained to
reason about concurrency with an interleaving semantics. Moreover, for
nondeterministic languages, big-step semantics offer no general way to express
termination: A judgment indicates a possibility (executing \li{S} in state
\li{s} may result in state \li{t}), not a necessity.

\emph{Small-step} (\emph{operational}) \emph{semantics} give us a
finer-coarsed view on computation. The transition relation has type
\li{program × state → program × state → Prop}.
Notice the presence of \li{program} in the type of the second operand. The
intuition is that \li{(S, s) ⇒ (T, t)} indicates that executing one step of
program \li{S} in state \li{s} leaves the program \li{T} to be executed, in
state \li{t}. If there is no program left to be executed, we put \li{skip}.

An \emph{execution} is a finite or infinite chain \li{(S₀, s₀) ⇒ (S₁, s₁) ⇒ ⋯}.
A pair \hbox{\li{(S, s)}} is called a \emph{configuration}; it is \emph{final} if
no transition of the form \li{(S, s) ⇒ _} is possible.
Here is an example execution:
%
\begin{center}
\begin{tabular}{r@{}l}
  & \hbox{\li|(x := x + y; y := 0, [x ↦ 3, y ↦ 5])|} \\
\hbox{\li|⇒|}~ & \hbox{\li|(skip; y := 0, [x ↦ 8, y ↦ 5])|} \\
\hbox{\li|⇒|}~ & \hbox{\li|(y := 0, [x ↦ 8, y ↦ 5])|} \\
\hbox{\li|⇒|}~ & \hbox{\li|(skip, [x ↦ 8, y ↦ 0])|}
\end{tabular}
\end{center}

The derivation rules for small-step semantics judgments are given below.

\begin{gather*}
\prftree[r]{\textsc{Asn}}
  {\strut( \texttt{\itshape x}~\texttt{:=}~\texttt{{\itshape a},}~
  \texttt{\itshape s})
  \Rightarrow (\texttt{skip,}~ \texttt{\itshape s}\{\texttt{\itshape x} \mapsto
  \texttt{{\itshape a}\;{\itshape s}}\})}
\\[2\jot]
\prftree[r]{\textsc{Seq-Step}}
  {\strut(\texttt{{\itshape S}, {\itshape s}}) \Rightarrow
    (\texttt{{\itshape S\/}$'$, {\itshape s}$'$})}
  {\strut(\texttt{{\itshape S}{;}\,{\itshape T}, {\itshape s}})
   \Rightarrow (\texttt{{\itshape S\/}$'${;}\,{\itshape T}, {\itshape s}$'$})}
\\[2\jot]
\prftree[r]{\textsc{Seq-Skip}}
  {\strut(\texttt{skip{;}\,{\itshape T}, {\itshape s}}) \Rightarrow
  (\texttt{{\itshape T}, {\itshape s}})}
\\[2\jot]
\prftree[r]{\textsc{If-True}\quad if \li{b s} is true}
  {\strut(\texttt{if~{\itshape b}~then~{\itshape S$_1$}~else~{\itshape S$_2$}, {\itshape s}})
  \Rightarrow (\texttt{{\itshape S$_1$}, {\itshape s}})}
\\[2\jot]
\prftree[r]{\textsc{If-False}\quad if \li{b s} is false}
  {\strut(\texttt{if~{\itshape b}~then~{\itshape S$_1$}~else~{\itshape S$_2$}, {\itshape s}})
  \Rightarrow (\texttt{{\itshape S$_2$}, {\itshape s}})}
\\[2\jot]
\prftree[r]{\textsc{While}}
  {\strut(\texttt{while~{\itshape b}~do~{\itshape S}, {\itshape s}}) \Rightarrow
  (\texttt{if {\itshape b} then (while~{\itshape b}~do~{\itshape S}, {\itshape s}) else skip})}
\end{gather*}

Unlike with the big-step semantics, there is no rule for the \li{skip}
statement in the small-step semantics. This is because a state of the form
\li{(skip, S)} is now considered final; \li{skip} is understood as the program
whose execution is vacuous. By inspection of the rules, it is easy to see that
a configuration is final if and only if its first component is \li{skip}.

There are two rules for sequential composition \li{S; T}. The first rule is
applicable if some progress can be made executing \li{S}. But if \li{S} is
\li{skip}, no progress can be made and the second rule applies.

The rules for \li{if} check the condition and, according to that, put the
``then'' or the ``else'' branch as the remaining computation to perform.

Finally, for the \li{while} loop, there is a single unconditional rule that
unfolds one iteration of the loop, introducing an \li{if} statement. It is
then the role of the \textsc{If-True} and \textsc{If-False} rules to process the
\li{if}. In the \textsc{If-True} case, we eventually reach the \li{while} loop
again. This can continue like this forever for infinite loops.

In Lean, the small-step semantics is specified as follows:

\lstinputlisting[linerange=small_step-q]{../lean/love08_operational_semantics_demo_master.lean}

Equipped with a small-step semantics, we can \emph{define} a big-step
semantics as follows:
%
\[\hbox{\li{(S, s) ⟹ t} if and only if \li{(S, s) ⇒* (skip, t)}}\]
%
where \li{r*} denotes the reflexive transitive closure of a relation \li{r}.
Alternatively, if we have already defined a big-step semantics, we can
\emph{prove} the above equivalence theorem to \emph{validate} our definitions.

We can prove that a configuration \li{(S, s)} is final if and only if
\li{S = skip}; this ensures that we have not forgotten a derivation rule.

The main disadvantage of small-step semantics is that we now have two
relations, \li{⇒} and \li{⇒*}, and the derivation rules and proofs tend to be
more complicated than with big steps.

\section{Lemmas about the Small-Step Semantics}

We can define inversion rules also about the small-step semantics. Here
are three examples:

\lstinputlisting[linerange=small_step_skip-q]{../lean/love08_operational_semantics_demo_master.lean}
\lstinputlisting[linerange=small_step_seq_iff-q]{../lean/love08_operational_semantics_demo_master.lean}
\lstinputlisting[linerange=small_step_ite_iff-q]{../lean/love08_operational_semantics_demo_master.lean}

A more important result is the connection between the big-step and the
small-step semantics. If \li{⇒*} denotes the reflexive transitive closure of
the small-step relation \li{⇒}, we have the following theorem:

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