\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, to prove properties of the
semantics, and to reason about concrete programs.

This chapter is heavily inspired by Chapter~7 of \emph{Concrete Semantics:\ With
Isa\-belle\slash HOL}~\cite{nipkow-klein-2014}.

\section{Formal Semantics}
\label{sec:formal-semantics}

A formal semantics allows us to specify and reason about a programming language
and about individual programs written in that language. It can form the basis
of verified compilers, interpreters, verifiers, static analyzers, type
checkers, and more. Without formal proofs, these tools are almost always wrong.

Consider WebAssembly, a new machine-like language for web browsers,
designed as a portable target for compiling high-level languages such as C++
and Rust. A researcher, Conrad Watt \cite{watt-2018}, formalized its semantics
and type system using the Isa\-belle\slash HOL proof assistant. He found many
issues (our italics):
%
\begin{quote}
\tabletsmall
We have produced a full Isa\-belle mechanisation of the core execution semantics
and type system of the WebAssembly language. %(\S3).
In addition, we have created a mechanised proof for the type soundness
properties stated in the working group's paper. In order to complete this
proof, \emph{several deficiencies} in the official WebAssembly specification,
uncovered by our proof and modelling work, needed to be corrected by the
specification authors.
% (\S4).
In some cases, these meant that \emph{the type system was originally unsound}.

\begin{sloppypar}
We have maintained a constructive dialogue with elements of the working group,
mechanising and verifying new features as they are added to the
specification. In particular, the mechanism by which a WebAssembly
implementation interfaces with its host environment was not formally
specified in the working group's original paper. Extending our mechanisation
to model this feature \emph{revealed a deficiency} in the WebAssembly specification
that \emph{sabotaged the soundness of the type \hbox{system}}.
\end{sloppypar}
\end{quote}

Watt's research is only one example among many. Proof assistants are widely used
for programming language research. Every year, around 10\%--20\% of
papers presented at the Principles of Programming Languages (POPL) conference
are formalized. This is possible because comparatively little machinery is
needed to get started. The proofs tend to have lots of cases, which is a good
match for computers. Moreover, proof assistants are extremely convenient to
keep track of what needs to be changed as we extend a programming language with
more features.

\section{A Minimalistic Imperative Language}
\label{sec: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@{}}
\ttvar{S} & \li|::=| & \li|skip|
  & \text{(no-op)} \\
& $\mid$ & \ttvar{x} \li|:=| \ttvar{a}
  & \text{(assignment)} \\
& $\mid$ & \ttvar{S} \li|;| \ttvar{S}
  & \text{(sequential composition)} \\
& $\mid$ & \li|if| \ttvar{b} \li|then| \ttvar{S} \li|else| \ttvar{S}
  & \text{(conditional statement)} \\
& $\mid$ & \li|while| \ttvar{b} \li|do| \ttvar{S}
  & \text{(\li{while} loop)}
\end{tabular}
\end{center}
%
where \ttvar{S} stands for a \emph{statement} (also called
\emph{command} or \emph{program}), \ttvar{x} for a program variable,
\ttvar{a} for an arithmetic expression, and \ttvar{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 Booleans.

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

These two options correspond 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., \hbox{\li{aexp})} with a semantics (e.g., \li{eval}). 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 about a program's syntax. A shallow
embedding is more lightweight, because we can use it directly, without having
to define a semantics. A shallow embedding is its own semantics.

In Chapter~\ref{chap:monads}, we used a shallow embedding of effectful programs.
Here, we will use a deep embedding of programs (which we find interesting and
want to study closely) and a shallow embedding of arithmetic and Boolean
expressions (which we find less interesting). Our Lean definition of programs
follows:

\lstinputlisting[linerange=stmt-q]{../lean/love08_operational_semantics_demo_master.lean}
%
The infix syntax \li{S ;; T} abbreviates \li{stmt.seq S T}. We cannot use a
single semicolon \li{;} because it means ``and then''
(Section~\ref{sec:tactics-and-tactic-combinators}).

The correspondence between the inductive type's constructors and the WHILE
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.

The following small program illustrates deep embedding:

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

\section{Big-Step Semantics}
\label{sec:big-step-semantics}

An \emph{operational semantics} corresponds to an idealized 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.

In a \emph{big-step operational 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} may terminate in the state \li{t}.
\end{quote}
%
For deterministic languages, since programs always have a single outcome,
``may terminate'' means the same as ``must terminate'' or ``terminates.''

