nominal2: comparison Slides/Slides1.thy

equal deleted inserted replaced

-:dd3b9c046c7d
+:4da5c5c29009
 \begin{frame}<1-2>
 \frametitle{\begin{tabular}{c}Binding in Old Nominal\end{tabular}}
 \mbox{}\\[-6mm]
 \begin{itemize}
-\item old Nominal provided a reasoning infrastructure for single binders\medskip
+\item the old Nominal Isabelle provided a reasoning infrastructure for single binders\medskip
 \begin{center}
 Lam [a].(Var a)
 \end{center}\bigskip
 \small
 for example\\
 \begin{tabular}{l@ {\hspace{2mm}}l}
 \pgfuseshading{smallspherered} & a $\fresh$ Lam [a]. t\\
 \pgfuseshading{smallspherered} & Lam [a]. (Var a) \alert{$=$} Lam [b]. (Var b)\\
-\pgfuseshading{smallspherered} & Barendregt style reasoning about bound variables\\
+\pgfuseshading{smallspherered} & Barendregt-style reasoning about bound variables\\
 \end{tabular}
 \end{textblock}}
 \end{frame}}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \frametitle{\begin{tabular}{c}Inspiration from Ott\end{tabular}}
 \mbox{}\\[-3mm]
 \begin{itemize}
 \item this way of specifying binding is inspired by
