editing

paper/gtt.tex

@@ -1559,13 +1559,35 @@ interpreted as value types in call-by-push-value.
 \section{Theorems in Gradual Type Theory}
 
 In this section, we derive equational and inequational properties of
-Gradual Type Theory.  In what follows, ``unique'' means up to $\equidyn$.  
+Gradual Type Theory.
 
-\subsection{Basic structure of GTT}
+In what follows, ``unique'' means up to term equidynamism $\equidyn$.
 
-GTT inherits a lot of stuff from CPBV, for example [TODO: cite CPBV book]
+\subsection{Inclusion of CBPV}
 
-\begin{lemma}[Intitial objects] \label{lem:initial}
+Because the GTT term equidynamism relation includes the congruence and
+$\beta\eta$ axioms of call-by-push-value, the types inherit the
+universal properties they have there~\cite{cpbv}.  We recall some
+relevant definitions and facts:
+
+\begin{definition}[Isomorphism] ~
+  \begin{enumerate}
+  \item We write $A \cong_v A'$ for a \emph{value isomorphism between
+    $A$ and $A'$}, which consists of two complex values $x : A \vdash V'
+    : A'$ and $x' : A' \vdash V : A$ such that $x : A \vdash V[V'/x']
+    \equidyn x : A$ and $x' : A' \vdash V'[V/x] \equidyn x' : A'$.
+  \item We write $\u B \cong_v \u B'$ for a \emph{computation
+    isomorphism between $\u B$ and $\u B'$}, which consists of two
+    complex stacls $\bullet : \u B \vdash S' : \u B'$ and $\bullet' : \u
+    B' \vdash S : \u B$ such that $\bullet : \u B \vdash S[S'/x']
+    \equidyn \bullet : \u B$ and $\bullet' : \u B' \vdash S'[S/\bullet]
+    \equidyn \bullet' : \u B'$.
+  \end{enumerate}
+\end{definition}
+
+\smallskip
+
+\begin{lemma}[Intitial objects] ~ \label{lem:initial}
   \begin{enumerate}
   \item For all (value or computation) types $T$, there exists a unique
     expression $x : 0 \vdash E : T$.
@@ -1579,7 +1601,7 @@ GTT inherits a lot of stuff from CPBV, for example [TODO: cite CPBV book]
   \item $\u F 0$ is not provably \emph{strictly} initial among computation types.
   \end{enumerate}
 \end{lemma}
-  \begin{proof}
+\begin{proof}~
     \begin{enumerate}
     \item Take $E$ to be $x : 0 \vdash \abort{x} : T$.  Given any $E'$,
       we have $E \equidyn E'$ by the $\eta$ principle for $0$.
@@ -1626,7 +1648,7 @@ GTT inherits a lot of stuff from CPBV, for example [TODO: cite CPBV book]
     \end{enumerate}
 \end{proof}
   
-  \begin{lemma}[Terminal objects] \label{lem:terminal}
+  \begin{lemma}[Terminal objects] ~ \label{lem:terminal}
     \begin{enumerate}
     \item For any computation type $\u B$, there exists a unique stack
       $\bullet : \u B \vdash S : \top$.
@@ -1638,7 +1660,7 @@ GTT inherits a lot of stuff from CPBV, for example [TODO: cite CPBV book]
     \item $\top$ is not a strict terminal object.  
     \end{enumerate}
   \end{lemma}
-  \begin{proof}
+  \begin{proof} ~
     \begin{enumerate}
     \item Take $S = \{\}$.  The $\eta$ rule for $\top$, $\bullet : \top
       \vdash \bullet \equidyn \{\} : \top$, under the substitution of
@@ -1672,10 +1694,12 @@ GTT inherits a lot of stuff from CPBV, for example [TODO: cite CPBV book]
 
 \subsection{Derived Cast Rules}
 
-Some helpful derived rules:
+The cast universal properties in Figure~\ref{fig:gtt-term-dyn-axioms}
+imply a number of seemingly more general rules for reasoning about
+casts, which will be helpful for the proofs below:
 
 \begin{lemma}[Shifted Casts]
-  The following are derivable
+  The following are derivable:
   \begin{mathpar}
       \inferrule
     {\Gamma \pipe \Delta \vdash M : \u F A' \and A \ltdyn A'}
@@ -1785,10 +1809,12 @@ $\dncast{\u B}{\u B''}{\bullet''}\ltdyn {\bullet''} : \u B \ltdyn \u B''$,
 which is true by downcast left.
 \end{proof}
 
-\subsection{Type-generic Cast Properties}
+\subsection{Type-generic Properties of Casts}
+
+The following results apply to casts in any types:
 
-\begin{theorem}{Casts (de)composition} \label{thm:decomposition}
-  For any $A \ltdyn A' \ltdyn A''$ and $\u B \ltdyn \ltdyn \u B' \ltdyn \u B''$:
+\begin{theorem}[Casts (de)composition] \label{thm:decomposition}
+  For any $A \ltdyn A' \ltdyn A''$ and $\u B \ltdyn \u B' \ltdyn \u B''$:
   \begin{enumerate}
   \item $x : A \vdash \upcast A A x \equidyn x : A$
   \item $x : A \vdash \upcast A {A''}x \equidyn \upcast{A'}{A''}\upcast A{A'} x : A''$
