
\documentclass{beamer}

\usetheme{Frankfurt}
\usecolortheme{seahorse}
% \usetheme{split}

\newcommand\comment[1]{} 
\AtBeginSection[]
{
   \begin{frame}
       \frametitle{Outline}
       \tableofcontents[currentsection]
   \end{frame}
}
\comment% \AtBeginSubsection[]
{
   \begin{frame}
       \frametitle{Outline}
       \tableofcontents[currentsection,currentsubsection]
   \end{frame}
}
\comment{
}

% monad related definitions
\newcommand\ext{\textit{ext}}
\newcommand\id{\textit{id}}
\newcommand\unit{\textit{unit}}
\newcommand\map{\textit{map}}
\newcommand\join{\textit{join}}
\newcommand\oo{\ensuremath{\circ}}
\newcommand\om{\ensuremath{\odot}}
\newcommand\swap{\textit{swap}}
\newcommand\prodd{\textit{prod}}
\newcommand\dorp{\textit{dorp}}
\newcommand\pext{\textit{pext}}
\newcommand\tc{\textit{\_tc}}
\newcommand\uc{\textit{\_uc}}
\newcommand\gc{\textit{\_gc}}
\newcommand\s{\textit{\_s}}
\newcommand\nt{\textit{\_nt}}
\newcommand\M{\ensuremath{_M}}
\newcommand\N{\ensuremath{_N}}
\newcommand\NM{\ensuremath{_{MN}}}
\newcommand\KM{$\mathcal{K}(M)$}
\newcommand\KNM{$\mathcal{K}(MN)$}
\newcommand\oM{\ensuremath{\odot_{M}}}
\newcommand\oN{\ensuremath{\odot_{N}}}
\newcommand\oNM{\ensuremath{\odot_{MN}}}

\newcommand\Cs{\ensuremath{\mathcal{C}}}
\newcommand\Bs{\ensuremath{\mathcal{B}}}
\newcommand\As{\ensuremath{\mathcal{A}}}
\newcommand\NonTerm{\texttt{NonTerm}}
\newcommand\Term{\texttt{Term}}
\newcommand\TorN{\texttt{TorN}}
\newcommand\bool{\textit{bool}}
\newcommand\set{\textit{set}}
\newcommand\state{\textit{state}}
\newcommand\outcome{\textit{outcome}}
\newcommand\tcres{\textit{tcres}}
\newcommand\choice{\textit{choice}}
\newcommand\ucl{\textit{up\_cl}}
\newcommand\ucss{\textit{ucss}}
\newcommand\evaluc{\textit{eval\_uc}}
\newcommand\ktoss{\textit{K\_to\_SS}}
\newcommand\Ball{\textit{Ball}}
\newcommand\Bex{\textit{Bex}}

% gs related definitions
\newcommand\magic{\textit{magic}}
\newcommand\abort{\textit{abort}}
\newcommand\skp{\textit{skip}}
\newcommand\frm{\textit{frame}}
\renewcommand\wp{\textit{wp}}
\newcommand\infchs{\textit{infchs}}
\newcommand\icnt{\textit{icnt}}
\newcommand\reachnt{\textit{reach\_NT}}

