diff --git a/paper/gtt.tex b/paper/gtt.tex
index d9a0932841a200e921757e7997f3349c3f5101f7..ec5d727a76b34003f6be548799004c4d3783ed95 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -1848,25 +1848,29 @@ themselves.
\end{enumerate}
\end{lemma}
-When combined with the logical relation interpretation of CBPV, this
-is our graduality theorem.
-\begin{theorem}[Dynamism Preservation of Contract Translation (Graduality Part 1)]
- Let $\rho$ be a dynamic type interpretation. Then the following are true,
+Our goal in the remainder of this section is to establish the
+following ``axiomatic graduality'' theorem, which interprets a term
+dynamism judgment of GTT as an ordering ``up to cast'' in CBPV. In the
+next section, we provide an operational \emph{model} of CBPV and thus
+obtain by composition an operational gradulity theorem (the dynamic
+gradual guarantee).
+\begin{theorem}[Axiomatic Graduality]
+ For any dynamic type interpretation, the following are true:
\begin{mathpar}
\inferrule
- {\Gamma \ltdyn \Gamma' \vdash M \ltdyn M' : \u B \ltdyn \u B'}
- {\srho{\Gamma} \vdash \srho{M} \ltdyn \srho{\dncast {\u B}{\u B'}}[\srho{M'[\srho{\upcast{\Gamma}{\Gamma'}}\Gamma/\Gamma']}] : \srho {\u B}}
-
- \inferrule
- {\Gamma \ltdyn \Gamma' \vdash V \ltdyn V' : A \ltdyn A'}
- {\srho{\Gamma} \vdash \srho{\upcast{A}{A'}}[\srho{V}] \ltdyn\srho{V'[\srho{\upcast{\Gamma}{\Gamma'}}\Gamma/\Gamma']} : \srho {A'}}
+ {\Phi : \Gamma \ltdyn \Gamma'\\
+ \Psi : \Delta \ltdyn \Delta'\\
+ \Phi \pipe \Psi \vdash M \ltdyn M' : \u B \ltdyn \u B'}
+ {\sem\Gamma \pipe \sem{\Delta'} \vdash \sem M[\sem{\Psi}] \ltdyn \sdncast{\u B}{\u B'}[\sem{M'}[\sem{\Phi}]] : \sem{\u B}}
\inferrule
- {\Gamma \ltdyn \Gamma' \pipe \bullet \ltdyn \bullet : \u B \ltdyn \u B' \vdash S \ltdyn S' : \u C \ltdyn \u C'}
- {\srho{\Gamma} \pipe \bullet : \srho{\u B'} \vdash \srho{S}[\srho{\dncast{\u B}{\u B'}}] \ltdyn \srho{\dncast {\u C}{\u C'}}[\srho{S'}[\srho{\upcast{\Gamma}{\Gamma'}}\Gamma/\Gamma']] : \srho {\u C}}
+ {\Phi : \Gamma \ltdyn \Gamma' \\
+ \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}
\end{theorem}
+
Quite frequently we need the following commuting conversions, which
are derivable from the $\eta$ rules for positive connectives.
@@ -2403,17 +2407,32 @@ value and one when the continuation is a term.
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.
-%
-A similar lemma says that the projection downcasts determine the
-embeddings but I don't see anywhere where we need that.
-\begin{lemma}[Value Embedding determines Projection]
+\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
$(V_e, S_1)$ and $(V_e, S_2)$ are both value ep pairs, then
\[ S_1 \equidyn S_2 \]
-\end{lemma}
+ Similarly for any values $x : U\u B \vdash V_1 : U \u B'$ and $x :
+ U\u B \vdash V_2 : U \u B'$ and stack $\bullet : \u B' \vdash S_p :
+ \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}
By symmetry it is sufficient to show $S_1 \ltdyn S_2$.
@@ -2428,22 +2447,18 @@ embeddings but I don't see anywhere where we need that.
{\bindXtoYinZ {S_1} x \ret x \ltdyn \bindXtoYinZ \bullet x S_2[\ret x]}}
{\bullet : \u F A' \vdash S_1 \ltdyn S_2 : \u F A}
\end{mathpar}
-\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$,
+ similarly to show $V_1 \ltdyn V_2$:
\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
+ \inferrule%
+ {\inferrule
+ {\inferrule
+ {x : U \u B \vdash \thunk\force V_2 \ltdyn \thunk \force V_2 : U \u B'}
+ {x : U \u B \vdash \thunk \force x \ltdyn \thunk S_p[\force V_2]}}
+ {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{lemma}
-\begin{proof}
- TODO: induction on everything
\end{proof}
-
\begin{lemma}[Cast Decomposition]
For any dynamic type interpretation $\rho$,
\begin{mathpar}
@@ -2462,75 +2477,150 @@ to proving that GTT is a conservative extension of CBPV.
\begin{enumerate}
\item $A \ltdyn A' \ltdyn A''$
\begin{enumerate}
- \item If $A = \dynv$, then $A' = A'' = \dynv$ TODO
- \item If $A \neq \dynv$ and $A' = \dynv$, then $A'' = \dynv$: TODO
- \item If $A, A' \neq \dynv$ and $A'' = \dynv$: TODO
- \item If $A,A',A'' \neq \dynv$, then they all have the same
+ \item If $A = 0$, we need to show $x : 0 \vdash
+ \supcast{0}{A''}[x] \equidyn
+ \supcast{A'}{A''}[\supcast{0}{A'}[x]] : A''$ which follows by
+ $0\eta$.
+ \item If $A = \dynv$, then $A' = A'' = \dynv$, and both casts are
+ the identity.
+ \item If $A \not\in \{\dynv, 0 \}$ and $A' = \dynv$, then $A'' =
+ \dynv$ and $\supcast{\dynv}{\dynv}[\supcast{A}{\dynv}] =
+ \supcast{A}{\dynv}$ by definition.
+ \item If $A, A' \not\in \{\dynv, 0 \}$ and $A'' = \dynv$, then
+ $\floor A = \floor {A'}$, which we call $G$ and
+ \[ \supcast{A}{\dynv} = \supcast{G}{\dynv}[\supcast{A}{G}] \]
+ and
+ \[ \supcast{A'}{\dynv}[\supcast{A}{A'}] = \supcast{G}{\dynv}[\supcast{A'}{G}[\supcast{A}{A'}]] \]
+ so this reduces to the case for $A \ltdyn A' \ltdyn G$, below.
+ \item If $A,A',A'' \not\in \{\dynv, 0 \}$, then they all have the same
top-level constructor:
\begin{enumerate}
- \item $0$: TODO
- \item $+$: TODO
- \item $1$: TODO
- \item $\times$: TODO
- \item $U \u B \ltdyn U \u B' \ltdyn U \u B''$. TODO, but here's
- the argument: by IH we know the downcasts compose. But
- projections determine embeddings and ep pairs compose, so the
- upcasts compose. Beautiful!
+ \item $+$: We need to show for $A_1 \ltdyn A_1' \ltdyn A_1''$
+ and $A_2 \ltdyn A_2' \ltdyn A_2''$:
+ \[
+ x : \sem{A_1} + \sem{A_2} \vdash
+ \supcast{A_1'+A_2'}{A_1''+A_2''}[\supcast{A_1+A_2}{A_1'+A_2'}[x]]\equidyn
+ \supcast{A_1+A_2}{A_1''+A_2''}[x]
+ : \sem{A_1''}+\sem{A_2''}.
+ \]
+ We proceed as follows:
+ \begin{align*}
+ &\supcast{A_1'+A_2'}{A_1''+A_2''}[\supcast{A_1+A_2}{A_1'+A_2'}[x]]\\
+ &\equidyn \caseofX {x}\tag{$+\eta$}\\
+ &\qquad\thenY {x_1. \supcast{A_1'+A_2'}{A_1''+A_2''}[\supcast{A_1+A_2}{A_1'+A_2'}[\inl x_1]]}\\
+ &\qquad\elseZ {x_2. \supcast{A_1'+A_2'}{A_1''+A_2''}[\supcast{A_1+A_2}{A_1'+A_2'}[\inr x_2]]}\\
+ &\equidyn \caseofX {x}\tag{cast reduction}\\
+ &\qquad\thenY {x_1. \supcast{A_1'+A_2'}{A_1''+A_2''}[\inl\supcast{A_1}{A_1'}[x_1]]}\\
+ &\qquad\elseZ {x_2. \supcast{A_1'+A_2'}{A_1''+A_2''}[\inr\supcast{A_2}{A_2'}[x_2]]}\\
+ &\equidyn \caseofX {x}\tag{cast reduction}\\
+ &\qquad\thenY {x_1. \inl\supcast{A_1'}{A_1''}[\supcast{A_1}{A_1'}[x_1]]}\\
+ &\qquad\elseZ {x_2. \inr\supcast{A_2'}{A_2''}[\supcast{A_2}{A_2'}[x_2]]}\\
+ &\equidyn \caseofX {x}\tag{IH}\\
+ &\qquad\thenY {x_1. \inl\supcast{A_1}{A_1''}[x_1]}\\
+ &\qquad\elseZ {x_2. \inr\supcast{A_2}{A_2''}[x_2]}\\
+ &= \supcast{A_1+A_2}{A_1''+A_2''}[x] \tag{definition}
+ \end{align*}
+ \item $1$: By definition both sides are the identity.
+ \item $\times$: We need to show for $A_1 \ltdyn A_1' \ltdyn A_1''$
+ and $A_2 \ltdyn A_2' \ltdyn A_2''$:
+ \[
+ x : \sem{A_1} \times \sem{A_2} \vdash
+ \supcast{A_1'\times A_2'}{A_1''\times A_2''}[\supcast{A_1\times A_2}{A_1'\times A_2'}[x]]\equidyn
+ \supcast{A_1\times A_2}{A_1''\times A_2''}[x]
+ : \sem{A_1''}\times \sem{A_2''}.
+ \]
+ We proceed as follows:
+ \begin{align*}
+ &\supcast{A_1'\times A_2'}{A_1''\times A_2''}[\supcast{A_1\times A_2}{A_1'\times A_2'}[x]]\\
+ &\equidyn\pmpairWtoXYinZ x y z \supcast{A_1'\times A_2'}{A_1''\times A_2''}[\supcast{A_1\times A_2}{A_1'\times A_2'}[(y,z)]]\tag{$\times\eta$}\\
+ &\equidyn\pmpairWtoXYinZ x y z \supcast{A_1'\times A_2'}{A_1''\times A_2''}[(\supcast{A_1}{A_1'}[y], \supcast{A_2}{A_2'}[z])]\tag{cast reduction}\\
+ &\equidyn\pmpairWtoXYinZ x y z (\supcast{A_1'}{A_1''}[\supcast{A_1}{A_1'}[y]], \supcast{A_2'}{A_2''}[\supcast{A_2}{A_2'}[z]])\tag{cast reduction}\\
+ &\equidyn\pmpairWtoXYinZ x y z (\supcast{A_1}{A_1''}[y], \supcast{A_2}{A_2''}[z])\tag{IH}\\
+ &=\supcast{A_1\times A_2}{A_1'' \times A_2''}[x]\tag{definition}
+ \end{align*}
+ \item $U \u B \ltdyn U \u B' \ltdyn U \u B''$.
+ We need to show
+ \[
+ x : U \u B \vdash \supcast{U\u B'}{U\u B''}[\supcast{U\u B}{U\u B'}[x]] \equidyn
+ \supcast{U\u B}{U\u B''}[x] : U\u B''
+ \]
+ By composition of ep pairs, we know $(x.\supcast{U\u B'}{U\u
+ B''}[\supcast{U\u B}{U\u B'}[x]], \sdncast{\u B}{\u
+ B'}[\sdncast{\u B'}{\u B''}])$ is a computation ep pair.
+ Furthermore, by inductive hypothesis, we know
+ \[ \sdncast{\u B}{\u B'}[\sdncast{\u B'}{\u B''}] \equidyn \sdncast{\u B}{\u B''}\]
+ so then both sides form ep pairs paired with $\sdncast{\u
+ B}{\u B''}$, so it follows because computation projections
+ determine embeddings (TODO ref).
\end{enumerate}
\end{enumerate}
\item $\u B \ltdyn \u B' \ltdyn \u B''$
\begin{enumerate}
- \item If $\u B = \dync$, then $\u B' = \u B'' = \dync$ TODO
- \item If $\u B \neq \dync$, and $\u B' = \dync$, then $\u B'' = \dync$ TODO
- \item If $\u B,\u B' \neq \dync$, and $\u B'' = \dync$ TODO
- \item If $\u B,\u B',\u B'' \neq \dync$, then they all have the
+ \item If $\u B = \top$, then the result is immediate by $\eta\top$.
+ \item If $\u B = \dync$, then $\u B' = \u B'' = \dync$ then both
+ sides are just $\bullet$.
+ \item If $\u B \not\in \{\dync, \top\}$, and $\u B' = \dync$, then
+ $\u B'' = \dync$
+ \[ \sdncast{\u B}{\dync}[\sdncast{\dync}{\dync}] = \sdncast{\u B}{\dync} \]
+
+ \item If $\u B,\u B' \not\in \{\dync,\top\}$, and $\u B'' = \dync$ , and $\floor {\u B} = \floor {\u B'}$, which we
+ call $\u G$. Then we need to show
+ \[ \sdncast{\u B}{\u B'}[\sdncast{\u B'}{\u G}[\sdncast{\u G}{\dync}]]
+ \equidyn
+ \sdncast{\u B}{\u G}[\sdncast{\u G}[\dync]]
+ \]
+ so the result follows from the case $\u B \ltdyn \u B' \ltdyn \u
+ G$, which is handled below.
+ \item If $\u B,\u B',\u B'' \not\in \{\dync, \top\}$, then they all have the
same top-level constructor:
\begin{enumerate}
- \item $\top$
- \item $\with$
- \item $\to$
- \item $\u F A \ltdyn \u F A' \ltdyn \u F A''$: TODO, but same
- argument as the $UUU$ case
+ \item $\with$ We are given $\u B_1 \ltdyn \u B_1' \ltdyn \u
+ B_1''$ and $\u B_2 \ltdyn \u B_2' \ltdyn \u B_2''$ and we need to show
+ \[
+ \bullet : \u B_1'' \with \u B_2''
+ \vdash
+ \sdncast{\u B_1 \with \u B_2}{\u B_1' \with \u B_2'}[\sdncast{\u B_1' \with \u B_2'}{\u B_1'' \with \u B_2''}]
+ : \u B_1 \with \u B_2
+ \]
+ We proceed as follows:
+ \begin{align*}
+ &\sdncast{\u B_1 \with \u B_2}{\u B_1' \with \u B_2'}[\sdncast{\u B_1' \with \u B_2'}{\u B_1'' \with \u B_2''}]\\
+ &\equidyn\pairone{\pi\sdncast{\u B_1 \with \u B_2}{\u B_1' \with \u B_2'}[\sdncast{\u B_1' \with \u B_2'}{\u B_1'' \with \u B_2''}]}\tag{$\with\eta$}\\
+ &\quad\pairtwo{\pi'\sdncast{\u B_1 \with \u B_2}{\u B_1' \with \u B_2'}[\sdncast{\u B_1' \with \u B_2'}{\u B_1'' \with \u B_2''}]}\\
+ &\equidyn\pairone{\sdncast{\u B_1}{\u B_1'}[\pi\sdncast{\u B_1' \with \u B_2'}{\u B_1'' \with \u B_2''}]}\tag{cast reduction}\\
+ &\quad\pairtwo{\sdncast{\u B_2}{\u B_2'}[\pi'\sdncast{\u B_1' \with \u B_2'}{\u B_1'' \with \u B_2''}]}\\
+ &\equidyn\pairone{\sdncast{\u B_1}{\u B_1'}[\sdncast{\u B_1'}{\u B_1''}[\pi\bullet]]}\tag{cast reduction}\\
+ &\quad\pairtwo{\sdncast{\u B_2}{\u B_2'}\sdncast{\u B_2'}{\u B_2''}[\pi'\bullet]}\\
+ &\equidyn\pair{\sdncast{\u B_1}{\u B_1''}[\pi\bullet]}{\sdncast{\u B_2}{\u B_2''}[\pi'\bullet]}\tag{IH}\\
+ &= \sdncast{\u B_1 \with \u B_2}{\u B_1'' \with \u B_2''} \tag{definition}
+ \end{align*}
+ \item $\to$, assume we are given $A \ltdyn A' \ltdyn A''$ and
+ $\u B \ltdyn \u B' \ltdyn \u B''$, then we proceed:
+ \begin{align*}
+ &\sdncast{A \to \u B}{A' \to \u B'}[\sdncast{A' \to \u B'}{A'' \to \u B''}]\\
+ &\equidyn \lambda x:A. (\sdncast{A \to \u B}{A' \to \u B'}[\sdncast{A' \to \u B'}{A'' \to \u B''}][\bullet])\,x\tag{$\to\eta$}\\
+ &\equidyn \lambda x:A. \sdncast{\u B}{\u B'}[(\sdncast{A' \to \u B'}{A'' \to \u B''}[\bullet])\, \supcast{A}{A'}[x]] \tag{cast reduction}\\
+ &\equidyn \lambda x:A. \sdncast{\u B}{\u B'}[\sdncast{\u B'}{\u B''}[\bullet\, \supcast{A'}{A''}[\supcast{A}{A'}[x]]]]\tag{cast reduction}\\
+ &\equidyn \lambda x:A. \sdncast{\u B}{\u B''}[\bullet\,\supcast{A}{A''}[x]]\\
+ &= \sdncast{A \to \u B}{A \to \u B''}[\bullet]\tag{definition}
+ \end{align*}
+ \item $\u F A \ltdyn \u F A' \ltdyn \u F A''$. First, by
+ composition of ep pairs, we know
+ \[ (x. \supcast{A'}{A''}[\supcast{A}{A'}[x]], \sdncast{\u F
+ A}{\u F A'})[\sdncast{\u F A'}{\u F A''}]\]
+ form a value ep pair.
+ Furthermore, by inductive hypothesis, we know
+ \[ x : A \vdash \supcast{A'}{A''}[\supcast{A}{A'}[x]] \equidyn \supcast{A}{A''}[x] \]
+ so the two sides of our equation are both projections with the
+ same value embedding, so the equation follows from uniqueness
+ of projections from value embeddings.
\end{enumerate}
\end{enumerate}
\end{enumerate}
-
\end{proof}
-\begin{lemma}[Cast Compatibility Lemmas]
- The following rules are valid
- \begin{enumerate}
- \item Value Type Rules
- \begin{enumerate}
- \item
- $\inferrule{\Gamma \vdash M \ltdyn \sdn{\u B}{\u B'}[M'] : \srho{\u B}}{\Gamma \vdash \sup{U \u B}{U \u B'}\thunk M \ltdyn \thunk M' : U \srho{\u B'}}$ By Galois lemma (TODO)
- \item
- $\inferrule{\Gamma \vdash \sup{U \u B}{U \u B'}V \ltdyn V' : \srho {U \u B'}}
- {\Gamma \vdash \force V \ltdyn \sdn{U \u B}{U \u B'} \force V'} : \srho {U \u B}$ by Galois lemma (TODO)
- \end{enumerate}
- \item Computation Type rules
- \begin{enumerate}
- \item
- $\inferrule{\Gamma, x: \srho{A} \vdash N \ltdyn N'[\sup{A}{A'}[x]/x'] : \u B}
- {\Gamma \vdash \bindXtoYinZ {\sdn{\u F A}{\u F A'}\bullet} x N \ltdyn \bindXtoYinZ \bullet {x'} N'} : \u B'$
- By Galois lemma (TODO):
- \begin{align*}
- \bindXtoYinZ {\sdn{\u F A}{\u F A'}\bullet} x N
- &\ltdyn\bindXtoYinZ {\sdn{\u F A}{\u F A'}\bullet} x N'[\sup{A}{A'}[x]/x']\\
- &\ltdyn \bindXtoYinZ \bullet {x'} N'
- \end{align*}
- \item $\inferrule{\Gamma \vdash \sup{A}{A'} V \ltdyn V' : A'}{\Gamma \vdash \ret V \ltdyn \sdn{\u F A}{\u F A'} \ret V'}$ Direct by Galois lemma (TODO)
- \end{enumerate}
- \end{enumerate}
-\end{lemma}
-
-\begin{lemma}[Graduality Substitution Principles]
- TODO: substituting value in a value, term or stack, substituting a
- term in a stack (use substitution for the target, decomposition)
-\end{lemma}
-
\begin{theorem}[Axiomatic Graduality]
- Let $\rho$ be a dynamic type interpretation. Then the following are true,
+ For any dynamic type interpretation, the following are true:
\begin{mathpar}
\inferrule
{\Phi : \Gamma \ltdyn \Gamma'\\