From 64021bd5517f43e83707df72d7aaabd0cfaf29c8 Mon Sep 17 00:00:00 2001
From: Max New <maxsnew@gmail.com>
Date: Tue, 6 Nov 2018 10:23:08 -0500
Subject: [PATCH] some spacey stuff for the long version
---
paper/gtt.tex | 103 +++++++++++++++++++++++++++++++++++---------------
1 file changed, 73 insertions(+), 30 deletions(-)
diff --git a/paper/gtt.tex b/paper/gtt.tex
index b3b1ac7..e71ca80 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -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$.
--
GitLab