equal
deleted
inserted
replaced
9 |
9 |
10 (*>*) |
10 (*>*) |
11 |
11 |
12 |
12 |
13 text_raw {* |
13 text_raw {* |
14 \renewcommand{\slidecaption}{Cambridge, 8.~June 2010} |
14 %%\renewcommand{\slidecaption}{Cambridge, 8.~June 2010} |
|
15 \renewcommand{\slidecaption}{Uppsala, 3.~March 2011} |
15 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
16 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
16 \mode<presentation>{ |
17 \mode<presentation>{ |
17 \begin{frame}<1>[t] |
18 \begin{frame}<1>[t] |
18 \frametitle{% |
19 \frametitle{% |
19 \begin{tabular}{@ {\hspace{-3mm}}c@ {}} |
20 \begin{tabular}{@ {\hspace{-3mm}}c@ {}} |
185 \item the order does matter \textcolor{gray}{(iterated single binders)} |
186 \item the order does matter \textcolor{gray}{(iterated single binders)} |
186 \end{itemize} |
187 \end{itemize} |
187 |
188 |
188 \onslide<2->{ |
189 \onslide<2->{ |
189 \begin{center} |
190 \begin{center} |
190 \isacommand{bind\_res}\hspace{6mm} |
191 \isacommand{bind (set+)}\hspace{6mm} |
191 \isacommand{bind\_set}\hspace{6mm} |
192 \isacommand{bind (set)}\hspace{6mm} |
192 \isacommand{bind} |
193 \isacommand{bind} |
193 \end{center}} |
194 \end{center}} |
194 |
195 |
195 \end{frame}} |
196 \end{frame}} |
196 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
197 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
266 \begin{itemize} |
267 \begin{itemize} |
267 \item we allow multiple ``binders'' and ``bodies''\smallskip |
268 \item we allow multiple ``binders'' and ``bodies''\smallskip |
268 \begin{center} |
269 \begin{center} |
269 \begin{tabular}{l} |
270 \begin{tabular}{l} |
270 \isacommand{bind} a b c \ldots \isacommand{in} x y z \ldots\\ |
271 \isacommand{bind} a b c \ldots \isacommand{in} x y z \ldots\\ |
271 \isacommand{bind\_set} a b c \ldots \isacommand{in} x y z \ldots\\ |
272 \isacommand{bind (set)} a b c \ldots \isacommand{in} x y z \ldots\\ |
272 \isacommand{bind\_res} a b c \ldots \isacommand{in} x y z \ldots |
273 \isacommand{bind (set+)} a b c \ldots \isacommand{in} x y z \ldots |
273 \end{tabular} |
274 \end{tabular} |
274 \end{center}\bigskip\medskip |
275 \end{center}\bigskip\medskip |
275 the reason is that with our definition of $\alpha$-equivalence\medskip |
276 the reason is that with our definition of $\alpha$-equivalence\medskip |
276 \begin{center} |
277 \begin{center} |
277 \begin{tabular}{l} |
278 \begin{tabular}{l} |
278 \isacommand{bind\_res} as \isacommand{in} x y $\not\Leftrightarrow$\\ |
279 \isacommand{bind (set+)} as \isacommand{in} x y $\not\Leftrightarrow$\\ |
279 \hspace{8mm}\isacommand{bind\_res} as \isacommand{in} x, \isacommand{bind\_res} as \isacommand{in} y |
280 \hspace{8mm}\isacommand{bind (set+)} as \isacommand{in} x, \isacommand{bind (set+)} as \isacommand{in} y |
280 \end{tabular} |
281 \end{tabular} |
281 \end{center}\medskip |
282 \end{center}\medskip |
282 |
283 |
283 same with \isacommand{bind\_set} |
284 same with \isacommand{bind (set)} |
284 \end{itemize}} |
285 \end{itemize}} |
285 \end{itemize} |
286 \end{itemize} |
286 |
287 |
287 |
288 |
288 \end{frame}} |
289 \end{frame}} |
372 \item lets first look at pairs\bigskip\medskip |
373 \item lets first look at pairs\bigskip\medskip |
373 |
374 |
374 \begin{tabular}{@ {\hspace{1cm}}l} |
375 \begin{tabular}{@ {\hspace{1cm}}l} |
375 $(as, x) \onslide<2->{\approx\!}\makebox[0mm][l]{\only<2-6>{${}_{\text{set}}$}% |
376 $(as, x) \onslide<2->{\approx\!}\makebox[0mm][l]{\only<2-6>{${}_{\text{set}}$}% |
376 \only<7>{${}_{\text{\alert{list}}}$}% |
377 \only<7>{${}_{\text{\alert{list}}}$}% |
377 \only<8>{${}_{\text{\alert{res}}}$}}% |
378 \only<8>{${}_{\text{\alert{set+}}}$}}% |
378 \onslide<3->{^{R,\text{fv}}}\,\onslide<2->{(bs,y)}$ |
379 \onslide<3->{^{R,\text{fv}}}\,\onslide<2->{(bs,y)}$ |
379 \end{tabular}\bigskip |
380 \end{tabular}\bigskip |
380 \end{itemize} |
381 \end{itemize} |
381 |
382 |
382 \only<1>{ |
383 \only<1>{ |
436 \begin{tikzpicture} |
437 \begin{tikzpicture} |
437 \draw (0,0) node[inner sep=1mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] |
438 \draw (0,0) node[inner sep=1mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] |
438 {\tiny\color{darkgray} |
439 {\tiny\color{darkgray} |
439 \begin{minipage}{3.4cm}\raggedright |
440 \begin{minipage}{3.4cm}\raggedright |
440 \begin{tabular}{r@ {\hspace{1mm}}l} |
441 \begin{tabular}{r@ {\hspace{1mm}}l} |
441 \multicolumn{2}{@ {}l}{res:}\\ |
442 \multicolumn{2}{@ {}l}{set+:}\\ |
442 $\exists\pi.$ & $\text{fv}(x) - as = \text{fv}(y) - bs$\\ |
443 $\exists\pi.$ & $\text{fv}(x) - as = \text{fv}(y) - bs$\\ |
443 $\wedge$ & $\text{fv}(x) - as \fresh^* \pi$\\ |
444 $\wedge$ & $\text{fv}(x) - as \fresh^* \pi$\\ |
444 $\wedge$ & $\pi \cdot x = y$\\ |
445 $\wedge$ & $\pi \cdot x = y$\\ |
445 \\ |
446 \\ |
446 \end{tabular} |
447 \end{tabular} |
495 \only<1>{$(\{x, y\}, x \rightarrow y) \approx_? (\{x, y\}, y \rightarrow x)$} |
496 \only<1>{$(\{x, y\}, x \rightarrow y) \approx_? (\{x, y\}, y \rightarrow x)$} |
496 \only<2>{$([x, y], x \rightarrow y) \approx_? ([x, y], y \rightarrow x)$} |
497 \only<2>{$([x, y], x \rightarrow y) \approx_? ([x, y], y \rightarrow x)$} |
497 \end{center} |
498 \end{center} |
498 |
499 |
499 \begin{itemize} |
500 \begin{itemize} |
500 \item $\approx_{\text{res}}$, $\approx_{\text{set}}$% |
501 \item $\approx_{\text{set+}}$, $\approx_{\text{set}}$% |
501 \only<2>{, \alert{$\not\approx_{\text{list}}$}} |
502 \only<2>{, \alert{$\not\approx_{\text{list}}$}} |
502 \end{itemize} |
503 \end{itemize} |
503 |
504 |
504 |
505 |
505 \only<1->{ |
506 \only<1->{ |
507 \begin{tikzpicture} |
508 \begin{tikzpicture} |
508 \draw (0,0) node[inner sep=1mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] |
509 \draw (0,0) node[inner sep=1mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] |
509 {\tiny\color{darkgray} |
510 {\tiny\color{darkgray} |
510 \begin{minipage}{3.4cm}\raggedright |
511 \begin{minipage}{3.4cm}\raggedright |
511 \begin{tabular}{r@ {\hspace{1mm}}l} |
512 \begin{tabular}{r@ {\hspace{1mm}}l} |
512 \multicolumn{2}{@ {}l}{res:}\\ |
513 \multicolumn{2}{@ {}l}{set+:}\\ |
513 $\exists\pi.$ & $\text{fv}(x) - as = \text{fv}(y) - bs$\\ |
514 $\exists\pi.$ & $\text{fv}(x) - as = \text{fv}(y) - bs$\\ |
514 $\wedge$ & $\text{fv}(x) - as \fresh^* \pi$\\ |
515 $\wedge$ & $\text{fv}(x) - as \fresh^* \pi$\\ |
515 $\wedge$ & $\pi \cdot x = y$\\ |
516 $\wedge$ & $\pi \cdot x = y$\\ |
516 \\ |
517 \\ |
517 \end{tabular} |
518 \end{tabular} |
565 \begin{center} |
566 \begin{center} |
566 \only<1>{$(\{x\}, x) \approx_? (\{x, y\}, x)$} |
567 \only<1>{$(\{x\}, x) \approx_? (\{x, y\}, x)$} |
567 \end{center} |
568 \end{center} |
568 |
569 |
569 \begin{itemize} |
570 \begin{itemize} |
570 \item $\approx_{\text{res}}$, $\not\approx_{\text{set}}$, |
571 \item $\approx_{\text{set+}}$, $\not\approx_{\text{set}}$, |
571 $\not\approx_{\text{list}}$ |
572 $\not\approx_{\text{list}}$ |
572 \end{itemize} |
573 \end{itemize} |
573 |
574 |
574 |
575 |
575 \only<1->{ |
576 \only<1->{ |
577 \begin{tikzpicture} |
578 \begin{tikzpicture} |
578 \draw (0,0) node[inner sep=1mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] |
579 \draw (0,0) node[inner sep=1mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] |
579 {\tiny\color{darkgray} |
580 {\tiny\color{darkgray} |
580 \begin{minipage}{3.4cm}\raggedright |
581 \begin{minipage}{3.4cm}\raggedright |
581 \begin{tabular}{r@ {\hspace{1mm}}l} |
582 \begin{tabular}{r@ {\hspace{1mm}}l} |
582 \multicolumn{2}{@ {}l}{res:}\\ |
583 \multicolumn{2}{@ {}l}{set+:}\\ |
583 $\exists\pi.$ & $\text{fv}(x) - as = \text{fv}(y) - bs$\\ |
584 $\exists\pi.$ & $\text{fv}(x) - as = \text{fv}(y) - bs$\\ |
584 $\wedge$ & $\text{fv}(x) - as \fresh^* \pi$\\ |
585 $\wedge$ & $\text{fv}(x) - as \fresh^* \pi$\\ |
585 $\wedge$ & $\pi \cdot x = y$\\ |
586 $\wedge$ & $\pi \cdot x = y$\\ |
586 \\ |
587 \\ |
587 \end{tabular} |
588 \end{tabular} |
666 \end{center} |
667 \end{center} |
667 \end{itemize} |
668 \end{itemize} |
668 |
669 |
669 \only<1->{ |
670 \only<1->{ |
670 \begin{textblock}{8}(12,3.8) |
671 \begin{textblock}{8}(12,3.8) |
671 \footnotesize $^*$ set, res, list |
672 \footnotesize $^*$ set, set+, list |
672 \end{textblock}} |
673 \end{textblock}} |
673 |
674 |
674 \end{frame}} |
675 \end{frame}} |
675 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
676 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
676 *} |
677 *} |
881 |
882 |
882 \[\mbox{}\hspace{-4mm} |
883 \[\mbox{}\hspace{-4mm} |
883 \infer[\text{LetRec-}\!\approx_\alpha] |
884 \infer[\text{LetRec-}\!\approx_\alpha] |
884 {\text{LetRec}\;as\;t \approx_\alpha \text{LetRec}\;as'\;t'} |
885 {\text{LetRec}\;as\;t \approx_\alpha \text{LetRec}\;as'\;t'} |
885 {(\text{bn}(as), (t, as)) \approx\!\makebox[0mm][l]{${}_{\text{list}}$} |
886 {(\text{bn}(as), (t, as)) \approx\!\makebox[0mm][l]{${}_{\text{list}}$} |
886 ^{R,fv} (\text{bn}(as'), (t', as'))} |
887 ^{R,\text{fv}} (\text{bn}(as'), (t', as'))} |
887 \]\bigskip |
888 \]\bigskip |
888 |
889 |
889 \onslide<1->{\alert{deep recursive binders}} |
890 \onslide<1->{\alert{deep recursive binders}} |
890 \end{frame}} |
891 \end{frame}} |
891 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
892 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
931 \only<2>{[x].t = [x'].t'}} |
932 \only<2>{[x].t = [x'].t'}} |
932 \] |
933 \] |
933 |
934 |
934 |
935 |
935 \item the properties for support are implied by the properties of $[\_].\_$ |
936 \item the properties for support are implied by the properties of $[\_].\_$ |
936 \item we can derive strong induction principles (almost automatic---matter of time) |
937 \item we can derive strong induction principles |
937 \end{itemize} |
938 \end{itemize} |
938 |
939 |
939 |
940 |
940 \end{frame}} |
941 \end{frame}} |
941 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
942 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
979 \end{center} |
980 \end{center} |
980 |
981 |
981 \begin{itemize} |
982 \begin{itemize} |
982 \item Core Haskell: 11 types, 49 term-constructors, 7 binding functions |
983 \item Core Haskell: 11 types, 49 term-constructors, 7 binding functions |
983 \begin{center} |
984 \begin{center} |
984 $\sim$ 1 min |
985 $\sim$ 2 mins |
985 \end{center} |
986 \end{center} |
986 \end{itemize} |
987 \end{itemize} |
987 |
988 |
988 \end{frame}} |
989 \end{frame}} |
989 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
990 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
1057 |
1058 |
1058 text_raw {* |
1059 text_raw {* |
1059 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
1060 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
1060 \mode<presentation>{ |
1061 \mode<presentation>{ |
1061 \begin{frame}<1->[c] |
1062 \begin{frame}<1->[c] |
|
1063 \frametitle{\begin{tabular}{c}Future Work\end{tabular}} |
|
1064 \mbox{}\\[-6mm] |
|
1065 |
|
1066 \begin{itemize} |
|
1067 \item Function definitions |
|
1068 \end{itemize} |
|
1069 |
|
1070 \end{frame}} |
|
1071 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1072 *} |
|
1073 |
|
1074 |
|
1075 text_raw {* |
|
1076 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
1077 \mode<presentation>{ |
|
1078 \begin{frame}<1->[c] |
1062 \frametitle{\begin{tabular}{c}Questions?\end{tabular}} |
1079 \frametitle{\begin{tabular}{c}Questions?\end{tabular}} |
1063 \mbox{}\\[-6mm] |
1080 \mbox{}\\[-6mm] |
1064 |
1081 |
1065 \begin{center} |
1082 \begin{center} |
1066 \alert{\huge{Thanks!}} |
1083 \alert{\huge{Thanks!}} |
1067 \end{center} |
1084 \end{center} |
1068 |
1085 |
1069 \end{frame}} |
1086 \end{frame}} |
1070 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
1087 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
1071 *} |
1088 *} |
|
1089 |
|
1090 |
1072 |
1091 |
1073 text_raw {* |
1092 text_raw {* |
1074 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
1093 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
1075 \mode<presentation>{ |
1094 \mode<presentation>{ |
1076 \begin{frame}<1-2>[c] |
1095 \begin{frame}<1-2>[c] |
1086 $(\{a,b\}, (a \rightarrow b, a \rightarrow b))$\\ |
1105 $(\{a,b\}, (a \rightarrow b, a \rightarrow b))$\\ |
1087 \hspace{17mm}$\not\approx_\alpha (\{a, b\}, (a \rightarrow b, b \rightarrow a))$ |
1106 \hspace{17mm}$\not\approx_\alpha (\{a, b\}, (a \rightarrow b, b \rightarrow a))$ |
1088 \end{center} |
1107 \end{center} |
1089 |
1108 |
1090 \onslide<2-> |
1109 \onslide<2-> |
1091 {1.) \hspace{3mm}\isacommand{bind\_set} as \isacommand{in} $\tau_1$, |
1110 {1.) \hspace{3mm}\isacommand{bind (set)} as \isacommand{in} $\tau_1$, |
1092 \isacommand{bind\_set} as \isacommand{in} $\tau_2$\medskip |
1111 \isacommand{bind (set)} as \isacommand{in} $\tau_2$\medskip |
1093 |
1112 |
1094 2.) \hspace{3mm}\isacommand{bind\_set} as \isacommand{in} $\tau_1$ $\tau_2$ |
1113 2.) \hspace{3mm}\isacommand{bind (set)} as \isacommand{in} $\tau_1$ $\tau_2$ |
1095 } |
1114 } |
1096 |
1115 |
1097 \end{frame}} |
1116 \end{frame}} |
1098 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
1117 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
1099 *} |
1118 *} |