max appendix fix

paper-new/appendix.tex

 \section{Gradual Typing Syntax}
 
-\max{decide if we want to include $\times$ or not}
-
-\begin{align*} % TODO is hole a term?
-  &\text{Types } A := \dyn \alt \nat \alt A \times A \alt (A \ra A') \\
-  &\text{Value Contexts } \Gamma := \cdot \alt (\Gamma, x : A) \\
-  &\text{Terms } M, N := \upc c M \alt \dnc c M
-  &\quad\quad \alt \ret {V} \alt \bind{x}{M}{N} \alt V_f\, V_x \alt \dn{A}{B} M 
-\end{align*}
-
-The type precision derivations $c : A \ltdyn A'$ is inductively defined by
-reflexivity, transitivity, congruence for $\ra$ and $\times$, and generators
-$\textsf{Inj}_\ra : (D \ra D) \ltdyn D$ and $\textsf{Inj}_{\text{nat}}
-: \nat \ltdyn D$.
-%
-We define equivalence of type precision derivations to be inductively generated by congruence for all constructors, category laws for reflexivity and transitivity as well as functoriality laws for $\ra$ and $\times$ congruence
-\[ (c_i \ra c_o)(c_i' \ra c_o) = (c_ic_i') \ra (c_oc_o') \]
-\[ (c_1 \times c_2)(c_1' \times c_2') = (c_1c_1') \times (c_2c_2') \]
-
+\newcommand{\dynof}[1]{\textrm{dyn}(#1)}
 \begin{theorem}
+  For every $A$, there is a derivation $\dynof A : A \ltdyn D$
+\end{theorem}
+\begin{proof}
+  By induction on $A$:
   \begin{enumerate}
-  \item For every $A$, there is a derivation $c : A \ltdyn D$
-  \item Any two derivations $c,c' : A \ltdyn A'$ of the same precision
-    are equivalent.
+  \item $A = \dyn$, then $r(\dyn) : \dyn \ltdyn \dyn$
+  \item $A = \nat$, then $\inat : \nat \ltdyn \dyn$
+  \item $A = A_1 \ra A_2$ then $(\dynof {A_1} \ra \dynof {A_2})\iarr : A_1 \ra A_2 \ltdyn \dyn$ 
+  \item $A = A_1 \times A_2$ then $(\dynof {A_1} \times \dynof{A_2})\itimes : A_1 \times A_2 \ltdyn \dyn$ 
   \end{enumerate}
+\end{proof}
+
+\begin{theorem}
+  For any two derivations $c,c' : A \ltdyn A'$ of the same precision
+  $c \equiv c'$
 \end{theorem}
 \begin{proof}
   \begin{enumerate}
-  \item By induction over $A$.
   \item We show this by showing that derivations have a canonical
     form.
 
     The following presentation of precision derivations has unique derivations
     \begin{mathpar}
-      \inferrule{}{\textrm{refl}(D) : D \ltdyn D}
-      \inferrule{}{\textsf{Inj}_{\text{nat}} : \nat \ltdyn D}
-      \inferrule{}{\textrm{refl}(\nat) : \nat \ltdyn \nat}
-      \inferrule{c : A_i \ra A_o \ltdyn D\ra D}{c(\textsf{Inj}_{\text{arr}}) : A_i \ra A_o \ltdyn \nat}
+      \inferrule{}{\textrm{refl}(D) : D \ltdyn D}\and
+      \inferrule{}{\textsf{Inj}_{\text{nat}} : \nat \ltdyn D}\and
+      \inferrule{}{\textrm{refl}(\nat) : \nat \ltdyn \nat}\and
+      \inferrule{c : A_i \ra A_o \ltdyn D\ra D}{c(\textsf{Inj}_{\text{arr}}) : A_i \ra A_o \ltdyn \nat}\and
       \inferrule{c : A_i \ltdyn A_i' \and d : A_o \ltdyn A_o'}{c \ra d : A_i \ra A_o \ltdyn A_i'\ra A_o'}
       %% \inferrule{A_1 \times A_2 \ltdyn D\times D}{A_1 \times A_2 \ltdyn \nat}
       %% \inferrule{A_1 \ltdyn A_1' \and A_2 \ltdyn A_2'}{A_1 \times A_2 \ltdyn A_1'\times A_2'}
@@ -47,19 +39,6 @@ We define equivalence of type precision derivations to be inductively generated
   \end{enumerate}
 \end{proof}
 
-The gradually typed lambda calculus we consider is call-by-value
-gradual lambda calculus with $\ra$ and $\nat$ as the only base types.
-Casts are generated by the rule
-\begin{mathpar}
-  \inferrule
-  {\Gamma \vdash M : A \and c : A \ltdyn A'}
-  {\Gamma \vdash \upc c M : A'}
-
-  \inferrule
-  {\Gamma \vdash M : A' \and c : A \ltdyn A'}
-  {\Gamma \vdash \dnc c M : A}
-\end{mathpar}
-
 Type precision is a binary relation on typed terms. The original
 gradual guarantee rules are as follows:
 \begin{mathpar}
@@ -80,24 +59,18 @@ gradual guarantee rules are as follows:
 Where the cast $M :: A_2$ is defined to be
 \[ \dnc {dyn(A_2)}{\upc {dyn(A)} M} \]
 
-These two rules are admissible from the following principles:
-%% \begin{mathpar}
-%% \end{mathpar}
+These two rules are admissible in our presentation.
 
 For the first rule, we first prove that $\dnc {dyn(A_2)}\upc {dyn(A)} M = \dnc {c'}\upc{c} M$
 \begin{align*}
   \dnc {dyn(A_2)}\upc {dyn(A)} M
-  &= \dnc {c \,\textrm{dyn}(A')}\upc{c' \,\textrm{dyn}(A')} M \tag{All derivations are equal}\\
-  &= \dnc {c}\dnc {\textrm{dyn}(A')}\upc{\textrm{dyn}(A')}\upc{c'} M\tag{functoriality}\\
+  &= \dnc {(c \dynof {A'})}\upc{(c'\dynof{A'})} M \tag{All derivations are equal}\\
+  &= \dnc {c}\dnc {\dynof{A'}}\upc{\dynof{A'}}\upc{c'} M\tag{functoriality}\\
   &= \dnc {c}\upc{c'} M\tag{retraction}\\
 \end{align*}
 
-Then the rest follows by the up/dn rules above and the fact that precision derivations are all equal.
-\begin{mathpar}
-  \inferrule*
-  {c' = \textrm{dyn}(A_2)\max{todo}}
-  {\dnc {c'}\upc {c} M \ltdyn M' : c'}
-\end{mathpar}
+Then the rest follows by the up/dn rules above and the fact that
+precision derivations are all equal.
 
 Thus the following properties are sufficient to provide an extensional
 model of gradual typing without requiring transitivity of term