
\documentclass{beamer}

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

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

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

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

\def\dem{\mathop{\rm dem}}
\def\ang{\mathop{\rm ang}}

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

\begin{document}

\frame{\titlepage}

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

\section{Introduction}
\frame
{
  \frametitle{Introduction}
  Several sorts of refinement suggested by Dunne. \\
  \begin{itemize}
\item General Correctness 
\item Total Correctness 
\item Chorus Angelorum 
  \end{itemize}
  Each is based, implicitly or explicitly, on a notion of what a computation
  is, an underlying ``model of computation'' \\[1ex]

  Each underlying ``model of computation'' is based on a \alert{monad} \\[1ex]

  Each of these monads is, or is somewhat like, a \alert{compound monad}
  }

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

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

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

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

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

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

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

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

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

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

\subsection{The Total Correctness Operational Model} \label{s-tcom}
\frame
{
  \frametitle{The Total Correctness Operational Model}
  Related to semantics of the B-method, \\
  only interested in total correctness (weakest preconditions). \\[1ex]

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

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

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

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

  }

\subsection{The Chorus Angelorum Operational Model} \label{s-chom}
\frame
{
  \frametitle{The Chorus Angelorum Operational Model}
  Ordinarily, non-determinism is \alert{demonic} choice \\
  (all possible results must satisfy post-condition $\equiv$ \\
  the result chosen by a \alert{demon} satisfies post-condition) \\[1ex]

  Want to model \alert{angelic} and \alert{demonic} non-determinism \\[1ex]

  Computation returns a \alert{set of sets} \As\ of states:
  \begin{itemize}
  \item angel chooses set $A \in \As$
  \item demon chooses state $a \in A$
  \end{itemize}
weakest precondition function (hence refinement):
$$ [C]\ Q\ s = \exists U \in C\ s.\ (\forall u \in U.\ Q\ u)$$ 

If $A \in \As$, $A' \supseteq A$, to include $A'$ in \As, or not, makes no
difference: \\
consider only \As\ \alert{up-closed}:
if $A' \supseteq A$ and $A \in \mathcal A$
then $A' \in \mathcal A$.
  }

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

  In each case, to confirm model is appropriate,
  % having formally described a model of computation, 
  \begin{itemize}
  \item we show two computations refinement-equivalent 
  iff they are the same function (of type used in model) 
  \item we \alert{define} operations operationally,
  and  \alert{prove} these definitions
  correspond to Dunne's definitions 
  (which use weakest preconditions)
  \end{itemize}
  (Caveat: we ignore ``frames''). \\[1ex]
  Note: all proofs in the theorem prover Isabelle/HOL
  }

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

~ 

