\Section{Optimisation validation}\sectionlabel{use case validation}
We turn to validating optimisations, and begin with the operation-wise
valid ones.

For each optimisation $\mopt$ in \{{Discard, Pure Hoist, Hoist}\}, we
define a set $\optset\mopt \subset \Opset$ of the operations that
satisfy its algebraic condition:
\begin{gather*}
  \optset{\text{Discard}} \definedby \set{\ndop, \reglookop \,\suchthat\,
    \mreg \in \RReg}
  \qquad
  \optset{\text{Pure Hoist}} \definedby \emptyset
  \\
  \optset{\text{Hoist}} \definedby \set{\raiseop, \throwop, \abortop,
    \rollbackop}
%, \sbot}
\end{gather*}

\begin{proposition}\propositionlabel{unary operation-wise validity}
  For each optimisation $\mopt$ in \{{Discard, Pure Hoist,
    Hoist}\}, if $\e \subset \optset\mopt$ then $\mopt$ is valid in
  the theory $\mL_{\e}$ of $\conservative\mModel$.
\end{proposition}

\begin{proof}%
  Note that $\tx\ndop\tx = \tx$ in $\NDTheory$ and $\NDTheory$ is a
  subtheory of $\mL$, not necessarily conservative. Therefore $\tx\ndop\tx = \tx$ holds in $\mL$.
  Similarly, for every $\mreg$ in $\RReg$, $\reglookop$
  satisfies the absorption law in $\EnvTheory[]$ or
  $\GlobalStateTheory[]$ and hence $\mL$.  Thus all operations in
  $\optset{\text{Discard}}$ satisfy the absorption law in $\mL$. If $\e
  \subset \optset{\text{Discard}}$, then every $\mop$ in $\e$
  satisfies the absorption law in $\mL$, and hence in the conservative
  restriction $\mL_{\e}$. By \theoremref{operationwise
    discard} $\mL_{\e}$ satisfies the Discard optimisation.

  A similar argument using \theoremref{operationwise hoist} shows the
  corresponding statement for Hoist. \theoremref{operationwise pure
    hoist} shows the statement for Pure Hoist holds.
\end{proof}

Analogously, for each $\mopt$ in \{{Swap, Weak Swap (WSwap), isolated
  swap (ISwap)}\} and for each $\mop \in \Opset$ define the set
$\optset\mopt(\mop)$ of effect operations that $\mopt$-commute with
$\mop$.  For the non-symmetric Weak Swap, this condition is that for
$\mop\of \arity\Ar\Pa$ and $\mop'\of\arity\Ar\Pa$, $ \mop'\in
\optset{\text{WSwap}}(\mop)$ if and only if for all $\mpa \in
\msem\Pa$ and $\mpa' \in \msem{\Pa'}$, $\mL$ proves that:
\begin{gather*}
  \mop_{\mpa}(\mop'_{\mpa'}(\tx_1, \ldots, \tx_1),
             \mop'_{\mpa'}(\tx_n, \ldots, \tx_n))
  \\=\\
  \mop'_{\mpa'}(\mop_{\mpa}(\tx_1, \ldots, \tx_n),
              \mop_{\mpa}(\tx_1, \ldots, \tx_n))
\end{gather*}
where $n$ is the cardinality of $\msem\Ar$.

Note that because Swap implies Weak Swap, which implies Isolated Swap, we
have
\(
\optset{\text{Swap}}(\mop) \subset \optset{\text{WSwap}}(\mop)
\subset\optset{\text{ISwap}}(\mop)
\).  These sets are given in \figureref{swap-sets}.

\begin{figure}
\vspace{-.4cm}
\Include{swap-sets}
\vspace{-.4cm}
\caption{\figurelabel{swap-sets}swap sets}
\end{figure}

From \theoremref{operationwise swap} we deduce the validity of swapping:

\begin{proposition}\propositionlabel{swap operation-wise validity}
  Let $\mopt$ be one of the three {Swap} optimisations.  Let
  $\e_1, \e_2 \subset \e$ be three effect sets.  If $\e_2 \subset \bigcap_{\mop
    \in \e_1} \optset\mopt(\mop)$ then the optimisation $\mopt$ is
  valid for
  $\mL_{\e_1}\to\mL_{\e}\from\mL_{\e_2}$.