In accordance with the definition of WHILE programs, a state \li{s} is a
function of type \li{string → ℕ}. An example 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 represent the function
\hbox{\li{λv, if v =}} \li{"x" then 3 else if v = "y" then 5 else 0} and
similarly for \li{[x ↦ 8, y ↦ 0]}. Intuitively, the judgment holds.

The traditional 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{ssec:type-checking-and-type-inference}~and~\ref{sec:dependent-types}. The
derivation rules for big-step semantics judgments are given below. The rules
can be seen as an idealized interpreter for WHILE programs.

\vskip\abovedisplayskip

\centerline{\prftree[r]{\textsc{Skip}}
  {\strut\text{\li{(skip, s) ⟹ s}}}}

\vskip2\jot

\centerline{\prftree[r]{\textsc{Asn}}
  {\strut\text{\ttfamily\li{(x := a, s) ⟹ s}\{\li{x ↦ a s}\}}}}

\vskip2\jot

\centerline{\prftree[r]{\textsc{Seq}}
  {\strut\text{\li{(S, s) ⟹ t}}}
  {\strut\text{\li{(T, t) ⟹ u}}}
  {\strut\text{\li{(S; T, s) ⟹ u}}}}

\vskip2\jot

\centerline{\prftree[r]{\textsc{If-True}\quad if \li{b s} is true}
  {\strut\text{\li|(S, s) ⟹ t|}}
  {\strut\text{\li|(if b then S else T, s) ⟹ t|}}}

\vskip2\jot

\centerline{\prftree[r]{\textsc{If-False}\quad if \li{b s} is false}
  {\strut\text{\li|(T, s) ⟹ t|}}
  {\strut\text{\li|(if b then S else T, s) ⟹ t|}}}

\vskip2\jot

\centerline{\prftree[r]{\textsc{While-True}\quad if \li{b s} is true}
  {\strut\text{\li|(S, s) ⟹ t|}}
  {\strut\text{\li|(while b do S, t) ⟹ u|}}
  {\strut\text{\li|(while b do S, s) ⟹ u|}}}

\vskip2\jot

\centerline{\prftree[r]{\textsc{While-False}\quad if \li{b s} is false}
  {\strut\text{\li|(while b do S, s) ⟹ s|}}}

\vskip\belowdisplayskip

In the rules, \li{a s} denotes the value of arithmetic expression~\hbox{\li{a}} in
state \li{s}, and similarly for \li{b s}. Moreover, the syntax
\li|s{x ↦ n}| represents the state that is identical to \li{s} except that it
maps the variable~\li{x} to \li{n}. Formally:
%
\[\hbox{\lic|s{x ↦ n} = (λv, if v = x then n else s v)|}\]
%
This syntax and its automation are provided by \li{LoVelib}.

As an exercise, let us derive the example judgment above.
Let \hbox{\li{s :=}} \li{[x ↦ 3,} \li{y ↦ 5]}, \li{t := [x ↦ 8, y ↦ 5]}, and
\hbox{\li{u := [x ↦ 8, y ↦ 0]}.} Then we have
%
\[\prftree[r]{\textsc{Seq}}
  {\prftree[r]{\textsc{Asn}}
    {\strut\text{\li|(x := x + y, s) ⟹ t|}}}
  {\prftree[r]{\textsc{Asn}}
    {\strut\text{\li|(y := 0, t) ⟹ u|}}}
  {\strut\text{\li|(x := x + y; y := 0, s) ⟹ u|}}\]

