--- a/Slides/Slides1.thy Thu Jun 03 15:02:52 2010 +0200
+++ b/Slides/Slides1.thy Mon Jun 07 11:43:01 2010 +0200
@@ -41,7 +41,7 @@
\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)
@@ -64,7 +64,7 @@
\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}}
@@ -235,7 +235,7 @@
\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>{
@@ -264,11 +264,11 @@
\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$ &
@@ -296,7 +296,7 @@
\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}
@@ -396,7 +396,7 @@
\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\\
@@ -415,7 +415,7 @@
\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}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -424,7 +424,7 @@
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
- \begin{frame}<1-2>
+ \begin{frame}<1-3>
\frametitle{\begin{tabular}{c}Examples\end{tabular}}
\mbox{}\\[-3mm]
@@ -445,7 +445,7 @@
\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]
@@ -461,7 +461,7 @@
\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]
@@ -477,7 +477,7 @@
\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]
@@ -572,7 +572,7 @@
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
- \begin{frame}<1>
+ \begin{frame}<1-2>
\frametitle{\begin{tabular}{c}Examples\end{tabular}}
\mbox{}\\[-3mm]
@@ -635,6 +635,21 @@
\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}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
@@ -647,10 +662,10 @@
\mbox{}\\[-7mm]
\begin{itemize}
- \item we take $(as, x) \approx\!\makebox[0mm][l]{${}_{\star}$}^{=,\text{supp}} (bs, y)$\medskip
- \item they are equivalence relations\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$}
@@ -660,11 +675,15 @@
$\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}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -674,7 +693,7 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\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}
@@ -824,14 +843,16 @@
{\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
+ \onslide<1->{\small{}bn-function $\Rightarrow$ \alert{deep binders}}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
+
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
@@ -859,6 +880,51 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
+
+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>{
@@ -868,7 +934,7 @@
\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
\[
@@ -881,8 +947,7 @@
\item the properties for support are implied by the properties of $[\_].\_$
- \item we can derive strong induction principles (almost automatic---just a matter of
- another week or two)
+ \item we can derive strong induction principles (almost automatic---matter of time)
\end{itemize}
@@ -928,7 +993,10 @@
\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}}
@@ -992,6 +1060,21 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
+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
(*>*)
\ No newline at end of file