From e4c07041493a3cd01542ff5522ee20e79e390c0c Mon Sep 17 00:00:00 2001
From: Eric Giovannini <ecg19@seas.upenn.edu>
Date: Thu, 18 Jan 2024 17:55:36 -0500
Subject: [PATCH] begin discussion of abstract model constructions
---
paper-new/categorical-model.tex | 225 +++++++++++++++++++++++++++++---
1 file changed, 205 insertions(+), 20 deletions(-)
diff --git a/paper-new/categorical-model.tex b/paper-new/categorical-model.tex
index 9f48a66..818bd54 100644
--- a/paper-new/categorical-model.tex
+++ b/paper-new/categorical-model.tex
@@ -1,4 +1,4 @@
-\section{Abstract Categorical Models of Graduality}
+\section{Abstract Categorical Models of Graduality}\label{sec:abstract-models}
First, what is a categorical model of call-by-push-value? We will use
the following notion as our basic structure\footnote{There are models
@@ -123,13 +123,14 @@ That is, for the values, we have
$\rv : \mathcal V_f \to \mathcal V_{sq}$.
\end{enumerate}
-Likewise, we have an analogous definition for computations.
+Likewise, we have the analogous definitions for computations.
We write $c : A \rel A'$ to mean that $c \in \ob(\vsq)$ such that
-$\sv(c) = A$ and $\tv(A) = A'$.
+$\sv(c) = A$ and $\tv(c) = A'$.
+%
Likewise, let $c_i : A_i \rel A_i'$ and $c_o : A_o \rel A_o'$,
and let $f \in \vf(A_i, A_o)$ and $f' \in \vf(A_i', A_o')$.
-The judgment $\beta : f \ltdyn_{c_o}^{c_i} f'$ is defined to mean
+The notation $\beta : f \ltdyn_{c_o}^{c_i} f'$ is defined to mean
\begin{enumerate}
\item $\beta \in \vsq(c_i, c_o)$
@@ -153,6 +154,10 @@ Picorially, this is depicted as a commuting square:
\arrow["\alpha"{description}, draw=none, from=0, to=1]
\end{tikzcd}\]
+% Note: When the identity of the square $\beta$ is not important, we may omit it
+% and write $f \ltdyn_{c_o}^{c_i} f'$. In this case the meaning is that there exists
+% a square $\beta : f \ltdyn_{c_o}^{c_i} f'$.
+
Composition of squares $\beta : f \ltdyn_{c_2}^{c_1} g$ and $\beta' : f' \ltdyn_{c_3}^{c_2} g'$
corresponds to ``stacking'' the square for $\beta'$ below the square for $\beta$.
Fuctoriality of $s$ and $t$ ensure that the left and right sides of the resulting square are as expected,
@@ -170,6 +175,8 @@ All of the above holds in an analogous manner for the computations.
We will work in ``locally thin'' models where there is at most one
square with a given boundary.
That is, if $\beta, \beta' : f \ltdyn_{c_o}^{c_i} f'$, then $\beta = \beta'$.
+Thus, we may unambiguously omit the identity of the square, i.e., we may write
+$f \ltdyn_{c_o}^{c_i} f'$.
We also have a ``horizontal" composition operation on value edges and on computation edges.
That is, let
@@ -342,11 +349,13 @@ In summary, an extensional model consists of:
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Intensional Models}\label{sec:abstract-intensional-models}
An intensional model of gradual typing is defined similarly to an extensional model,
-with two key differences that will be discussed below.
+with a few key differences that will be discussed below.
%
The starting point is similar to that of the extensional model: an intensional model
will be given by a diagram in the category of CBPV objects, satisfying
@@ -372,16 +381,17 @@ In particular, this consists of a functor
$m_{\mathcal{V}} : \vsq \times_{\sv = \tv} \vsq \to \vsq$ for composition of value
relations/squares, and a functor $m_{\mathcal{E}} : \esq \times_{\se = \te} \esq \to \esq$
for composition of computation relations/squares.
+Furthermore, $s \circ m = s \circ \pi_1$ and $t \circ m = t \circ \pi_2$.
% If we spell this all out explicitly, we end up with a definition similar to the
% one for the extensional case, but now with the addition of a functor $m_{\mathcal{V}}$ for
% composition of value relations/squares and a functor $m_{\mathcal{E}}$ for
% composition of computation relations/squares.
-For the sake of ease of reference, we recap the definition of a step-1 model:
+For the sake of ease of reference, we recap the definition of a step-0 model:
\begin{definition}
- A \emph{step-1} model of intensional gradual typing consists of a category internal to the
+ A \emph{step-0} model of intensional gradual typing consists of a category internal to the
category of CBPV models.
\end{definition}
@@ -391,7 +401,7 @@ For the sake of ease of reference, we recap the definition of a step-1 model:
% But we now have horizontal composition of squares as well.
-\subsubsection{Bisimilarity}
+\subsubsection{Bisimilarity}\label{sec:abstract-model-bisimilarity}
Working intensionally means we need to take into consideration the steps
taken by terms. One consequence of this is that we need a way to specify
@@ -412,7 +422,7 @@ We can specify all of this abstractly via categories $\vsim$ and $\esim$ along w
functors $\rvsim : \vf \to \vsim$ and $\svsim, \tvsim : \vsim \to \vf$,
and likewise for computations.
Since bisimilarity of morphisms $f$ and $f'$ requires that they share source and target,
-we require that $\svsim$ and $\tvsim$ agree on objects and likewise for $\sesim and \tesim$.
+we require that $\svsim$ and $\tvsim$ agree on objects and likewise for $\sesim$ and $\tesim$.
Thus, the objects of $\vsim$ are identified with $\ob(\vf)$.
The morphisms of $\vsim$ are ``bisimilarity proofs'', analogous to the commuting squares of $\vsq$.
@@ -423,16 +433,26 @@ and $\text{sym}_{\mathcal{V}}^\bisim \circ \text{sym}_{\mathcal{V}}^\bisim$ is t
Likewise there is a symmetry endofunctor $\text{sym}_{\mathcal{E}}^\bisim : \esim \to \esim$.
% TODO explain what this means in terms of bisimilarity "squares"?
+In this setting, we write $\refl_A : A \bisim A$ to mean that $\refl_A \in \ob(\vsim)$,
+such that $\svsim(\refl_A) = A = \tvsim(\refl_A)$.
+Let $f, f' \in \vf(A_i, A_o)$.
+The judgment $\gamma : f \bisim_{A_i, A_o} f'$ is defined to mean:
+
+\begin{enumerate}
+ \item $\gamma \in \vsim(\refl_{A_i}, \refl_{A_o})$
+ \item $\svsim(\gamma) = f$
+ \item $\tvsim(\gamma) = f'$
+\end{enumerate}
% Spelling this all out concretely, for any pair...
-\begin{definition}
-A \emph{step-2 intensional model} consists of all the data of a step-1 intensional model along
+\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.
\end{definition}
-\subsubsection{Perturbations}
+\subsubsection{Perturbations}\label{sec:abstract-model-perturbations}
A second consequence of working intensionally is that the squares in the representable
properties must now involve a notion of ``delay" or ``perturbation'' in order to
@@ -492,8 +512,8 @@ forms a monoid under composition.
This is summarized below:
-\begin{definition}
- A \emph{step-3} model of intensional gradual typing consists of all the data of a step-2 model plus:
+\begin{definition}\label{def:step-2-model}
+ A \emph{step-2} model of intensional gradual typing consists of all the data of a step-1 model plus:
\begin{enumerate}
\item $\pv_A$ and a monoid homomorphism
\[ \ptbv_A : \pv_A \to \{ f \in \vf(A,A) \mid f \bisim \id \} \]
@@ -517,7 +537,8 @@ but as mentioned above, now there
are perturbations involved in order to keep both sides ``in lock-step".
The precise definitions are as follows.
-Let $c : A \rel A'$. We say that $c$ is \emph{quasi-left-representable by}
+\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:
@@ -544,8 +565,10 @@ $\delta_c^{r,e} \in \pv_{A'}$ such that the following squares commute:
\end{tikzcd}
\end{tabular}
\end{center}
+\end{definition}
-Similarly, let $d : B \rel B'$. We say that $d$ is
+\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:
@@ -573,7 +596,7 @@ $\delta_d^{r,p} \in \pe_{B'}$ such that the following squares commute:
\end{tikzcd}
\end{tabular}
\end{center}
-
+\end{definition}
Besides the perturbations, one other difference between the extensional
and intensional versions of the representability axioms is that in the
@@ -587,9 +610,9 @@ so we can take the simpler versions as primitive and derive the ones
involving composition (though we must be careful about the perturbations
when doing so!).
-\begin{definition}
- A \emph{step-4 intensional model}, or simply an \emph{intensional model}, consists
- of all the data of a step-3 intensional model, with the following additional data:
+\begin{definition}\label{def:step-3-model}
+ A \emph{step-3 intensional model} consists
+ of all the data of a step-2 intensional model, with the following additional data:
\begin{enumerate}
\item 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
@@ -598,4 +621,166 @@ when doing so!).
\end{definition}
+\subsubsection{The Dynamic Type}
+
+Now we can discuss what it means for an intensional model to model the dynamic type.
+
+\begin{definition}\label{def:step-4-model}
+ A \emph{step-4 intensional model}, or simply an \emph{intensional model}, consists
+ of all the data of a step-3 intensional model, along with
+ %a distinguished value object $D \in \ob(\vf)$ such that:
+ %
+ \begin{enumerate}
+ \item A distinguished value object $D \in \ob(\vf)$.
+ (By definition of a step-3 model, this means there is also a monoid $\pv_D$ of
+ perturbations and a homomorphism $\ptbv_D$.)
+ \item For each value type $A$, there is a value relation $\text{inj}_A : A \rel D$.
+ (By definition of a step-3 model, this relation satisfies the push-pull property and is
+ quasi-left-representable.)
+ \item If $c : A \rel A'$, then $\text{inj}_{A} = c \comp \text{inj}_{A'}$.
+ \end{enumerate}
+\end{definition}
+
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\subsection{Constructing an Extensional Model}\label{sec:extensional-model-construction}
+
+In the previous section, we have given the definition of an intensional model
+of gradual typing as a series of steps with each definition building on the previous one.
+%
+Here, we discuss how to construct an extensional model from an intensional model.
+We do so in several phases, beginning with a step-1 intensional model
+and ending with an extensional model.
+Moreover, this construction is \emph{modular}, in that each phase of the
+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.
+
+% Going from a step-1 intensional model $\mathcal{M}_1$ to a step-2 intensional model
+% requires defining a bisimilarity relation on the value morphisms and on
+% the computation morphisms of $\mathcal{M}_1$.
+% In particular, we need for every $A$ and $A'$ a reflexive, symmetric relation
+% $\bisim_{A,A'}$ on $\vf(A, A')$ and for every $B$ and $B'$ a reflexive, symmetric relation
+% $\bisim_{B,B'}$ on $\ef(B, B')$. Moreover, the relation must respect composition of morphisms.
+% This phase of the construction is quite simple, because it consists entirely of extra structure
+% supplied as input to the construction.
+
+\subsubsection{Adding 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
+category internal to the category of CBPV models), along with the necessary
+categories and functors for bisimilarity as discussed in Section
+\ref{sec:abstract-model-bisimilarity}.
+Further, recall that a \hyperref[def:step-2-model]{step-2 model} has everything
+a step-1 model has, with the addition of perturbation monoids $\pv_A$ for all
+$A$ and $\pe_B$ for all $B$.
+% These perturbations must be interpretable as endomorphisms via homomorphisms
+% $\ptb_A$ and $\ptb_B$,
+These perturbations must be interpretable via homomorphisms
+$\ptb_A$ and $\ptb_B$ as endomorphisms bisimilar to the identity,
+and moreover, the push-pull property must hold for all
+value relations $c$ and all computation relations $d$.
+
+% TODO do we really need all of this data?
+What ``external" data do we need to define such a model?
+Suppose we are given, for each value type $A$, a monoid $\pv_A$ with homomorphism
+$\ptb_A$ into the endomorphisms on $A$ bisimilar to the identity, and likewise, for
+each computation type $B$, a monoid $\pv_B$ and homomorphism $\ptb_B$.
+Furthermore, suppose we are given, for each value type $A$, a distinguished endomorphism
+$\delta_A \in \ef(FA, FA)$ such that $\delta_A \bisim \id_{FA}$.
+Finally, suppose that each value relation $c : A \rel A'$ satisfies the push-pull property
+and likewise for each computation relation $d : B \rel B'$.
+
+Then we claim that from the above data, we can construct a step-2 intensional model.
+For the proof, see Lemma \ref{lem:step-1-model-to-step-2-model} in the Appendix.
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\subsubsection{Adding Quasi-Representability}
+
+Now suppose we have a step-2 intensional model $\mathcal{M}$.
+We will describe how to construct a \hyperref[def:step-3-model]{step-3 intensional model} $\mathcal{M'}$.
+We begin with a definition.
+
+\begin{definition}[representation structure]
+Let $c : A \rel A'$ be a value relation. A \emph{left-representation structure} $\rho^L_c$ for $c$ consists of
+a value morphism $u \in \vf(A, A')$ such that $c$ is quasi-left-representable by $u$ (see Definition \ref{def:quasi-left-representable}).
+
+Likewise, let $d : B \rel B'$. A \emph{right-representation structure} $\rho^R_d$ for $d$ consists of
+a computation morphism $d \in \ef(B', B)$ such that $d$ is quasi-right-representable by $d$ (see Definition \ref{def:quasi-right-representable}).
+\end{definition}
+
+(Notice that the direction of the morphism is opposite in the definition of
+right-representation structure.)
+
+We now describe the construction of a step-3 model $\mathcal M'$.
+The objects of $\mathcal M'$ are defined to be the same as the objects of the
+step-2 model $\mathcal M$.
+The value and computation morphisms in $\mathcal M'$ are the same as those of
+$\mathcal M$.
+A value relation is defined to be a pair $(c, \rho^L_c)$ with $c$ a value
+relation in $\mathcal M$ and $\rho^L_c$ a left-representation structure for $c$.
+Likewise, a computation relation is defined to be a pair $(d, \rho^R_d)$ with
+$d$ a computation relation in $\mathcal M$ and $\rho^R_d$ a right-representation
+structure for $d$.
+Lastly, morphisms of value relations (i.e., value squares) are defined by simply
+ignoring the representation structure. That is, a morphism of value relations
+$\alpha \in \vsq'((c, \rho^L_c), (c' \rho^L_{c'}))$ is simply a morphism of value
+relations in $\vsq(c, c')$. Likewise for computations.
+
+Now we define the functors $F$, $U$, and $\arr$.
+On objects, the behavior is the same as the respective functors in $\mathcal M$.
+For relations, we define
+$\Fsq' (c, \rho^L_c) = (\Fsq c, \rho^R_{F c})$ and
+$\Usq' (d, \rho^R_d) = (\Usq d, \rho^L_{U d})$.
+We define $(c, \rho^L_c) \arr (d, \rho^R_d) = (c \arr d, \rho^R_{c \arr d})$.
+
+
+
+We now verify that the construction meets the requirements of a step-3 model.
+First, we check that composition of value relations (resp. computation relations)
+is well-defined. This might seem obvious, but there is actually a subtlety here:
+what should the representation structure be for the composition?
+
+
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\subsubsection{Defining an Extensional Model}
+
+Finally, suppose $\mathcal M$ is a step-3 intensional model.
+We now describe how to build an extensional model.
+
+The idea is to define an extensional model whose squares are the ``bisimilarity-closure''
+of the squares of the provided intensional model $\mathcal M$.
+
+The categories $\vf$, $\ef$ are the same as those of $\mathcal M$.
+Additionally, the objects of $\vsq$ and $\esq$, i.e., the value and
+computation relations, are the same.
+The difference arises in the \emph{morphisms} of $\vsq$ and $\esq$,
+i.e., the commuting squares. In particular, a morphism
+$\alpha_e \in \vsq'(c_i, c_o)$ with source $f$ and target $g$ is given by:
+\begin{itemize}
+ \item a morphism $f' \in \vf(A_i, A_o)$ with $f \bisim f'$.
+ \item a morphism $g' \in \vf(A_i', A_o')$ with $g \bisim g'$.
+ \item a square $\alpha_i \in \vsq(c_i, c_o)$ with source $f'$ and target $g'$.
+\end{itemize}
+
+Using our existing notation, we say that $f \le_{c_o}^{c_i} g$ if there exist $f'$ and $g'$ such that
+
+\[ f \bisim_{A_i,A_o} f' \ltdyn_{c_o}^{c_i} g' \bisim_{A_i',A_o'} g. \]
+
+We make the analogous construction for the computation squares.
+
+Next, we check that the requirements of an extensional model are satisfied.
+In particular, we need to verify the representability properties.
+We define functors $\upf$ and $\dnf$
+
+
+
--
GitLab