14   \renewcommand{\slidecaption}{TU Munich, 28.~May 2010}

    14   \renewcommand{\slidecaption}{Cambridge, 8.~June 2010}

    23   \large General Bindings in Isabelle\\[15mm]

    23   \large General Bindings in Isabelle/HOL\\[5mm]

    26   joint work with {\bf Cezary} and Brian Huf\!fman\\[0mm] 

    26   Christian Urban

    27   \end{center}

    28   \begin{center}

    29   joint work with {\bf Cezary Kaliszyk}\\[0mm] 

    37   \frametitle{\begin{tabular}{c}Part I: Nominal Theory\end{tabular}}

    40   \frametitle{\begin{tabular}{c}Binding in Old Nominal\end{tabular}}

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

    39 

    40   \begin{itemize}

    41   \item sorted atoms and sort-respecting permutations\medskip

    42 

    43   \onslide<2->{

    44   \item[] in old Nominal: atoms have \underline{dif\!ferent} type\medskip

    45 

    46   \begin{center}

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

    48   $[]\;\act\;c \dn c$ &

    49   $(a\;b)\!::\!\pi\;\act\;c \dn$ 

    50   $\begin{cases}

    51   b & \text{if}\; \pi \act c = a\\

    52   a & \text{if}\; \pi \act c = b\\

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

    54   \end{cases}$

    55   \end{tabular}

    56   \end{center}}

    57   \end{itemize}

    58 

    59   \end{frame}}

    60   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

    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 @{text "_ \<bullet> _ :: \<alpha> perm \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}\bigskip

    72 

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

    74 

    75   \begin{center}

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

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

    78   \end{center}\bigskip

    79   

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

    81 

    82   \item type-classes

    83   \end{itemize}

    84 

    85   \end{frame}}

    86   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

    87 *}

    88 

    89 text_raw {*

    90   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    91   \mode<presentation>{

    92   \begin{frame}<1-4>

    93   \frametitle{\begin{tabular}{c}Our New Solution\end{tabular}}

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

    95 *}

    96 datatype atom = Atom string nat

    97 

    98 text_raw {*

    99   \mbox{}\bigskip

   100   \begin{itemize}

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

   102 

   103      \begin{itemize}

   104      \item sort-respecting \hspace{5mm}($\forall a.\;\text{sort}(f a) = \text{sort}(a)$)

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

   106      \end{itemize}\medskip

   107 

   108   \item<3-> swappings:

   109      \small

   110      \[

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

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

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

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

   115         & \text{else}\;\only<3>{\mbox{\textcolor{red}{\bf ?}}}\only<4->{\text{id}}

   116      \end{array}

   117      \]

   118   \end{itemize}

   119 

   120   \end{frame}}

   121   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   122 *}

   123 

   124 text_raw {*

   125   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   126   \mode<presentation>{

   127   \begin{frame}<1-6>

   128   \frametitle{\begin{tabular}{c}\LARGE{}A Smoother Nominal Theory\end{tabular}}

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

   130 

   131   \begin{itemize}

   132   \item<1-> $(a\;b) = (b\;a) \onslide<3->{= (a\;c) + (b\;c) + (a\;c)}$\bigskip  

   133 

   134   \item<2-> permutations are an instance of group\_add\\ $0$, $\pi_1 + \pi_2$, $- \pi$\bigskip

   135 

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

   137   

   138    \begin{itemize}

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

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

   141    \end{itemize}

   142 

   143    \small

   144    \onslide<6->{$\text{finite}(\text{supp}\;x)$, $\forall \pi. P$}

   145   \end{itemize}

   146 

   147   \only<4>{

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

   149   \begin{tikzpicture}

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

   151   {\normalsize\color{darkgray}

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

   153   This is slightly odd, since in general: 

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

   155   \end{minipage}};

   156   \end{tikzpicture}

   157   \end{textblock}}

   158 

   159   \end{frame}}

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

   161 *}

   162 

   163 text_raw {*

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

   165   \mode<presentation>{

   166   \begin{frame}<1-3>

   167   \frametitle{\begin{tabular}{c}Very Few Snatches\end{tabular}}

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

   169 

   170   \begin{itemize}

   171   \item \underline{concrete} atoms:

   172   \end{itemize}

   173 *}

   174 (*<*)

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

   176 (*>*)

   177 

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

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

   180 

   181 text_raw {*

   182   \mbox{}\bigskip\bigskip

   183   \begin{itemize}

   184   \item<2-> there is an overloaded  function \underline{atom}, which injects concrete 

   185   atoms into generic ones\medskip 

   186   \begin{center}

   187   \begin{tabular}{l}

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

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

   190   \end{tabular}

   191   \end{center}\bigskip\medskip

   192 

   193   \onslide<3->

   194   {I would like to have $a \fresh x$, $(a\; b)$, \ldots}

   195 

   196   \end{itemize}

   197 

   198   \end{frame}}

   199   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   200 *}

   201 

   202 text_raw {*

   203   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   204   \mode<presentation>{

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

   206   \frametitle{\begin{tabular}{c}\LARGE{}End of Part I\end{tabular}}

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

   208 

   209   \begin{itemize}

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

   211   work with (sorts are occasionally explicit)\bigskip

   212 

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

   214 

   215   \item allow sort-disrespecting swappings\onslide<2->{: just define them as the identity}

   216   \end{itemize}

   217 

   218   

   219   \end{frame}}

   220   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   221 *}

   222 

   223 text_raw {*

   224   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   225   \mode<presentation>{

   226   \begin{frame}<1-2>

   227   \frametitle{\begin{tabular}{c}\LARGE{}Part II: General Bindings\end{tabular}}

   243   with single binders is a \alert{major} pain; take my word for it!

    56   with single binders and reasoning about it is a \alert{\bf major} pain; 

    57   take my word for it!

   365   vacuous binders (restriction)\medskip

   180   vacuous binders \textcolor{gray}{(restriction)}\medskip

   368   must be the same (abstraction)\medskip

   183   must be the same \textcolor{gray}{(abstraction)}\medskip

   404   \multicolumn{2}{l}{\onslide<3->{\hspace{5mm}\phantom{$|$} bn(ANil) $=$ $\varnothing$}}\\

   219   \multicolumn{2}{l}{\onslide<3->{\hspace{5mm}\phantom{$|$} bn(ANil) $=$ []}}\\

   405   \multicolumn{2}{l}{\onslide<3->{\hspace{5mm}$|$ bn(ACons a t as) $=$ $\{$a$\}$ $\cup$ bn(as)}}\\

   220   \multicolumn{2}{l}{\onslide<3->{\hspace{5mm}$|$ bn(ACons a t as) $=$ [a] @ bn(as)}}\\

   406   \end{tabular}

   221   \end{tabular}

   407 

   222 

   408 

   223 

   409 

   224 

   410   \end{frame}}

   225   \end{frame}}

   411   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   226   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   412 *}

   227 *}

   413 

   228 

   414 text_raw {*

   229 text_raw {*

   415   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   230   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   416   \mode<presentation>{

   231   \mode<presentation>{

   417   \begin{frame}<1-4>

   232   \begin{frame}<1-5>

   418   \frametitle{\begin{tabular}{c}Ott\end{tabular}}

   233   \frametitle{\begin{tabular}{c}Inspiration from Ott\end{tabular}}

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

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

   420 

   235 

   421   \begin{itemize}

   236   \begin{itemize}

   422   \item this way of specifying binding is pretty much stolen from 

   237   \item this way of specifying binding is inspired by 

   423   Ott\onslide<2->{, \alert{\bf but} with adjustments:}\medskip

   238   Ott\onslide<2->{, \alert{\bf but} we made adjustments:}\medskip

   424 

   239   

   425   \begin{itemize}

   240 

   426   \item<2-> Ott allows specifications like\smallskip

   241   \only<2>{

   242   \begin{itemize}

   243   \item Ott allows specifications like\smallskip

   429   \end{center}\medskip

   246   \end{center}

   430 

   247   \end{itemize}}

   431   \item<3-> whether something is bound can depend on other bound things\smallskip

   248 

   432   \begin{center}

   249   \only<3-4>{

   433   Foo $(\lambda x. t)\; s$ 

   250   \begin{itemize}

   434   \end{center}\medskip

   251   \item whether something is bound can depend in Ott on other bound things\smallskip

   435   \onslide<4->{this might make sense for ``raw'' terms, but not at all 

   252   \begin{center}

   253   \begin{tikzpicture}

   254   \node (A) at (-0.5,1) {Foo $(\lambda y. \lambda x. t)$};

   255   \node (B) at ( 1.1,1) {$s$};

   256   \onslide<4>{\node (C) at (0.5,0) {$\{y, x\}$};}

   257   \onslide<4>{\draw[->,red,line width=1mm] (A) -- (C);}

   258   \onslide<4>{\draw[->,red,line width=1mm] (C) -- (B);}

   259   \end{tikzpicture}

   260   \end{center}

   261   \onslide<4>{this might make sense for ``raw'' terms, but not at all 

   437   \end{itemize}

   263   \end{itemize}}

   438   \end{itemize}

   264 

   439 

   265   \only<5>{

   440 

   266   \begin{itemize}

   441   \end{frame}}

   267   \item we allow multiple binders and bodies\smallskip

   442   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   268   \begin{center}

   443 *}

   269   \isacommand{bind} a b c \isacommand{in} x y z

   270   \end{center}\bigskip\medskip

   271   the reason is that in general

   272   \begin{center}

   273   \begin{tabular}{rcl}

   274   \isacommand{bind\_res} as \isacommand{in} x y & $\not\Leftrightarrow$ &

   275   \begin{tabular}{@ {}l}

   276   \isacommand{bind\_res} as \isacommand{in} x,\\

   277   \isacommand{bind\_res} as \isacommand{in} y

   278   \end{tabular}

   279   \end{tabular}

   280   \end{center}\smallskip

   281 

   282   same with \isacommand{bind\_set}

   283   \end{itemize}}

   284   \end{itemize}

   285 

   286 

   287   \end{frame}}

   288   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   289 *}

   290 

   452   \item in old Nominal we represented single binders as partial functions:\bigskip

   299   \item in old Nominal, we represented single binders as partial functions:\bigskip

   456   Lam [$a$].$t$ $\;\dn$\\[2mm]

   303   Lam [$a$].\,$t$ $\;{^\text{``}}\!\dn{}\!^{\text{''}}$\\[2mm]

   458   \phantom{\;\;\;\;$\lambda b.$\;\;\;}$\text{if}\;b \fresh t\;

   305   \phantom{\;\;\;\;$\lambda b.$\;\;\;\;\;\;}$\text{if}\;b \fresh t\;

   899   where $R =\;\approx_\alpha\times\approx_\alpha$ and $fv = \text{fv}\times\text{fv}$

   804   where $R =\;\approx_\alpha\times\approx_\alpha$ and $fv = \text{fv}\cup\text{fv}$

   998   Lam [a]. (Var a) \alert{$=$} Lam [b]. (Var b)

   980   Lam a (Var a) \alert{$=$} Lam b (Var b)

  1003   \item<3-> it took quite some time to get here, but it seems worthwhile (POPL 2011 tutorial)\medskip

   985   \item<3-> it took quite some time to get here, but it seems worthwhile 

  1004   \item<4-> Thanks goes to Cezary!\\ 

   986   (Barendregt's variable convention is unsound in general, 

  1005   \only<5->{\hspace{3mm}\ldots{}and of course others $\in$ Isabelle-team!} 

   987   found bugs in two paper proofs, quotient package, POPL 2011 tutorial)\medskip