\Section{Presentation models}\sectionlabel{presentation models}
We now utilise the algebraic descriptions to account for our hierarchical models.

\begin{definition+}{\revisit{definition}{presentable type assignment}}
Let $\Opset$ be a set. A \defterm{presentation type assignment for
  $\Opset$} is a set-theoretic type assignment (see
\definitionref+{set-type-assignment}) such that, for all $\mop \of
\arity\Ar\Pa$, the arity type $\Ar$ is a finite set.
\end{definition+}

For example, if $\StorVal$ is a finite set denoting storable values,
then the global state type assignment from \exampleref+{set theoretic
  global state type assignment} is a presentation type assignment.

\begin{definition+}{\algebraicrevisit{definition}{generic-model}{set-generic-model}}{}{}{}
\definitionlabel{presentation-generic-model}{}{}
Let $\Signature$ be a hierarchy. A \defterm{\DELTA{presentation}
  $\Signature$-model} is a quadruple
  \[
  \seq{\arities, \DELTA{\PresAx\placeholder, \PresTrans\placeholder,
      \presopsem[\placeholder]\placeholder}}
  \]
  where:
  \begin{itemize}
  \item $\arities$ is a \DELTA{presentation} type assignment for
    $\Signature$;
  \item \DELTA{$\PresAx\placeholder$} assigns to each $\e$ in $\E$ a \DELTA{presentation
    $\PresAx{\e}$};
  \item \DELTA{$\PresTrans\placeholder$} assigns to each
    $\e\subset\e'$ in $\E$ a \DELTA{translation  $\PresTrans{\e\subset\e'} \of
    \PresAx{\e} \to \PresAx{\e'}$};
  \item \DELTA{$\presopsem[\placeholder]\placeholder$} assigns to each $\e \in
    \E$, and $\mop \of \arity\Ar\Pa$ in $\e$ a \DELTA{$\Pa$-indexed
      family $\presopsem\mop$ of\/} \DELTA{terms over $\Ar$};

  \item for all $\e
    \subset \e' \subset \e''$ in $\E$:
    \[
    \DELTA{\PresTrans{\e\subset\e}\TransEq{} \id},
    \qquad
    \DELTA{\PresTrans{\e'\subset\e''}\compose\PresTrans{\e\subset\e'}}
    \DELTA{{}\TransEq\PresTrans{\e\subset\e''}}
    \]
    i.e., \DELTA{$\PresTrans{\placeholder}$} is \defterm{functorial};
  \end{itemize}
  and, for all $\e\subset\e'$ in $\E$,  $\mop \of \arity\Ar\Pa$ in
    $\e$, \DELTA{and $\mpa \in \Pa$}:
  \[
  \DELTA{
    \PresAx{\e'} \proves
      \PresTrans{\e\subset\e'}(\presopsem[\e]\mop(\mpa)) =
      \presopsem[\e']\mop(\mpa)
  }
  \]
    Thus, \DELTA{$\PresTrans{\placeholder}$} preserves the
    \DELTA{effect terms}.
\end{definition+}

Let \( \seq{\arities, \PresAx\placeholder, \PresTrans\placeholder,
  \presopsem[\placeholder]\placeholder} \) be a presentation
$\Signature$-model. We construct a set-theoretic $\Signature$-model \(
\seq{\arities, \Monad_{\placeholder}, \MonadMorphism_{\placeholder},
  \genopsem[\placeholder]\placeholder} \) as follows. For every $\e$
in $\E$, $\Monad_{\e}$ is the free $\PresAx\e$-model monad. For every
$\e \subset \e'$, $\MonadMorphism_{\e\subset\e'}$ is the monad
morphism corresponding to the translation
$\PresTrans{\e\subset\e'}$. Finally, for every $\e$ in $\E$ and $\mop
\of \arity\Ar\Pa$ in $\e$, we set
\begin{mapdef*}
\genopsem\mop \of& \Pa &    \to \Monad_{\e}\Ar \\
                 & \mpa&\mapsto [\presopsem\mop(\mpa)]
\end{mapdef*}%

\cats{}Note that each of the monads $\Monad_{\e}$ in this construction
is finitary. The converse statement also holds, in light of the
essential surjectivity of the functor ${\Monad_{\placeholder} \of
\PresentationCat \to \EnrichedRankedMonad[\aleph_0]\Set}$
(\theoremref{presentations are essentially surjective}). Thus, every
set-theoretic $\Signature$-model with a presentation type assignment
arises from a presentation $\Signature$-model in this way.

\newpage
\hspace{1cm}
\vspace{-1\baselineskip}
\nocats{}Our goal is to generate hierarchical models from given
algebraic descriptions of the non-hierarchical models. We therefore
first need a notion of such models.

\begin{definition+}{\revisitalgebraic{definition}{non-hierarchical cbpv model}{non-hierarchical algebraic cbpv model}}
  Let $\Opset$ be a set. A \defterm{presentation $\Opset$-model} is a
  triple \[
  \seq{\arities, \PresAx{}, \presopsem[]\placeholder}
  \]
  where:
  \begin{itemize}
  \item $\arities$ is a presentation type assignment for $\Opset$;
  \item $\PresAx{}$ is a presentation; and
  \item $\presopsem[]\placeholder$ assigns to each $\mop \of
    \arity\Ar\Pa$ in $\Opset$ a $\Pa$-indexed family
    $\presopsem[]\mop$ of terms over $\Ar$.
  \end{itemize}
\end{definition+}

\begin{example}\examplelabel{global state presentation model}
Take $\Opset \definedby \set{\lookupop, \updateop}$. Let $\StorVal =
\set{\mval_1, \ldots, \mval_n}$, $n \geq 2$ be any finite set denoting
storable values. Let $\arities$ be the presentation type assignment
from \exampleref{presentable type assignment}. Let $\PresAx{}$ be the
presentation of $\StorVal$-mnemoids from \exampleref{mnemoid
  presentation}. Define:
\[
\presopsem[]\lookupop \of \unitval \mapsto \lookupop(\mval_1, \ldots,
\mval_n) \qquad
\presopsem[]\updateop \of \mval_0  \mapsto \updateop_{\mval_0}(\unitval)
\]
Then $\triple \arities{\PresAx{}}{\presopsem[]\placeholder}$ is a
presentation $\Opset$-model for global $\StorVal$-state.
\end{example}

\begin{example}
Take $\Opset \definedby \set{\chooseop}$. Let $\arities$ be the
presentation type assignment given by $\chooseop \of \twoobj$, $\PresAx{}$ be
the semilattice presentation from \exampleref{semilattice
  presentation}, and set
\[
\presopsem[]\chooseop \of \unitval \mapsto (\inj1\unitval)\orop(\inj2\unitval)
\]
Then $\triple \arities{\PresAx{}}{\presopsem[]\placeholder}$ is a
presentation $\Opset$-model for non-deterministic choice.
\end{example}

\begin{example}\examplelabel{IO and exception presentation
    non-hierarchical model}
Take $\Opset \definedby \set{\inputop, \outputop, \raiseop}$. Let
$\Char = \set{\mchar_1, \ldots, \mchar_n}$ be a finite set denoting
terminal characters. Let $\arities$ be the presentation type
assignment given by
\[
\inputop \of \Char \qquad
\outputop \of \arity\terminal\Char \qquad
\raiseop \of \arity\initial\String
\]
Let $\PresAx{}$ be the free presentation over the signature:
\[
\set{\inputop \of n, \outputop_{\mchar}\of 1,
  \raiseop_{\mstring}\of 0 \suchthat \mchar \in \Char, \mstring \in \String}
\]
Set
\begin{mapdef*}
\presopsem[]\inputop &\of \unitval &\mapsto \inputop(\mchar_1, \ldots, \mchar_n)\\
\presopsem[]\outputop&\of \mchar   &\mapsto \outputop_{\mchar}(\unitval) \\
\presopsem[]\raiseop &\of \mstring &\mapsto \raiseop_{\mstring}
\end{mapdef*}%
Then $\triple \arities{\PresAx{}}{\presopsem[]\placeholder}$ is a
presentation $\Opset$-model for terminal I/O and exceptions.
\end{example}

Note that these examples illustrate that our notion of presentation
$\Opset$-models is lightweight: the only proof obligations it incurs
are the finiteness of the arity types, and the well-formedness of the
equations and effect terms.

\cats{}The $\Opset$-model in \exampleref{IO and
  exception presentation non-hierarchical model} does \emph{not} arise
from an algebraic $\Opset$-model with a finitary Lawvere theory, as
the type assignment is not finitely presentable. We can capture this
model by switching to countable Lawvere theories, but these capture
monads that cannot be presented using our finitary notion of
presentations. Therefore, there is a mismatch between our notion of a
presentation $\Opset$-model and our notion of a finitary algebraic
$\Opset$-model. As we do not wish to diverge from the standard notions
of universal algebra and of enriched Lawvere theories, we do not
resolve this mismatch in this thesis.\label{mismatch between lawvere theories and presentations}

\nocats{}We now present the main construction of this chapter, the
conservative restriction model:
\begin{theorem+}{\revisit{theorem}{categorical conservative
      restriction}}\theoremlabel+{presentation conservative restriction}
  Let $\Opset$ be a set, and let
  $\mModel = \triple\arities{\PresAx{}}{\presopsem[]\placeholder}$ be a
  presentation $\Opset$-model. For every effect hierarchy $\Signature$
  whose set of operations is $\Opset$, we have a $\Signature$-model
  defined by
  \[
  \conservative\mModel \definedby \seq{\arities, \PresAx\placeholder,
    \PresTrans\placeholder, \presopsem[\placeholder]\placeholder}
  \]
  together with the auxiliary data \(
  \seq{
    \enum\placeholder,
    \ressig\placeholder, \resinit\placeholder, \resepi\placeholder,
    \resmono\placeholder, \resinittrans\placeholder
  }
  \), where:
  \begin{itemize}
  \item $\enum\placeholder$ assigns to each $\mop \of \arity\Ar\Pa$,
    $\cardinality\Ar = n$,
    in $\Opset$ a bijection $\enum\mop \of \Ar \isomorphic \set{1,
      \ldots, n}$;
  \item $\ressig\placeholder$ assigns to every $\e \in \E$ a
    signature $\ressig\e$ given by
    \[
    \ressig\e \definedby \set{\mop_{\mpa} \of n \suchthat \mop \of
      \arity\Ar\Pa, \cardinality\Ar = n, \mpa \in \Pa}
    \]
  \item $\resinit\placeholder$ assigns to every $\e \in \E$ the
    translation $\resinit\e \of \pair{\ressig\e}\emptyset\to\PresAx{}$
    given by the substitution
    \[
    \resinit\e(\mop) \definedby \presopsem[]\mop\uasub
    \]
    where $\uasub$ is the substitution given by $\uasub(\mar)
    \definedby \tx_{\enum\mop\mar}$ for every ${\mar\in\Ar}$;
  \item for every $\e \in \E$,
    $\triple{\PresAx\e}{\resepi\e}{\resmono\e}$ is the factorisation from
    \theoremref{translation factorisation},
    $${\resinit\e \of \pair{\ressig\e}\emptyset \xepimor{\resepi\e}
    \PresAx\e \xmonomor{\resmono\e}\PresAx{}}$$ i.e., $\PresAx\e$ has
    $\ressig\e$ as signature, $\resepi\e$ is the evident surjective
    extension, and $\resmono\e$ is the evident conservative
    translation;
  \item $\presopsem[\placeholder]\placeholder$ assigns to every $\e
    \in \E$ and $\mop \of \arity\Ar\Pa$, $\cardinality\Ar = n$ in $\e$
    the family
    \[
    \presopsem\mop \definedby
    \seq[\mpa\in\Pa]{\mop_{\mpa}(\enum*\mop1, \ldots, \enum*\mop n)}
    \]
  \item $\resinittrans\placeholder$ assigns to every $\e \subset\e'$
    in $\E$ the evident extension $\resinittrans{\e\subset\e'} \of
    \pair{\ressig\e}\emptyset \to \PresAx{\e'}$; and
  \item $\PresTrans{\placeholder}$ assigns to every $\e \subset \e'$
    the evident extension $\PresTrans{\e\subset\e'} \of \PresAx\e \to
    \PresAx{\e'}$, and, moreover, this extension is conservative.
  \end{itemize}
  We call $\conservative\mModel$ the \defterm{set-theoretic conservative restriction
  $\Signature$-model} for the given $\Opset$-model.
\end{theorem+}

Note that this theorem gives us an explicit and uniform definition of
$\conservative\mModel$. However, working out the exact syntactic
description of each presentation $\PresAx\e$ is impractical, as these
presentations always have infinitely many axioms. In every concrete case, we
will find alternative and simpler ways to present the monad
corresponding to $\PresAx\e$. Our technique is to rely on
\corollaryref{translation factorisation uniqueness}: we will factorise
the translation $\resinit\e$ to a surjective-conservative
factorisation. The factorising presentation is then, up to the
equi\-va\-lence~$\TransEq$, canonically isomorphic to $\PresAx\e$.

\begin{example+}{\revisit{example}{global state conservative restriction}}
  Let $\Opset \definedby \set{\lookupop, \updateop}$. Let $\StorVal =
  \set{\mval_1, \ldots, \mval_n}$, $n \geq 2$, be a finite set
  denoting storable values. Let
  $\mModel \definedby \triple\arities{\PresAx{}}{\presopsem[]\placeholder}$ be the global state
  $\Opset$-model from \exampleref{global state presentation
    model}. Let $\Signature$ be the full powerset hierarchy. We
  analyse the conservative restriction model $\conservative\mModel$.

  The presentation $\PresAx\emptyset$ can be alternatively described
  by the empty presentation. Indeed, because the theory of mnemoids
  is consistent, we have a factorisation consisting of extensions:
  \[
  \pair{\ressig\emptyset}\emptyset = \pair\emptyset\emptyset \epimor
  \pair\emptyset\emptyset \monomor \PresAx{}
  \] Therefore, by \corollaryref{translation factorisation
    uniqueness}, $\PresAx\emptyset$ and the empty presentation both
  present the same monad.

  The presentation $\PresAx{\set\lookupop}$ can be alternatively
  described by the environment presentation $\Ax_{\Environment}$ from
  \exampleref{environment presentation}, as the two evident extensions
  form a factorisation
  \[
  \resinit{\set\lookupop}
  \of
  \pair{\set{\lookupop_{\unitval}\of
      n}}\emptyset
  \epimor
  \Ax_{\Environment}
  \monomor
  \PresAx{}
  \]
  Indeed, as $\Ax_{\Environment}$'s signature is $\set{\lookupop\of
    n}$, the first translation is surjective. The monad morphism
  corresponding to the second translation is the monad morphism
  $\MonadMorphism_{\set\lookupop\subset\set{\lookupop, \updateop}}$
  from \exampleref+{set theoretic global state model}. Direct
  calculation shows this monad morphism is componentwise injective,
  hence the second translation is conservative.

  Similarly, the presentation $\PresAx{\set\updateop}$ can be alternatively
  described by the overwrite presentation $\PresAx{\Overwrite}$ from
  \exampleref{stateful presentations and monads}.

  Finally, the presentation $\PresAx{\set{\lookupop, \updateop}}$ can
  be alternatively described by the presentation $\PresAx{}$ itself.

  In summary, the set-theoretic $\Signature$-model corresponding to
  $\conservative\mModel$ is the $\Signature$-model for global state
  from \exampleref+{set theoretic global state model}.
\end{example+}

\begin{example}
Let $\Opset \definedby \set{\inputop, \outputop, \raiseop}$ and
$\mModel \definedby \triple\arities{\PresAx{}}{\presopsem[]{}}$ be the
terminal I/O and exception presentation $\Opset$-model from
\exampleref{IO and exception presentation non-hierarchical
  model}. Let $\Signature$ be the full powerset hierarchy. We
analyse conservative restriction model $\conservative\mModel$.

For every $\e \subset \Opset$, we have the following factorisation of extensions:
\[
\resinit\e \of \pair{\ressig\e}\emptyset \epimor
\pair{\ressig\e}\emptyset \monomor \PresAx{}
\]
Indeed, the first extension is evidently surjective. As $\PresAx{}$ is
free, the second extension is conservative. Therefore, $\PresAx\e$ may
be alternatively presented by $\pair{\ressig\e}\emptyset$. Therefore,
the set-theoretic model corresponding to $\conservative\mModel$ is the
$\Signature$-model for terminal I/O and exceptions given in
\exampleref{exceptions-and-IO}.
\end{example}

The last two examples show that the conservative restriction model
yields the natural $\Signature$-models from \sectionref{set-theoretic
  models}. Note how we transitioned from specifying \emph{structure}
to specifying \emph{properties}: there is very little overhead in
proof obligations while describing the structure of the starting
$\Opset$-model. A more elaborate analysis of the \emph{properties} of
the resulting conservative restriction models recovers the rest of the
elaborate model structure. Thus, we avoid the need to specify the
exponentially large structure required by set-theoretic
$\Signature$-models.

In summary, we reviewed the relevant background in universal algebra,
equational logic, and its relationship to finitary monads and Lawvere
theories, and reformulated our conservative restriction construction
in terms of presentations.
