Skip to content
Snippets Groups Projects
Commit c12408c0 authored by Eric Giovannini's avatar Eric Giovannini
Browse files

changes to categorical model

parent fa5a9c09
Branches
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
paper-new/categorical-model.tex
+ 172
− 70
View file @ c12408c0
......@@ -445,16 +445,35 @@ The judgment $\gamma : f \bisim_{A_i, A_o} f'$ is defined to mean:
\item $\tvsim(\gamma) = f'$
\end{enumerate}
Lastly, we require that for any value object $A$, the hom-set $\ef(FA, FA)$ contains a
distinguished morphism $\delta_A^*$, such that $\delta_A^* \bisim_{FA, FA} \id_{FA}$.
% Spelling this all out concretely, for any pair...
% Spelling this all out concretely, for any pair...
% Lastly, we require that for any value object $A$, the hom-set $\ef(FA, FA)$ contains a
% distinguished morphism $\delta_{FA}^*$, such that $\delta_A^* \bisim_{FA, FA} \id_{FA}$.
% Moreover, we require that these morphisms are related in that for any
% $c : A \rel A'$, we have a square $\delta_{FA}^* \ltdyn_{Fc}^{Fc} \delta_{FA'}^*$.
Lastly, we require that for any computation object $B$, the hom-set $\vf(UB, UB)$ contains a
distinguished morphism $\delta_{UB}^*$, such that $\delta_{UB}^* \bisim_{UB, UB} \id_{UB}$.
Moreover, we require that these morphisms are related in that for any
$d : B \rel B'$, we have a square $\delta_{UB}^* \ltdyn_{Ud}^{Ud} \delta_{UB'}^*$.
We also require that these morphisms commute with computation morphisms, in the sense
that for any $\phi \in \ef(B, B')$ we have $U\phi \circ \delta_{UB_1}^* = \delta_{UB_2} \circ U\phi$.
Given the existence of the morphisms $\delta_{UB}^*$, we can define computation morphisms
$\delta_{FA}^* \in \ef(FA, FA)$ for all $A$ using the
\begin{definition}\label{def:step-1-model}
A \emph{step-1 intensional model} consists of all the data of a step-0 intensional model along
with the additional categories and functors for bisimiarity described above, as well as
the existence of a distinguised computation morphism $\delta_A^* \bisim \id_{FA}$ for each $A$.
with:
\begin{itemize}
\item The categories and functors for bisimiarity described above.
\item The existence of a distinguished value morphism $\delta_{UB}^* \bisim \id_{UB}$ for each $B$.
\item A square $\delta_{UB}^* \ltdyn_{Ud}^{Ud} \delta_{UB'}^*$ for all $d : B \rel B'$.
\item The commutativity condition $U\phi \circ \delta_{UB_1}^* = \delta_{UB_2} \circ U\phi$ for any $\phi \in \ef(B, B')$.
\end{itemize}
% We also require the existence of a distinguised computation morphism $\delta_{FA}^* \bisim \id_{FA}$ for each $A$,
% and a square $\delta_{FA}^* \ltdyn_{Fc}^{Fc} \delta_{FA'}^*$ for all $c : A \rel A'$.
\end{definition}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
......@@ -484,7 +503,7 @@ capturing the notion that they have no effect other than to delay.
% the set of endomorphisms $f$ such that $f$ is weakly bisimilar to the identity
% forms a monoid under composition.
We require that $\delta_A^* \in \pe_{FA}$ for all $A$, where $\delta_A^*$ is the distinguished
We require that $\delta_{FA}^* \in \pe_{FA}$ for all $A$, where $\delta_{FA}^*$ is the distinguished
morphism that is required to be present in every hom-set $\ef(FA, FA)$ per the definition
of a step-1 model.
......@@ -534,7 +553,7 @@ This is summarized below:
$\{ f \in \vf(A,A) \mid f \bisim \id \}$.
\item For each computation type $B$, there is a monoid $\pe_B$ that is a submonoid of
$\{ g \in \ef(B,B) \mid g \bisim \id \}$.
\item For all $A$, the distinguished endomorphism $\delta_A^*$ is in $\pe_{FA}$.
\item For all $A$, the distinguished endomorphism $\delta_{FA}^*$ is in $\pe_{FA}$.
% \item $\pv_A$ and a monoid homomorphism
% \[ \ptbv_A : \pv_A \to \{ f \in \vf(A,A) \mid f \bisim \id \} \]
% \item $\pe_B$ and a monoid homomorphism
......@@ -557,76 +576,156 @@ As is the case in the extensional model, there is a relationship between
vertical (i.e., function) morphisms and horizontal (i.e., relation) morphisms,
but as mentioned above, now there
are perturbations involved in order to keep both sides ``in lock-step".
We begin with a step-2 intensional model as defined in the previous section,
and provide the additional conditions that axiomatize the behavior of casts.
The precise definitions are as follows.
First, let $\mathcal M$ be any double category with a notion of perturbations,
i.e., for any object $X$ in $\mathcal M$ there is a monoid $P_X$ which is a
submonoid of the endomorphisms on $X$.
% TODO: Give these squares names
\begin{definition}\label{def:quasi-left-representable}
Let $c : A \rel A'$ be a value relation. We say that $c$ is \emph{quasi-left-representable by}
$f \in \vf(A, A')$ if there are perturbations $\delta_c^{l,e} \in \pv_A$ and
$\delta_c^{r,e} \in \pv_{A'}$ such that the following squares commute:
Let $R$ be a horizontal morphism in $\mathcal M$ between objects $X$ and $Y$.
We say that $R$ is quasi-left-representable by a vertical morphism $f$ in
$\mathcal M(X, Y)$ if there are perturbations $\delle_R \in P_X$ and
$\delre_R \in P_Y$ such that the following squares commute:
\begin{center}
\begin{tabular}{ m{7em} m{7em} }
% UpL
\begin{tikzcd}[ampersand replacement=\&]
A \& {A'} \\
{A'} \& {A'}
\arrow["f"', from=1-1, to=2-1]
\arrow["\delta_c^{r,e}", from=1-2, to=2-2]
\arrow["c", "\shortmid"{marking}, no head, from=1-1, to=1-2]
\arrow[from=2-1, to=2-2, Rightarrow, no head]
\end{tikzcd}
&
% UpR
\begin{tikzcd}[ampersand replacement=\&]
A \& {A} \\
{A} \& {A'}
\arrow["\delta_c^{l,e}"', from=1-1, to=2-1]
\arrow["f", from=1-2, to=2-2]
\arrow[from=1-1, to=1-2, Rightarrow, no head]
\arrow["c"', "\shortmid"{marking}, no head, from=2-1, to=2-2]
\end{tikzcd}
\end{tabular}
\end{center}
\begin{center}
\begin{tabular}{ m{7em} m{7em} }
% UpL
\begin{tikzcd}[ampersand replacement=\&]
X \& {Y} \\
{Y} \& {Y}
\arrow["f"', from=1-1, to=2-1]
\arrow["\delta_R^{r,e}", from=1-2, to=2-2]
\arrow["R", "\shortmid"{marking}, no head, from=1-1, to=1-2]
\arrow[from=2-1, to=2-2, Rightarrow, no head]
\end{tikzcd}
&
% UpR
\begin{tikzcd}[ampersand replacement=\&]
X \& {X} \\
{X} \& {Y}
\arrow["\delta_R^{l,e}"', from=1-1, to=2-1]
\arrow["f", from=1-2, to=2-2]
\arrow[from=1-1, to=1-2, Rightarrow, no head]
\arrow["R"', "\shortmid"{marking}, no head, from=2-1, to=2-2]
\end{tikzcd}
\end{tabular}
\end{center}
We call the first square $\upl$ and the second square $\upr$.
We call the first square $\upl$ and the second square $\upr$.
\end{definition}
\begin{definition}\label{def:quasi-right-representable}
Let $d : B \rel B'$ be a computation relation. We say that $d$ is
\emph{quasi-right-representable by} $f \in \ef(B', B)$
if there exist perturbations $\delta_d^{l,p} \in \pe_B$ and
$\delta_d^{r,p} \in \pe_{B'}$ such that the following squares commute:
\begin{center}
\begin{tabular}{ m{7em} m{7em} }
% DnR
\begin{tikzcd}[ampersand replacement=\&]
{B} \& {B'} \\
{B} \& {B}
\arrow["\delta_d^{l,p}"', from=1-1, to=2-1]
\arrow["g", from=1-2, to=2-2]
\arrow["R", "\shortmid"{marking}, no head, from=1-1, to=1-2]
\arrow[from=2-1, to=2-2, Rightarrow, no head]
\end{tikzcd}
&
% DnL
\begin{tikzcd}[ampersand replacement=\&]
{B'} \& {B'} \\
{B} \& {B'}
\arrow["g"', from=1-1, to=2-1]
\arrow["\delta_d^{r,p}", from=1-2, to=2-2]
\arrow[from=1-1, to=1-2, Rightarrow, no head]
\arrow["R"', "\shortmid"{marking}, no head, from=2-1, to=2-2]
\end{tikzcd}
\end{tabular}
\end{center}
Let $R$ be a horizontal morphism between $X$ and $Y$. We say that $R$ is
\emph{quasi-right-representable by} $f \in \mathcal M(Y, X)$
if there exist perturbations $\dellp_R \in P_X$ and
$\delrp_R \in P_Y$ such that the following squares commute:
\begin{center}
\begin{tabular}{ m{7em} m{7em} }
% DnR
\begin{tikzcd}[ampersand replacement=\&]
{X} \& {Y} \\
{X} \& {X}
\arrow["\delta_R^{l,p}"', from=1-1, to=2-1]
\arrow["f", from=1-2, to=2-2]
\arrow["R", "\shortmid"{marking}, no head, from=1-1, to=1-2]
\arrow[from=2-1, to=2-2, Rightarrow, no head]
\end{tikzcd}
&
% DnL
\begin{tikzcd}[ampersand replacement=\&]
{Y} \& {Y} \\
{X} \& {Y}
\arrow["f"', from=1-1, to=2-1]
\arrow["\delta_R^{r,p}", from=1-2, to=2-2]
\arrow[from=1-1, to=1-2, Rightarrow, no head]
\arrow["R"', "\shortmid"{marking}, no head, from=2-1, to=2-2]
\end{tikzcd}
\end{tabular}
\end{center}
We call the first square $\dnr$ and the second square $\dnl$.
\end{definition}
We call the first square $\dnr$ and the second square $\dnl$.
\end{definition}
% TODO: Give these squares names
% \begin{definition}\label{def:quasi-left-representable}
% Let $c : A \rel A'$ be a value relation. We say that $c$ is \emph{quasi-left-representable by}
% $f \in \vf(A, A')$ if there are perturbations $\delta_c^{l,e} \in \pv_A$ and
% $\delta_c^{r,e} \in \pv_{A'}$ such that the following squares commute:
% \begin{center}
% \begin{tabular}{ m{7em} m{7em} }
% % UpL
% \begin{tikzcd}[ampersand replacement=\&]
% A \& {A'} \\
% {A'} \& {A'}
% \arrow["f"', from=1-1, to=2-1]
% \arrow["\delta_c^{r,e}", from=1-2, to=2-2]
% \arrow["c", "\shortmid"{marking}, no head, from=1-1, to=1-2]
% \arrow[from=2-1, to=2-2, Rightarrow, no head]
% \end{tikzcd}
% &
% % UpR
% \begin{tikzcd}[ampersand replacement=\&]
% A \& {A} \\
% {A} \& {A'}
% \arrow["\delta_c^{l,e}"', from=1-1, to=2-1]
% \arrow["f", from=1-2, to=2-2]
% \arrow[from=1-1, to=1-2, Rightarrow, no head]
% \arrow["c"', "\shortmid"{marking}, no head, from=2-1, to=2-2]
% \end{tikzcd}
% \end{tabular}
% \end{center}
% We call the first square $\upl$ and the second square $\upr$.
% \end{definition}
% \begin{definition}\label{def:quasi-right-representable}
% Let $d : B \rel B'$ be a computation relation. We say that $d$ is
% \emph{quasi-right-representable by} $f \in \ef(B', B)$
% if there exist perturbations $\delta_d^{l,p} \in \pe_B$ and
% $\delta_d^{r,p} \in \pe_{B'}$ such that the following squares commute:
% \begin{center}
% \begin{tabular}{ m{7em} m{7em} }
% % DnR
% \begin{tikzcd}[ampersand replacement=\&]
% {B} \& {B'} \\
% {B} \& {B}
% \arrow["\delta_d^{l,p}"', from=1-1, to=2-1]
% \arrow["g", from=1-2, to=2-2]
% \arrow["R", "\shortmid"{marking}, no head, from=1-1, to=1-2]
% \arrow[from=2-1, to=2-2, Rightarrow, no head]
% \end{tikzcd}
% &
% % DnL
% \begin{tikzcd}[ampersand replacement=\&]
% {B'} \& {B'} \\
% {B} \& {B'}
% \arrow["g"', from=1-1, to=2-1]
% \arrow["\delta_d^{r,p}", from=1-2, to=2-2]
% \arrow[from=1-1, to=1-2, Rightarrow, no head]
% \arrow["R"', "\shortmid"{marking}, no head, from=2-1, to=2-2]
% \end{tikzcd}
% \end{tabular}
% \end{center}
% We call the first square $\dnr$ and the second square $\dnl$.
% \end{definition}
With these definitions, we return to the more specific setting of a step-2
intensional model $\mathcal M$ and specify the new requirements for relations.
We require that there are functors $\upf : \ve \to \vf$ and $\dnf : \ee^{op} \to \ef$
Every value edge $c : A \rel A'$ must be quasi-left-representable by $\upf(c)$,
and every computation edge $d : B \rel B'$ is quasi-right-representable by $\dnf(d)$.
Besides the perturbations, one other difference between the extensional
and intensional versions of the representability axioms is that in the
......@@ -639,6 +738,7 @@ In the intensional setting, we do have horizontal composition of squares,
so we can take the simpler versions as primitive and derive the ones
involving composition.
\begin{comment}
Lastly, we require that the model satisfy a weak version of functoriality for
the CBPV connectives $U,F,\times,\to$.
First, we will need a definition:
......@@ -682,7 +782,7 @@ which we specify as follows:
\item $(cc') \to (dd') \qordeq (c \to d)(c' \to d')$
\item $(c_1c_1') \times (c_2c_2') \qordeq (c_1 \times c_2)(c_1'\times c_2')$
\end{itemize}
\end{comment}
We summarize the requirements of a step-3 model below:
......@@ -693,7 +793,8 @@ We summarize the requirements of a step-3 model below:
\item There are functors $\upf : \ve \to \vf$ and $\dnf : \ee^{op} \to \ef$ % TODO: image is thin?
\item Every value edge $c : A \rel A'$ is quasi-left-representable by $\upf(c)$ and
every computation edge $d : B \rel B'$ is quasi-right-representable by $\dnf(d)$.
\item The CBPV connectives $U,F,\times,\to$ are quasi-functorial on relations.
\item \eric{Do we need the quasi-functoriality of CBPV connectives on relations?}
% \item The CBPV connectives $U,F,\times,\to$ are quasi-functorial on relations.
\end{enumerate}
\end{definition}
......@@ -701,6 +802,7 @@ We summarize the requirements of a step-3 model below:
% F c \comp F c' = F(c \comp c')
% Add requirement: Either the model is functorial with respect to up/downcasts or with repsect to relations
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsubsection{The Dynamic Type}
......@@ -749,7 +851,7 @@ construction does not depend on the details of the previous ones.
% However, this process cannot proceed in isolation: some phases require
% additional inputs. We will make clear what data must be supplied to each phase.
\subsubsection{Adding Perturbations}
\subsubsection{Adding Perturbations}\label{sec:constructing-perturbations}
Suppose we have a \hyperref[def:step-1-model]{step-1 intensional model} $\mathcal{M}$.
Recall that a step-1 intensional model consists of a step-0 model (i.e., a
......@@ -763,7 +865,7 @@ Moreover, the push-pull property must hold for all
value relations $c$ and all computation relations $d$.
We claim that from a step-1 model, we can construct a step-2 model.
% TODO give overview
\eric{TODO give overview}
For the proof, see Lemma \ref{lem:step-1-model-to-step-2-model} in the Appendix.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
......@@ -773,7 +875,7 @@ For the proof, see Lemma \ref{lem:step-1-model-to-step-2-model} in the Appendix.
Now suppose we have a step-2 intensional model $\mathcal{M}$.
We claim that we can construct a \hyperref[def:step-3-model]{step-3 intensional model} $\mathcal{M'}$.
% TODO give overview
\eric{TODO give overview}
For the proof, see Lemma \ref{lem:step-2-model-to-step-3-model} in the Appendix.
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment