1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
|
\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}
\[ \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
\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)
\]
%
\begin{gather*}
\Gamma \vdash t : \tau
\;\;\leadsto\;\;
D_1[\Gamma] \vdash \tlet\ \Dc\Gamma[t]\ \tin\ \ttup{\Dp\Gamma[t], \lambda d.\ \Dd{\Gamma_M,\Gamma_A} d[t]} : D_1[\tau] \times (D_2[\tau] \lto \tEVM\ D_2[\Gamma_A]\ (\Tup[D_2[D^M_{\Gamma_M}[t]]])) \\
\DD\Gamma[t] \coloneqq (\Dc\Gamma[t], \Dp\Gamma[t], D^M_{\Gamma_M}[t], \Dd\Gamma d[t])
\end{gather*}
\end{document}
|
