From cb57f25c154fa8891131096e4d37265046c40bc8 Mon Sep 17 00:00:00 2001
From: Max New <maxsnew@gmail.com>
Date: Thu, 25 Oct 2018 10:43:07 -0400
Subject: [PATCH] contributions, various edits
---
paper/gtt.tex | 63 +++++++++++++++++++++++++++++++++++++++++----------
1 file changed, 51 insertions(+), 12 deletions(-)
diff --git a/paper/gtt.tex b/paper/gtt.tex
index dfe6f55..bb7a081 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -767,6 +767,46 @@ functions.
Our modular proof architecture allows us to easily prove correctness
of $\beta, \eta$ and graduality for all of these interpretations.
+\textbf{Contributions}
+
+The main contributions of the paper are as follows.
+\begin{enumerate}
+\item We present Gradual Type Theory in \secref{sec:gtt}, a simple
+ axiomatic theory of gradual typing. The theory axiomatizes three
+ simple assumptions about a gradual language: compositionality,
+ graduality, and type-based reasoning in the form of $\eta$
+ equivalences.
+\item We prove many theorems in the formal logic of Gradual Type
+ Theory in \secref{sec:theorems-in-gtt}. Chief among these are the
+ uniqueness implementation theorems for casts which show that for
+ each type connective of GTT, the $\eta$ principle for the type
+ ensures that the casts must implement the lazy contract
+ semantics. Furthermore, we show that upcasts are always pure
+ functions and dually that downcasts are always strict functions, as
+ long as the base type casts are pure/strict.
+\item To substantiate that GTT is a reasonable axiomatic theory for
+ gradual typing, we construct \emph{models} of GTT in sections
+ \ref{sec:contract}, \ref{sec:complex} and \ref{sec:lr}. This
+ proceeds in two stages. First (Section \ref{sec:contract}), we use
+ call-by-push-value as a typed metalanguage to construct several
+ models of GTT using different recursive types to implement the
+ dynamic types of GTT and interpret the casts as embedding-projection
+ pairs. This extends standard translations of dynamic typing into
+ static typing using type tags: the dynamic value type is constructed
+ as a recursive sum of basic value types, but dually the dynamic
+ computation type is constructed as a recursive \emph{product} of
+ basic computation types. We observe that this interpretation of the
+ dynamic computation type naturally models stack-based
+ implementations of variable-arity functions as used in the Scheme
+ language.
+\item We then give an operational model of the term dynamism ordering
+ as contextual error approximation in sections \ref{sec:complex} and
+ \ref{sec:lr}. To construct this model, we extend previous work on
+ logical relations for error approximation from call-by-value to
+ call-by-push-value \cite{newahmed18}, simplifying the presentation
+ in the process.
+\end{enumerate}
+
\begin{shortonly}
\textbf{Extended version:} As supplementary materials, we attach an
extended version of the paper, which has omitted cases of definitions,
@@ -919,7 +959,6 @@ lemmas, and proofs.
% mutual refinement) because two greatest elements must each be greater
% than the other and dually for least elements.
-
%% Our proof architecture is as follows:
%% \begin{tikzcd}
%% GTT \arrow[d,"contract insertion"] \\
@@ -7804,7 +7843,7 @@ M : \u B$, $\Gamma' \vdash C[M] : \u B'$ (and similarly for
values/stacks). Using contexts, we can lift any relation on
\emph{results} to relations on open terms, values and stacks.
\begin{definition}[Contextual Lifting]
- Given any relation $\sim \subseteq \text{Result}^2$, we can define
+ Given any relation ${\sim} \subseteq \text{Result}^2$, we can define
its \emph{observational lift} $\ctxize\sim$ to be the typed relation
defined by
\[ \Gamma \pipe \Delta \vDash E \ctxize\sim E' \in T = \forall C : (\Gamma\pipe\Delta \vdash T) \Rightarrow (\cdot \vdash \u F2).~ \result(C[E]) \sim \result(C[E'])\]
@@ -7956,8 +7995,7 @@ We present these graphically (with two more) in Figure
The goal of this section is to prove that a symmetric equality $E \equidyn
E'$ in CBPV (i.e. $E \ltdyn E'$ and $E' \ltdyn E$) implies contextual
equivalence $E \ctxize= E'$ and that inequality in CBPV $E \ltdyn E'$
-implies error approximation $E \ctxize\ltdyn E'$, which will give operational
-graduality\ifshort .\else :\fi
+implies error approximation $E \ctxize\ltdyn E'$, proving graduality of the operational model\ifshort .\else :\fi
\begin{longonly}
\begin{small}
\begin{mathpar}
@@ -7979,7 +8017,9 @@ terms \emph{are} related.
\begin{shortonly}
A preorder $\apreorder$ is only recoverable from its finite
approximations if $\diverge$ is a \emph{least} element, $\diverge
- \apreorder R$, which we call a \emph{divergence preorder}.~
+ \apreorder R$, because a diverging term will cause a time out for
+ any finite index. We call a preorder with $\diverge \apreorder R$ a
+ \emph{divergence preorder}.~
\end{shortonly}
%
\begin{longonly}
@@ -8173,10 +8213,9 @@ to develop logical relations for divergence preorders below.
\begin{shortonly}
We use a logical relation to prove results about $E \ctxize\apreorder
E'$ where $\apreorder$ is a divergence preorder. The
-``finitization'' of divergence preorder is a relation between
+``finitization'' of a divergence preorder is a relation between
\emph{programs} and \emph{results}: a program approximates a result $R$
-at index $i$ if it reduces to $R$ in $< i$ steps or it reduces at
-least $i$ times.
+at index $i$ if it reduces to $R$ in $< i$ steps or it ``times out'' by reducing at least $i$ times.
\end{shortonly}
\begin{longonly}
@@ -8412,7 +8451,7 @@ if they are related at $i$ for each $x:A \in \Gamma$.
The logical preorder for open terms is defined as usual by quantifying
over all related closing substitutions, but also over all stacks to the
-observation type $\u F (1+1)$.
+observation type $\u F (1+1)$:
%% The intuition is that while the contextual preorder defines
%% observation by application of program contexts, the logical preorder
%% defines observation in terms of the ``input-output'' behavior: given
@@ -9173,9 +9212,9 @@ $\precltdyn, \ltdyn\succeq$
typed $S, M$,
\begin{small}
\begin{mathpar}
- \Gamma \vDash S[\err] \ilr \omega \err \in \u B \and
- \Gamma \vDash \err \ilr \omega S[\err] \in \u B\and
- \err \ilrof\precltdyn \omega M\and
+ S[\err] \ilr \omega \err \and
+ \err \ilr \omega S[\err] \and
+ \err \ilrof\precltdyn \omega M \and
M \ilrof{\errordivergerightop} \omega \err
\end{mathpar}
\end{small}
--
GitLab