--- a/Slides/Slides2.thy Sat Jul 10 23:36:45 2010 +0100
+++ b/Slides/Slides2.thy Sun Jul 11 00:58:54 2010 +0100
@@ -100,7 +100,7 @@
\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)
@@ -148,7 +148,7 @@
\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}
@@ -176,7 +176,7 @@
\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}
@@ -191,7 +191,7 @@
\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}}
@@ -219,7 +219,8 @@
\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>{
@@ -241,8 +242,35 @@
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}
@@ -259,30 +287,19 @@
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{center}
+ \pause
+ One would like to have $a \fresh x$, $\swap{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}}
-
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
@@ -317,7 +334,7 @@
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
- \begin{frame}<1-3>
+ \begin{frame}<1-2>
\frametitle{Non-Working Solution}
Instead of\isanewline\isanewline
@@ -330,7 +347,7 @@
\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
@@ -342,30 +359,42 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
+(*<*)
+hide_const sort
+(*>*)
+
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
- \begin{frame}<1-3>
+ \begin{frame}<1-4>
\frametitle{A Working Solution}
*}
datatype sort = Sort string "sort list"
- datatype atom\<iota>\<iota> = Atom\<iota>\<iota> string nat
-
-text_raw {*
-\isanewline\isanewline
-have
-\isanewline\isanewline
-*}
-
- datatype 'a atom\<iota>\<iota>\<iota> = Atom\<iota>\<iota> 'a nat
+ datatype atom\<iota>\<iota>\<iota>\<iota> = Atom\<iota>\<iota>\<iota>\<iota> sort nat
+(*<*)
+consts sort_ty :: "nat \<Rightarrow> sort"
+(*>*)
text_raw {*
\pause
+ \isanewline
+
+ {\small\begin{tabular}{rcl}
+ @{text "sort_ty (TVar x)"} & @{text "\<equiv>"} & @{text "Sort ''TVar'' [Sort x []]"} \\
+ @{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]"}\\
+ \end{tabular}}
+ \pause
\isanewline\isanewline
- But then
- \begin{center}
- @{text "_ \<bullet> _ :: \<alpha> perm \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}
- \end{center}
+ \isacommand{typedef} @{text "var = {a :: atom. sort a \<in> range sort_ty}"}
+ \pause
+ \isanewline\isanewline
+ \small
+ \begin{minipage}{12cm}
+ @{text "Var x \<tau> \<equiv> \<lceil> Atom (sort_ty \<tau>) x \<rceil>"}\isanewline
+
+ @{text "(Var x \<tau> \<leftrightarrow> Var y \<tau>) \<bullet> Var x \<tau> = Var y \<tau>"}\\
+ @{text "(Var x \<tau> \<leftrightarrow> Var y \<tau>) \<bullet> Var x \<tau>' = Var x \<tau>'"}\\
+ \end{minipage}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
@@ -373,17 +402,22 @@
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
- \begin{frame}<1-2>[c]
+ \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)\medskip
- \item permutations: ``be as abstract as you can'' (group\_add is a slight oddity)\bigskip
+ \item crucial insight: allow sort-disrespecting swappings%
+ \onslide<2->{ just define them as the identity}%
+ \onslide<3->{ (a referee called this a \alert{``hack''})}\medskip
- \item allow sort-disrespecting swappings\onslide<2->{: just define them as the identity}
+ \item<4-> there will be a hands-on tutorial about Nominal Isabelle at \alert{POPL'11}
+ in Austin Texas
\end{itemize}
@@ -391,6 +425,21 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
+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}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
(*<*)
end
(*>*)
\ No newline at end of file