Define unit and extension functions, satisfying rules
\begin{align*}
\unit &: \alpha \to M \alpha \\[-0.5ex]
\ext &: (\alpha \to M \beta) \to (M \alpha \to M \beta) 
\end{align*}
\begin{align*}
\clabel{E1} \ext\ f \oo \unit & = f  \\[-0.5ex]
\clabel{E2} \ext\ \unit & = \id  \\[-0.5ex]
\clabel{E3'} \ext\ (\ext\ g \oo f) & = \ext\ g \oo ext\ f  
\end{align*}

or functions \unit, \map\ and \join\ (7 axioms for these)

~

Can represent the structure of a computation (Moggi)

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

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

\pause 

Properties \eqref{krid} to \eqref{kass} show that we have a category:

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

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

\pause 

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

\subsection{Compound Monads} \label{s-cms}
\frame
{
  \frametitle{Compound Monads}
Let $M$ and $N$,
each with unit and extension functions, be monads.
\\[1ex] 
Then is $M N \alpha$ a monad?  
Need $\unit\NM : \alpha \to M N \alpha$ and $\ext\NM$ 
\\[1ex]
\ext\NM\ ``extends'' a function $f$ from domain $\alpha$ to $M N \alpha$.
\\[1ex] 
\pext, ``partial extension'', does part of this
%
\begin{align*}
\ext\NM &: (\alpha \to M N \beta) \to (M N \alpha \to M N \beta) \\[-0.5ex]
\pext &: (\alpha \to M N \beta) \to (N \alpha \to M N \beta) 
\end{align*}
\pause
Definitions using \pext\ for a compound monad
% \label{E3K} \pext\ (g \oNM f) & = \pext\ g \oM pext\ f  \\
\begin{align*}
\clabel{EC} \ext\NM\ g & = \ext\M\ (\pext\ g)  \\[-0.5ex]
\clabel{UC} \unit\NM & = \unit\M \oo \unit\N
\end{align*}
  }

\frame
{
  \frametitle{Compound Monads --- rules for \pext}
\pext\ also must satisfy three rules
\begin{align*}
\clabel{E1K'} \pext\ f \oo \unit\N & = f  \\
\clabel{E2K} \pext\ \unit\NM & = \unit\M  \\
\clabel{E3'K_o} \pext\ (\ext\NM\ g \oo f) & = \ext\NM\ g \oo pext\ f  
\end{align*}
% Note that in view of \eqref{EC}, \eqref{E3'K_o} and \eqref{E3K}
% are equivalent, and that \eqref{E2K} and \eqref{E3K} give that 
% \pext\ is a functor from \KNM\ to \KM. 
\unit\NM\ and \pext\ are the unit and extension functions
of a monad \emph{in} the category \KM, whose Kleisli category is also \KNM.
  }

\frame
{
  \frametitle{Compound Monads --- Distributive Law}
Jones \& Duponcheel: two conditions, J(1) and J(2), \\
which compound monads may satisfy.

~ 

Assuming $\unit\NM = \unit\M \oo \unit\N$ and $\map\NM = \map\M \oo \map\N$, \\
compound monads arise from a function \pext\
iff J(1) holds 

~

Compound monads satisfying J(1) and J(2) are those arising from a 
\alert{distributive law} $\swap : N M \alpha \to M N \alpha$ \\
A {distributive law} satisfies S(1) to S(4) of Jones \& Duponcheel

$$\swap = \pext\ (\map\M\ \unit\N)$$
  }

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

~

Arises from a distributive law: $\swap = \pext\ (\map\M\ \unit\N)$, so
$$\swap\gc : \TorN\ \set\ \alpha \to \set\ \TorN\ \alpha$$
\begin{align*}
\swap\gc\ \NonTerm & = \{\NonTerm\} \\
\swap\gc\ (\Term\ S) & = \{\Term\ s \,|\, s \in S\}
\end{align*}
  }

\subsection{The Total Correctness Compound Monad} \label{s-tcmon}
\comment% simplified slide follows \frame
{
  \frametitle{The Total Correctness Compound Monad}

Recall \tcres\ = \TorN\ \set\ \state. 
\begin{align*}
\unit\tc & : \state \to \tcres \notag \\[-0.5ex]
  \prodd\tc & : \set\ \tcres \to tcres \notag \\[-0.5ex]
  \pext\tc & : (\state \to \tcres) \to \set\ \state \to \tcres \notag \\[-0.5ex]
  \ext\tc & : (\state \to \tcres) \to \tcres \to \tcres \notag  \\
\unit\tc\ s & = \Term\ \{s\} \\[-0.5ex]
 \prodd\tc\ S & = \NonTerm  \qquad \mbox{if $\NonTerm \in S$}\\[-0.5ex]
  \prodd\tc\ \{\Term\ s \,|\, s \in S\} & = 
    \Term\ (\textstyle \bigcup S) \\[-0.5ex]
 \pext\tc\ A\ S & = \prodd\tc\ \{A\ s \,|\, s \in S\} \\[-0.5ex]
 \ext\tc\ A\ S & = \ext\nt\ (\pext\tc\ A)\ S
\end{align*}
  }

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

\frame
{
  \frametitle{The Total Correctness Compound Monad}
  \framesubtitle{A Distributive Law and Monad Morphism}
Total Correctness monad also arises from a distributive law: 
\begin{align*}
\swap\tc & : \set\ \TorN\ \sigma \to \TorN\ \set\ \sigma \notag \\
 \swap\tc\ S & = \NonTerm  \qquad \mbox{if $\NonTerm \in S$}\\[-0.5ex]
  \swap\tc\ \{\Term\ s \,|\, s \in S\} & = \Term\ S 
\end{align*}
  }

\subsection{Relating the General and Total Correctness monads}
\frame
{
  \frametitle{Relating the General and Total Correctness monads}
$\swap\tc : \set\ \TorN\ \sigma \to \TorN\ \set\ \sigma$
is also a \alert{monad morphism} \\
from the {general correctness} monad to the {total correctness} monad.
\begin{align*}
\unit\tc\ a & = \swap\tc\ (\unit\gc\ a) \\[-0.5ex]
\ext\tc\ (\swap\tc \oo f)\ (\swap\tc\ x) & = \swap\tc\ (\ext\gc\ f\ x) 
\end{align*}
Since it is \emph{surjective}, 
could use 
 monad axioms for {general correctness} monad to prove
 axioms for {total correctness} monad.
  }

\subsection{The Chorus Angelorum Monad} \label{s-chmon}
\frame
{
  \frametitle{The Chorus Angelorum Monad}
  \framesubtitle{up-closure, swapping angel and demon}
Result $\As : \set\ \set\ \state$ (up-closed): \\
angel chooses $A \in \As$, demon chooses $a \in A$. \\[1ex]

Alternative model: demon chooses first, then angel. \\[1ex]

\swap\uc\ turns 
angel-chooses-first result into 
demon-chooses-first. \\[1ex]

\ucl: the \emph{up-closure} of a set of sets.
\begin{align*}
\swap\uc\ \As & = \{B \,|\, \forall A \in \As.\ B \cap A \not= \{\}\}
\\[-0.5ex]
\ucl\ \As & = \{A' \,|\, \exists A \in \As.\ A \subseteq A'\} 
\end{align*}
\pause
\begin{align*}
\ucl\ (\ucl\ \As) & = \ucl\ \As &
\swap\uc\ (\swap\uc\ \As) & = \ucl\ \As \\[-0.5ex]
\swap\uc\ (\ucl\ \As) & = \swap\uc\ \As &
\ucl\ (\swap\uc\ \As) & = \swap\uc\ \As 
\end{align*}
So work on equivalence classes of sets of sets of states \\
$\As \equiv \As'$ iff $\ucl\ \As = \ucl\ \As'$ \\
each equivalence class has exactly one up-closed member.

  }

\frame
{
  \frametitle{The Chorus Angelorum Monad}
  \framesubtitle{proofs of monad rules}
\begin{itemize}
\item
try to prove S(1) to S(4) (to show distributive law): \\
cannot, but we can prove them modulo up-closure, eg
\begin{align}
% \swap\uc \oo \map\s\ (\map\s\ f) & = \ucl \oo \map\s\ (\map\s\ f) \oo \swap\uc
  % \label{S1'} \tag*{S(1)$'$} \\[-0.5ex]
\swap\uc\ {A} & = \ucl\ (\map\s\ \unit\s\ A) 
  \label{S2'} \tag*{S(2)$'$} \\[-0.5ex]
\swap\uc\ (\map\s\ \unit\s\ A) & = \ucl\ {A}
  \label{S3'} \tag*{S(3)$'$} % \\[-0.5ex]
% \prodd\uc \oo \map\s\ \dorp\uc\ & = \dorp\uc \oo \prodd\uc \tag*{S(4)}
% \\
% \swap\uc \oo \map\s\ \join\s & = \dorp\uc \oo \swap\uc \tag*{(D3)} \\[-0.5ex]
% \swap\uc \oo \join\s & = \prodd\uc \oo \map\s\ \swap\uc \tag*{(D4)} 
\end{align}

\item proofs of the monad axioms for $\set\ \set\ \alpha$ \\
(again, some equalities only modulo up-closure) \\
difficult, but imitated usual proofs from S(1) to S(4)

\item defined type $\ucss\ \alpha$ :
\emph{up-closed} sets of sets \\
(ie, a representative of each equivalence class)

\item
defined the monad functions for the $\ucss\ \alpha$ type 
\item
translated results about $\set\ \set\ \alpha$ 
to $\ucss\ \alpha$: it is a monad!
\end{itemize}
  }

\frame
{
  \frametitle{The Chorus Angelorum Monad}
  \framesubtitle{Link to Continuation Monad}
First, recall functions used by Jones \& Duponcheel
\begin{align*}
\join & : M\ N\ M\ N\ \alpha \to M\ N\ \alpha &
\prodd & : N\ M\ N\ \alpha \to M\ N\ \alpha \\[-0.5ex]
\dorp & : M\ N\ M\ \alpha \to M\ N\ \alpha &
\swap & : N\ M\ \alpha \to M\ N\ \alpha 
\end{align*}
Think of $M$ ($N$) as a set from which angel (demon) chooses.
\\[1ex]

``evaluation function'' 
$\evaluc : \set\ \set\ \alpha \to (\alpha \to \bool) \to \bool$,
\\[1ex]
$\evaluc\ \As\ P$ tells whether the post-condition $P$ is satisfied when
angel and demon have made their choices from \As.
\\[1ex]
$\evaluc\ \Bs\ P \equiv \exists B \in \Bs.\ \forall b \in B.\ P\ b$.
\\[1ex]
$(\alpha \to \bool) \to \bool$ is type of \alert{continuation}
monad $K\ \alpha$ 
\\[1ex]
\Ball\ and \Bex : $\set\ \alpha \to (\alpha \to \bool) \to \bool$,
ie : $\set\ \alpha \to K\ \alpha$ \\
express quantification over a given set:
$\Ball\ S\ P \equiv \forall s \in S.\ P\ s$
  }

\frame
{
  \frametitle{The Chorus Angelorum Monad}
  \framesubtitle{Link to Continuation Monad -- ctd}
\begin{align*}
  \evaluc & = \Ball \odot_K \Bex \\
 \evaluc \oo \swap\uc & = \Bex \odot_K \Ball
\end{align*}
Using obvious isomorphism $K\ \alpha \to \set\ \set\ \alpha$, called \ktoss:
\begin{align*}
\join\uc & = \ktoss \oo (\Ball \odot_K \Bex \odot_K \Ball \odot_K \Bex)
\\[-0.5ex]
\dorp\uc & = \ktoss \oo (\Bex \odot_K \Ball \odot_K \Bex) \\[-0.5ex]
\prodd\uc & = \ktoss \oo (\Ball \odot_K \Bex \odot_K \Ball) \\[-0.5ex]
\swap\uc & = \ktoss \oo (\Bex \odot_K \Ball) \\[-0.5ex]
\ext\uc\ f & = \ktoss \oo 
  (\Ball \odot_K (\Bex \oo f) \odot_K \Ball \odot_K \Bex) \\[-0.5ex]
\pext\uc\ f & = \ktoss \oo (\Ball \odot_K (\Bex \oo f) \odot_K \Ball) 
% \\ f \odot_{uc} g & = \ktoss \oo ((\evaluc \oo f) \odot_K (\evaluc \oo g))
\end{align*}
  }

\subsection{Definition of Choice} \label{s-defs}
\comment% \frame
{
  \frametitle{Definition of the choice command}
Defining by weakest precondition: \\
conjunction of individual weakest preconditions.
\\[1ex]
General Correctness: $\choice\gc\ \Cs\ s = \bigcup_{C \in \Cs} C\ s$. 
\\[1ex]
Total Correctness: \\
\choice\tc\ $\Cs$ can fail to terminate 
if any $C \in \Cs$ can fail to terminate.
\\[1ex]
$\choice\tc\ \Cs\ s  = \pext\tc\ (\lambda C.\ C\ s)\ \Cs$, expands to  
\begin{itemize}
\item
if $\{C\ s \,|\, C \in \Cs\}$ contains \NonTerm\ then 
$\choice\tc\ \Cs\ s = \NonTerm$
\item
if $\{C\ s \,|\, C \in \Cs\} = \{\Term\ S_C \,|\, C \in \Cs\}$,
then $\choice\tc\ \Cs\ s = \Term\ (\bigcup_{C \in \Cs} S_C)$
\end{itemize}

  }

\frame
{
  \frametitle{Angelic and Demonic Choice}
We defined these as follows (simplified by \\
\begin{itemize}
\item omitting conversion between the
$\set\ \set\ \alpha$ and $\ucss\ \alpha$ types
\item assuming up-closed families of sets)
\end{itemize}
\begin{align*}
\dem\ \Bs\ s & = \textstyle \bigcap\ \{B\ s\ |\ B \in \Bs\} \\
\ang\ \Bs\ s & = \textstyle \bigcup\ \{B\ s\ |\ B \in \Bs\}
\end{align*}
giving these results (which would normally be the definitions)
\begin{align*}
[\dem\ \Bs]\ Q\ s & = \forall B \in \Bs.\ [B]\ Q\ s \\
[\ang\ \Bs]\ Q\ s & = \exists B \in \Bs.\ [B]\ Q\ s \\[1ex]
\end{align*}
  }

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

\frame
{
  \frametitle{Examples of beamer use}
\begin{block}{title}
block
\end{block}
  \begin{itemize}
  \item<1-2> Normal LaTeX class.
  \item<3-4> \emph{Easy} \alert{overlays}.
  \item<2-3> No external programs needed.      
  \end{itemize}
\color<2-3>{green} green
\color<1-2>{blue} blue
}
    


