|
1 (*<*) |
|
2 theory Slides3 |
|
3 imports "LaTeXsugar" "Nominal" |
|
4 begin |
|
5 |
|
6 notation (latex output) |
|
7 set ("_") and |
|
8 Cons ("_::/_" [66,65] 65) |
|
9 |
|
10 (*>*) |
|
11 |
|
12 |
|
13 text_raw {* |
|
14 \renewcommand{\slidecaption}{Cambridge, 8.~June 2010} |
|
15 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
16 \mode<presentation>{ |
|
17 \begin{frame}<1>[t] |
|
18 \frametitle{% |
|
19 \begin{tabular}{@ {\hspace{-3mm}}c@ {}} |
|
20 \\ |
|
21 \huge Nominal 2\\[-2mm] |
|
22 \large Or, How to Reason Conveniently with\\[-5mm] |
|
23 \large General Bindings in Isabelle/HOL\\[5mm] |
|
24 \end{tabular}} |
|
25 \begin{center} |
|
26 Christian Urban |
|
27 \end{center} |
|
28 \begin{center} |
|
29 joint work with {\bf Cezary Kaliszyk}\\[0mm] |
|
30 \end{center} |
|
31 \end{frame}} |
|
32 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
33 |
|
34 *} |
|
35 |
|
36 text_raw {* |
|
37 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
38 \mode<presentation>{ |
|
39 \begin{frame}<1-2> |
|
40 \frametitle{\begin{tabular}{c}Binding in Old Nominal\end{tabular}} |
|
41 \mbox{}\\[-6mm] |
|
42 |
|
43 \begin{itemize} |
|
44 \item old Nominal provided a reasoning infrastructure for single binders\medskip |
|
45 |
|
46 \begin{center} |
|
47 Lam [a].(Var a) |
|
48 \end{center}\bigskip |
|
49 |
|
50 \item<2-> but representing |
|
51 |
|
52 \begin{center} |
|
53 $\forall\{a_1,\ldots,a_n\}.\; T$ |
|
54 \end{center}\medskip |
|
55 |
|
56 with single binders and reasoning about it is a \alert{\bf major} pain; |
|
57 take my word for it! |
|
58 \end{itemize} |
|
59 |
|
60 \only<1>{ |
|
61 \begin{textblock}{6}(1.5,11) |
|
62 \small |
|
63 for example\\ |
|
64 \begin{tabular}{l@ {\hspace{2mm}}l} |
|
65 & a $\fresh$ Lam [a]. t\\ |
|
66 & Lam [a]. (Var a) \alert{$=$} Lam [b]. (Var b)\\ |
|
67 & Barendregt style reasoning about bound variables\\ |
|
68 \end{tabular} |
|
69 \end{textblock}} |
|
70 |
|
71 \end{frame}} |
|
72 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
73 *} |
|
74 |
|
75 text_raw {* |
|
76 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
77 \mode<presentation>{ |
|
78 \begin{frame}<1-4> |
|
79 \frametitle{\begin{tabular}{c}Binding Sets of Names\end{tabular}} |
|
80 \mbox{}\\[-3mm] |
|
81 |
|
82 \begin{itemize} |
|
83 \item binding sets of names has some interesting properties:\medskip |
|
84 |
|
85 \begin{center} |
|
86 \begin{tabular}{l} |
|
87 $\forall\{x, y\}.\, x \rightarrow y \;\;\approx_\alpha\;\; \forall\{y, x\}.\, y \rightarrow x$ |
|
88 \bigskip\smallskip\\ |
|
89 |
|
90 \onslide<2->{% |
|
91 $\forall\{x, y\}.\, x \rightarrow y \;\;\not\approx_\alpha\;\; \forall\{z\}.\, z \rightarrow z$ |
|
92 }\bigskip\smallskip\\ |
|
93 |
|
94 \onslide<3->{% |
|
95 $\forall\{x\}.\, x \rightarrow y \;\;\approx_\alpha\;\; \forall\{x, \alert{z}\}.\, x \rightarrow y$ |
|
96 }\medskip\\ |
|
97 \onslide<3->{\hspace{4cm}\small provided $z$ is fresh for the type} |
|
98 \end{tabular} |
|
99 \end{center} |
|
100 \end{itemize} |
|
101 |
|
102 \begin{textblock}{8}(2,14.5) |
|
103 \footnotesize $^*$ $x$, $y$, $z$ are assumed to be distinct |
|
104 \end{textblock} |
|
105 |
|
106 \only<4>{ |
|
107 \begin{textblock}{6}(2.5,4) |
|
108 \begin{tikzpicture} |
|
109 \draw (0,0) node[inner sep=3mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] |
|
110 {\normalsize\color{darkgray} |
|
111 \begin{minipage}{8cm}\raggedright |
|
112 For type-schemes the order of bound names does not matter, and |
|
113 alpha-equivalence is preserved under \alert{vacuous} binders. |
|
114 \end{minipage}}; |
|
115 \end{tikzpicture} |
|
116 \end{textblock}} |
|
117 \end{frame}} |
|
118 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
119 *} |
|
120 |
|
121 text_raw {* |
|
122 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
123 \mode<presentation>{ |
|
124 \begin{frame}<1-3> |
|
125 \frametitle{\begin{tabular}{c}Other Binding Modes\end{tabular}} |
|
126 \mbox{}\\[-3mm] |
|
127 |
|
128 \begin{itemize} |
|
129 \item alpha-equivalence being preserved under vacuous binders is \underline{not} always |
|
130 wanted:\bigskip\bigskip\normalsize |
|
131 |
|
132 \begin{tabular}{@ {\hspace{-8mm}}l} |
|
133 $\text{let}\;x = 3\;\text{and}\;y = 2\;\text{in}\;x - y\;\text{end}$\medskip\\ |
|
134 \onslide<2->{$\;\;\;\only<2>{\approx_\alpha}\only<3>{\alert{\not\approx_\alpha}} |
|
135 \text{let}\;y = 2\;\text{and}\;x = 3\only<3->{\alert{\;\text{and} |
|
136 \;z = \text{loop}}}\;\text{in}\;x - y\;\text{end}$} |
|
137 \end{tabular} |
|
138 |
|
139 |
|
140 \end{itemize} |
|
141 |
|
142 \end{frame}} |
|
143 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
144 *} |
|
145 |
|
146 text_raw {* |
|
147 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
148 \mode<presentation>{ |
|
149 \begin{frame}<1> |
|
150 \frametitle{\begin{tabular}{c}\LARGE{}Even Another Binding Mode\end{tabular}} |
|
151 \mbox{}\\[-3mm] |
|
152 |
|
153 \begin{itemize} |
|
154 \item sometimes one wants to abstract more than one name, but the order \underline{does} matter\bigskip |
|
155 |
|
156 \begin{center} |
|
157 \begin{tabular}{@ {\hspace{-8mm}}l} |
|
158 $\text{let}\;(x, y) = (3, 2)\;\text{in}\;x - y\;\text{end}$\medskip\\ |
|
159 $\;\;\;\not\approx_\alpha |
|
160 \text{let}\;(y, x) = (3, 2)\;\text{in}\;x - y\;\text{end}$ |
|
161 \end{tabular} |
|
162 \end{center} |
|
163 |
|
164 |
|
165 \end{itemize} |
|
166 |
|
167 \end{frame}} |
|
168 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
169 *} |
|
170 |
|
171 text_raw {* |
|
172 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
173 \mode<presentation>{ |
|
174 \begin{frame}<1-2> |
|
175 \frametitle{\begin{tabular}{c}\LARGE{}Three Binding Modes\end{tabular}} |
|
176 \mbox{}\\[-3mm] |
|
177 |
|
178 \begin{itemize} |
|
179 \item the order does not matter and alpha-equivelence is preserved under |
|
180 vacuous binders \textcolor{gray}{(restriction)}\medskip |
|
181 |
|
182 \item the order does not matter, but the cardinality of the binders |
|
183 must be the same \textcolor{gray}{(abstraction)}\medskip |
|
184 |
|
185 \item the order does matter |
|
186 \end{itemize} |
|
187 |
|
188 \onslide<2->{ |
|
189 \begin{center} |
|
190 \isacommand{bind\_res}\hspace{6mm} |
|
191 \isacommand{bind\_set}\hspace{6mm} |
|
192 \isacommand{bind} |
|
193 \end{center}} |
|
194 |
|
195 \end{frame}} |
|
196 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
197 *} |
|
198 |
|
199 text_raw {* |
|
200 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
201 \mode<presentation>{ |
|
202 \begin{frame}<1-3> |
|
203 \frametitle{\begin{tabular}{c}Specification of Binding\end{tabular}} |
|
204 \mbox{}\\[-6mm] |
|
205 |
|
206 \mbox{}\hspace{10mm} |
|
207 \begin{tabular}{ll} |
|
208 \multicolumn{2}{l}{\isacommand{nominal\_datatype} trm $=$}\\ |
|
209 \hspace{5mm}\phantom{$|$} Var name\\ |
|
210 \hspace{5mm}$|$ App trm trm\\ |
|
211 \hspace{5mm}$|$ Lam \only<2->{x::}name \only<2->{t::}trm |
|
212 & \onslide<2->{\isacommand{bind} x \isacommand{in} t}\\ |
|
213 \hspace{5mm}$|$ Let \only<2->{as::}assn \only<2->{t::}trm |
|
214 & \onslide<2->{\isacommand{bind} bn(as) \isacommand{in} t}\\ |
|
215 \multicolumn{2}{l}{\isacommand{and} assn $=$}\\ |
|
216 \multicolumn{2}{l}{\hspace{5mm}\phantom{$|$} ANil}\\ |
|
217 \multicolumn{2}{l}{\hspace{5mm}$|$ ACons name trm assn}\\ |
|
218 \multicolumn{2}{l}{\onslide<3->{\isacommand{binder} bn \isacommand{where}}}\\ |
|
219 \multicolumn{2}{l}{\onslide<3->{\hspace{5mm}\phantom{$|$} bn(ANil) $=$ []}}\\ |
|
220 \multicolumn{2}{l}{\onslide<3->{\hspace{5mm}$|$ bn(ACons a t as) $=$ [a] @ bn(as)}}\\ |
|
221 \end{tabular} |
|
222 |
|
223 |
|
224 |
|
225 \end{frame}} |
|
226 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
227 *} |
|
228 |
|
229 text_raw {* |
|
230 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
231 \mode<presentation>{ |
|
232 \begin{frame}<1-5> |
|
233 \frametitle{\begin{tabular}{c}Inspiration from Ott\end{tabular}} |
|
234 \mbox{}\\[-3mm] |
|
235 |
|
236 \begin{itemize} |
|
237 \item this way of specifying binding is inspired by |
|
238 Ott\onslide<2->{, \alert{\bf but} we made adjustments:}\medskip |
|
239 |
|
240 |
|
241 \only<2>{ |
|
242 \begin{itemize} |
|
243 \item Ott allows specifications like\smallskip |
|
244 \begin{center} |
|
245 $t ::= t\;t\; |\;\lambda x.t$ |
|
246 \end{center} |
|
247 \end{itemize}} |
|
248 |
|
249 \only<3-4>{ |
|
250 \begin{itemize} |
|
251 \item whether something is bound can depend in Ott on other bound things\smallskip |
|
252 \begin{center} |
|
253 \begin{tikzpicture} |
|
254 \node (A) at (-0.5,1) {Foo $(\lambda y. \lambda x. t)$}; |
|
255 \node (B) at ( 1.1,1) {$s$}; |
|
256 \onslide<4>{\node (C) at (0.5,0) {$\{y, x\}$};} |
|
257 \onslide<4>{\draw[->,red,line width=1mm] (A) -- (C);} |
|
258 \onslide<4>{\draw[->,red,line width=1mm] (C) -- (B);} |
|
259 \end{tikzpicture} |
|
260 \end{center} |
|
261 \onslide<4>{this might make sense for ``raw'' terms, but not at all |
|
262 for $\alpha$-equated terms} |
|
263 \end{itemize}} |
|
264 |
|
265 \only<5>{ |
|
266 \begin{itemize} |
|
267 \item we allow multiple binders and bodies\smallskip |
|
268 \begin{center} |
|
269 \isacommand{bind} a b c \isacommand{in} x y z |
|
270 \end{center}\bigskip\medskip |
|
271 the reason is that in general |
|
272 \begin{center} |
|
273 \begin{tabular}{rcl} |
|
274 \isacommand{bind\_res} as \isacommand{in} x y & $\not\Leftrightarrow$ & |
|
275 \begin{tabular}{@ {}l} |
|
276 \isacommand{bind\_res} as \isacommand{in} x,\\ |
|
277 \isacommand{bind\_res} as \isacommand{in} y |
|
278 \end{tabular} |
|
279 \end{tabular} |
|
280 \end{center}\smallskip |
|
281 |
|
282 same with \isacommand{bind\_set} |
|
283 \end{itemize}} |
|
284 \end{itemize} |
|
285 |
|
286 |
|
287 \end{frame}} |
|
288 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
289 *} |
|
290 |
|
291 text_raw {* |
|
292 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
293 \mode<presentation>{ |
|
294 \begin{frame}<1> |
|
295 \frametitle{\begin{tabular}{c}Alpha-Equivalence\end{tabular}} |
|
296 \mbox{}\\[-3mm] |
|
297 |
|
298 \begin{itemize} |
|
299 \item in old Nominal, we represented single binders as partial functions:\bigskip |
|
300 |
|
301 \begin{center} |
|
302 \begin{tabular}{l} |
|
303 Lam [$a$].\,$t$ $\;{^\text{``}}\!\dn{}\!^{\text{''}}$\\[2mm] |
|
304 \;\;\;\;$\lambda b.$\;$\text{if}\;a = b\;\text{then}\;t\;\text{else}$\\ |
|
305 \phantom{\;\;\;\;$\lambda b.$\;\;\;\;\;\;}$\text{if}\;b \fresh t\; |
|
306 \text{then}\;(a\;b)\act t\;\text{else}\;\text{error}$ |
|
307 \end{tabular} |
|
308 \end{center} |
|
309 \end{itemize} |
|
310 |
|
311 \begin{textblock}{10}(2,14) |
|
312 \footnotesize $^*$ alpha-equality coincides with equality on functions |
|
313 \end{textblock} |
|
314 \end{frame}} |
|
315 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
316 *} |
|
317 |
|
318 text_raw {* |
|
319 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
320 \mode<presentation>{ |
|
321 \begin{frame}<1-> |
|
322 \frametitle{\begin{tabular}{c}New Design\end{tabular}} |
|
323 \mbox{}\\[4mm] |
|
324 |
|
325 \begin{center} |
|
326 \begin{tikzpicture} |
|
327 \alt<2> |
|
328 {\draw (0,0) node[inner sep=3mm, ultra thick, draw=red, rounded corners=2mm] |
|
329 (A) {\textcolor{red}{\begin{minipage}{1.1cm}bind.\\spec.\end{minipage}}};} |
|
330 {\draw (0,0) node[inner sep=3mm, ultra thick, draw=white, rounded corners=2mm] |
|
331 (A) {\begin{minipage}{1.1cm}bind.\\spec.\end{minipage}};} |
|
332 |
|
333 \alt<3> |
|
334 {\draw (3,0) node[inner sep=3mm, ultra thick, draw=red, rounded corners=2mm] |
|
335 (B) {\textcolor{red}{\begin{minipage}{1.1cm}raw\\terms\end{minipage}}};} |
|
336 {\draw (3,0) node[inner sep=3mm, ultra thick, draw=white, rounded corners=2mm] |
|
337 (B) {\begin{minipage}{1.1cm}raw\\terms\end{minipage}};} |
|
338 |
|
339 \alt<4> |
|
340 {\draw (6,0) node[inner sep=3mm, ultra thick, draw=red, rounded corners=2mm] |
|
341 (C) {\textcolor{red}{\begin{minipage}{1.1cm}$\alpha$-\\equiv.\end{minipage}}};} |
|
342 {\draw (6,0) node[inner sep=3mm, ultra thick, draw=white, rounded corners=2mm] |
|
343 (C) {\begin{minipage}{1.1cm}$\alpha$-\\equiv.\end{minipage}};} |
|
344 |
|
345 \alt<5> |
|
346 {\draw (0,-3) node[inner sep=3mm, ultra thick, draw=red, rounded corners=2mm] |
|
347 (D) {\textcolor{red}{\begin{minipage}{1.1cm}quot.\\type\end{minipage}}};} |
|
348 {\draw (0,-3) node[inner sep=3mm, ultra thick, draw=white, rounded corners=2mm] |
|
349 (D) {\begin{minipage}{1.1cm}quot.\\type\end{minipage}};} |
|
350 |
|
351 \alt<6> |
|
352 {\draw (3,-3) node[inner sep=3mm, ultra thick, draw=red, rounded corners=2mm] |
|
353 (E) {\textcolor{red}{\begin{minipage}{1.1cm}lift\\thms\end{minipage}}};} |
|
354 {\draw (3,-3) node[inner sep=3mm, ultra thick, draw=white, rounded corners=2mm] |
|
355 (E) {\begin{minipage}{1.1cm}lift\\thms\end{minipage}};} |
|
356 |
|
357 \alt<7> |
|
358 {\draw (6,-3) node[inner sep=3mm, ultra thick, draw=red, rounded corners=2mm] |
|
359 (F) {\textcolor{red}{\begin{minipage}{1.1cm}add.\\thms\end{minipage}}};} |
|
360 {\draw (6,-3) node[inner sep=3mm, ultra thick, draw=white, rounded corners=2mm] |
|
361 (F) {\begin{minipage}{1.1cm}add.\\thms\end{minipage}};} |
|
362 |
|
363 \draw[->,white!50,line width=1mm] (A) -- (B); |
|
364 \draw[->,white!50,line width=1mm] (B) -- (C); |
|
365 \draw[->,white!50,line width=1mm, line join=round, rounded corners=2mm] |
|
366 (C) -- (8,0) -- (8,-1.5) -- (-2,-1.5) -- (-2,-3) -- (D); |
|
367 \draw[->,white!50,line width=1mm] (D) -- (E); |
|
368 \draw[->,white!50,line width=1mm] (E) -- (F); |
|
369 \end{tikzpicture} |
|
370 \end{center} |
|
371 |
|
372 \end{frame}} |
|
373 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
374 *} |
|
375 |
|
376 |
|
377 |
|
378 text_raw {* |
|
379 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
380 \mode<presentation>{ |
|
381 \begin{frame}<1-9> |
|
382 \frametitle{\begin{tabular}{c}Alpha-Equivalence\end{tabular}} |
|
383 \mbox{}\\[-3mm] |
|
384 |
|
385 \begin{itemize} |
|
386 \item lets first look at pairs\bigskip\medskip |
|
387 |
|
388 \begin{tabular}{@ {\hspace{1cm}}l} |
|
389 $(as, x) \onslide<2->{\approx\!}\makebox[0mm][l]{\only<2-7>{${}_{\text{set}}$}% |
|
390 \only<8>{${}_{\text{\alert{list}}}$}% |
|
391 \only<9>{${}_{\text{\alert{res}}}$}}% |
|
392 \onslide<3->{^{R,\text{fv}}}\,\onslide<2->{(bs,y)}$ |
|
393 \end{tabular}\bigskip |
|
394 \end{itemize} |
|
395 |
|
396 \only<1>{ |
|
397 \begin{textblock}{8}(3,8.5) |
|
398 \begin{tabular}{l@ {\hspace{2mm}}p{8cm}} |
|
399 & $as$ is a set of atoms\ldots the binders\\ |
|
400 & $x$ is the body\\ |
|
401 & $\approx_{\text{set}}$ is where the cardinality |
|
402 of the binders has to be the same\\ |
|
403 \end{tabular} |
|
404 \end{textblock}} |
|
405 |
|
406 \only<4->{ |
|
407 \begin{textblock}{12}(5,8) |
|
408 \begin{tabular}{ll@ {\hspace{1mm}}l} |
|
409 $\dn$ & \onslide<5->{$\exists \pi.\,$} & $\text{fv}(x) - as = \text{fv}(y) - bs$\\[1mm] |
|
410 & \onslide<5->{$\;\;\;\wedge$} & \onslide<5->{$\text{fv}(x) - as \fresh^* \pi$}\\[1mm] |
|
411 & \onslide<6->{$\;\;\;\wedge$} & \onslide<6->{$(\pi \act x)\;R\;y$}\\[1mm] |
|
412 & \onslide<7-8>{$\;\;\;\wedge$} & \onslide<7-8>{$\pi \act as = bs$}\\ |
|
413 \end{tabular} |
|
414 \end{textblock}} |
|
415 |
|
416 \only<8>{ |
|
417 \begin{textblock}{8}(3,13.8) |
|
418 \footnotesize $^*$ $as$ and $bs$ are \alert{lists} of atoms |
|
419 \end{textblock}} |
|
420 \end{frame}} |
|
421 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
422 *} |
|
423 |
|
424 text_raw {* |
|
425 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
426 \mode<presentation>{ |
|
427 \begin{frame}<1-2> |
|
428 \frametitle{\begin{tabular}{c}Examples\end{tabular}} |
|
429 \mbox{}\\[-3mm] |
|
430 |
|
431 \begin{itemize} |
|
432 \item lets look at ``type-schemes'':\medskip\medskip |
|
433 |
|
434 \begin{center} |
|
435 $(as, x) \approx\!\makebox[0mm][l]{${}_{\text{set}}$}\only<1>{{}^{R,\text{fv}}}\only<2->{{}^{\alert{=},\alert{\text{fv}}}} (bs, y)$ |
|
436 \end{center}\medskip |
|
437 |
|
438 \onslide<2->{ |
|
439 \begin{center} |
|
440 \begin{tabular}{l} |
|
441 $\text{fv}(x) = \{x\}$\\[1mm] |
|
442 $\text{fv}(T_1 \rightarrow T_2) = \text{fv}(T_1) \cup \text{fv}(T_2)$\\ |
|
443 \end{tabular} |
|
444 \end{center}} |
|
445 \end{itemize} |
|
446 |
|
447 |
|
448 \only<2->{ |
|
449 \begin{textblock}{4}(0.3,12) |
|
450 \begin{tikzpicture} |
|
451 \draw (0,0) node[inner sep=1mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] |
|
452 {\tiny\color{darkgray} |
|
453 \begin{minipage}{3.4cm}\raggedright |
|
454 \begin{tabular}{r@ {\hspace{1mm}}l} |
|
455 \multicolumn{2}{@ {}l}{res:}\\ |
|
456 $\exists\pi.$ & $\text{fv}(x) - as = \text{fv}(y) - bs$\\ |
|
457 $\wedge$ & $\text{fv}(x) - as \fresh^* \pi$\\ |
|
458 $\wedge$ & $\pi \cdot x = y$\\ |
|
459 \\ |
|
460 \end{tabular} |
|
461 \end{minipage}}; |
|
462 \end{tikzpicture} |
|
463 \end{textblock}} |
|
464 \only<2->{ |
|
465 \begin{textblock}{4}(5.2,12) |
|
466 \begin{tikzpicture} |
|
467 \draw (0,0) node[inner sep=1mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] |
|
468 {\tiny\color{darkgray} |
|
469 \begin{minipage}{3.4cm}\raggedright |
|
470 \begin{tabular}{r@ {\hspace{1mm}}l} |
|
471 \multicolumn{2}{@ {}l}{set:}\\ |
|
472 $\exists\pi.$ & $\text{fv}(x) - as = \text{fv}(y) - bs$\\ |
|
473 $\wedge$ & $\text{fv}(x) - as \fresh^* \pi$\\ |
|
474 $\wedge$ & $\pi \cdot x = y$\\ |
|
475 $\wedge$ & $\pi \cdot as = bs$\\ |
|
476 \end{tabular} |
|
477 \end{minipage}}; |
|
478 \end{tikzpicture} |
|
479 \end{textblock}} |
|
480 \only<2->{ |
|
481 \begin{textblock}{4}(10.2,12) |
|
482 \begin{tikzpicture} |
|
483 \draw (0,0) node[inner sep=1mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] |
|
484 {\tiny\color{darkgray} |
|
485 \begin{minipage}{3.4cm}\raggedright |
|
486 \begin{tabular}{r@ {\hspace{1mm}}l} |
|
487 \multicolumn{2}{@ {}l}{list:}\\ |
|
488 $\exists\pi.$ & $\text{fv}(x) - as = \text{fv}(y) - bs$\\ |
|
489 $\wedge$ & $\text{fv}(x) - as \fresh^* \pi$\\ |
|
490 $\wedge$ & $\pi \cdot x = y$\\ |
|
491 $\wedge$ & $\pi \cdot as = bs$\\ |
|
492 \end{tabular} |
|
493 \end{minipage}}; |
|
494 \end{tikzpicture} |
|
495 \end{textblock}} |
|
496 |
|
497 \end{frame}} |
|
498 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
499 *} |
|
500 |
|
501 text_raw {* |
|
502 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
503 \mode<presentation>{ |
|
504 \begin{frame}<1-2> |
|
505 \frametitle{\begin{tabular}{c}Examples\end{tabular}} |
|
506 \mbox{}\\[-3mm] |
|
507 |
|
508 \begin{center} |
|
509 \only<1>{$(\{x, y\}, x \rightarrow y) \approx_? (\{x, y\}, y \rightarrow x)$} |
|
510 \only<2>{$([x, y], x \rightarrow y) \approx_? ([x, y], y \rightarrow x)$} |
|
511 \end{center} |
|
512 |
|
513 \begin{itemize} |
|
514 \item $\approx_{\text{res}}$, $\approx_{\text{set}}$% |
|
515 \only<2>{, \alert{$\not\approx_{\text{list}}$}} |
|
516 \end{itemize} |
|
517 |
|
518 |
|
519 \only<1->{ |
|
520 \begin{textblock}{4}(0.3,12) |
|
521 \begin{tikzpicture} |
|
522 \draw (0,0) node[inner sep=1mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] |
|
523 {\tiny\color{darkgray} |
|
524 \begin{minipage}{3.4cm}\raggedright |
|
525 \begin{tabular}{r@ {\hspace{1mm}}l} |
|
526 \multicolumn{2}{@ {}l}{res:}\\ |
|
527 $\exists\pi.$ & $\text{fv}(x) - as = \text{fv}(y) - bs$\\ |
|
528 $\wedge$ & $\text{fv}(x) - as \fresh^* \pi$\\ |
|
529 $\wedge$ & $\pi \cdot x = y$\\ |
|
530 \\ |
|
531 \end{tabular} |
|
532 \end{minipage}}; |
|
533 \end{tikzpicture} |
|
534 \end{textblock}} |
|
535 \only<1->{ |
|
536 \begin{textblock}{4}(5.2,12) |
|
537 \begin{tikzpicture} |
|
538 \draw (0,0) node[inner sep=1mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] |
|
539 {\tiny\color{darkgray} |
|
540 \begin{minipage}{3.4cm}\raggedright |
|
541 \begin{tabular}{r@ {\hspace{1mm}}l} |
|
542 \multicolumn{2}{@ {}l}{set:}\\ |
|
543 $\exists\pi.$ & $\text{fv}(x) - as = \text{fv}(y) - bs$\\ |
|
544 $\wedge$ & $\text{fv}(x) - as \fresh^* \pi$\\ |
|
545 $\wedge$ & $\pi \cdot x = y$\\ |
|
546 $\wedge$ & $\pi \cdot as = bs$\\ |
|
547 \end{tabular} |
|
548 \end{minipage}}; |
|
549 \end{tikzpicture} |
|
550 \end{textblock}} |
|
551 \only<1->{ |
|
552 \begin{textblock}{4}(10.2,12) |
|
553 \begin{tikzpicture} |
|
554 \draw (0,0) node[inner sep=1mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] |
|
555 {\tiny\color{darkgray} |
|
556 \begin{minipage}{3.4cm}\raggedright |
|
557 \begin{tabular}{r@ {\hspace{1mm}}l} |
|
558 \multicolumn{2}{@ {}l}{list:}\\ |
|
559 $\exists\pi.$ & $\text{fv}(x) - as = \text{fv}(y) - bs$\\ |
|
560 $\wedge$ & $\text{fv}(x) - as \fresh^* \pi$\\ |
|
561 $\wedge$ & $\pi \cdot x = y$\\ |
|
562 $\wedge$ & $\pi \cdot as = bs$\\ |
|
563 \end{tabular} |
|
564 \end{minipage}}; |
|
565 \end{tikzpicture} |
|
566 \end{textblock}} |
|
567 |
|
568 \end{frame}} |
|
569 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
570 *} |
|
571 |
|
572 text_raw {* |
|
573 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
574 \mode<presentation>{ |
|
575 \begin{frame}<1> |
|
576 \frametitle{\begin{tabular}{c}Examples\end{tabular}} |
|
577 \mbox{}\\[-3mm] |
|
578 |
|
579 \begin{center} |
|
580 \only<1>{$(\{x\}, x) \approx_? (\{x, y\}, x)$} |
|
581 \end{center} |
|
582 |
|
583 \begin{itemize} |
|
584 \item $\approx_{\text{res}}$, $\not\approx_{\text{set}}$, |
|
585 $\not\approx_{\text{list}}$ |
|
586 \end{itemize} |
|
587 |
|
588 |
|
589 \only<1->{ |
|
590 \begin{textblock}{4}(0.3,12) |
|
591 \begin{tikzpicture} |
|
592 \draw (0,0) node[inner sep=1mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] |
|
593 {\tiny\color{darkgray} |
|
594 \begin{minipage}{3.4cm}\raggedright |
|
595 \begin{tabular}{r@ {\hspace{1mm}}l} |
|
596 \multicolumn{2}{@ {}l}{res:}\\ |
|
597 $\exists\pi.$ & $\text{fv}(x) - as = \text{fv}(y) - bs$\\ |
|
598 $\wedge$ & $\text{fv}(x) - as \fresh^* \pi$\\ |
|
599 $\wedge$ & $\pi \cdot x = y$\\ |
|
600 \\ |
|
601 \end{tabular} |
|
602 \end{minipage}}; |
|
603 \end{tikzpicture} |
|
604 \end{textblock}} |
|
605 \only<1->{ |
|
606 \begin{textblock}{4}(5.2,12) |
|
607 \begin{tikzpicture} |
|
608 \draw (0,0) node[inner sep=1mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] |
|
609 {\tiny\color{darkgray} |
|
610 \begin{minipage}{3.4cm}\raggedright |
|
611 \begin{tabular}{r@ {\hspace{1mm}}l} |
|
612 \multicolumn{2}{@ {}l}{set:}\\ |
|
613 $\exists\pi.$ & $\text{fv}(x) - as = \text{fv}(y) - bs$\\ |
|
614 $\wedge$ & $\text{fv}(x) - as \fresh^* \pi$\\ |
|
615 $\wedge$ & $\pi \cdot x = y$\\ |
|
616 $\wedge$ & $\pi \cdot as = bs$\\ |
|
617 \end{tabular} |
|
618 \end{minipage}}; |
|
619 \end{tikzpicture} |
|
620 \end{textblock}} |
|
621 \only<1->{ |
|
622 \begin{textblock}{4}(10.2,12) |
|
623 \begin{tikzpicture} |
|
624 \draw (0,0) node[inner sep=1mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] |
|
625 {\tiny\color{darkgray} |
|
626 \begin{minipage}{3.4cm}\raggedright |
|
627 \begin{tabular}{r@ {\hspace{1mm}}l} |
|
628 \multicolumn{2}{@ {}l}{list:}\\ |
|
629 $\exists\pi.$ & $\text{fv}(x) - as = \text{fv}(y) - bs$\\ |
|
630 $\wedge$ & $\text{fv}(x) - as \fresh^* \pi$\\ |
|
631 $\wedge$ & $\pi \cdot x = y$\\ |
|
632 $\wedge$ & $\pi \cdot as = bs$\\ |
|
633 \end{tabular} |
|
634 \end{minipage}}; |
|
635 \end{tikzpicture} |
|
636 \end{textblock}} |
|
637 |
|
638 \end{frame}} |
|
639 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
640 *} |
|
641 |
|
642 text_raw {* |
|
643 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
644 \mode<presentation>{ |
|
645 \begin{frame}<1-3> |
|
646 \frametitle{\begin{tabular}{c}General Abstractions\end{tabular}} |
|
647 \mbox{}\\[-7mm] |
|
648 |
|
649 \begin{itemize} |
|
650 \item we take $(as, x) \approx\!\makebox[0mm][l]{${}_{\star}$}^{=,\text{supp}} (bs, y)$\medskip |
|
651 \item they are equivalence relations\medskip |
|
652 \item we can therefore use the quotient package to introduce the |
|
653 types $\beta\;\text{abs}_\star$\bigskip |
|
654 \begin{center} |
|
655 \only<1>{$[as].\,x$} |
|
656 \only<2>{$\text{supp}([as].x) = \text{supp}(x) - as$} |
|
657 \only<3>{% |
|
658 \begin{tabular}{r@ {\hspace{1mm}}l} |
|
659 \multicolumn{2}{@ {\hspace{-7mm}}l}{$[as]. x \alert{=} [bs].y\;\;\;\text{if\!f}$}\\[2mm] |
|
660 $\exists \pi.$ & $\text{supp}(x) - as = \text{supp}(y) - bs$\\ |
|
661 $\wedge$ & $\text{supp}(x) - as \fresh^* \pi$\\ |
|
662 $\wedge$ & $\pi \act x = y $\\ |
|
663 $(\wedge$ & $\pi \act as = bs)\;^\star$\\ |
|
664 \end{tabular}} |
|
665 \end{center} |
|
666 \end{itemize} |
|
667 |
|
668 |
|
669 \end{frame}} |
|
670 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
671 *} |
|
672 |
|
673 text_raw {* |
|
674 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
675 \mode<presentation>{ |
|
676 \begin{frame}<1> |
|
677 \frametitle{\begin{tabular}{c}One Problem\end{tabular}} |
|
678 \mbox{}\\[-3mm] |
|
679 |
|
680 \begin{center} |
|
681 $\text{let}\;x_1=t_1 \ldots x_n=t_n\;\text{in}\;s$ |
|
682 \end{center} |
|
683 |
|
684 \begin{itemize} |
|
685 \item we cannot represent this as\medskip |
|
686 \begin{center} |
|
687 $\text{let}\;[x_1,\ldots,x_n]\alert{.}s\;\;[t_1,\ldots,t_n]$ |
|
688 \end{center}\bigskip |
|
689 |
|
690 because\medskip |
|
691 \begin{center} |
|
692 $\text{let}\;[x].s\;\;[t_1,t_2]$ |
|
693 \end{center} |
|
694 \end{itemize} |
|
695 |
|
696 |
|
697 \end{frame}} |
|
698 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
699 *} |
|
700 |
|
701 text_raw {* |
|
702 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
703 \mode<presentation>{ |
|
704 \begin{frame}<1-> |
|
705 \frametitle{\begin{tabular}{c}Our Specifications\end{tabular}} |
|
706 \mbox{}\\[-6mm] |
|
707 |
|
708 \mbox{}\hspace{10mm} |
|
709 \begin{tabular}{ll} |
|
710 \multicolumn{2}{l}{\isacommand{nominal\_datatype} trm $=$}\\ |
|
711 \hspace{5mm}\phantom{$|$} Var name\\ |
|
712 \hspace{5mm}$|$ App trm trm\\ |
|
713 \hspace{5mm}$|$ Lam x::name t::trm |
|
714 & \isacommand{bind} x \isacommand{in} t\\ |
|
715 \hspace{5mm}$|$ Let as::assn t::trm |
|
716 & \isacommand{bind} bn(as) \isacommand{in} t\\ |
|
717 \multicolumn{2}{l}{\isacommand{and} assn $=$}\\ |
|
718 \multicolumn{2}{l}{\hspace{5mm}\phantom{$|$} ANil}\\ |
|
719 \multicolumn{2}{l}{\hspace{5mm}$|$ ACons name trm assn}\\ |
|
720 \multicolumn{2}{l}{\isacommand{binder} bn \isacommand{where}}\\ |
|
721 \multicolumn{2}{l}{\hspace{5mm}\phantom{$|$} bn(ANil) $=$ $[]$}\\ |
|
722 \multicolumn{2}{l}{\hspace{5mm}$|$ bn(ACons a t as) $=$ $[$a$]$ @ bn(as)}\\ |
|
723 \end{tabular} |
|
724 |
|
725 \end{frame}} |
|
726 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
727 *} |
|
728 |
|
729 text_raw {* |
|
730 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
731 \mode<presentation>{ |
|
732 \begin{frame}<1-2> |
|
733 \frametitle{\begin{tabular}{c}``Raw'' Definitions\end{tabular}} |
|
734 \mbox{}\\[-6mm] |
|
735 |
|
736 \mbox{}\hspace{10mm} |
|
737 \begin{tabular}{ll} |
|
738 \multicolumn{2}{l}{\isacommand{datatype} trm $=$}\\ |
|
739 \hspace{5mm}\phantom{$|$} Var name\\ |
|
740 \hspace{5mm}$|$ App trm trm\\ |
|
741 \hspace{5mm}$|$ Lam name trm\\ |
|
742 \hspace{5mm}$|$ Let assn trm\\ |
|
743 \multicolumn{2}{l}{\isacommand{and} assn $=$}\\ |
|
744 \multicolumn{2}{l}{\hspace{5mm}\phantom{$|$} ANil}\\ |
|
745 \multicolumn{2}{l}{\hspace{5mm}$|$ ACons name trm assn}\\[5mm] |
|
746 \multicolumn{2}{l}{\isacommand{function} bn \isacommand{where}}\\ |
|
747 \multicolumn{2}{l}{\hspace{5mm}\phantom{$|$} bn(ANil) $=$ $[]$}\\ |
|
748 \multicolumn{2}{l}{\hspace{5mm}$|$ bn(ACons a t as) $=$ $[$a$]$ @ bn(as)}\\ |
|
749 \end{tabular} |
|
750 |
|
751 \only<2>{ |
|
752 \begin{textblock}{5}(10,5) |
|
753 $+$ \begin{tabular}{l}automatically\\ |
|
754 generate fv's\end{tabular} |
|
755 \end{textblock}} |
|
756 \end{frame}} |
|
757 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
758 *} |
|
759 |
|
760 text_raw {* |
|
761 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
762 \mode<presentation>{ |
|
763 \begin{frame}<1> |
|
764 \frametitle{\begin{tabular}{c}\LARGE``Raw'' Alpha-Equivalence\end{tabular}} |
|
765 \mbox{}\\[6mm] |
|
766 |
|
767 \begin{center} |
|
768 Lam x::name t::trm \hspace{10mm}\isacommand{bind} x \isacommand{in} t\\ |
|
769 \end{center} |
|
770 |
|
771 |
|
772 \[ |
|
773 \infer[\text{Lam-}\!\approx_\alpha] |
|
774 {\text{Lam}\;x\;t \approx_\alpha \text{Lam}\;x'\;t'} |
|
775 {([x], t) \approx\!\makebox[0mm][l]{${}_{\text{list}}$} |
|
776 ^{\approx_\alpha,\text{fv}} ([x'], t')} |
|
777 \] |
|
778 |
|
779 |
|
780 \end{frame}} |
|
781 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
782 *} |
|
783 |
|
784 text_raw {* |
|
785 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
786 \mode<presentation>{ |
|
787 \begin{frame}<1> |
|
788 \frametitle{\begin{tabular}{c}\LARGE``Raw'' Alpha-Equivalence\end{tabular}} |
|
789 \mbox{}\\[6mm] |
|
790 |
|
791 \begin{center} |
|
792 Lam x::name y::name t::trm s::trm \hspace{5mm}\isacommand{bind} x y \isacommand{in} t s\\ |
|
793 \end{center} |
|
794 |
|
795 |
|
796 \[ |
|
797 \infer[\text{Lam-}\!\approx_\alpha] |
|
798 {\text{Lam}\;x\;y\;t\;s \approx_\alpha \text{Lam}\;x'\;y'\;t'\;s'} |
|
799 {([x, y], (t, s)) \approx\!\makebox[0mm][l]{${}_{\text{list}}$} |
|
800 ^{R, fv} ([x', y'], (t', s'))} |
|
801 \] |
|
802 |
|
803 \footnotesize |
|
804 where $R =\;\approx_\alpha\times\approx_\alpha$ and $fv = \text{fv}\cup\text{fv}$ |
|
805 |
|
806 \end{frame}} |
|
807 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
808 *} |
|
809 |
|
810 text_raw {* |
|
811 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
812 \mode<presentation>{ |
|
813 \begin{frame}<1-2> |
|
814 \frametitle{\begin{tabular}{c}\LARGE``Raw'' Alpha-Equivalence\end{tabular}} |
|
815 \mbox{}\\[6mm] |
|
816 |
|
817 \begin{center} |
|
818 Let as::assn t::trm \hspace{10mm}\isacommand{bind} bn(as) \isacommand{in} t\\ |
|
819 \end{center} |
|
820 |
|
821 |
|
822 \[ |
|
823 \infer[\text{Let-}\!\approx_\alpha] |
|
824 {\text{Let}\;as\;t \approx_\alpha \text{Let}\;as'\;t'} |
|
825 {(\text{bn}(as), t) \approx\!\makebox[0mm][l]{${}_{\text{list}}$} |
|
826 ^{\approx_\alpha,\text{fv}} (\text{bn}(as'), t') & |
|
827 \onslide<2>{as \approx_\alpha^{\text{bn}} as'}} |
|
828 \] |
|
829 |
|
830 |
|
831 \end{frame}} |
|
832 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
833 *} |
|
834 |
|
835 text_raw {* |
|
836 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
837 \mode<presentation>{ |
|
838 \begin{frame}<1-> |
|
839 \frametitle{\begin{tabular}{c}\LARGE{}$\alpha$ for Binding Functions\end{tabular}} |
|
840 \mbox{}\\[-6mm] |
|
841 |
|
842 \mbox{}\hspace{10mm} |
|
843 \begin{tabular}{l} |
|
844 \ldots\\ |
|
845 \isacommand{binder} bn \isacommand{where}\\ |
|
846 \phantom{$|$} bn(ANil) $=$ $[]$\\ |
|
847 $|$ bn(ACons a t as) $=$ $[$a$]$ @ bn(as)\\ |
|
848 \end{tabular}\bigskip |
|
849 |
|
850 \begin{center} |
|
851 \mbox{\infer{\text{ANil} \approx_\alpha^{\text{bn}} \text{ANil}}{}}\bigskip |
|
852 |
|
853 \mbox{\infer{\text{ACons}\;a\;t\;as \approx_\alpha^{\text{bn}} \text{ACons}\;a'\;t'\;as'} |
|
854 {t \approx_\alpha t' & as \approx_\alpha^{bn} as'}} |
|
855 \end{center} |
|
856 |
|
857 |
|
858 \end{frame}} |
|
859 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
860 *} |
|
861 |
|
862 text_raw {* |
|
863 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
864 \mode<presentation>{ |
|
865 \begin{frame}<1-> |
|
866 \frametitle{\begin{tabular}{c}Automatic Proofs\end{tabular}} |
|
867 \mbox{}\\[-6mm] |
|
868 |
|
869 \begin{itemize} |
|
870 \item we can show that $\alpha$'s are equivalence relations\medskip |
|
871 \item as a result we can use the quotient package to introduce the type(s) |
|
872 of $\alpha$-equated terms |
|
873 |
|
874 \[ |
|
875 \infer |
|
876 {\text{Lam}\;x\;t \alert{=} \text{Lam}\;x'\;t'} |
|
877 {\only<1>{([x], t) \approx\!\makebox[0mm][l]{${}_{\text{list}}$} |
|
878 ^{=,\text{supp}} ([x'], t')}% |
|
879 \only<2>{[x].t = [x'].t'}} |
|
880 \] |
|
881 |
|
882 |
|
883 \item the properties for support are implied by the properties of $[\_].\_$ |
|
884 \item we can derive strong induction principles (almost automatic---just a matter of |
|
885 another week or two) |
|
886 \end{itemize} |
|
887 |
|
888 |
|
889 \end{frame}} |
|
890 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
891 *} |
|
892 |
|
893 text_raw {* |
|
894 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
895 \mode<presentation>{ |
|
896 \begin{frame}<1>[t] |
|
897 \frametitle{\begin{tabular}{c}Runtime is Acceptable\end{tabular}} |
|
898 \mbox{}\\[-7mm]\mbox{} |
|
899 |
|
900 \footnotesize |
|
901 \begin{center} |
|
902 \begin{tikzpicture} |
|
903 \draw (0,0) node[inner sep=2mm, ultra thick, draw=white, rounded corners=2mm] |
|
904 (A) {\begin{minipage}{0.8cm}bind.\\spec.\end{minipage}}; |
|
905 |
|
906 \draw (2,0) node[inner sep=2mm, ultra thick, draw=white, rounded corners=2mm] |
|
907 (B) {\begin{minipage}{0.8cm}raw\\terms\end{minipage}}; |
|
908 |
|
909 \draw (4,0) node[inner sep=2mm, ultra thick, draw=white, rounded corners=2mm] |
|
910 (C) {\begin{minipage}{0.8cm}$\alpha$-\\equiv.\end{minipage}}; |
|
911 |
|
912 \draw (0,-2) node[inner sep=2mm, ultra thick, draw=white, rounded corners=2mm] |
|
913 (D) {\begin{minipage}{0.8cm}quot.\\type\end{minipage}}; |
|
914 |
|
915 \draw (2,-2) node[inner sep=2mm, ultra thick, draw=white, rounded corners=2mm] |
|
916 (E) {\begin{minipage}{0.8cm}lift\\thms\end{minipage}}; |
|
917 |
|
918 \draw (4,-2) node[inner sep=2mm, ultra thick, draw=white, rounded corners=2mm] |
|
919 (F) {\begin{minipage}{0.8cm}add.\\thms\end{minipage}}; |
|
920 |
|
921 \draw[->,white!50,line width=1mm] (A) -- (B); |
|
922 \draw[->,white!50,line width=1mm] (B) -- (C); |
|
923 \draw[->,white!50,line width=1mm, line join=round, rounded corners=2mm] |
|
924 (C) -- (5,0) -- (5,-1) -- (-1,-1) -- (-1,-2) -- (D); |
|
925 \draw[->,white!50,line width=1mm] (D) -- (E); |
|
926 \draw[->,white!50,line width=1mm] (E) -- (F); |
|
927 \end{tikzpicture} |
|
928 \end{center} |
|
929 |
|
930 \begin{itemize} |
|
931 \item Core Haskell: 11 types, 49 term-constructors, |
|
932 \end{itemize} |
|
933 |
|
934 \end{frame}} |
|
935 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
936 *} |
|
937 |
|
938 |
|
939 text_raw {* |
|
940 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
941 \mode<presentation>{ |
|
942 \begin{frame}<1-> |
|
943 \frametitle{\begin{tabular}{c}Interesting Phenomenon\end{tabular}} |
|
944 \mbox{}\\[-6mm] |
|
945 |
|
946 \small |
|
947 \mbox{}\hspace{10mm} |
|
948 \begin{tabular}{ll} |
|
949 \multicolumn{2}{l}{\isacommand{nominal\_datatype} trm $=$}\\ |
|
950 \hspace{5mm}\phantom{$|$} Var name\\ |
|
951 \hspace{5mm}$|$ App trm trm\\ |
|
952 \hspace{5mm}$|$ Lam x::name t::trm |
|
953 & \isacommand{bind} x \isacommand{in} t\\ |
|
954 \hspace{5mm}$|$ Let as::assn t::trm |
|
955 & \isacommand{bind} bn(as) \isacommand{in} t\\ |
|
956 \multicolumn{2}{l}{\isacommand{and} assn $=$}\\ |
|
957 \multicolumn{2}{l}{\hspace{5mm}\phantom{$|$} ANil}\\ |
|
958 \multicolumn{2}{l}{\hspace{5mm}$|$ ACons name trm assn}\\ |
|
959 \multicolumn{2}{l}{\isacommand{binder} bn \isacommand{where}}\\ |
|
960 \multicolumn{2}{l}{\hspace{5mm}\phantom{$|$} bn(ANil) $=$ $[]$}\\ |
|
961 \multicolumn{2}{l}{\hspace{5mm}$|$ bn(ACons a t as) $=$ $[$a$]$ @ bn(as)}\\ |
|
962 \end{tabular}\bigskip\medskip |
|
963 |
|
964 we cannot quotient assn: ACons a \ldots $\not\approx_\alpha$ ACons b \ldots |
|
965 |
|
966 \end{frame}} |
|
967 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
968 *} |
|
969 |
|
970 text_raw {* |
|
971 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
972 \mode<presentation>{ |
|
973 \begin{frame}<1-> |
|
974 \frametitle{\begin{tabular}{c}Conclusion\end{tabular}} |
|
975 \mbox{}\\[-6mm] |
|
976 |
|
977 \begin{itemize} |
|
978 \item the user does not see anything of the raw level\medskip |
|
979 \only<1>{\begin{center} |
|
980 Lam a (Var a) \alert{$=$} Lam b (Var b) |
|
981 \end{center}\bigskip} |
|
982 |
|
983 \item<2-> we have not yet done function definitions (will come soon and |
|
984 we hope to make improvements over the old way there too)\medskip |
|
985 \item<3-> it took quite some time to get here, but it seems worthwhile |
|
986 (Barendregt's variable convention is unsound in general, |
|
987 found bugs in two paper proofs, quotient package, POPL 2011 tutorial)\medskip |
|
988 \end{itemize} |
|
989 |
|
990 |
|
991 \end{frame}} |
|
992 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
993 *} |
|
994 |
|
995 (*<*) |
|
996 end |
|
997 (*>*) |