%%
%%
\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\mono{\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\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{lemma}[thm]{Lemma}
%\newtheorem{defn}[thm]{Definition}
%\newtheorem{cor}{Corollary}[thm]
%\renewcommand\thecor{\thethm(\arabic{cor})}

\pagestyle{plain}

\begin{document}

%% Here begins the main text

\title{Compound Monads and Models of Computation}% (Extended Abstract)}

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

\section{Introduction}
\label{s-id}

In several papers Dunne has proposed formal systems for analysing 
(variously named) ``computations'', given rules for combining these
computations in various ways, and proved results about them.
Underlying each of these theories 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 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 gave an account of general correctness
(Jacob \& Gries \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}, which used
the construction of Plotkin \cite{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 considered the generalised substitutions used in the B~method.
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 \cite{back-vw},
and Rewitzky \cite{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.
Recently, in \cite{dunne-chorus} Dunne defined an ``extended substitution''
language,
which encompasses the generalised substitutions, 
allowing for angelic choice as well as demonic choice.
% He described the model for these in terms of ``up-closed binary
% multirelations''.  
In this paper we describe how the operational model we use 
(equivalent to the multirelation model) is 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.
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.

All results referred to in this paper have been proved using 
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  (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:
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$.

% 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 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 
and total correctness refinement accordingly:
\begin{align*}
[C]\ Q\ s & = \exists S.\ (\forall x \in S.\ Q\ x) \land C\ s = \Term\ S \\
A \sqsubseteq_{tc} B & = \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'$.

\subsection{The Chorus Angelorum Operational Model} \label{s-chom}

In \cite{dunne-chorus}, Dunne notes that conventional program analysis 
involves demonic choice: we want a non-deterministic program to satisfy its
post-condition, regardless of what choices the demon makes.
% First he dualises this, so that the choices are made by an angel (who aims
% to see the post-condition 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}
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 = \exists U \in C s.\ (\forall u \in U.\ Q\ u)$$ 

% 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}, 
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,
of the types shown,
and show that the unit and extension functions
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 sequencing of computations $B$ and $A$,
as $\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 following
expected properties \eqref{krid} to \eqref{kass}.
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 examples of monads used in this paper are the ``non-termination'' monad
(well-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 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 \\[-0.5ex]
\map\nt\ f\ \NonTerm & = \NonTerm &
\map\nt\ f\ (\Term\ s) & = \Term\ (f\ s) \\[-0.5ex]
\join\nt\ \NonTerm & = \NonTerm \\[-0.5ex]
\join\nt\ (\Term\ (\Term\ f)) & = \Term\ f &
\join\nt\ (\Term\ \NonTerm) & = \NonTerm \\[-0.5ex]
\ext\nt\ f\ \NonTerm & = \NonTerm &
\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.
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},
and are closely related to the distributive law
of Barr \& Wells \cite[\S 9.2]{bwttt}.

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. 
Space does not permit us to give details of the latter.

Jones \& Duponcheel \cite{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 compound monads that satisfy both J(1) and J(2) are those which arise
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,
or from a function \pext\ as above, 
though it seems that in most cases they do so. 
If so, $\lambda = \pext\ (\mapM\ \unitN)$.

The function \swap\ of \cite{jd-cm} is the distributive law 
$\lambda$ of \cite[\S 9.2]{bwttt}.
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$.
% 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.

Likewise, conditions S(1) to S(4) of \cite{jd-cm} on the function \swap\
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) can be shown 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, where 
$\Cs = \{\swap\tc\ A \,|\, A \in \As\}$.
 
\subsection{Definition of Commands} \label{s-defs}
In \cite{dunne-gen-subs}, Dunne 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},
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 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*}
}
Expanding this definition shows that:

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

\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, 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 &
\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*}
\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) & = \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 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}.

Then, as in \cite{jd-cm}, we define 
\join\uc\ by \eqref{join-prod}, or equivalently \eqref{join-dorp}.
We then 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}
\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 post-condition $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}.

Now the type $(\alpha \to \bool) \to \bool$ is the type of the continuation
monad $K\ \alpha$ \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
$$\mono_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
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.\ \mono_K\ (f\ a) \land \forall b.\ \mono_K\ (g\ b)  
  \Rightarrow \forall x.\ \mono_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 \\
  & \quad 
    (\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 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.
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}.
The theory underlying these has been analysed,
for example by Hyland, Plotkin and Power \cite{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}

