\documentclass{beamer} \usetheme{Frankfurt} \usecolortheme{seahorse} % \usetheme{split} \newcommand\comment[1]{} \newcommand\clabel[1]{} \AtBeginSection[] { \begin{frame} \frametitle{Outline} \tableofcontents[currentsection] \end{frame} } \comment% \AtBeginSubsection[] { \begin{frame} \frametitle{Outline} \tableofcontents[currentsection,currentsubsection] \end{frame} } \comment{ } \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}} \def\dem{\mathop{\rm dem}} \def\ang{\mathop{\rm ang}} \title{Compound Monads in Specification Languages} \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} Several sorts of refinement suggested by Dunne. \\ \begin{itemize} \item General Correctness \item Total Correctness \item Chorus Angelorum \end{itemize} Each is based, implicitly or explicitly, on a notion of what a computation is, an underlying ``model of computation'' \\[1ex] Each underlying ``model of computation'' is based on a \alert{monad} \\[1ex] Each of these monads is, or is somewhat like, 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}. 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$ } 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} Related to semantics of the B-method, \\ only interested in total correctness (weakest preconditions). \\[1ex] A 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{The Chorus Angelorum Operational Model} \label{s-chom} \frame { \frametitle{The Chorus Angelorum Operational Model} Ordinarily, non-determinism is \alert{demonic} choice \\ (all possible results must satisfy post-condition $\equiv$ \\ the result chosen by a \alert{demon} satisfies post-condition) \\[1ex] Want to model \alert{angelic} and \alert{demonic} non-determinism \\[1ex] Computation returns a \alert{set of sets} \As\ of states: \begin{itemize} \item angel chooses set $A \in \As$ \item demon chooses state $a \in A$ \end{itemize} weakest precondition function (hence refinement): $$ [C]\ Q\ s = \exists U \in C\ s.\ (\forall u \in U.\ Q\ u)$$ If $A \in \As$, $A' \supseteq A$, to include $A'$ in \As, or not, makes no difference: \\ consider only \As\ \alert{up-closed}: if $A' \supseteq A$ and $A \in \mathcal A$ then $A' \in \mathcal A$. } \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 we \alert{define} operations operationally, and \alert{prove} these definitions correspond to Dunne's definitions (which use weakest preconditions) \end{itemize} (Caveat: we ignore ``frames''). \\[1ex] Note: all proofs in the theorem prover Isabelle/HOL } \section{The Monads used in these Models} \label{s-monmod} \subsection{Monads} \label{s-monads} \frame { \frametitle{Monads} Long known in category theory. ~ 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*} \clabel{E1} \ext\ f \oo \unit & = f \\[-0.5ex] \clabel{E2} \ext\ \unit & = \id \\[-0.5ex] \clabel{E3'} \ext\ (\ext\ g \oo f) & = \ext\ g \oo ext\ f \end{align*} or functions \unit, \map\ and \join\ (7 axioms for these) ~ 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$. % % The unit function models the computation which does nothing (\skp). % \begin{align} \label{krid} f \om \unit & = f \\[-0.5ex] \label{klid} \unit \om f & = f \\[-0.5ex] \label{kass} h \om (g \om f) & = (h \om g) \om f % \\ % \label{E3} \ext\ (g \om f) & = \ext\ g \oo ext\ f \end{align} \pause Properties \eqref{krid} to \eqref{kass} 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 using \pext\ for a compound monad % \label{E3K} \pext\ (g \oNM f) & = \pext\ g \oM pext\ f \\ \begin{align*} \clabel{EC} \ext\NM\ g & = \ext\M\ (\pext\ g) \\[-0.5ex] \clabel{UC} \unit\NM & = \unit\M \oo \unit\N \end{align*} } \frame { \frametitle{Compound Monads --- rules for \pext} \pext\ also must satisfy three rules \begin{align*} \clabel{E1K'} \pext\ f \oo \unit\N & = f \\ \clabel{E2K} \pext\ \unit\NM & = \unit\M \\ \clabel{E3'K_o} \pext\ (\ext\NM\ g \oo f) & = \ext\NM\ g \oo pext\ f \end{align*} % Note that in view of \eqref{EC}, \eqref{E3'K_o} and \eqref{E3K} % are equivalent, and that \eqref{E2K} and \eqref{E3K} give that % \pext\ is a functor from \KNM\ to \KM. \unit\NM\ and \pext\ are the unit and extension functions of a monad \emph{in} the category \KM, whose Kleisli category is also \KNM. } \frame { \frametitle{Compound Monads --- Distributive Law} Jones \& Duponcheel: two conditions, J(1) and J(2), \\ which compound monads may satisfy. ~ Assuming $\unit\NM = \unit\M \oo \unit\N$ and $\map\NM = \map\M \oo \map\N$, \\ compound monads arise from a function \pext\ iff J(1) holds ~ Compound monads satisfying J(1) and J(2) are those arising from a \alert{distributive law} $\swap : N M \alpha \to M N \alpha$ \\ A {distributive law} satisfies S(1) to S(4) of Jones \& Duponcheel $$\swap = \pext\ (\map\M\ \unit\N)$$ } \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 \clabel{pextTerm} \\ \pext\ f\ \NonTerm & = unit\M\ \NonTerm \clabel{pextNT} \end{align*} Proof of \pext\ axioms easy. ~ Arises from a distributive law: $\swap = \pext\ (\map\M\ \unit\N)$, so $$\swap\gc : \TorN\ \set\ \alpha \to \set\ \TorN\ \alpha$$ \begin{align*} \swap\gc\ \NonTerm & = \{\NonTerm\} \\ \swap\gc\ (\Term\ S) & = \{\Term\ s \,|\, s \in S\} \end{align*} } \subsection{The Total Correctness Compound Monad} \label{s-tcmon} \comment% simplified slide 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 \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*} } \frame { \frametitle{The Total Correctness Compound Monad} \framesubtitle{A Distributive Law and Monad Morphism} Total Correctness monad also arises from a distributive law: \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*} } \subsection{Relating the General and Total Correctness monads} \frame { \frametitle{Relating the General and Total Correctness monads} $\swap\tc : \set\ \TorN\ \sigma \to \TorN\ \set\ \sigma$ 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. } \subsection{The Chorus Angelorum Monad} \label{s-chmon} \frame { \frametitle{The Chorus Angelorum Monad} \framesubtitle{up-closure, swapping angel and demon} Result $\As : \set\ \set\ \state$ (up-closed): \\ angel chooses $A \in \As$, demon chooses $a \in A$. \\[1ex] Alternative model: demon chooses first, then angel. \\[1ex] \swap\uc\ turns angel-chooses-first result into demon-chooses-first. \\[1ex] \ucl: the \emph{up-closure} of a set of sets. \begin{align*} \swap\uc\ \As & = \{B \,|\, \forall A \in \As.\ B \cap A \not= \{\}\} \\[-0.5ex] \ucl\ \As & = \{A' \,|\, \exists A \in \As.\ A \subseteq A'\} \end{align*} \pause \begin{align*} \ucl\ (\ucl\ \As) & = \ucl\ \As & \swap\uc\ (\swap\uc\ \As) & = \ucl\ \As \\[-0.5ex] \swap\uc\ (\ucl\ \As) & = \swap\uc\ \As & \ucl\ (\swap\uc\ \As) & = \swap\uc\ \As \end{align*} So work on equivalence classes of sets of sets of states \\ $\As \equiv \As'$ iff $\ucl\ \As = \ucl\ \As'$ \\ each equivalence class has exactly one up-closed member. } \frame { \frametitle{The Chorus Angelorum Monad} \framesubtitle{proofs of monad rules} \begin{itemize} \item try to prove S(1) to S(4) (to show distributive law): \\ cannot, but we can prove them modulo up-closure, eg \begin{align} % \swap\uc \oo \map\s\ (\map\s\ f) & = \ucl \oo \map\s\ (\map\s\ f) \oo \swap\uc % \label{S1'} \tag*{S(1)$'$} \\[-0.5ex] \swap\uc\ {A} & = \ucl\ (\map\s\ \unit\s\ A) \label{S2'} \tag*{S(2)$'$} \\[-0.5ex] \swap\uc\ (\map\s\ \unit\s\ A) & = \ucl\ {A} \label{S3'} \tag*{S(3)$'$} % \\[-0.5ex] % \prodd\uc \oo \map\s\ \dorp\uc\ & = \dorp\uc \oo \prodd\uc \tag*{S(4)} % \\ % \swap\uc \oo \map\s\ \join\s & = \dorp\uc \oo \swap\uc \tag*{(D3)} \\[-0.5ex] % \swap\uc \oo \join\s & = \prodd\uc \oo \map\s\ \swap\uc \tag*{(D4)} \end{align} \item proofs of the monad axioms for $\set\ \set\ \alpha$ \\ (again, some equalities only modulo up-closure) \\ difficult, but imitated usual proofs from S(1) to S(4) \item defined type $\ucss\ \alpha$ : \emph{up-closed} sets of sets \\ (ie, a representative of each equivalence class) \item defined the monad functions for the $\ucss\ \alpha$ type \item translated results about $\set\ \set\ \alpha$ to $\ucss\ \alpha$: it is a monad! \end{itemize} } \frame { \frametitle{The Chorus Angelorum Monad} \framesubtitle{Link to Continuation Monad} First, recall functions used by Jones \& Duponcheel \begin{align*} \join & : M\ N\ M\ N\ \alpha \to M\ N\ \alpha & \prodd & : N\ M\ N\ \alpha \to M\ N\ \alpha \\[-0.5ex] \dorp & : M\ N\ M\ \alpha \to M\ N\ \alpha & \swap & : N\ M\ \alpha \to M\ N\ \alpha \end{align*} Think of $M$ ($N$) as a set from which angel (demon) chooses. \\[1ex] ``evaluation function'' $\evaluc : \set\ \set\ \alpha \to (\alpha \to \bool) \to \bool$, \\[1ex] $\evaluc\ \As\ P$ tells whether the post-condition $P$ is satisfied when angel and demon have made their choices from \As. \\[1ex] $\evaluc\ \Bs\ P \equiv \exists B \in \Bs.\ \forall b \in B.\ P\ b$. \\[1ex] $(\alpha \to \bool) \to \bool$ is type of \alert{continuation} monad $K\ \alpha$ \\[1ex] \Ball\ and \Bex : $\set\ \alpha \to (\alpha \to \bool) \to \bool$, ie : $\set\ \alpha \to K\ \alpha$ \\ express quantification over a given set: $\Ball\ S\ P \equiv \forall s \in S.\ P\ s$ } \frame { \frametitle{The Chorus Angelorum Monad} \framesubtitle{Link to Continuation Monad -- ctd} \begin{align*} \evaluc & = \Ball \odot_K \Bex \\ \evaluc \oo \swap\uc & = \Bex \odot_K \Ball \end{align*} Using obvious isomorphism $K\ \alpha \to \set\ \set\ \alpha$, called \ktoss: \begin{align*} \join\uc & = \ktoss \oo (\Ball \odot_K \Bex \odot_K \Ball \odot_K \Bex) \\[-0.5ex] \dorp\uc & = \ktoss \oo (\Bex \odot_K \Ball \odot_K \Bex) \\[-0.5ex] \prodd\uc & = \ktoss \oo (\Ball \odot_K \Bex \odot_K \Ball) \\[-0.5ex] \swap\uc & = \ktoss \oo (\Bex \odot_K \Ball) \\[-0.5ex] \ext\uc\ f & = \ktoss \oo (\Ball \odot_K (\Bex \oo f) \odot_K \Ball \odot_K \Bex) \\[-0.5ex] \pext\uc\ f & = \ktoss \oo (\Ball \odot_K (\Bex \oo f) \odot_K \Ball) % \\ f \odot_{uc} g & = \ktoss \oo ((\evaluc \oo f) \odot_K (\evaluc \oo g)) \end{align*} } \subsection{Definition of Choice} \label{s-defs} \comment% \frame { \frametitle{Definition of the choice command} 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} } \frame { \frametitle{Angelic and Demonic Choice} We defined these as follows (simplified by \\ \begin{itemize} \item omitting conversion between the $\set\ \set\ \alpha$ and $\ucss\ \alpha$ types \item assuming up-closed families of sets) \end{itemize} \begin{align*} \dem\ \Bs\ s & = \textstyle \bigcap\ \{B\ s\ |\ B \in \Bs\} \\ \ang\ \Bs\ s & = \textstyle \bigcup\ \{B\ s\ |\ B \in \Bs\} \end{align*} giving these results (which would normally be the definitions) \begin{align*} [\dem\ \Bs]\ Q\ s & = \forall B \in \Bs.\ [B]\ Q\ s \\ [\ang\ \Bs]\ Q\ s & = \exists B \in \Bs.\ [B]\ Q\ s \\[1ex] \end{align*} } \end{document} \comment{ \section{Conclusion} \frame { \frametitle{The End} The End } } \frame { \frametitle{Examples of beamer use} \begin{block}{title} block \end{block} \begin{itemize} \item<1-2> Normal LaTeX class. \item<3-4> \emph{Easy} \alert{overlays}. \item<2-3> No external programs needed. \end{itemize} \color<2-3>{green} green \color<1-2>{blue} blue }