# HG changeset patch # User Christian Urban # Date 1278801405 -3600 # Node ID ac064c47138b814297cd3b1d3439d3f15fb01419 # Parent f961a32eb0d9b760fee1d98370ba930e22501078 more on slides diff -r f961a32eb0d9 -r ac064c47138b Slides/Slides2.thy --- a/Slides/Slides2.thy Sat Jul 10 15:50:33 2010 +0100 +++ b/Slides/Slides2.thy Sat Jul 10 23:36:45 2010 +0100 @@ -18,12 +18,11 @@ \frametitle{% \begin{tabular}{@ {\hspace{-3mm}}c@ {}} \\ - \LARGE Proof Pearl:\\[-2mm] + \LARGE Proof Pearl:\\[-0mm] \LARGE A New Foundation for\\[-2mm] \LARGE Nominal Isabelle\\[12mm] \end{tabular}} \begin{center} - \small Brian Huf\!fman and {\bf Christian Urban}\\[0mm] \end{center} \end{frame}} @@ -34,28 +33,43 @@ text_raw {* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \mode{ - \begin{frame}<1-2> - \frametitle{\begin{tabular}{c}Nominal Isabelle\end{tabular}} - \mbox{}\\[-3mm] + \begin{frame}<1-2>[c] + \frametitle{Nominal Isabelle} \begin{itemize} - \item sorted atoms and sort-respecting permutations\medskip + \item \ldots is a definitional extension of Isabelle/HOL + (let-polymorphism and type classes)\medskip + + \item \ldots provides a convenient reasoning infrastructure for + terms involving binders (e.g.~lambda calculus, variable convention)\medskip + + \item<2-> \ldots mainly used to find errors in my own + (published) paper proofs and in that of others \alert{\bf ;o)} + \end{itemize} + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}<1-3>[c] + \frametitle{Nominal Theory} + + by Pitts; at its core are:\bigskip + + \begin{itemize} + \item sorted atoms and + \item sort-respecting permutations + \end{itemize} \onslide<2->{ - \item[] in old Nominal: atoms have \underline{dif\!ferent} type\medskip + \begin{textblock}{8}(4,11) + \onslide<3->{$\text{inv\_of\_}\pi \,\act\, ($}\onslide<2->{$\pi \,\act\, x$}% + \onslide<3->{$) \,=\, x$} + \end{textblock}} - \begin{center} - \begin{tabular}{c@ {\hspace{7mm}}c} - $[]\;\act\;c \dn c$ & - $(a\;b)\!::\!\pi\;\act\;c \dn$ - $\begin{cases} - b & \text{if}\; \pi \act c = a\\ - a & \text{if}\; \pi \act c = b\\ - \pi \act c & \text{otherwise} - \end{cases}$ - \end{tabular} - \end{center}} - \end{itemize} \end{frame}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @@ -64,29 +78,37 @@ text_raw {* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \mode{ - \begin{frame}<1-2> - \frametitle{\begin{tabular}{c}Nominal Theory\end{tabular}} - \mbox{}\\[-3mm] - + \begin{frame}<1-4>[t] + \frametitle{The ``Old Way''} + \begin{itemize} - \item sorted atoms and sort-respecting permutations\medskip - + \item sorted atoms\\ \alert{$\quad\mapsto$ separate types}\; (``copies'' of nat)\bigskip + \item sort-respecting permutations\\ \alert{$\quad\mapsto$ lists of pairs of atoms (list swappings)} \onslide<2->{ - \item[] in old Nominal: atoms have \underline{dif\!ferent} type\medskip - - \begin{center} + \begin{center} \begin{tabular}{c@ {\hspace{7mm}}c} - $[]\;\act\;c \dn c$ & - $(a\;b)\!::\!\pi\;\act\;c \dn$ - $\begin{cases} - b & \text{if}\; \pi \act c = a\\ - a & \text{if}\; \pi \act c = b\\ - \pi \act c & \text{otherwise} + $\text{[]} \,\act\, c = c$ & + $\swap{a}{b}\!::\!\pi \,\act\, c = + \begin{cases} + b & \text{if}\, \pi\act c = a\\ + a & \text{if}\, \pi\act c = b\\ + \pi\act c & \text{otherwise} \end{cases}$ \end{tabular} \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. + \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}. + \end{textblock} + } + \end{frame}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *} @@ -94,9 +116,8 @@ text_raw {* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \mode{ - \begin{frame}<1> - \frametitle{\begin{tabular}{c}Problems\end{tabular}} - \mbox{}\\[-3mm] + \begin{frame}<1-4> + \frametitle{Problems} \begin{itemize} \item @{text "_ \ _ :: \ perm \ \ \ \"}\bigskip @@ -110,9 +131,29 @@ \item $\forall \pi_{\alpha_1} \ldots \pi_{\alpha_n}\;.\; P$\bigskip - \item type-classes + \item type-classes + \onslide<3>{\small\hspace{5mm}can only have \alert{\bf one} type parameter} + \begin{itemize} + \item<2-> $\text{[]}\,\act\, x = x$ + \item<2-> $(\pi_1 @ \pi_2) \,\act \, x = \pi_1 \,\act\,(\pi_2 \,\act\, x)$ + \item<2-> if $\pi_1 \sim \pi_2$ then $\pi_1 \,\act\, x = \pi_2 \,\act\, x$ + \end{itemize} \end{itemize} + \only<4->{ + \begin{textblock}{9}(3,7)\begin{tikzpicture} + \draw (0,0) node[inner sep=3mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] + {\normalsize\color{darkgray} + \begin{quote} + \begin{itemize} + \item \alert{lots} of ML-code + \item \alert{not} pretty + \item \alert{not a proof pearl} :o( + \end{itemize} + \end{quote}}; + \end{tikzpicture} + \end{textblock}} + \end{frame}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *} @@ -120,34 +161,39 @@ text_raw {* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \mode{ - \begin{frame}<1-4> - \frametitle{\begin{tabular}{c}Our New Solution\end{tabular}} - \mbox{}\\[-3mm] + \begin{frame}<1-5> + \frametitle{A Better Way} *} datatype atom = Atom string nat text_raw {* \mbox{}\bigskip \begin{itemize} - \item<2-> permutations are (restricted) bijective functions from @{text "atom \ atom"} + \item<3-> permutations are (restricted) bijective functions from @{text "atom \ atom"} \begin{itemize} - \item sort-respecting \hspace{5mm}($\forall a.\;\text{sort}(f a) = \text{sort}(a)$) - \item finite domain \hspace{5mm}($\text{finite} \{a.\;f a \not= a\}$) + \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<3-> swappings: + + \item<4-> \alert{What about 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}\; \text{if}\;b = c\;\text{then}\;a\;\text{else}\;c\\ - & \text{else}\;\only<3>{\mbox{\textcolor{red}{\bf ?}}}\only<4->{\text{id}} + & \text{else}\;\only<4>{\raisebox{-5mm}{\textcolor{red}{\huge\bf $?$}}} + \only<5->{\text{\alert{\bf id}}} \end{array} \] \end{itemize} + \only<3>{ + \begin{textblock}{7}(4,11) + @{text "\ \ _ :: perm \ \ \ \"} + \end{textblock}} + \end{frame}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *} @@ -155,27 +201,28 @@ text_raw {* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \mode{ - \begin{frame}<1-6> - \frametitle{\begin{tabular}{c}\LARGE{}A Smoother Nominal Theory\end{tabular}} - \mbox{}\\[-3mm] + \begin{frame}<1-7> + \frametitle{A Smoother Nominal Theory} + + From there it is essentially plain sailing:\bigskip \begin{itemize} - \item<1-> $(a\;b) = (b\;a) \onslide<3->{= (a\;c) + (b\;c) + (a\;c)}$\bigskip + \item<2-> $(a\;b) = (b\;a) \onslide<4->{= (a\;c) + (b\;c) + (a\;c)}$\bigskip - \item<2-> permutations are an instance of group\_add\\ $0$, $\pi_1 + \pi_2$, $- \pi$\bigskip + \item<3-> permutations are an instance of Isabelle's\\ + group\_add ($0$, $\pi_1 + \pi_2$, $- \pi$)\bigskip - \item<5-> $\_\;\act\;\_ :: \text{perm} \Rightarrow \alpha \Rightarrow \alpha$\medskip + \item<6-> $\_\;\act\;\_ :: \text{perm} \Rightarrow \alpha \Rightarrow \alpha$\medskip \begin{itemize} \item $0\;\act\;x = x$\\ \item $(\pi_1 + \pi_2)\;\act\;x = \pi_1\;\act\;(\pi_2\;\act\;x)$ - \end{itemize} + \end{itemize}\medskip - \small - \onslide<6->{$\text{finite}(\text{supp}\;x)$, $\forall \pi. P$} + \onslide<7->{\alert{$\;\mapsto\;$}only one type class, $\text{finite}(\text{supp}\;x)$, $\forall \pi. P$} \end{itemize} - \only<4>{ + \only<5>{ \begin{textblock}{6}(2.5,11) \begin{tikzpicture} \draw (0,0) node[inner sep=3mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] @@ -195,8 +242,8 @@ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \mode{ \begin{frame}<1-3> - \frametitle{\begin{tabular}{c}Very Few Snatches\end{tabular}} - \mbox{}\\[-3mm] + \frametitle{One Snatch} + \begin{itemize} \item \underline{concrete} atoms: @@ -212,7 +259,7 @@ text_raw {* \mbox{}\bigskip\bigskip \begin{itemize} - \item<2-> there is an overloaded function \underline{atom}, which injects concrete + \item<2-> there is an overloaded function \alert{\bf atom}, which injects concrete atoms into generic ones\medskip \begin{center} \begin{tabular}{l} @@ -222,9 +269,46 @@ \end{center}\bigskip\medskip \onslide<3-> - {I would like to have $a \fresh x$, $(a\; b)$, \ldots} + {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}} + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} - \end{itemize} +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}<1-4> + \frametitle{Sorts Reloaded} +*} +datatype atom\ = Atom\ string nat + +text_raw {* + \isanewline\isanewline + \pause + \alert{Problem}: HOL-binders or Church-style lambda-terms + \begin{center} + $\lambda x_\alpha.\, x_\alpha\;x_\beta$ + \end{center} + \pause + \isanewline\isanewline + +\isacommand{datatype} ty = TVar string $\mid$ ty $\rightarrow$ ty\\ +\isacommand{datatype} var = Var name ty\\ +\pause +$(x \leftrightarrow y) \,\act\, (x_\alpha, x_\beta) = (y_\alpha, y_\beta)$ \end{frame}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @@ -233,8 +317,64 @@ text_raw {* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \mode{ + \begin{frame}<1-3> + \frametitle{Non-Working Solution} + +Instead of\isanewline\isanewline +*} + datatype atom\\ = Atom\\ string nat + +text_raw {* +\isanewline\isanewline +have +\isanewline\isanewline +*} + + datatype 'a atom\\\ = Atom\\ 'a nat +text_raw {* + \pause + \isanewline\isanewline + But then + \begin{center} + @{text "_ \ _ :: \ perm \ \ \ \"} + \end{center} + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}<1-3> + \frametitle{A Working Solution} + +*} + datatype sort = Sort string "sort list" + datatype atom\\ = Atom\\ string nat + +text_raw {* +\isanewline\isanewline +have +\isanewline\isanewline +*} + + datatype 'a atom\\\ = Atom\\ 'a nat +text_raw {* + \pause + \isanewline\isanewline + But then + \begin{center} + @{text "_ \ _ :: \ perm \ \ \ \"} + \end{center} + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ \begin{frame}<1-2>[c] - \frametitle{\begin{tabular}{c}\LARGE{}End of Part I\end{tabular}} + \frametitle{Conclusion} \mbox{}\\[-3mm] \begin{itemize} diff -r f961a32eb0d9 -r ac064c47138b Slides/document/beamerthemeplainculight.sty --- a/Slides/document/beamerthemeplainculight.sty Sat Jul 10 15:50:33 2010 +0100 +++ b/Slides/document/beamerthemeplainculight.sty Sat Jul 10 23:36:45 2010 +0100 @@ -1,4 +1,4 @@ -\ProvidesPackage{beamerthemeplaincu}[2003/11/07 ver 0.93] +%%\Providespackage{beamerthemeplainculight}[2003/11/07 ver 0.93] \NeedsTeXFormat{LaTeX2e}[1995/12/01] % Copyright 2003 by Till Tantau . @@ -6,7 +6,7 @@ % This program can be redistributed and/or modified under the terms % of the LaTeX Project Public License Distributed from CTAN % archives in directory macros/latex/base/lppl.txt. - + \newcommand{\slidecaption}{} \mode