%% %% \documentclass{sigplanconf} \usepackage{icfp2007} % requires current version of natbib \usepackage{natbib} \bibpunct();A{}, \let\cite=\citep % \documentclass{llncs} %\documentclass[a4paper,11pt]{article} %\usepackage{makeidx} %\usepackage{acmnew-xref} % \usepackage[scrtime]{prelim2e} \usepackage{latexsym} \usepackage{amsmath} \usepackage{amssymb} % \usepackage{exptrees} \usepackage{url} %\RequirePackage{mathptm} %\RequirePackage{times} %\RequirePackage{palatino} \renewcommand{\today}{\number\day\ \ifcase\month\or January\or February\or March\or April\or May\or June\or July\or August\or September\or October\or November\or December\fi \ \number\year} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% Preamble \newcommand\cfile{} \newcommand\comment[1]{} % \newcommand\cc[1]{} % for label names \newcommand\cc[1]{#1} % for label names % \renewcommand\footnote[1]{} % for footnotes % \pagestyle{myheadings} \renewcommand\theenumi{(\alph{enumi})} \renewcommand\labelenumi{\theenumi} \renewcommand\theenumii{(\roman{enumii})} \renewcommand\labelenumii{\theenumii} \newcommand\page[1]{page~\pageref{#1}} \newcommand\fig[1]{Fig.~\ref{fig:#1}} \newcommand\ch[1]{Chapter~\ref{ch:#1}} \newcommand\tbl[1]{Table~\ref{tbl:#1}} \newcommand\thrm[1]{Theorem~\ref{thrm:#1}} \newcommand\lem[1]{Lemma~\ref{lem:#1}} \newcommand\up[1]{\vspace{-#1ex}} \newcommand\vpf{\vspace{-3ex}} % to reduce space before proof tree \def\dem{\mathop{\rm dem}} \def\ang{\mathop{\rm ang}} \newcommand\set{\textit{set}} \newcommand\state{\textit{state}} \newcommand\outcome{\textit{outcome}} \newcommand\tcres{\textit{tcres}} \newcommand\swapi{\textit{swapi}} \newcommand\infch{\textit{infch}} \newcommand\infchs{\textit{infchs}} \newcommand\icnt{\textit{icnt}} \newcommand\reachnt{\textit{reach\_NT}} \newcommand\TorN{\texttt{TorN}} \newcommand\Term{\texttt{Term}} \newcommand\ssos{\texttt{sts\_of\_ocs}} \newcommand\NonTerm{\texttt{NonTerm}} \newcommand\KM{$\mathcal{K}(M)$} \newcommand\KNM{$\mathcal{K}(MN)$} \newcommand\val{\textit{value}} \newcommand\name{\textit{name}} \newcommand\choice{\textit{choice}} \newcommand\Cs{\ensuremath{\mathcal{C}}} \newcommand\Bs{\ensuremath{\mathcal{B}}} \newcommand\As{\ensuremath{\mathcal{A}}} \newcommand\Ss{\ensuremath{\mathcal{S}}} \newcommand\Ts{\ensuremath{\mathcal{T}}} \newcommand\spom{\textit{spom}} \newcommand\wpom{\textit{wpom}} \newcommand\wlp{\textit{wlp}} \newcommand\slp{\textit{slp}} \renewcommand\wp{\textit{wp}} \renewcommand\sp{\textit{sp}} \newcommand\trm{\textit{trm}} \newcommand\fis{\textit{fis}} \newcommand\bool{\textit{bool}} \newcommand\nat{\textit{nat}} \newcommand\aexp{\textit{exp}} \newcommand\bexp{\textit{bexp}} \newcommand\seq{\textit{seq}} \newcommand\skp{\textit{skip}} \newcommand\magic{\textit{magic}} \newcommand\abort{\textit{abort}} \newcommand\pcaux{\textit{pc\_aux}} \newcommand\while{\textit{while}} \newcommand\iif{\textit{if}} \newcommand\els{\textit{else}} \newcommand\then{\textit{then}} \newcommand\eend{\textit{end}} \newcommand\ddo{\textit{do}} \newcommand\prd{\textit{prd}} \newcommand\fram{\textit{frame}} \newcommand\frm{\textit{frame}} \newcommand\rep{\textit{rep}} \newcommand\repall{\textit{repall}} \newcommand\setvars{\textit{setvars}} \newcommand\chst{\textit{chst}} \newcommand\tc{\textit{\_tc}} \newcommand\uc{\textit{\_uc}} \newcommand\gc{\textit{\_gc}} \newcommand\s{\textit{\_s}} \newcommand\nt{\textit{\_nt}} \newcommand\lub{\textit{lub}} \newcommand\ucl{\textit{up\_cl}} \newcommand\uca{\textit{uca}} \newcommand\evaluc{\textit{eval\_uc}} \newcommand\ktoss{\textit{K\_to\_SS}} \newcommand\mon{\textit{mono}} \newcommand\Ball{\textit{Ball}} \newcommand\Bex{\textit{Bex}} \newcommand\ucAbs{\textit{uc\_Abs}} \newcommand\tctoch{\textit{tc\_to\_ch}} \newcommand\Abs{\textit{Abs}} \newcommand\Rep{\textit{Rep}} \newcommand\pext{\textit{pext}} \newcommand\prodd{\textit{prod}} \newcommand\dorp{\textit{dorp}} \newcommand\swap{\textit{swap}} \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\M{\ensuremath{_M}} \newcommand\NM{\ensuremath{_{MN}}} \newcommand\unitM{\ensuremath{\unit_{M}}} \newcommand\extM{\ensuremath{\ext_M}} \newcommand\mapM{\ensuremath{\map_M}} \newcommand\joinM{\ensuremath{\join_M}} \newcommand\oM{\ensuremath{\odot_M}} \newcommand\N{\ensuremath{_N}} \newcommand\extN{\ensuremath{\ext_N}} \newcommand\mapN{\ensuremath{\map_N}} \newcommand\unitN{\ensuremath{\unit_N}} \newcommand\joinN{\ensuremath{\join_N}} \newcommand\oN{\ensuremath{\odot_N}} % type constructors first in the following now \newcommand\extNM{\ensuremath{\ext_{MN}}} \newcommand\unitNM{\ensuremath{\unit_{MN}}} \newcommand\mapNM{\ensuremath{\map_{MN}}} \newcommand\joinNM{\ensuremath{\join_{MN}}} \newcommand\oNM{\ensuremath{\odot_{MN}}} \newcommand\extfun{\textit{ext-funct}} \newcommand\extlu{\textit{ext-L-unit}} \newcommand\extru{\textit{ext-R-unit}} \newcommand\pextlu{\textit{pext-L-unit}} \newcommand\pextru{\textit{pext-R-unit}} \newcommand\pextfun{\textit{pext-funct}} \newcommand\pextomap{\textit{pextomap}} \newcommand\pextpm{\textit{pext-pm}} \newcommand\omext{\textit{\om -ext}} \newcommand\extom{\textit{ext-\om}} \newcommand\mapext{\textit{map-ext}} \newcommand\joinext{\textit{join-ext}} % \newcommand\ompext{\textit{\om -pext}} % \newcommand\bindext{\textit{bind-ext}} % \newcommand\pextext{\textit{pext-ext}} \newcommand\extjm{\textit{ext-jm}} \setcounter{secnumdepth}2 \setcounter{tocdepth}2 \newtheorem{condition}{Condition} % automatically defined in LLNCS style \newtheorem{thm}{Theorem}%[chapter] \newtheorem{theorem}{Theorem}%[chapter] \newtheorem{lemma}[thm]{Lemma} \newtheorem{defn}[thm]{Definition} \newtheorem{definition}[thm]{Definition} \newtheorem{cor}{Corollary}[thm] \renewcommand\thecor{\thethm(\arabic{cor})} \begin{document} \conferenceinfo{PLPV'07,} {October 5, 2007, Freiburg, Germany.} \CopyrightYear{2007} \copyrightdata{978-1-59593-677-6/07/0010} \titlebanner{Compound Monads in Specification Languages} % These are ignored unless \preprintfooter{Compound Monads in Specification Languages} % 'preprint' option specified. \title{Compound Monads in Specification Languages} % \subtitle{Subtitle Text, if any} \authorinfo{Jeremy E.\ Dawson} {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/}} \maketitle \begin{abstract} We consider the language of ``extended subsitutions'' involving both angelic and demonic choice. For other related languages expressing program semantics the implicit model of computation is based on a combination of monads by a distributive law. We show how the model of computation underlying extended subsitutions is based on a monad which, while not being a compound monad, has strong similarities to a compound monad based on a distributive law. We discuss these compound monads and monad morphisms between them. We have used the theorem prover Isabelle to formalise and machine-check our results. \end{abstract} \category{F.3.1}{LOGICS AND MEANINGS OF PROGRAMS} {Specifying and Verifying and Reasoning about Programs} [Logics of programs, Pre- and post-conditions] \category{D.2.1}{SOFTWARE ENGINEERING} {Requirements/Specifications}[Languages] \terms Languages, Theory, Verification \keywords specification languages, extended substitutions, compound monads, distributive law for monads, generalised substitutions, demonic choice, angelic choice \comment{ in llncs \pagestyle{plain} \begin{document} %% Here begins the main text \title{Compound Monads and Models of Computation} \author{ Jeremy E.\ Dawson\inst{1}\inst{2}} \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/} } \date{\today} %% Title \maketitle \begin{abstract} We consider the theory of ``extended subsitutions'' involving both angelic and demonic choice. For other related formal theories describing program semantics the implicit model of computation is based on a combination of monads by a distributive law. We show how the model of computation underlying extended subsitutions is based on a monad which, while not being a compound monad, has strong similarities to a compound monad based on a distributive law. We discuss these compound monads and monad morphisms between them. We have used the theorem prover Isabelle to formalise and machine-check our results. \\ {\bf Keywords}: extended substitutions, compound monads, distributive law for monads, generalised substitution, demonic choice, angelic choice \end{abstract} end of llncs version portion } \section{Introduction} \label{s-id} In several papers Dunne has proposed specification languages for analysing (variously named) ``computations'', given rules for combining these computations in various ways, and stated and proved results about them. These languages contain some constructs similar to those found in Dijkstra's guarded command language \cite{dijkstra-gcl}. Underlying each of these languages, whether explicitly or implicitly, is a notion of what a computation is, and for some of these % (see \cite{dawson-fgc} and \cite{dawson-fgs}) we have used the Isabelle theorem prover to define Dunne's various operations in terms of the identified underlying notion of computation, and have proved that defining the operations in this way implies the definitions and results given by Dunne. In this work we used the fact that a compound monad underlies the model of computation involved. % In \cite{dunne-abstr-cmds} Dunne \citet{dunne-abstr-cmds} gave an account of general correctness % (Jacob \& Gries \cite{JG}), \cite{JG}, which combines the concepts of partial correctness and total correctness, arguing for its utility in analysing the behaviour of programs. Calling the computations ``abstract commands'', he gave several basic abstract commands and operators for joining them, for which he gave rules in terms of weakest liberal preconditions and termination conditions, and many results about these operators. In \cite{dawson-fgc} we described an operational interpretation of abstract commands equivalent to that of % Jacob \& Gries \cite{JG}, \citet{JG}, which used the construction of % Plotkin \cite{plotkin-powerdomain}. \citet{plotkin-powerdomain}. % We used the automated theorem proving system Isabelle to prove that % this operational interpretation implies the rules and results given by Dunne. % we considered this abstract command language % and described the operational interpretation of the abstract commands. % Similarly, in \cite{dunne-gen-subs}, Dunne Similarly, \citet{dunne-gen-subs} considered the generalised substitutions used in the B~method, which is based on total correctness. In \cite{dawson-fgs} we formalised the theory he gave, and the operational model underlying it, using a similar approach to, and in some cases the results of, \cite{dawson-fgc}. We compared this operational model with that of the theory of % We compared this operational model with that underlying the theory of general correctness. % and of that of abstract commands, and the compound monads involved in % them. % We discussed the difference between the operational models of this theory % and of that of abstract commands, and the compound monads involved in % them. % In \cite{dunne-abstr-cmds} % Dunne argued that general correctness provides a better framework for % program refinement than either total or partial correctness, and % its relative simplicity is supported by the results at the end of % \cite[\S 3.2]{dawson-fgc}. % However the theory of generalised substitutions is based on total correctness, % so that when two generalised substitutions with the same frame are % equivalent in total correctness, they are regarded as the same, % although they may not be equivalent in terms of general correctness. % So we need to model program (statements) in such a way that % two such generalised substitutions are equal. For both general correctness and total correctness we used the Isabelle/HOL theorem prover to define an operational model and prove that it implied the rules and results given by Dunne. In both cases the operational model is based on a compound monad and in both cases this compound monad can be explained (\emph{inter alia}) in terms of a distributive law for combining two monads \cite[\S 9.2]{bwttt}. % We used the automated theorem proving system Isabelle to prove that % the operational interpretation implies the rules given by Dunne. Semantic models combining angelic and demonic non-determinism have been developed by % Back and von Wright \cite{back-vw}, \citet{back-vw}, % and Rewitzky \cite{rewitzky-03}, and \citet{rewitzky-03}, who described a model using binary multirelations, which is developed further in \cite{mcr}, for computations involving angelic and demonic non-determinism. In \cite{back-vw} and \cite{mcr} these computations are described in terms of a game between the angel and the demon, where the angel and the demon make ``moves'' to try to ensure that the postconditon is or is not satisfied. Recently, % in \cite{dunne-chorus} Dunne \citet{dunne-chorus} defined an ``extended substitution'' language, which encompasses the generalised substitutions, allowing for angelic choice as well as demonic choice, ie, choices which will be made to ensure, if possible, that the postcondition is, or is not, satisfied. As explained in \S\ref{s-monads} we would expect to see a monad underlying the model of computation for this language. % He described the model for these in terms of ``up-closed binary % multirelations''. In this paper we show how the operational model we use (equivalent to the multirelation model) for this language is in fact based on a monad. We found that while it is not a compound monad, it can be described using the concepts and results about joining two monads by a distributive law. Indeed, in proving that it is a monad, we were helped significantly by copying and adapting the proofs of results relating to compound monads based on a distributive law. In this paper we describe this construction after surveying the role of compound monads based on distributive laws in the operational models for general and total correctness. % In this paper therefore we focus on the monads % involved in each of these operational models. In \S\ref{s-om} we discuss the operational models underlying each of these theories. In \S\ref{s-monmod} we briefly introduce monads, and compound monads. We then show how the theories of general correctness and total correctness are each based on a compound monad which is based on a distributive law, and that one of these distributive laws is also a monad morphism between these two monads. In \S\ref{s-chmon} we describe the construction of the monad underlying the extended substitutions. This is not actually a compound monad but it is based on equivalence classes of a structure rather like a compound monad, and we describe how we used the results on combining two monads by a distributive law to show that this construction gives a compound monad. We use the interactive theorem prover Isabelle/HOL. Isabelle is a framework based on intuitionistic typed higher-order logic, on which a variety of object logics can be built. We use the HOL (``higher-order logic'') object logic, which is a classical strongly typed higher-order logic, giving an object language which has strong similarities to the functional programming languages Standard ML and Haskell. In the logic, functions are total, function equality is defined extensionally, and functions are not necessarily computable. All results referred to in this paper have been proved using Isabelle. % the theorem prover Isabelle. % Again, we find a monad underlying this model: in this case it is based % on equivalence classes of a structure which is rather like, but is not, % a compound monad. \section{The Operational Models} \label{s-om} We describe the operational models. Firstly, we make a caveat concerning the role of frames. In each case Dunne's definition of a computation involves a \emph{frame}, which, loosely, is the set of variables which ``might'' be affected. In this paper we ignore frames (equivalently, we assume the frame to be the set of all variables in the machine state). In fact this enables us to treat the machine state entirely as an abstract type. In each case, a computation is modelled by a function from the state type to a result type, which is different for each model. Having described the operational model, we showed in each case that two computations are refinement-equivalent (as defined by Dunne, but ignoring frames) if and only if they correspond to the same function in the operational model. \comment{ FRAME STUFF Note, however, that $\frm (x := x) = \{x\}$. Also, from any command a new command may be defined which has an enlarged frame but is otherwise the same. Thus, clearly, we cannot deduce the frame of a computation from its behaviour. So, in our proofs, we ignored frames, and when we proved that two computations are equal, this would mean that they have the same behaviour but not necessarily the same frame. For example we would say that the computations \skp\ and $x := x$ are equal because they behave the same way, although they have different frames. In certain cases, the definition of operations which combine commands involved the frames of the individual commands (thus the \emph{behaviour} of $A || B$ depends on the \emph{frames} of $A$ and of $B$). In fact, much of our work treated the machine state as abstract, rather than as a function from variable names to values, and of course this requires ignoring frames as we do. % We describe these models without reference to frames. % Furthermore, where we state that we have proved a result of Dunne % \cite{dunne-gen-subs}, this will usually mean that we have proved the result % as modified by deleting reference to the frames of the substitutions. } \subsection{The General Correctness Operational Model} \label{s-gcom} Firstly, we describe the operational model of \cite{dawson-fgc}, used to describe ``abstract commands'' and general correctness. % In \cite{JG} Jacobs \& Gries \citet{JG} (see also \cite{dunne-abstr-cmds}) explain how, in the case of a non-deterministic computation, weakest preconditions and total correctness do not distinguish a computation which simply fails to terminate from one which (on a given input) may terminate in a particular final state or may fail to terminate. On the other hand, weakest liberal preconditions and partial correctness fail to distinguish a computation which terminates in a given final state from one which may do that or may fail to terminate. Accordingly, they develop the theory of general correctness, which does distinguish each of these pairs of computations, and in which refinement (as defined in \cite{dunne-abstr-cmds}) means partial correctness refinement \emph{and} total correctness refinement. The computational model that we use underlying this theory is the following, suggested by \citet{JG}: each computation (on a given initial state) results in (one of) a set of \emph{outcomes}, where each outcome is either non-termination, or termination in a particular final state. Then we proved that two abstract commands are equivalent in general correctness refinement if and only if they are the same function in this model, from states to sets of outcomes. So we let an outcome be either the tag \NonTerm, indicating non-termination, or \Term\ $s$, indicating termination in the state $s$, as expressed in Isabelle by % To express this we declare the Isabelle datatype \begin{center} \tt datatype $\sigma$ TorN = NonTerm | Term $\sigma$ \end{center} where $\sigma$ is a type variable, and, in Isabelle, a type constructor follows its argument. This means that a value of the type $\sigma$ \TorN\ is either the tag \NonTerm\ or a member of the type $\sigma$, tagged with the tag \Term. % (Following the Isabelle convention, we write a type constructor % such as \TorN\ or \set\ after its type argument). But we will generally write a type constructor such as \TorN\ or \set\ \emph{before} its type argument. % Thus the type \outcome\ is \state\ \TorN, Thus the type \outcome\ is \TorN\ \state, and the type of computations in this model is % $\state \to \state\ \TorN\ \set$. $\state \to \set\ (\TorN\ \state)$. Thus a computation which (from a given initial state) can terminate in either state $s_1$ or $s_2$ is represented by the outcome set $\{\Term\ s_1, \Term\ s_2\}$; if the computation can also fail to terminate, it is represented by $\{\Term\ s_1, \Term\ s_2, \NonTerm\}$. % To express that a command can either terminate in a new state or % fail to terminate, % in \cite{dawson-fgc} we considered command \emph{outcomes}, % where an outcome is either termination in a new state or non-termination. % Then we model a command as a function, % of type $\state \to \outcome\ \set$, from states to sets of outcomes. % This model can distinguish between a command which % (when executed in a particular given state) % must fail to terminate from one which may or may not fail to terminate. % Since Dunne's treatment of \emph{abstract commands} \cite{dunne-abstr-cmds} % distinguished between two such commands, % this model was effective in considering {abstract commands}. % However a theory of total correctness, using weakest preconditions, % does not distinguish between two such commands. \subsection{The Total Correctness Operational Model} \label{s-tcom} Subsequently, % in \cite{dunne-gen-subs}, Dunne \citet{dunne-gen-subs} described generalised substitutions, based on the B~method, in which only total correctness is of interest. So we want to consider computations equal if they are equivalent in total correctness refinement: we do not want to distinguish a computation which may terminate or not (on a particular initial state) from one which will not terminate. So here the model of computation we want is that a computation is a function which, given an initial state, returns either possible non-termination, or guaranteed termination, in (one of) a set of final states. We then define the type \tcres\ (``total correctness result'') % to be \state\ \set\ \TorN, to be \TorN\ (\set\ \state), that is, either \NonTerm, meaning possible non-termination, or \Term\ $S$, termination in (one of) a set $S$ of states. So we define the weakest precondition function $[C]$, where $[C]\ Q\ s$ is the condition that command $C$, when executed in state $s$, \emph{will} terminate in a state satisfying the predicate $Q$. \begin{align*} [C]\ Q\ s & \equiv (\exists S.\ (\forall x \in S.\ Q\ x) \land (C\ s = \Term\ S)) \end{align*} Then we define the total correctness refinement relation $\sqsubseteq_{tc}$ accordingly, where $[A]\ Q \longrightarrow [B]\ Q$ is an abbreviation for $\forall s.\ [A]\ Q\ s \Rightarrow [B]\ Q\ s$. \begin{align*} A \sqsubseteq_{tc} B & \equiv (\forall Q.\ [A]\ Q \longrightarrow [B]\ Q) \end{align*} This definition of refinement $\sqsubseteq_{tc}$ is as in \cite[\S 7]{dunne-gen-subs}, but ignoring frames. Then we proved that two generalised substitutions are equivalent in total correctness refinement % (that is, the refinement as defined in \cite[\S 7]{dunne-gen-subs}, % but ignoring the frames), that is, they have the same weakest precondition function, if and only if they are the same when considered as functions in this computational model. Equivalently, the weakest precondition function is injective, that is, if $[C]\ Q = [C']\ Q$, then $C = C'$. In this model the two computations mentioned at the end of \S\ref{s-gcom} are represented by the results $\Term \{s_1, s_2\}$ and \NonTerm. For the second of these, the representation \NonTerm\ reflects the fact that, in total correctness, the computation is indistinguishable from one which must fail to terminate: they both fail to satisfy any postcondition. \subsection{The Chorus Angelorum Operational Model} \label{s-chom} % In \cite{dunne-chorus}, Dunne \citet{dunne-chorus} notes that conventional program analysis involves demonic choice: we want a non-deterministic program to satisfy its postcondition, regardless of what choice the demon (who is trying to ensure that the postcondition is not satisfied) makes. % First he dualises this, so that the choices are made by an angel (who aims % to see the postcondition satisfied). His framework of computations called ``extended substitutions'' involving both demonic and angelic choice, is based on the underlying computational model of % Rewitzky \cite{rewitzky-03} \citet{rewitzky-03} which is expressed in terms of up-closed binary multirelations. We describe this in an equivalent way: a computation is a function which, given an initial state, returns a set \Ss\ of sets of final states. The meaning of this is that the angel will choose one, $S \in \Ss$, of these sets, and the demon will choose one final state $s$ from that chosen set $S$. We define the weakest precondition function accordingly: $$ [C]\ Q\ s \equiv (\exists U \in C s.\ (\forall u \in U.\ Q\ u))$$ This reflects that the angel tries to make a choice $U$ which defeats the demon, who in turn tries to make a choice $u$ from $U$ which fails the postcondition $Q$. % But considering a result $\Ss : \state\ \set\ \set$, But considering a result $\Ss : \set\ \set\ \state$, if $S' \supseteq S$ for $S',S \in \mathcal S$, then the angel could always choose $S$ rather than $S'$ to limit the demon's choice. So it is enough to consider only results \Ss\ which, as sets of sets, are ``up-closed'', that is, where, if $S' \supseteq S$ and $S \in \Ss$ then $S' \in \Ss$; under this restriction we then find that two extended substitions which are refinement-equivalent (ie, have the same weakest precondition function) are represented by the same function in this computational model. \section{The Monads used in these Models} \label{s-monmod} \subsection{Monads} \label{s-monads} As discovered by % Moggi \cite{moggi-monads}, \citet{moggi-monads}, monads (long known in category theory) are useful for representing the structure of a computation. To define a monad $M$, we need to define the unit and extension functions \unit\ and \ext, of the types shown, and show that they satisfy the following rules required for a monad, where $M$ is a type constructor, eg, \set\ or \TorN. \begin{align*} \unit &: \alpha \to M \alpha \\[-0.5ex] \ext &: (\alpha \to M \beta) \to (M \alpha \to M \beta) \end{align*} \begin{align} \label{E1} \ext\ f \oo \unit & = f \\[-0.5ex] \label{E2} \ext\ \unit & = \id \\[-0.5ex] \label{E3'} \ext\ (\ext\ g \oo f) & = \ext\ g \oo ext\ f \end{align} % % As a standard result (see \cite{Wadler-essence}), % a monad can be characterised either by the three % functions \unit, \map\ and \join, and seven rules involving these % functions, % or the functions \unit\ and \ext\ and the three rules shown above. We define $B \om A = \ext\ B \oo A$, and this represents $(A\,;B)$, the sequencing of computations $B$ and $A$, since $\ext\ B$ models the action of computation $B$ on the result of a previous computation. The unit function models the computation which does nothing (\skp). So then rules \eqref{E1} to \eqref{E3'} give us the properties \eqref{krid} to \eqref{kass}. We would expect these properties to hold in a model of computation, since they say that the sequencing operation is associative, and that the \skp\ computation is its identity. These properties show that we have a category, in which the objects are types, an arrow from $\alpha$ to $\beta$ is a function of type $\alpha \to M \beta$, the identity arrow for object $\alpha$ is the function $\unit : \alpha \to M \alpha$ and composition is given by \om. This category is 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 basic category of types and functions. \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} Two well-known examples of monads used in this paper are the ``non-termination'' monad (known under various names such as ``error monad'' or ``exception monad''), and the set monad. In each case the unit function turns a simple state into the form of a computation result, and the extension function turns a computation acting on a simple initial state into a computation acting on the result of a previous computation. Also associated with each monad are functions \map\ and \join\ of the types shown, and in fact a monad can alternatively be characterised by seven rules involving the functions \unit, \map\ and \join\ (see \cite{Wadler-essence}). % We will also use the \map\ function which applies a transformation to % each item of the simple type involved in a given value of the monadic type. \begin{align*} \join &: M M \alpha \to M \alpha \\[-0.5ex] \map &: (\alpha \to \beta) \to (M \alpha \to M \beta) \\ \ext\ f &= \join \oo \map\ f \end{align*} The non-termination monad has unit, map, join and extension functions: % where $\ext\nt$ is the extension function of the $\TorN$ monad \begin{align*} \unit\nt\ s & = \Term\ s \\ \map\nt\ f\ \NonTerm & = \NonTerm \\[-0.5ex] \map\nt\ f\ (\Term\ s) & = \Term\ (f\ s) \\ \join\nt\ (\Term\ \NonTerm) & = \join\nt\ \NonTerm = \NonTerm \\[-0.5ex] \join\nt\ (\Term\ (\Term\ f)) & = \Term\ f \\ \ext\nt\ f\ \NonTerm & = \NonTerm \\[-0.5ex] \ext\nt\ f\ (\Term\ s) & = f\ s \end{align*} The set monad has unit, map, join and extension functions \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*} Thus the non-termination monad gives a model where a computation either terminates in a new state, or fails to terminate, and the set monad models non-deterministic (but necessarily terminating) computations. \subsection{Compound Monads} \label{s-cms} Given that each of the type constructors $M$ and $N$, with their unit and extension functions, is a monad, it does not follow, however, that $M N \alpha$ (relative to $\alpha$) is a monad. Yet, in \S\ref{s-gcom} and \S\ref{s-tcom}, we have found such combination of type constructors arise naturally in modelling programs. There are several seemingly distinct approaches to constructing a monad out of two simpler monads; see for example \cite[\S 7.3]{lhj}, \cite{hpp-sum-tensor}. In some cases, several of these constructions may be applicable. This point is discussed further in \S\ref{s-concl}. We use our results in \cite{dawson-cmkc}, which develop those of % Jones \& Duponcheel \cite{jd-cm}, \citet{jd-cm}, and are closely related to the distributive law of % Barr \& Wells \cite[\S 9.2]{bwttt}. \citet[\S 9.2]{bwttt}. We describe how those results show that the non-termination monad and the set monad can be composed in both ways, ie, $\set\ (\TorN\ \alpha)$ and $\TorN\ (\set\ \alpha)$ to form compound monads. As in \cite{jd-cm}, we consider the composition of two monads $M$ and $N$, % but as in Isabelle, we write a type constructor after the type, so the compound monadic type is $M N \alpha$. We write \extNM, \extM\ and \extN\ for the extension functions of $MN$, $M$\ and $N$, etc. % respectively. To define the compound monad, we need the function \extNM, which ``extends'' a function $f$ from a ``smaller'' domain, $\alpha$, to a ``larger'' one, $M N \alpha$. So we use a ``partial extension'' function which does part of this job: \begin{align*} \extNM &: (\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*} The following rules and definitions are sufficient to define a compound monad using such a function \pext. 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. (In fact, \unitNM\ and \pext\ are the unit and extension functions of a monad \emph{in} the category \KM, whose Kleisli category is also \KNM, see \cite{dawson-cmkc}). % and we also show the definition of \unitNM\ and \extNM\ % for the compound monad in terms of \pext. % \begin{align} \label{E1K'} \pext\ f \oo \unitN & = f \\[-0.5ex] \label{E2K} \pext\ \unitNM & = \unitM \\[-0.5ex] \label{E3'K_o} \pext\ (\extNM\ g \oo f) & = \extNM\ g \oo pext\ f \\ \label{E3K} \pext\ (g \oNM f) & = \pext\ g \oM pext\ f \\ \label{EC} \extNM\ g & = \extM\ (\pext\ g) \\[-0.5ex] \label{UC} \unitNM & = \unitM \oo \unitN \end{align} % \subsubsection{Relation to distributive laws and compatible monads} Here we briefly outline the relationships between our sufficient conditions for compound monads and other work in the literature. % Jones \& Duponcheel \cite{jd-cm} \citet{jd-cm} give two conditions, J(1) and J(2), which compound monads may satisfy. Under the reasonable assumptions that $\unitNM = \unitM \oo \unitN$ and $\mapNM = \mapM \oo \mapN$, the compound monads that arise from a function \pext\ are those that satisfy J(1). Jones \& Duponcheel use a function \textit{prod}, % where $\prodd = \pext\ \id$ and $\pext\ f = \prodd\ \oo \mapN\ f$, where $\pext\ f = \prodd\ \oo \mapN\ f$, % and $\prodd = \pext\ \id$, and give conditions for defining a compound monad using \textit{prod}. The following are equivalent to J(1) and J(2) respectively. \begin{align} \extM\ \joinNM & = \joinNM \oo \joinM \label{J1} \tag*{J(1)$'$} \\ \extNM\ (\mapM\ \joinN) & = \mapM\ \joinN \oo \joinNM \label{J2} \tag*{J(2)$'$} \end{align} The compound monads that satisfy both J(1) and J(2) are those which arise from a function $\swap : N M \alpha \to M N \alpha$ satisfying conditions S(1) to S(4) of \cite{jd-cm}, shown below. % from a ``distributive law'', that is, a natural transformation, % which in the present context is a polymorphic function % $\lambda : N M \alpha \to M N \alpha$ satisfying S(1) below; % see Barr \& Wells \cite[\S 9.2]{bwttt}. % Compound monads do not necessarily arise from a distributive law, Compound monads do not necessarily arise from such a function \swap, or from a function \pext\ as above, though it seems that in most cases they do so. If so, $\swap = \pext\ (\mapM\ \unitN)$. Conditions S(1) to S(4) of \cite{jd-cm}, shown below, on a function $\swap : N M \alpha \to M N \alpha$ are necessary and sufficient to define a compound monad in terms of \swap. The statement of S(4) uses two further functions \prodd\ and \dorp\ defined in terms of \swap. \begin{align*} \prodd & : N\ M\ N\ \alpha \to M\ N\ \alpha \\[-0.5ex] \dorp & : M\ N\ M\ \alpha \to M\ N\ \alpha \\ \prodd & = \mapM\ \joinN \oo \swap \\[-0.5ex] \dorp & = \extM\ \swap \\ \swap \oo \mapN\ (\mapM\ f) & = \mapNM\ f \oo \swap\ \tag*{S(1)} \\[-0.5ex] \swap \oo \unitN & = \mapM\ \unitN \tag*{S(2)} \\[-0.5ex] \swap \oo \mapN\ \unitM & = \unitM \tag*{S(3)} \\[-0.5ex] \prodd \oo \mapN\ \dorp & = \dorp \oo \prodd \tag*{S(4)} \end{align*} In fact the function \swap\ of \cite{jd-cm} is the distributive law $\lambda$ of \cite[\S 9.2]{bwttt}. In this paper we use the terminology and results % of Jones \& Duponcheel \cite{jd-cm} of \citet{jd-cm} rather than the text \cite{bwttt} because \citet{jd-cm} also describe \prodd\ and \dorp, which we use. We now relate \cite{jd-cm} to \cite[\S 9.2]{bwttt}, but this is not used in the remainder of this paper. We have shown in \cite{dawson-cmkc} that conditions J(1) and J(2) match conditions (C1) to (C5) of \cite[\S 9.2]{bwttt}, for compatibility of monads $N$, $M$ and $MN$. These are the conditions on a compound monad which are necessary and sufficient for it to be definable by a distributive law, that is, by a \swap\ function. % Of the conditions (C1) to (C5) for compatibility of \cite[\S 9.2]{bwttt}, Conditions (C2) and (C5) (which are in fact equivalent) are equivalent to J(2) of \cite{jd-cm}, and conditions (C3) and (C4) (which are also equivalent) are equivalent to J(1) of \cite{jd-cm}. Finally, condition (C1) % of \cite[\S 9.2]{bwttt} is \eqref{UC} above. We have also shown in \cite{dawson-cmkc} that conditions S(1) to S(4) correspond to conditions (D1) to (D4) of \cite[\S 9.2]{bwttt} defining a distributive law. S(1) simply says that \swap\ is a natural transformation, S(2) and S(3) are (D2) and (D1), and, in the presence of these, S(4) is equivalent to (D3) and (D4). % See \cite{dawson-cmkc} for proofs of these. \subsection{The General Correctness Compound Monad} \label{s-gcmon} Here we need to show that $\set\ (\TorN\ \alpha)$ is a monad; in fact, for any monad $M$, $M\ (\TorN\ \alpha)$ is a monad % Here we need to show that $\alpha\ \TorN\ \set$ is a monad; % in fact, for any monad $M$, $\alpha\ \TorN\ M$ is a monad (as is well-known, see, eg, \cite[\S 7.3]{lhj}, \cite{hpp-sum-tensor}). % For an arbitrary monad $M$ we define the compound monad $\alpha\ \TorN\ M$ by For an arbitrary monad $M$ we define the compound monad $M\ (\TorN\ \alpha)$ by \begin{align} \pext\ f\ (\Term\ a) & = f\ a \label{pextTerm} \\[-0.5ex] \pext\ f\ \NonTerm & = unit\M\ \NonTerm \label{pextNT} \end{align} We also define \unit\ and \ext\ for the compound monad by (\ref{UC}) and (\ref{EC}). Then we prove the \pext\ rules (\ref{E1K'}) to (\ref{E3'K_o}) as follows. (\ref{E1K'}) is just (\ref{pextTerm}). From \eqref{pextTerm} and \eqref{pextNT}, we get (\ref{E2K}) using \eqref{UC}, and (\ref{E3'K_o}) using (\ref{E1}) for $M$ and (\ref{EC}). % \begin{align*} % \pext\ \unit\ (\Term\ a) & = \unit\ a = \unitM\ (\Term\ a) \\ % \pext\ \unit\ \NonTerm & = \unitM\ \NonTerm % \end{align*} % and using these definitions and also (\ref{E1}) for $M$ and (\ref{EC}) % we get (\ref{E3'K_o}). \comment{ \begin{align*} \pext\ (\extNM\ g \oo f) (\Term\ a) & = (\extNM\ g \oo f)\ a \tag{\ref{pextTerm}} \\ & = \extNM\ g\ (f a) \\ & = \extNM\ g\ (\pext\ f\ (\Term\ a)) \tag{\ref{pextTerm}} \\ & = (\extNM\ g \oo \pext\ f)\ (\Term\ a) \end{align*} % \begin{align*} \pext\ (g \om f)\ \NonTerm & = \unitM\ \NonTerm \tag{\ref{pextNT}} \\ & = \pext\ g\ \NonTerm \tag{\ref{pextNT}} \\ & = \extM\ (\pext\ g)\ (\unitM\ \NonTerm) \tag{\ref{extru}} \\ & = \extM\ (\pext\ g)\ (\pext\ f\ \NonTerm) \tag{\ref{pextNT}} \\ & = (\pext\ g \oM \pext\ f)\ \NonTerm \tag{\ref{omext}M} \end{align*} } In fact the general correctness monad can be defined using \swap: that is, it satisfies J(1) and J(2). % of \cite{jd-cm}, % and (C1) to (C5) of \cite[\S 9.2]{bwttt}. Then the function \swap\ is given by the rule $\swap = \pext\ (\mapM\ \unitN)$, so with $M$ the \set\ monad we have % $\swap\ \NonTerm = \unitM\ \NonTerm = \{\NonTerm\}$, % and $\swap\ (\Term\ S) = \mapM\ \Term\ S = \{\Term\ s \,|\, s \in S\}$. \begin{align*} \swap\ \NonTerm & = \unitM\ \NonTerm = \{\NonTerm\} \\[-0.5ex] \swap\ (\Term\ S) & = \mapM\ \Term\ S = \{\Term\ s \,|\, s \in S\} \end{align*} We proved in Isabelle that \pext\ defined in this way satisfies rules (\ref{E1K'}) to (\ref{E3'K_o}) as outlined above, and we also proved that \swap\ satisfies the conditions S(1) to S(4), % of \cite{jd-cm}, and so $\swap$ is a distributive law for these monads. These Isabelle proofs are available at \url{http://users.rsise.anu.edu.au/~jeremy/isabelle/fgc/Dmng.{thy,ML}}. Henceforth we will refer to the functions defined for the general correctness monad as \pext\gc, \swap\gc, \ext\gc, and so on. \subsection{The Total Correctness Compound Monad} \label{s-tcmon} % The type \tcres\ = \state\ \set\ \TorN, relative to the type \state, The type \tcres\ = \TorN\ (\set\ \state), relative to the type \state, with the unit and extension functions defined below, is also a monad, % which we will call the \emph{total correctness} monad. % We have that \tcres\ = \state\ \set\ \TorN. % Each of the type constructors \set\ and \TorN\, % with their associated unit and extension functions, is a monad. % It does not follow, however, that \tcres\ (relative to \state) is a monad. To prove that the total correctness monad is in fact a monad, we now give the definitions for our particular monads $N = \set$ and $M = \TorN$. % These definitions use some auxiliary functions. \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\ \Ts & = \NonTerm \qquad \qquad \mbox{if $\NonTerm \in \Ts$}\\[-0.5ex] \prodd\tc\ \{\Term\ s \,|\, s \in \Ss\} & = \Term\ (\textstyle \bigcup \Ss) \\[-0.5ex] \pext\tc\ A\ S & = \prodd\tc\ \{A\ s \,|\, s \in S\} \\[-0.5ex] \ext\tc\ A\ T & = \ext\nt\ (\pext\tc\ A)\ T \end{align*} % where $\ext\nt$ is the extension function of the $\TorN$ monad (see \S \ref{s-monads}). % and $f ` S$ is Isabelle notation for $\{f\ s \,|\, s \in S\}$. % the set obtained by applying the % function $f$ to each member of the set $S$. We then proved, in Isabelle, that $\TorN\ (\set\ \alpha)$ is a compound monad, % $\sigma\ \set\ \TorN$ is a compound monad, by proving rules (\ref{E1K'}) to (\ref{E3'K_o}), noting that (\ref{EC}) and (\ref{UC}) follow directly from our definitions. % We have proved, in Isabelle, the following result. % We did this by proving rules (\ref{E1K'}) to (\ref{E3'K_o}), % noting that (\ref{EC}) and (\ref{UC}) follow directly from our definitions. % \begin{theorem} % $\sigma\ \set\ \TorN$ is a compound monad. % \end{theorem} \comment{ We have proved (see \S \ref{s-tc-pfs}) that these functions satisfy the monad rules: $$ \begin{array}{rcl@{\qquad \qquad \qquad \qquad}r} \ext\tc\ k \circ \unit\tc & = & k & \mbox{(Left Unit)} \\ \ext\tc\ \unit\tc & = & id & \mbox{(Right Unit)}\\ \ext\tc\ (\ext\tc\ h \circ k) & = & \ext\tc\ h \circ \ext\tc\ k & \mbox{\hfill (Assoc)} \end{array} $$ } % Jones \& Duponcheel \cite{jd-cm} also use a function % $\swap : \alpha M N \to \alpha N M$ to define a compound monad. % As they show, when such a function \swap\ can be defined, satisfying certain % conditions S(1) to S(4), then the compound monad $\alpha N M$ can be % constructed. % Equivalently, the function $\swap$ is a distributive law for monads, % see Barr \& Wells \cite[\S 9.2]{bwttt}. % The definition of \swap\ depends on the particular monads $M$ and $N$. In fact the total correctness monad can be defined using \swap. In this case $M$ is the \TorN\ monad, and $N$ is the set monad, and \swap\ is a function \begin{align*} % \swap\tc & : \sigma\ \TorN\ \set \to \sigma\ \set\ \TorN \notag \\ \swap\tc & : \set\ (\TorN\ \alpha) \to \TorN\ (\set\ \alpha) \notag \\ \swap\tc\ S & = \NonTerm \qquad \qquad \mbox{if $\NonTerm \in S$}\\[-0.5ex] \swap\tc\ \{\Term\ s \,|\, s \in S\} & = \Term\ S \end{align*} Our Isabelle proofs included the conditions S(1) to S(4), % of \cite{jd-cm}, and so we have also shown that $\swap\tc$ is a distributive law for the monads. These Isabelle proofs are available at \url{http://users.rsise.anu.edu.au/~jeremy/isabelle/fgc/Dtc.{thy,ML}}. Often, where two monads can be composed to form another monad, the construction depends on one of them, and the other may be arbitrary. Thus, as discussed in \S \ref{s-gcmon}, the \TorN\ monad % (ie, the type \emph{outcome} relative to the type \emph{state}) can be composed with any other % monad $M$ to give a compound monad $\alpha\ \TorN\ M$, monad $M$ to give a compound monad $M\ (\TorN\ \alpha)$, which gave the \emph{outcome set} monad. \comment{ In \cite[\S 3.1]{dawson-fgc}, we discussed how, although two monads cannot in general be composed to form another monad, but the \TorN\ monad (ie, the type \emph{outcome} relative to the type \emph{state}) can in general be composed with any other monad to give a compound monad. We used this fact to compose it with the set monad to form the {outcome set} monad. } % % In this case we have shown that the type $\sigma\ \set\ \TorN$, In this case we have shown that the type $\TorN\ (\set\ \alpha)$, with \unit\tc\ and \ext\tc\ as defined, is a monad, % (relative to $\alpha$), but we have not been able to give a more general construction for unit and extension functions to exhibit, for an arbitrary monad $M$, % either $\sigma\ M\ \TorN$ or $\sigma\ \set\ M$ as a monad. either $\TorN\ (M\ \alpha)$ or $M\ (\set\ \alpha)$ as a monad. \subsection{Relating the general correctness and total correctness monads} \label{s-gctc} % The function $\swap\tc : \sigma\ \TorN\ \set \to \sigma\ \set\ \TorN$ The function $\swap\tc : \set\ (\TorN\ \sigma) \to \TorN\ (\set\ \sigma)$ is also a \emph{monad morphism} from the {general correctness} monad to the {total correctness} monad. We have the following results, which characterise a monad morphism: % where \unit\gc\ and \ext\gc\ are the unit and extension functions for the % general correctness monad, as defined in \S \ref{s-gcmon}. % \begin{align*} % \unit\gc & : \state \to \outcome\ \set \\[-0.5ex] % \ext\gc & : (\state \to \outcome\ \set) \to \outcome\ \set \to \outcome\ \set % \end{align*} \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 this monad morphism is surjective, we could use the fact that the {general correctness} monad satisfies the monad rules to give an alternative proof to show that the {total correctness} monad also satisfies them. % DELETE IF SHORT OF SPACE The definition of \swap\tc\ reflects the fact that in the general correctness framework (the abstract command language) a computation (on a particular given input) may non-deteministically either terminate or not; in total correctness such a computation (on that input) does not satisfy any postcondition, and so is equivalent to a computation which simply does not terminate. We note that the definitions of many generalised substitution operations may be obtained by translation from the definitions in \cite{dawson-fgc} for abstract commands. Indeed, for the $\choice\tc$ function (see below), some results were more easily proved using the following translation from $\choice\gc$ of the general correctness model: $\choice\tc\ \Cs\ s = \swap\tc\ (\choice\gc\ \As\ s)$, for any set \As\ of abstract commands which gives the generalised substitutions \Cs, ie, such that $\Cs = \{\swap\tc\ A \,|\, A \in \As\}$. \subsection{Definition of Commands} \label{s-defs} % In \cite{dunne-gen-subs}, Dunne \citet{dunne-gen-subs} then defines a number of substitutions and operations on them, by giving their weakest preconditions and frames. % We then proved that the weakest precondition function is injective, % that is, if $[C]\ Q = [C']\ Q$, then $C = C'$. % (Again, we are ignoring frames). % This result justifies the practice of defining substitutions by % giving their weakest precondition, and shows that refinement-equivalent % substitutions are equal. In \cite{dawson-fgs} we give operational definitions for the % various generalised substitutions defined by % Dunne in \cite{dunne-gen-subs}, \citet{dunne-gen-subs}, and show that these definitions correspond. For example, sequencing, % of commands, which was defined by Dunne as $[A;B]\ Q = [B]\ ([A] Q)$, is represented by the composition $\odot$ in the Kleisli category. Then Dunne's definition gives an alternative proof (once we have proved that the weakest precondition function is injective) of the associativity of sequencing, and so of $\odot$, one of the key properties of monads. \comment{ \subsubsection{magic, abort, termination, feasibility} OMIT THIS UNLESS GIVING magic, abort for CHORUS The substitutions \magic\ (\abort) are those which always (never) satisfy any given postcondition. We \emph{define} \magic\ and \abort\ in terms of the operational model, as $\magic\ s = \Term\ \{\}$ and $\abort\ s = \NonTerm$. COULD OMIT Dunne defines the termination and feasibility predicates on initial states: $\trm(S) = [S] \mbox{true}$, and $\fis(S) = \lnot [S] \mbox{false}$. Our corresponding definitions are $\trm\tc\ C s \equiv C\ s \not= \NonTerm$ and $\fis\tc\ C s \equiv C\ s \not= \Term\ \{\}$. } \subsubsection{choice} \label{s-choice} % In \cite[\S 3.1]{dunne-gen-subs} Dunne \citet[\S 3.1]{dunne-gen-subs} defines a binary operator, $\Box$: $A \Box B$ is a computation which can choose between two computations $A$ and $B$. Again, Dunne defines this by giving its weakest precondition, $[A \Box B] Q = [A] Q \land [B] Q$. % (the conjunction of the weakest preconditions of the individual computations). This is a special case of choice among an arbitrary set of commands. In the general correctness setting this was easy to define, $\choice\gc\ \Cs\ s = \bigcup_{C \in \Cs} C\ s$. In the total correctness setting, where \choice\tc\ $\Cs$ can fail to terminate if any $C \in \Cs$ can fail to terminate, we define \choice\tc\ % as shown below. by: $\choice\tc\ \Cs\ s = \pext\tc\ (\lambda C.\ C\ s)\ \Cs$. % \comment{ As the definition is rather unintuitive, we show the types of some of its parts. % constituent parts. Recall that if the type $\sigma$ represents the machine state, then a command has type $\sigma \to \TorN\ (\set\ \sigma)$. % then a command has type $\sigma \to \sigma\ \set\ \TorN$. The definition is unintuitive perhaps because where \pext\ is used (indirectly) in defining sequencing of computations, the types $\alpha$ and $\beta$ are both the state type $\sigma$. But in the use of \pext\ below, $\alpha$ is the type of computations. % \begin{align*} \choice\tc\ \Cs\ s & = \pext\ (\lambda C.\ C\ s)\ \Cs \\ \choice\tc & : (\sigma \to \sigma\ \set\ \TorN)\ \set \to \sigma \to \sigma\ \set\ \TorN \\[-0.5ex] \pext\ & : (\alpha \to \beta\ \set\ \TorN) \to \alpha\ \set \to \beta\ \set\ \TorN \\[-0.5ex] \lambda C.\ C\ s & : (\sigma \to \sigma\ \set\ \TorN) \to \sigma\ \set\ \TorN \\[-0.5ex] \pext\ (\lambda C.\ C\ s) & : (\sigma \to \sigma\ \set\ \TorN)\ \set \to \sigma\ \set\ \TorN \end{align*} } Note how this definition uses polymorphism: when we use \pext\tc\ (indirectly) in defining sequencing of computations, the types $\alpha$ and $\beta$ are both the state type $\sigma$. But in this use of \pext, $\alpha$ is the type of computations. \begin{equation*} \pext\ : (\alpha \to \TorN\ (\set\ \beta)) \to \set\ \alpha \to \TorN\ (\set\ \beta) % (\alpha \to \beta\ \set\ \TorN) \to \alpha\ \set \to \beta\ \set\ \TorN \end{equation*} % Expanding the definition shows that: \begin{itemize} \item[] if $\NonTerm \in \{C\ s \,|\, C \in \Cs\}$ 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} \section{The Chorus Angelorum Monad} \label{s-chmon} In \S \ref{s-chom} we described a model of the computation as a function returning an up-closed set of sets of final states. % As Dunne \cite[\S 5.2]{dunne-chorus} explains, As \citet[\S 5.2]{dunne-chorus} explains, there is an alternative model, where a computation returns a set of sets of states, of which the demon first chooses one set of states, from which the angel chooses one state. We define a function \swap\uc\ which turns an angel-chooses-first result into the corresponding demon-chooses-first result; it swaps the order of the choices of the demon and the angel. As we shall see, it also has a role similar to that of the \swap\ function (the distributive law) discussed in \S\ref{s-cms}. We also define the \emph{up-closure} of a set of sets. % \begin{definition} \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*} % \end{definition} We then have the following results, which suggest that we should work on equivalence classes of sets of sets of states, where $\As \equiv \As'$ iff $\ucl\ \As = \ucl\ \As'$, and each equivalence class has exactly one up-closed member. \begin{lemma} With \ucl\ and \swap\uc\ as defined above, \begin{align*} \ucl\ (\ucl\ \As) & = \ucl\ \As \\[-0.5ex] \swap\uc\ (\swap\uc\ \As) & = \ucl\ \As \\[-0.5ex] \swap\uc\ (\ucl\ \As) & = \swap\uc\ \As \\[-0.5ex] \ucl\ (\swap\uc\ \As) & = \swap\uc\ \As \end{align*} \end{lemma} We cannot define a monad based on the \set\ (\set\ \_) type constructor, but we can define a monad on this set of equivalence classes. As such it is not a compound monad, but in obtaining it we proceed much as though we were combining the \set\ monad with itself using \swap\uc\ as a distributive law. The results described in this section have been proved in Isabelle, \url{http://users.rsise.anu.edu.au/~jeremy/isabelle/monad/Chorus.{thy,ML}} and \url{http://users.rsise.anu.edu.au/~jeremy/isabelle/fgc/{Dch,Dch_tc}.{thy,ML}}. Firstly we list some functions and their types, as used in \cite{jd-cm}. \begin{align*} % \join & : \alpha\ N\ M\ N\ M \to \alpha\ N\ M & % \prodd & : \alpha\ N\ M\ N \to \alpha\ N\ M \\[-0.5ex] % \dorp & : \alpha\ M\ N\ M \to \alpha\ N\ M & % \swap & : \alpha\ M\ N \to \alpha\ N\ M \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*} Here both the type constructors $M$ and $N$ are \set, but we can intuitively understand these functions, and some of the results about them, % Firstly, we give the types of these functions as in \cite{jd-cm}. by thinking of the type constructor $M$ as representing a set from which the angel is to choose, and $N$ as representing a set from which the demon is to choose. The final result is to be a set of sets from which the angel is to choose first, and then the demon. % We define a monad on this set of equivalence classes Imitating the procedure for defining $\set\ (\set\ \alpha)$ as a compound monad %$\alpha\ \set\ \set$, using the function $\swap\uc$, % using the function $\swap\uc\ : \set\ (\set\ \alpha) \to \set\ (\set\ \alpha)$, % we try to prove S(1) to S(4): % of \cite[\S 3.4]{jd-cm}: we cannot, but we can prove them modulo up-closure. We proved the following results, where \dorp\uc\ and \prodd\uc\ are defined from \swap\uc, following \cite{jd-cm}: \begin{align} \dorp\uc & = \join\s\ \oo \map\s\ \swap\uc \notag \\[-0.5ex] \prodd\uc & = \map\s\ \join\s\ \oo \swap\uc \notag % \\[1ex] \end{align} \begin{lemma} With \dorp\uc\ and \prodd\uc\ defined from \swap\uc\ as shown, \begin{align*} \swap\uc \oo \map\s\ (\map\s\ f) & = \\[-0.5ex] \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*} \end{lemma} That is, we have proved S(1) to S(3) modulo up-closure, and S(4). The proof of S(4) is difficult, and uses (equivalents of) (D3) and (D4) of % Barr \& Wells \cite[\S 9.2]{bwttt}. \citet[\S 9.2]{bwttt}. Then, as in \cite{jd-cm}, we define \join\uc\ by \eqref{join-prod}, or equivalently \eqref{join-dorp}. Defining \map\uc\ in the obvious way by \eqref{mapuc}, we define \ext\uc\ and $\odot_{uc}$ from \join\uc\ in the usual way by \eqref{extjm} and \eqref{oucext}, and also \pext\uc\ from \prodd\uc\ by \eqref{pextpm}. We can then prove \eqref{extEC} and \eqref{prod_Inter}. We also give the equivalent literal expressions for \ext\uc\ and \pext\uc. \begin{align} \map\uc\ f & = \map\s\ (\map\s\ f) \label{mapuc} \\[-0.5ex] \join\uc & = \join\s\, \oo \map\s\ \prodd\uc \label{join-prod} \\[-0.5ex] \join\uc & = \map\s\ \join\s\, \oo \dorp\uc \label{join-dorp} \\ \ext\uc\ f & = \join\uc\, \oo \map\uc\ f \label{extjm} \\[-0.5ex] \ext\uc & = \ext\s\, \oo \pext\uc \label{extEC} \\ g \odot_{uc} f & = \ext\uc\ g \oo f \label{oucext} \\ \pext\uc\ f & = \prodd\uc\, \oo \map\s\ f \label{pextpm} \\ \prodd\uc\ \As & = \textstyle \bigcap \{ \map\s\ \ucl\ \As \} \label{prod_Inter} \\ \pext\uc\ f\ A &= \{B \;|\; \forall a \in A.\ \exists B' \in f\ a.\ B' \subseteq B\} \\ \ext\uc\ f\ \As &= \{B \;|\; \exists A \in \As.\ \forall a \in A.\ \exists B' \in f\ a.\ B' \subseteq B\} \label{extlit} \end{align} The proofs of the monad rules for $\set\ (\set\ \alpha)$ %$\alpha\ \set\ \set$ (again, some equalities only modulo up-closure: compare the results below with \eqref{E1} to \eqref{E3'})) proceed as normal from S(1) to S(4) (see, eg, \cite{jd-cm} or \cite{dawson-cmkc}). \begin{lemma} \label{lem-extuc} With \join\uc\ defined by \eqref{join-prod} or equivalently \eqref{join-dorp}, and \ext\uc\ by \eqref{extjm} \begin{align} \ext\uc\ f\ \{\{x\}\} & = \ucl\ (f\ \{\{x\}\}) \label{E1uc} \\[-0.5ex] \ext\uc\ (\lambda x.\ \{\{x\}\}) & = \ucl \label{E2uc} \\[-0.5ex] \ext\uc\ (\ext\uc\ g \oo f) & = \ext\uc\ g \oo \ext\uc\ f \label{E3'uc} \end{align} \end{lemma} \subsubsection{The Monad Functions on \emph{Up-closed} Sets of Sets} Finally we need to show that these results give a monad on the set of equivalence classes, which requires several lemmas concerning the behaviour of \ext\uc\ and other functions on different but ``equivalent'' arguments. Isabelle's \emph{type definition} facility was useful here, not least in ensuring that no necessary part of the proof was overlooked. We define the type $\uca\ \alpha$ % $\alpha\ \uca$ (``up-closed abstract'') as the type of up-closed sets of sets (a representative of each of the equivalence classes). % mentioned earlier). % This uses an Isabelle \emph{type definition}: The set of members of the new type is isomorphic to, but distinct from, the set of up-closed sets of sets. In Isabelle, defining a new type $\sigma$ (the ``abstract'' type) isomorphic to a set $S : \set\ \rho$ causes the creation of an abstraction function $\Abs : \rho \to \sigma$ and a representation function $\Rep : \sigma \to \rho$, such that \Abs\ and \Rep\ are mutually inverse bijections between $S$ and the set of all values of type $\sigma$. Note that the domain of \Abs\ is the type $\rho$, but that nothing is said about the values it takes outside the set $S$. Thus we get abstraction and representation functions $\Rep\_\uca : \uca\ \alpha \to \set\ (\set\ \alpha)$ and $\Abs\_\uca : \set\ (\set\ \alpha) \to \uca\ \alpha$. We define an alternative abstraction function \ucAbs\ of the same type as \Abs\_\uca\ but whose action is specified, in the natural way, on non-upclosed sets: $\ucAbs\ \As \equiv \Abs\_\uca\ (\ucl\ \As)$. Then we define the monad functions \unit\_\uca\ and \ext\_\uca\ for the $\uca\ \alpha$ type; we also define \swap\ on this type. \begin{definition} \label{def-uca} \begin{align} \unit\_\uca\ a & = \ucAbs\ \{\{a\}\} \label{unitU_def} \\[-0.5ex] \ext\_\uca\ f\ \As & = \ucAbs\ (\ext\uc\ (\Rep\_\uca\ \oo f)\ (\Rep\_\uca\ \As)) \label{extU_def} \\[-0.5ex] \swap\_\uca\ \As & = \ucAbs\ (\swap\uc\ (\Rep\_\uca\ \As)) \label{swapU_def} \end{align} \end{definition} We then used \eqref{E1uc} to \eqref{E3'uc} about the type $\set\ (\set\ \alpha)$ to prove the monad rules \eqref{E1} to \eqref{E3'} for the type $\uca\ \alpha$. \begin{theorem} \label{thm-uca} The type constructor \uca, with unit and extension functions \unit\_\uca\ and \ext\_\uca, is a monad. \end{theorem} \subsubsection{Changing the Interpretation ; the Conjugate of a Substitution} \label{s-conj} The result of a computation might equally well be modelled as a set of sets from which the demon is to choose first, using the same monad, but translating the result by \swap\uc. % but applying \swap\uc\ to the result. We showed that the function \swap\_\uca\ (Definition~\ref{def-uca}, \eqref{swapU_def}) is a monad morphism. % We also proved some results such as $\swap\uc \oo \prodd\uc = \dorp\uc$ which would involve a type error if $M$ and $N$ were not the same monad. Dunne also defines the conjugate of a substitution \cite[\S 3.4]{dunne-chorus}: $[T^o] Q = \lnot [T] \lnot Q$. This also amounts to switching the interpretation of the set-of-sets result from angel-chooses-first to demon-chooses-first. Thus we can obtain it by applying \swap\uc\ to the result of a computation, so we proved $T^o\ s = \swap\_\uca\ (T\ s)$. \subsubsection{A Link to the Continuation Monad} \label{s-cont-mon} We can obtain an interesting link to the continuation monad \cite[\S 3.1]{Wadler-essence}. We define an ``evaluation function'' $\evaluc : \set\ (\set\ \alpha) \to (\alpha \to \bool) \to \bool$, where $\evaluc\ \As\ P$ tells whether the postcondition $P$ is satisfied when angel and demon have made their choices from \As. (The weakest precondition function could then be defined in terms of \evaluc). Naturally it is defined by $\evaluc\ \Bs\ P \equiv \exists B \in \Bs.\ \forall b \in B.\ P\ b$, and so has the property that $\evaluc\ \Bs\ = \evaluc\ (\ucl\ \Bs)$. % in Isabelle, uc_eval_of_uc Thus also, if \Bs\ is up-closed and $P'$ is the set corresponding to predicate $P$, then we have $\evaluc\ \Bs\ P' = P \in \Bs$. This shows that the model we describe is also essentially that of the choice semantics of % Back \& von Wright \cite[Ch~15]{back-vw}. \citet[Ch~15]{back-vw}. Now the type $K\ \alpha = (\alpha \to \bool) \to \bool$ is the type of the continuation monad $K$ \cite[\S 3.1]{Wadler-essence}, when the fixed ``answer'' type is \bool. The composition $\odot_K$ in the Kleisli category for $K$ can be given simply in terms of the $C$ combinator: % oK_def, C_def \begin{align*} C\ f\ x\ y &= f\ y\ x & g \odot_K f &= C\ (C\ f \oo C\ g) \end{align*} The functions \Ball\ and \Bex, of type $\set\ \alpha \to K\ \alpha$, used in Isabelle to express quantification over a given set: $\Ball\ S\ P \equiv \forall s \in S.\ P\ s$, can be used to express the way the functions above involve the demonic and angelic choices. We find that % (where $\odot_K$ is the composition in the Kleisli category for $K$) $\evaluc = \Ball \odot_K \Bex$ and $\evaluc \oo \swap\uc = \Bex \odot_K \Ball$. % \begin{align*} % \evaluc & = \Ball \odot_K \Bex & % \evaluc \oo \swap\uc & = \Bex \odot_K \Ball % \end{align*} Further, there is an obvious isomorphism $K\ \alpha \to \set\ (\set\ \alpha)$, which we call \ktoss. Thus $\ucl = \ktoss\, \circ\, \evaluc$. % in Isabelle, uc_of_fam Then we find these results which represent the sequence of angelic and demonic choices involved in these functions. % % \newpage new para causes page break here, for version submitted % The last of these rusults provides an % alternative proof of the associativity of $\odot\uc$, % which translates to rule (\ref{kass}) for the \uca\ monad. % \begin{align*} % in Isabelle, uc_of_fam, uc_swap_fam, uc_dorp_fam, uc_prod_fam, % uc_join_fam, uc_pext_fam, uc_ext_fam \ucl & = \ktoss \oo (\Ball \odot_K \Bex) \\ \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*} Under the isomorphism \ktoss, up-closed sets correspond to \emph{monotonic} continuations, which we define by % in Isabelle, monoK_def, liftimp, ucf_iff_monobc $$\mon_K\ c \equiv \forall P\ Q.\ (\forall s.\ P\ s \Rightarrow Q\ s) \Rightarrow c\ P \Rightarrow c\ Q$$ Then we find that \ktoss\ and \evaluc\ are mutually inverse bijections between the up-closed families of sets and the monotonic continuations. % in Isabelle, eval_of_fam, KtoSS_eval It follows that there is a bijective correspondence between functions $f : \alpha \to K\ \beta$ which always return monotonic continuations, and functions $S : \alpha \to \set\ (\set\ \beta)$ which always return up-closed families. From this we can get the bijective correspondence of \citet{rewitzky-03} between monotonic predicate transformers $F : (\beta \to \bool) \to (\alpha \to \bool)$ and up-closed binary multirelations. Trivially, $\Ball\ S$ and $\Bex\ S$ are monotonic, % in Isabelle, monoK_Ball, monoK_Bex and also $\odot_K$ preserves monotonicity in this sense: % in Isabelle, oK_monoK $$\forall a.\ \mon_K\ (f\ a) \land \forall b.\ \mon_K\ (g\ b) \Rightarrow \forall x.\ \mon_K\ ((g \odot_K f)\ x)$$ Similar to the results above is the following: $$f \odot_{uc} g = \ktoss \oo ((\evaluc \oo f) \odot_K (\evaluc \oo g))$$ This leads to an alternative proof of the associativity of $\odot\uc$, for % and thence of rule (\ref{kass}) for the \uca\ monad \begin{align*} f & \odot_{uc} (g \odot_{uc} h) \\ & = \ktoss \oo ((\evaluc \oo f) \odot_K \\ & \qquad (\evaluc \oo (\ktoss \oo ((\evaluc \oo g) \odot_K (\evaluc \oo h))))) \\ & = \ktoss \oo ((\evaluc \oo f) \odot_K ((\evaluc \oo g) \odot_K (\evaluc \oo h))) \end{align*} where $\evaluc\, \oo \ktoss$ is the identity on its argument, which is monotonic. Thus the associativity of $\odot_{uc}$ follows from that of $\odot_K$. \subsubsection{Angelic and Demonic Choice} \label{s-adchoice} % In \cite{dunne-chorus} Dunne \citet{dunne-chorus} defines angelic (demonic) choice by giving their weakest preconditions, which are just the disjunctions (conjunctions) of the preconditions of the individual substitutions. In the case of each of these, applying a set of computations to an initial state gives a set of sets of sets of final states, of type $\set\ (\set\ (\set\ \sigma))$. In the case of angelic choice, the angel makes the first two choices and the demon the final choice, so for angelic choice we simply take the union of the results of the individual computations. For demonic choice, the consecutive choices are made by the demon, the angel and the demon again. This is exactly as for the \prodd\uc\ function. % (The actual definition uses \pext\uc, and is similar to that of \choice\tc). The definitions are as follows, but we omit the functions \ucAbs\ and \Rep\_\uca\ between the $\set\ (\set\ \alpha)$ and the $\uca\ \alpha$ types. \begin{align*} \dem\ \Bs\ s & = \prodd\uc\ \{B\ s\ |\ B \in \Bs\} = \pext\uc\ (\lambda B.\ B\ s)\ \Bs \\ \ang\ \Bs\ s & = \textstyle \bigcup\ \{B\ s\ |\ B \in \Bs\} \end{align*} So these results are analogous to those above: % % in Isabelle, Union_fam, uc_prod_Inter, uc_prod_fam \begin{align*} \textstyle \ucl \oo \bigcup = \bigcup \oo\, \map\s\ \ucl & = \ktoss \oo (\Ball \odot_K \Bex \odot_K \Bex) \\ \textstyle \bigcap \oo\, \map\s\ \ucl & = \ktoss \oo (\Ball \odot_K \Bex \odot_K \Ball) \end{align*} \subsubsection{Sequencing and Choice} \label{s-seq-choice} We proved the following results about the distribution of demonic or angelic choice over sequencing, where the notation implies demonic or angelic choice of a set of commands. $$\dem\ \Bs\ ;\ C = \dem_{B \in \Bs}\ (B\, ; C) \qquad \ang\ \Bs\ ;\ C = \ang_{B \in \Bs}\ (B\, ; C) $$ Note that these results hold because in either case there is first a choice of $B \in \Bs$, and then execution of $(B\, ; C)$. The similar results for choice of $C$, ie, $B\, ; (\dem_{C \in \Cs} C) = \dem_{C \in \Cs} (B\, ; C)$ do not hold, since that would involve reordering the demonic choice of $C$ with the choices involved in executing $B$. The proofs of these results use \eqref{exts_ouc} and \eqref{pext_ouc} (which is of the form of \eqref{E3'K_o}); note however that in this use of them, $g$ is $C$, while $f$ is not a command, but rather the function $\lambda B.\ B\ s$, for an initial state $s$. \begin{align} \ext\s\ (\ext\uc\ g \oo f) & = \ext\uc\ g \oo \ext\s\ f \label{exts_ouc} \\[-0.5ex] \pext\uc\ (\ext\uc\ g \oo f) & = \ext\uc\ g \oo \pext\uc\ f \label{pext_ouc} \end{align} Since $\ext\uc = \ext\s \oo \pext\uc$, \eqref{exts_ouc} and \eqref{pext_ouc} combine to give \eqref{E3'uc}, of the form of \eqref{E3'}, which is the significant (usually non-trivial) one among the monad rules. \subsubsection{A Monad Morphism from the Total Correctness Monad} \label{s-ch2tc} As Dunne points out, the language of extended substitutions encompasses that of generalised substitutions. We defined the inclusion mapping \tctoch, of type $\TorN\ (\set\ \alpha) \to \uca\ \alpha$, as shown below (and as suggested by the discussion in \cite[\S 5.1,\S 5.2]{dunne-chorus}) \begin{align} \label{tctoch_Term} \tctoch\ (\Term\ S) & = \ucAbs\ \{S\} \\[-0.5ex] \label{tctoch_NT} \tctoch\ \NonTerm & = \ucAbs\ \{\} \end{align} % OMIT TO SAVE SPACE For the result \NonTerm, which fails every postcondition, we get the corresponding result $\{\}$, because from it the angel cannot choose a set of results all of which satisfy even the postcondition \emph{true}. At the other extreme is the result $\Term\ \{\}$, which satisfies every postcondition. Corresponding to it we have a result from which the angel can choose $\{\}$, from which the demon cannot choose any which will fail to satisfy even the postcondition \emph{false}. We proved that this mapping is a monad morphism. Since this mapping is \emph{injective}, it gives an alternative proof that the total correctness monad is in fact a monad. This is an interesting contrast to the point noted in \S\ref{s-gctc}, where a \emph{surjective} mapping \emph{from} the general correctness monad into the type $\tcres\ \alpha$ provided yet another proof that the total correctness monad is in fact a monad. \section{Conclusion; Further Work} \label{s-concl} We have shown how several models of computation arising naturally in the study of program semantics are based on monads, which can be shown to be monads using results on combining two monads using a distributive law. % The construction used in \S \ref{s-gcmon} For the general correctness monad we used a well-known general construction combining the error (\TorN) monad with \emph{any} monad $M$. % In \S \ref{s-tcmon} we used a different The total correctness monad used a different construction, which seems not to be similarly generalisable. For the Chorus Angelorum monad, having combined the set monad with itself, we needed to take equivalence classes of the result. In the first two cases the combined monad arises from a distributive law for monads, and in the third case, the distributive law equations are satisfied modulo the equivalence relation. In this case the proofs that we have a monad were helped significantly by basing our approach on the results of \cite{bwttt} and \cite{jd-cm} on compound monads based on a distributive law. (Trying to prove equation \eqref{E3'uc} using \eqref{extlit} as a definition is not recommended!) We also found some monad morphisms relating these monads: in some cases the distributive laws are themselves monad morphisms. All the discussion of compound monads in this paper focussed on distributive laws. There are several monad transformers, or constructions which produce compound monads, such as those described by % Liang, Hudak and Jones \cite{lhj}. \citet{lhj}. The theory underlying these has been analysed, for example by % Hyland, Plotkin and Power \cite{hpp-sum-tensor}, \citet{hpp-sum-tensor}, who give several general constructions, dealing with arbitrary categories (such as $\omega-$\textbf{Cpo}) rather than just the category of sets. While all our work (and in particular, our Isabelle proofs) are, following \cite{JG} and \cite{dunne-chorus}, in terms of sets, it would be interesting to investigate whether the Chorus Angelorum operational model and monad can be extended in this way to a more general category than \textbf{Set}, and whether any of the constructions for a compound monad, other than the distributive law, can similarly be applied to that situation. % \paragraph{Acknowledgements} % Finally, we thank some anonymous referees for very helpful comments. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Here begins the end matter %\vspace*{-1em} % \bibliography{cmsl} % \bibliographystyle{plainnat} % above lines replaced by the following from cmsl.bbl \begin{thebibliography}{18} \providecommand{\natexlab}[1]{#1} \providecommand{\url}[1]{\texttt{#1}} \expandafter\ifx\csname urlstyle\endcsname\relax \providecommand{\doi}[1]{doi: #1}\else \providecommand{\doi}{doi: \begingroup \urlstyle{rm}\Url}\fi \bibitem[Back and von Wright(1998)]{back-vw} Ralph-Johan Back and Joakim von Wright. \newblock \emph{Refinement Calculus: A Systematic Introduction}. \newblock Graduate Texts in Computer Science, Springer, 1998. \newblock URL \url{http://crest.cs.abo.fi/publications/public/1998/RefinementCalculusBook.% pdf}. \bibitem[Barr and Wells(1983)]{bwttt} Michael Barr and Charles Wells. \newblock \emph{Toposes, Triples and Theories}. \newblock Springer-Verlag, 1983. \newblock URL \url{http://www.cwru.edu/artsci/math/wells/pub/ttt.html}. \bibitem[Dawson(2007{\natexlab{a}})]{dawson-cmkc} Jeremy~E Dawson. \newblock Compound monads and the {K}leisli category. \newblock Unpublished note, 2007{\natexlab{a}}. \newblock URL \url{http://users.rsise.anu.edu.au/~jeremy/pubs/cmkc/}. \bibitem[Dawson(2004)]{dawson-fgc} Jeremy~E Dawson. \newblock Formalising general correctness. \newblock In \emph{Computing: The Australasian Theory Symposium}, volume ENTCS {91}, pages 21--42, 2004. \newblock URL \url{http://www.elsevier.com/locate/entcs}. \bibitem[Dawson(2007{\natexlab{b}})]{dawson-fgs} Jeremy~E Dawson. \newblock Formalising generalised substitutions. \newblock In \emph{Theorem Proving in Higher-Order Logics}, page to appear, 2007{\natexlab{b}}. \newblock URL \url{http://users.rsise.anu.edu.au/~jeremy/pubs/fgc/fgs/}. \bibitem[Dijkstra(1976)]{dijkstra-gcl} Edsger~W Dijkstra. \newblock \emph{A Discipline of Programming}. \newblock Prentice-Hall International, 1976. \bibitem[Dunne(2001)]{dunne-abstr-cmds} Steve Dunne. \newblock Abstract commands: A uniform notation for specifications and implementations. \newblock In \emph{Computing: The Australasian Theory Symposium}, volume ENTCS {42}, pages 104--123, 2001. \newblock URL \url{http://www.elsevier.com/locate/entcs}. \bibitem[Dunne(2007)]{dunne-chorus} Steve Dunne. \newblock Chorus angelorum. \newblock In \emph{B 2007: Formal Specification and Development in B}, volume LNCS 4355, pages 19--33. Springer, 2007. \bibitem[Dunne(2002)]{dunne-gen-subs} Steve Dunne. \newblock A theory of generalised substitutions. \newblock In \emph{Formal Specification and Development in Z and B, (ZB 2002)}, volume LNCS 2272, pages 270--290. Springer, 2002. \vfill\eject \bibitem[Hyland et~al.(2006)Hyland, Plotkin, and Power]{hpp-sum-tensor} Martin Hyland, Gordon~D Plotkin, and John~A Power. \newblock Combining effects: Sum and tensor. \newblock \emph{Theor. Comput. Sci.}, 357:\penalty0 70--99, 2006. \bibitem[Jacobs and Gries(1985)]{JG} Dean Jacobs and David Gries. \newblock General correctness: A unification of partial and total correctness. \newblock \emph{Acta Informatica}, 22:\penalty0 67--83, 1985. \bibitem[Jones and Duponcheel(1993)]{jd-cm} Mark~P Jones and Luc Duponcheel. \newblock Composing monads. \newblock Technical Report YALEU/DCS/RR-1004, Yale University, 1993. \bibitem[Liang et~al.(1995)Liang, Hudak, and Jones]{lhj} Sheng Liang, Paul Hudak, and Mark~P Jones. \newblock Monad transformers and modular interpreters. \newblock In \emph{Symposium on Principles of Programming Languages (POPL'95)}, pages 333--343, 1995. \bibitem[Martin et~al.(2007)Martin, Curtis, and Rewitzky]{mcr} Clare~E Martin, Sharon~A Curtis, and Ingrid Rewitzky. \newblock Modelling angelic and demonic nondeterminism with multirelations. \newblock \emph{Sci. Comput. Program.}, 65:\penalty0 140--158, 2007. \bibitem[Moggi(1989)]{moggi-monads} Eugenio Moggi. \newblock Computational lambda-calculus and monads. \newblock In \emph{Symposium on Logic in Computer Science (LICS)}. IEEE, 1989. \bibitem[Plotkin(1976)]{plotkin-powerdomain} Gordon~D Plotkin. \newblock A powerdomain construction. \newblock \emph{SIAM J.~Computing}, 5:\penalty0 452--487, 1976. \bibitem[Rewitzky(2003)]{rewitzky-03} Ingrid Rewitzky. \newblock Binary multirelations. \newblock In \emph{Theory and Applications of Relational Structures as Knowledge Instruments 2003}, volume LNCS 2929, pages 256--271. Springer, 2003. \bibitem[Wadler(1992)]{Wadler-essence} Philip Wadler. \newblock The essence of functional programming. \newblock In \emph{Symposium on Principles of Programming Languages (POPL'92)}, pages 1--14, 1992. \end{thebibliography} \end{document} %%% Local Variables: %%% mode: latex %%% TeX-master: t %%% End: