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

define most of the lemmas for the GTT -> CBPV translation

parent fe7751de
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 169 additions and 41 deletions
paper/gtt.tex
+ 169
− 41
View file @ 91c85d90
......@@ -107,10 +107,17 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% DEFINITIONS
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% WARNING: I changed these commands
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\renewcommand{\u}{\underline}
\renewcommand{\sup}[2]{\srho{\upcast{#1}{#2}}}
\newcommand{\cbpv}{\text{CBPV}_{\mu,\nu,\err,\ltdyn}}
\newcommand{\cbpvtxt}{$\cbpv$}
\newcommand{\sem}[1]{\llbracket#1\rrbracket}
\newcommand{\srho}[1]{\sem{#1}_\rho}
\newcommand{\sdn}[2]{\srho{\dncast{#1}{#2}}}
\newcommand{\hetplug}[1]{\langle#1\rangle}
\newcommand{\nats}{\mathbb{N}}
\newtheorem{principle}{Principle}
......@@ -120,10 +127,7 @@
\newcommand{\stoup}{\,\,\text{stoup}}
\newcommand{\pipe}{\,\,|\,\,}
\newcommand{\hole}{\bullet}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% WARNING: I changed this command
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\renewcommand{\u}{\underline}
\newcommand{\floor}[1]{\lfloor#1\rfloor}
\newcommand{\ltdyn}{\sqsubseteq}
\newcommand{\gtdyn}{\sqsupseteq}
\newcommand{\equidyn}{\mathrel{\gtdyn\ltdyn}}
......@@ -174,18 +178,18 @@
\newcommand{\relto}{\to}
\newcommand{\M}{\mathcal{M}}
\newcommand{\sq}{\square}
\newcommand{\lett}{\text{let}\,\,}
\newcommand{\lett}{\kw{let}}
\newcommand{\letXbeYinZ}[2]{\lett#2 = #1;}
\newcommand{\bindXtoYinZ}[2]{\text{bind}\,\,#2 \leftarrow #1;}
\newcommand{\too}{\text{to}\,\,}
\newcommand{\case}{\text{case}\,\,}
\newcommand{\kw}[1]{\text{#1}\,\,}
\newcommand{\bindXtoYinZ}[2]{\kw{bind}#2 \leftarrow #1;}
\newcommand{\too}{\kw{to}}
\newcommand{\case}{\kw{case}}
\newcommand{\kw}[1]{\texttt{#1}\,\,}
\newcommand{\caseofXthenYelseZ}[3]{\case #1 \{ #2 \pipe #3 \}}
\newcommand{\pmpairWtoXYinZ}[4]{\kw{split} #1 \kw{to} (#2,#3). #4}
\newcommand{\pmmuXtoYinZ}[3]{\kw{unroll} #1 \kw{to} \roll #2. #3}
\newcommand{\ret}{\text{ret}\,\,}
\newcommand{\thunk}{\text{thunk}\,\,}
\newcommand{\force}{\text{force}\,\,}
\newcommand{\ret}{\kw{ret}}
\newcommand{\thunk}{\kw{thunk}}
\newcommand{\force}{\kw{force}}
\newcommand{\abort}{\kw {abort}}
\newcommand{\with}{\mathop{\&}}
......@@ -395,7 +399,7 @@ different concrete interpertations using logical relations, domains,
etc.
%
This way we can add gradual typing as a sort of ``axiomatic mixin''
that can be added modularly to the axioms of an existing logic.
that can be added modularly to the axioms of an existing type theory.
To study gradual typing axiomatically, we first need to understand the
relational principles that gradual typing should satisfy.
......@@ -811,62 +815,55 @@ with more general types for \emph{recursive} value types and
A $\dynv,\dync$ interpretation $\rho$ consists of first a \cbpvtxt
value type $\rho(\dynv)$, a \cbpvtxt computation type $\rho(\dync)$.
This is extended in the obvious way to interpretations of all
ground types $\sem G \rho$ and $\sem {\u G} \rho$.
ground types $\srho G$ and $\srho {\u G}$.
The interpretation furthermore has for each value ground type, an
interpretation of the upcast and the downcast with $\rho(\dynv)$
such that the upcast is thunkable and the pair satisfy
retraction and projection:
such that the upcast is a (possibly complex) value and the pair
satisfy retraction and projection:
\begin{mathpar}
\inferrule
{}
{x : \sem G \rho \vdash \rho_{up}(G) : \u F \rho (\dynv)}
{x : \srho G \vdash \rho_{up}(G) : \rho (\dynv)}
\inferrule
{}
{y : \rho(\dynv) \vdash \rho_{dn}(G) : \u F \sem G \rho }
\inferrule*[Right=Thunkability]
{}
{x : \sem G \rho \vdash \bindXtoYinZ {\rho_{up}(G)} x' \ret\thunk\ret x' \equidyn \ret\thunk \rho_{up}(G) : \u F U \u F \rho(\dynv)}
{y : \rho(\dynv) \vdash \rho_{dn}(G) : \u F \srho G }
\inferrule*[Right=Retraction]
{}
{x : \sem G\vdash \ret x\equidyn \bindXtoYinZ {\rho_{up}(G)} y \rho_{dn}(G) : \u F \sem G \rho}
{x : \srho G\vdash \ret x\equidyn \letXbeYinZ {\rho_{up}(G)} y \rho_{dn}(G) : \u F \srho G}
\inferrule*[Right=Projection]
{}
{y : \rho(\dynv) \rho \vdash \bindXtoYinZ {\rho_{dn}(G)} x \rho_{up}(G) \ltdyn \ret y : \u F \rho(\dynv)}
{y : \rho(\dynv) \rho \vdash \bindXtoYinZ {\rho_{dn}(G)} x \ret\rho_{up}(G) \ltdyn \ret y : \u F \rho(\dynv)}
\end{mathpar}
And for each computation ground type, an interpretation of the
downcast and upcast with $\rho(\dync)$ such that the downcast is
linear and the pair satisfy retraction and projection:
downcast and upcast with $\rho(\dync)$ such that the downcast is a
(possibly complex) stack and the pair satisfy retraction and
projection:
\begin{mathpar}
\inferrule
{}
{w : U \rho (\dync) \vdash \rho_{dn}(\u G) : \sem {\u G} \rho}
{\bullet : \rho (\dync) \vdash \rho_{dn}(\u G) : \srho {\u G}}
\inferrule
{}
{z : U \sem {\u G} \rho \vdash \rho_{up}(\u G) : \rho(\dync)}
\inferrule*[right=Linearity]
{}
{th : U\u F U \rho(\dync) \vdash \bindXtoYinZ {\force th} w \rho_{dn}(\u G) \equidyn \letXbeYinZ {\thunk (\bindXtoYinZ {\force th} {w'} \force w')} w \rho_{dn}(\u G)}
{z : U \srho {\u G} \vdash \rho_{up}(\u G) : \rho(\dync)}
\inferrule*[right=Retraction]
{}
{z : U \sem {\u G} \rho \vdash \force z \equidyn
\letXbeYinZ {\rho_{up}(\u G)} w \rho_{dn}(\u G)
: \sem {\u G} \rho}
{z : U \srho {\u G} \vdash \force z \equidyn
\rho_{dn}(\u G)[\force {\rho_{up}(\u G)}]
: \srho {\u G}}
\inferrule*[right=Projection]
{}
{w : U \rho(\dync) \vdash
{\bullet : \rho(\dync) \vdash
\letXbeYinZ {\thunk \rho_{dn}(\u G)} z \rho_{up}(\u G)
\ltdyn
\force w
\bullet
: \rho(\dync)
}
\end{mathpar}
......@@ -996,11 +993,11 @@ booleans.
\begin{theorem}[Interpretation of Casts]
\begin{enumerate}
\item If $A \ltdyn A'$, then $\sem{\upcast A {A'}}\rho$ is
\item If $A \ltdyn A'$, then $\srho{\upcast A {A'}}$ is
thunkable, and $\sem{\upcast A {A'}}$ and $\sem{\dncast {\u F
A}{\u F A}}$ are a value embedding-projection pair.
\item If $\u B \ltdyn \u B'$, then $\sem{\dncast {\u B} {\u
B'}}\rho$ is linear, and $\sem{\dncast {\u B} {\u B'}}\rho$ and
B'}}\rho$ is linear, and $\srho{\dncast {\u B} {\u B'}}$ and
$\sem{\upcast {U \u B} {U \u B'}}$ are a computation
embedding-projection pair.
\end{enumerate}
......@@ -1012,9 +1009,140 @@ booleans.
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,
\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'}}
\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}}
\end{mathpar}
\end{theorem}
\begin{lemma}[Cast Decomposition]
For any dynamic type interpretation $\rho$,
\begin{mathpar}
\inferrule
{A \ltdyn A' \ltdyn A''}
{x : A \vdash \srho{\upcast A {A''}} \equidyn \srho{\upcast {A'} {A''}}[\srho{\upcast {A} {A'}}] : A''}
\inferrule
{\u B \ltdyn \u B' \ltdyn \u B''}
{\bullet : \u B'' \vdash \srho{\dncast{\u B}{\u B''}} \equidyn
\srho{\dncast{\u B}{\u B'}}[\srho{\dncast{\u B'}{\u B''}}]}
\end{mathpar}
\end{lemma}
\begin{lemma}[Casts are Galois Insertions]
For any dynamic type interpretation $\rho$,
\begin{mathpar}
\inferrule
{A \ltdyn A'}
{}
\end{mathpar}
\end{lemma}
\begin{corollary}[Up on the left or Down on the right]
For any dynamic type interpretation $\rho$, if $A \ltdyn A'$ and $\u
B \ltdyn \u B'$ then the following equivalences hold for any
well-typed $V,V',M,M',S,S'$:
\begin{mathpar}
\mprset{fraction={===}}
\inferrule
{\Gamma \vdash \ret\srho{\upcast A{A'}} V \ltdyn M' : \u F \srho{A'}}
{\Gamma \vdash \ret V \ltdyn \srho{\dncast{\u F A}{\u F A'}}[M'] : \u F \srho {A}}
\inferrule
{\Gamma, z' : U {\srho{\u B'}} \vdash M \ltdyn S'[\srho{\dncast {\u B}{\u B'}} \force z] : \u C}
{\Gamma, z : U {\srho{\u B}} \vdash M[\srho{\upcast{U \u B}{U \u B'}} z/z'] \ltdyn S'[\force z] : \u C}
\end{mathpar}
\end{corollary}
Finally, we reach the case-by-case proof of the graduality lemma.
\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{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}
\subsection{Complex Value/Stack Elimination}
Next, to bridge the gap between the semantic notion of complex value
and stack with the more rigid operational notion, we perform a
complexity-elimination pass.
%
This translates any term with complex values in it to an equivalent
(i.e. $\equidyn$) one without complex values, showing that while
complex values are convenient for reasoning, they are not ultimately
\emph{necessary} for compuatation.
%
The high-level idea behind the translation is that complex values all
consist of pattern matching where the continuation is a value, such as
$\pmpairWtoXYinZ V x y V'$.
%
Since our notion of a whole program is a term, and not a value, this
pattern match appears in the context of a larger term: either in a
return, or a function application.
%
Since pattern matching is always a safe operation, it can be lifted up
to the term level, so for instance:
\[ \ret \pmpairWtoXYinZ V x y V' \equidyn \pmpairWtoXYinZ V x y \ret V'\]
and
\[ M\, \pmpairWtoXYinZ V x y V' \equidyn \pmpairWtoXYinZ V x y M\, V'\]
In the equational theory, this transformation is justified by the
$\eta$ laws for the value types: they say exactly that pattern matches
are safe to perform at any point.
%
Note that this can lead to a large blowup of term size, when
eliminating pattern matching for sums.
Our pass is almost exactly the same as the one given in the CBPV
monograph (TODO cite), and so we relegate the details to the extended
version/appendix.
\subsection{Call-by-push-value operational semantics}
We present the operational semantics for our CBPV in figure TODO ref.
......@@ -1031,7 +1159,7 @@ corecursive type.
\begin{figure}
\begin{mathpar}
S[\err] \stepzero \err
S[\err] \stepzero \err\\
S[\caseofXthenYelseZ{\inl V}{x_1. M_1}{x_2. M_2}] \stepzero S[M_1[V/x_1]]\\
S[\caseofXthenYelseZ{\inr V}{x_1. M_1}{x_2. M_2}] \stepzero S[M_2[V/x_2]]\\
S[\pmpairWtoXYinZ{(V_1,V_2)}{x_1}{x_2}{M} \stepzero S[M[V_1/x_1,V_2/x_2]]]\\
......
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