\bibliographystyle{plain}

\begin{thebibliography}{99}

\bibitem{back-vw}
Ralph-Johan Back and Joakim von Wright.
Refinement Calculus: A Systematic Introduction.
Graduate Texts in Computer Science, Springer, 1998.
\url{http://crest.cs.abo.fi/publications/public/1998/RefinementCalculusBook.pdf}

\bibitem{bwttt}
Michael Barr and Charles Wells.
Toposes, Triples and Theories.
Springer-Verlag, 1983, or see
\url{http://www.cwru.edu/artsci/math/wells/pub/ttt.html}

\bibitem{dawson-cmkc} Jeremy~E~Dawson.
{Compound Monads and the Kleisli Category}.
Unpublished note. 
\url{http://users.rsise.anu.edu.au/~jeremy/pubs/cmkc/} 

\bibitem{dawson-fgc} Jeremy~E~Dawson.
{Formalising General Correctness}.
In Computing: The Australasian Theory Symposium (2004),
% Electronic Notes in Theoretical Computer Science \textbf{91} (2004),
% 21--42.
ENTCS \textbf{91} (2001), 21--42.
{\url{http://www.elsevier.com/locate/entcs}}

\bibitem{dawson-fgs} Jeremy~E~Dawson.
{Formalising General Substitutions}.  Submitted.
\url{http://users.rsise.anu.edu.au/~jeremy/pubs/fgc/fgs/} 

\bibitem{dunne-abstr-cmds} Steve Dunne. 
{Abstract Commands: A Uniform Notation for Specifications and Implementations}.
In Computing: The Australasian Theory Symposium (2001),
% Electronic Notes in Theoretical Computer Science \textbf{42} (2001),
% 104--123.
ENTCS \textbf{42} (2001), 104--123.
{\url{http://www.elsevier.com/locate/entcs}}

\bibitem{dunne-gen-subs} Steve Dunne. 
A Theory of Generalised Substitutions.  
In Formal Specification and Development in Z and B,
2nd International Conference of B and Z Users, Grenoble, 2002 (ZB 2002), 
Lecture Notes in Computer Science 2272, Springer 2002, 270--290.

\bibitem{dunne-chorus} Steve Dunne. 
Chorus Angelorum.  In 
B 2007: Formal Specification and Development in B,
7th International Conference of B Users, Besan\c con, 2007,
LNCS 4355, Springer, 2007, 19--33.

\bibitem{JG} Dean Jacobs and David Gries.
\emph{General Correctness: A Unification of Partial and Total Correctness}.
Acta Informatica \textbf{22} (1985), 67-83.

\bibitem{hpp-sum-tensor}
Martin Hyland, Gordon D Plotkin and John A Power.
Combining effects: Sum and tensor.
Theor. Comput. Sci. 357(1-3): 70-99, 2006.

\bibitem{jd-cm} Mark P~Jones \& Luc Duponcheel. Composing Monads.
Research Report YALEU/DCS/RR-1004, Yale University, December 1993

\bibitem{lhj} Sheng Liang, Paul Hudak and Mark P Jones.
Monad Transformers and Modular Interpreters.
In Symposium on Principles of Programming Languages (POPL'95), 1995, 333--343.

\bibitem{mcr} 
Clare E Martin, Sharon A Curtis, Ingrid Rewitzky.
Modelling angelic and demonic nondeterminism with multirelations.
Sci. Comput. Program.  65(2): 140-158 (2007).

\bibitem{moggi-monads} Eugenio Moggi.
Computational lambda-calculus and monads.
In IEEE Symposium on Logic in Computer Science (LICS), IEEE, June 1989.

\bibitem{plotkin-powerdomain} Gordon D Plotkin.
A powerdomain construction.  SIAM J.~Computing. 5 (1976), 452--487.

\bibitem{rewitzky-03} 
Ingrid Rewitzky. Binary Multirelations.
Theory and Applications of Relational Structures as Knowledge Instruments 2003,
LNCS 2929, Springer, 2003, 256--271.

\bibitem{Wadler-essence} Philip Wadler. The Essence of Functional Programming.
In Symposium on Principles of Programming Languages (POPL'92), 1992, 1--14.

\end{thebibliography}

\end{document}

%%% Local Variables: 
%%% mode: latex
%%% TeX-master: t
%%% End: 

