From bbc27e359971307e2cc766f4ef04570e992d720d Mon Sep 17 00:00:00 2001
From: Max New <maxsnew@gmail.com>
Date: Wed, 25 Apr 2018 14:11:10 -0400
Subject: [PATCH] add description of additives
---
gcbpv.tex | 301 ++++++++++++++++++++++++++++++++++++++++++++----------
1 file changed, 248 insertions(+), 53 deletions(-)
diff --git a/gcbpv.tex b/gcbpv.tex
index f014685..5ed9817 100644
--- a/gcbpv.tex
+++ b/gcbpv.tex
@@ -1,5 +1,6 @@
\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:
--
GitLab