\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
incorrect.

Consider WebAssembly, a new assembly-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, a substantial fraction of the
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}

We introduce \emph{WHILE}%
\footnote{Fans of backronyms might enjoy this one:\ Weak Hypothetical
  Imperative Language Example.},
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{fun s : State ↦ s "x" + s "y" + 1}, and \li{a ≠ b} would be represented by
  the predicate \hbox{\li{fun s : State ↦}} \hbox{\li{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:effectful-programming}, 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,keywords={inductive,Type,where,Prop}]{../lean/LoVe/LoVe09_OperationalSemantics_DemoMaster.lean}
%
The infix syntax \li{S; T} abbreviates \li{Stmt.seq S T}.

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 all possible variable names exist in the state and are assigned a value.

The following small program illustrates the deeply embedded WHILE syntax
(and its shallowly embedded aspects):

\lstinputlisting[linerange=sillyLoop-q]{../lean/LoVe/LoVe09_OperationalSemantics_DemoMaster.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 such as WHILE, 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{fun v ↦}} \li{if v = "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{sec: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{Assign}}
  {\strut\text{\ttfamily\li{(x := a, s) ⟹ s[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] = (fun v ↦ if v = x then n else s v)|}\]
%
This syntax is provided by \li{LoVelib}.

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}.

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{Assign}}
    {\strut\text{\li|(x := x + y, s) ⟹ t|}}}
  {\prftree[r]{\textsc{Assign}}
    {\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}.

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

\lstinputlisting[linerange=BigStep-q,keywords={inductive,Prop,where}]{../lean/LoVe/LoVe09_OperationalSemantics_DemoMaster.lean}

Using an inductive predicate as opposed to a recursive function allows us to
cope with nontermination (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 instead 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.ifThenElse b S T, s =>
    if b s then eval S s else eval T s
  | S; T,                  s => eval T (eval S s)
  | Stmt.whileDo b S,      s =>
    if b s then eval (Stmt.whileDo b S) (eval S s) else s
\end{lstlisting}
%
we would face nontermination of the \li{Stmt.whileDo} case.
Indeed, since the program \li{Stmt.whileDo (fun _ ↦ True) Stmt.skip} loops forever,
trying to evaluate it using \li{eval} would never return.

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 theorems such as the following:

\lstinputlisting[linerange=sillyLoop_from_1_BigStep-q]{../lean/LoVe/LoVe09_OperationalSemantics_DemoMaster.lean}

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

A big-step semantics allows us to reason about concrete programs, proving
theorems relating final states with initial states. Perhaps as importantly, it
allows us to 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 \hbox{\li|BigStep|} \li|(Stmt.assign x a, s) (s[y ↦ a s])|
with \li{y} instead of \li{x}, we can suddenly 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=BigStep_deterministic-q]{../lean/LoVe/LoVe09_OperationalSemantics_DemoMaster.lean}
%
The Lean proof is in the demonstration file associated with this chapter.
For technical reasons, the pair \li|(S, s)| is represented by a single variable
\li|Ss|. 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}, we need \li{l = s}.
Similarly, by case analysis on \li{(skip, s) ⟹ r}, we obtain \li{r = s}.
Hence, \li{l = r}.

\textsc{Case} \textsc{Assign}: 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
\hbox{\li|∀r, (S, s)|} \hbox{\li|⟹|} \hbox{\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 \hbox{\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 \hbox{\li{(S,}} \li{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=BigStep_terminates-q]{../lean/LoVe/LoVe09_OperationalSemantics_DemoMaster.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.whileDo (fun _ ↦ true) S} will never terminate, regardless of the start
%state:
%\lstinputlisting[linerange=BigStep_doesnt_terminate-q]{../lean/LoVe/LoVe09_OperationalSemantics_DemoMaster.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=BigStep_skip_iff-q]{../lean/LoVe/LoVe09_OperationalSemantics_DemoMaster.lean}
\betweenlistings
\lstinputlisting[linerange=BigStep_assign_iff-q]{../lean/LoVe/LoVe09_OperationalSemantics_DemoMaster.lean}
\betweenlistings
\lstinputlisting[linerange=BigStep_seq_iff-q]{../lean/LoVe/LoVe09_OperationalSemantics_DemoMaster.lean}
\betweenlistings
\lstinputlisting[linerange=BigStep_if_iff-q]{../lean/LoVe/LoVe09_OperationalSemantics_DemoMaster.lean}
\betweenlistings
\lstinputlisting[linerange=BigStep_while_iff-q]{../lean/LoVe/LoVe09_OperationalSemantics_DemoMaster.lean}
\betweenlistings
\lstinputlisting[linerange=BigStep_while_true_iff-q]{../lean/LoVe/LoVe09_OperationalSemantics_DemoMaster.lean}
\betweenlistings
\lstinputlisting[linerange=BigStep_while_false_iff-q]{../lean/LoVe/LoVe09_OperationalSemantics_DemoMaster.lean}

We add the rules to the simp set, except for \li{BigStep_}\allowbreak\li{while_Iff}, which would make \li{simp} loop.

\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, \li{(S, s) ⇒} \li{(T,} \li{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 \hbox{\li{(S₀, s₀) ⇒ (S₁, s₁) ⇒}} \li{⋯}
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 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
each step.

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

\vskip\abovedisplayskip

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

\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 trivial. 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=SmallStep-q]{../lean/LoVe/LoVe09_OperationalSemantics_DemoMaster.lean}

Based on a small-step semantics, we can \emph{define} a big-step semantics as
follows:
%
\[\hbox{\li{(S, s) ⟹ t}\quad if and only if\quad \li{(S, s) ⇒* (skip, t)}}\]
%
where \li{p*} denotes the reflexive transitive closure (\li|RTC|) 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, in which we need to apply the theorem
%
\begin{center}
\begin{tabular}{@{}r@{}l@{}}
\lic|RTC.head| & \lic| : ?R ?a ?b → RTC ?R ?b ?c → RTC ?R ?a ?c| \\
\end{tabular}
\end{center}
%
once for each small step:

\lstinputlisting[linerange=sillyLoop_from_1_SmallStep-q]{../lean/LoVe/LoVe09_OperationalSemantics_DemoMaster.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 theorem statement is as follows:
%
\lstinputlisting[linerange=SmallStep_final-q]{../lean/LoVe/LoVe09_OperationalSemantics_DemoMaster.lean}
%
The proof is by structural induction on \li{S}.

Like the big-step semantics, the small-step semantics is deterministic:
%
\lstinputlisting[linerange=SmallStep_deterministic-q]{../lean/LoVe/LoVe09_OperationalSemantics_DemoMaster.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.whileDo (fun _ ↦ 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=SmallStep_skip-q]{../lean/LoVe/LoVe09_OperationalSemantics_DemoMaster.lean}
\betweenlistings
\lstinputlisting[linerange=SmallStep_seq_iff-q]{../lean/LoVe/LoVe09_OperationalSemantics_DemoMaster.lean}
\betweenlistings
\lstinputlisting[linerange=SmallStep_if_iff-q]{../lean/LoVe/LoVe09_OperationalSemantics_DemoMaster.lean}

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

\lstinputlisting[linerange=BigStep_iff_RTC_SmallStep-q]{../lean/LoVe/LoVe09_OperationalSemantics_DemoMaster.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.
