\Section{$\wCPO$-enriched \cbpv{} models}
\cats{}We turn to incorporate recursion into \cbpv{}.
The following notion appears in Levy's work~\cite{levy:thesis,
  levy:cbpv-book}:
\begin{definition}
  Let $\Monad$ be a strong monad over a cartesian category $\ValCat$,
  let $\Algebra$, $\Algebra'$ in $\Obj{\smash{\AlgebraCat\ValCat\Monad}}$
  be two algebras, and let $\mG\inObj\ValCat$ be any $\ValCat$-object.
  A \defterm{$\Monad$-algebra homomorphism from $\Algebra$ to
    $\Algebra'$ over $\mG$} is a morphism $h \of
  \mG\times\carrier\Algebra\to \carrier{\Algebra'}$, satisfying:
  \inlinediagram{homomorphism-over-object-def-01}
\end{definition}

We will make use of the following properties of algebras:
\begin{lemma}\lemmalabel{homomorphism lemma}
Let $\Monad$ be a strong monad over a cartesian category $\ValCat$,
and $\Algebra$, $\Algebrav$ be any $\Monad$-algebras.
\begin{enumerate}
\item\label{homomorphism lemma: generalisation} If $h \of \Algebra \to \Algebrav$ is a $\Monad$-algebra homomorphism in
  the usual sense, then, for all $\mG$, the following morphism is an
  algebra homomorphism over $\mG$:
  \[
  \mG\times\carrier\Algebra \xto{\proj2}\carrier\Algebra\xto{h}\carrier{\Algebrav}
  \]
\item\label{homomorphism lemma: exponential}If the exponential $\carrier{\Algebrav}^{\mG}$ exists in $\ValCat$,
  then there is a $\Monad$-algebra structure over
  $\carrier{\Algebrav}^{\mG}$, denoted by ${\Algebrav}^{\mG}$, given by:
  \[
  \ilam\mG{\parent{\Monad(\carrier{\Algebrav}^{\mG})\times\mG
    \xto{\costrength}
    \Monad(\carrier{\Algebrav}\times\mG)
    \xto{\Monad\eval}
    \Monad\carrier{\Algebrav}
    \xto{\algebra[\Algebrav]}
    \carrier{\Algebrav}}}
  \]
  In this case, every algebra homomorphism over $\mG$, ${h
  \of \mG\times \carrier\Algebra \to \carrier{\Algebrav}}$, gives rise
  to a (unique) algebra homomorphism from $\Algebra$ to ${\Algebrav}^{\mG}$:
  \[
  \ilam{\mG}{\parent{\carrier\Algebra\times\mG \xto{\swap}
      \mG\times\carrier\Algebra\xto{h} \carrier{\Algebrav}}}
  \]
\item\label{homomorphism lemma: lifting} For all morphisms $f \of
  \mG\times\mV\to\carrier\Algebra$, the lifting $\lifting f \of
  \mG\times\Monad\mV\to\carrier\Algebra$ is the unique
  $\Monad$-algebra homomorphism from $\F\mV$ to $\Algebra$ over $\mG$,
  satisfying
  \inlinediagram{homomorphism-lemma-proof-04}
\end{enumerate}
\end{lemma}

\begin{proof}
  The following diagram proves part~\ref{homomorphism lemma: generalisation}:
  \inlinediagram{homomorphism-lemma-proof-01}

  In part~\ref{homomorphism lemma: exponential}, the fact that
  $\Algebrav^{\mG}$ is a $\Monad$-algebra is well-known, and follows
  by routine calculation.
  The fact that $\ilam\mG{\parent{h\compose\swap}}$ is a homomorphism follows, by the
  exponential universal property, from the following diagram:
  \inlinediagram{homomorphism-lemma-proof-02}
  The uniqueness proof is also straightforward, but we omit it, as we will not make
  use of it in the sequel.

  Finally, the following diagram proves part~\ref{homomorphism lemma: lifting}:
  \inlinediagram{homomorphism-lemma-proof-03}
  Straightforward calculation shows that
  \inlinediagram{homomorphism-lemma-proof-04}
  and that $\lifting f$ is the unique such homomorphism, but we omit
  these calculations as we will not make use of them in the sequel.
\end{proof}

\begin{definition+}{\recursion{definition}{cbpv model}}
  An \defterm{\DELTA{$\wCPO$-enriched} (Eilenberg-Moore) \cbpv{} model} is a pair
  $\seq{\ValCat, \Monad}$ where:
  \begin{itemize}
  \item $\ValCat$ is a\DELTA{n $\wCPO$-enriched} distributive
  category;
  \item $\Monad$ is a\DELTA{n $\wCPO$-enriched} strong monad over
    $\ValCat$; and
  \item $\ValCat$ has all \DELTA{$\wCPO$-enriched} exponentials
    ${\carrier\Algebra}^{\mV}$ of all $\Monad$-algebra carriers $\carrier\Algebra$ by all
    objects $\mV$ in $\ValCat$.
  \end{itemize}

  A   \defterm{recursion \cbpv{} model} is an $\wCPO$-enriched model
  $\pair\ValCat\Monad$ for which:
  \begin{itemize}
  \item for all objects $\mG \inObj
  \ValCat$ and algebras
  $\Algebra\inObj{\AlgebraCat\ValCat\Monad}$,
  $\homset[\ValCat]{\mG}{\carrier{\Algebra}}$ is pointed; and,
  \item for all $f
  \of \mGv \to \mG$ in $\ValCat$ and homomorphisms $h$ from $\Algebra$
  to $\Algebrav$ over $\mG$:
  \begin{align*}
    \bot_{\mG,\Algebra} \compose f = \bot_{\mGv, \Algebra}&&
    h\compose\prodmorphism\mG{\bot_{\mG,\Algebra}} = \bot_{\mG,\Algebrav}
  \end{align*}
  \end{itemize}
\end{definition+}

\begin{example}\examplelabel{enriched exceptions and IO}
  Recall the collection of monads $\Monad_{\placeholder}$ for
  exceptions and terminal
  I/O from \exampleref{exceptions-and-IO}, and let $\e \subset
  \set{\raiseop, \inputop, \outputop}$ be any effect set.
  If $\mW$ is an \wcpo{}, then $\Monad_{\e}\carrier\mW$ inherits an \wcpo{}
  structure, by inductively taking the smallest partial order satisfying:
  \begin{itemize}
  \item if $\mw \leq \mw'$ in $\mW$
    then $\mw \leq_{\Monad_{\e}\mW} \mw'$;
  \item if $\inputop \in \e$, and for all $\mchar \in \Char$,
    $\mterm_{\mchar}\leq_{\Monad_{\e}\mW}\mterm'_{\mchar}$, then
    \[
    \pair I{\seq[\mchar\in\Char]{\mterm_{\mchar}}}
    \leq_{\Monad_{\e}\mW} \pair
      I{\seq[\mchar\in\Char]{\mterm'_{\mchar}}}
      \]
    \item if $\outputop \in \e$, $\mchar \in \Char$, and $\mterm \leq
      \mterm'$, then
      \[
      \triple O\mchar{\mterm} \leq_{\Monad_{\e}\mW} \triple O\mchar{\mterm'}
      \]
  \end{itemize}

  As trees, two elements of $\Monad_{\e}\mW$ are comparable if they
  have the same shape, and corresponding leaves are compatibly
  comparable in $\mW$. Thus, an $\omega$-chain of such trees is a sequence
  of trees with the same shape, whose corresponding leaves form
  $\omega$-chains.  Hence, the suprema of such an $\omega$-chain is the
  same tree, with the suprema of each leaf $\omega$-chain in its corresponding
  leaf.

  The monadic structure of $\Monad_{\e}$ is
  $\wCPO$-enriched, and $\pair{\wCPO}{\Monad_{\e}}$ is an
  $\wCPO$-enriched \cbpv{} model.
  %
  If $\mW$ is not pointed, then clearly $\Monad_{\e}\mW$ is not
  pointed. Therefore this model is not a recursion model.
\end{example}

\begin{example}\examplelabel{lifting monad}
  The \defterm{lifting monad} $\LiftingMonad$ is given by
  \[
  \begin{array}{*{1}{r@{\ }l@{\ }l@{\ }l}@{\qquad}*{2}{l@{}}@{\ }l@{}l}
  \carrier{\LiftingMonad \mW} &\definedby&
  \multicolumn{2}{l}{\set{\bot}+\carrier{\mW}} &\multicolumn{2}{r}{\mw \leq \mw'}  &\!\!\!\iff &\mw= \inj1\bot\text{, or } \\
  \LiftingMonad f             &\definedby& \multicolumn{2}{l}{\set{\bot}+f }           &&              &&\mw=\inj2\hat\mw,\mw'=\inj2\hat\mw' \text{, and } \hat\mw\leq_{\mW}\hat\mw'\\
  \unit                       &\of       & \mw &\mapsto \inj2\mw          & \monmult \of \inj1     &\bot  &\mapsto \inj1&\bot \\
   \strength[\mW\mWv] &\of& \pair\mw{\inj1\bot}&\mapsto \inj1\bot         & \monmult \of \inj2\inj1&\bot  &\mapsto \inj1&\bot \\
  \strength[\mW\mWv] &\of& \pair\mw{\inj2\mw}  &\mapsto \inj2\pair\mw\mwv & \monmult \of \inj2\inj2&\mw   &\mapsto \inj2&\mw
\end{array}
\]
Note that a monad $\Monad$ is strict if and only if there is a monad
morphism $\LiftingMonad \to \Monad$.

The morphism map \[
\LiftingMonad = \set{\bot}+\placeholder = \coprodmorphism{\inj1}{\inj2\compose\placeholder}
\] is continuous, hence $\LiftingMonad$ is an $\wCPO$-enriched strong monad. Thus $\pair\wCPO\LiftingMonad$ is an $\wCPO$-enriched \cbpv{} model.

The $\LiftingMonad$-algebras are precisely the pointed
\wcpo{}s. Indeed, let $\Algebra$ be any $\LiftingMonad$-algebra.
By fiat, $\inj1\bot$ is the least element of $\LiftingMonad\carrier\Algebra$. Thus, for all $\malg\in\carrier{\carrier{\Algebra[{\mW}]}}$ :
\[
\algebra[{\Algebra[{\mW}]}][\inj1\bot]
\explain\leq{$\algebra[{\Algebra[{\mW}]}]$-continuity}
\algebra[{\Algebra[{\mW}]}][\inj2\mw] = \algebra[{\Algebra[{\mW}]}][\unit(\mw)] \explain={algebra} \mw
\]
We have shown that every $\LiftingMonad$-algebra is pointed. Therefore,
$\mg\mapsto\algebra[{\Algebra[{\mW}]}][\inj1\bot]$ is the least element of
$\homset[\wCPO]{\mG}{\carrier{\Algebra[{\mW}]}}$. Conversely, if $\mW$
is pointed with a least element $\bot_{\Algebra[\mW]}$ then the algebra structure over $\mW$ is given by
\[
\algebra[{\Algebra[{\mW}]}][\mw] \definedby
\begin{cases}
  \bot_{\Algebra[\mW]} & \mw = \inj1 \bot \\
  \mw' & \mw = \inj2 \mw
\end{cases}
\]

If $f \of \mGv \to \mG$, then $\bot_{\mG,\Algebra}(f(\mgv)) = \algebra[{\Algebra[{\mW}]}][\inj1\bot] = \bot(\mgv)$,
hence $\bot \compose f = \bot$.  Let $h$ be a homomorphism from
$\carrier{{\Algebra[{\mWv}]}}$ to $\carrier{\Algebra[{\mW}]}$ over $\mG$. By the
definition of homomorphisms over $\mG$, we have:
\inlinediagram{chasing-lifting-01}
Thus, $h\compose\prodmorphism\mG\bot = \bot$.
In conclusion, we have a recursion \cbpv{} model.
\end{example}

In light of \lemmaref{homomorphism lemma}, we can replace the
condition on homomorphisms over objects with homomorphisms in the
usual sense:
\begin{theorem}\theoremlabel{recursion models via standard homomorphisms}
  Let $\pair\ValCat\Monad$ be an $\wCPO$-enriched \cbpv{} model. It is
  a recursion model if and only if:
  \begin{itemize}
  \item for all objects $\mG\inObj\ValCat$
    and algebras $\Algebra\inObj*{\AlgebraCat\ValCat\Monad}$,
    $\homset[\ValCat]\mG{\carrier\Algebra}$ is pointed; and
  \item for all $f
    \of \mGv \to \mG$ and homomorphisms $h$ from $\Algebra$ to
    $\Algebrav$:
    \[
    \bot_{\mG, \Algebra}\compose f = \bot_{\mGv,\Algebra}
    \qquad
    h \compose \bot_{\mG, \Algebra} = \bot_{\mG,\Algebrav}
    \]
  \end{itemize}
\end{theorem}

\begin{proof}%
  We show that the two homomorphism conditions are equivalent:
  \begin{enumerate}
  \item[$\implies$]Take any object $\mG \inObj \ValCat$ and homomorphism $h$ from $\Algebra$
    to $\Algebrav$ in the usual sense.  By \lemmaref{homomorphism lemma}(\ref{homomorphism lemma:
    generalisation}), $h \compose \proj2$ is a homomorphism from
    $\Algebra$ to $\Algebrav$ over $\mG$, hence:
    \[
    \bot = (h \compose \proj2) \compose \prodmorphism\mG\bot = h
    \compose \bot
    \]
  \item[$\impliedby$]Take any object $\mG\inObj\ValCat$ and homomorphism $h$ from
    $\Algebra$ to $\Algebrav$ over $\mG$. As $\pair{\ValCat}\Monad$ is
    an $\wCPO$-enriched $\cbpv{}$, the $\wCPO$-enriched exponential
    $\carrier\Algebrav^{\mG}$ exists in $\ValCat$. By \lemmaref{homomorphism
      lemma}(\ref{homomorphism lemma: exponential}),
    $\ilam\mG{(h\compose\swap)}$ is an algebra homomorphism from
    $\Algebra$ to $\Algebrav^{\mG}$, therefore:
    \[
    (\ilam\mG{(h\compose\swap)})\compose \bot_{\mG,\Algebra} = \bot_{\mG,\carrier\Algebrav^{\mG}}
    \explain={\lemmaref{pointed functionspace}}
    \ilam\mG{\bot_{\mG\times\mG,\carrier\Algebrav}}
    \of \terminal \to \carrier{\Algebrav}^{\mG}
    \tag{$*$}
    \]
    The commutativity of the following diagram completes the proof:
    \inlinediagram{recursion-model-lemma-proof-01}
  \end{enumerate}
  \vspace{-1.5\baselineskip}
\end{proof}

\begin{example}\examplelabel{exceptions and recursion}
We present a recursion model for exception raising computations.

Let $\Monad_{\set\raiseop}$ be the monad for exception raising from
\exampleref{enriched exceptions and IO}, and $\LiftingMonad$ the
lifting monad from \exampleref{lifting monad}. Define $\Monad
\definedby \LiftingMonad\compose\Monad_{\set\raiseop}$.  Let $\mW$ be
any $\wCPO$, then
\[
\carrier{\Monad\mW} = \set{\bot} + \String + \carrier\mW
\]
and the \wcpo{} structure is given by $\mx \leq\my$ if and only if either:
\begin{enumerate}
\item[($\bot$).] \label{exception recursion example: bottom case} $\mx = \bot$; or
\item[(raise).] $\mx = \my = \pair R\mstring$, $\mstring\in\String$; or
\item[($\mW$)] $\mx = \mw\in\mW$, $\my = \mwv\in\mW$ and $\mw \leq \mwv$.
\end{enumerate}
and suprema are given by:
\[
\lub \mx_n =
\begin{cases}
  \bot & \text{for all $n$, $\mx_n = \bot$}\\
  \pair R\mstring & \text{for some $n_0$, for all $n \geq n_0$, $\mx_n = \pair
    R\mstring$}\\
  \lub\mw_n & \text{for some $n_0$, for all $n \geq n_0$, $\mx_n = \mw_n \in \mW$}
\end{cases}
\]

Consider $\Monad_{\set\raiseop}\compose\LiftingMonad\mW$. Its carrier
set is also $\set{\bot} + \String + \carrier\mW$, and the \wcpo{}
structure is given by $\mx\leq \my$ iff either:
\begin{enumerate}
\item[(raise).]   $\mx = \my = \pair R\mstring$, $\mstring\in\String$; or
\item[($\bot'$\/).]   $\mx = \bot$, $\my = \mw \in \mW$; or
\item[($\mW$).]   $\mx = \mw\in\mW$, $\my = \mwv\in\mW$ and $\mw \leq \mwv$.
\end{enumerate}
and least upper bounds given by:
\[
\lub \mx_n =
\begin{cases}
  \pair R\mstring & \text{for some $n_0$, for all $n \geq n_0$, $\mx_n = \pair
    R\mstring$, for some $n_0$}\\
  \bot & \text{for all $n$, $\mx_n = \bot$}\\
  \lub\mw_n & \text{for some $n_0$, for all $n \geq n_0$, $\mx_n = \mw_n \in \mW$}
\end{cases}
\]
Therefore, the map $\lam\mx\mx$ from
$\Monad_{\set\raiseop}\compose\LiftingMonad\mW$ to
$\LiftingMonad\compose\Monad_{\set\raiseop}\mW$ is continuous.  Direct
calculation shows it yields a distributive law of $\LiftingMonad$
over $\Monad_{\set\raiseop}$.

Thus, $\Monad$ has a strong monad structure, given by the inclusion
$\unit \of \mW \subset\Monad\mW$ and
\begin{mapdef*}[3]
\monmult &\of \bot            &\mapsto \bot            &\qquad&&& \strength &\of \pair \mg\bot              &\mapsto \bot \\
\monmult &\of \pair R\mstring &\mapsto \pair R\mstring &\qquad&&& \strength &\of \pair \mg{\pair R\mstring} &\mapsto \pair R\mstring\\
\monmult &\of \mx             &\mapsto \mx             &\qquad&&& \strength &\of \pair \mg\mw               &\mapsto \pair\mg\mw
\end{mapdef*}

If $\Algebra$ is any $\Monad$-algebra, then $\carrier\Algebra$ is
pointed, with $\algebra[\Algebra][\bot]$ the least element.
Therefore, $\homset[\wCPO]\mG{\carrier\Algebra}$ is pointed with
$\lam\mg\bot$ the least element.

Given any function $f \of \mGv\to\mG$ and $\Monad$-algebra
homomorphism $h \of \Algebra\to\Algebrav$, we have:
\[
(h\compose(\lam\mg\bot)\compose f)(\mgv) = h(\bot) =
h(\algebra[\Algebra][\bot]) \explain={$T$-algebra homomorphism}
\algebra[\Algebrav][(\Monad h)(\bot)] = \algebra[\Algebrav][\bot]
\]
hence $h\compose\bot\compose f = \bot$, and, by \theoremref{recursion
  models via standard homomorphisms}, $\pair\wCPO\Monad$ is a
recursion model.
\end{example}

Finally, we define our category of \cbpv{} models:

\begin{definition+}{\recursion{definition}{adjV}}
  Let $\ValCat$ be an $\wCPO$-enriched distributive category. The category $\wCPOAdjunctions
  \ValCat$ has as \textbf{objects} \cbpv{} models with
  $\F\leftadjointto\U\of\CompCat\to\ValCat$, and as \textbf{morphisms}
  $(\F_1 \leftadjointto \U_1)\to(F_2\leftadjointto \U_2)$ strong monad
  morphisms $\MonadMorphism \of \Monad_1 \to \Monad_2$.
\end{definition+}

\inlinediagram{butterfly-01}
\pagebreak

\Section{$\wCPO$-enriched algebraic operations}
\cats{}In the $\wCPO$-enriched case, enriched algebraic operations coincide with the ordinary ones:
\begin{definition+}{\recursion{definition}{alg ops}
    (\textnormal{enriched algebraic operations})}
Let $\F \leftadjointto \U \of \CompCat \to \ValCat$ be an $\wCPO$-enriched resolution of
an $\wCPO$-enriched strong monad $\Monad = \U\F$, and $\Ar$,$\Pa$ be $\ValCat$ objects
such that all $\wCPO$-enriched exponentials of objects $\U\mC$ by
$\Ar$,$\Pa$ exist.
%
An \defterm{$\wCPO$-enriched algebraic operation of type $\arity{\Ar}{\Pa}$} for $\F
\leftadjointto \U$ is an an algebraic operation for the underlying
ordinary resolution $\F\leftadjointto\U$.
\end{definition+}
Similarly, the definition of an enriched monad morphism mapping an
enriched operation to an enriched operation coincides with its ordinary
counterpart.

\begin{example}\examplelabel{lifting monad}
Consider the lifting monad $\LiftingMonad$ from \exampleref{lifting
  monad}. Given any $\LiftingMonad$-algebra $\Algebra$, define:
\begin{mapdef*}
  \bot_{\Algebra}&\of\Algebra^{\initial} &\to      \Algebra^{\terminal} \\
  \bot_{\Algebra}&\of\unitval          &\mapsto \lam\unitval\bot
\end{mapdef*}%
To see that $\bot$ is an algebraic operation of type $\bot \of
\initial$, consider any $f \of \mG\times\mW\to\carrier\Algebra$.
By \lemmaref{homomorphism lemma}(\ref{homomorphism lemma: lifting}),
$\lifting f \of \mG\times\LiftingMonad\mW \to \carrier\Algebra$ is a
homomorphism over $\mG$. As $\pair\wCPO\LiftingMonad$ is a recursion
model, we deduce that $\lifting f(\mg,\bot) = \bot$ for every $\mg \in
\mG$. Therefore:
\inlinediagram{chasing-lifting-02}
Hence $\bot \of \initial$ is an $\wCPO$-enriched algebraic operation
for $\LiftingMonad$.
\end{example}

The argument in the last example can be generalised to arbitrary
recursion models:
\begin{lemma}\lemmalabel{divergence operation}
  Let $\pair\ValCat\Monad$ be a recursion model. Then there is an
  algebraic operation $\divergeop \of \initial$ for the Eilberg-Moore
  resolution of $\Monad$, given
  by:
  \[
  \divergeop_{\Algebra} \definedby
  \ilam\terminal{\bot_{\carrier\Algebra^{\initial}\times\terminal}} \of \carrier\Algebra^{\initial}\to\carrier\Algebra^{\terminal}
  \]
  The corresponding generic effect is then given by
  \[
  \generic{\divergeop} \definedby \bot_{\terminal,\F\initial} \of
  \terminal \to \Monad\initial
    \]
\end{lemma}

\begin{proof}%
  As $\pair\ValCat\Monad$ is a recursion model,
  $\homset[\ValCat]\terminal{\Monad\initial}$ is pointed, hence the generic
  operation
  \[
    \mgen \definedby \bot_{\terminal,\F\initial} \of
  \terminal \to \Monad\initial
  \]
  is well-defined. Define $\divergeop \definedby \operation{\mgen}{}$ and
  obtain, by \theoremref{operations-vs-effects}, an algebraic operation $\divergeop \of \initial$ satisfying:
  $\generic\divergeop = \bot$.  Note that the enriched model structure
  guarantees $\divergeop$ is an enriched operation.

  Let $\Algebra$ be any algebra. We have:
  \inlinediagram{bottom-effect-operation-proof-01}
  Thus, by \theoremref{operations-vs-effects},
  \(\divergeop_{\Algebra} =
  \ilam\terminal{\bot_{\carrier\Algebra^{\initial}\times\terminal}}
  \), and we are done.
\end{proof}

\begin{example}\examplelabel{exceptions and IO operations}Recall the monads for exceptions and terminal I/O from
  \exampleref{enriched exceptions and IO}. Using
  \theoremref{operations-vs-effects} we obtain enriched algebraic operations
  for $\Monad_{\e}$:
  \begin{itemize}
  \item if $\raiseop \in \e$:
    \begin{mapdef*}
      \raiseop &\of \initial\\
      \raiseop_{\Algebra} &\of \unitval &\mapsto \lam\mstring{\algebra[\Algebra][\pair R\mstring]}
    \end{mapdef*}
  \item if $\inputop \in \e$:
    \begin{mapdef*}
      \inputop &\of \Char \\
      \inputop_{\Algebra} &\of \lam\mchar{\malg_{\mchar}} &\mapsto
      \lam\unitval{\algebra[\Algebra][\pair
          I{\seq[\mchar\in\Char]{\malg_{\mchar}}}]}
    \end{mapdef*}
  \item if $\outputop \in \e$:
    \begin{mapdef*}
      \outputop &\of \arity\terminal\Char \\
      \outputop_{\Algebra} &\of \lam\unitval\malg &\mapsto
      \lam\mchar{\algebra[\Algebra][\triple O\mchar\malg]}
    \end{mapdef*}
  \end{itemize}

  For each $\e \subset \e'$, the inclusions are continuous.
\end{example}

The following definition ties all the previous concepts together:
\begin{definition+}{\recursion{definition}{non-hierarchical cbpv model}}
  Let $\Opset$ be a set. An \defterm{\DELTA{$\wCPO$-enriched} \cbpv{}
    $\Opset$-model} is a quadruple
  \[
  \seq{\ValCat,\arities,\Monad,\opsem[]\placeholder}
  \] where:
  \begin{itemize}
  \item $\ValCat$ is a\DELTA{n $\wCPO$-enriched} distributive category, called the
    \defterm{value category};
  \item $\arities$ is a type assignment for $\Opset$ in
    $\ValCat$;
  \item $\pair\ValCat\Monad$ is a\DELTA{n $\wCPO$-enriched} \cbpv{} model; and
  \item $\opsem[]\placeholder$ assigns to every $\mop \of
    \arity\Ar\Pa$ in
    $\Opset$ an \DELTA{$\wCPO$-enriched} algebraic operation $\opsem[]\mop \of
    \arity\Ar\Pa$ for $\Monad$.
  \end{itemize}

  \noindent
  We say that an $\wCPO$-enriched \cbpv{} $\Opset$-model \(
  \seq{\ValCat,\arities,\Monad,\opsem[]\placeholder}
  \) is a
  \defterm{recursion \cbpv{} $\Opset$-model} if $\Opset$ has a
  distinguished effect operation $\divergeop$ such that:
  \begin{itemize}
  \item $\pair\ValCat\Monad$ is a \cbpv{} recursion model; and
  \item $\opsem[]\divergeop$ is the divergence operation (see
    \lemmaref{divergence operation}).
  \end{itemize}
\end{definition+}

\begin{example}
  The monads $\Monad_{\e}$ for
  exceptions and terminal I/O from \exampleref{enriched exceptions and
  IO} give rise to $\wCPO$-enriched $\e$-\cbpv{} models, as
  $\pair{\wCPO}{\Monad_{\e}}$ is an enriched \cbpv{} model (see
  \exampleref{enriched exceptions and IO}), and the operations are
  interpreted as the enriched operations from \exampleref{exceptions
    and IO operations}. This model is not a recursion model.
\end{example}

\begin{example}
  The lifting monad $\LiftingMonad$ gives rise to a
  recursion $\set{\divergeop}$-\cbpv{} model, as
  $\pair\wCPO{\LiftingMonad}$ is a recursion \cbpv{} model (see
  \exampleref{lifting monad}), and we interpret the distinguished (and
  only) $\divergeop$ operation as the divergence algebraic operation.
\end{example}

\pagebreak
\Section{Recursion models}
\cats{}We are finally ready to incorporate recursion into our models for
effect analysis:

\begin{definition+}{\recursion{definition}{cat-type-assignment}}\definitionlabel+{enriched-type-assignment}
  Let $\Signature$ be a recursion hierarchy and $\ValCat$
  an $\wCPO$-enriched distributive category. A
  \defterm{{recursion} $\Signature$-type assignment in
    $\ValCat$} is a $\Signature$-type assignment in the underlying
  ordinary category of $\ValCat$,
  such that $\divergeop \of \initial$, i.e., $\divergeop \of \arity\initial\terminal$.
\end{definition+}

\begin{example}\examplelabel{non-determinism hierarchy}
A recursion type assignment in $\wCPO$ for non-determinism is:
\[
\chooseop  \of \twoobj
\qquad
\divergeop \of \initial
\]
\unhangdisplay
\end{example}

We are now ready to define recursion $\Signature$-models:
\begin{definition+}{\recursion{definition}{categorical-model}}\definitionlabel+{recursion-categorical-model}
Let $\Signature$ be a \DELTA{recursion} hierarchy. A
\defterm{\DELTA{recursion} $\Signature$-model} is a
quadruple \[
\seq{\ValCat, \arities, \Presheaf, \opsem[\placeholder]\placeholder}
\] where:
\begin{itemize}
\item
$\ValCat$ is a\DELTA{n $\wCPO$-enriched} distributive category, called the \defterm{value
  category};
\item
$\arities$ is a \DELTA{recursion} $\Signature$-type assignment in $\ValCat$;
\item
$\Presheaf$ is a functor $\E \to \DELTA{\wCPOAdjunctions\ValCat}$, called the
\defterm{model hierarchy}\DELTA{, such that, for} \DELTA{all $\e\in\E$ with $\divergeop \in \e$,
  $\Presheaf\e$ is a recursion model};
\item
$\opsem[\placeholder]\placeholder$ assigns to each $\e \in \E$ and $\mop
\in \e$, $\mop \of \arity\Ar\Pa$ an \DELTA{(enriched)} algebraic operation $\opsem\mop$
of type $\arity\Ar\Pa$ for $\Presheaf \e$\DELTA{, such that, for all
  $\e \in \E$ with $\divergeop \in \e$,} \DELTA{$\opsem\divergeop$ is the
  divergence operation (see \lemmaref{divergence operation})};
\end{itemize}
and $\Presheaf\parent{\e\subset\e'}$ preserves the operations;
\end{definition+}

\begin{example}
We construct a domain-theoretic model for exceptions, terminal I/O,
and recursion.

To keep this example simple, we choose the recursion hierarchy by setting
$\Opset$ to be $\set{\raiseop, \inputop,
  \outputop, \divergeop}$, and
\[
\E\definedby \Powerset{\set{\raiseop, \inputop,
    \outputop}}\union\Powerset{\set{\divergeop, \raiseop}}
\]
We will extend this model to the full powerset hierarchy in
\sectionref{recursion exception and IO example} (\exampleref+{exceptions-and-IO-and-recursion}).

Take $\Char$ and $\String$ be the discrete \wcpo{}s whose carriers are
the corresponding sets $\Char$ and $\String$ from
\exampleref{exceptions-and-IO}.

The recursion model $\seq{\wCPO, \arities, \Presheaf,
  \opsem[\placeholder]\placeholder}$ is given as follows.

The type assignment is given by
  \begin{align*}
  \raiseop&\of\arity\emptyset\String &\inputop &\of \Char
  &\outputop &\of \arity\terminal\Char
  &{\divergeop }&{\vphantom{\divergeop}\of\initial}
  \end{align*}

Recall the enriched models $\pair{\wCPO}{\Monad_{\placeholder}}$ for exceptions and terminal
I/O from \exampleref{enriched exceptions and IO}, the recursion model
$\pair\wCPO{\Monad_{\set\divergeop}}$ from \exampleref{lifting monad}
given by the lifting monad, and the recursion model
$\pair\wCPO{\Monad_{\set{\raiseop, \divergeop}}}$ for exceptions from \exampleref{exceptions and recursion}.
Note that, for every $\e \subset \e'$ in $\E$, we have a continuous inclusion
\[
\MonadMorphism_{\e\subset\e'} \of \Monad_{\e} \subset \Monad_{\e'}
\]
Thus, by choosing $\Presheaf\e$ to be $\pair\wCPO{\Monad_{\e}}$ and
$\Presheaf(\e\subset\e')$ to be $\MonadMorphism_{\e\subset\e'}$, we
obtain a functor from $\E$ to $\wCPOAdjunctions\wCPO$, and in the
cases where $\divergeop\in\e$, namely $\set{\divergeop}$ and
$\set{\raiseop, \divergeop}$, we have a recursion model.

For every
$\e\in\E$, we define:
\newcommand\eSideCondition[1]{\text{if $#1$}&\text{$\in\e$, define:}&}
\begin{mapdef*}[2]
\eSideCondition\raiseop & \opsem\raiseop_{\Algebra} & \of\unitval
&\mapsto\ilam\mstring{\algebra[\Algebra][\pair R\mstring]} \\
\eSideCondition\inputop & \opsem\inputop_{\Algebra} & \of\lam\mchar{\malg_{\mchar}}
&\mapsto\ilam\unitval{\algebra[\Algebra][\pair I{\seq[\mchar\in\Char]{\malg_{\mchar}}}]} \\
\eSideCondition\outputop & \opsem\outputop_{\Algebra} & \of\lam\unitval\malg
&\mapsto\ilam\mchar{\algebra[\Algebra][\triple O\mchar\malg]} \\
\eSideCondition\divergeop & \opsem\divergeop_{\Algebra} & \of\unitval
&\mapsto\ilam\mstring{\algebra[\Algebra][\bot]}
\end{mapdef*}%
Note how $\opsem\divergeop$ is the operation from \lemmaref{divergence
operation}, that $\opsem\raiseop$ does indeed define an algebraic
operation for $\Monad_{\set{\raiseop, \divergeop}}$, and that the
inclusions $\Presheaf{\e\subset\e'}$ do indeed preserve the operations.

Thus $\seq{\ValCat, \arities, \Presheaf,
  \opsem[\placeholder]\placeholder}$ is a recursion $\Signature$-model.
\end{example}

As in \sectionref{generic effects}, we define models in terms of
generic effects:
\begin{definition+}{\recursionalternative{definition}{generic-model}}
Let $\Signature$ be a hierarchy. A \defterm{generic \DELTA{recursion} $\Signature$-model} is a
quadruple \[
\seq{\ValCat, \arities, \Presheaf, \genopsem[\placeholder]\placeholder}
\] where:
\begin{itemize}
\item
$\ValCat$ is a\DELTA{n $\wCPO$-enriched} distributive category, called the \defterm{value
  category};
\item
$\arities$ is a \DELTA{recursion} $\Signature$-type assignment in $\ValCat$;
\item
$\Presheaf$ is a functor $\E \to \DELTA{\wCPOAdjunctions\ValCat}$, called the
\defterm{model hierarchy}\DELTA{, such that, for} \DELTA{all
  $\e\in\E$ with $\divergeop \in \e$, $\Presheaf\e$ is a recursion model};
\item
$\genopsem[\placeholder]\placeholder$ assigns to each $\e \in \E$ and $\mop
\in \e$, $\mop \of \arity\Ar\Pa$ a generic effect $\genopsem\mop$
of type $\arity\Ar\Pa$ for $\Presheaf \e$\DELTA{, such that, for all
  $\e \in \E$ with $\divergeop\in\e$, $\genopsem\divergeop$ is the} \DELTA{%
  generic divergence effect (see \lemmaref{divergence operation})};
\end{itemize}
and $\Presheaf\parent{\e\subset\e'}$ preserves the effects.
\end{definition+}

As $\wCPO$-enrichment for algebraic operations, generic effects, and
their preservation coincides with the preservation of their ordinary
counterparts, we obtain the following
theorem:
\begin{theorem+}{\recursion{theorem}{categorical and generic models bijection}}
  Let $\Signature$ be a \DELTA{recursion} hierarchy. \DELTA{Recursion}
  $\Signature$-models
  \[\seq{\ValCat,
    \arities, \Presheaf, {\opsem[\placeholder]\placeholder}}\] and
  generic \DELTA{recursion} $\Signature$-models \[\seq{\ValCat, \arities, \Presheaf,
    \genopsem[\placeholder]\placeholder}\] are in bijection given via
  $\generic{\opsem\mop} = \genopsem\mop$.
\end{theorem+}

Finally, recursion models are a subclass of
our categorical models:

\begin{theorem}
  Let $\pair\Signature\divergeop$ be a recursion hierarchy. Every
  recursion $\pair\Signature\divergeop$-model can be seen as
  a $\Signature$-model, by forgetting the enriched structure and
  non-dis\-tin\-gui\-shing $\divergeop$.
\end{theorem}

\Section{Domain-theoretic models}\sectionlabel{recursion exception and IO example}

\nocats%
We now specialise to the category of \wcpo{}s. The following
definition characterises all categorical recursion models of this category:

\begin{definition+}{\recursionrevisit{definition}{set-type-assignment}{enriched-type-assignment}}
  Let $\Signature$ be a \DELTA{recursion} hierarchy. A
  \defterm{\DELTA{domain-theoretic recursion} type
    assignment for $\Signature$} is an assignment $\arities(\mop) =
  \pair\Ar\Pa$ of a pair of \DELTA{\wcpo{}s} to each ${\mop \in
  \Opset}$\DELTA{, such that $\divergeop \of \initial$}.
\end{definition+}

\begin{example+}{\revisit{example}{non-determinism hierarchy}}
A recursion type assignment in $\wCPO$ for non-determinism is:
\[
\chooseop  \of \twoobj
\qquad
\divergeop \of \initial
\]
\unhangdisplay[1.2]
\end{example+}

\begin{definition+}{\recursionrevisit{definition}{set-generic-model}{recursion-categorical-model}}
  Let $\Signature$ be a \DELTA{recursion} hierarchy.  A
  \defterm{\DELTA{domain-theoretic recursion}
    $\Signature$-model} is a quadruple
  \[
  \seq{\arities, \Monad_{\placeholder},
    \MonadMorphism_{\placeholder},
    \genopsem[\placeholder]\placeholder}
  \]
  where:
  \begin{itemize}
  \item $\arities$ is a \DELTA{domain-theoretic recursion} type assignment for
    $\Signature$;
  \item $\Monad_{\placeholder}$ assigns to each $\e$ in $\E$ a
    \DELTA{locally continuous} monad
    $\Monad_{\e}$\DELTA{, such that, for all $\e \in \E$} \DELTA{with
      $\divergeop \in \e$, $\Monad_{\e}$ is strict};
  \item $\MonadMorphism_{\placeholder}$ assigns to each
    $\e\subset\e'$ in $\E$ a monad morphism $\MonadMorphism_{\e\subset\e'} \of
    \Monad_{\e} \to \Monad_{\e'}$;
  \item $\genopsem[\placeholder]\placeholder$ assigns to each $\e \in
    \E$, and $\mop \of \arity\Ar\Pa$ in $\e$ a \DELTA{continuous}
    generic effect $\genopsem\mop
    \of \Pa \to \Monad_{\e}\Ar$\DELTA{, such that $\genopsem\divergeop
      \of \unitval\mapsto \bot$};
  \item
    $\MonadMorphism_{\placeholder}$ is \defterm{functorial};
  \end{itemize}
  and $\MonadMorphism_{\placeholder}$ preserves the generic
    effects.
\end{definition+}

\begin{example+}{\recursion{example}{exceptions-and-IO}}\examplelabel+{exceptions-and-IO-and-recursion}
We construct a domain-theoretic model for exceptions, terminal I/O,
and recursion.

We choose the hierarchy by $\Opset\definedby
\set{\raiseop, \inputop, \outputop{, \divergeop}}$, and set $\E$
to be $\Powerset{\Opset}$.

Take $\Char$ and $\String$ be the discrete \wcpo{}s whose carriers are
the corresponding sets $\Char$ and $\String$ from
\exampleref{exceptions-and-IO}.

The recursion model $\seq{\arities, \Monad_{\placeholder}, \MonadMorphism_{\placeholder},
  \genopsem[\placeholder]\placeholder}$ is given as follows.

The type assignment is given by
  \begin{align*}
  \raiseop&\of\arity\emptyset\String &\inputop &\of \Char
  &\outputop &\of \arity\terminal\Char
  &{\divergeop }&{\vphantom{\divergeop}\of\initial}
  \end{align*}

First, we define $\Monad_{\e}$ for $\e \subset \Opset\setminus\set\divergeop$.
Let $\mW$ be any \wcpo{}, and take any
\(\e \subset\set{\raiseop, \inputop,
  \outputop}
\). We take carrier set $\carrier{\Monad\mW}$ to be
$\carrier{\Monad_{\e}}\carrier\mW$, where $\carrier{\Monad_{\e}}$ is
the set-theoretic monad for exceptions and terminal I/O from
\exampleref{exceptions-and-IO}.

The set $\carrier{\Monad_{\e}}\carrier\mW$ inductively inherits an \wcpo{}
structure from $\mW$:
\begin{itemize}
\item if $\mw \leq \mw'$ in $\mW$ then $\mw \leq
  \mw'$ in $\Monad_{\e}$;
\item for all $\mstring\in\String$, $\pair R\mstring\leq\pair R\mstring$;
\item if $\inputop \in \e$, and for all $\mchar \in \Char$,
  $\mterm_{\mchar}\leq\mterm'_{\mchar}$, then
  \[
  \pair I{\seq[\mchar\in\Char]{\mterm_{\mchar}}}
  \leq \pair
  I{\seq[\mchar\in\Char]{\mterm'_{\mchar}}}
  \]
\item if $\outputop \in \e$, $\mchar \in \Char$, and $\mterm \leq
  \mterm'$, then
  \[
  \triple O\mchar{\mterm} \leq \triple O\mchar{\mterm'}
  \]
\end{itemize}

As trees, two elements of $\Monad_{\e}\mW$ are comparable if they have
the same shape, and corresponding leaves are compatibly comparable in
$\mW$. Thus, an $\omega$-chain of such trees is a sequence of trees
with the same shape, whose corresponding leaves form $\omega$-chains.
Thus, the suprema of such an $\omega$-chain is the same tree, with the
suprema of each such $\omega$-chain in that leaf.
Inductive calculations show that the unit and multiplication of
$\carrier{\Monad_{\e}}$ are continuous, hence define a monad
$\Monad_{\e}$ over $\wCPO$. An additional calculation shows
$\Monad_{\e}$ is locally continuous.

Next, we define $\Monad_{\e}$ for $\e$ with $\divergeop \in \e$.  This
time, we proceed co-inductively. Let $\mW$ be any \wcpo{}. We define
$\carrier{\Monad_{\e}\mW}$ as the largest set $\mX$ such that if
$\mterm \in \mX$ then either:
  \newlength{\optionalwidth}
  \newlength{\casetaglength}
\newenvironment{pattern match}[1][{}]{
  \begingroup
  \settowidth{\optionalwidth}{when $\outputop$}
  \newcommand\pmcasetag[2]{\settowidth{\casetaglength}{$(\outputop_{##1})$}\makebox[\casetaglength][l]{($##2_{##1}$)}}
  \newcommand\pmcase[2][]{\item[{\makebox[\optionalwidth][l]{}\hphantom{${}\in\e$:
        }{\pmcasetag{##1}{##2}}}]}
  \WithSuffix\newcommand\pmcase*[2][]{\item[{\makebox[\optionalwidth][l]{when
          $##2$}${}\in \e$: \pmcasetag{##1}{##2}}]}
  \settowidth\leftmargini{{\renewcommand\item[1][{}]{##1}\pmcase[{#1}]{\outputop}
  }}
  \begin{itemize}
}{
  \end{itemize}
  \endgroup
}
\begin{pattern match}
\pmcase{\bot}$\mterm = \bot$; or
\pmcase{\mW} $\mterm \in \mW$; or
\pmcase*\raiseop $\mterm = \raiseop$; or
\pmcase*\inputop $\mterm = \pair
  I{\seq[\mchar\in\Char]{\mterm_{\mchar}}}$, where, for all $\mchar
  \in \Char$, $\mterm_{\mchar} \in \mX$; or
\pmcase*\outputop $\mterm = \triple
  O\mchar{\mterm'}$, where $\mterm' \in \mX$.
\end{pattern match}
Thus $\carrier{\Monad_{\e}\mW}$ is the set of finite and infinite trees
whose nodes are labeled by $R$, $I$, and $O$, depending on whether
$\raiseop$, $\inputop$, and $\outputop$ are in $\e$, and whose leaves
are either the bottom element $\bot$, or a $\mW$ element. In
co-algebraic terms, $\carrier{\Monad_{\e}\mW}$ is the final co-algebra
for the following polynomial functor:
\[
\set{\bot} + \carrier\mW + \String + (\placeholder)^{\Char} + \Char\times(\placeholder)
\]
where each of the last three summands is included depending on whether
$\raiseop$, $\inputop$, and $\outputop$ are in $\e$.

As any final co-algebra, $\carrier{\Monad_{\e}\mW}$ is equipped with a
co-induction principle. A \defterm{bisimulation} is a binary relation
$\mR$ over $\carrier{\Monad_{\e}\mW}$ for which $\pair\mterm\mtermv
\in \mR$ implies:
\newcommand\bis{\text{bis}}
\begin{pattern match}[\bis]
\pmcase[\bis]\bot $\mterm = \mtermv = \bot$; or
\pmcase[\bis]\mW  $\mterm = \mtermv = \mw$, $\mw \in \mW$; or
\pmcase*[\bis]\raiseop $\mterm = \mtermv =
  \pair R\mstring$, $\mstring \in \String$; or
\pmcase*[\bis]\inputop  $\mterm = \pair I{\seq[\mchar\in\Char]{\mterm_{\mchar}}}$, $\mtermv = \pair
  I{\seq[\mchar\in\Char]{\mterm_{\mchar}}}$, where, for all $\mchar$
  in $\Char$, $\pair{\mterm_{\mchar}}{\mtermv_{\mchar}} \in \mR$; or
\pmcase*[\bis]\outputop $\mterm =
  \triple O\mchar{\mterm'}$, $\mtermv = \triple O\mchar{\mtermv'}$,
  where $\pair{\mterm'}{\mtermv'} \in \mR$.
\end{pattern match}
The co-induction principle states that all bisimulations are subsets
of the equality relation on $\carrier{\Monad_{\e}\mW}$, i.e., if $\mR$
is a bisimulation, and $\pair\mterm\mtermv \in \mR$
then $\mterm = \mtermv$.

The partial order structure on $\carrier{\Monad_{\e}\mW}$ is also
defined co-inductively.  We define $\leq$ as the largest relation
$\mR$ over
$\carrier{\Monad_{\e}\mW}$ for which $\pair\mterm\mtermv \in \mR$
implies either:
\begin{pattern match}[\leq]
\pmcase[\leq]\bot $\mterm = \bot$; or
\pmcase[\leq]\mW  $\mterm = \mw$, $\mtermv = \mwv$, $\mw,\mwv\in\mW$,
$\mw\leq\mwv$; or
\pmcase*[\leq]\raiseop $\mterm = \mtermv = \pair R\mstring$, $\mstring \in
\String$; or
\pmcase*[\leq]\inputop $\mterm = \pair I{\seq[\mchar\in\Char]{\mterm _{\mchar}}}$,
                 $\mtermv= \pair I{\seq[\mchar\in\Char]{\mtermv_{\mchar}}}$
where, for all $\mchar \in \Char$,
$\pair{\mterm_{\mchar}}{\mtermv_{\mchar}} \in \mR$; or
\pmcase*[\leq]\outputop $\mterm = \triple O\mchar{\mterm'}$,
                        $\mtermv= \triple O\mchar{\mtermv'}$
where $\pair{\mterm'}{\mtermv'}\in\mR$.
\end{pattern match}

Informally, we have $\mterm \leq \mtermv$ when $\mtermv$ can be
obtained from $\mterm$ by substituting the leaves $\mw$ with larger
leaves $\mw' \geq \mw$, and by substituting $\bot$ with any other
term.  Using this informal description, the
order is $\omega$-complete: the least upper bound of an $\omega$-chain
is obtained by taking the least upper bounds on the leaves from $\mW$,
and adding infinite branches where the shape of the term does not
stabilise.

We establish that $\leq$ equips $\carrier{\Monad_{\e}\mW}$ with an
\wcpo{} structure more formally.
\begin{proposition*}
The relation $\leq$ is a partial order.
\end{proposition*}

\begin{proof}%
Case analyses show that the
  diagonal relations $\Diagonal \definedby \set{\pair
    \mterm\mterm \suchthat \mterm \in \carrier{\Monad_{\e}\mW}}$ and
  $\leq^2$ both satisfy the condition in $\leq$'s definition, hence
  $\mathrel{\Diagonal}{}\subset{}\leq$ and $\leq^2{}\subset{}\leq$,
  ergo $\leq$ is reflexive and transitive.
  Case analysis shows that $\leq\intersect\geq$
  is a bisimulation, hence $(\leq\intersect\geq) \subset{}=$, ergo $\leq$
  is anti-symmetric.
\end{proof}

Given a poset $\mPoset$, denote by $\wChains\mPoset$ its set of
ascending $\omega$-chains.  Note we may conduct the following case analysis on
any $\omega$-chain $\seq[n\in\naturals]{\mterm_n}$ in $\wChains{\carrier\Monad_{\e}\mW}$:
\begin{pattern match}[\lub]
\pmcase[\lub]\bot for all $n$, $\mterm = \bot$;
  otherwise, there is a least $n_0$ for which $\mterm_{n_0}\neq\bot$, and either:
\pmcase[\lub]\mW $\mterm_{n_0} = \mw$; then,  for all $n\geq n_0$,
$\mterm_n \geq \mw_{n_0}$, hence $\mterm_n = \mw_n \in \mW$, and
$\mw_n$ is an $\omega$-chain in $\mW$; or
\pmcase*[\lub]\raiseop $\mterm_{n_0} = \pair R\mstring$; then, as in
the previous case, for all
$n \geq n_0$, $\mterm_n = \pair R\mstring$; or
\pmcase*[\lub]\inputop $\mterm_{n_0} = \pair I{\seq[\mchar \in
    \Char]{\mterm_{n_0}^{\mchar}}}$; then, for all $n\geq n_0$,
$$\mterm_n = \pair I{\seq[\mchar\in\Char]{\mterm_{n}^{\mchar}}}$$and,
for all $\mchar\in\Char$, $\seq[n\geq n_0]{\mterm_{n}^{\mchar}}$ is an
$\omega$-chain; or
\pmcase*[\lub]\outputop $\mterm_{n_0} = \triple
O\mchar{\mterm'_{n_0}}$; then, for all $n \geq n_0$, $\mterm_n =
\triple O\mchar{\mterm'_n}$, and $\seq[n\geq n_0]{\mterm'_n}$ is an $\omega$-chain.
\end{pattern match}

Using this case analysis, finality of $\carrier{\Monad_{\e}\mW}$
implies there exists a unique function $\lub \of
\wChains{\carrier{\Monad_{\e}\mW}} \to \carrier{\Monad_{\e}\mW}$
satisfying the following conditions.  For all $\seq[n\in\naturals]{\mterm_n}$,
using the previous notation:
\begin{pattern match}[\lub]
\pmcase[\lub]\bot
  $\lub\seq{t_n} = \bot$;
\pmcase[\lub]\mW $\lub\seq{t_n} = \lub_{n\geq n_0}\mw_n$;
\pmcase*[\lub]\raiseop $\lub\seq{t_n} = \pair R\mstring$$;$
\pmcase*[\lub]\inputop $\lub\seq{t_n} = \pair I{\seq[\mchar\in\Char]{\lub_{n\geq
      n_0}\mterm^{\mchar}_{n}}}$;
\pmcase*[\lub]\outputop $\lub\seq{t_n} = \triple O\mchar{\lub_{n\geq n_0}\mterm'_n}$.
\end{pattern match}
More explicitly, the above case analysis gives
$\wChains{\carrier{\Monad_{\e}\mW}}$ a co-algebra structure, and
finality yields $\lub$.

\begin{proposition*}
  For all $\omega$-chains $\seq{\mterm_n}$ in
  $\wChains{\carrier{\Monad_{\e}\mW}}$, $\lub_n\mterm_n$ is the least
  upper bound of $\seq{\mterm_n}$.
\end{proposition*}
\begin{proof}%
Define the following two relations:
\begin{align*}
  \mR^{\mathrm{bound}} &\definedby \set{\pair{\mterm_m}{\smash{\lub_n\mterm_n}}\suchthat
    \seq[n\in\naturals]{\mterm_n} \in
    \wChains{\carrier{\Monad_{\e}\mW}}, m \in \naturals}
  \\\\
  \mR^{\mathrm{least}} &\definedby \set{\pair{\smash{\lub_n\mterm_n}}{\mtermv}
    \suchthat     \seq[n\in\naturals]{\mterm_n} \in
    \wChains{\carrier{\Monad_{\e}\mW}}, \text{ for all $n \in
      \naturals$, }\mtermv \geq \mterm_n}
\end{align*}
Case analyses on $\seq{\mterm_n}$ show that $\mR^{\mathrm{bound}}$ and $\mR^{\mathrm{least}}$
satisfy the condition in the definition of $\leq$, hence
$\mR^{\mathrm{bound}} \subset{}\leq$, hence $\lub_n\mterm_n$ is an upper bound of
$\seq{\mterm_n}$, but then $\mR^{\mathrm{least}}\subset{} \leq$ shows
$\lub_n\mterm_n$ is the least upper bound.
\end{proof}

Thus, $\Monad_{\e}\mW$ is an \wcpo{}.

We define the morphism map structure of $\Monad_{\e}$ by mapping
each $f \of \mWv \to \mW$ to the the unique
function $\Monad_{\e}f \of
\Monad_{\e}\mWv \to \Monad_{\e}\mW$ satisfying:
\newcommand\mortag{\text{mor}}
\begin{pattern match}[\mortag]
  \pmcase[\mortag]\bot $\Monad_{\e}f(\mterm) = \bot$;
  \pmcase[\mortag]\mW $\Monad_{\e}f(\mterm) = f(\mw)$;
  \pmcase*[\mortag]\raiseop $\Monad_{\e}f(\mterm) = \pair R\mstring$;
  \pmcase*[\mortag]\inputop $\Monad_{\e}f(\mterm) = \pair I{\seq[\mchar\in\Char]{\Monad_{\e}f(\mterm_{\mchar})}}$;
  \pmcase*[\mortag]\outputop $\Monad_{\e}f(\mterm) = \triple O\mchar{\Monad_{\e}f(\mterm')}$.
\end{pattern match}

\begin{proposition*}
$\Monad_{\e}$ is a strict functor  over $\wCPO$.
\end{proposition*}

\begin{proof}%
  Case analyses on $\mterm$ show that the following two relations are bisimulations:
  \[
  \set{\pair{\mterm}{\Monad_{\e}\id(\mterm)}\suchthat \mterm \in
    \carrier{\Monad_{\e}\mW}}
  ,\qquad
  \set{\pair{\Monad_{\e}(f\compose g)(\mterm)}{(\Monad_{\e} f \compose
      \Monad_{\e} g)(t)} \suchthat \mterm \in
    \carrier{\Monad_{\e}\mW}}
  \]
  Thus, $\Monad_{\e}$ is
  a functor. Case analysis on $\mterm$ shows, by $\leq$'s definition,
  that if $f \leq g$, for any $f,g\of \mWv\to\mW$, then
  \[
  \set{\pair{\Monad_{\e}f(t)}{\Monad_{\e}g(t)} \suchthat \mterm \in
    \carrier{\Monad_{\e}\mW}} \subset {}\leq
  \]
  Thus, $\Monad_{\e}$ is locally monotone. Note that, by the definitions
of $\leq$ and $\lub$, the maps $\seq{\mterm_{\mchar}} \mapsto \pair
I{\seq{\mterm_{\mchar}}}$ and $\mterm \mapsto \triple O\mchar\mterm$
are continuous. For any $\omega$-chain of functions $\seq{f_n}$, we
use this continuity within further case analysis on
$\mterm$ to show that the following relation is a bisimulation:
\[
\set{\pair{\smash{\Monad_{\e}(\lub_n{f_n}(\mterm))}}{\smash{\lub_n(\Monad_{\e}f_n(\mterm))}}\suchthat \mterm \in \carrier{\Monad_{\e}\mW}}
\]
Thus, $\Monad_{\e}$ is a locally continuous functor.

Note $\Monad_{\e}$ is pointed, with $\bot \in \Monad_{\e}\mW$ is the
least element, and by fiat $\Monad_{\e}f$ preserves $\bot$.  Thus
$\Monad_{\e}$ is strict.
\end{proof}

Next, we equip $\Monad_{\e}$ with a monad structure. The unit is given
by the inclusion $\mW \subset \Monad_{\e}$. The definition of the multiplication map
$\monmult^{\e}(\overline\mterm)$ is
given co-inductively, by case analysis on any $\overline\mterm \in \Monad_{\e}^2\mW$:
\begin{pattern match}
\pmcase\bot $\bot$;
\pmcase\mW $\mtermv$, where $\overline\mterm = \mtermv$;
\pmcase*\raiseop $\pair R\mstring$;
\pmcase*\inputop $\pair I{\seq{\monmult^{\e}(\overline\mterm_{\mchar})}}$;
\pmcase*\outputop $\triple O\mchar{\monmult^{\e}(\overline\mterm')}$.
\end{pattern match}
Note that some care is needed in the case ($\mW$), and it requires
further case analysis on $\mtermv$ to properly define the required
co-algebra structure.

Straightforward calculations show that these maps are indeed continuous natural
transformations that satisfy the monad laws.

To summarise, we defined the monads $\Monad_{\placeholder}$
required in the definition of domain-theoretic recursion models.

Note that if $\divergeop \in \e \subset\e'$, then, by definition,
$\Monad_{\e}\mW \subset \Monad_{\e'}\mW$, and the inclusion is
continuous. Also, if $\divergeop \notin\e$, then $\Monad_{\e}\mW$ is
the subset of $\Monad_{\e\union\set{\divergeop}}\mW$ that includes only the finite trees
containing no $\bot$. In this case, the inclusion $\Monad_{\e}\mW \subset
\Monad_{\e\union\set\divergeop}\mW$ is continuous. In both cases, the
inclusions in fact form monad morphisms.  Therefore, for all
$\e\subset \e' \in \E$, we choose
$\MonadMorphism_{\e\subset\e'}$ as the inclusions, and obtain a
functorial family of (continuous) monad morphisms.

We choose the following generic effects, whenever they belong to the effect set $\e$:
\begin{mapdef*}[2]
  \genopsem\divergeop &\of \terminal &\to \Monad_{\e}\initial &   \genopsem\raiseop  &\of \String &\to \Monad_{\e}\initial\\
  \genopsem\divergeop &\of \unitval  &\mapsto \bot           &   \genopsem\raiseop & \of \mstring &\to \pair R\mstring \\
  \\
  \genopsem\inputop  &\of\terminal &\mapsto \Monad_{\e}\Char  &   \genopsem\outputop &\of\Char &\mapsto \Monad_{\e}\terminal \\
  \genopsem\inputop  &\of\unitval & \mapsto \pair
  I{\seq[\mchar\in\Char]{\mchar}}\qquad                      &   \genopsem\outputop &\of\mchar &\mapsto \triple O\mchar{\unitval}
\end{mapdef*}

As the definitions of the generic effects are uniform in
$\e$, they are preserves by the inclusions.

In summary, $\seq{\arities, \Monad_{\placeholder}, \MonadMorphism_{\placeholder},
  \genopsem[\placeholder]\placeholder}$ is a domain-theoretic
recursion $\Signature$-model.
\end{example+}

Note that in the last example our treatment was only semi-uniform. It
was uniform for all $\e$ without $\divergeop$, and separately uniform
for all $\e$ containing $\divergeop$. However, when moving between the
two cases, some care was required.  Also, the two cases were different
in nature: when $\divergeop$ was not present, the treatment was
completely inductive. With $\divergeop$ present, the natural models
become co-inductive. Compare this account to \exampleref{enriched
  exceptions and IO}, in which our account of exceptions and
divergence was also inductive.  This phenomena is a well-known
consequence of the limit-colimit
coincidence~\cite{scott:continuous-lattices,
  plotkin-smyth:the-category-theoretic-solution-of-recursive-domain-equations}.
In particular, despite their co-inductive appearance, the models can
still be viewed as initial algebras. The conservative restriction
construction we will present in
\chapterref{algebraic-models} construct these hierarchical models
for I/O, Exception, recursion, and global state in a uniform manner.

\cats
We conclude this section by establishing that domain-theoretic
recursion models indeed characterise all recursion models over
$\wCPO$.

\begin{lemma}\lemmalabel{strictness and recursion models}
  An $\wCPO$-enriched \cbpv{} model $\pair\wCPO\Monad$ is a recursion
  model if and only if $\Monad$ is strict.
\end{lemma}

\begin{proof}%
  First, assume the model is a recursion model. For any \wcpo{} $\mW$,
  $\Monad\mW$ is pointed, as
  \(
  \Monad\mW \isomorphic \homset[\wCPO]\terminal{\Monad\mW}
  \) via $\mw \mapsto \ilam\unitval\mw$.
  Given any $f \of \mWv \to \mW$, $\Monad f \of \Monad \mWv \to
  \Monad\mW$ is a homomorphism, hence:
  \[
  \bot = (\lam\unitval\bot)(\unitval) \explain={\theoremref{recursion models
    via standard homomorphisms}} (\Monad f) \compose
  (\lam\unitval\bot) (\unitval) = (\Monad f)(\bot)
  \]
  Thus $\Monad$ is strict.

  Conversely, assume $\Monad$ is strict.  Let $\Algebra$ be any
  $\Monad$-algebra. As $\Monad$ is pointed, $\carrier\Monad$ has a
  least element $\bot$. For any $\malg \in \carrier\Algebra$, we have
  $\bot \leq \unit(\malg)$. Therefore:
  \[
  \algebra[\Algebra][\bot] \explain\leq{continuity}
  \algebra[\Algebra][\unit(\malg)]
  \explain={$\Monad$-algebra}
  \malg
  \]
  Hence $\carrier\Algebra$ is pointed with $\algebra[\Algebra][\bot]$
  the least element. By \lemmaref{pointed functionspace}, for all $\mG
  \inObj \wCPO$, $\homset[\wCPO]\mG{\carrier\Algebra}$ is pointed,
  with $\lam\mg\bot$ the least element.

  If $f \of \mGv \to \mG$ is any function and $h \of \Algebra \to \Algebrav$ any
  $\Monad$-algebra homomorphism, we have:
  \[
  (h\compose(\lam\mg\bot)\compose f)(\mgv) =
  h(\algebra[\Algebra][bot])
  \explain={$\Monad$-algebra homomorphism}
  \algebra[\Algebrav][\Monad h(\bot)]
  \explain={$\Monad$ is strict}
  \algebra[\Algebrav][\bot]
  =\bot
  \]
  Hence, by \theoremref{recursion models via standard homomorphisms},
  $\pair\wCPO\Monad$ is a recursion model.
\end{proof}

\begin{proposition+}{\recursion{proposition}{set models characterisation}}
Let $\Signature$ be a \DELTA{recursion} hierarchy.
\DELTA{Domain-theoretic recursion} $\Signature$-models
$\seq{\arities, \Monad_{\placeholder}, \MonadMorphism_{\placeholder},
  \genopsem[\placeholder]\placeholder}$ and (categorical) \DELTA{recursion}
$\Signature$-models $\seq{\Set, \arities, \Presheaf,
  \genopsem[\placeholder]\placeholder}$ are in bijection given via
\begin{itemize}
\item for all $\e \in \E$, $\Presheaf\e = \Monad_{\e}$; and

\item for all $\e \subset \e'$ in $\E$, $\Presheaf(\e\subset\e') = \MonadMorphism_{\e\subset\e'}$.
\end{itemize}
\end{proposition+}

\begin{proof}%
  From Kock's work~\cite{kock:strong-functors-and-monoidal-monads} follows that all
  locally continuous monads over $\wCPO$ have a unique continuous strength. By
  \lemmaref{strictness and recursion models}, the conditions
  on recursion models and strict monads are equivalent. The rest of
  the proof is analogous to that of \propositionref{set models
    characterisation}.
\end{proof}