@@ -1799,7 +1825,7 @@ which is true by downcast left.
   \end{enumerate}
 \end{theorem}
 
-\begin{proof}
+\begin{proof} ~
 \begin{enumerate}
 \item To show $x : A \vdash \upcast A A x \ltdyn x$, by upcast left, it
   suffices to show $x : A \vdash x \ltdyn x$, which is true by the
@@ -1853,7 +1879,7 @@ x : A \vdash \upcast{A}{\dynv}{x} \equidyn \upcast{A'}{\dynv}{\upcast{A}{A'}{x}}
   \item $x : U \u B \vdash x \ltdyn \thunk{(\dncast{B}{B'}{(\force{(\upcast{U \u B}{U \u B'}{x})})})} : U \u B$
   \end{enumerate}
 \end{theorem}
-\begin{proof}
+\begin{proof} ~
   \begin{enumerate}
   \item By $\eta$ for $F$ types, $\bullet' : \u F A' \vdash \bullet'
     \equidyn \bindXtoYinZ{\bullet'}{x'}{\ret{x'}} : \u F A'$, so it
@@ -1921,7 +1947,7 @@ x : A \vdash \upcast{A}{\dynv}{x} \equidyn \upcast{A'}{\dynv}{\upcast{A}{A'}{x}}
 \end{proof}
 
 In Figure~\ref{fig:gtt-term-dyn-axioms}, we asserted the retract axiom
-for casts into the dynamic type.  More generally, we have
+for casts into the dynamic type.  More generally:
 \begin{theorem}{Retract Property for General Casts}
   \begin{enumerate}
   \item
@@ -1984,39 +2010,42 @@ for casts into the dynamic type.  More generally, we have
 The specification of upcasts and downcasts by their right and left
 $\ltdyn$ rules defines them \emph{uniquely} up to $\equidyn$.
 %
-In category-theoretic terms this says that the upcasts and downcasts
-have a \emph{universal property}, and so we can show that something
-else is equivalent to the upcast or downcast by showing that it has
-the \emph{same} property.
+In category-theoretic terms this says that ``being an upcast/downcast''
+is a \emph{universal property}, and so we can show that something else
+is equivalent to the upcast or downcast by showing that it has the
+\emph{same} property.
 %
 
-\begin{theorem}{Specification for Casts is a Universal Property} \label{thm:casts-unique}
-  If $A \ltdyn A'$ and $x : A \vdash V_u[x] : A'$ is a value such that
-  the following judgments are provable:
+\begin{theorem}[Specification for Casts is a Universal Property]
+  ~ \label{thm:casts-unique}
+  \begin{enumerate}
+  \item 
+  If $A \ltdyn A'$ and $x : A \vdash V[x] : A'$ is a value such that
   \begin{mathpar}
     \inferrule
     {}
-    {x : A \ltdyn x' : A' \vdash V_u[x] \ltdyn x' : A'}
+    {x : A \ltdyn x' : A' \vdash V[x] \ltdyn x' : A'}
 
     \inferrule
     {}
-    {x_2 : A \ltdyn x : A \vdash x_2 \ltdyn V_u[x] : A \ltdyn A'}
+    {x_2 : A \ltdyn x : A \vdash x_2 \ltdyn V[x] : A \ltdyn A'}
   \end{mathpar}
+  then $x : A \vdash V \equidyn x : A$.
 
-  then we can prove $x : A \vdash V_u[x] \equidyn x : A$.
-
-  Similarly, if $\u B \ltdyn \u B'$ and $\bullet : \u B' \vdash S_d :
-  \u B$ is a stack such that the following are provable:
+  \item 
+  If $\u B \ltdyn \u B'$ and $\bullet : \u B' \vdash S :
+  \u B$ is a stack such that
   \begin{mathpar}
     \inferrule
     {}
-    {\bullet \ltdyn \bullet : \u B' \vdash S_d \ltdyn \bullet : \u B \ltdyn \u B'}
+    {\bullet \ltdyn \bullet : \u B' \vdash S \ltdyn \bullet : \u B \ltdyn \u B'}
 
     \inferrule
     {}
-    {\bullet \ltdyn \bullet : \u B \ltdyn \u B' \vdash \bullet \ltdyn S_d : \u B}
+    {\bullet \ltdyn \bullet : \u B \ltdyn \u B' \vdash \bullet \ltdyn S : \u B}
   \end{mathpar}
-  then we can prove $\bullet : \u B' \vdash S_d \equidyn \dncast{\u B}{\u B'}\bullet : \u B$
+  then $\bullet : \u B' \vdash S \equidyn \dncast{\u B}{\u B'}\bullet : \u B$
+  \end{enumerate}
 \end{theorem}
 \begin{proof}
   \begin{mathpar}