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

cast decomposition lemma

parent 7768bdf2
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 174 additions and 84 deletions
paper/gtt.tex
+ 174
− 84
View file @ 865d40b2
......@@ -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'\\
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment