From da77a185ad4d4fcc7dc53c6c7abeccc9f6dca7ae Mon Sep 17 00:00:00 2001
From: Dan Licata <drl@cs.cmu.edu>
Date: Fri, 6 Jul 2018 10:58:22 -0400
Subject: [PATCH] editing
---
paper/gtt.tex | 91 +++++++++++++++++++++++++++++++++------------------
1 file changed, 60 insertions(+), 31 deletions(-)
diff --git a/paper/gtt.tex b/paper/gtt.tex
index d30f422..ab62b39 100644
--- a/paper/gtt.tex
+++ b/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}
--
GitLab