\end{proposition}

\goodbreak

\begin{proof}%
We omit the $48$ calculations that show the operations in the middle three columns
of the table do indeed satisfy the corresponding swap law in $\mL$,
and hence in $\mL_{\e}$. Most of these calculations follow from the
tensor equations. All of these calculations are straightforward.
\theoremref{operationwise swap} completes the proof.
\end{proof}

Note that despite our brute force examination of about $160$ pairs of
effect operations, we are still exponentially better off than trying
to exhaust the space of $2^{16}$ possible pairs $\e_1$, $\e_2$.  In
\sectionref{mechanised analysis} we will generate these optimisation
tables mechanically.

We now turn to non-operation-wise valid optimisations, and begin with Copy.

\begin{proposition}\propositionlabel{copy validity}
  Let $\e \subset \Opset$ be any effect set.  If $\inputop, \updateop, \ndop
  \notin \e$ and, for all $\mreg$ in $\RWReg$, $\set{\reglookop,
    \regupop}  \nsubset \e$, then $\mL_{\e}$ validates the
  {Copy} optimisation.
\end{proposition}

\begin{proof}
The premise of the proposition guarantees that $\mL_{\e}$ has
a sub-signature of the signature for
\[
\mL' \definedby
\SignatureTheory{\set{\raiseop, \throwop}}
+
(\SignatureTheory{\set{\rollbackop, \abortop}}
\tensor
\Tensor\EnvTheory[]\tensor\Tensor\OverwriteTheory[])
\]
Moreover, if $\mL'_{\e}$ is the conservative restriction of $\mL'$ to
$\e$, then $\mL_{\e}$ satisfies all $\mL'_{\e}$-equations, and possibly
more.

Each combined theory validates the Copy optimisation. The first two
theories contain only constants, hence \theoremref{constant copy
  combination} is applicable. As $\OverwriteTheory[]$ is unary,
\theoremref{unary copy combination} is applicable for its
combination. As $\EnvTheory[]$ also validates Discard,
\theoremref{absorption copy combination} is applicable for its
combination. Thus, $\mL'$ satisfies the idempotency law, hence
$\mL'_{\e}$ also satisfies it. Consequently, $\mL_{\e}$ satisfies this
law too,
and therefore validates Copy.
\end{proof}

We treat the Weak Copy optimisation similarly:
\begin{proposition}\propositionlabel{weak copy validity}
  Let $\e \subset \Opset$ be any effect set.  If $\inputop, \outputop \notin
  \e$ and for all $\mreg$ in $\RWReg$, ${\set{\reglookop,
    \regupop}  \nsubset \e}$, then $\mL_{\e}$ validates the
  {Weak Copy} optimisation.
\end{proposition}

\begin{proof}%
  The difference from the previous proof is that we also need to
  consider the theory for non-determinism $\NDTheory$, which satisfies both Weak Copy and
  Discard. Therefore, we may apply \theoremref{absorption copy
    combination}. The rest of the proof is identical.
\end{proof}

Finally, we treat the Unique optimisation:
\begin{proposition}\propositionlabel{unique validity}
  Let $\e \subset \Opset$ be any effect set.  If $\e \intersect \set{%\sbot,
    \raiseop, \rollbackop} = \set\mop$ and ${\e \subset
  \optset{\text{Swap}}(\mop)}$, or if the intersection is
  empty, then $\mL_{\e}$ validates the {Unique}
  optimisation.
\end{proposition}

\begin{proof}%
  If the intersection is empty, then vacuously all nullary operations
  commute with every operation. If $\e \intersect \set{%\sbot,
    \raiseop, \rollbackop} = \set{\mop}$, then $\mop$ is the only
  nullary constant in $\e$. The condition $\e \subset
  \optset{\text{Swap}}(\mop)$ guarantees all $\e$-operations commute
  with $\mop$.
  %
  Either way, \theoremref{unique combination} ensures $\mL_{\e}$
  validates the Unique optimisation.
\end{proof}