-Ott\onslide<2->{, \alert{\bf but} we made adjustments:}\medskip
+{\bf Ott}\onslide<2->{, \alert{\bf but} we made some adjustments:}\medskip
 \only<2>{
 \begin{itemize}
 \item Ott allows specifications like\smallskip
 for $\alpha$-equated terms}
 \end{itemize}}
 \only<5>{
 \begin{itemize}
-\item we allow multiple binders and bodies\smallskip
+\item we allow multiple ``binders'' and ``bodies''\smallskip
 \begin{center}
 \isacommand{bind} a b c \isacommand{in} x y z
 \end{center}\bigskip\medskip
-the reason is that in general
+the reason is that with our definitions of $\alpha$-equivalence
 \begin{center}
 \begin{tabular}{rcl}
 \isacommand{bind\_res} as \isacommand{in} x y & $\not\Leftrightarrow$ &
 \begin{tabular}{@ {}l}
 \isacommand{bind\_res} as \isacommand{in} x,\\
 \begin{frame}<1>
 \frametitle{\begin{tabular}{c}Alpha-Equivalence\end{tabular}}
 \mbox{}\\[-3mm]
 \begin{itemize}
-\item in old Nominal, we represented single binders as partial functions:\bigskip
+\item in the old Nominal Isabelle, we represented single binders as partial functions:\bigskip
 \begin{center}
 \begin{tabular}{l}
 Lam [$a$].\,$t$ $\;{^\text{``}}\!\dn{}\!^{\text{''}}$\\[2mm]
 \;\;\;\;$\lambda b.$\;$\text{if}\;a = b\;\text{then}\;t\;\text{else}$\\
 \end{itemize}
 \only<1>{
 \begin{textblock}{8}(3,8.5)
 \begin{tabular}{l@ {\hspace{2mm}}p{8cm}}
-\pgfuseshading{smallspherered} & $as$ is a set of atoms\ldots the binders\\
+\pgfuseshading{smallspherered} & $as$ is a set of names\ldots the binders\\
 \pgfuseshading{smallspherered} & $x$ is the body\\
 \pgfuseshading{smallspherered} & $\approx_{\text{set}}$ is where the cardinality
 of the binders has to be the same\\
 \end{tabular}
 \end{textblock}}
 \end{tabular}
 \end{textblock}}
 \only<8>{
 \begin{textblock}{8}(3,13.8)
-\footnotesize $^*$ $as$ and $bs$ are \alert{lists} of atoms
+\footnotesize $^*$ $as$ and $bs$ are \alert{lists} of names
 \end{textblock}}
 \end{frame}}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 *}
 text_raw {*
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \mode<presentation>{
-\begin{frame}<1-2>
+\begin{frame}<1-3>
 \frametitle{\begin{tabular}{c}Examples\end{tabular}}
 \mbox{}\\[-3mm]
 \begin{itemize}
 \item lets look at ``type-schemes'':\medskip\medskip
 \end{tabular}
 \end{center}}
 \end{itemize}
-\only<2->{
+\only<3->{
 \begin{textblock}{4}(0.3,12)
 \begin{tikzpicture}
 \draw (0,0) node[inner sep=1mm,fill=cream, ultra thick, draw=red, rounded corners=2mm]
 {\tiny\color{darkgray}
 \begin{minipage}{3.4cm}\raggedright
 \\
 \end{tabular}
 \end{minipage}};
 \end{tikzpicture}
 \end{textblock}}
-\only<2->{
+\only<3->{
 \begin{textblock}{4}(5.2,12)
 \begin{tikzpicture}
 \draw (0,0) node[inner sep=1mm,fill=cream, ultra thick, draw=red, rounded corners=2mm]
 {\tiny\color{darkgray}
 \begin{minipage}{3.4cm}\raggedright
 $\wedge$ & $\pi \cdot as = bs$\\
 \end{tabular}
 \end{minipage}};
 \end{tikzpicture}
 \end{textblock}}
-\only<2->{
+\only<3->{
 \begin{textblock}{4}(10.2,12)
 \begin{tikzpicture}
 \draw (0,0) node[inner sep=1mm,fill=cream, ultra thick, draw=red, rounded corners=2mm]
 {\tiny\color{darkgray}
 \begin{minipage}{3.4cm}\raggedright
 *}
 text_raw {*
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \mode<presentation>{
-\begin{frame}<1>
+\begin{frame}<1-2>
 \frametitle{\begin{tabular}{c}Examples\end{tabular}}
 \mbox{}\\[-3mm]
 \begin{center}
 \only<1>{$(\{x\}, x) \approx_? (\{x, y\}, x)$}
 \end{tabular}
 \end{minipage}};
 \end{tikzpicture}
 \end{textblock}}
+\only<2>{
+\begin{textblock}{6}(2.5,4)
+\begin{tikzpicture}
+\draw (0,0) node[inner sep=5mm,fill=cream, ultra thick, draw=red, rounded corners=2mm]
+{\normalsize
+\begin{minipage}{8cm}\raggedright
+\begin{itemize}
+\item \color{darkgray}$\alpha$-equivalences coincide when a single name is
+abstracted
+\item \color{darkgray}in that case they are equivalent to ``old-fashioned'' definitions of $\alpha$
+\end{itemize}
+\end{minipage}};
+\end{tikzpicture}
+\end{textblock}}
 \end{frame}}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 *}
 text_raw {*
 \begin{frame}<1-3>
 \frametitle{\begin{tabular}{c}General Abstractions\end{tabular}}
 \mbox{}\\[-7mm]
 \begin{itemize}
-\item we take $(as, x) \approx\!\makebox[0mm][l]{${}_{\star}$}^{=,\text{supp}} (bs, y)$\medskip
+\item we take $(as, x) \approx\!\makebox[0mm][l]{${}_{{}*{}}$}^{=,\text{supp}} (bs, y)$\medskip
 \item they are equivalence relations\medskip
 \item we can therefore use the quotient package to introduce the
-types $\beta\;\text{abs}_\star$\bigskip
+types $\beta\;\text{abs}_*$\bigskip
 \begin{center}
 \only<1>{$[as].\,x$}
 \only<2>{$\text{supp}([as].x) = \text{supp}(x) - as$}
 \only<3>{%
 \begin{tabular}{r@ {\hspace{1mm}}l}
 \multicolumn{2}{@ {\hspace{-7mm}}l}{$[as]. x \alert{=}  [bs].y\;\;\;\text{if\!f}$}\\[2mm]
 $\exists \pi.$ & $\text{supp}(x) - as = \text{supp}(y) - bs$\\
 $\wedge$       & $\text{supp}(x) - as \fresh^* \pi$\\
 $\wedge$       & $\pi \act x = y $\\
-$(\wedge$       & $\pi \act as = bs)\;^\star$\\
+$(\wedge$       & $\pi \act as = bs)\;^*$\\
 \end{tabular}}
 \end{center}
 \end{itemize}
+\only<1->{
+\begin{textblock}{8}(12,3.8)
+\footnotesize $^*$ set, res, list
+\end{textblock}}
 \end{frame}}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 *}
 text_raw {*
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \mode<presentation>{
 \begin{frame}<1>
-\frametitle{\begin{tabular}{c}One Problem\end{tabular}}
+\frametitle{\begin{tabular}{c}A Problem\end{tabular}}
 \mbox{}\\[-3mm]
 \begin{center}
 $\text{let}\;x_1=t_1 \ldots x_n=t_n\;\text{in}\;s$
 \end{center}
 \[
 \infer[\text{Let-}\!\approx_\alpha]
 {\text{Let}\;as\;t \approx_\alpha \text{Let}\;as'\;t'}
 {(\text{bn}(as), t) \approx\!\makebox[0mm][l]{${}_{\text{list}}$}
 ^{\approx_\alpha,\text{fv}} (\text{bn}(as'), t') &
-\onslide<2>{as \approx_\alpha^{\text{bn}} as'}}
+\onslide<2->{as \approx_\alpha^{\text{bn}} as'}}
-\]
+\]\bigskip
-\end{frame}}
+\onslide<1->{\small{}bn-function $\Rightarrow$ \alert{deep binders}}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\end{frame}}
-*}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
 text_raw {*
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \mode<presentation>{
 \begin{frame}<1->
 \end{frame}}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 *}
+text_raw {*
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}<1>
+\frametitle{\begin{tabular}{c}\LARGE``Raw'' Alpha-Equivalence\end{tabular}}
+\mbox{}\\[6mm]
+\begin{center}
+LetRec as::assn t::trm \hspace{10mm}\isacommand{bind} bn(as) \isacommand{in} t \alert{as}\\
+\end{center}
+\[\mbox{}\hspace{-4mm}
+\infer[\text{LetRec-}\!\approx_\alpha]
+{\text{LetRec}\;as\;t \approx_\alpha \text{LetRec}\;as'\;t'}
+{(\text{bn}(as), (t, as)) \approx\!\makebox[0mm][l]{${}_{\text{list}}$}
+^{R,fv} (\text{bn}(as'), (t', as'))}
+\]\bigskip
+\onslide<1->{\alert{deep recursive binders}}
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+text_raw {*
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}<1->
+\frametitle{\begin{tabular}{c}Restrictions\end{tabular}}
+\mbox{}\\[-6mm]
+Our restrictions on binding specifications:
+\begin{itemize}
+\item a body can only occur once in a list of binding clauses\medskip
+\item you can only have one binding function for a deep binder\medskip
+\item binding functions can return: the empty set, singletons, unions (similarly for lists)
+\end{itemize}
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
 text_raw {*
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \mode<presentation>{
 \begin{frame}<1->
 \frametitle{\begin{tabular}{c}Automatic Proofs\end{tabular}}
 \mbox{}\\[-6mm]
 \begin{itemize}
 \item we can show that $\alpha$'s are equivalence relations\medskip
-\item as a result we can use the quotient package to introduce the type(s)
+\item as a result we can use our quotient package to introduce the type(s)
 of $\alpha$-equated terms
 \[
 \infer
 {\text{Lam}\;x\;t \alert{=} \text{Lam}\;x'\;t'}
 \only<2>{[x].t = [x'].t'}}
 \]
 \item the properties for support are implied by the properties of $[\_].\_$
-\item we can derive strong induction principles (almost automatic---just a matter of
+\item we can derive strong induction principles (almost automatic---matter of time)
-another week or two)
 \end{itemize}
 \end{frame}}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \draw[->,white!50,line width=1mm] (E) -- (F);
 \end{tikzpicture}
 \end{center}
 \begin{itemize}
-\item Core Haskell: 11 types, 49 term-constructors,
+\item Core Haskell: 11 types, 49 term-constructors, 7 binding functions
+\begin{center}
+$\sim$ 1 min
+\end{center}
 \end{itemize}
 \end{frame}}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 *}
 \end{frame}}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 *}
+text_raw {*
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}<1->[c]
+\frametitle{\begin{tabular}{c}Questions?\end{tabular}}
+\mbox{}\\[-6mm]
+\begin{center}
+\alert{\huge{Thanks!}}
+\end{center}
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
 (*<*)
 end
 (*>*)

changeset 2311	4da5c5c29009
parent 2309	13f20fe02ff3
child 2313	25d2cdf7d7e4