Skip to content
Snippets Groups Projects
Commit bbc27e35 authored by Max New's avatar Max New
Browse files

add description of additives

parent b6325554
Branches
Tags
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 248 additions and 53 deletions
gcbpv.tex
+ 248
− 53
View file @ bbc27e35
\documentclass{article}
\usepackage{float}
\usepackage{amsmath,amssymb}
\usepackage{tikz-cd}
\usepackage{mathpartir}
......@@ -21,6 +22,8 @@
\newcommand{\ltdynv}{\mathrel{\sqsubseteq_V}}
\newcommand{\ltdynt}{\mathrel{\sqsubseteq_T}}
\newcommand{\pair}[2]{\{ \pi \mapsto {#1} \pipe \pi' \mapsto {#2}\}}
\newcommand{\dyn}{{?}}
\newcommand{\dynv}{{?}}
\newcommand{\dync}{\u {\text{?`}}}
......@@ -58,7 +61,7 @@ Gradual Call-by-push-value adds an ordering form for each of these
judgments: value type dynamism, computation type dynamism, value
dynamism, term dynamism and stack dynamism.
\begin{figure}
\begin{figure}[H]
\begin{mathpar}
A \vtype \and
......@@ -124,7 +127,7 @@ Additionally, there are rules making each of the orderings into
\emph{preorders}: i.e., there are reflexivity and transitivity rules
for each.
\begin{figure}
\begin{figure}[H]
\begin{mathpar}
\inferrule
{}
......@@ -141,10 +144,10 @@ for each.
{\Gamma \vdash v[\gamma] : A}
\inferrule
{\Phi' \vdash v_1 \ltdyn v_2 : A_1 \ltdyn A_2\and
{\Phi' \vdash v_1 \ltdyn v_2 : A_1 \ltdyn A_2\\
\forall (x_1' \ltdyn x_2' : A_1' \ltdyn A_2' \in \Phi'). \Phi \vdash \gamma_1(x_1') \ltdyn \gamma_2(x_2') : A_1' \ltdyn A_2'
}
{\Phi \vdash v_1[\gamma_1] \ltdyn v_2[\gamma_2] : A_1 \ltdyn A_2}
{\Phi \vdash v_1[\gamma_1] \ltdyn v_2[\gamma_2] : A_1 \ltdyn A_2}\\
\inferrule
{\gamma : \prod_{x' : A' \in \Gamma'} \Gamma \vdash \cdot : A'\and
......@@ -153,10 +156,10 @@ for each.
{\Gamma \vdash M[\gamma] : \u B}
\inferrule
{\Phi' \vdash M_1 \ltdyn M_2 : \u B_1 \ltdyn \u B_2\and
{\Phi' \vdash M_1 \ltdyn M_2 : \u B_1 \ltdyn \u B_2\\
\forall (x_1' \ltdyn x_2' : A_1' \ltdyn A_2' \in \Phi'). \Phi \vdash \gamma_1(x_1') \ltdyn \gamma_2(x_2') : A_1' \ltdyn A_2'
}
{\Phi \vdash M_1[\gamma_1] \ltdyn M_2[\gamma_2] : \u B_1 \ltdyn \u B_2}
{\Phi \vdash M_1[\gamma_1] \ltdyn M_2[\gamma_2] : \u B_1 \ltdyn \u B_2}\\
\inferrule
{\gamma : \prod_{x' : A' \in \Gamma'} \Gamma \vdash \cdot : A'\and
......@@ -165,10 +168,10 @@ for each.
{\Gamma\pipe \u B \vdash S[\gamma] : \u C}
\inferrule
{\Phi'\pipe \hole\ltdyn \hole : \u B_1 \ltdyn \u B_2 \vdash S_1 \ltdyn S_2 : \u C_1 \ltdyn \u C_2\and
{\Phi'\pipe \hole\ltdyn \hole : \u B_1 \ltdyn \u B_2 \vdash S_1 \ltdyn S_2 : \u C_1 \ltdyn \u C_2\\
\forall (x_1' \ltdyn x_2' : A_1' \ltdyn A_2' \in \Phi'). \Phi \vdash \gamma_1(x_1') \ltdyn \gamma_2(x_2') : A_1' \ltdyn A_2'
}
{\Phi \pipe \hole\ltdyn \hole : \u B_1 \ltdyn \u B_2 \vdash S_1[\gamma_1] \ltdyn S_2[\gamma_2] : \u C_1 \ltdyn \u C_2}
}
{\Phi \pipe \hole\ltdyn \hole : \u B_1 \ltdyn \u B_2 \vdash S_1[\gamma_1] \ltdyn S_2[\gamma_2] : \u C_1 \ltdyn \u C_2}\\
\inferrule{}{\Gamma\pipe \hole : \u B \vdash \hole : \u B}
......@@ -185,7 +188,7 @@ for each.
\caption{GCBPV Basic Judgmental Rules 1 (Identities, Substitutions)}
\end{figure}
\begin{figure}
\begin{figure}[H]
\begin{mathpar}
\inferrule
{}
......@@ -282,7 +285,7 @@ be \emph{derived} using the $F,U$ adjoint type constructors, which
will both be defined to be \emph{monotone} with respect to type
dynamism.
\begin{figure}
\begin{figure}[H]
\begin{mathpar}
\inferrule
{\Gamma \vdash v : A_1 \and A_1 \ltdyn A_2}
......@@ -344,7 +347,7 @@ theorem that monotone functors preserve representability, so we get
that for $\u F$ and $U$ types, we have both an upcast and a downcast
from a preordering.
\begin{figure}
\begin{figure}[H]
\begin{mathpar}
\inferrule
{A \vtype}
......@@ -433,7 +436,7 @@ from a preordering.
\caption{Adjunction Constructors (Stoupified) Beta and Eta are presented with and without cuts}
\end{figure}
\begin{figure}
\begin{figure}[H]
\begin{mathpar}
\inferrule
{\Gamma, x : A_1 \vdash \upcast {A_1} {A_2} x : A_2}
......@@ -462,7 +465,7 @@ from a preordering.
\caption{Functoriality Preserves Representability (Theorem Statments)}
\end{figure}
\begin{figure}
\begin{figure}[H]
\begin{mathpar}
\inferrule*
{\hole \ltdyn \lett x = \hole; \ret x \and
......@@ -514,8 +517,12 @@ from a preordering.
\end{figure}
It seems like the easiest thing to do is have a most dynamic function
type and product type, but I'm not sure if it's really necessary.
%
Explore this in the models.
\begin{figure}
\begin{figure}[H]
\begin{mathpar}
\inferrule{}{\dynv \vtype}
......@@ -528,57 +535,193 @@ from a preordering.
\caption{Dynamic Types}
\end{figure}
\section{Models}
\section{Connectives and Contract Uniqueness Theorems}
A model of gcbpv consists of a preorder-enriched cbpv model with
specified interpretations of $\dynv, \dync$ and the following
precision judgments. Note that we don't need $0 \ltdyn \dynv$ and
$\top \ltdyn \dync$ because those are uniquely determined by the
universal property.
Next we consider the multiplicative and additive connectives of
gradual call-by-push value, and their corresponding contracts.
%
We start with the additives because they are comparatively easier.
\begin{mathpar}
1 \ltdyn \dynv
\subsection{Additive Connectives: Positive Sum, Negative Product}
\dynv \times \dynv \ltdyn \dynv
\dynv + \dynv \ltdyn \dynv
First, we introduce the sum type, which is a \emph{value} type
constructor.
%
It has two value constructors $\sigma$ and $\sigma'$ for the left and
right injections.
%
It's universal property is given by case analysis.
%
It should have this universal property \emph{any} time it appears as a
variable, which means that we need case analysis values, computations
and stacks.
%
Having two different, seemingly unrelated forms of pattern matching
looks problematic, but they are not unrelated, we can show that
substituting a value with a pattern match into a term is equivalent to
first lifting the pattern match out of the term and then substituting.
%
This
\begin{align*}
M[\case v \{ \sigma x \mapsto v_k \pipe \sigma' x' \mapsto v_k' \}/x_+ ]
&=
M[\case y \{ \sigma x \mapsto v_k \pipe \sigma' x' \mapsto v_k' \}/x_+][v/y]\\
&\equidyn
(\case y \{ \\ &\qquad
\sigma x \mapsto M[\case \sigma x \{ \sigma x \mapsto v_k \pipe \sigma' x' \mapsto v_k' \}/x_+]\\ &\qquad
\pipe \sigma' x' \mapsto M[\case \sigma' x' \{ \sigma x \mapsto v_k \pipe \sigma' x' \mapsto v_k' \}/x_+]\\ &\quad
\})[v/y] \\
&\equidyn
(\case y \{ \\ &\qquad
\sigma x \mapsto M[v_k /x_+]\\ &\qquad
\pipe \sigma' x' \mapsto M[v_k'/x_+]\\ &\quad
\})[v/y] \\
&=
\case v \{ \sigma x \mapsto M[v_k/x_+] \pipe \sigma' x' \mapsto M[v_k'/x_+] \}
\end{align*}
\begin{figure}[H]
\begin{mathpar}
\inferrule
{A \vtype \and A' \vtype}
{A + A' \vtype}
\inferrule
{A_1 \ltdyn A_2 \and A_1' \ltdyn A_2'}
{A_1 + A_1' \ltdyn A_2 + A_2'}\\
U \dync \ltdyn \dynv\\
\dync \wedge \dync \ltdyn \dync
\inferrule
{\Gamma \vdash v : A}
{\Gamma \vdash \sigma_{A,A'} v : A + A'}
\dynv \to \dync \ltdyn \dync
\inferrule
{\Gamma \vdash v' : A'}
{\Gamma \vdash \sigma'_{A,A'} v' : A + A'}
\u F \dynv \ltdyn \dync
\end{mathpar}
\inferrule
{v_1 \ltdyn v_2 : A_1 \ltdyn A_2 \and A_1' \ltdyn A_2'}
{\sigma v_1 \ltdyn \sigma v_2 : A_1 + A_1' \ltdyn A_2 + A_2'}
Next, we will use poset CBPV as a metalanguage and compile GCBPV into
poset CBPV with recursive types.
\inferrule
{v_1' \ltdyn v_2' : A_1' \ltdyn A_2' \and A_1 \ltdyn A_2}
{\sigma' v_1' \ltdyn \sigma' v_2' : A_1 + A_1' \ltdyn A_2 + A_2'}
\begin{mathpar}
\dynv(X, \u Y) = 1 + (X \times X) + (X + X) + U \u Y
\inferrule
{\Gamma \vdash v : A + A'\and
\Gamma, x:A \vdash v_k : A_3\and
\Gamma, x':A' \vdash v_k' : A_3}
{\Gamma \vdash \case v \{\sigma x \mapsto v_k \pipe \sigma' x' \mapsto v_k'\} : A_3}
\dync(X, \u Y) = (\u Y \wedge \u Y) \wedge (X \to \u Y) \wedge \u F X
\inferrule
{\Phi \vdash v_1 \ltdyn v_2 : A_1 + A_1' \ltdyn A_2 + A_2'\\
\Phi, x_1\ltdyn x_1:A_1 \ltdyn A_1 \vdash v_{k,1} \ltdyn v_{k,2} : A_3 \ltdyn A_4\\
\Phi, x_1'\ltdyn x_1':A_1' \ltdyn A_1' \vdash v_{k,1}' \ltdyn v_{k,2}' : A_3 \ltdyn A_4}
{\Phi \vdash \case v_1 \{\sigma x_1 \mapsto v_{k,1} \pipe \sigma' x_1' \mapsto v_{k,1}'\}
\ltdyn \case v_2 \{\sigma x_2 \mapsto v_{k,2} \pipe \sigma' x_2' \mapsto v_{k,2}'\} : A_3 \ltdyn A_4}
\dynv = \mu X. \dynv(X, \u \mu \u Y. \dync(X, \u Y))
\dync = \mu \u Y. \dync(\mu X. \dynv(X, \u Y), \u Y)
\end{mathpar}
\inferrule
{\Gamma \vdash v : A + A'\and
\Gamma, x:A\pipe \Delta \vdash M : \u B\and
\Gamma, x':A' \pipe \Delta \vdash M' : \u B}
{\Gamma\pipe \Delta \vdash \case v \{\sigma x \mapsto M \pipe \sigma' x' \mapsto M'\} : \u B}
We call the cases of $\dynv$ the ``tag types'' and abbreviate them $T$
because they are the tags of the sum, and the cases of the $\dync$ the
``message types'' and abbreviate them $\u M$ because they are the
possible messages of the ``coinductive'' dynamic type.
%
We implement the appropriate casts and their adjoints as follows
\inferrule
{\Phi \vdash v_1 \ltdyn v_2 : A_1 + A_1' \ltdyn A_2 + A_2'\\
\Phi, x_1\ltdyn x_1:A_1 \ltdyn A_1 \pipe \Psi \vdash M_1 \ltdyn M_2 : \u B_1 \ltdyn \u B_2 \\
\Phi, x_1'\ltdyn x_1':A_1' \ltdyn A_1'\pipe\Psi \vdash M_1' \ltdyn M_2' : \u B_1 \ltdyn \u B_2}
{\Phi\pipe\Psi \vdash \case v_1 \{\sigma x_1 \mapsto M_1 \pipe \sigma' x_1' \mapsto M_1'\}
\ltdyn \case v_2 \{\sigma x_2 \mapsto M_2 \pipe \sigma' x_2' \mapsto M_2'\} : \u B_1 \ltdyn \u B_2}
\[ \upcast T \dynv x = \roll \sigma_T x \]
\[ \dncast {\u F T} {\u F \dynv} \hole = \lett x = \hole; \case \unroll x \{ \sigma_T y \mapsto y; \sigma_{T'} y \mapsto \err \} \]
\case \sigma v \{ \sigma x \mapsto v_k \pipe \sigma' x' \mapsto v_k' \} \equidyn v_k[v/x]\\
\case \sigma' v' \{ \sigma x \mapsto v_k \pipe \sigma' x' \mapsto v_k' \} \equidyn v_k'[v'/x']\\
\case \sigma v \{ \sigma x \mapsto M \pipe \sigma' x' \mapsto M' \} \equidyn M[v/x]\\
\case \sigma' v' \{ \sigma x \mapsto M \pipe \sigma' x' \mapsto M' \} \equidyn M'[v'/x']\\
\[ \dncast {\u M} \dync \hole = \pi_{\u M} \u \unroll \hole \]
\[ \upcast {U \u M} {U \dync} x = \u \roll \thunk [ \pi_{\u M} \mapsto \force x; \pi_{\u M'} \mapsto \err ] \]
\inferrule
{x_+ : A + A'}
{v \equidyn \case x_+ \{ \sigma x \mapsto v[\sigma x/x+_] \pipe \sigma' x' \mapsto v[\sigma' x'/x_+] \}}
\inferrule
{x_+ : A + A'}
{M \equidyn \case x_+ \{ \sigma x \mapsto M[\sigma x/x+_] \pipe \sigma' x' \mapsto M[\sigma' x'/x_+] \}}
\end{mathpar}
\caption{Binary Sum}
\end{figure}
\begin{figure}[H]
\begin{mathpar}
\inferrule
{B \ctype \and B' \ctype}
{B \wedge B' \ctype}
\inferrule
{B_1 \ltdyn B_2 \and B_1' \ltdyn B_2'}
{B_1 \wedge B_1' \ltdyn B_2 \wedge B_2'}
\inferrule
{\Gamma\pipe\Delta \vdash M : \u B\and
\Gamma\pipe\Delta \vdash M' : \u B'}
{\Gamma\pipe \Delta \vdash \pair M {M'} : \u B \wedge \u B'}
\inferrule
{\Phi\pipe\Psi \vdash M_1 \ltdyn M_2 : \u B_1 \ltdyn \u B_2 \\
\Phi\pipe\Psi \vdash M_1' \ltdyn M_2' : \u B_1' \ltdyn \u B_2'}
{\Phi\pipe \Psi \vdash \pair {M_1} {M_1'} \ltdyn \pair {M_2} {M_2'} : \u B_1 \wedge \u B_1' \ltdyn \u B_2 \wedge \u B_2'}
\inferrule
{\Gamma \pipe \Delta \vdash M : \u B \wedge \u B'}
{\Gamma \pipe \Delta \vdash \pi M : \u B}
\begin{figure}
\inferrule
{\Gamma \pipe \Delta \vdash M : \u B \wedge \u B'}
{\Gamma \pipe \Delta \vdash \pi' M : \u B'}
\inferrule
{\Phi \pipe \Psi \vdash M_1 \ltdyn M_2 : \u B_1 \wedge \u B_1' \ltdyn \u B_2 \wedge \u B_2'
\and \u B_1 \ltdyn \u B_2 \and \u B_1' \ltdyn \u B_2'}
{\Phi \pipe \Psi \vdash \pi M_1 \ltdyn \pi M_2 : \u B_1 \ltdyn \u B_2}
\inferrule
{\Phi \pipe \Psi \vdash M_1 \ltdyn M_2 : \u B_1 \wedge \u B_1' \ltdyn \u B_2 \wedge \u B_2'
\and \u B_1 \ltdyn \u B_2 \and \u B_1' \ltdyn \u B_2'}
{\Phi \pipe \Psi \vdash \pi' M_1 \ltdyn \pi' M_2 : \u B_1 \ltdyn \u B_2}
\pi \pair M {M'} \equidyn M\and
\pi' \pair M {M'} \equidyn M'\\
\inferrule
{M : \u B \wedge \u B'}
{M \equidyn \pair {\pi M}{\pi' M}}
\end{mathpar}
\caption{Binary Computation Product}
\end{figure}
\begin{figure}[H]
\begin{mathpar}
\upcast{A_1 + A_1'}{A_2 + A_2'} x_{+,1} \equidyn\\
\case x_{+,1} \{ \sigma x \mapsto \upcast {A_1} {A_2} \pipe \sigma' x' \mapsto \upcast {A_1'} {A_2'} \}\\
\dncast{\u F(A_1 + A_1')}{\u F(A_2 + A_2')} \bullet \equidyn \lett x_{+,2} = \bullet; \\ \case x_{+,2} \{
\sigma x_2 \mapsto \dncast{\u F A_1}{\u F A_2}\ret x_2
\pipe \sigma' x_2' \mapsto \dncast{\u F A_1'}{\u F A_2'}\ret x_2'
\}
\dncast{\u B_1 \wedge \u B_1'}{\u B_2 \wedge \u B_2'}\bullet \equidyn \pair {\dncast{\u B_1}{\u B_2}\pi\bullet}{\dncast{\u B_1'}{\u B_2'}\pi'\bullet}\\
\upcast{U({\u B_1 \wedge \u B_1'})}{U({\u B_2 \wedge \u B_2'})}x_{\wedge} \equidyn\\
\pair
{\force \upcast{U \u B_1}{U \u B_2}\thunk \pi\force x_{\wedge}}
{\force \upcast{U \u B_1'}{U \u B_2'}\thunk \pi'\force x_{\wedge}}
\end{mathpar}
\caption{Binary Sum and Binary Computation Product Contract Uniqueness Theorems}
\end{figure}
\begin{figure}[H]
\begin{mathpar}
\inferrule
{A \vtype \and \u B \ctype}
......@@ -609,7 +752,7 @@ We implement the appropriate casts and their adjoints as follows
\caption{Function Type}
\end{figure}
\begin{figure}
\begin{figure}[H]
\begin{mathpar}
\inferrule
{}
......@@ -627,6 +770,58 @@ We implement the appropriate casts and their adjoints as follows
\caption{Function Contract Theorem, Proof}
\end{figure}
\section{Models}
A model of gcbpv consists of a preorder-enriched cbpv model with
specified interpretations of $\dynv, \dync$ and the following
precision judgments. Note that we don't need $0 \ltdyn \dynv$ and
$\top \ltdyn \dync$ because those are uniquely determined by the
universal property.
\begin{mathpar}
1 \ltdyn \dynv
\dynv \times \dynv \ltdyn \dynv
\dynv + \dynv \ltdyn \dynv
U \dync \ltdyn \dynv\\
\dync \wedge \dync \ltdyn \dync
\dynv \to \dync \ltdyn \dync
\u F \dynv \ltdyn \dync
\end{mathpar}
Next, we will use poset CBPV as a metalanguage and compile GCBPV into
poset CBPV with recursive types.
\begin{mathpar}
\dynv(X, \u Y) = 1 + (X \times X) + (X + X) + U \u Y
\dync(X, \u Y) = (\u Y \wedge \u Y) \wedge (X \to \u Y) \wedge \u F X
\dynv = \mu X. \dynv(X, \u \mu \u Y. \dync(X, \u Y))
\dync = \mu \u Y. \dync(\mu X. \dynv(X, \u Y), \u Y)
\end{mathpar}
We call the cases of $\dynv$ the ``tag types'' and abbreviate them $T$
because they are the tags of the sum, and the cases of the $\dync$ the
``message types'' and abbreviate them $\u M$ because they are the
possible messages of the ``coinductive'' dynamic type.
%
We implement the appropriate casts and their adjoints as follows
\[ \upcast T \dynv x = \roll \sigma_T x \]
\[ \dncast {\u F T} {\u F \dynv} \hole = \lett x = \hole; \case \unroll x \{ \sigma_T y \mapsto y; \sigma_{T'} y \mapsto \err \} \]
\[ \dncast {\u M} \dync \hole = \pi_{\u M} \u \unroll \hole \]
\[ \upcast {U \u M} {U \dync} x = \u \roll \thunk [ \pi_{\u M} \mapsto \force x; \pi_{\u M'} \mapsto \err ] \]
\end{document}
%% Local Variables:
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment