21 \huge Nominal 2\\[-2mm] |
21 \huge Nominal 2\\[-2mm] |
22 \large Or, How to Reason Conveniently with\\[-5mm] |
22 \large Or, How to Reason Conveniently with\\[-5mm] |
23 \large General Bindings\\[15mm] |
23 \large General Bindings\\[15mm] |
24 \end{tabular}} |
24 \end{tabular}} |
25 \begin{center} |
25 \begin{center} |
26 joint work with {\bf Cezary} and Brian Huffman\\[0mm] |
26 joint work with {\bf Cezary} and Brian Huf\!fman\\[0mm] |
27 \end{center} |
27 \end{center} |
28 \end{frame}} |
28 \end{frame}} |
29 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
29 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
30 |
30 |
31 *} |
31 *} |
32 |
32 |
33 text_raw {* |
33 text_raw {* |
34 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
34 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
35 \mode<presentation>{ |
35 \mode<presentation>{ |
36 \begin{frame}<1> |
36 \begin{frame}<1-2> |
37 \frametitle{\begin{tabular}{c}Part I: Nominal Theory\end{tabular}} |
37 \frametitle{\begin{tabular}{c}Part I: Nominal Theory\end{tabular}} |
38 \mbox{}\\[-3mm] |
38 \mbox{}\\[-3mm] |
39 |
39 |
|
40 \begin{itemize} |
|
41 \item sorted atoms and sort-respecting permutations\medskip |
|
42 |
|
43 \onslide<2->{ |
|
44 \item[] in old Nominal: atoms have dif\!ferent type |
|
45 |
|
46 \begin{center} |
|
47 \begin{tabular}{c@ {\hspace{7mm}}c} |
|
48 $[] \act c \dn c$ & |
|
49 @{text "(a b)::\<pi> \<bullet> c \<equiv>"} |
|
50 $\begin{cases} |
|
51 \mbox{@{text "b"}} & \text{if} \mbox{@{text "\<pi> \<bullet> c = a"}}\\ |
|
52 \mbox{@{text "a"}} & \text{if} \mbox{@{text "\<pi> \<bullet> c = b"}}\\ |
|
53 \mbox{@{text "\<pi> \<bullet> c"}} & \text{otherwise} |
|
54 \end{cases}$ |
|
55 \end{tabular} |
|
56 \end{center}} |
|
57 \end{itemize} |
40 |
58 |
41 \end{frame}} |
59 \end{frame}} |
42 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
60 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
43 *} |
61 *} |
|
62 |
|
63 text_raw {* |
|
64 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
65 \mode<presentation>{ |
|
66 \begin{frame}<1> |
|
67 \frametitle{\begin{tabular}{c}Problems\end{tabular}} |
|
68 \mbox{}\\[-3mm] |
|
69 |
|
70 \begin{itemize} |
|
71 \item $\_ \act \_ :: \alpha perm \Rightarrow \beta \Rightarrow \beta$ |
|
72 |
|
73 \item $supp \_ :: \beta \Rightarrow \alpha set$ |
|
74 |
|
75 \begin{center} |
|
76 $finite (supp x)_{\alpha_1} \ldots finite (supp x)_{\alpha_n}$ |
|
77 \end{center} |
|
78 |
|
79 \item $\forall \pi_{\alpha_1} \ldots \pi_{\alpha_n}\;.\; P$ |
|
80 \end{itemize} |
|
81 |
|
82 \end{frame}} |
|
83 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
84 *} |
|
85 |
44 |
86 |
45 text_raw {* |
87 text_raw {* |
46 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
88 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
47 \mode<presentation>{ |
89 \mode<presentation>{ |
48 \begin{frame}<1>[c] |
90 \begin{frame}<1>[c] |