42 |
42 |
43 \item \ldots provides a convenient reasoning infrastructure for |
43 \item \ldots provides a convenient reasoning infrastructure for |
44 terms involving binders (e.g.~lambda calculus, variable convention)\medskip |
44 terms involving binders (e.g.~lambda calculus, variable convention)\medskip |
45 |
45 |
46 \item<2-> \ldots mainly used to find errors in my own |
46 \item<2-> \ldots mainly used to find errors in my own |
47 (published) paper proofs and in that of others \alert{\bf ;o)} |
47 (published) paper proofs and in those of others \alert{\bf ;o)} |
48 \end{itemize} |
48 \end{itemize} |
49 |
49 |
50 \end{frame}} |
50 \end{frame}} |
51 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
51 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
52 *} |
52 *} |
55 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
55 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
56 \mode<presentation>{ |
56 \mode<presentation>{ |
57 \begin{frame}<1-3>[c] |
57 \begin{frame}<1-3>[c] |
58 \frametitle{Nominal Theory} |
58 \frametitle{Nominal Theory} |
59 |
59 |
60 by Pitts; at its core are:\bigskip |
60 \ldots by Pitts; at its core are:\bigskip |
61 |
61 |
62 \begin{itemize} |
62 \begin{itemize} |
63 \item sorted atoms and |
63 \item sorted atoms and |
64 \item sort-respecting permutations |
64 \item sort-respecting permutations |
65 \end{itemize} |
65 \end{itemize} |
135 \onslide<3>{\small\hspace{5mm}can only have \alert{\bf one} type parameter} |
135 \onslide<3>{\small\hspace{5mm}can only have \alert{\bf one} type parameter} |
136 \begin{itemize} |
136 \begin{itemize} |
137 \item<2-> $\text{[]}\,\act\, x = x$ |
137 \item<2-> $\text{[]}\,\act\, x = x$ |
138 \item<2-> $(\pi_1 @ \pi_2) \,\act \, x = \pi_1 \,\act\,(\pi_2 \,\act\, x)$ |
138 \item<2-> $(\pi_1 @ \pi_2) \,\act \, x = \pi_1 \,\act\,(\pi_2 \,\act\, x)$ |
139 \item<2-> if $\pi_1 \sim \pi_2$ then $\pi_1 \,\act\, x = \pi_2 \,\act\, x$ |
139 \item<2-> if $\pi_1 \sim \pi_2$ then $\pi_1 \,\act\, x = \pi_2 \,\act\, x$ |
|
140 \item<2-> if $\pi_1$, $\pi_2$ have dif$\!$f.~type, then |
|
141 $\pi_1 \act (\pi_2 \act x) = \pi_2 \act (\pi_1 \act x)$ |
140 \end{itemize} |
142 \end{itemize} |
141 \end{itemize} |
143 \end{itemize} |
142 |
144 |
143 \only<4->{ |
145 \only<4->{ |
144 \begin{textblock}{9}(3,7)\begin{tikzpicture} |
146 \begin{textblock}{9}(3,7)\begin{tikzpicture} |
159 *} |
161 *} |
160 |
162 |
161 text_raw {* |
163 text_raw {* |
162 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
164 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
163 \mode<presentation>{ |
165 \mode<presentation>{ |
164 \begin{frame}<1-5> |
166 \begin{frame}<1-4> |
165 \frametitle{A Better Way} |
167 \frametitle{A Better Way} |
166 *} |
168 *} |
167 datatype atom = Atom string nat |
169 datatype atom = Atom string nat |
168 |
170 |
169 text_raw {* |
171 text_raw {* |
170 \mbox{}\bigskip |
172 \mbox{}\bigskip |
171 \begin{itemize} |
173 \begin{itemize} |
172 \item<3-> permutations are (restricted) bijective functions from @{text "atom \<Rightarrow> atom"} |
174 \item<2-> permutations are (restricted) bijective functions from @{text "atom \<Rightarrow> atom"} |
173 |
175 |
174 \begin{itemize} |
176 \begin{itemize} |
175 \item sort-respecting \hspace{5mm}($\,\forall a.\;\text{sort}(\pi a) = \text{sort}(a)$) |
177 \item sort-respecting \hspace{5mm}($\,\forall a.\;\text{sort}(\pi a) = \text{sort}(a)$) |
176 \item finite domain \hspace{5mm}($\text{finite} \{a.\;\pi a \not= a\}$) |
178 \item finite domain \hspace{5mm}($\text{finite} \{a.\;\pi a \not= a\}$) |
177 \end{itemize}\medskip |
179 \end{itemize}\medskip |
178 |
180 |
179 \item<4-> \alert{What about {\bf swappings}?} |
181 \item<3-> \alert{What about {\bf swappings}?} |
180 \small |
182 \small |
181 \[ |
183 \[ |
182 \begin{array}{l@ {\hspace{1mm}}l} |
184 \begin{array}{l@ {\hspace{1mm}}l} |
183 (a\;b) \dn & \text{if}\;\text{sort}(a) = \text{sort}(b)\\ |
185 (a\;b) \dn & \text{if}\;\text{sort}(a) = \text{sort}(b)\\ |
184 & \text{then}\;\lambda c. \text{if}\;a = c\;\text{then}\;b\;\text{else}\; |
186 & \text{then}\;\lambda c. \text{if}\;a = c\;\text{then}\;b\;\text{else}\; |
185 \text{if}\;b = c\;\text{then}\;a\;\text{else}\;c\\ |
187 \text{if}\;b = c\;\text{then}\;a\;\text{else}\;c\\ |
186 & \text{else}\;\only<4>{\raisebox{-5mm}{\textcolor{red}{\huge\bf $?$}}} |
188 & \text{else}\;\only<3>{\raisebox{-5mm}{\textcolor{red}{\huge\bf $?$}}} |
187 \only<5->{\text{\alert{\bf id}}} |
189 \only<4->{\text{\alert{\bf id}}} |
188 \end{array} |
190 \end{array} |
189 \] |
191 \] |
190 \end{itemize} |
192 \end{itemize} |
191 |
193 |
192 \only<3>{ |
194 \only<2>{ |
193 \begin{textblock}{7}(4,11) |
195 \begin{textblock}{7}(4,11) |
194 @{text "_ \<bullet> _ :: perm \<Rightarrow> \<beta> \<Rightarrow> \<beta>"} |
196 @{text "_ \<bullet> _ :: perm \<Rightarrow> \<beta> \<Rightarrow> \<beta>"} |
195 \end{textblock}} |
197 \end{textblock}} |
196 |
198 |
197 \end{frame}} |
199 \end{frame}} |
406 \frametitle{Conclusion} |
408 \frametitle{Conclusion} |
407 \mbox{}\\[-3mm] |
409 \mbox{}\\[-3mm] |
408 |
410 |
409 \begin{itemize} |
411 \begin{itemize} |
410 \item the formalised version of the nominal theory is now much nicer to |
412 \item the formalised version of the nominal theory is now much nicer to |
411 work with (sorts are occasionally explicit, \alert{@{text "\<forall>\<pi>. P"}})\medskip |
413 work with (sorts are occasionally explicit, \alert{$\forall \pi. P$})\medskip |
412 |
414 |
413 \item permutations: ``be as abstract as you can'' (group\_add is a slight oddity)\medskip |
415 \item permutations: ``be as abstract as you can'' (group\_add is a slight oddity)\medskip |
414 |
416 |
415 \item crucial insight: allow sort-disrespecting swappings% |
417 \item the crucial insight: allow sort-disrespecting swappings% |
416 \onslide<2->{ just define them as the identity}% |
418 \onslide<2->{ \ldots just define them as the identity}\\% |
417 \onslide<3->{ (a referee called this a \alert{``hack''})}\medskip |
419 \onslide<3->{ (a referee called this a \alert{``hack''})}\medskip |
418 |
420 |
419 \item<4-> there will be a hands-on tutorial about Nominal Isabelle at \alert{POPL'11} |
421 \item<4-> there will be a hands-on tutorial about Nominal Isabelle at \alert{POPL'11} |
420 in Austin Texas |
422 in Austin Texas |
421 \end{itemize} |
423 \end{itemize} |