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

logical relation parameterized by a pole, some more outline

parent 3e6e8e34
Branches
Tags
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 153 additions and 28 deletions
paper/gtt.tex
+ 153
− 28
View file @ 03d623a3
...@@ -108,6 +108,7 @@ ...@@ -108,6 +108,7 @@
%% DEFINITIONS %% DEFINITIONS
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\nats}{\mathbb{N}}
\newtheorem{principle}{Principle} \newtheorem{principle}{Principle}
\newcommand{\vtype}{\,\,\text{val type}} \newcommand{\vtype}{\,\,\text{val type}}
\newcommand{\ctype}{\,\,\text{comp type}} \newcommand{\ctype}{\,\,\text{comp type}}
...@@ -125,11 +126,22 @@ ...@@ -125,11 +126,22 @@
\newcommand{\ltdynv}{\mathrel{\sqsubseteq_V}} \newcommand{\ltdynv}{\mathrel{\sqsubseteq_V}}
\newcommand{\ltdynt}{\mathrel{\sqsubseteq_T}} \newcommand{\ltdynt}{\mathrel{\sqsubseteq_T}}
\newcommand{\ltlogty}[2]{\mathrel{\ltdyn^{#1}_{#2}}} \newcommand{\ltlogty}[2]{\mathrel{\ltdyn^{#1}_{#2}}}
\newcommand{\pole}{\Bot}
\newcommand{\ipole}[1]{\mathrel{\pole^{#1}}}
\newcommand{\logty}[2]{\mathrel{\lesssim^{#1}_{#2,\pole}}}
\newcommand{\logc}[1]{\mathrel{\pole}^{#1}}
\newcommand{\ltlogc}[1]{\mathrel{\ltdyn^{#1}_{\vdash}}} \newcommand{\ltlogc}[1]{\mathrel{\ltdyn^{#1}_{\vdash}}}
\newcommand{\ltctx}{\mathrel{\ltdyn^{ctx}}} \newcommand{\ltctx}{\mathrel{\ltdyn^{ctx}}}
\newcommand{\ltciu}{\mathrel{\ltdyn^{ciu}}} \newcommand{\ltciu}{\mathrel{\ltdyn^{ciu}}}
\newcommand{\ltlog}{\mathrel{\ltdyn^{log}}} \newcommand{\ltlog}{\mathrel{\ltdyn^{log}}}
%% Operational steps
\newcommand{\step}{\mapsto} \newcommand{\step}{\mapsto}
\newcommand{\stepsin}[1]{\mathrel{\mapsto^{#1}}}
\newcommand{\stepzero}{\stepsin 0}
\newcommand{\stepone}{\stepsin 1}
\newcommand{\bigstepsin}[1]{\mathrel{\Mapsto^{#1}}}
\newcommand{\bigstepzero}{\bigstepsin{0}}
\newcommand{\pair}[2]{\{ \pi \mapsto {#1} \pipe \pi' \mapsto {#2}\}} \newcommand{\pair}[2]{\{ \pi \mapsto {#1} \pipe \pi' \mapsto {#2}\}}
\newcommand{\tru}{\texttt{true}} \newcommand{\tru}{\texttt{true}}
...@@ -147,6 +159,7 @@ ...@@ -147,6 +159,7 @@
\newcommand{\err}{\mho} \newcommand{\err}{\mho}
\newcommand{\print}{\text{print}\,\,} \newcommand{\print}{\text{print}\,\,}
\newcommand{\roll}{\text{roll}\,\,} \newcommand{\roll}{\text{roll}\,\,}
\newcommand{\rollty}[1]{\text{roll}_{#1}\,\,}
\newcommand{\unroll}{\text{unroll}\,\,} \newcommand{\unroll}{\text{unroll}\,\,}
\newcommand{\Set}{\text{Set}} \newcommand{\Set}{\text{Set}}
...@@ -154,10 +167,14 @@ ...@@ -154,10 +167,14 @@
\newcommand{\M}{\mathcal{M}} \newcommand{\M}{\mathcal{M}}
\newcommand{\sq}{\square} \newcommand{\sq}{\square}
\newcommand{\lett}{\text{let}\,\,} \newcommand{\lett}{\text{let}\,\,}
\newcommand{\letXbeYinZ}[2]{\lett#1 = #2;} \newcommand{\letXbeYinZ}[2]{\lett#2 = #1;}
\newcommand{\bindXtoYinZ}[2]{\text{bind}\,\,#2 \leftarrow #1;} \newcommand{\bindXtoYinZ}[2]{\text{bind}\,\,#2 \leftarrow #1;}
\newcommand{\too}{\text{to}\,\,} \newcommand{\too}{\text{to}\,\,}
\newcommand{\case}{\text{case}\,\,} \newcommand{\case}{\text{case}\,\,}
\newcommand{\kw}[1]{\text{#1}\,\,}
\newcommand{\caseofXthenYelseZ}[3]{\case #1 \{ #2 \pipe #3 \}}
\newcommand{\pmpairWtoXYinZ}[4]{\kw{split} #1 \kw{to} (#2,#3). #4}
\newcommand{\pmmuXtoYinZ}[4]{\kw{unroll} #1 \kw{to} \roll #2. #3}
\newcommand{\ret}{\text{ret}\,\,} \newcommand{\ret}{\text{ret}\,\,}
\newcommand{\thunk}{\text{thunk}\,\,} \newcommand{\thunk}{\text{thunk}\,\,}
\newcommand{\force}{\text{force}\,\,} \newcommand{\force}{\text{force}\,\,}
...@@ -216,8 +233,10 @@ ...@@ -216,8 +233,10 @@
determines} the behavior of almost all casts of gradual typing. determines} the behavior of almost all casts of gradual typing.
% %
This shows that any gradual language that supports both must be This shows that any gradual language that supports both must be
equivalent to the lazy system, and any system that differs from it equivalent to the ``wrapping'' semantics, and any system that
must violate graduality or extensionality (typically the latter). differs from it must violate graduality or extensionality (typically
the latter), extending a previous result for a fragment of
call-by-name to full call-by-value and call-by-name.
% %
On the other hand the structure of the dynamic type itself, which is On the other hand the structure of the dynamic type itself, which is
taken for granted to be a sum in previous work, is not uniquely taken for granted to be a sum in previous work, is not uniquely
...@@ -483,6 +502,22 @@ call-by-name calculi, we can provide similar uniqueness theorems for ...@@ -483,6 +502,22 @@ call-by-name calculi, we can provide similar uniqueness theorems for
those systems by restricting GTT to only include the image of those those systems by restricting GTT to only include the image of those
embeddings. embeddings.
Our proof architecture is as follows:
\begin{tikzcd}
GTT \arrow[d] \\
CBPV \arrow[d] \\
LR \simeq CtxApprox
\end{tikzcd}
Our gradual type theory with casts and syntactic theory of term
dynamism is translated to Call-by-push-value with recursive types and
an inequational theory.
%
In fact, we give multiple translations by varying which dynamic types
we have in the source and their interpretation in the target.
%
We then give a model of the CBPV inequational theory using contextual
error approximation over the operational semantics of CBPV.
\section{Axiomatic Gradual Type Theory} \section{Axiomatic Gradual Type Theory}
\subsection{Call-by-Push-Value, Gradualized} \subsection{Call-by-Push-Value, Gradualized}
...@@ -662,8 +697,10 @@ interpreted as value types in call-by-push-value. ...@@ -662,8 +697,10 @@ interpreted as value types in call-by-push-value.
\section{Theorems in Gradual Type Theory} \section{Theorems in Gradual Type Theory}
From the axiomatics of Gradual Type Theory, we can derive many In this section, we derive equational and inequational properties of
consequences. Gradual Type Theory.
\subsection{Basic Structural properties}
\begin{theorem}{Casts (de)composition} \begin{theorem}{Casts (de)composition}
For any $A \ltdyn A' \ltdyn A''$ and $\u B \ltdyn \ltdyn \u B' \ltdyn \u B''$: For any $A \ltdyn A' \ltdyn A''$ and $\u B \ltdyn \ltdyn \u B' \ltdyn \u B''$:
...@@ -675,8 +712,65 @@ consequences. ...@@ -675,8 +712,65 @@ consequences.
\end{enumerate} \end{enumerate}
\end{theorem} \end{theorem}
\subsection{Upcasts are Thunkable, Downcasts are Linear, a posteriori}
While we have shown
\subsection{Uniqueness Principles for Casts}
From the axiomatics of Gradual Type Theory, we can derive many
consequences.
\section{Contract Translation to Call-by-push-value} \section{Contract Translation to Call-by-push-value}
\subsection{Call-by-push-value operational semantics}
We present the operational semantics for our CBPV in figure TODO ref.
%
It is morally the same as one given in the CBPV monograph (TODO:
cite), but there are two differences.
%
First, we present it in a Hieb-Felleisen style, rather than a stack
machine style, which is merely cosmetic.
%
Second, for the purposes of the logical relation, the step relation is
\emph{quantitative}: we count the steps that unroll an recursive or
corecursive type.
\begin{figure}
\begin{mathpar}
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]]]\\
S[\pmmuXtoYinZ{\rollty A V}{x}{M}] \stepone S[M[V/x]]\\
S[\force\thunk M] \stepzero S[M]\\
S[\letXbeYinZ V x M] \stepzero S[M[V/x]]\\
S[\bindXtoYinZ {\ret V} x M] \stepzero S[M[V/x]]\\
S[(\lambda x:A. M)\,V] \stepzero S[M[V/x]]\\
S[\pi \pair{M}{M'}] \stepzero S[M]\\
S[\pi' \pair{M}{M'}] \stepzero S[M']\\
S[\unroll \rollty{\u B} M] \stepone S[M]\\
\inferrule
{}
{M \bigstepsin 0 M}
\inferrule
{M_1 \stepsin{i} M_2 \and M_2 \bigstepsin j M_3}
{M_1 \bigstepsin {i+j} M_3}
\end{mathpar}
\caption{CBPV Operational Semantics}
\end{figure}
\subsection{Call-by-push-value Inequational Theory}
Next, we give the inequational theory for our CBPV language.
%
\subsection{Cast to Contract Translation} \subsection{Cast to Contract Translation}
\subsection{Graduality Logical Relation} \subsection{Graduality Logical Relation}
...@@ -684,38 +778,63 @@ consequences. ...@@ -684,38 +778,63 @@ consequences.
\begin{figure} \begin{figure}
\begin{mathpar} \begin{mathpar}
{\ltlogty{i}{A}} \subseteq \{ \cdot \vdash V : A \}^2 \quad\qquad{\ltlogty{i}{\u B}}\subseteq \{ \cdot \pipe \u B \vdash S : \u F (1 + 1) \}^2\quad\qquad {\ltlogc{i}} \subseteq \{ \cdot \vdash M : \u F (1 + 1) \}^2\\ {\logty{i}{A}} \subseteq \{ \cdot \vdash V : A \}^2 \quad\qquad{\logty{i}{\u B}}\subseteq \{ \cdot \pipe \u B \vdash S : \u F (1 + 1) \}^2\quad\qquad {\logc{i}} \subseteq \{ \cdot \vdash M : \u F (1 + 1) \}^2\\
M_1 \ltlogc{i} M_2 = (M_1 \step^{< i} \err) \vee (M_1, M_2 \step^{i}) \vee (M_1,M_2 \step^{< i} \ret \tru)\vee (M_1,M_2 \step^{< i} \ret \fls)\\
\begin{array}{rcl} \begin{array}{rcl}
\Gamma \vDash M_1 \ltdyn M_2 \in \u B &=& \forall i \in \mathbb{N}, \gamma_1 \ltlogty i \Gamma \gamma_2, S_1 \ltlogty i {\u B} S_2.~ S_1[M_1[\gamma_1]] \ltlogc i S_2[M_2[\gamma_2]]\\ \Gamma \vDash M_1 \ltdyn M_2 \in \u B &=& \forall i \in \mathbb{N}, \gamma_1 \logty i \Gamma \gamma_2, S_1 \logty i {\u B} S_2.~ S_1[M_1[\gamma_1]] \logc i S_2[M_2[\gamma_2]]\\
\Gamma \vDash V_1 \ltdyn V_2 \in A &=& \forall i \in \mathbb{N}, \gamma_1 \ltlogty i \Gamma \gamma_2.~ V_1[\gamma_1] \ltlogty i A V_2[\gamma_2]\\ \Gamma \vDash V_1 \ltdyn V_2 \in A &=& \forall i \in \mathbb{N}, \gamma_1 \logty i \Gamma \gamma_2.~ V_1[\gamma_1] \logty i A V_2[\gamma_2]\\
\Gamma\pipe \bullet : \u B \vDash S_1 \ltdyn S_2 \in \u B' &=& \forall i \in \mathbb{N}, \gamma_1 \ltlogty i \Gamma \gamma_2, S_1' \ltlogty i {\u B'} S_2'.~ S_1'[S_1[\gamma_1]] \ltlogc i S_2'[S_2[\gamma_2]]\\ \Gamma\pipe \bullet : \u B \vDash S_1 \ltdyn S_2 \in \u B' &=& \forall i \in \mathbb{N}, \gamma_1 \logty i \Gamma \gamma_2, S_1' \logty i {\u B'} S_2'.~ S_1'[S_1[\gamma_1]] \logc i S_2'[S_2[\gamma_2]]\\
\end{array}\\ \end{array}\\
\begin{array}{rcl} \begin{array}{rcl}
\cdot \ltlogty i {\cdot} \cdot &=& \top\\ \cdot \logty i {\cdot} \cdot &=& \top\\
\gamma_1,x \mapsto V_1 \ltlogty i {\Gamma,x:A} \gamma_2,x\mapsto V_2 &=& \gamma_1 \ltlogty i \Gamma \gamma_2 \wedge V_1 \ltlogty i A V_2\\ \gamma_1,x \mapsto V_1 \logty i {\Gamma,x:A} \gamma_2,x\mapsto V_2 &=& \gamma_1 \logty i \Gamma \gamma_2 \wedge V_1 \logty i A V_2\\
V_1 \ltlogty i 0 V_2 &=& \bot\\ V_1 \logty i 0 V_2 &=& \bot\\
\inl V_1 \ltlogty i {A + A'} \inl V_2 &= & V_1 \ltlogty i A V_2\\ \inl V_1 \logty i {A + A'} \inl V_2 &= & V_1 \logty i A V_2\\
\inr V_1 \ltlogty i {A + A'} \inr V_2 &= & V_1 \ltlogty i {A'} V_2 \\ \inr V_1 \logty i {A + A'} \inr V_2 &= & V_1 \logty i {A'} V_2 \\
() \ltlogty i 1 () &=& \top\\ () \logty i 1 () &=& \top\\
(V_1,V_1') \ltlogty i {A \times A'} (V_2, V_2') &=& V_1 \ltlogty i A V_2 \wedge V_1' \ltlogty i {A'} V_2'\\ (V_1,V_1') \logty i {A \times A'} (V_2, V_2') &=& V_1 \logty i A V_2 \wedge V_1' \logty i {A'} V_2'\\
% Should this be a roll or not? % Should this be a roll or not?
\roll_{\mu X. A} V_1 \ltlogty 0 {\mu X. A} \roll_{\mu X. A} V_2 &=& \top\\ \rollty {\mu X. A} V_1 \logty 0 {\mu X. A} \rollty {\mu X. A} V_2 &=& \top\\
\roll_{\mu X. A} V_1 \ltlogty {i+1} {\mu X. A} \roll_{\mu X. A} V_2 &=& V_1 \ltlogty i {A[\mu X.A/X]} V_2\\ \rollty {\mu X. A} V_1 \logty {i+1} {\mu X. A} \rollty {\mu X. A} V_2 &=& V_1 \logty i {A[\mu X.A/X]} V_2\\
V_1 \ltlogty i {U \u B} V_2 &=& \forall j \leq i, S_1 \ltlogty j {\u B} S_2.~ S_1[\force V_1] \ltlogc j S_2[\force V_2] \\\\ V_1 \logty i {U \u B} V_2 &=& \forall j \leq i, S_1 \logty j {\u B} S_2.~ S_1[\force V_1] \logc j S_2[\force V_2] \\\\
S_1[\bullet V_1] \ltlogty i {A \to \u B} S_1[\bullet V_2] & = & V_1 \ltlogty i A V_2 \wedge S_1 \ltlogty {i}{\u B} S_2\\ S_1[\bullet V_1] \logty i {A \to \u B} S_1[\bullet V_2] & = & V_1 \logty i A V_2 \wedge S_1 \logty {i}{\u B} S_2\\
S_1[\pi_1 \bullet] \ltlogty i {\u B \wedge \u B'} S_2[\pi_1 \bullet] &=& S_1 \ltlogty i {\u B} S_2\\ S_1[\pi_1 \bullet] \logty i {\u B \wedge \u B'} S_2[\pi_1 \bullet] &=& S_1 \logty i {\u B} S_2\\
S_1[\pi_2 \bullet] \ltlogty i {\u B \wedge \u B'} S_2[\pi_2 \bullet] &=& S_1 \ltlogty i {\u B'} S_2\\ S_1[\pi_2 \bullet] \logty i {\u B \wedge \u B'} S_2[\pi_2 \bullet] &=& S_1 \logty i {\u B'} S_2\\
S_1 \ltlogty i {\top} S_2 &=& \bot\\ S_1 \logty i {\top} S_2 &=& \bot\\
S_1[\unroll \bullet] \ltlogty 0 {\nu \u Y. \u B} S_2[\unroll \bullet] &=& \top\\ S_1[\unroll \bullet] \logty 0 {\nu \u Y. \u B} S_2[\unroll \bullet] &=& \top\\
S_1[\unroll \bullet] \ltlogty {i+1} {\nu \u Y. \u B} S_2[\unroll \bullet] &=& S_1 \ltlogty i {\u B[\nu \u Y. \u B/\u Y]} S_2\\ S_1[\unroll \bullet] \logty {i+1} {\nu \u Y. \u B} S_2[\unroll \bullet] &=& S_1 \logty i {\u B[\nu \u Y. \u B/\u Y]} S_2\\
S_1 \ltlogty i {\u F A} S_2 & = & \forall j\leq i, V_1 \ltlogty j A V_2.~ S_1[\ret V_1] \ltlogc j S_2[\ret V_2] S_1 \logty i {\u F A} S_2 & = & \forall j\leq i, V_1 \logty j A V_2.~ S_1[\ret V_1] \logc j S_2[\ret V_2]
\end{array} \end{array}
\end{mathpar} \end{mathpar}
\caption{Observational Error Approximation Logical Relation} \caption{Observational Error Approximation Logical Relation}
\end{figure} \end{figure}
\begin{definition}[Pole]
A \emph{pole} $\pole$ is a function from natural numbers to sets of
closed programs of type $\u F (1 + 1)$ satisfying
\begin{enumerate}
\item Downward closure: If $M_1 \ipole i M_2$ and $j \leq i$ then $M_1 \ipole j M_2$.
\item Step-indexed anti-reduction: If $M_1 \stepsin j M_1'$ and $M_2
\step M_2'$ and $M_1' \ipole i M_2'$ then $M_1' \ipole {i+j} M_2'$.
\item Step-indexed transitivity: If $M_1 \ipole i M_2$ and $M_2
\ipole \omega M_3$ then $M_1 \ipole i M_3$.
% TODO: might as well make error the least element? not sure
\item Error awareness: For all $i \in \nats$, $\err \ipole i \err$.
\end{enumerate}
\end{definition}
\begin{theorem}[Logical Relations Theorem/Fundamental property]
For any pole $\pole$, the logical relation generated by it is a
congruence, i.e. a model of the congruence rules of CBPV.
\end{theorem}
\begin{proof}
By induction on the congruence proofs of CBPV.
\begin{enumerate}
\item
\end{enumerate}
\end{proof}
\begin{theorem}[LR is Sound for Contextual Error Approximation] \begin{theorem}[LR is Sound for Contextual Error Approximation]
\begin{enumerate} \begin{enumerate}
\item If $\Gamma \vDash M_1 \ltdyn M_2 \in \u B$, then $\Gamma \vDash M_1 \ltctx M_2 \in \u B$. \item If $\Gamma \vDash M_1 \ltdyn M_2 \in \u B$, then $\Gamma \vDash M_1 \ltctx M_2 \in \u B$.
...@@ -971,6 +1090,12 @@ This gives some evidence that the specific choice of connectives of ...@@ -971,6 +1090,12 @@ This gives some evidence that the specific choice of connectives of
CBPV occupies a certain ``sweet spot'' between semantic expressivity CBPV occupies a certain ``sweet spot'' between semantic expressivity
and amenability to extensions. and amenability to extensions.
\appendix
\section{Call-by-value Gradual Type Theory}
\section{Call-by-name Gradual Type Theory}
\end{document} \end{document}
%% Local Variables: %% Local Variables:
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment