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

some spacey stuff for the long version

parent ae86766d
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 73 additions and 30 deletions
paper/gtt.tex
+ 73
− 30
View file @ 64021bd5
......@@ -1691,7 +1691,53 @@ our design choice is forced for all casts, as long as the casts between ground t
}
{\Phi \mid \Psi \vdash M_2[M_1/\bullet] \ltdyn M_2'[M_1'/\bullet] : \u B_2 \ltdyn \u B_2'}
\\\\
\ifshort
\inferrule*[lab=$\times$ICong]
{\Phi \vdash V_1 \ltdyn V_1' : A_1 \ltdyn A_1'\\\\
\Phi\vdash V_2 \ltdyn V_2' : A_2 \ltdyn A_2'}
{\Phi \vdash (V_1,V_2) \ltdyn (V_1',V_2') : A_1 \times A_2 \ltdyn A_1' \times A_2'}
\quad
\inferrule*[lab=$\to$ICong]
{\Phi, x \ltdyn x' : A \ltdyn A' \pipe \Psi \vdash M \ltdyn M' : \u B \ltdyn \u B'}
{\Phi \pipe \Psi \vdash \lambda x : A . M \ltdyn \lambda x' : A' . M' : A \to \u B \ltdyn A' \to \u B'}
\\\\
\inferrule*[lab=$\times$ECong]
{\Phi \vdash V \ltdyn V' : A_1 \times A_2 \ltdyn A_1' \times A_2' \\\\
\Phi, x \ltdyn x' : A_1 \ltdyn A_1', y \ltdyn y' : A_2 \ltdyn A_2' \mid \Psi \vdash E \ltdyn E' : T \ltdyn T'
}
{\Phi \mid \Psi \vdash \pmpairWtoXYinZ V x y E \ltdyn \pmpairWtoXYinZ {V'} {x'} {y'} {E'} : T \ltdyn T'}
\,\,
\inferrule*[lab=$\to$ECong]
{\Phi \pipe \Psi \vdash M \ltdyn M' : A \to \u B \ltdyn A' \to \u B' \\\\
\Phi \vdash V \ltdyn V' : A \ltdyn A'}
{\Phi \pipe \Psi \vdash M\,V \ltdyn M'\,V' : \u B \ltdyn \u B' }
\\\\
\inferrule*[lab=$F$ICong]
{\Phi \vdash V \ltdyn V' : A \ltdyn A'}
{\Phi \pipe \cdot \vdash \ret V \ltdyn \ret V' : \u F A \ltdyn \u F A'}
\qquad
\inferrule*[lab=$F$ECong]
{\Phi \pipe \Psi \vdash M \ltdyn M' : \u F A \ltdyn \u F A' \\\\
\Phi, x \ltdyn x' : A \ltdyn A' \pipe \cdot \vdash N \ltdyn N' : \u B \ltdyn \u B'}
{\Phi \pipe \Psi \vdash \bindXtoYinZ M x N \ltdyn \bindXtoYinZ {M'} {x'} {N'} : \u B \ltdyn \u B'}
\\\\
\fi
\end{array}
\]
\vspace{-0.25in}
\caption{GTT Term Dynamism (Structural \ifshort and Congruence\fi Rules) \ifshort
(Rules for $U,1,+,0,\with,\top$ in extended version)
\fi}
\label{fig:gtt-term-dynamism-structural}
\end{small}
\end{figure}
\iflong
\begin{figure}
\begin{small}
\[
\begin{array}{c}
\inferrule*[lab=$+$IlCong]
{\Phi \vdash V \ltdyn V' : A_1 \ltdyn A_1'}
{\Phi \vdash \inl V \ltdyn \inl V' : A_1 + A_2 \ltdyn A_1' + A_2'}
......@@ -1720,7 +1766,6 @@ our design choice is forced for all casts, as long as the casts between ground t
}
{\Phi \mid \Psi \vdash \pmpairWtoinZ V E \ltdyn \pmpairWtoinZ V' E' : T \ltdyn T'}
\\\\
\fi
\inferrule*[lab=$\times$ICong]
{\Phi \vdash V_1 \ltdyn V_1' : A_1 \ltdyn A_1'\\\\
\Phi\vdash V_2 \ltdyn V_2' : A_2 \ltdyn A_2'}
......@@ -1742,7 +1787,6 @@ our design choice is forced for all casts, as long as the casts between ground t
\Phi \vdash V \ltdyn V' : A \ltdyn A'}
{\Phi \pipe \Psi \vdash M\,V \ltdyn M'\,V' : \u B \ltdyn \u B' }
\\\\
\iflong
\inferrule*[lab=$U$ICong]
{\Phi \mid \cdot \vdash M \ltdyn M' : \u B \ltdyn \u B'}
{\Phi \vdash \thunk M \ltdyn \thunk M' : U \u B \ltdyn U \u B'}
......@@ -1751,7 +1795,6 @@ our design choice is forced for all casts, as long as the casts between ground t
{\Phi \vdash V \ltdyn V' : U \u B \ltdyn U \u B'}
{\Phi \pipe \cdot \vdash \force V \ltdyn \force V' : \u B \ltdyn \u B'}
\\\\
\fi
\inferrule*[lab=$F$ICong]
{\Phi \vdash V \ltdyn V' : A \ltdyn A'}
{\Phi \pipe \cdot \vdash \ret V \ltdyn \ret V' : \u F A \ltdyn \u F A'}
......@@ -1761,7 +1804,6 @@ our design choice is forced for all casts, as long as the casts between ground t
\Phi, x \ltdyn x' : A \ltdyn A' \pipe \cdot \vdash N \ltdyn N' : \u B \ltdyn \u B'}
{\Phi \pipe \Psi \vdash \bindXtoYinZ M x N \ltdyn \bindXtoYinZ {M'} {x'} {N'} : \u B \ltdyn \u B'}
\\\\
\iflong
\inferrule*[lab=$\top$ICong]{ }{\Phi \mid \Psi \vdash \{\} \ltdyn \{\} : \top \ltdyn \top}
\qquad
\inferrule*[lab=$\with$ICong]
......@@ -1776,16 +1818,13 @@ our design choice is forced for all casts, as long as the casts between ground t
\inferrule*[lab=$\with$E'Cong]
{\Phi \mid \Psi \vdash M \ltdyn M' : \u B_1 \with \u B_2 \ltdyn \u B_1' \with \u B_2'}
{\Phi \mid \Psi \vdash \pi' M \ltdyn \pi' M' : \u B_2 \ltdyn \u B_2'}
\fi
\end{array}
\]
\vspace{-0.25in}
\caption{GTT Term Dynamism (Structural and Congruence Rules) \ifshort
(Rules for $U,1,+,0,\with,\top$ in extended version)
\fi}
\label{fig:gtt-term-dynamism-structural}
\caption{GTT Term Dynamism (Congruence Rules)}
\label{fig:gtt-term-dynamism-ext-congruence}
\end{small}
\end{figure}
\fi
The final piece of GTT is the \emph{term dynamism} relation, a syntactic
judgement that is used for reasoning about the behavioral properties of
......@@ -1832,7 +1871,7 @@ that the type satisfies in a non-gradual language. Thus, adding a new
type to gradual type theory does not require any a priori consideration
of its gradual behavior in the language definition; instead, this is
deduced as a theorem in the type theory. The basic structural rules of
term dynamism in Figure~\ref{fig:gtt-term-dynamism-structural} say that
term dynamism in Figure~\ref{fig:gtt-term-dynamism-structural}\iflong\ and Figure~\ref{fig:gtt-term-dynamism-ext-congruence}\fi\ say that
it is reflexive and transitive (\textsc{TmDynRefl},
\textsc{TmDynTrans}), that assumptions can be used and substituted for
(\textsc{TmDynVar}, \textsc{TmDynValSubst}, \textsc{TmDynHole},
......@@ -2324,7 +2363,7 @@ and then substitution of the premise into this gives the conclusion.
\end{longproof}
Though we did not include congruence rules for casts in
Figure~\ref{fig:gtt-term-dynamism-structural}, it is derivable:
Figure~\ifshort\ref{fig:gtt-term-dynamism-structural}\else\ref{fig:gtt-term-dynamism-ext-congruence}\fi, it is derivable:
\begin{lemma}[Cast congruence rules] \label{lem:cast-congruence}
The following congruence rules for casts are derivable:
\begin{small}
......@@ -3752,7 +3791,7 @@ This suggests taking $\bot_v := 0$ and $\bot_c := \top$.
%% $0 \ltdyn A$ and $\top \ltdyn \u B$, in which case we have:
%% \end{shortonly}
\begin{theorem}
The casts determined $0 \ltdyn A$ are
The casts determined by $0 \ltdyn A$ are
\[
\upcast{0}{A}z \equidyn \absurd z \qquad \dncast{\u F 0}{\u F A}{\bullet} \equidyn \bindXtoYinZ{\bullet}{\_}{\err}
\]
......@@ -4215,7 +4254,7 @@ casts and the dynamic types $\dynv, \dync$ (the shaded pieces) from the
syntax and typing rules in Figure~\ref{fig:gtt-syntax-and-terms}. There
is no type dynamism, and the inequational theory of \cbpv* is the
homogeneous fragment of term dynamism in
Figure~\ref{fig:gtt-term-dynamism-structural} (judgements $\Gamma \vdash
Figure~\ref{fig:gtt-term-dynamism-structural}\iflong\ and Figure~\ref{fig:gtt-term-dynamism-ext-congruence}\fi\ (judgements $\Gamma \vdash
E \ltdyn E' : T$ where $\Gamma \vdash E,E' : T$, with all the same rules
in that figure thus restricted). The inequational axioms are the
Type Universal Properties ($\beta\eta$ rules)
......@@ -6580,9 +6619,11 @@ introduction/elimination forms, and are all simple calculations.
&\pmpairWtoXYinZ {\sem V} x y {\sem{M}[\sem{\Psi}]}\\
&\ltdyn\pmpairWtoXYinZ {\sem V} x y \sdncast{\u B}{\u B'}[\sem{M'}[\sem\Phi][\supcast{A_1}{A_1'}[x]/x'][\supcast{A_2}{A_2'}[y]/y']]\tag{IH}\\
&\equidyn
\pmpairWtoXYinZ {\sem V} x y \pmpairWtoXYinZ {(\supcast{A_1}{A_1'}[x],\supcast{A_2}{A_2'}[y])} {x'} {y'} \sdncast{\u B}{\u B'}[\sem{M'}[\sem\Phi]]\tag{$\times\beta$}\\
\pmpairWtoXYinZ {\sem V} x y\tag{$\times\beta$}\\
&\qquad \pmpairWtoXYinZ {(\supcast{A_1}{A_1'}[x],\supcast{A_2}{A_2'}[y])} {x'} {y'} \sdncast{\u B}{\u B'}[\sem{M'}[\sem\Phi]]\\
&\equidyn
\pmpairWtoXYinZ {\sem V} x y\pmpairWtoXYinZ {\supcast{A_1\times A_2'}{A_1'\times A_2'}[(x,y)]} {x'} {y'} \sdncast{\u B}{\u B'}[\sem{M'}[\sem\Phi]]\tag{cast reduction}\\
\pmpairWtoXYinZ {\sem V} x y\tag{cast reduction}\\
&\qquad \pmpairWtoXYinZ {\supcast{A_1\times A_2'}{A_1'\times A_2'}[(x,y)]} {x'} {y'} \sdncast{\u B}{\u B'}[\sem{M'}[\sem\Phi]]\\
&\equidyn
\pmpairWtoXYinZ {\supcast{A_1\times A_2}{A_1'\times A_2'}[{\sem V}]} {x'} {y'} \sdncast{\u B}{\u B'}[\sem{M'}[\sem\Phi]]\tag{$\times\eta$}\\
&\ltdyn \pmpairWtoXYinZ {\sem{V'}[\sem\Phi]} {x'}{y'} \sdncast{\u B}{\u B'}[\sem{M'}[\sem\Phi]]\tag{IH}\\
......@@ -7508,7 +7549,9 @@ morphisms from smaller ones.
\[ \caseofXthenYelseZ V {y_1. M_1} {y_2. M_2} \]
is linear in $x$.
\begin{align*}
& \caseofXthenYelseZ V {y_1. M_1[\thunk{(\bindXtoYinZ {\force z} x \force x)}/x]} {y_2. M_2[\thunk{(\bindXtoYinZ {\force z} x \force x)}/x]}\\
& \caseofX V\\
& \,\,\thenY {y_1. M_1[\thunk{(\bindXtoYinZ {\force z} x \force x)}/x]}\\
& \,\,\elseZ {y_2. M_2[\thunk{(\bindXtoYinZ {\force z} x \force x)}/x]}\\
&\equidyn \caseofXthenYelseZ V {y_1. \bindXtoYinZ {\force z} x M_1}{y_2. \bindXtoYinZ {\force z} x M_2}\tag{$M_1,M_2$ linear}\\
&\equidyn
\bindXtoYinZ {\force z} x \caseofXthenYelseZ V {y_1. M_1}{y_2. M_2}
......@@ -7945,22 +7988,22 @@ values/stacks). Using contexts, we can lift any relation on
C_V & ::= [\cdot] & \rollty{\mu X.A}C_V \mid \inl{C_V} \mid \inr{C_V} \mid (C_V,V)\mid(V,C_V)\mid \thunk{C_M}\\
\\
C_M & ::= & [\cdot] \mid \letXbeYinZ {C_V} x M \mid \letXbeYinZ V x
C_M \mid \pmmuXtoYinZ {C_V} x M \mid\pmmuXtoYinZ V x C_M \mid \\
& & \rollty{\nu \u Y.\u B} C_M \mid \unroll C_M \mid \abort{C_V} \mid \\
& & \caseofXthenYelseZ {C_V} {x_1. M_1}{x_2.M_2}
C_M \mid \pmmuXtoYinZ {C_V} x M \mid\pmmuXtoYinZ V x C_M \\
& & \mid \rollty{\nu \u Y.\u B} C_M \mid \unroll C_M \mid \abort{C_V} \mid \caseofXthenYelseZ {C_V} {x_1. M_1}{x_2.M_2} \\
& &
\mid\caseofXthenYelseZ V {x_1. C_M}{x_2.M_2} \mid\caseofXthenYelseZ
V {x_1. M_1}{x_2.C_M} \mid\\
& & \pmpairWtoinZ {C_V} M \mid \pmpairWtoinZ V C_M \mid \pmpairWtoXYinZ {C_V} x y M\mid \pmpairWtoXYinZ V x y C_M
\mid \force{C_V} \mid \\
& & \ret{C_V} \mid \bindXtoYinZ{C_M}{x}{N}
\mid\bindXtoYinZ{M}{x}{C_M} \mid \lambda x:A.C_M \mid C_M\,V \mid M\,C_V \mid\\
& & \pair{C_M}{M_2}\mid \pair{M_1}{C_M} \mid \pi C_M \mid \pi' C_M
V {x_1. M_1}{x_2.C_M} \mid \pmpairWtoinZ {C_V} M\\
& & \mid \pmpairWtoinZ V C_M \mid \pmpairWtoXYinZ {C_V} x y M\mid \pmpairWtoXYinZ V x y C_M
\mid \force{C_V} \\
& & \mid \ret{C_V} \mid \bindXtoYinZ{C_M}{x}{N}
\mid\bindXtoYinZ{M}{x}{C_M} \mid \lambda x:A.C_M \mid C_M\,V \mid M\,C_V \\
& & \mid \pair{C_M}{M_2}\mid \pair{M_1}{C_M} \mid \pi C_M \mid \pi' C_M
\\
C_S &=& \pi C_S \mid \pi' C_S \mid S\,C_V\mid C_S\,V\mid \bindXtoYinZ {C_S} x M \mid \bindXtoYinZ S x C_M
\end{array}
\end{mathpar}
\end{small}
\caption{CBPV Context}
\caption{CBPV Contexts}
\end{longfigure}
\begin{shortonly}
......@@ -8649,7 +8692,7 @@ Next, we show the fundamental theorem:
\Gamma, x_1 : A_1 \vDash M_1 \ilr i M_1' \in \u B\and
\Gamma, x_2 : A_2 \vDash M_2 \ilr i M_2' \in \u B
}
{\Gamma \vDash \caseofXthenYelseZ V {x_1. M_1}{x_2.M_2} \ilr i \caseofXthenYelseZ {V'} {x_1. M_1'}{x_2.M_2'} \in \u B}$
{\Gamma \vDash \caseofXthenYelseZ V {x_1. M_1}{x_2.M_2} \ilr i \caseofXthenYelseZ {V'} {x_1. M_1'}{x_2.M_2'} \in \u B}$\\
By case analysis of $V[\gamma_1] \ilr i V'[\gamma_2]$.
\begin{enumerate}
\item If $V[\gamma_1]=\inl V_1, V'[\gamma_2] = \inl V_1'$ with
......@@ -8711,14 +8754,14 @@ Next, we show the fundamental theorem:
Which follows by downward-closure for terms and substitutions.
\item $\inferrule {\Gamma \vDash V \ilr i V' \in U \u B} {\Gamma
\vDash \force V \ilr i \force V' \in \u B}$. We need to show
\vDash \force V \ilr i \force V' \in \u B}$. \\ We need to show
$S_1[\force V[\gamma_1]] \ix\apreorder i \result(S_2[\force
V'[\gamma_2]])$, which follows by the definition of $V[\gamma_1]
\itylr i {U \u B} V'[\gamma_2]$.
\item $\inferrule
{\Gamma \vDash V \ilr i V' \in A}
{\Gamma \vDash \ret V \ilr i \ret V' \in \u F A}$
{\Gamma \vDash \ret V \ilr i \ret V' \in \u F A}$\\
We need to show $S_1[\ret V[\gamma_1]] \ix\apreorder i \result(S_2[\ret
V'[\gamma_2]])$, which follows by the orthogonality definition of
$S_1 \itylr i {\u F A} S_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