1 (*<*)

     2 theory Slides2

     3 imports "~~/src/HOL/Library/LaTeXsugar" "Nominal"

     4 begin

     5 

     6 notation (latex output)

     7   set ("_") and

     8   Cons  ("_::/_" [66,65] 65) 

     9 

    10 (*>*)

    11 

    12 

    13 text_raw {*

    14   \renewcommand{\slidecaption}{Edinburgh, 11.~July 2010}

    15   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    16   \mode<presentation>{

    17   \begin{frame}<1>[t]

    18   \frametitle{%

    19   \begin{tabular}{@ {\hspace{-3mm}}c@ {}}

    20   \\

    21   \LARGE Proof Pearl:\\[-0mm]

    22   \LARGE A New Foundation for\\[-2mm] 

    23   \LARGE Nominal Isabelle\\[12mm]

    24   \end{tabular}}

    25   \begin{center}

    26   Brian Huf\!fman and {\bf Christian Urban}\\[0mm] 

    27   \end{center}

    28   \end{frame}}

    29   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

    30 

    31 *}

    32 

    33 text_raw {*

    34   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    35   \mode<presentation>{

    36   \begin{frame}<1-2>[c]

    37   \frametitle{Nominal Isabelle}

    38 

    39   \begin{itemize}

    40   \item \ldots is a definitional extension of Isabelle/HOL

    41   (let-polymorphism and type classes)\medskip

    42 

    43   \item \ldots provides a convenient reasoning infrastructure for

    44   terms involving binders (e.g.~lambda calculus, variable convention)\medskip

    45   

    46   \item<2-> \ldots mainly used to find errors in my own 

    47   (published) paper proofs and in those of others \alert{\bf ;o)}

    48   \end{itemize}

    49 

    50   \end{frame}}

    51   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

    52 *}

    53  

    54 text_raw {*

    55   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    56   \mode<presentation>{

    57   \begin{frame}<1-3>[c]

    58   \frametitle{Nominal Theory}

    59   

    60   \ldots by Pitts; at its core are:\bigskip

    61 

    62   \begin{itemize}

    63   \item sorted atoms and 

    64   \item sort-respecting permutations

    65   \end{itemize}

    66 

    67   \onslide<2->{

    68   \begin{textblock}{8}(4,11)

    69   \onslide<3->{$\text{inv\_of\_}\pi \,\act\, ($}\onslide<2->{$\pi \,\act\, x$}%

    70   \onslide<3->{$) \,=\, x$}

    71   \end{textblock}}

    72 

    73 

    74   \end{frame}}

    75   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

    76 *}

    77 

    78 text_raw {*

    79   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    80   \mode<presentation>{

    81   \begin{frame}<1-4>[t]

    82   \frametitle{The ``Old Way''}

    83   

    84   \begin{itemize}

    85   \item sorted atoms\\ \alert{$\quad\mapsto$ separate types}\; (``copies'' of nat)\bigskip 

    86   \item sort-respecting permutations\\ \alert{$\quad\mapsto$ lists of pairs of atoms (list swappings)}

    87   \onslide<2->{

    88   \begin{center} 

    89   \begin{tabular}{c@ {\hspace{7mm}}c}

    90   $\text{[]} \,\act\, c = c$ &

    91   $\swap{a}{b}\!::\!\pi \,\act\, c =

    92   \begin{cases}

    93   b & \text{if}\, \pi\act c = a\\

    94   a & \text{if}\, \pi\act c = b\\

    95   \pi\act c & \text{otherwise}

    96   \end{cases}$

    97   \end{tabular}

    98   \end{center}}

    99   \end{itemize}

   100 

   101   \only<3>{

   102   \begin{textblock}{14}(1,12.5)

   103   \alert{The big benefit:} the type system takes care of the sort-respecting requirement.

   104   \end{textblock}}

   105   \only<4>{

   106   \begin{textblock}{14}(1,12.5)

   107   \alert{A small benefit:} permutation composition is \alert{list append} 

   108   and permutation inversion is \alert{list reversal}.

   109   \end{textblock}

   110   }

   111 

   112   \end{frame}}

   113   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   114 *}

   115 

   116 text_raw {*

   117   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   118   \mode<presentation>{

   119   \begin{frame}<1-4>

   120   \frametitle{Problems}

   121 

   122   \begin{itemize}

   123   \item @{text "_ \<bullet> _ :: \<alpha> perm \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}\bigskip

   124 

   125   \item @{text "supp _ :: \<beta> \<Rightarrow> \<alpha> set"}

   126 

   127   \begin{center}

   128   $\text{finite} (\text{supp}\;x)_{\,\alpha_1\,\text{set}}$ \ldots 

   129   $\text{finite} (\text{supp}\;x)_{\,\alpha_n\,\text{set}}$

   130   \end{center}\bigskip

   131   

   132   \item $\forall \pi_{\alpha_1} \ldots \pi_{\alpha_n}\;.\; P$\bigskip

   133 

   134   \item type-classes 

   135   \onslide<3>{\small\hspace{5mm}can only have \alert{\bf one} type parameter}

   136   \begin{itemize}

   137   \item<2-> $\text{[]}\,\act\, x = 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$

   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)$

   142   \end{itemize}

   143   \end{itemize}

   144 

   145   \only<4->{

   146   \begin{textblock}{9}(3,7)\begin{tikzpicture}

   147   \draw (0,0) node[inner sep=3mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] 

   148   {\normalsize\color{darkgray}

   149   \begin{quote}

   150   \begin{itemize}

   151   \item \alert{lots} of ML-code 

   152   \item \alert{not} pretty 

   153   \item \alert{not a {\bf proof pearl}} :o( 

   154   \end{itemize}

   155   \end{quote}};

   156   \end{tikzpicture}

   157   \end{textblock}}

   158 

   159   \end{frame}}

   160   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   161 *}

   162 

   163 text_raw {*

   164   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   165   \mode<presentation>{

   166   \begin{frame}<1-4>

   167   \frametitle{A Better Way}

   168 *}

   169 datatype atom = Atom string nat

   170 

   171 text_raw {*

   172   \mbox{}\bigskip

   173   \begin{itemize}

   174   \item<2-> permutations are (restricted) bijective functions from @{text "atom \<Rightarrow> atom"}

   175 

   176      \begin{itemize}

   177      \item sort-respecting \hspace{5mm}($\,\forall a.\;\text{sort}(\pi a) = \text{sort}(a)$)

   178      \item finite domain \hspace{5mm}($\text{finite} \{a.\;\pi a \not= a\}$)

   179      \end{itemize}\medskip

   180      

   181   \item<3-> \alert{What about {\bf swappings}?}

   182      \small

   183      \[

   184      \begin{array}{l@ {\hspace{1mm}}l}

   185      (a\;b) \dn & \text{if}\;\text{sort}(a) = \text{sort}(b)\\

   186         & \text{then}\;\lambda  c. \text{if}\;a = c\;\text{then}\;b\;\text{else}\;

   187           \text{if}\;b = c\;\text{then}\;a\;\text{else}\;c\\

   188         & \text{else}\;\only<3>{\raisebox{-5mm}{\textcolor{red}{\huge\bf $?$}}}

   189           \only<4->{\text{\alert{\bf id}}}

   190      \end{array}

   191      \]

   192   \end{itemize}

   193 

   194   \only<2>{

   195   \begin{textblock}{7}(4,11)

   196   @{text "_ \<bullet> _ :: perm \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}

   197   \end{textblock}}

   198   

   199   \end{frame}}

   200   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   201 *}

   202 

   203 text_raw {*

   204   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   205   \mode<presentation>{

   206   \begin{frame}<1-7>

   207   \frametitle{A Smoother Nominal Theory}

   208   

   209   From there it is essentially plain sailing:\bigskip

   210 

   211   \begin{itemize}

   212   \item<2-> $(a\;b) = (b\;a) \onslide<4->{= (a\;c) + (b\;c) + (a\;c)}$\bigskip  

   213 

   214   \item<3-> permutations are an instance of Isabelle's\\  

   215   group\_add ($0$, $\pi_1 + \pi_2$, $- \pi$)\bigskip

   216 

   217   \item<6-> $\_\;\act\;\_ :: \text{perm} \Rightarrow \alpha \Rightarrow \alpha$\medskip

   218   

   219    \begin{itemize}

   220    \item $0\;\act\;x = x$\\

   221    \item $(\pi_1 + \pi_2)\;\act\;x = \pi_1\;\act\;(\pi_2\;\act\;x)$

   222    \end{itemize}\medskip

   223 

   224    \onslide<7->{\alert{$\;\mapsto\;$}only one type class needed, $\text{finite}(\text{supp}\;x)$,\\

   225    \hspace{9mm}$\forall \pi. P$}

   226   \end{itemize}

   227 

   228   \only<5>{

   229   \begin{textblock}{6}(2.5,11)

   230   \begin{tikzpicture}

   231   \draw (0,0) node[inner sep=3mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] 

   232   {\normalsize\color{darkgray}

   233   \begin{minipage}{8cm}\raggedright

   234   This is slightly odd, since in general: 

   235   \begin{center}$\pi_1 + \pi_2 \alert{\not=} \pi_2 + \pi_1$\end{center}

   236   \end{minipage}};

   237   \end{tikzpicture}

   238   \end{textblock}}

   239 

   240   

   241 

   242   \end{frame}}

   243   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   244 *}

   245 

   246 text_raw {*

   247   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   248   \mode<presentation>{

   249   \begin{frame}<1>[c]

   250   \frametitle{One Snatch}

   251 *}

   252 

   253 datatype \<iota>atom = \<iota>Atom string nat

   254 

   255 

   256 text_raw {*

   257   \isanewline\isanewline

   258   \begin{itemize}

   259   \item You like to get the advantages of the old way back: you 

   260   \alert{cannot mix} atoms of dif$\!$ferent sort:\bigskip

   261   

   262   \small

   263   e.g.~LF-objects:

   264   \begin{center}

   265   $\quad M ::= c \mid x \mid \lambda x\!:\!A. M \mid M_1\;M_2$

   266   \end{center}

   267   \end{itemize}

   268 

   269   \end{frame}}

   270   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   271 *}

   272 

   273 text_raw {*

   274   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   275   \mode<presentation>{

   276   \begin{frame}<1-2>

   277   \frametitle{Our Solution}

   278 

   279 

   280   \begin{itemize}

   281   \item \underline{concrete} atoms:

   282   \end{itemize}

   283 *}

   284 (*<*)

   285 consts sort :: "atom \<Rightarrow> string"

   286 (*>*)

   287 

   288 typedef name = "{a :: atom. sort a = ''name''}" (*<*)sorry(*>*)

   289 typedef ident = "{a :: atom. sort a = ''ident''}" (*<*)sorry(*>*)

   290 

   291 text_raw {*

   292   \mbox{}\bigskip\bigskip

   293   \begin{itemize}

   294   \item they are a ``subtype'' of the generic atom type

   295   \item there is an overloaded  function \alert{\bf atom}, which injects concrete 

   296   atoms into generic ones\medskip 

   297   \begin{center}

   298   \begin{tabular}{l}

   299   $\text{atom}(a) \fresh x$\\

   300   $(a \leftrightarrow b) \dn (\text{atom}(a)\;\;\text{atom}(b))$

   301   \end{tabular}

   302   \end{center}

   303   \pause

   304   One would like to have $a \fresh x$, $\swap{a}{b}$, \ldots

   305   \end{itemize}

   306 

   307   \end{frame}}

   308   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   309 *}

   310 

   311 text_raw {*

   312   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   313   \mode<presentation>{

   314   \begin{frame}<1-4>

   315   \frametitle{Sorts Reloaded}

   316 *}

   317 datatype atom\<iota> = Atom\<iota> string nat

   318 

   319 text_raw {*

   320   \isanewline\isanewline

   321   \pause

   322   \alert{Problem}: HOL-binders or Church-style lambda-terms

   323   \begin{center}

   324   $\lambda x_\alpha.\, x_\alpha\;x_\beta$

   325   \end{center}

   326   \pause

   327   \isanewline\isanewline

   328 

   329 \isacommand{datatype} ty = TVar string $\mid$ ty $\rightarrow$ ty\\

   330 \isacommand{datatype} var = Var name ty\\

   331 \pause

   332 $(x \leftrightarrow y) \,\act\, (x_\alpha, x_\beta) = (y_\alpha, y_\beta)$

   333 

   334   \end{frame}}

   335   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   336 *}

   337 

   338 text_raw {*

   339   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   340   \mode<presentation>{

   341   \begin{frame}<1-2>

   342   \frametitle{Non-Working Solution}

   343 

   344 Instead of\isanewline\isanewline

   345 *}

   346     datatype atom\<iota>\<iota> = Atom\<iota>\<iota> string nat

   347 

   348 text_raw {*

   349 \isanewline\isanewline

   350 have

   351 \isanewline\isanewline

   352 *}

   353 

   354     datatype 'a atom\<iota>\<iota>\<iota> = Atom\<iota>\<iota>\<iota> 'a nat

   355 text_raw {*

   356   \pause

   357   \isanewline\isanewline

   358   But then

   359   \begin{center}

   360   @{text "_ \<bullet> _ :: \<alpha> perm \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}

   361   \end{center}

   362   \end{frame}}

   363   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   364 *}

   365 

   366 (*<*)

   367 hide_const sort

   368 (*>*)

   369 

   370 text_raw {*

   371   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   372   \mode<presentation>{

   373   \begin{frame}<1-4>

   374   \frametitle{A Working Solution}

   375 

   376 *}

   377     datatype sort = Sort string "sort list"

   378     datatype atom\<iota>\<iota>\<iota>\<iota> = Atom\<iota>\<iota>\<iota>\<iota> sort nat

   379 (*<*)

   380 consts sort_ty :: "nat \<Rightarrow> sort"

   381 (*>*)

   382 text_raw {*

   383   \pause

   384   \isanewline

   385 

   386   {\small\begin{tabular}{rcl}

   387   @{text "sort_ty (TVar x)"}  & @{text "\<equiv>"} & @{text "Sort ''TVar'' [Sort x []]"} \\

   388   @{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]"}\\

   389   \end{tabular}}

   390   \pause

   391   \isanewline\isanewline

   392   \isacommand{typedef} @{text "var = {a :: atom. sort a \<in> range sort_ty}"}

   393   \pause

   394   \isanewline\isanewline

   395   \small

   396   \begin{minipage}{12cm}

   397   @{text "Var x \<tau> \<equiv> \<lceil> Atom (sort_ty \<tau>) x \<rceil>"}\isanewline

   398 

   399   @{text "(Var x \<tau> \<leftrightarrow> Var y \<tau>) \<bullet> Var x \<tau> = Var y \<tau>"}\\

   400   @{text "(Var x \<tau> \<leftrightarrow> Var y \<tau>) \<bullet> Var x \<tau>' = Var x \<tau>'"}\\

   401   \end{minipage}

   402   \end{frame}}

   403   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   404 *}

   405 

   406 text_raw {*

   407   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   408   \mode<presentation>{

   409   \begin{frame}<1-4>[c]

   410   \frametitle{Conclusion}

   411   \mbox{}\\[-3mm]

   412 

   413   \begin{itemize}

   414   \item the formalised version of the nominal theory is now much nicer to 

   415   work with (sorts are occasionally explicit, \alert{$\forall \pi. P$})\medskip

   416 

   417   \item permutations: ``be as abstract as you can'' (group\_add is a slight oddity)\medskip

   418 

   419   \item the crucial insight: allow sort-disrespecting swappings%

   420   \onslide<2->{ \ldots just define them as the identity}\\%

   421   \onslide<3->{ (a referee called this a \alert{``hack''})}\medskip

   422 

   423   \item<4-> there will be a hands-on tutorial about Nominal Isabelle at \alert{POPL'11}

   424   in Austin Texas

   425   \end{itemize}

   426 

   427   

   428   \end{frame}}

   429   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   430 *}

   431 

   432 text_raw {*

   433   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   434   \mode<presentation>{

   435   \begin{frame}<1>[c]

   436   \frametitle{

   437   \begin{tabular}{c}

   438   \mbox{}\\[23mm]

   439   \alert{\LARGE Thank you very much}\\

   440   \alert{\Large Questions?}

   441   \end{tabular}}

   442   

   443   \end{frame}}

   444   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   445 *}

   446 

   447 (*<*)

   448 end

   449 (*>*)