path: root/rules/rules.tex

\documentclass[11pt,a4paper]{article}
\usepackage[margin=2.5cm]{geometry}
\usepackage[utf8]{inputenc}
\usepackage[T1]{fontenc}
\usepackage[british]{babel}
\usepackage{microtype}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{mathtools}
\usepackage{hyperref}
% \usepackage{parskip}
% \usepackage{graphicx}
% \usepackage{xifthen}
% \usepackage{wasysym}
% \usepackage{verbatim}
% \usepackage{changepage}
\usepackage{xcolor}

% fonts
\usepackage{libertine}
\usepackage[varqu]{zi4}
\usepackage[libertine]{newtxmath}

\let\oldepsilon\epsilon \let\epsilon\varepsilon \let\varepsilon\oldepsilon
\let\oldphi\phi \let\phi\varphi \let\varphi\oldphi
\let\oldemptyset\emptyset \let\emptyset\varnothing \let\varnothing\oldemptyset

\newcommand\coloneqqq{\mathbin{\raisebox{0.04em}{::}\hspace{-0.25em}=}}

\newcommand\multiline[1]{\begin{array}[t]{@{}l@{}} #1 \end{array}}
\newcommand\precomma{\mathllap{,\mkern1mu}}

\newcommand\R{\mathbb R}
\newcommand\Z{\mathbb Z}
\newcommand\tArray{\mathrm{Array}}
\newcommand\tEVM{\mathrm{EVM}}
\newcommand\tUnit{\mathbf{1}}
\newcommand\ttup[1]{\langle #1 \rangle}
\newcommand\tunit{\ttup{}}
\newcommand\tfst{\mathrm{fst}}
\newcommand\tsnd{\mathrm{snd}}
\newcommand\op[1]{\mathit{op}(#1)}
\newcommand\tlet{\mathbf{let}}
\newcommand\tin{\mathbf{in}}
\newcommand\tinl{\mathrm{inl}}
\newcommand\tinr{\mathrm{inr}}
\newcommand\tcase[1]{\mathbf{case}\ #1\ \mathbf{of}}
\newcommand\tdo{\mathbf{do}}
\newcommand\lto{\multimap}
\newcommand\app{\mathbin{{+}\mkern-4mu{+}}}
\newcommand\evm[1]{\underline{\vphantom{\mathbf{b}}\smash{\mathbf{#1}}}}

\newcommand\luplus{\mathbin{\underline{\uplus}}}
\newcommand\linzero{\underline{\mathbf0}}

\newcommand\Dc[1]{D^0_{#1}}
\newcommand\Dp[1]{D^1_{#1}}
\newcommand\Dd[2]{D^2_{#1,#2}}
\newcommand\DD[1]{\bar D_{#1}}

\newcommand\TupBinds{\mathrm{TupBinds}}


\begin{document}

\section*{Original triple CHAD}

\[ \begin{array}{@{}c@{\qquad}c@{}}
  \begin{array}{@{}l@{}}
    \sigma, \tau \coloneqqq
      \tUnit
      \mid \sigma \times \tau
      \mid \sigma \uplus \tau
      \mid \R
      \mid \Z
      \textcolor{gray}{{} \mid \tArray\ \tau} \\
    C \coloneqqq \{ \overline{x = t} \}
  \end{array}
  &
  \begin{array}{@{}l@{\;}r@{\;}l@{}}
    s,t &\coloneqqq& x \mid \tlet\ C\ \tin\ t \\
    &\mid& \tunit \\
    &\mid& \ttup{s, t} \mid \tfst\ t \mid \tsnd\ t \\
    &\mid& \tinl\ t \mid \tinr\ t \mid \tcase{s}\ \{ \ldots \} \\
    &\mid& c \mid \op{t_1,\ldots,t_n} \\
    &\textcolor{gray}{\mid}& \textcolor{gray}{\textit{array stuff}} \\
  \end{array}
\end{array} \]

\begin{gather*}
  D_1[\tUnit] = \tUnit \qquad
  D_1[\sigma \times \tau] = D_1[\sigma] \times D_1[\tau] \qquad
  D_1[\sigma \uplus \tau] = D_1[\sigma] \uplus D_1[\tau] \\
  D_1[\R] = \R \qquad
  D_1[\Z] = \Z \qquad
  D_1[\tArray\ \tau] = \tArray\ D_1[\tau]
  \\[0.5em]
  D_2[\tUnit] = \tUnit \qquad
  D_2[\sigma \times \tau] = D_2[\sigma] \times D_2[\tau] \qquad
  D_2[\sigma \uplus \tau] = D_2[\sigma] \luplus D_2[\tau] \\
  D_2[\R] = \R \qquad
  D_2[\Z] = \tUnit \qquad
  D_2[\tArray\ \tau] = \tArray\ D_2[\tau]
  \\[0.5em]
  \TupBinds[\{x_1 = t_1, \ldots, x_n = t_n\}] = \ttup{x_1, \ttup{x_2, \ldots \ttup{x_{n-1}, x_n}\ldots}}
\end{gather*}

\begin{gather*}
  \Gamma \vdash t : \tau
    \;\;\leadsto\;\; 
    D_1[\Gamma] \vdash \tlet\ \Dc\Gamma[t]\ \tin\ \ttup{\Dp\Gamma[t], \lambda d.\ \Dd\Gamma d[t]} : D_1[\tau] \times (D_2[\tau] \lto \tEVM\ D_2[\Gamma]\ \tUnit) \\
  \DD\Gamma[t] \coloneqq (\Dc\Gamma[t], \Dp\Gamma[t], \Dd\Gamma d[t])
\end{gather*}
%
\begin{align*}
  \DD\Gamma[x : \tau]
    &= (\epsilon, x : D_2[\tau], \evm{one}_{x : D_2[\tau] \in D_2[\Gamma]}\ d)
  \\
  \DD\Gamma[\tlet\ x : \tau = s\ \tin\ t]
    &= (\multiline{
          \Dc\Gamma[s] \app \{x = \Dp\Gamma[t]\} \app \Dc\Gamma[t] \\
          \precomma \Dp\Gamma[t] \\
          \precomma \tdo\ \multiline{
            \ttup{\tunit, \mathit{dx}} \leftarrow \evm{scope}_{D_2[\Gamma],D_2[\tau]}\ (\Dd\Gamma d[t]) \\
            \Dd\Gamma{\mathit{dx}}[s])
       }}
  \\
  \DD\Gamma[\tunit]
    &= (\epsilon, \tunit, \evm{return}\ \tunit)
  \\
  \DD\Gamma[\ttup{s,t}]
    &= (\Dc\Gamma[s] \app \Dc\Gamma[t], \ttup{\Dp\Gamma[s], \Dp\Gamma[t]}, \tlet\ \ttup{d_1,d_2} = d\ \tin\ \tdo\ \Dd\Gamma{d_1}[s]; \Dd\Gamma{d_2}[t])
  \\
  \DD\Gamma[\tfst\ t]
    &= (\Dc\Gamma[t], \tfst\ \Dp\Gamma[t], \Dd\Gamma{\ttup{d, \linzero}}[t])
  \\
  \DD\Gamma[\tinl\ t]
    &= (\Dc\Gamma[t], \tinl\ \Dp\Gamma[t], \Dd\Gamma{(\mathbf{lcastl}\ d)}[t])
  \\
  \DD\Gamma[\multiline{\tcase{s : \sigma \uplus \tau} \\ \quad\mathrlap{\{}\hphantom{\mid {}} \tinl\ x \to t_1 \\ \quad \mid \tinr\ y \to t_2 \}]}
    &= (\multiline{
          \Dc\Gamma[s] \app \{z = \Dp\Gamma[s]\} \app {} \\
          \{\ttup{v, \mathit{tape}} = \multiline{
            \tcase z \\
            \quad \mathrlap{\{}\hphantom{\mid {}} \tinl\ x \to \tlet\ \Dc\Gamma[t_1]\ \tin\ \ttup{\Dp\Gamma[t_1], \tinl\ (\TupBinds[\Dc\Gamma[t_1]])} \\
            \quad \mid \tinr\ y \to \tlet\ \Dc\Gamma[t_2]\ \tin\ \ttup{\Dp\Gamma[t_2], \tinr\ (\TupBinds[\Dc\Gamma[t_2]])} \}\}
          } \\
          \precomma v \\
          \precomma \tdo\ \multiline{
            \mathit{dz'} \leftarrow \multiline{
              \tcase{\mathit{tape}} \\
              \quad \mathrlap{\{}\hphantom{\mid {}} \tinl\ (\TupBinds[\Dc\Gamma[t_1]]) \to \tdo\ \multiline{
                \ttup{\tunit, \mathit{dz}} \leftarrow \evm{scope}_{D_2[\Gamma],D_2[\sigma]}\ (\Dd\Gamma d[t_1]) \\
                \evm{return}\ (\mathbf{linl}\ \mathit{dz})
              } \\
              \quad \mid \tinr\ (\TupBinds[\Dc\Gamma[t_2]]) \to \tdo\ \multiline{
                \ttup{\tunit, \mathit{dz}} \leftarrow \evm{scope}_{D_2[\Gamma],D_2[\tau]}\ (\Dd\Gamma d[t_2]) \\
                \evm{return}\ (\mathbf{linr}\ \mathit{dz}) \}
              }
            } \\
            \Dd\Gamma{dz'}[s])
          }
       }
  \\
  \DD\Gamma[c]
    &= (\epsilon, c, \evm{return}\ \tunit)
  \\
  \DD\Gamma[\op{t_1,\ldots,t_n}]
    &= (\multiline{
          \Dc\Gamma[t_1] \app \cdots \app \Dc\Gamma[t_n] \app \{x_1 = \Dp\Gamma[t_1], \ldots, x_n = \Dp\Gamma[t_n]\} \\
          \precomma \op{x_1, \ldots, x_n} \\
          \precomma \tlet\ \ttup{d_1, \ldots, d_n} = D\mathit{op}^\top(x_1,\ldots,x_n; d)\ \tin\ \tdo\ \Dd\Gamma{d_1}[t_1]; \ldots; \Dd\Gamma{d_n}[t_n])
       }
\end{align*}

\newpage

\section*{With accumulators and selective merge envs}

\newcommand\Tup{\mathrm{Tup}}
\[
  \Tup[x_1 : \tau_1, \ldots, x_n : \tau_n] = \tau_1 \times (\tau_2 \times \cdots (\tau_{n-1} \times \tau_n)\cdots)
\]
%
\renewcommand\DD[2]{\bar D_{#1,#2}}%
\newcommand\Dzero[1]{D^0_{#1}}%
\newcommand\Dsave[1]{D^{0\mathrm{S}}_{#1}}%
\renewcommand\Dp[1]{D^1_{#1}}%
\newcommand\Dmerge[1]{D^M_{#1}}%
\renewcommand\Dd[3]{D^2_{#1,#2,#3}}%
\newcommand\Dac{D_{2\mathrm{Ac}}}%
\begin{gather*}
  \DD{\Gamma_M}{\Gamma_A}\,t = (\Dzero\Gamma\,t, \Dsave\Gamma\,t, \Dp\Gamma\,t, \Dmerge{\Gamma_M}\,t, \Dd{\Gamma_M}{\Gamma_A}{d}\,t) \qquad(\Gamma \coloneqq \Gamma_M \cup \Gamma_A\text{, disjoint}) \\
  \Dac[x_1 : \tau_1, \ldots, x_n : \tau_n] \coloneqq x_1 : \mathrm{Accum}\ \tau_1, \ldots, x_n : \mathrm{Accum}\ \tau_n \\
  \Gamma \vdash t : \tau
    \;\;\leadsto\;\; 
    \left\{ \begin{array}{ll}
      \Dzero\Gamma\,t & \text{list of bindings in $D_1\,\Gamma$} \\
      \Dsave\Gamma\,t & \text{subset of $\Dzero\Gamma\,t$ (``save list'')} \\
      \Dp\Gamma\,t & D_1\,\Gamma, \Dzero\Gamma\,t \vdash \Dp\Gamma\,t : D_1\,\tau \\
      \Dmerge{\Gamma_M}\,t & \text{subset of $\Gamma_M$} \\
      \Dd{\Gamma_M}{\Gamma_A}{d}\,t & \Dac\,\Gamma_A, \Dsave\Gamma\,t, d : D_2\,\tau \vdash \Dd{\Gamma_M}{\Gamma_A}{d} : \Tup[D_2[\Dmerge{\Gamma_M}\,t]]
        \qquad\text{(accumulation effect)}
    \end{array} \right. \\
  \text{Top-level: } D_1\,\Gamma, \Dac\,{\Gamma_A} \vdash \mathbf{let}\ \Dzero\Gamma\,t\ \mathbf{in}\ \ttup{\Dp\Gamma\,t, \lambda d.\ \Dd{\Gamma_M}{\Gamma_A}{d}\,t} : D_1\,\tau \times (D_2\,\tau \lto \Tup[D_2\,\Gamma_M])
\end{gather*}
Accumulation effect:
\begin{gather*}
  \frac{\Gamma \vdash t_1 : D_2\,\tau
        \quad \Gamma, \mathrm{Accum}\ \tau \vdash t_2 : \alpha}
       {\Gamma \vdash \underline{\mathrm{with}}\ t_1\ t_2 : \alpha \times D_2\,\tau}
  \qquad
  \frac{\tau_1 \overset{p}{\rightsquigarrow} \tau_2, \tau_{\mathrm{idx}}
        \quad \Gamma \vdash t_1 : \tau_{\mathrm{idx}}
        \quad \Gamma \vdash t_2 : D_2\,\tau_2
        \quad \Gamma \vdash t_3 : \mathrm{Accum}\ \tau_1}
       {\Gamma \vdash \underline{\mathrm{accum}}_p\ t_1\ t_2\ t_3 : \tUnit}
\end{gather*}


\end{document}