\title{Formalising Generalised Substitutions}
\author{Jeremy Dawson}
\institute{
Logic and Computation Program, NICTA
\thanks{National ICT Australia is funded by the Australian Government's
Dept of Communications, Information Technology and the Arts and
the Australian Research Council through Backing Australia's Ability
and the ICT Centre of Excellence program.}
\and
Automated Reasoning Group,
\\ Australian National University,
   Canberra, ACT 0200, Australia
\\ \url{http://users.rsise.anu.edu.au/~jeremy/} 
}

\begin{document}

\frame{\titlepage}

% \section[Outline]{}
\frame{
  \frametitle{Outline}
  \tableofcontents}

\section{Introduction}
\frame
{
  \frametitle{Introduction}
Dunne developed a theory of the \alert{generalised substitutions}
used in the B~method. \\[1ex]
He then proved properties of these 
generalised substitutions.  \\[1ex]
Theory based on total correctness:
contrast to \alert{abstract command} language,
based on \alert{general} correctness\\[1ex]

Both underlying ``models of computation'' based on a \alert{monad} \\[1ex]

Each of these is a \alert{compound monad}
  }

\section{The Operational Models} \label{s-om}
\comment{
\frame
{
  \frametitle{The Operational Models}
  }
  }

\subsection{The General Correctness Operational Model} \label{s-gcom}
\frame
{
  \frametitle{The General Correctness Operational Model}
  % Non-deterministic computations

  Want to distinguish computations which (on a given initial state) 
  \begin{itemize}
  \item fail to terminate
  \item terminate in final state $s$
  \item non-deterministically, either of the above
  \end{itemize}

  Neither $wlp$ / partial correctness \\
  nor $wp$ / total correctness does this. \\[1ex]

  General correctness refinement (Dunne): 
  $$A \sqsubseteq B \equiv wp(A,Q) \Rightarrow wp (B,Q) \land
   wlp(A,Q) \Rightarrow wlp (B,Q)$$
  }

\frame
{
  \frametitle{The General Correctness Operational Model}
  \framesubtitle{Type of Computations}
  A computation (on given state) produces a set of \alert{outcomes} \\[1ex]

  An \alert{outcome} is either
  \begin{itemize}
  \item \NonTerm, indicating non-termination, or
  \item \Term\ $s$, indicating termination in the state $s$.
  \end{itemize}
In Isabelle: 
{ \tt datatype $\sigma$ TorN = NonTerm | Term $\sigma$ } \\[1ex]

For a non-deterministic computation
(from given initial state), 
result is a \alert{set} of outcomes. \\[1ex]

type \outcome\ = \TorN\ \state\ \\[1ex]

type of computations is % $\state \to \state\ \TorN\ \set$
$\state \to \set\ \TorN\ \state$
  }

\subsection{The Total Correctness Operational Model} \label{s-tcom}
\frame
{
  \frametitle{The Total Correctness Operational Model}
  Only interested in total correctness (weakest preconditions). \\[1ex]

  Any computation which \alert{may} fail to terminate
fails every post-condition. \\[1ex]

Such computation is refinement-equivalent to a computation 
which \alert{does} fail to terminate. \\[1ex]

Type of results is either 
  \begin{itemize}
  \item \NonTerm, indicating \alert{possible} non-termination, or
  \item \Term\ $S$, indicating termination in a state $s \in S$.
  \end{itemize}

type of result \tcres\ (``total correctness result'') = % \state\ \set\ \TorN
\TorN\ \set\ \state
\\[1ex]
type of computations is $\state \to \TorN\ \set\ \state$
\\[1ex]
weakest precondition function (hence refinement):
$$[C]\ Q\ s = \exists S.\ (\forall x \in S.\ Q\ x) \land C\ s = \Term\ S$$ 

  }

\subsection{Confirming the Models} 
\frame
{
  \frametitle{Confirming the Models}

  In each case, to confirm model is appropriate,
  % having formally described a model of computation, 
  \begin{itemize}
  \item we show two computations refinement-equivalent 
  iff they are the same function (of type used in model) 
\item $A \sqsubseteq_{tc} B ~\land B ~ \sqsubseteq_{tc} A 
  ~\Rightarrow ~ A = B$
\item equivalently, $[A] = [B] \Rightarrow A = B$
  \item we define operations operationally, and prove these definitions
  correspond to Dunne's definitions (which use weakest preconditions)
  \end{itemize}
  (Caveat: we ignore ``frames''). \\[1ex]

  }

\section{The Monads used in these Models} \label{s-monmod}
\subsection{Monads} \label{s-monads}
\frame
{
  \frametitle{Monads}
Long known in category theory \\[1ex]

Define unit and extension functions, satisfying rules
\begin{align*}
\unit &: \alpha \to M \alpha \\[-0.5ex]
\ext &: (\alpha \to M \beta) \to (M \alpha \to M \beta) 
\end{align*}
\begin{align*}
\ext\ f \oo \unit & = f  \\[-0.5ex]
\ext\ \unit & = \id  \\[-0.5ex]
\ext\ (\ext\ g \oo f) & = \ext\ g \oo ext\ f  
\end{align*}
or functions \unit, \map\ and \join\ (7 axioms for these) \\[1ex]

Can represent the structure of a computation (Moggi)

  }
\frame
{
  \frametitle{Monads --- the Kleisli category}
$\ext\ B$ models the action of $B$ on result of previous computation \\[1ex]

Define $B \om A = \ext\ B \oo A$ :
sequencing computations $B$ and $A$. \\[1ex]
\unit\ models the computation which does nothing (\skp).%
% 
\begin{align*}
f \om \unit & = f \\[-0.5ex]
\unit \om f & = f \\[-0.5ex]
h \om (g \om f) & = (h \om g) \om f % \\
% \label{E3} \ext\ (g \om f) & = \ext\ g \oo ext\ f
\end{align*}

These properties are as expected for sequencing and \skp\\[1ex]
they give another category --- the \emph{Kleisli} category 
}

\comment% omit for TPHOLs \frame
{
  \frametitle{Monads --- the Kleisli category}
Properties above show that we have a category:

\begin{itemize}
\item objects are types
\item arrow from $\alpha$ to $\beta$ is function $\alpha \to M \beta$,
\item the identity arrow for object $\alpha$ is the function 
$\unit : \alpha \to M \alpha$ 
\item composition is given by \om.  
\end{itemize}
Called the Kleisli category of $M$, \KM.
%
% We can write \eqref{E3'} as \eqref{E3}, 
% and \eqref{E2} and \eqref{E3} also show that \ext\ is a functor from 
% \KM\ to the ordinary category of types and functions.

  }
\frame
{
  \frametitle{Monads --- Examples}
The \alert{non-termination} monad: 
a computation either terminates in a new state, or fails to terminate.
\begin{align*}
\unit\nt\ s & = \Term\ s \\[-0.5ex]
\map\nt\ f\ \NonTerm & = \NonTerm &
\map\nt\ f\ (\Term\ s) & = \Term\ (f\ s) \\[-0.5ex]
\ext\nt\ f\ \NonTerm & = \NonTerm &
\ext\nt\ f\ (\Term\ s) & = f\ s
\end{align*}

\pause 

The \alert{set} monad:
models non-deterministic (but necessarily terminating) computations.
\begin{align*}
\unit\s\ s & = \{s\} &
\join\s\ \As & = \textstyle \bigcup \As \\
\map\s\ f\ S & = \{f\ s \,|\, s \in S\} &
\ext\s\ f\ S & = \textstyle \bigcup_{s \in S} f\ s
\end{align*}
  }

\subsection{Compound Monads} \label{s-cms}
\frame
{
  \frametitle{Compound Monads}
Let $M$ and $N$,
each with unit and extension functions, be monads.
\\[1ex] 
Then is $M N \alpha$ a monad?  
Need $\unit\NM : \alpha \to M N \alpha$ and $\ext\NM$ 
\\[1ex]
\ext\NM\ ``extends'' a function $f$ from domain $\alpha$ to $M N \alpha$.
\\[1ex] 
\pext, ``partial extension'', does part of this
%
\begin{align*}
\ext\NM &: (\alpha \to M N \beta) \to (M N \alpha \to M N \beta) \\[-0.5ex]
\pext &: (\alpha \to M N \beta) \to (N \alpha \to M N \beta) 
\end{align*}
\pause
Definitions for a compound monad using \pext\ 
\begin{align*}
 \ext\NM\ g & = \ext\M\ (\pext\ g)  \\[-0.5ex]
 \unit\NM & = \unit\M \oo \unit\N
\end{align*}
Also require that \pext\ satisfies three rules
}
\comment% omit for TPHOLs \frame
{
  \frametitle{Compound Monads --- rules for \pext}
Rules that \pext\ needs to satisfy
\begin{align*}
 \pext\ f \oo \unit\N & = f  \\[-0.5ex]
 \pext\ \unit\NM & = \unit\M  \\[-0.5ex]
 \pext\ (\ext\NM\ g \oo f) & = \ext\NM\ g \oo pext\ f  
\end{align*}
\unit\NM\ and \pext\ are the unit and extension functions
of a monad \emph{in} the category \KM, whose Kleisli category is also \KNM.
  }

\subsection{The General Correctness Compound Monad} \label{s-gcmon}
\frame
{
  \frametitle{The General Correctness Compound Monad}
Want $\set\ \TorN\ \alpha$ is a monad; \\
in fact, for any monad $M$, $M\ \TorN\ \alpha$ is a monad
$$\pext : (\alpha \to M\ \TorN\ \beta) \to 
  (\TorN\ \alpha \to M\ \TorN\ \beta)$$%
\begin{align*} 
\pext\ f\ (\Term\ a) & = f\ a  \\ 
\pext\ f\ \NonTerm & = unit\M\ \NonTerm 
\end{align*} 
Proof of \pext\ rules easy.
  }

\subsection{The Total Correctness Compound Monad} \label{s-tcmon}
\comment% simplified slide for TPHOLs follows \frame
{
  \frametitle{The Total Correctness Compound Monad}
Recall \tcres\ = \TorN\ \set\ \state. 
\begin{align*}
\unit\tc & : \state \to \tcres \notag \\[-0.5ex]
  \prodd\tc & : \set\ \tcres \to tcres \notag \\[-0.5ex]
  \pext\tc & : (\state \to \tcres) \to \set\ \state \to \tcres \notag \\[-0.5ex]
  \ext\tc & : (\state \to \tcres) \to \tcres \to \tcres \notag  \\
\unit\tc\ s & = \Term\ \{s\} \\[-0.5ex]
 \prodd\tc\ S & = \NonTerm  \qquad \mbox{if $\NonTerm \in S$}\\[-0.5ex]
  \prodd\tc\ \{\Term\ s \,|\, s \in S\} & = 
    \Term\ (\textstyle \bigcup S) \\[-0.5ex]
 \pext\tc\ A\ S & = \prodd\tc\ \{A\ s \,|\, s \in S\} \\[-0.5ex]
 \ext\tc\ A\ S & = \ext\nt\ (\pext\tc\ A)\ S
\end{align*}
  }

% simplified slide for TPHOLs 
\frame
{
  \frametitle{The Total Correctness Compound Monad}
Recall \tcres\ = \TorN\ \set\ \state. 
  $$ \pext\tc : (\state \to \tcres) \to \set\ \state \to \tcres $$
  defined using 
  $$ \prodd\tc : \set\ \tcres \to tcres $$
\begin{align*}
 \prodd\tc\ S & = \NonTerm  \qquad \mbox{if $\NonTerm \in S$}\\
  \prodd\tc\ \{\Term\ s \,|\, s \in S\} & = 
    \Term\ (\textstyle \bigcup S) 
\end{align*}
  }

\subsection{Relating the General and Total Correctness monads}
\frame
{
  \frametitle{Relating the General and Total Correctness monads}
\begin{align*}
\swap\tc & : \set\ \TorN\ \sigma \to \TorN\ \set\ \sigma \notag \\
 \swap\tc\ S & = \NonTerm  \qquad \mbox{if $\NonTerm \in S$}\\[-0.5ex]
  \swap\tc\ \{\Term\ s \,|\, s \in S\} & = \Term\ S 
\end{align*}
$\swap\tc$ is also a \alert{monad morphism} \\
from the {general correctness} monad to the {total correctness} monad.
\begin{align*}
\unit\tc\ a & = \swap\tc\ (\unit\gc\ a) \\[-0.5ex]
\ext\tc\ (\swap\tc \oo f)\ (\swap\tc\ x) & = \swap\tc\ (\ext\gc\ f\ x) 
\end{align*}
Since it is \emph{surjective}, 
could use 
 monad axioms for {general correctness} monad to prove
 axioms for {total correctness} monad. \\[1ex]
For some other results also, easiest to prove for general correctness 
and use \swap\tc\ to ``transfer'' them to total correctness 
  }

\section{The Generalised Substitutions} \label{s-gs}
\frame
{
  \frametitle{Frames and Variables}
Each substitution has a \emph{frame},
loosely, the variables which ``might'' be affected.
But $\frm (x := x) = \{x\}$. \\[1ex]

Behaviour of command (alone) doesn't determine frame.\\[1ex]

Mostly we ignore frames.\\[1ex]

For many generalised substitution operations
(except assignment)
consider abstract machine state, not variables
}

\subsection{Definition of Commands} \label{s-defs}
\frame
{
  \frametitle{skip, sequencing, magic, abort}
  skip and sequencing given by \unit\ and \om\ of monad \\ ~

  \alert{define} \magic\ and \abort\ operationally; \\[1ex]

\begin{tt}
magic\_tc\_def = "magic\_tc s == Term \{\}" \\
abort\_tc\_def = "abort\_tc s == NonTerm" 
\end{tt} \\ ~
 
\pause 
\alert{prove}, as consequences, Dunne's definitions \\[1ex]
\begin{tt}
magic\_alt = "magic\_tc = guard\_tc (\%s.\ False) unit\_tc" \\
abort\_alt = "abort\_tc = precon\_tc (\%s.\ False) unit\_tc" 
\end{tt}
  }
\frame
{
  \frametitle{preconditioned command, guarded command}
  Again, we \alert{define} them operationally; \\[1ex]
\begin{tt}
"precon\_tc P C s = if P s then C s else NonTerm" \\
"guard\_tc P C s = if P s then C s else Term \{\}"
\end{tt} \\ ~

\pause 
 and \alert{prove}, as consequences, Dunne's definitions \\[1ex]
\begin{tt}
"wp\_tc (precon\_tc P C) Q s = (P s \& wp\_tc C Q s)" \\
"wp\_tc (guard\_tc P C) Q s = (P s --> wp\_tc C Q s)" 
\end{tt}
  }
\frame
{
  \frametitle{Definition of Commands --- Choice}
Defining by weakest precondition: \\
conjunction of individual weakest preconditions.
\\[1ex]
General Correctness: $\choice\gc\ \Cs\ s = \bigcup_{C \in \Cs} C\ s$. 
\\[1ex]
Total Correctness: \\
\choice\tc\ $\Cs$ can fail to terminate 
if any $C \in \Cs$ can fail to terminate.
\\[1ex]
$\choice\tc\ \Cs\ s  = \pext\tc\ (\lambda C.\ C\ s)\ \Cs$, expands to  
\begin{itemize}
\item
if $\{C\ s \,|\, C \in \Cs\}$ contains \NonTerm\ then 
$\choice\tc\ \Cs\ s = \NonTerm$
\item
if $\{C\ s \,|\, C \in \Cs\} = \{\Term\ S_C \,|\, C \in \Cs\}$,
then $\choice\tc\ \Cs\ s = \Term\ (\bigcup_{C \in \Cs} S_C)$
\end{itemize}

  }
\subsection{Repetition and Iteration} 
\frame
{
  \frametitle{Use of Coinductive Definitions}
  $A^0 = \skp$, $A^{n+1} = A\ ; A^n$ \\ ~

$A^\wedge$ is like choice of any $A^n$, 
also \NonTerm\ if infinite repetition possible 
(an ``infinite chain'') \\ ~

In [6] we defined an infinite chain by a function : $\mathbb N \to \state$
(satisfying conditions) \\ ~

Better to use Isabelle's coinductive definition facility, related proofs much
easier
  }
\frame
{
  \frametitle{Use of Coinductive Definitions}
$\infchs\tc\ C$:\ 
the set of states from which it is possible to 
execute $C$ infinitely many times sequentially  \\[1ex]

\begin{tt}
coinductive "infchs\_tc C"   \\ 
  ~~ intros "C s = Term S ==> ns :\ S ==> \\ 
   \hfill   ns :\ infchs\_tc C ==> s :\ infchs\_tc C"\\ 
\end{tt}
~ \\
\pause
$\reachnt\ C$:
the set of states from which \NonTerm\ is reachable \\[1ex]
\begin{tt}
inductive "reach\_NT C"\\ 
 ~~ intros "C s = NonTerm ==> s :\ reach\_NT C"\\ 
   ~~~~"C s = Term S ==> ns :\ S ==> \\
   \hfill ns :\ reach\_NT C ==> s :\ reach\_NT C" 
\end{tt}
  }
\frame
{
  \frametitle{Use of Coinductive Definitions}
$\icnt\tc\ C$:\ 
the states from which $C\ s$ gives \NonTerm\ \\[1ex]

\begin{tt}
coinductive "icnt\_tc C"\\ 
 ~~ intros "C s = NonTerm ==> s :\ icnt\_tc C"\\ 
   ~~~~"C s = Term S ==> ns :\ S ==> \\
   \hfill ns :\ icnt\_tc C ==> s :\ icnt\_tc C" \\[1ex]
\end{tt}

(same intro rules as for \texttt{reach\_NT} which was an inductive definition)
\\[1ex]
We then prove that $\icnt\tc\ C = \reachnt\ C \cup \infchs\tc\ C$
  }
\frame
{
  \frametitle{Definitions of $A^\wedge$}
  Dunne \alert{defined} $A^\wedge$ as a least-fixed point \\[1ex]

We use the operational definition for $A^\wedge$ and then \alert{prove} that
$A^\wedge$ is least fixpoint of $\lambda X.\ (A ; X)\ \Box\ \skp$
(where $\Box$ means choice) \\[1ex]

\begin{tt}
rephat\_def = "rephat C state == \\
 \hfill  if state :\ icnt\_tc C then NonTerm \hfill \mbox{} \\
  \hfill else Term (treach C state)" \\
fprep\_tc\_def = "fprep\_tc A X ==  \\
 \hfill X = choice\_tc {seq\_tc A X, unit\_tc}"  \\
rephat\_isfp = "fprep\_tc A (rephat A)"  \\
rephat\_is\_lfp = "fprep\_tc A Y ==> ref\_tc (rephat A) Y"  \\
\end{tt}
  }
\frame
{
  \frametitle{Other results}
  Least upper bound of set of generalised substitutions \\ ~

  Least upper bound of set of conjunctive predicate transformers \\ ~

  Generalised substitutions correspond to 
   predicate transformers satisfying a non-empty 
  conjunctivity condition \\ ~

  Discussion of results involving frames --- how to express them \\ ~

  Assorted further results from Dunne [8], see paper, also Appendix
  }

\end{document}
\comment{
\section{Conclusion}
\frame
{
  \frametitle{The End}
  The End 
  }
  }

