cbvgtt.tex

\documentclass{article}

\usepackage{amsmath,amssymb,amsthm}
\usepackage{tikz-cd}
\usepackage{mathpartir}

\newtheorem{theorem}{Theorem}
\newtheorem{corollary}[theorem]{Corollary}
\newtheorem{definition}{Definition}

\newcommand{\type}{\,\,\text{type}}
\newcommand{\ctx}{\,\,\text{ctx}}
\newcommand{\ltdyn}{\sqsubseteq}
\newcommand{\gtdyn}{\sqsupseteq}
\newcommand{\equidyn}{\mathrel{\gtdyn\ltdyn}}
\newcommand{\ltdynv}{\mathrel{\sqsubseteq_V}}
\newcommand{\ltdynt}{\mathrel{\sqsubseteq_T}}

\newcommand{\upcast}[2]{\langle #2 \leftarrowtail #1 \rangle}
\newcommand{\dncast}[2]{\langle #1 \twoheadleftarrow #2 \rangle}

\newcommand{\Set}{\text{Set}}
\newcommand{\relto}{\to}
\newcommand{\M}{\mathcal{M}}
\newcommand{\sq}{\square}
\newcommand{\lett}{\text{let}\,\,}
\newcommand{\ret}{\text{ret}\,\,}

\begin{document}
\title{Call-by-value Gradual Type Theory}
\author{Max S. New, Daniel R. Licata and Amal Ahmed}
\maketitle

\begin{figure}
  \begin{mathpar}
    A \type \and
    \Gamma \ctx\\

    \inferrule
    {A \type \and A' \type}
    {A \ltdynv A'}

    \inferrule
    {A \type \and A' \type}
    {A \ltdynt A'}\\

    \inferrule
    {\Gamma \ctx \and A \type}
    {\Gamma \vdash^v v : A}

    \inferrule
    {\Gamma \ctx \and A \type}
    {\Gamma \vdash^T t : A}\\

    \inferrule
    {\Gamma \ctx\and \Gamma' \ctx}
    {\Phi_v : \Gamma \ltdynv \Gamma'}

    \inferrule
    {\Gamma \ctx\and \Gamma' \ctx}
    {\Phi_t : \Gamma \ltdyn \Gamma'}\\

    \inferrule
    {\Phi_v : \Gamma \ltdyn \Gamma'\and
      \Gamma \vdash^v v : A \and
      \Gamma' \vdash^v v' : A'
    }
    {\Phi_v \vdash^v v \ltdynv v' : A \ltdynv A'}

    \inferrule
    {\Phi : \Gamma \ltdyn \Gamma'\and
      \Gamma \vdash^T t : A \and
      \Gamma' \vdash^T t' : A'
    }
    {\Phi \vdash^T t \ltdyn t' : A \ltdyn A'}
  \end{mathpar}
  \caption{GTTv Judgments and their Pressupositions}
\end{figure}

\begin{figure}
  \begin{mathpar}
    \inferrule{x:A \in \Gamma}
    {\Gamma \vdash^v x : A}

    \inferrule{\gamma : \prod_{x:A \in \Gamma} \Delta \vdash \gamma(x) : A\and
      \Gamma \vdash v : B
    }{\Delta \vdash v[\gamma] : B}

    \inferrule{\gamma : \prod_{x:A \in \Gamma} \Delta \vdash \gamma(x) : A\and
      \Gamma \vdash t : B
    }{\Delta \vdash t[\gamma] : B}

    \inferrule{\Gamma \vdash v : A}
    {\Gamma \vdash \ret v : A}

    \inferrule{\Gamma \vdash t : A\and \Gamma, x : A \vdash u : B}
    {\Gamma \vdash \lett x = t; u : B}

    \lett x = \ret v; t \cong t[v/x]\\
    v[\gamma][\delta] = v[\delta \circ \gamma]\\
    t[\gamma][\delta] = t[\delta \circ \gamma]\
    v[x/x,\ldots] = v\\
    t[x/x,\ldots] = t\\

    \lett x = (\lett y = r; s); t \cong \lett y = r; \lett x = s; t\\
  \end{mathpar}
  \caption{GTTv Judgmental Term, Value Rules}
\end{figure}

\begin{mathpar}
  \inferrule
  {}
  {\Phi, x \ltdyn x' : A \ltdyn A' \vdash \ret x \ltdyn \ret x' : A \ltdyn A'}

  \inferrule
  {\Phi \vdash t \ltdyn t' : A \ltdyn A'\and
    \Phi, x \ltdyn x' : A \ltdyn A' \vdash u \ltdyn u' : C \ltdyn C'}
  {\Phi \vdash \lett x = t; u \ltdyn \lett x' = t'; u' : C \ltdyn C'}
\end{mathpar}

\begin{mathpar}
  \inferrule
  {\Gamma \vdash^v v : A \and A \ltdyn A'}
  {\Gamma \vdash^T \upcast{A}{A'}v : A'}

  \inferrule
  {\Gamma \vdash^v v : A' \and A \ltdyn A'}
  {\Gamma \vdash^T \dncast{A}{A'}v : A}

  \inferrule
  {}
  {x \ltdyn x' : A \ltdyn A' \vdash \upcast{A}{A'}x \ltdyn \ret x' : A'}

  \inferrule
  {}
  {x : A \vdash \ret x \ltdyn \upcast{A}{A'}x : A \ltdyn A'}

  \inferrule
  {}
  {x \ltdyn x' : A \ltdyn A' \vdash \ret x \ltdyn \dncast{A}{A'}x' : A'}

  \inferrule
  {}
  {x' : A' \vdash \dncast{A}{A'}x' \ltdyn x' : A \ltdyn A'}
\end{mathpar}

\begin{mathpar}
  \inferrule{A \type \and B \type}{A \times B \type}

  \inferrule
  {\Gamma \vdash v_1 : A_1 \and \Gamma \vdash v_2 : A_2}
  {\Gamma \vdash^{V} (v_1, v_2) : A_1 \times A_2}

  \inferrule
  {\Gamma \vdash t : A_1 \times A_2\and
    \Gamma, x_1 : A_1, x_2 : A_2 \vdash u : C}
  {\Gamma \vdash \lett (x,x') = t; u : C}
  
  \inferrule
  {}
  {x \ltdyn x' : A \ltdyn A', y \ltdyn y' : B \ltdyn B' \vdash \ret (x,y) \ltdyn \ret (x',y') : A \times B \ltdyn A' \times B'}

  \inferrule
  {\Phi \vdash t \ltdyn t' : A \times B \ltdyn A' \times B'\and
    \Phi, x \ltdyn x' : A \ltdyn A', y \ltdyn y' : B \ltdyn B' \vdash u \ltdyn u' : C \ltdyn C'}
  {\Phi \vdash \lett (x,y) = t; u \ltdyn \lett (x',y') = t'; u' : C \ltdyn C'}

  \inferrule
  {}
  {\Gamma \vdash \lett (x_1,x_2) = (v_1,v_2); t \equidyn t[v_1/x_1,v_2/x_2] : C}

  \inferrule
  {}
  {\Gamma \vdash t \equidyn \lett (x_1,x_2) = t; \ret (x_1,x_2) : A_1 \times A_2}
\end{mathpar}

\begin{theorem}[Product Contract]
  If $A_1 \ltdyn A_1'$ and $A_2 \ltdyn A_2'$ then

  \begin{align*}
  x' : A_1' \times A_2' \vdash
  \dncast{A_1\times A_2}{A_1'\times A_2'}x'
  &\equidyn\\
  \lett (x_1', x_2') = x'; \lett y_1 = \dncast{A_1}{A_1'}x_1'; \lett y_2 = \dncast{A_2}{A_2'}x_2'; \ret (y_1,y_2)&\equidyn\\
  \lett (x_1', x_2') = x'; \lett y_2 = \dncast{A_2}{A_2'}x_2'; \lett y_1 = \dncast{A_1}{A_1'}x_1'; \ret (y_1,y_2)\\
  \end{align*}
\end{theorem}
\begin{proof}
  First, we show the direction that requires $\eta$ expansion.
  \begin{mathpar}
    \inferrule{}
    {
  \dncast{A_1\times A_2}{A_1'\times A_2'}x'
  \ltdyn
  \lett (x_1', x_2') = x'; \lett y_1 = \dncast{A_1}{A_1'}x_1'; \lett y_2 = \dncast{A_2}{A_2'}x_2'; \ret (y_1,y_2)}
  \end{mathpar}

  By the Down-Left rule, it is sufficient to prove that under $x \ltdyn x' : (A_1 \times A_2) \ltdyn (A_1' \times A_2')$,
  \begin{mathpar}
  {x \ltdyn
  \lett (x_1', x_2') = x'; \lett y_1 = \dncast{A_1}{A_1'}x_1'; \lett y_2 = \dncast{A_2}{A_2'}x_2'; \ret (y_1,y_2)}
  \end{mathpar}

  By the $\eta$ rule for products and the let-rule for values, $x :
  A_1 \times A_2$ can be expanded as follows:
  \begin{align*}
  x &\equidyn
  \lett (x_1,x_2) = x; \ret (x_1,x_2)\\
  &\equidyn
  \lett (x_1,x_2) = x; \lett y_1 =\ret x_1; \ret (y_1,x_2)\\
  &\equidyn
  \lett (x_1,x_2) = x; \lett y_1 = \ret x_1; \lett y_2 = \ret x_2; \ret (y_1,y_2)
  \end{align*}

Now that we have the two sides with the same structre, we use the
congruence rules for product pattern matching and we have to use the
Down-Right rule twice:

\begin{mathpar}
  x_1 \ltdyn x_1' : A_1 \ltdyn A_1' \vdash \ret x_1 \ltdyn \dncast{A_1}{A_1'}{x_1'} : A_1
  
  x_2 \ltdyn x_2' : A_2 \ltdyn A_2' \vdash \ret x_2 \ltdyn \dncast{A_2}{A_2'}{x_2'} : A_2
\end{mathpar}

Next, we show the reverse inequality using $\eta$ contraction

  \begin{mathpar}
    {
      \lett (x_1', x_2') = x'; \lett y_1 = \dncast{A_1}{A_1'}x_1'; \lett y_2 = \dncast{A_2}{A_2'}x_2'; \ret (y_1,y_2)\ltdyn \dncast{A_1\times A_2}{A_1'\times A_2'}x' }
  \end{mathpar}

  This time, we need to use congruence \emph{first}, because the
  downcast is on the right, we can't use the Down-Right rule unless
  the left side is already at the less dynamic type.

  So we rewrite the right side as
  \begin{align*}
    \dncast{A_1\times A_2}{A_1'\times A_2'}x'
    &\ltdyn
    \lett (x_1',x_2') = x'; \dncast{A_1\times A_2}{A_1'\times A_2'}(x_1',x_2')\\
    &\ltdyn
    \lett (x_1',x_2') = x'; \lett y_1' = x_1'; \dncast{A_1\times A_2}{A_1'\times A_2'}(x_1',x_2')\\
    &\ltdyn
    \lett (x_1',x_2') = x'; \lett y_1' = x_1'; \lett y_2' = x_2'; \dncast{A_1\times A_2}{A_1'\times A_2'}(x_1',x_2')
  \end{align*}
\end{proof}

Then the proof is again by the congruence rules, using Down-Left twice
and Down-Right once:

\begin{mathpar}
  x_1' : A_1' \vdash \dncast{A_1}{A_1'}x_1' \ltdyn \ret x_1'

  x_2' : A_2' \vdash \dncast{A_2}{A_2'}x_2' \ltdyn \ret x_2'

  x_1 \ltdyn x_1', x_2 \ltdyn x_2' \vdash (x_1,x_2) \ltdyn \dncast{A_1\times A_2}{A_1'\times A_2'}(x_1',x_2')
\end{mathpar}

\begin{corollary}[Projections commute]
 For any $A \ltdyn A', B \ltdyn B'$ and $\Gamma, x:A, y : B \vdash t : C$,
 \[
 \lett x = \dncast{A}{A'}x'; \lett y = \dncast B {B'} y'; t
 \equidyn
 \lett y = \dncast B {B'} y'; \lett x = \dncast{A}{A'}x'; t
 \]
\end{corollary}
\begin{proof}
  By the previous theorem, both are equivalent to
  \[
  \lett z = \dncast{A\times B}{A' \times B'}(x',y');
  \lett (x,y) = z;
  t
  \]
\end{proof}

\end{document}

%% Local Variables:
%% compile-command: "pdflatex main.tex"
%% End: