1 (*<*) |
|
2 theory Slides5 |
|
3 imports "~~/src/HOL/Library/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 %% shallow, deep, and recursive binders |
|
15 %% |
|
16 %%\renewcommand{\slidecaption}{Cambridge, 8.~June 2010} |
|
17 %%\renewcommand{\slidecaption}{Uppsala, 3.~March 2011} |
|
18 \renewcommand{\slidecaption}{Saarbrücken, 31.~March 2011} |
|
19 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
20 \mode<presentation>{ |
|
21 \begin{frame}<1>[t] |
|
22 \frametitle{% |
|
23 \begin{tabular}{@ {\hspace{-3mm}}c@ {}} |
|
24 \\ |
|
25 \LARGE General Bindings and\\ |
|
26 \LARGE Alpha-Equivalence\\ |
|
27 \LARGE in Nominal Isabelle\\[3mm] |
|
28 \Large Or, Nominal Isabelle 2\\[-5mm] |
|
29 \end{tabular}} |
|
30 \begin{center} |
|
31 Christian Urban |
|
32 \end{center} |
|
33 \begin{center} |
|
34 joint work with {\bf Cezary Kaliszyk}\\[0mm] |
|
35 \end{center} |
|
36 \end{frame}} |
|
37 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
38 |
|
39 *} |
|
40 |
|
41 text_raw {* |
|
42 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
43 \mode<presentation>{ |
|
44 \begin{frame}<1-2> |
|
45 \frametitle{\begin{tabular}{c}Binding in Old Nominal\end{tabular}} |
|
46 \mbox{}\\[-6mm] |
|
47 |
|
48 \begin{itemize} |
|
49 \item the old Nominal Isabelle provided a reasoning infrastructure for single binders\medskip |
|
50 |
|
51 \begin{center} |
|
52 Lam [a].(Var a) |
|
53 \end{center}\bigskip |
|
54 |
|
55 \item<2-> but representing |
|
56 |
|
57 \begin{center} |
|
58 $\forall\{a_1,\ldots,a_n\}.\; T$ |
|
59 \end{center}\medskip |
|
60 |
|
61 with single binders and reasoning about it is a \alert{\bf major} pain; |
|
62 take my word for it! |
|
63 \end{itemize} |
|
64 |
|
65 \only<1>{ |
|
66 \begin{textblock}{6}(1.5,11) |
|
67 \small |
|
68 for example\\ |
|
69 \begin{tabular}{l@ {\hspace{2mm}}l} |
|
70 & a $\fresh$ Lam [a]. t\\ |
|
71 & Lam [a]. (Var a) \alert{$=$} Lam [b]. (Var b)\\ |
|
72 & Barendregt-style reasoning about bound variables\\ |
|
73 \end{tabular} |
|
74 \end{textblock}} |
|
75 |
|
76 \end{frame}} |
|
77 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
78 *} |
|
79 |
|
80 |
|
81 |
|
82 text_raw {* |
|
83 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
84 \mode<presentation>{ |
|
85 \begin{frame}<1-6> |
|
86 \frametitle{New Types in HOL} |
|
87 |
|
88 \begin{center} |
|
89 \begin{tikzpicture}[scale=1.5] |
|
90 %%%\draw[step=2mm] (-4,-1) grid (4,1); |
|
91 |
|
92 \onslide<2-4,6>{\draw[very thick] (0.7,0.4) circle (4.25mm);} |
|
93 \onslide<1-4,6>{\draw[rounded corners=1mm, very thick] ( 0.0,-0.8) rectangle ( 1.8, 0.9);} |
|
94 \onslide<3-5,6>{\draw[rounded corners=1mm, very thick] (-1.95,0.85) rectangle (-2.85,-0.05);} |
|
95 |
|
96 \onslide<3-4,6>{\draw (-2.0, 0.845) -- (0.7,0.845);} |
|
97 \onslide<3-4,6>{\draw (-2.0,-0.045) -- (0.7,-0.045);} |
|
98 |
|
99 \onslide<4-4,6>{\alert{\draw ( 0.7, 0.4) node {\footnotesize\begin{tabular}{@ {}c@ {}}$\alpha$-\\[-1mm]classes\end{tabular}};}} |
|
100 \onslide<4-5,6>{\alert{\draw (-2.4, 0.4) node {\footnotesize\begin{tabular}{@ {}c@ {}}$\alpha$-eq.\\[-1mm]terms\end{tabular}};}} |
|
101 \onslide<1-4,6>{\draw (1.8, 0.48) node[right=-0.1mm] |
|
102 {\footnotesize\begin{tabular}{@ {}l@ {}}existing\\[-1mm] type\\ \onslide<4-4,6>{\alert{(sets of raw terms)}}\end{tabular}};} |
|
103 \onslide<2-4,6>{\draw (0.9, -0.35) node {\footnotesize\begin{tabular}{@ {}l@ {}}non-empty\\[-1mm]subset\end{tabular}};} |
|
104 \onslide<3-5,6>{\draw (-3.25, 0.55) node {\footnotesize\begin{tabular}{@ {}l@ {}}new\\[-1mm]type\end{tabular}};} |
|
105 |
|
106 \onslide<3-4,6>{\draw[<->, very thick] (-1.8, 0.3) -- (-0.1,0.3);} |
|
107 \onslide<3-4,6>{\draw (-0.95, 0.3) node[above=0mm] {\footnotesize{}isomorphism};} |
|
108 |
|
109 \onslide<6>{\draw[->, line width=2mm, red] (-1.0,-0.4) -- (0.35,0.16);} |
|
110 \end{tikzpicture} |
|
111 \end{center} |
|
112 |
|
113 \begin{center} |
|
114 \textcolor{red}{\large\bf\onslide<6>{define $\alpha$-equivalence}} |
|
115 \end{center} |
|
116 |
|
117 \end{frame}} |
|
118 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
119 *} |
|
120 |
|
121 |
|
122 |
|
123 text_raw {* |
|
124 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
125 \mode<presentation>{ |
|
126 \begin{frame}<1-4> |
|
127 \frametitle{\begin{tabular}{c}Binding Sets of Names\end{tabular}} |
|
128 \mbox{}\\[-3mm] |
|
129 |
|
130 \begin{itemize} |
|
131 \item binding sets of names has some interesting properties:\medskip |
|
132 |
|
133 \begin{center} |
|
134 \begin{tabular}{l} |
|
135 \textcolor{blue}{$\forall\{x, y\}.\, x \rightarrow y \;\;\approx_\alpha\;\; \forall\{y, x\}.\, y \rightarrow x$} |
|
136 \bigskip\smallskip\\ |
|
137 |
|
138 \onslide<2->{% |
|
139 \textcolor{blue}{$\forall\{x, y\}.\, x \rightarrow y \;\;\not\approx_\alpha\;\; \forall\{z\}.\, z \rightarrow z$} |
|
140 }\bigskip\smallskip\\ |
|
141 |
|
142 \onslide<3->{% |
|
143 \textcolor{blue}{$\forall\{x\}.\, x \rightarrow y \;\;\approx_\alpha\;\; \forall\{x, \alert{z}\}.\, x \rightarrow y$} |
|
144 }\medskip\\ |
|
145 \onslide<3->{\hspace{4cm}\small provided $z$ is fresh for the type} |
|
146 \end{tabular} |
|
147 \end{center} |
|
148 \end{itemize} |
|
149 |
|
150 \begin{textblock}{8}(2,14.5) |
|
151 \footnotesize $^*$ $x$, $y$, $z$ are assumed to be distinct |
|
152 \end{textblock} |
|
153 |
|
154 \only<4>{ |
|
155 \begin{textblock}{6}(2.5,4) |
|
156 \begin{tikzpicture} |
|
157 \draw (0,0) node[inner sep=3mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] |
|
158 {\normalsize\color{darkgray} |
|
159 \begin{minipage}{8cm}\raggedright |
|
160 For type-schemes the order of bound names does not matter, and |
|
161 $\alpha$-equivalence is preserved under \alert{vacuous} binders. |
|
162 \end{minipage}}; |
|
163 \end{tikzpicture} |
|
164 \end{textblock}} |
|
165 \end{frame}} |
|
166 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
167 *} |
|
168 |
|
169 text_raw {* |
|
170 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
171 \mode<presentation>{ |
|
172 \begin{frame}<1-3> |
|
173 \frametitle{\begin{tabular}{c}Other Binding Modes\end{tabular}} |
|
174 \mbox{}\\[-3mm] |
|
175 |
|
176 \begin{itemize} |
|
177 \item alpha-equivalence being preserved under vacuous binders is \underline{not} always |
|
178 wanted:\bigskip\bigskip\normalsize |
|
179 |
|
180 \textcolor{blue}{\begin{tabular}{@ {\hspace{-8mm}}l} |
|
181 $\text{let}\;x = 3\;\text{and}\;y = 2\;\text{in}\;x - y\;\text{end}$\medskip\\ |
|
182 \onslide<2->{$\;\;\;\only<2>{\approx_\alpha}\only<3>{\alert{\not\approx_\alpha}} |
|
183 \text{let}\;y = 2\;\text{and}\;x = 3\only<3->{\alert{\;\text{and} |
|
184 \;z = \text{loop}}}\;\text{in}\;x - y\;\text{end}$} |
|
185 \end{tabular}} |
|
186 |
|
187 |
|
188 \end{itemize} |
|
189 |
|
190 \end{frame}} |
|
191 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
192 *} |
|
193 |
|
194 text_raw {* |
|
195 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
196 \mode<presentation>{ |
|
197 \begin{frame}<1> |
|
198 \frametitle{\begin{tabular}{c}\LARGE{}Even Another Binding Mode\end{tabular}} |
|
199 \mbox{}\\[-3mm] |
|
200 |
|
201 \begin{itemize} |
|
202 \item sometimes one wants to abstract more than one name, but the order \underline{does} matter\bigskip |
|
203 |
|
204 \begin{center} |
|
205 \textcolor{blue}{\begin{tabular}{@ {\hspace{-8mm}}l} |
|
206 $\text{let}\;(x, y) = (3, 2)\;\text{in}\;x - y\;\text{end}$\medskip\\ |
|
207 $\;\;\;\not\approx_\alpha |
|
208 \text{let}\;(y, x) = (3, 2)\;\text{in}\;x - y\;\text{end}$ |
|
209 \end{tabular}} |
|
210 \end{center} |
|
211 |
|
212 |
|
213 \end{itemize} |
|
214 |
|
215 \end{frame}} |
|
216 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
217 *} |
|
218 |
|
219 text_raw {* |
|
220 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
221 \mode<presentation>{ |
|
222 \begin{frame}<1-2> |
|
223 \frametitle{\begin{tabular}{c}\LARGE{}Three Binding Modes\end{tabular}} |
|
224 \mbox{}\\[-3mm] |
|
225 |
|
226 \begin{itemize} |
|
227 \item the order does not matter and alpha-equivelence is preserved under |
|
228 vacuous binders \textcolor{gray}{(restriction)}\medskip |
|
229 |
|
230 \item the order does not matter, but the cardinality of the binders |
|
231 must be the same \textcolor{gray}{(abstraction)}\medskip |
|
232 |
|
233 \item the order does matter \textcolor{gray}{(iterated single binders)} |
|
234 \end{itemize} |
|
235 |
|
236 \onslide<2->{ |
|
237 \begin{center} |
|
238 \isacommand{bind (set+)}\hspace{6mm} |
|
239 \isacommand{bind (set)}\hspace{6mm} |
|
240 \isacommand{bind} |
|
241 \end{center}} |
|
242 |
|
243 \end{frame}} |
|
244 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
245 *} |
|
246 |
|
247 text_raw {* |
|
248 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
249 \mode<presentation>{ |
|
250 \begin{frame}<1-3> |
|
251 \frametitle{\begin{tabular}{c}Specification of Binding\end{tabular}} |
|
252 \mbox{}\\[-6mm] |
|
253 |
|
254 \mbox{}\hspace{10mm} |
|
255 \begin{tabular}{ll} |
|
256 \multicolumn{2}{l}{\isacommand{nominal\_datatype} trm $=$}\\ |
|
257 \hspace{5mm}\phantom{$|$} Var name\\ |
|
258 \hspace{5mm}$|$ App trm trm\\ |
|
259 \hspace{5mm}$|$ Lam \only<2->{x::}name \only<2->{t::}trm |
|
260 & \onslide<2->{\isacommand{bind} x \isacommand{in} t}\\ |
|
261 \hspace{5mm}$|$ Let \only<2->{as::}assns \only<2->{t::}trm |
|
262 & \onslide<2->{\isacommand{bind} bn(as) \isacommand{in} t}\\ |
|
263 \multicolumn{2}{l}{\isacommand{and} assns $=$}\\ |
|
264 \multicolumn{2}{l}{\hspace{5mm}\phantom{$|$} ANil}\\ |
|
265 \multicolumn{2}{l}{\hspace{5mm}$|$ ACons name trm assns}\\ |
|
266 \multicolumn{2}{l}{\onslide<3->{\isacommand{binder} bn \isacommand{where}}}\\ |
|
267 \multicolumn{2}{l}{\onslide<3->{\hspace{5mm}\phantom{$|$} bn(ANil) $=$ []}}\\ |
|
268 \multicolumn{2}{l}{\onslide<3->{\hspace{5mm}$|$ bn(ACons a t as) $=$ [a] @ bn(as)}}\\ |
|
269 \end{tabular} |
|
270 |
|
271 |
|
272 |
|
273 \end{frame}} |
|
274 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
275 *} |
|
276 |
|
277 |
|
278 text_raw {* |
|
279 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
280 \mode<presentation>{ |
|
281 \begin{frame}<1-8> |
|
282 \frametitle{\begin{tabular}{c}Alpha-Equivalence\end{tabular}} |
|
283 \mbox{}\\[-3mm] |
|
284 |
|
285 \begin{itemize} |
|
286 \item lets first look at pairs\bigskip\medskip |
|
287 |
|
288 \textcolor{blue}{\begin{tabular}{@ {\hspace{1cm}}l} |
|
289 $(as, x) \onslide<2->{\approx\!}\makebox[5mm][l]{\only<2-6>{${}_{\text{set}}$}% |
|
290 \only<7>{${}_{\text{\alert{list}}}$}% |
|
291 \only<8>{${}_{\text{\alert{set+}}}$}}% |
|
292 \,\onslide<2->{(bs,y)}$ |
|
293 \end{tabular}}\bigskip |
|
294 \end{itemize} |
|
295 |
|
296 \only<1>{ |
|
297 \begin{textblock}{8}(3,8.5) |
|
298 \begin{tabular}{l@ {\hspace{2mm}}p{8cm}} |
|
299 & \textcolor{blue}{$as$} is a set of names\ldots the binders\\ |
|
300 & \textcolor{blue}{$x$} is the body (might be a tuple)\\ |
|
301 & \textcolor{blue}{$\approx_{\text{set}}$} is where the cardinality |
|
302 of the binders has to be the same\\ |
|
303 \end{tabular} |
|
304 \end{textblock}} |
|
305 |
|
306 \only<4->{ |
|
307 \begin{textblock}{12}(5,8) |
|
308 \textcolor{blue}{ |
|
309 \begin{tabular}{ll@ {\hspace{1mm}}l} |
|
310 $\dn$ & \onslide<5->{$\exists \pi.\,$} & $\text{fv}(x) - as = \text{fv}(y) - bs$\\[1mm] |
|
311 & \onslide<5->{$\;\;\;\wedge$} & \onslide<5->{$\text{fv}(x) - as \fresh^* \pi$}\\[1mm] |
|
312 & \onslide<5->{$\;\;\;\wedge$} & \onslide<5->{$(\pi \act x) = y$}\\[1mm] |
|
313 & \only<6-7>{$\;\;\;\wedge$}\only<8>{\textcolor{gray}{\xout{$\;\;\;\wedge$}}} & |
|
314 \only<6-7>{$\pi \act as = bs$}\only<8>{\textcolor{gray}{\xout{$\pi \act as = bs$}}}\\ |
|
315 \end{tabular}} |
|
316 \end{textblock}} |
|
317 |
|
318 \only<7>{ |
|
319 \begin{textblock}{7}(3,13.8) |
|
320 \footnotesize $^*$ $as$ and $bs$ are \alert{lists} of names |
|
321 \end{textblock}} |
|
322 \end{frame}} |
|
323 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
324 *} |
|
325 |
|
326 text_raw {* |
|
327 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
328 \mode<presentation>{ |
|
329 \begin{frame}<1-3> |
|
330 \frametitle{\begin{tabular}{c}Examples\end{tabular}} |
|
331 \mbox{}\\[-3mm] |
|
332 |
|
333 \begin{itemize} |
|
334 \item lets look at type-schemes:\medskip\medskip |
|
335 |
|
336 \begin{center} |
|
337 \textcolor{blue}{$(as, x) \approx\!\makebox[5mm][l]{${}_{\text{set}}$} (bs, y)$} |
|
338 \end{center}\medskip |
|
339 |
|
340 \onslide<2->{ |
|
341 \begin{center} |
|
342 \textcolor{blue}{ |
|
343 \begin{tabular}{l} |
|
344 $\text{fv}(x) = \{x\}$\\[1mm] |
|
345 $\text{fv}(T_1 \rightarrow T_2) = \text{fv}(T_1) \cup \text{fv}(T_2)$\\ |
|
346 \end{tabular}} |
|
347 \end{center}} |
|
348 \end{itemize} |
|
349 |
|
350 |
|
351 \only<3->{ |
|
352 \begin{textblock}{4}(0.3,12) |
|
353 \begin{tikzpicture} |
|
354 \draw (0,0) node[inner sep=1mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] |
|
355 {\tiny\color{darkgray} |
|
356 \begin{minipage}{3.4cm}\raggedright |
|
357 \begin{tabular}{r@ {\hspace{1mm}}l} |
|
358 \multicolumn{2}{@ {}l}{set+:}\\ |
|
359 $\exists\pi.$ & $\text{fv}(x) - as = \text{fv}(y) - bs$\\ |
|
360 $\wedge$ & $\text{fv}(x) - as \fresh^* \pi$\\ |
|
361 $\wedge$ & $\pi \cdot x = y$\\ |
|
362 \\ |
|
363 \end{tabular} |
|
364 \end{minipage}}; |
|
365 \end{tikzpicture} |
|
366 \end{textblock}} |
|
367 \only<3->{ |
|
368 \begin{textblock}{4}(5.2,12) |
|
369 \begin{tikzpicture} |
|
370 \draw (0,0) node[inner sep=1mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] |
|
371 {\tiny\color{darkgray} |
|
372 \begin{minipage}{3.4cm}\raggedright |
|
373 \begin{tabular}{r@ {\hspace{1mm}}l} |
|
374 \multicolumn{2}{@ {}l}{set:}\\ |
|
375 $\exists\pi.$ & $\text{fv}(x) - as = \text{fv}(y) - bs$\\ |
|
376 $\wedge$ & $\text{fv}(x) - as \fresh^* \pi$\\ |
|
377 $\wedge$ & $\pi \cdot x = y$\\ |
|
378 $\wedge$ & $\pi \cdot as = bs$\\ |
|
379 \end{tabular} |
|
380 \end{minipage}}; |
|
381 \end{tikzpicture} |
|
382 \end{textblock}} |
|
383 \only<3->{ |
|
384 \begin{textblock}{4}(10.2,12) |
|
385 \begin{tikzpicture} |
|
386 \draw (0,0) node[inner sep=1mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] |
|
387 {\tiny\color{darkgray} |
|
388 \begin{minipage}{3.4cm}\raggedright |
|
389 \begin{tabular}{r@ {\hspace{1mm}}l} |
|
390 \multicolumn{2}{@ {}l}{list:}\\ |
|
391 $\exists\pi.$ & $\text{fv}(x) - as = \text{fv}(y) - bs$\\ |
|
392 $\wedge$ & $\text{fv}(x) - as \fresh^* \pi$\\ |
|
393 $\wedge$ & $\pi \cdot x = y$\\ |
|
394 $\wedge$ & $\pi \cdot as = bs$\\ |
|
395 \end{tabular} |
|
396 \end{minipage}}; |
|
397 \end{tikzpicture} |
|
398 \end{textblock}} |
|
399 |
|
400 \end{frame}} |
|
401 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
402 *} |
|
403 |
|
404 text_raw {* |
|
405 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
406 \mode<presentation>{ |
|
407 \begin{frame}<1-2> |
|
408 \frametitle{\begin{tabular}{c}Examples\end{tabular}} |
|
409 \mbox{}\\[-3mm] |
|
410 |
|
411 \begin{center} |
|
412 \textcolor{blue}{ |
|
413 \only<1>{$(\{x, y\}, x \rightarrow y) \approx_? (\{x, y\}, y \rightarrow x)$} |
|
414 \only<2>{$([x, y], x \rightarrow y) \approx_? ([x, y], y \rightarrow x)$}} |
|
415 \end{center} |
|
416 |
|
417 \begin{itemize} |
|
418 \item \textcolor{blue}{$\approx_{\text{set+}}$, $\approx_{\text{set}}$% |
|
419 \only<2>{, \alert{$\not\approx_{\text{list}}$}}} |
|
420 \end{itemize} |
|
421 |
|
422 |
|
423 \only<1->{ |
|
424 \begin{textblock}{4}(0.3,12) |
|
425 \begin{tikzpicture} |
|
426 \draw (0,0) node[inner sep=1mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] |
|
427 {\tiny\color{darkgray} |
|
428 \begin{minipage}{3.4cm}\raggedright |
|
429 \begin{tabular}{r@ {\hspace{1mm}}l} |
|
430 \multicolumn{2}{@ {}l}{set+:}\\ |
|
431 $\exists\pi.$ & $\text{fv}(x) - as = \text{fv}(y) - bs$\\ |
|
432 $\wedge$ & $\text{fv}(x) - as \fresh^* \pi$\\ |
|
433 $\wedge$ & $\pi \cdot x = y$\\ |
|
434 \\ |
|
435 \end{tabular} |
|
436 \end{minipage}}; |
|
437 \end{tikzpicture} |
|
438 \end{textblock}} |
|
439 \only<1->{ |
|
440 \begin{textblock}{4}(5.2,12) |
|
441 \begin{tikzpicture} |
|
442 \draw (0,0) node[inner sep=1mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] |
|
443 {\tiny\color{darkgray} |
|
444 \begin{minipage}{3.4cm}\raggedright |
|
445 \begin{tabular}{r@ {\hspace{1mm}}l} |
|
446 \multicolumn{2}{@ {}l}{set:}\\ |
|
447 $\exists\pi.$ & $\text{fv}(x) - as = \text{fv}(y) - bs$\\ |
|
448 $\wedge$ & $\text{fv}(x) - as \fresh^* \pi$\\ |
|
449 $\wedge$ & $\pi \cdot x = y$\\ |
|
450 $\wedge$ & $\pi \cdot as = bs$\\ |
|
451 \end{tabular} |
|
452 \end{minipage}}; |
|
453 \end{tikzpicture} |
|
454 \end{textblock}} |
|
455 \only<1->{ |
|
456 \begin{textblock}{4}(10.2,12) |
|
457 \begin{tikzpicture} |
|
458 \draw (0,0) node[inner sep=1mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] |
|
459 {\tiny\color{darkgray} |
|
460 \begin{minipage}{3.4cm}\raggedright |
|
461 \begin{tabular}{r@ {\hspace{1mm}}l} |
|
462 \multicolumn{2}{@ {}l}{list:}\\ |
|
463 $\exists\pi.$ & $\text{fv}(x) - as = \text{fv}(y) - bs$\\ |
|
464 $\wedge$ & $\text{fv}(x) - as \fresh^* \pi$\\ |
|
465 $\wedge$ & $\pi \cdot x = y$\\ |
|
466 $\wedge$ & $\pi \cdot as = bs$\\ |
|
467 \end{tabular} |
|
468 \end{minipage}}; |
|
469 \end{tikzpicture} |
|
470 \end{textblock}} |
|
471 |
|
472 \end{frame}} |
|
473 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
474 *} |
|
475 |
|
476 text_raw {* |
|
477 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
478 \mode<presentation>{ |
|
479 \begin{frame}<1-2> |
|
480 \frametitle{\begin{tabular}{c}Examples\end{tabular}} |
|
481 \mbox{}\\[-3mm] |
|
482 |
|
483 \begin{center} |
|
484 \textcolor{blue}{\only<1>{$(\{x\}, x) \approx_? (\{x, y\}, x)$}} |
|
485 \end{center} |
|
486 |
|
487 \begin{itemize} |
|
488 \item \textcolor{blue}{$\approx_{\text{set+}}$, $\not\approx_{\text{set}}$, |
|
489 $\not\approx_{\text{list}}$} |
|
490 \end{itemize} |
|
491 |
|
492 |
|
493 \only<1->{ |
|
494 \begin{textblock}{4}(0.3,12) |
|
495 \begin{tikzpicture} |
|
496 \draw (0,0) node[inner sep=1mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] |
|
497 {\tiny\color{darkgray} |
|
498 \begin{minipage}{3.4cm}\raggedright |
|
499 \begin{tabular}{r@ {\hspace{1mm}}l} |
|
500 \multicolumn{2}{@ {}l}{set+:}\\ |
|
501 $\exists\pi.$ & $\text{fv}(x) - as = \text{fv}(y) - bs$\\ |
|
502 $\wedge$ & $\text{fv}(x) - as \fresh^* \pi$\\ |
|
503 $\wedge$ & $\pi \cdot x = y$\\ |
|
504 \\ |
|
505 \end{tabular} |
|
506 \end{minipage}}; |
|
507 \end{tikzpicture} |
|
508 \end{textblock}} |
|
509 \only<1->{ |
|
510 \begin{textblock}{4}(5.2,12) |
|
511 \begin{tikzpicture} |
|
512 \draw (0,0) node[inner sep=1mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] |
|
513 {\tiny\color{darkgray} |
|
514 \begin{minipage}{3.4cm}\raggedright |
|
515 \begin{tabular}{r@ {\hspace{1mm}}l} |
|
516 \multicolumn{2}{@ {}l}{set:}\\ |
|
517 $\exists\pi.$ & $\text{fv}(x) - as = \text{fv}(y) - bs$\\ |
|
518 $\wedge$ & $\text{fv}(x) - as \fresh^* \pi$\\ |
|
519 $\wedge$ & $\pi \cdot x = y$\\ |
|
520 $\wedge$ & $\pi \cdot as = bs$\\ |
|
521 \end{tabular} |
|
522 \end{minipage}}; |
|
523 \end{tikzpicture} |
|
524 \end{textblock}} |
|
525 \only<1->{ |
|
526 \begin{textblock}{4}(10.2,12) |
|
527 \begin{tikzpicture} |
|
528 \draw (0,0) node[inner sep=1mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] |
|
529 {\tiny\color{darkgray} |
|
530 \begin{minipage}{3.4cm}\raggedright |
|
531 \begin{tabular}{r@ {\hspace{1mm}}l} |
|
532 \multicolumn{2}{@ {}l}{list:}\\ |
|
533 $\exists\pi.$ & $\text{fv}(x) - as = \text{fv}(y) - bs$\\ |
|
534 $\wedge$ & $\text{fv}(x) - as \fresh^* \pi$\\ |
|
535 $\wedge$ & $\pi \cdot x = y$\\ |
|
536 $\wedge$ & $\pi \cdot as = bs$\\ |
|
537 \end{tabular} |
|
538 \end{minipage}}; |
|
539 \end{tikzpicture} |
|
540 \end{textblock}} |
|
541 |
|
542 \only<2>{ |
|
543 \begin{textblock}{6}(2.5,4) |
|
544 \begin{tikzpicture} |
|
545 \draw (0,0) node[inner sep=5mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] |
|
546 {\normalsize |
|
547 \begin{minipage}{8cm}\raggedright |
|
548 \begin{itemize} |
|
549 \item \color{darkgray}$\alpha$-equivalences coincide when a single name is |
|
550 abstracted |
|
551 \item \color{darkgray}in that case they are equivalent to ``old-fashioned'' definitions of $\alpha$ |
|
552 \end{itemize} |
|
553 \end{minipage}}; |
|
554 \end{tikzpicture} |
|
555 \end{textblock}} |
|
556 |
|
557 \end{frame}} |
|
558 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
559 *} |
|
560 |
|
561 text_raw {* |
|
562 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
563 \mode<presentation>{ |
|
564 \begin{frame}<1-> |
|
565 \frametitle{\begin{tabular}{c}Our Specifications\end{tabular}} |
|
566 \mbox{}\\[-6mm] |
|
567 |
|
568 \mbox{}\hspace{10mm} |
|
569 \begin{tabular}{ll} |
|
570 \multicolumn{2}{l}{\isacommand{nominal\_datatype} trm $=$}\\ |
|
571 \hspace{5mm}\phantom{$|$} Var name\\ |
|
572 \hspace{5mm}$|$ App trm trm\\ |
|
573 \hspace{5mm}$|$ Lam x::name t::trm |
|
574 & \isacommand{bind} x \isacommand{in} t\\ |
|
575 \hspace{5mm}$|$ Let as::assns t::trm |
|
576 & \isacommand{bind} bn(as) \isacommand{in} t\\ |
|
577 \multicolumn{2}{l}{\isacommand{and} assns $=$}\\ |
|
578 \multicolumn{2}{l}{\hspace{5mm}\phantom{$|$} ANil}\\ |
|
579 \multicolumn{2}{l}{\hspace{5mm}$|$ ACons name trm assns}\\ |
|
580 \multicolumn{2}{l}{\isacommand{binder} bn \isacommand{where}}\\ |
|
581 \multicolumn{2}{l}{\hspace{5mm}\phantom{$|$} bn(ANil) $=$ $[]$}\\ |
|
582 \multicolumn{2}{l}{\hspace{5mm}$|$ bn(ACons a t as) $=$ $[$a$]$ @ bn(as)}\\ |
|
583 \end{tabular} |
|
584 |
|
585 \end{frame}} |
|
586 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
587 *} |
|
588 |
|
589 text_raw {* |
|
590 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
591 \mode<presentation>{ |
|
592 \begin{frame}<1>[c] |
|
593 \frametitle{\begin{tabular}{c}Binding Functions\end{tabular}} |
|
594 |
|
595 \begin{center} |
|
596 \begin{tikzpicture} |
|
597 \node (A) at (-0.5,1) {Foo $(\lambda y. \lambda x. t)$}; |
|
598 \node (B) at ( 1.5,1) {$s$}; |
|
599 \onslide<1>{\node (C) at (0.5,-0.5) {$\{y, x\}$};} |
|
600 \onslide<1>{\draw[->,red,line width=1mm] (A) -- (C);} |
|
601 \onslide<1>{\draw[->,red,line width=1mm] (C) -- (B);} |
|
602 \end{tikzpicture} |
|
603 \end{center} |
|
604 |
|
605 |
|
606 \end{frame}} |
|
607 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
608 *} |
|
609 |
|
610 text_raw {* |
|
611 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
612 \mode<presentation>{ |
|
613 \begin{frame}<1->[t] |
|
614 \frametitle{\begin{tabular}{c}Binder Clauses\end{tabular}} |
|
615 |
|
616 \begin{itemize} |
|
617 \item We need for a bound variable to have a `clear scope', and bound |
|
618 variables should not be free and bound at the same time.\bigskip |
|
619 \end{itemize} |
|
620 |
|
621 \begin{center} |
|
622 \only<1>{ |
|
623 \begin{tabular}{@ {\hspace{-5mm}}l} |
|
624 \alert{\bf shallow binders}\\ |
|
625 \hspace{4mm}Lam x::name t::trm\hspace{4mm} \isacommand{bind} x \isacommand{in} t\\ |
|
626 \hspace{4mm}All xs::name set T::ty\hspace{4mm} \isacommand{bind} xs \isacommand{in} T\\ |
|
627 \hspace{4mm}Foo x::name t$_1$::trm t$_2$::trm\hspace{4mm} |
|
628 \isacommand{bind} x \isacommand{in} t$_1$, \isacommand{bind} x \isacommand{in} t$_2$\\ |
|
629 \hspace{4mm}Bar x::name t$_1$::trm t$_2$::trm\hspace{4mm} |
|
630 \isacommand{bind} x \isacommand{in} t$_1$ t$_2$\\ |
|
631 \end{tabular}} |
|
632 \only<2>{ |
|
633 \begin{tabular}{@ {\hspace{-5mm}}l} |
|
634 \alert{\bf deep binders} \\ |
|
635 \hspace{4mm}Let as::assns t::trm\hspace{4mm} \isacommand{bind} bn(as) \isacommand{in} t\\ |
|
636 \hspace{4mm}Foo as::assns t$_1$::trm t$_2$::trm\\ |
|
637 \hspace{20mm}\isacommand{bind} bn(as) \isacommand{in} t$_1$, \isacommand{bind} bn(as) \isacommand{in} t$_2$\\[4mm] |
|
638 \makebox[0mm][l]{\alert{$\times$}}\hspace{4mm}Bar as::assns t$_1$::trm t$_2$::trm\\ |
|
639 \hspace{20mm}\isacommand{bind} bn$_1$(as) \isacommand{in} t$_1$, \isacommand{bind} bn$_2$(as) \isacommand{in} t$_2$\\ |
|
640 \end{tabular}} |
|
641 \only<3>{ |
|
642 \begin{tabular}{@ {\hspace{-5mm}}l} |
|
643 {\bf deep \alert{recursive} binders} \\ |
|
644 \hspace{4mm}Let\_rec as::assns t::trm\hspace{4mm} \isacommand{bind} bn(as) \isacommand{in} t as\\[4mm] |
|
645 |
|
646 \makebox[0mm][l]{\alert{$\times$}}\hspace{4mm}Foo\_rec as::assns t$_1$::trm t$_2$::trm\hspace{4mm}\\ |
|
647 \hspace{20mm}\isacommand{bind} bn(as) \isacommand{in} t$_1$ as, \isacommand{bind} bn(as) \isacommand{in} t$_2$\\ |
|
648 |
|
649 \end{tabular}} |
|
650 \end{center} |
|
651 |
|
652 \end{frame}} |
|
653 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
654 *} |
|
655 |
|
656 text_raw {* |
|
657 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
658 \mode<presentation>{ |
|
659 \begin{frame}<2-5> |
|
660 \frametitle{\begin{tabular}{c}Our Work\end{tabular}} |
|
661 \mbox{}\\[-6mm] |
|
662 |
|
663 \begin{center} |
|
664 \begin{tikzpicture}[scale=1.5] |
|
665 %%%\draw[step=2mm] (-4,-1) grid (4,1); |
|
666 |
|
667 \onslide<1>{\draw[very thick] (0.7,0.4) circle (4.25mm);} |
|
668 \onslide<1>{\draw[rounded corners=1mm, very thick] ( 0.0,-0.8) rectangle ( 1.8, 0.9);} |
|
669 \onslide<1->{\draw[rounded corners=1mm, very thick] (-1.95,0.85) rectangle (-2.85,-0.05);} |
|
670 |
|
671 \onslide<1>{\draw (-2.0, 0.845) -- (0.7,0.845);} |
|
672 \onslide<1>{\draw (-2.0,-0.045) -- (0.7,-0.045);} |
|
673 |
|
674 \onslide<1>{\alert{\draw ( 0.7, 0.4) node {\footnotesize\begin{tabular}{@ {}c@ {}}$\alpha$-\\[-1mm]classes\end{tabular}};}} |
|
675 \onslide<1->{\alert{\draw (-2.4, 0.4) node {\footnotesize\begin{tabular}{@ {}c@ {}}$\alpha$-eq.\\[-1mm]terms\end{tabular}};}} |
|
676 \onslide<1>{\draw (1.8, 0.48) node[right=-0.1mm] |
|
677 {\footnotesize\begin{tabular}{@ {}l@ {}}existing\\[-1mm] type\\ \onslide<1>{\alert{(sets of raw terms)}}\end{tabular}};} |
|
678 \onslide<1>{\draw (0.9, -0.35) node {\footnotesize\begin{tabular}{@ {}l@ {}}non-empty\\[-1mm]subset\end{tabular}};} |
|
679 \onslide<1->{\draw (-3.25, 0.55) node {\footnotesize\begin{tabular}{@ {}l@ {}}new\\[-1mm]type\end{tabular}};} |
|
680 |
|
681 \onslide<1>{\draw[<->, very thick] (-1.8, 0.3) -- (-0.1,0.3);} |
|
682 \onslide<1>{\draw (-0.95, 0.3) node[above=0mm] {\footnotesize{}isomorphism};} |
|
683 |
|
684 \onslide<1>{\draw[->, line width=2mm, red] (-1.0,-0.4) -- (0.35,0.16);} |
|
685 \end{tikzpicture} |
|
686 \end{center} |
|
687 |
|
688 \begin{textblock}{9.5}(6,3.5) |
|
689 \begin{itemize} |
|
690 \item<1-> defined fv and $\alpha$ |
|
691 \item<3-> derived a reasoning infrastructure ($\fresh$, distinctness, injectivity, cases,\ldots) |
|
692 \item<4-> a (weak) induction principle |
|
693 \item<5-> derive a {\bf stronger} induction principle (Barendregt variable convention built in)\\ |
|
694 \begin{center} |
|
695 \textcolor{blue}{Foo ($\lambda x. \lambda y. t$) ($\lambda u. \lambda v. s$)} |
|
696 \end{center} |
|
697 \end{itemize} |
|
698 \end{textblock} |
|
699 |
|
700 |
|
701 \end{frame}} |
|
702 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
703 *} |
|
704 |
|
705 |
|
706 text_raw {* |
|
707 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
708 \mode<presentation>{ |
|
709 \begin{frame}<1-> |
|
710 \frametitle{\begin{tabular}{c}Conclusion\end{tabular}} |
|
711 \mbox{}\\[-6mm] |
|
712 |
|
713 \begin{itemize} |
|
714 \item the user does not see anything of the raw level\medskip |
|
715 \only<1>{\begin{center} |
|
716 Lam a (Var a) \alert{$=$} Lam b (Var b) |
|
717 \end{center}\bigskip} |
|
718 |
|
719 \item<2-> it took quite some time to get here, but it seems worthwhile |
|
720 (Barendregt's variable convention is unsound in general, |
|
721 found bugs in two paper proofs)\bigskip\medskip |
|
722 |
|
723 \item<3-> \textcolor{blue}{http://isabelle.in.tum.de/nominal/} |
|
724 \end{itemize} |
|
725 |
|
726 |
|
727 \end{frame}} |
|
728 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
729 *} |
|
730 |
|
731 |
|
732 |
|
733 text_raw {* |
|
734 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
735 \mode<presentation>{ |
|
736 \begin{frame}<1->[c] |
|
737 \frametitle{\begin{tabular}{c}Questions?\end{tabular}} |
|
738 \mbox{}\\[-6mm] |
|
739 |
|
740 \begin{center} |
|
741 \alert{\huge{Thanks!}} |
|
742 \end{center} |
|
743 |
|
744 \end{frame}} |
|
745 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
746 *} |
|
747 |
|
748 |
|
749 |
|
750 text_raw {* |
|
751 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
752 \mode<presentation>{ |
|
753 \begin{frame}<1-2>[c] |
|
754 \frametitle{\begin{tabular}{c}Examples\end{tabular}} |
|
755 \mbox{}\\[-6mm] |
|
756 |
|
757 \textcolor{blue}{ |
|
758 \begin{center} |
|
759 $(\{a,b\}, a \rightarrow b) \approx_\alpha (\{a, b\}, a \rightarrow b)$ |
|
760 $(\{a,b\}, a \rightarrow b) \approx_\alpha (\{a, b\}, b \rightarrow a)$ |
|
761 \end{center}} |
|
762 |
|
763 \textcolor{blue}{ |
|
764 \begin{center} |
|
765 $(\{a,b\}, (a \rightarrow b, a \rightarrow b))$\\ |
|
766 \hspace{17mm}$\not\approx_\alpha (\{a, b\}, (a \rightarrow b, b \rightarrow a))$ |
|
767 \end{center}} |
|
768 |
|
769 \onslide<2-> |
|
770 {1.) \hspace{3mm}\isacommand{bind (set)} as \isacommand{in} $\tau_1$, |
|
771 \isacommand{bind (set)} as \isacommand{in} $\tau_2$\medskip |
|
772 |
|
773 2.) \hspace{3mm}\isacommand{bind (set)} as \isacommand{in} $\tau_1$ $\tau_2$ |
|
774 } |
|
775 |
|
776 \end{frame}} |
|
777 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
778 *} |
|
779 |
|
780 |
|
781 |
|
782 (*<*) |
|
783 end |
|
784 (*>*) |
|