The derivation rules can be read intuitively. Consider \textsc{Seq}:
%
\begin{quote}
If (1)~executing \li{S} in state \li{s} leads to state \li{t} and (2)~executing
\li{T} in state \li{t} leads to state \li{u}, then executing the sequential
composition \li{S; T} in state \li{s} leads to state \li{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 condition \li{b} is true in state \li{s}. If (1)~executing
\li{S} in state~\li{s} leads to state \li{t} and (2)~executing
\li{while} \li{b} \li{do} \li{S} from state \li{t} leads to state \li{u}, then executing
\li{while} \li{b} \li{do} \li{S} in state~\li{s} leads to state~\li{u}.
\end{quote}
%
Another way to think about \textsc{While-True} is in terms of loop unrolling. If
the loop condition is true, \li{while} \li{b} \li{do} \li{S} is equivalent to
the compound statement \li{S;}\ \li{while} \li{b} \li{do} \li{S}. The two
premises of \textsc{While-True} correspond to the two premises of the instance
of the \textsc{Seq} rule for \li{S; while b do S}.

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

\lstinputlisting[linerange=big_step-q]{../lean/love08_operational_semantics_demo_master.lean}
%
We use implicit arguments, within curly braces, for many of the variables
corresponding to the derivation rule's metavariables.

Using an inductive predicate as opposed to a recursive function allows us to
cope with nontermination (e.g., a diverging \hbox{\li{while})} and, for languages
richer than WHILE, nondeterminism. It also arguably provides a nicer syntax,
closer to the judgment rules that are traditionally used in the scientific
literature. If we were to attempt a recursive definition such as
%
\begin{lstlisting}
def eval : stmt → state → state
| stmt.skip         s := s
| (stmt.assign x a) s := s{x ↦ a s}
| (stmt.ite b S T)  s := if b s then eval S s else eval T s
| (S ;; T)          s := eval T (eval S s)
| (stmt.while b S)  s :=
  if b s then eval (stmt.while b S) (eval S s) else s
\end{lstlisting}
%
instead, we would face nontermination of the \li{stmt.while} case.
Indeed, since the program \li{stmt.while (λ_, true) stmt.skip} loops forever,
trying to evaluate it using \li{eval} would never return. (There are other
issues with the above definition, due to the use of \li{Prop} to represent
Boolean expressions.)

Equipped with a big-step semantics, we can reason about concrete programs such
as the one defined in Section~\ref{sec:a-minimalistic-imperative-language} and
prove lemmas such as the following:

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

\section{Properties of the Big-Step Semantics}
\label{sec:properties-of-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
determinism and nontermination.

We start with determinism. It may seem like a trivial property, but it is easy
to mistype a rule and obtain nondeterminism. For example, in the rule for
assignment,
if we mistakenly write \li|big_step (stmt.assign x a, s) (s{y ↦ a s})|
with \li{y} instead of \li{x}, we suddenly can use the rule to modify any
variable \li{y} we please. In other words, an execution of the program could
modify any variable at random. So let us verify that our WHILE language really
is deterministic:

\lstinputlisting[linerange=big_step_deterministic-q]{../lean/love08_operational_semantics_demo_master.lean}
%
The Lean proof is in the demonstration file associated with this chapter. We
content ourselves with an informal proof sketch:
%
\begin{quote}
The proof is by rule induction over \li{(S, s) ⟹ l}. %, generalizing over \li{r}.

\textsc{Case} \textsc{Skip}: To have \li{(skip, s) ⟹ l} or
\hbox{\li{(skip, s) ⟹ r}}, we need \li{l = r = s}.

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

\textsc{Case} \textsc{Seq}:
We have the hypotheses \li{(S, s) ⟹ t},
\li{(T, t)} \li{⟹ l},
\hbox{\li{(S, s)}} \hbox{\li{⟹ t'},}
and \li{(T, t') ⟹ r} and the induction hypotheses
\li|∀r, (S, s)| \li|⟹ r → t = r| and
\li|∀r, (T,| \li|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}.

\textsc{Case} \textsc{If-True}:
Since \li{b s} is true, \hbox{\li{(if b then S else T, s)}}
\hbox{\li{⟹ r}} can only have been derived using \textsc{If-True} and thus
\hbox{\li{(S, s) ⟹ r}.} The induction hypothesis is
\li|∀r,| \hbox{\li|(S, s)|} \li|⟹ r → l = r|. We can apply \li{(S, s) ⟹ r} to
it to obtain \hbox{\li{l = r}.}

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

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

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

Given that the WHILE language is deterministic, for the big-step semantics,
termination would amount to the following:
%
\lstinputlisting[linerange=big_step_terminates-q]{../lean/love08_operational_semantics_demo_master.lean}
%
This property means that for every statement \li{S} and
state~\hbox{\li{s},} there exists a state \li{t} such that executing \li{S}
starting in \li{s} may terminate in \li{t}. Because WHILE is deterministic,
``may terminate'' means the same as ``must terminate.''

However, the property does not hold. The big-step semantics can be used to show
that \li{stmt.while (λ_, true) S} will never terminate, regardless of the start
state:

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

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

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

We add most of the rules to the simp set. We leave out \li{big_}\allowbreak\li{step_while_iff} and
\li{big_step_while_true_iff} because they could make \li{simp} loop, due to the
presence on the right-hand side of a term that matches the left-hand side.

\section{Small-Step Semantics}
\label{sec: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 \li{s} and the final state \li{t}. This is too coarse-grained to reason
about multithreaded programs, where several processes can interact with each
other's intermediate states. 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} \emph{may} result in state
\li{t}), not a necessity.

\emph{Small-step operational semantics} provide a finer view. The transition
predicate \li{⇒} has type \li{stmt × state → stmt × state → Prop}.
Intuitively, \hbox{\li{(S, s) ⇒}} \hbox{\li{(T, t)}} means 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 nothing left to be executed, we put \li{skip}.

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

If we take the analogy of a computer processor, the \li{S} component of a
configuration \li{(S, s)} can be thought of as a program counter, which
indicates which instructions should be executed next. The step-by-step execution
of a program resembles running a program in a debugger with a breakpoint at
every step.

The valid small-step judgments are given as derivation rules:

\vskip\abovedisplayskip

\centerline{\prftree[r]{\textsc{Asn}}
  {\strut\text{\ttfamily\li{(x := a, s) ⇒ (skip, s}\{\li{x ↦ a s}\}\li{)}}}}

\vskip2\jot

\centerline{\prftree[r]{\textsc{Seq-Step}}
  {\strut\text{\li{(S, s) ⇒ (S', s')}}}
  {\strut\text{\li{(S; T, s) ⇒ (S'; T, s')}}}}

\vskip2\jot

\centerline{\prftree[r]{\textsc{Seq-Skip}}
  {\strut\text{\li{(skip; T, s) ⇒ (T, s)}}}}

\vskip2\jot

\centerline{\prftree[r]{\textsc{If-True}\quad if \li{b s} is true}
  {\strut\text{\li{(if b then S else T, s) ⇒ (S, s)}}}}

\vskip2\jot

\centerline{\prftree[r]{\textsc{If-False}\quad if \li{b s} is false}
  {\strut\text{\li{(if b then S else T, s) ⇒ (T, s)}}}}

\vskip2\jot

\centerline{\prftree[r]{\textsc{While}}
  {\strut\text{\li{(while b do S, s) ⇒ (if b then (S; while b do S) else skip, s)}}}}

\vskip\belowdisplayskip

The rules are reminiscent of the tennis game transition system of
Section~\ref{ssec:tennis-games}. These, too, specified small steps:\ from
\li{0–0} to \li{15–0}, to \li{15–15}, and so on.

Unlike in the big-step semantics, there is no rule for \li{skip}
in the small-step semantics. This is because a configuration of the form
\li{(skip, s)} is considered final; \li{skip} is understood as the statement
whose execution is vacuous. By inspection of the rules, we can convince
ourselves that a configuration is final if and only if its first component is
\li{skip}.

Two rules concern 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 \li{b} and, depending on its
truth value, put the \li{then} or the \li{else} branch as the remaining
computation to perform.

For the \li{while} loop, there is a single unconditional rule that
expands 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 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}

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

The main disadvantage of small-step semantics is that we now have two
predicates, \li{⇒} and \li{⇒*}, and the derivation rules and proofs tend to be
more complicated than with big steps. This is clearly visible on the following
example, which requires us to apply the lemma
%
\begin{center}
\begin{tabular}{@{}r@{}l@{}}
\lic|star.head| & \lic| : ?r ?a ?b → star ?r ?b ?c → star ?r ?a ?c| \\
\end{tabular}
\end{center}
%
once for each small step:

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

\section{Properties of the Small-Step Semantics}
\label{sec:properties-of-the-small-step-semantics}

We can prove that a configuration \li{(S, s)} is final if and only if
\hbox{\li{S =}} \hbox{\li{skip}.}
Doing so ensures that we have not forgotten a derivation rule and
hence that the small-steps semantics cannot get stuck.
The lemma statement is as follows:
%
\lstinputlisting[linerange=small_step_final-q]{../lean/love08_operational_semantics_demo_master.lean}
%
The proof is by structural induction on \li{S}.

Like the big-step semantics, the small-step semantics is deterministic:
%
\lstinputlisting[linerange=small_step_deterministic-q]{../lean/love08_operational_semantics_demo_master.lean}
%
The proof is by rule induction on \li{hl} or \li{hr}.

For the small-step semantics, a configuration \li{(S₀, s₀)} terminates if
all executions starting in it are finite:
\li|(S₀, s₀) ⇒| \hbox{\li|(S₁, s₁)|} \li|⇒ ⋯ ⇒ (Sₙ, sₙ)|.
It is nonterminating if there exists
an infinite chain \li{(S₀, s₀) ⇒ (S₁, s₁) ⇒ ⋯}. The programming language as a
whole is terminating if and only if all its configurations terminate. It is
easy to show that the WHILE language is nonterminating, by taking
\li{S₀ := stmt.while (λ_, true) stmt.skip}. For any \li{s₀}, we then have
%
\[\hbox{\li{(S₀, s₀) ⇒ (S₀, s₀) ⇒ (S₀, s₀) ⇒ ⋯}}\]

We can define inversion rules about the small-step semantics, such as these:

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

A more fundamental result is the equivalence between the big-step and the
small-step semantics:

\lstinputlisting[linerange=big_step_iff_star_small_step-q]{../lean/love08_operational_semantics_demo_master.lean}
%
Recall that \li{⇒*} denotes the reflexive transitive closure of the small-step
predicate \li{⇒}. The theorem's proof is beyond the scope of this course. We
refer to Chapter~7 of \emph{Concrete Semantics: With Isa\-belle\slash
HOL}~\cite{nipkow-klein-2014} or to the demonstration file for this chapter.

\section{Parallelism}
\label{sec:parallelism}

The WHILE language is a sequential language:\ one in which statements are
executed in turn, without interruptions or interference. In this section, we
will consider \emph{PAR}, an extension of WHILE with top-level parallelism. A
PAR program consists of a list \li{[S₁, …, Sₙ]} of WHILE programs. The
individual WHILE programs are executed in parallel, as their own threads, using
an interleaving semantics. This means that the semantics of the entire PAR
program is given by interleaving small steps of the threads.

A PAR configuration \li{(Ss, s)} consists of a list \li{Ss} of WHILE programs
and a state~\li{s}. A PAR step can be defined as follows:
%
\lstinputlisting[linerange=par_step-q]{../lean/love08_operational_semantics_demo_master.lean}
%
Informally, from an arbitrary configuration \hbox{\li{(Ts ++ [S] ++ Us, s)},} we can
make a small step to \li{(Ts ++ [S'] ++ Us, s')} whenever
\hbox{\li{(S, s) ⇒}} \hbox{\li{(S', s')}.} The \li{par_step} predicate's first
argument is the index of the thread that makes a transition.

To see that PAR is nondeterministic, consider the program \hbox{\li{[S₀, S₁]}},
with
\begin{align*}
  & \hbox{\lic{S₀ := stmt.assign "x" (λ_, 42)}}
& & \hbox{\lic{S₁ := stmt.assign "x" (λ_, 999)}}
\end{align*}
and consider the start state \li{s}. Taking a \li{par_step 0} step
results in the configuration \hbox{\li$([stmt.skip, S₁], s{x ↦ 42})$,}
whereas taking a \li{par_step 1} step results in
\li$([S₀, stmt.skip], s{x ↦ 999})$.

\begin{sloppypar}
Sometimes the nondeterminism is harmless, if the final result is the same. This
is called \emph{determinacy}. In particular, some languages enjoy the diamond
property:
%
\lstinputlisting[linerange=par_step_diamond-q]{../lean/love08_operational_semantics_demo_master.lean}
%
The diamond property implies determinacy. However, PAR is not determinate, and
hence cannot enjoy the diamond property. If we take \li{par_step 0} followed
by \li{par_step 1}, we inevitably reach the final state
\hbox{\li$([stmt.skip, stmt.skip],$} \hbox{\li$s{x ↦ 999})$,} whereas if we
start with \li{par_step 1} and then take \li{par_step 0}, we inevitably reach
\li$([stmt.skip, stmt.skip], s{x ↦ 42})$, a counterexample both to determinacy
and to the diamond property.
\end{sloppypar}

The counterexample has two threads writing to the same variable \li{x}. If we
were to restrict access to variables written by other threads, we could salvage
the diamond property. First, we need some auxiliary definitions:
%
\lstinputlisting[linerange=stmt.W_etc-q]{../lean/love08_operational_semantics_demo_master.lean}
%
The function \li{stmt.W} returns the set of variables written by a thread,
\li{stmt.R} is the set of variables read by a thread, and \li{stmt.V} is the
set of variables written or read by a thread. Notice the markedly semantic
definition of \li{exp.R}: A variable \li{x} is read by a shallowly embedded
arithmetic or Boolean expression \li{f} if there exists a state \li{s} and a
value \li{n} such that setting \li{x} to \li{n} in \li{s} influences \li{f}'s
behavior. If we had a deep embedding of arithmetic and Boolean expressions, we
could perform a syntactic analysis instead (as we do in \li{stmt.R} for
programs).

Using the above definitions, we can revise the diamond property:
%
\lstinputlisting[linerange=par_step_diamond_VW_disjoint-q]{../lean/love08_operational_semantics_demo_master.lean}
%
This proposition looks plausible, but considering Conrad Watt's experience with
WebAssembly and that of dozens of other researchers, we should not put too much
faith in it until we have established it formally.
