nominal2: comparison Slides/Slides2.thy

equal deleted inserted replaced

-:ac064c47138b
+:e2be455093a1
 \end{center}}
 \end{itemize}
 \only<3>{
 \begin{textblock}{14}(1,12.5)
-\alert{The big benefit:} the type system takes care of the sort-respecting part.
+\alert{The big benefit:} the type system takes care of the sort-respecting requirement.
 \end{textblock}}
 \only<4>{
 \begin{textblock}{14}(1,12.5)
 \alert{A small benefit:} permutation composition is \alert{list append}
 and permutation inversion is \alert{list reversal}.
 {\normalsize\color{darkgray}
 \begin{quote}
 \begin{itemize}
 \item \alert{lots} of ML-code
 \item \alert{not} pretty
-\item \alert{not a proof pearl} :o(
+\item \alert{not a {\bf proof pearl}} :o(
 \end{itemize}
 \end{quote}};
 \end{tikzpicture}
 \end{textblock}}
 \begin{itemize}
 \item sort-respecting \hspace{5mm}($\,\forall a.\;\text{sort}(\pi a) = \text{sort}(a)$)
 \item finite domain \hspace{5mm}($\text{finite} \{a.\;\pi a \not= a\}$)
 \end{itemize}\medskip
-\item<4-> \alert{What about swappings?}
+\item<4-> \alert{What about {\bf swappings}?}
 \small
 \[
 \begin{array}{l@ {\hspace{1mm}}l}
 (a\;b) \dn & \text{if}\;\text{sort}(a) = \text{sort}(b)\\
 & \text{then}\;\lambda  c. \text{if}\;a = c\;\text{then}\;b\;\text{else}\;
 \]
 \end{itemize}
 \only<3>{
 \begin{textblock}{7}(4,11)
-@{text "\<pi> \<bullet> _ :: perm \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}
+@{text "_ \<bullet> _ :: perm \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}
 \end{textblock}}
 \end{frame}}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 *}
 \begin{itemize}
 \item $0\;\act\;x = x$\\
 \item $(\pi_1 + \pi_2)\;\act\;x = \pi_1\;\act\;(\pi_2\;\act\;x)$
 \end{itemize}\medskip
-\onslide<7->{\alert{$\;\mapsto\;$}only one type class, $\text{finite}(\text{supp}\;x)$, $\forall \pi. P$}
+\onslide<7->{\alert{$\;\mapsto\;$}only one type class needed, $\text{finite}(\text{supp}\;x)$,\\
+\hspace{9mm}$\forall \pi. P$}
 \end{itemize}
 \only<5>{
 \begin{textblock}{6}(2.5,11)
 \begin{tikzpicture}
 *}
 text_raw {*
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \mode<presentation>{
-\begin{frame}<1-3>
+\begin{frame}<1>[c]
 \frametitle{One Snatch}
+*}
+datatype \<iota>atom = \<iota>Atom string nat
+text_raw {*
+\isanewline\isanewline
+\begin{itemize}
+\item You like to get the advantages of the old way back: you
+\alert{cannot mix} atoms of dif$\!$ferent sort:\bigskip
+\small
+e.g.~LF-objects:
+\begin{center}
+$\quad M ::= c \mid x \mid \lambda x\!:\!A. M \mid M_1\;M_2$
+\end{center}
+\end{itemize}
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+text_raw {*
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}<1-2>
+\frametitle{Solution}
 \begin{itemize}
 \item \underline{concrete} atoms:
 \end{itemize}
 typedef ident = "{a :: atom. sort a = ''ident''}" (*<*)sorry(*>*)
 text_raw {*
 \mbox{}\bigskip\bigskip
 \begin{itemize}
-\item<2-> there is an overloaded  function \alert{\bf atom}, which injects concrete
+\item they are a ``subtype'' of the generic atom type
+\item there is an overloaded  function \alert{\bf atom}, which injects concrete
 atoms into generic ones\medskip
 \begin{center}
 \begin{tabular}{l}
 $\text{atom}(a) \fresh x$\\
 $(a \leftrightarrow b) \dn (\text{atom}(a)\;\;\text{atom}(b))$
 \end{tabular}
-\end{center}\bigskip\medskip
-\onslide<3->
-{One would like to have $a \fresh x$, $(a\; b)$, \ldots}
-\end{itemize}
-\only<1>{
-\begin{textblock}{11}(2.5,8.5)
-You like to get the advantages of the old way back: you \alert{cannot mix} atoms
-of dif$\!$ferent sort:\bigskip
-\small
-e.g.~LF-objects:\\[-9mm]\mbox{}
-\begin{center}$\quad M ::= c \mid x \mid \lambda x\!:\!A. M \mid M_1\;M_2$
 \end{center}
-\end{textblock}}
+\pause
+One would like to have $a \fresh x$, $\swap{a}{b}$, \ldots
+\end{itemize}
 \end{frame}}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 *}
 *}
 text_raw {*
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \mode<presentation>{
-\begin{frame}<1-3>
+\begin{frame}<1-2>
 \frametitle{Non-Working Solution}
 Instead of\isanewline\isanewline
 *}
 datatype atom\<iota>\<iota> = Atom\<iota>\<iota> string nat
 \isanewline\isanewline
 have
 \isanewline\isanewline
 *}
-datatype 'a atom\<iota>\<iota>\<iota> = Atom\<iota>\<iota> 'a nat
+datatype 'a atom\<iota>\<iota>\<iota> = Atom\<iota>\<iota>\<iota> 'a nat
 text_raw {*
 \pause
 \isanewline\isanewline
 But then
 \begin{center}
 \end{center}
 \end{frame}}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 *}
-text_raw {*
+(*<*)
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+hide_const sort
-\mode<presentation>{
+(*>*)
-\begin{frame}<1-3>
+text_raw {*
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}<1-4>
 \frametitle{A Working Solution}
 *}
 datatype sort = Sort string "sort list"
-datatype atom\<iota>\<iota> = Atom\<iota>\<iota> string nat
+datatype atom\<iota>\<iota>\<iota>\<iota> = Atom\<iota>\<iota>\<iota>\<iota> sort nat
+(*<*)
-text_raw {*
+consts sort_ty :: "nat \<Rightarrow> sort"
-\isanewline\isanewline
+(*>*)
-have
+text_raw {*
-\isanewline\isanewline
+\pause
-*}
+\isanewline
-datatype 'a atom\<iota>\<iota>\<iota> = Atom\<iota>\<iota> 'a nat
+{\small\begin{tabular}{rcl}
-text_raw {*
+@{text "sort_ty (TVar x)"}  & @{text "\<equiv>"} & @{text "Sort ''TVar'' [Sort x []]"} \\
-\pause
+@{text "sort_ty (\<tau>\<^isub>1 \<rightarrow> \<tau>\<^isub>2)"} & @{text "\<equiv>"} & @{text "Sort ''Fun'' [sort_ty \<tau>\<^isub>1, sort_ty \<tau>\<^isub>2]"}\\
-\isanewline\isanewline
+\end{tabular}}
-But then
+\pause
-\begin{center}
+\isanewline\isanewline
-@{text "_ \<bullet> _ :: \<alpha> perm \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}
+\isacommand{typedef} @{text "var = {a :: atom. sort a \<in> range sort_ty}"}
-\end{center}
+\pause
-\end{frame}}
+\isanewline\isanewline
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\small
-*}
+\begin{minipage}{12cm}
+@{text "Var x \<tau> \<equiv> \<lceil> Atom (sort_ty \<tau>) x \<rceil>"}\isanewline
-text_raw {*
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+@{text "(Var x \<tau> \<leftrightarrow> Var y \<tau>) \<bullet> Var x \<tau> = Var y \<tau>"}\\
-\mode<presentation>{
+@{text "(Var x \<tau> \<leftrightarrow> Var y \<tau>) \<bullet> Var x \<tau>' = Var x \<tau>'"}\\
-\begin{frame}<1-2>[c]
+\end{minipage}
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+text_raw {*
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}<1-4>[c]
 \frametitle{Conclusion}
 \mbox{}\\[-3mm]
 \begin{itemize}
 \item the formalised version of the nominal theory is now much nicer to
-work with (sorts are occasionally explicit)\bigskip
+work with (sorts are occasionally explicit, \alert{@{text "\<forall>\<pi>. P"}})\medskip
-\item permutations: ``be as abstract as you can'' (group\_add is a slight oddity)\bigskip
+\item permutations: ``be as abstract as you can'' (group\_add is a slight oddity)\medskip
-\item allow sort-disrespecting swappings\onslide<2->{: just define them as the identity}
+\item crucial insight: allow sort-disrespecting swappings%
-\end{itemize}
+\onslide<2->{ just define them as the identity}%
+\onslide<3->{ (a referee called this a \alert{``hack''})}\medskip
+\item<4-> there will be a hands-on tutorial about Nominal Isabelle at \alert{POPL'11}
+in Austin Texas
+\end{itemize}
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+text_raw {*
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}<1>[c]
+\frametitle{
+\begin{tabular}{c}
+\mbox{}\\[23mm]
+\alert{\LARGE Thank you very much}\\
+\alert{\Large Questions?}
+\end{tabular}}
 \end{frame}}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 *}

changeset 2354	e2be455093a1
parent 2353	ac064c47138b
child 2355	b38f8d5e0b09