From 02c0501061f3e6c4c27ce2cc2e5f319b08b0c7f5 Mon Sep 17 00:00:00 2001
From: Max New <maxsnew@gmail.com>
Date: Mon, 2 Jul 2018 12:59:41 -0400
Subject: [PATCH] more prose in axiomatic graduality section
---
paper/gtt.tex | 437 ++++++++++++++++++++++++++------------------------
1 file changed, 231 insertions(+), 206 deletions(-)
diff --git a/paper/gtt.tex b/paper/gtt.tex
index 8f165b8..e3851e6 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -2491,7 +2491,7 @@ We break down this proof into 3 major steps.
\begin{enumerate}
\item (This section) We translate GTT into a statically
typed CBPV language where the casts of GTT are translated to
- ``contracts'' in GTT: i.e., ordinary functions that implement the
+ ``contracts'' in GTT: i.e., CBPV terms that implement the type
checking. The CBPV language has an inequational theory and we
translate proofs in GTT to proofs in CBPV. In fact we give multiple
translations by varying the structure of the dynamic type.
@@ -2510,8 +2510,8 @@ We break down this proof into 3 major steps.
\end{enumerate}
By composing these, we get a model of GTT where equidynamism is sound
-for observational and an operational semantics that satisfies the
-graduality theorem.
+for observational equivalence and an operational semantics that
+satisfies the graduality theorem.
\subsection{Call-by-push-value}
@@ -3273,7 +3273,7 @@ dynamism relation.
\begin{figure}
\begin{mathpar}
- x:\sem{A} \vdash \sem{\upcast{A}{A'}} : \sem{A'}\\
+ x:\sem{A} \vdash \sem{\upcast{A}{A'}} : \sem{A'}\and
\bullet:\sem{\u B'} \vdash \sem{\dncast{\u B}{\u B'}} : \sem{\u B}\\
\begin{array}{rcl}
x : 0 \vdash \supcast{0}{A} & = & \absurd x\\
@@ -3285,22 +3285,31 @@ dynamism relation.
x : \sem{A} \vdash \sem{\upcast{A}{\dynv}} & = & \sem{\upcast{A}{\lfloor A \rfloor}}[{\sem{\upcast{G}{\dynv}}}/x]\\
\bullet: \u F\dynv \vdash \sdncast{A}{\dynv} &=& \sdncast{A}{\floor A}[{\sdncast{\floor A}{\dynv}}]\\
x : \sem{A_1} + \sem{A_2} \vdash \sem{\upcast{A_1 + A_2}{A_1' + A_2'}}
- & = & \caseofXthenYelseZ x {x_1. \sem{\upcast{A_1}{A_1'}}[x_1/x]}{x_2. \sem{\upcast{A_2}{A_2'}}[x_2/x]}\\
+ & = & \caseofX x \\
+ && \thenY{x_1. \sem{\upcast{A_1}{A_1'}}[x_1/x]}\\
+ && \elseZ{x_2. \sem{\upcast{A_2}{A_2'}}[x_2/x]}\\
\bullet : \sem{A_1} + \sem{A_2} \vdash
\sem{\dncast{\u F(A_1 + A_2)}{\u F(A_1' + A_2')}}
&=&
- \bindXtoYinZ \bullet {x'} {\caseofXthenYelseZ {x'} {x_1'. \bindXtoYinZ {(\sdncast{\u FA_1}{\u F A_1'}\ret x_1')} {x_1} \ret x_1}{x_2'. \bindXtoYinZ {(\sdncast{\u FA_2}{\u F A_2'}\ret x_2')} {x_2} \ret x_2}}\\
+ \bindXtoYinZ \bullet {x'} \caseofX {x'}\\
+ &&\thenY{x_1'. \bindXtoYinZ {(\sdncast{\u FA_1}{\u F A_1'}\ret x_1')} {x_1} \ret x_1}\\
+ &&\elseZ{x_2'. \bindXtoYinZ {(\sdncast{\u FA_2}{\u F A_2'}\ret x_2')} {x_2} \ret x_2}\\
x : 1 \vdash \supcast{1}{1} &=& x\\
\bullet : \u F 1 \vdash \sdncast{\u F1}{\u F1} &=& x\\
- x : \sem{A_1}\times\sem{A_2} \vdash \sem{\upcast{A_1\times A_2}{A_1'\times A_2'}} &=& \pmpairWtoXYinZ x {x_1}{x_2} (\supcast{A_1}{A_1'}[x_1], \supcast{A_2}{A_2'}[x_2])\\
+ x : \sem{A_1}\times\sem{A_2} \vdash \sem{\upcast{A_1\times A_2}{A_1'\times A_2'}} &=& \pmpairWtoXYinZ x {x_1}{x_2}\\
+ &&(\supcast{A_1}{A_1'}[x_1], \supcast{A_2}{A_2'}[x_2])\\
\bullet \vdash \sdncast{\u F(A_1 \times A_2)}{\u F(A_1' \times A_2')}
&=&
- \bindXtoYinZ \bullet {x'} \pmpairWtoXYinZ {x'} {x_1'}{x_2'}
- \bindXtoYinZ {\sdncast{\u FA_1}{\u FA_1'}\ret x_1'} {x_1}
- \bindXtoYinZ {\sdncast{\u FA_2}{\u FA_2'}\ret x_2'} {x_2}
+ \bindXtoYinZ \bullet {x'} \pmpairWtoXYinZ {x'} {x_1'}{x_2'}\\
+ &&
+ \bindXtoYinZ {\sdncast{\u FA_1}{\u FA_1'}\ret x_1'} {x_1}\\
+ &&
+ \bindXtoYinZ {\sdncast{\u FA_2}{\u FA_2'}\ret x_2'} {x_2}\\
+ &&
\ret(x_1,x_2)\\
x : U\u F \sem{A} \vdash \sem{\upcast{U\u F A}{U \u F A'}} &=&
- \thunk ({\bindXtoYinZ {\force x} y \ret \sem{\upcast{A}{A'}}[y/x]})\\\\
+ \thunk (\bindXtoYinZ {\force x} y\\
+ &&\qquad\ret \sem{\upcast{A}{A'}}[y/x])\\\\
% Computation constructor upcasts
\bullet : \u B \vdash \sdncast{\top}{\u B} &=& \{ \}\\
x:U\top \vdash \supcast{U\top}{U\u B} &=& \thunk \err\\
@@ -3310,17 +3319,21 @@ dynamism relation.
x:U\u G \vdash \supcast{U\u G}{U\dync} &=& \rho_{up}(\u G)\\
\bullet : \dync \vdash \sdncast{\u B}{\dync} &=& \sdncast{\u B}{\floor {\u B}}[\sdncast{\floor{\u B}}{\dync}]\\
x:U\dync \vdash \supcast{U\u B}{U\dync}&=& \supcast{U\floor{\u B}}{U\dync}[\supcast{U\u B}{U\floor{\u B}}]\\
- \bullet : \sem{\u B_1'}\with \sem{\u B_2'}\vdash \sdncast{\u B_1\with\u B_2}{\u B_1'\with\u B_2'} &=& \pair{\sdncast{\u B_1}{\u B_1'}\pi\bullet}{\sdncast{\u B_2}{\u B_2'}\pi'\bullet}\\
+ \bullet : \sem{\u B_1'}\with \sem{\u B_2'}\vdash \sdncast{\u B_1\with\u B_2}{\u B_1'\with\u B_2'} &=& \pairone{\sdncast{\u B_1}{\u B_1'}\pi\bullet}\\
+ &&\pairtwo{\sdncast{\u B_2}{\u B_2'}\pi'\bullet}\\
x : U(\sem{\u B_1}\with \sem{\u B_2}) \vdash
{\supcast{U(\u B_1 \with \u B_2)}{U(\u B_1'\with\u B_2')}}
&=&
- \thunk\pair{\force \supcast{\u B_1}{\u B_1'}{(\thunk \pi\force x)}}
- {\force \supcast{\u B_2}{\u B_2'}{(\thunk \pi'\force x)}}\\
+ \thunk\\
+ &&\pairone{\force \supcast{\u B_1}{\u B_1'}{(\thunk \pi\force x)}}\\
+ &&\pairtwo{\force \supcast{\u B_2}{\u B_2'}{(\thunk \pi'\force x)}}\\
\bullet \vdash \sdncast{A \to \u B}{A' \to \u B'} &=& \lambda x:A. \sdncast{\u B}{\u B'}{(\bullet\, x)}\\
f : U(\sem{A} \to \sem{\u B}) \vdash
\supcast{U(A \to \u B)}{U(A' \to \u B')}
&=&
- \thunk\lambda x':A'. \bindXtoYinZ {\sdncast{\u F A}{\u FA'}\ret x'} x \force\supcast{U\u B}{U\u B'}\thunk {(\force f)\, x'}\\
+ \thunk\lambda x':A'. \\
+ &&\bindXtoYinZ {\sdncast{\u F A}{\u FA'}\ret x'} x\\
+ &&\force\supcast{U\u B}{U\u B'}\thunk {(\force f)\, x'}\\
\bullet : \u FU\u B' \vdash \sdncast{\u FU\u B}{\u FU\u B'}
&=&
\bindXtoYinZ \bullet {x'} \sdncast{\u B}{\u B'}\force x'
@@ -3477,9 +3490,11 @@ following sense:
\pipe\sem\Delta\vdash \sem E : \sem T$ in CBPV*.
\end{lemma}
-In effect we have now given a model of the types, terms and type
-dynamism proofs of GTT in CBPV*, and we now need to interpret the
-\emph{term dynamism} proofs.
+In effect we have now given an interpretation of the types, terms and
+type dynamism proofs of GTT in CBPV*.
+%
+To complete this to form a \emph{model} of GTT, we need to given an
+interpretation of the \emph{term dynamism} proofs.
%
Our goal in the remainder of this section is to establish the
following ``axiomatic graduality'' theorem, that defines such an
@@ -3487,7 +3502,8 @@ interpretation.
%
The basic idea is that GTT has \emph{heterogeneous} term dynamism
rules indexed by type dynamism, but CBPV* has only \emph{homogeneous}
-inequalities between terms with the same types.
+inequalities between terms, i.e. if $E \ltdyn E'$, then $E,E'$ have
+the \emph{same} context and types.
%
Since every type dynamism judgment has an associated cast, we can
translate a heterogeneous inequality to a homogeneous inequality
@@ -3506,13 +3522,11 @@ translate a heterogeneous inequality to a homogeneous inequality
\Phi \vdash V \ltdyn V' : A \ltdyn A'}
{\sem{\Gamma} \vdash \supcast{A}{A'}[\sem{V}] \ltdyn\sem{V'}[\sem\Phi] : \sem {A'}}
\end{mathpar}
- where we define $\sem{\Phi}, \sem{\Delta}$%
- \begin{shortonly}
- in the obvious way, where if $\Delta = \cdot$, then
- $M[\sem{\Delta}] = M$.
- \end{shortonly}
+ where we define $\sem{\Phi}$ to upcast each variable, and
+ $\sem{\Delta}$ to downcast $\bullet$ if it is nonempty, and if
+ $\Delta = \cdot$, then $M[\sem{\Delta}] = M$.
\begin{longonly}
- as follows.
+ More explicitly,
\begin{enumerate}
\item If $\Phi : \Gamma \ltdyn \Gamma'$, then there exists $n$
such that $\Gamma = x_1:A_1,\ldots,x_n:A_n$ and $\Gamma' =
@@ -3546,7 +3560,6 @@ of bind and thunk.
%
The full proofs can be found in the supplementary material.
\end{shortonly}
-
\begin{longonly}
First, to keep proofs high-level, we establish the following cast
reductions that follow easily from $\beta,\eta$ principles.
@@ -3586,14 +3599,70 @@ of bind and thunk.
\end{lemma}
\end{longonly}
-The first main lemma is the following ``fundamental theorem'' for
-that says that from the basic casts being ep pairs, we can prove that
-all casts are ep pairs.
+The first main lemma is the following ``fundamental theorem'' for
+casts that says that from the basic casts being ep pairs, we can prove
+that all casts are ep pairs.
%
-\begin{shortonly}
- This follows mostly from straightforward calculation, but also from
- some lemmas that say ep pairs compose.
-\end{shortonly}
+To interpret the $A \ltdyn \dynv$ rule, which uses a composition $A
+\ltdyn \floor{A} \ltdyn \dynv$, we use the \emph{composition} of ep
+pairs, which forms an ep pair by the following lemma. The $\u B \ltdyn
+\dync$ gets a symmetric lemma.
+
+\begin{lemma}[EP Pairs Compose]
+ \begin{enumerate}
+ \item If $(V_1, S_1)$ is a value ep pair from $A_1$ to $A_2$ and
+ $(V_2,S_2)$ is a value ep pair from $A_2$ to $A_3$, then
+ $(V_2[V_1], S_1[S_2])$ is a value ep pair from $A_1$ to $A_3$.
+ \item If $(V_1, S_1)$ is a computation ep pair from $\u B_1$ to $\u B_2$ and
+ $(V_2,S_2)$ is a computation ep pair from $\u B_2$ to $\u B_3$, then
+ $(V_2[V_1], S_1[S_2])$ is a computation ep pair from $\u B_1$ to $\u B_3$.
+ \end{enumerate}
+\end{lemma}
+\begin{longproof}
+ \begin{enumerate}
+ \item First, retraction follows from retraction twice:
+ \[ S_1[S_2[\ret V_2[V_1[x]]]] \equidyn S_1[\ret [V_1[x]]] \equidyn x \]
+ and projection follows from projection twice:
+ \begin{align*}
+ \bindXtoYinZ {S_1[S_2[\bullet]]} x \ret V_2[V_1[x]]
+ &\equidyn
+ {\bindXtoYinZ {S_1[S_2[\bullet]]} x \bindXtoYinZ {\ret [V_1[x]]} y \ret V_2[y]}\tag{$\u F\beta$}\\
+ &\equidyn
+ \bindXtoYinZ {(\bindXtoYinZ {S_1[S_2[\bullet]]} x {\ret [V_1[x]]})} y \ret V_2[y]\tag{Commuting conversion}\\
+ &\ltdyn
+ \bindXtoYinZ {S_2[\bullet]} y \ret V_2[y]\tag{Projection}\\
+ &\ltdyn \bullet \tag{Projection}
+ \end{align*}
+ \item Again retraction follows from retraction twice:
+ \[ S_1[S_2[\force V_2[V_1[z]]]] \equidyn S_1[\force V_1[z]] \equidyn \force z \]
+ and projection from projection twice:
+ \begin{align*}
+ V_2[V_1[\thunk S_1[S_2[\force w]]]]
+ &\equidyn V_2[V_1[\thunk S_1[\force \thunk S_2[\force w]]]]\tag{$U\beta$}\\
+ &\ltdyn V_2[\thunk S_2[\force w]] \tag{Projection}\\
+ &\ltdyn w \tag{Projection}
+ \end{align*}
+ \end{enumerate}
+\end{longproof}
+
+With this lemma, we can show that all casts come in ep pairs.
+%
+The proof is a somewhat tedious, but straightforward calculation.
+%
+However, the tedium here pays off greatly in later proofs: this is the
+\emph{only} proof in the entire development that needs to inspect the
+definition of a ``shifted'' cast: i.e., a downcast between $\u F$
+types or an upcast between $U$ types.
+%
+All later lemmas (identity expansion, coherence, fundamental theorem),
+have cases for these shifted casts, but \emph{only} use the property
+that there are part of an ep pair.
+%
+This is one of the biggest advantages of using an explicit syntax for
+complex values and complex stacks: the shifted casts are the only ones
+that non-trivially use effectful terms, so after this lemma is
+established we only have to manipulate values and stacks, which
+compose much more nicely than effectful terms.
\begin{lemma}[Casts are EP Pairs]
\begin{enumerate}
@@ -3606,10 +3675,10 @@ all casts are ep pairs.
\end{enumerate}
\end{lemma}
\begin{longproof}
- By mutual induction on $A, \u B$
+ By induction on normalized type dynamism derivations.
\begin{enumerate}
\item TODO: There's a few base cases about the dynamic type
- \item $0$:
+ \item $0 \ltdyn A$ (that $A \in \{ \dyn, 0 \}$ is not important):
\begin{enumerate}
\item Retraction is
\[ x : 0 \vdash \ret x \equidyn \bindXtoYinZ {\ret\absurd x} y \err : \u F A \]
@@ -3966,142 +4035,21 @@ all casts are ep pairs.
\end{enumerate}
\end{longproof}
-\begin{longonly}
-Quite frequently we need the following commuting conversions, which
-are derivable from the $\eta$ rules for positive connectives.
-
-We need two versions of each rule for the positive value type
-connectives because of complex values: one when the continuation is a
-value and one when the continuation is a term.
-\begin{lemma}[Commuting Conversions]
- All of the following are provable when both sides are well-typed/scoped:
- % TODO: 1, 0?
- \begin{mathpar}
- E[\caseofXthenYelseZ V {x_1.V_1}{x_2.V_2}/y]
- \equidyn
- \caseofXthenYelseZ V {x_1.E[V_1/y]}{x_2.E[V_2/y]}
-
- S[\caseofXthenYelseZ V {x_1.M_1}{x_2.M_2}]
- \equidyn
- \caseofXthenYelseZ V {x_1.S[M_1]}{x_2.S[M_2]}
-
- E[\pmpairWtoXYinZ V {x}{y} V'/z]
- \equidyn
- \pmpairWtoXYinZ V {x}{y} E[V'/z]
-
- S[\pmpairWtoXYinZ V {x}{y} M']
- \equidyn
- \pmpairWtoXYinZ V {x}{y} S[M']
-
- S[\bindXtoYinZ M x N]
- \equidyn
- \bindXtoYinZ M x S[N]
- \end{mathpar}
-\end{lemma}
-\begin{proof}
- \begin{enumerate}
- \item For $+$, we just show one case since the other is exactly the same:
- \begin{align*}
- &E[\caseofXthenYelseZ V {x_1.V_1}{x_2.V_2}/y]\\
- &\equidyn
- \caseofXthenYelseZ V {x_1'. E[\caseofXthenYelseZ {\inl x_1'} {x_1.V_1}{x_2.V_2}/y]}{x_2'. E[\caseofXthenYelseZ {\inr x_2'} {x_1.V_1}{x_2.V_2}/y]}\tag{$+\eta$}\\
- &\equidyn \caseofXthenYelseZ V {x_1'. E[V_1[x_1'/x_1]]} {x_2'. E[V_2[x_2'/x_2]]}\tag{$+\beta$ twice}\\
- &\equidyn \caseofXthenYelseZ V {x_1. E[V_1]} {x_2. E[V_2]} \tag{$\alpha$}
- \end{align*}
- \item For $\times$
- \begin{align*}
- &E[\pmpairWtoXYinZ V x y V']\\
- &\pmpairWtoXYinZ V {x'}{y'} E[\pmpairWtoXYinZ {(x',y')} x y V']\tag{$\times\eta$}\\
- &\pmpairWtoXYinZ V {x'}{y'} E[V'[x'/x][y'/y]] \tag{$\times\beta$}\\
- &\pmpairWtoXYinZ V {x}{y} E[V'] \tag{$\alpha$}
- \end{align*}
- \item For $\u F$
- \begin{align*}
- &S[\bindXtoYinZ M x N]\\
- &\bindXtoYinZ M y S[\bindXtoYinZ {\ret y} x N]\tag{$\u F\eta$}\\
- &\bindXtoYinZ M y S[N[y/x]]\tag{$\u F\beta$}\\
- &\bindXtoYinZ M y S[N] \tag{$\alpha$}
- \end{align*}
- \end{enumerate}
-\end{proof}
-
-\end{longonly}
-
-\begin{lemma}[EP Pairs Compose]
- \begin{enumerate}
- \item If $(V_1, S_1)$ is a value ep pair from $A_1$ to $A_2$ and
- $(V_2,S_2)$ is a value ep pair from $A_2$ to $A_3$, then
- $(V_2[V_1], S_1[S_2])$ is a value ep pair from $A_1$ to $A_3$.
- \item If $(V_1, S_1)$ is a computation ep pair from $\u B_1$ to $\u B_2$ and
- $(V_2,S_2)$ is a computation ep pair from $\u B_2$ to $\u B_3$, then
- $(V_2[V_1], S_1[S_2])$ is a computation ep pair from $\u B_1$ to $\u B_3$.
- \end{enumerate}
-\end{lemma}
-\begin{proof}
- \begin{enumerate}
- \item First, retraction follows from retraction twice:
- \[ S_1[S_2[\ret V_2[V_1[x]]]] \equidyn S_1[\ret [V_1[x]]] \equidyn x \]
- and projection follows from projection twice:
- \begin{align*}
- \bindXtoYinZ {S_1[S_2[\bullet]]} x \ret V_2[V_1[x]]
- &\equidyn
- {\bindXtoYinZ {S_1[S_2[\bullet]]} x \bindXtoYinZ {\ret [V_1[x]]} y \ret V_2[y]}\tag{$\u F\beta$}\\
- &\equidyn
- \bindXtoYinZ {(\bindXtoYinZ {S_1[S_2[\bullet]]} x {\ret [V_1[x]]})} y \ret V_2[y]\tag{Commuting conversion}\\
- &\ltdyn
- \bindXtoYinZ {S_2[\bullet]} y \ret V_2[y]\tag{Projection}\\
- &\ltdyn \bullet \tag{Projection}
- \end{align*}
- \item Again retraction follows from retraction twice:
- \[ S_1[S_2[\force V_2[V_1[z]]]] \equidyn S_1[\force V_1[z]] \equidyn \force z \]
- and projection from projection twice:
- \begin{align*}
- V_2[V_1[\thunk S_1[S_2[\force w]]]]
- &\equidyn V_2[V_1[\thunk S_1[\force \thunk S_2[\force w]]]]\tag{$U\beta$}\\
- &\ltdyn V_2[\thunk S_2[\force w]] \tag{Projection}\\
- &\ltdyn w \tag{Projection}
- \end{align*}
- \end{enumerate}
-\end{proof}
-
-\begin{corollary}[Hom-set formulation of Adjunction]
- For any value embedding-projection pair $V_e,S_p$ from $A$ to $A'$,
- the following are equivalent:
- \begin{mathpar}
- \mprset{fraction={===}}
- \inferrule
- {\Gamma \vdash \ret V_e[V] \ltdyn M : \u F \srho{A'}}
- {\Gamma \vdash \ret V \ltdyn S_p[M] : \u F \srho {A}}
- \end{mathpar}
-
- For any computation ep pair $(V_e,S_p)$ from $\u B$ to $\u B'$, the
- following are equivalent:
- \begin{mathpar}
- \mprset{fraction={===}}
- \inferrule
- {\Gamma, z' : U \u B' \vdash M \ltdyn S[S_p[\force z']] : \u C}
- {\Gamma, z : U \u B \vdash M[V_e/z'] \ltdyn S[\force z] : \u C}
- \end{mathpar}
-\end{corollary}
-\begin{proof}
- TODO
-\end{proof}
-
-The following lemma is key to proving many ``axioms'' are valid in
-GTT, since an identity cast is inserted in translation. Also it is key
-to proving that GTT is a conservative extension of CBPV.
-\begin{lemma}[Identity Expansion]
- For any $A$ and $\u B$,
- \begin{mathpar}
- x:A \vdash \sem{\upcast{A}{A}} \equidyn x : A\\
- \bullet : \u B \vdash \sem{\dncast{\u B}{\u B}} \equidyn \bullet : \u B
- \end{mathpar}
-\end{lemma}
-\begin{proof}
- TODO: induction on everything
-\end{proof}
-
-The following lemma is key to proving the coherence lemma.
+Next, we want to show that casts can be decomposed nicely: a cast from
+a type to itself is the identity and if $A \ltdyn A' \ltdyn A''$ then
+the cast from $A$ to $A''$ factors through $A'$.
+%
+For all connectives except $\u F, U$ this uses the functoriality of
+the type constructors on values and stacks.
+%
+For the $\u F, U$ cases, we will use the corresponding fact about the
+dual cast, i.e., to prove the $\u F A$ to $\u F A$ downcast is the
+identity stack, we know by inductive hypothesis that the $A$ to $A$
+upcast is the identity, and that the identity stack is a projection
+for the identity.
+%
+Then from uniqueness of projections from embeddings, we know the $\u
+FA$ downcast must be equivalent to the identity.
\begin{lemma}[Value Embedding determines Projection, Computation Projection determines Embedding]
For any value $x : A \vdash V_e : A'$ and stacks $\bullet : \u F A'
\vdash S_1 : \u F A$ and $\bullet : \u F A' \vdash S_2 : \u F A$, if
@@ -4113,7 +4061,7 @@ The following lemma is key to proving the coherence lemma.
\u B$, if $(V_1, S_p)$ and $(V_2, S_p)$ are both computation ep pairs then
\[ V_1 \equidyn V_2 \]
\end{lemma}
-\begin{proof}
+\begin{longproof}
By symmetry it is sufficient to show $S_1 \ltdyn S_2$.
\begin{mathpar}
@@ -4138,7 +4086,37 @@ The following lemma is key to proving the coherence lemma.
{x : U \u B \vdash \thunk\force V_1 \ltdyn \thunk \force V_2 : U \u B'}}
{x : U \u B \vdash V_1 \ltdyn V_2 : U \u B'}
\end{mathpar}
+\end{longproof}
+
+Next, we show that casts from a type to itself are equivalent to the
+identity.
+%
+This is needed to prove the reflexivity case of the axiomatic
+graduality theorem.
+%
+It is also key to the conservativity result: i.e., that proving a
+homogeneous inequality in GTT is the same as proving the inequality
+between their translations.
+\begin{lemma}[Identity Expansion]
+ For any $A$ and $\u B$,
+ \begin{mathpar}
+ x:A \vdash \sem{\upcast{A}{A}} \equidyn x : A\\
+ \bullet : \u B \vdash \sem{\dncast{\u B}{\u B}} \equidyn \bullet : \u B
+ \end{mathpar}
+\end{lemma}
+\begin{proof}
+ TODO: induction on everything
\end{proof}
+
+Next, we want to show the decomposition/coherence theorem that says
+that a sequence of upcasts is equivalent to the direct upcast and
+similarly for downcasts.
+%
+We know again that this is true syntactically in GTT so it is not
+surprising that we need to show it in our model.
+%
+Specifically, it arises when we show how to translate
+\emph{transitivity} proofs from GTT.
\begin{lemma}[Cast Decomposition]
For any dynamic type interpretation $\rho$,
\begin{mathpar}
@@ -4152,7 +4130,7 @@ The following lemma is key to proving the coherence lemma.
\srho{\dncast{\u B}{\u B'}}[\srho{\dncast{\u B'}{\u B''}}]}
\end{mathpar}
\end{lemma}
-\begin{proof}
+\begin{longproof}
By mutual induction on $A, \u B$.
\begin{enumerate}
\item $A \ltdyn A' \ltdyn A''$
@@ -4297,8 +4275,74 @@ The following lemma is key to proving the coherence lemma.
\end{enumerate}
\end{enumerate}
\end{enumerate}
-\end{proof}
+\end{longproof}
+
+Next, we need the following theorem that let's us ``move a cast'' from
+left to right or vice-versa.
+%
+These arise in the proof cases for return and thunk, because in those
+cases the inductive hypothesis is in terms of an upcast (downcast) and
+the conclusion is in terms of a a downcast (upcast).
+\begin{lemma}[Hom-set formulation of Adjunction]
+ For any value embedding-projection pair $V_e,S_p$ from $A$ to $A'$,
+ the following are equivalent:
+ \begin{mathpar}
+ \mprset{fraction={===}}
+ \inferrule
+ {\Gamma \vdash \ret V_e[V] \ltdyn M : \u F A'}
+ {\Gamma \vdash \ret V \ltdyn S_p[M] : \u F A}
+ \end{mathpar}
+
+ For any computation ep pair $(V_e,S_p)$ from $\u B$ to $\u B'$, the
+ following are equivalent:
+ \begin{mathpar}
+ \mprset{fraction={===}}
+ \inferrule
+ {\Gamma, z' : U \u B' \vdash M \ltdyn S[S_p[\force z']] : \u C}
+ {\Gamma, z : U \u B \vdash M[V_e/z'] \ltdyn S[\force z] : \u C}
+ \end{mathpar}
+\end{lemma}
+\begin{longproof}
+ \begin{enumerate}
+ \item Assume $\ret V_e[V] \ltdyn M : \u F A'$. Then by retraction,
+ $\ret V \ltdyn S_p[\ret V_e[V]]$ so by transitivity, the result
+ follows by substitution:
+ \begin{mathar}
+ \inferrule
+ {S_p \ltdyn S_p \and \ret V_e[V] \tdyn M}
+ {S_p[\ret V_e[V]] \ltdyn M}
+ \end{mathar}
+ \item Assume $\ret V \ltdyn S_p[M] : \u F A$. Then by projection,
+ $\bindXtoYinZ {S_p[M]} x \ret V_e[x] \ltdyn M$, so it is sufficient to show
+ \[ \ret V_e[V] \ltdyn \bindXtoYinZ {S_p[M]} x \ret V_e[x] \]
+ but again by substitution we have
+ \[ \bindXtoYinZ {\ret V} x \ret V_e[x] \ltdyn \bindXtoYinZ {S_p[M]} x \ret V_e[x]\]
+ and by $\u F\beta$, the LHS is equivalent to $\ret V_e[V]$.
+ \item Assume $z' : U\u {B'} \vdash M \ltdyn S[S_p[\force z']]$, then
+ by projection, $S[S_p[\force V_e]] \ltdyn S[\force z]$
+ and by substitution:
+ \begin{mathpar}
+ \inferrule
+ {M \ltdyn S[S_p[\force z']]\and V_e \ltdyn V_e \and S[S_p[\force V_e]] = (S[S_p[\force z']])[V_e/z']}
+ {M[V_e/z'] \ltdyn S[S_p[\force V_e]]}
+ \end{mathpar}
+ \item Assume $z : U \u B \vdash M[V_e/z'] \ltdyn S[\force z]$. Then
+ by retraction, $M \ltdyn M[V_e[\thunk{S_p[\force z]}]]$ and by
+ substitution:
+ \[ M[V_e[\thunk{S_p[\force z]}]] \ltdyn S[\force \thunk{S_p[\force z]}] \]
+ and the right is equivalent to $S[S_p[\force z]]$ by $U\beta$.
+ \end{enumerate}
+\end{longproof}
+Finally we can now prove the axiomatic graduality theorem.
+%
+Most of the work is in the lemmas proven above.
+%
+The remainder is to prove the ``compatibility'' cases which are the
+congruence cases for introduction and elimination rules.
+%
+These come down to proving that the casts ``commute'' with
+introduction/elimination forms, and are all simple calculations.
\begin{theorem}[Axiomatic Graduality]
For any dynamic type interpretation, the following are true:
\begin{mathpar}
@@ -4314,10 +4358,10 @@ The following lemma is key to proving the coherence lemma.
{\sem{\Gamma} \vdash \supcast{A}{A'}[\sem{V}] \ltdyn\sem{V'}[\sem\Phi] : \sem {A'}}
\end{mathpar}
\end{theorem}
-\begin{proof}
+\begin{longproof}
By mutual induction over term dynamism derivations. For the $\beta,
- \eta$ and reflexivity rules, we use the identity expansion lemma
- (TODO ref).
+ \eta$ and reflexivity rules, we use the identity expansion lemma and
+ the corresponding $\beta, \eta$ rule of CBPV* (TODO ref).
For compatibility rules a pattern emerges. For universal rules
(positive intro, negative elim) are easy, don't need to reason about
@@ -4753,39 +4797,20 @@ The following lemma is key to proving the coherence lemma.
& \equidyn \sdncast{\u B}{\u B'}[\bindXtoYinZ {\sem{M'}[\Phi]} {x'} \sem{N}[\Phi]] \tag{commuting conversion}
\end{align*}
\end{enumerate}
-\end{proof}
+\end{longproof}
-\begin{lemma}[Conservativity]
- If the types of the two terms in dynamism judgment are the same,
- then that implies an ordering in CBPV between their translations
- (with no casts inserted).
- \begin{mathpar}
- \inferrule
- {\Gamma \ltdyn \Gamma \vdash M_1 \ltdyn M_2 : \u B \ltdyn \u B}
- {\sem\Gamma \vdash \sem{M_1} \ltdyn \sem{M_2} : \sem{\u B}}
- \end{mathpar}
-\end{lemma}
+Finally, as a corollary, we have the
+\begin{corollary}[Conservativity]
+ If $\Gamma, \Delta \vdash E, E' : T$ are two terms of the same type
+ in GTT, then $E \ltdyn E'$ is provable in GTT if and only if it is
+ provable in CBPV*.
+\end{corollary}
\begin{proof}
- By axiomatic graduality and the fact that identity casts are
- identities.
+ The reverse direction holds because CBPV* is a syntactic subset of
+ GTT. The forward direction holds by axiomatic graduality and the
+ fact that identity casts are identities.
\end{proof}
-\begin{figure}
- \begin{mathpar}
- \begin{array}{rcl}
- \srho {\upcast A {A'} V} &=& \srho{\upcast A {A'}} \sem V\\
- \srho {\dncast {\u B} {\u B'} \hat M} &=& \srho{\dncast {\u B} {\u B'}} \srho {\hat M}\\\\
-
- \srho{\upcast {A} \dynv} &=& \srho{\upcast{A}{\floor A}}[\rho(\floor A)]\\
- \srho{\upcast {A_1 \times A_2}{A_1'\times A_2'}} &=&
- \pmpairWtoXYinZ x {x_1}{x_2} (\upcast{A_1}{A_1'}[x_1/x], \upcast{A_2,A_2'}[x_2/x])\\
- \cdot\\
- \srho{\upcast {U \u B}{U \u B'}} &=& \cdots
- \end{array}
- \end{mathpar}
- \caption{Contract Translation of casts}
-\end{figure}
-
\section{Complex Value/Stack Elimination}
\label{sec:complex}
--
GitLab