nominal2: comparison Slides/Slides5.thy

equal deleted inserted replaced

-:43283267737c
+:3b8232f56941
 text_raw {*
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \mode<presentation>{
-\begin{frame}<1-2>
+\begin{frame}<1-6>
 \frametitle{New Types in HOL}
-picture
+\begin{center}
+\begin{tikzpicture}[scale=1.5]
+%%%\draw[step=2mm] (-4,-1) grid (4,1);
+\onslide<2-4,6>{\draw[very thick] (0.7,0.4) circle (4.25mm);}
+\onslide<1-4,6>{\draw[rounded corners=1mm, very thick] ( 0.0,-0.8) rectangle ( 1.8, 0.9);}
+\onslide<3-5,6>{\draw[rounded corners=1mm, very thick] (-1.95,0.85) rectangle (-2.85,-0.05);}
+\onslide<3-4,6>{\draw (-2.0, 0.845) --  (0.7,0.845);}
+\onslide<3-4,6>{\draw (-2.0,-0.045)  -- (0.7,-0.045);}
+\onslide<4-4,6>{\alert{\draw ( 0.7, 0.4) node {\footnotesize\begin{tabular}{@ {}c@ {}}$\alpha$-\\[-1mm]classes\end{tabular}};}}
+\onslide<4-5,6>{\alert{\draw (-2.4, 0.4) node {\footnotesize\begin{tabular}{@ {}c@ {}}$\alpha$-eq.\\[-1mm]terms\end{tabular}};}}
+\onslide<1-4,6>{\draw (1.8, 0.48) node[right=-0.1mm]
+{\footnotesize\begin{tabular}{@ {}l@ {}}existing\\[-1mm] type\\ \onslide<4-4,6>{\alert{(sets of raw terms)}}\end{tabular}};}
+\onslide<2-4,6>{\draw (0.9, -0.35) node {\footnotesize\begin{tabular}{@ {}l@ {}}non-empty\\[-1mm]subset\end{tabular}};}
+\onslide<3-5,6>{\draw (-3.25, 0.55) node {\footnotesize\begin{tabular}{@ {}l@ {}}new\\[-1mm]type\end{tabular}};}
+\onslide<3-4,6>{\draw[<->, very thick] (-1.8, 0.3) -- (-0.1,0.3);}
+\onslide<3-4,6>{\draw (-0.95, 0.3) node[above=0mm] {\footnotesize{}isomorphism};}
+\onslide<6>{\draw[->, line width=2mm, red] (-1.0,-0.4) -- (0.35,0.16);}
+\end{tikzpicture}
+\end{center}
+\begin{center}
+\textcolor{red}{\large\bf\onslide<6>{define $\alpha$-equivalence}}
+\end{center}
 \end{frame}}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 *}
 \begin{itemize}
 \item binding sets of names has some interesting properties:\medskip
 \begin{center}
 \begin{tabular}{l}
-$\forall\{x, y\}.\, x \rightarrow y \;\;\approx_\alpha\;\; \forall\{y, x\}.\, y \rightarrow x$
+\textcolor{blue}{$\forall\{x, y\}.\, x \rightarrow y \;\;\approx_\alpha\;\; \forall\{y, x\}.\, y \rightarrow x$}
 \bigskip\smallskip\\
 \onslide<2->{%
-$\forall\{x, y\}.\, x \rightarrow y \;\;\not\approx_\alpha\;\; \forall\{z\}.\, z \rightarrow z$
+\textcolor{blue}{$\forall\{x, y\}.\, x \rightarrow y \;\;\not\approx_\alpha\;\; \forall\{z\}.\, z \rightarrow z$}
 }\bigskip\smallskip\\
 \onslide<3->{%
-$\forall\{x\}.\, x \rightarrow y \;\;\approx_\alpha\;\; \forall\{x, \alert{z}\}.\, x \rightarrow y$
+\textcolor{blue}{$\forall\{x\}.\, x \rightarrow y \;\;\approx_\alpha\;\; \forall\{x, \alert{z}\}.\, x \rightarrow y$}
 }\medskip\\
 \onslide<3->{\hspace{4cm}\small provided $z$ is fresh for the type}
 \end{tabular}
 \end{center}
 \end{itemize}
 \begin{tikzpicture}
 \draw (0,0) node[inner sep=3mm,fill=cream, ultra thick, draw=red, rounded corners=2mm]
 {\normalsize\color{darkgray}
 \begin{minipage}{8cm}\raggedright
 For type-schemes the order of bound names does not matter, and
-alpha-equivalence is preserved under \alert{vacuous} binders.
+$\alpha$-equivalence is preserved under \alert{vacuous} binders.
 \end{minipage}};
 \end{tikzpicture}
 \end{textblock}}
 \end{frame}}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \begin{itemize}
 \item alpha-equivalence being preserved under vacuous binders is \underline{not} always
 wanted:\bigskip\bigskip\normalsize
-\begin{tabular}{@ {\hspace{-8mm}}l}
+\textcolor{blue}{\begin{tabular}{@ {\hspace{-8mm}}l}
 $\text{let}\;x = 3\;\text{and}\;y = 2\;\text{in}\;x - y\;\text{end}$\medskip\\
 \onslide<2->{$\;\;\;\only<2>{\approx_\alpha}\only<3>{\alert{\not\approx_\alpha}}
 \text{let}\;y = 2\;\text{and}\;x = 3\only<3->{\alert{\;\text{and}
 \;z = \text{loop}}}\;\text{in}\;x - y\;\text{end}$}
-\end{tabular}
+\end{tabular}}
 \end{itemize}
 \end{frame}}
 \begin{itemize}
 \item sometimes one wants to abstract more than one name, but the order \underline{does} matter\bigskip
 \begin{center}
-\begin{tabular}{@ {\hspace{-8mm}}l}
+\textcolor{blue}{\begin{tabular}{@ {\hspace{-8mm}}l}
 $\text{let}\;(x, y) = (3, 2)\;\text{in}\;x - y\;\text{end}$\medskip\\
 $\;\;\;\not\approx_\alpha
 \text{let}\;(y, x) = (3, 2)\;\text{in}\;x - y\;\text{end}$
-\end{tabular}
+\end{tabular}}
 \end{center}
 \end{itemize}
 \end{frame}}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 *}
-text_raw {*
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
-\begin{frame}<1-5>
-\frametitle{\begin{tabular}{c}Inspiration from Ott\end{tabular}}
-\mbox{}\\[-3mm]
-\begin{itemize}
-\item this way of specifying binding is inspired by
-{\bf Ott}\onslide<2->{, \alert{\bf but} we made some adjustments:}\medskip
-\only<2>{
-\begin{itemize}
-\item Ott allows specifications like\smallskip
-\begin{center}
-$t ::= t\;t\; |\;\lambda x.t$
-\end{center}
-\end{itemize}}
-\only<3-4>{
-\begin{itemize}
-\item whether something is bound can depend in Ott on other bound things\smallskip
-\begin{center}
-\begin{tikzpicture}
-\node (A) at (-0.5,1) {Foo $(\lambda y. \lambda x. t)$};
-\node (B) at ( 1.1,1) {$s$};
-\onslide<4>{\node (C) at (0.5,0) {$\{y, x\}$};}
-\onslide<4>{\draw[->,red,line width=1mm] (A) -- (C);}
-\onslide<4>{\draw[->,red,line width=1mm] (C) -- (B);}
-\end{tikzpicture}
-\end{center}
-\onslide<4>{this might make sense for ``raw'' terms, but not at all
-for $\alpha$-equated terms}
-\end{itemize}}
-\only<5>{
-\begin{itemize}
-\item we allow multiple ``binders'' and ``bodies''\smallskip
-\begin{center}
-\begin{tabular}{l}
-\isacommand{bind} a b c \ldots \isacommand{in} x y z \ldots\\
-\isacommand{bind (set)} a b c \ldots \isacommand{in} x y z \ldots\\
-\isacommand{bind (set+)} a b c \ldots \isacommand{in} x y z \ldots
-\end{tabular}
-\end{center}\bigskip\medskip
-the reason is that with our definition of $\alpha$-equivalence\medskip
-\begin{center}
-\begin{tabular}{l}
-\isacommand{bind (set+)} as \isacommand{in} x y $\not\Leftrightarrow$\\
-\hspace{8mm}\isacommand{bind (set+)} as \isacommand{in} x, \isacommand{bind (set+)} as \isacommand{in} y
-\end{tabular}
-\end{center}\medskip
-same with \isacommand{bind (set)}
-\end{itemize}}
-\end{itemize}
-\end{frame}}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-*}
-text_raw {*
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
-\begin{frame}<1>
-\frametitle{\begin{tabular}{c}Alpha-Equivalence\end{tabular}}
-\mbox{}\\[-3mm]
-\begin{itemize}
-\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}$\\
-\phantom{\;\;\;\;$\lambda b.$\;\;\;\;\;\;}$\text{if}\;b \fresh t\;
-\text{then}\;(a\;b)\act t\;\text{else}\;\text{error}$
-\end{tabular}
-\end{center}
-\end{itemize}
-\begin{textblock}{10}(2,14)
-\footnotesize $^*$ alpha-equality coincides with equality on functions
-\end{textblock}
-\end{frame}}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-*}
-text_raw {*
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
-\begin{frame}<1->
-\frametitle{\begin{tabular}{c}New Design\end{tabular}}
-\mbox{}\\[4mm]
-\begin{center}
-\begin{tikzpicture}
-{\draw (0,0) node[inner sep=3mm, ultra thick, draw=fg, rounded corners=2mm]
-(A) {\begin{minipage}{1.1cm}bind.\\spec.\end{minipage}};}
-{\draw (3,0) node[inner sep=3mm, ultra thick, draw=fg, rounded corners=2mm]
-(B) {\begin{minipage}{1.1cm}raw\\terms\end{minipage}};}
-\alt<2>
-{\draw (6,0) node[inner sep=3mm, ultra thick, draw=red, rounded corners=2mm]
-(C) {\textcolor{red}{\begin{minipage}{1.1cm}$\alpha$-\\equiv.\end{minipage}}};}
-{\draw (6,0) node[inner sep=3mm, ultra thick, draw=fg, rounded corners=2mm]
-(C) {\begin{minipage}{1.1cm}$\alpha$-\\equiv.\end{minipage}};}
-{\draw (0,-3) node[inner sep=3mm, ultra thick, draw=fg, rounded corners=2mm]
-(D) {\begin{minipage}{1.1cm}quot.\\type\end{minipage}};}
-{\draw (3,-3) node[inner sep=3mm, ultra thick, draw=fg, rounded corners=2mm]
-(E) {\begin{minipage}{1.1cm}lift\\thms\end{minipage}};}
-{\draw (6,-3) node[inner sep=3mm, ultra thick, draw=fg, rounded corners=2mm]
-(F) {\begin{minipage}{1.1cm}add.\\thms\end{minipage}};}
-\draw[->,fg!50,line width=1mm] (A) -- (B);
-\draw[->,fg!50,line width=1mm] (B) -- (C);
-\draw[->,fg!50,line width=1mm, line join=round, rounded corners=2mm]
-(C) -- (8,0) -- (8,-1.5) -- (-2,-1.5) -- (-2,-3) -- (D);
-\draw[->,fg!50,line width=1mm] (D) -- (E);
-\draw[->,fg!50,line width=1mm] (E) -- (F);
-\end{tikzpicture}
-\end{center}
-\end{frame}}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-*}
 text_raw {*
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \mode<presentation>{
 \begin{frame}<1-8>
 \mbox{}\\[-3mm]
 \begin{itemize}
 \item lets first look at pairs\bigskip\medskip
-\begin{tabular}{@ {\hspace{1cm}}l}
+\textcolor{blue}{\begin{tabular}{@ {\hspace{1cm}}l}
-$(as, x) \onslide<2->{\approx\!}\makebox[0mm][l]{\only<2-6>{${}_{\text{set}}$}%
+$(as, x) \onslide<2->{\approx\!}\makebox[5mm][l]{\only<2-6>{${}_{\text{set}}$}%
 \only<7>{${}_{\text{\alert{list}}}$}%
 \only<8>{${}_{\text{\alert{set+}}}$}}%
-\onslide<3->{^{R,\text{fv}}}\,\onslide<2->{(bs,y)}$
+\,\onslide<2->{(bs,y)}$
-\end{tabular}\bigskip
+\end{tabular}}\bigskip
 \end{itemize}
 \only<1>{
 \begin{textblock}{8}(3,8.5)
 \begin{tabular}{l@ {\hspace{2mm}}p{8cm}}
-& $as$ is a set of names\ldots the binders\\
+& \textcolor{blue}{$as$} is a set of names\ldots the binders\\
-& $x$ is the body (might be a tuple)\\
+& \textcolor{blue}{$x$} is the body (might be a tuple)\\
-& $\approx_{\text{set}}$ is where the cardinality
+& \textcolor{blue}{$\approx_{\text{set}}$} is where the cardinality
 of the binders has to be the same\\
 \end{tabular}
 \end{textblock}}
 \only<4->{
 \begin{textblock}{12}(5,8)
+\textcolor{blue}{
 \begin{tabular}{ll@ {\hspace{1mm}}l}
 $\dn$ & \onslide<5->{$\exists \pi.\,$} & $\text{fv}(x) - as = \text{fv}(y) - bs$\\[1mm]
 & \onslide<5->{$\;\;\;\wedge$} & \onslide<5->{$\text{fv}(x) - as \fresh^* \pi$}\\[1mm]
-& \onslide<5->{$\;\;\;\wedge$} & \onslide<5->{$(\pi \act x)\;R\;y$}\\[1mm]
+& \onslide<5->{$\;\;\;\wedge$} & \onslide<5->{$(\pi \act x) = y$}\\[1mm]
-& \onslide<6-7>{$\;\;\;\wedge$} & \onslide<6-7>{$\pi \act as = bs$}\\
+& \only<6-7>{$\;\;\;\wedge$}\only<8>{\textcolor{gray}{\xout{$\;\;\;\wedge$}}} &
-\end{tabular}
+\only<6-7>{$\pi \act as = bs$}\only<8>{\textcolor{gray}{\xout{$\pi \act as = bs$}}}\\
+\end{tabular}}
 \end{textblock}}
 \only<7>{
 \begin{textblock}{7}(3,13.8)
 \footnotesize $^*$ $as$ and $bs$ are \alert{lists} of names
 \begin{frame}<1-3>
 \frametitle{\begin{tabular}{c}Examples\end{tabular}}
 \mbox{}\\[-3mm]
 \begin{itemize}
-\item lets look at ``type-schemes'':\medskip\medskip
+\item lets look at type-schemes:\medskip\medskip
 \begin{center}
-$(as, x) \approx\!\makebox[0mm][l]{${}_{\text{set}}$}\only<1>{{}^{R,\text{fv}}}\only<2->{{}^{\alert{=},\alert{\text{fv}}}} (bs, y)$
+\textcolor{blue}{$(as, x) \approx\!\makebox[5mm][l]{${}_{\text{set}}$} (bs, y)$}
 \end{center}\medskip
 \onslide<2->{
 \begin{center}
+\textcolor{blue}{
 \begin{tabular}{l}
 $\text{fv}(x) = \{x\}$\\[1mm]
 $\text{fv}(T_1 \rightarrow T_2) = \text{fv}(T_1) \cup \text{fv}(T_2)$\\
-\end{tabular}
+\end{tabular}}
 \end{center}}
 \end{itemize}
 \only<3->{
 \begin{frame}<1-2>
 \frametitle{\begin{tabular}{c}Examples\end{tabular}}
 \mbox{}\\[-3mm]
 \begin{center}
+\textcolor{blue}{
 \only<1>{$(\{x, y\}, x \rightarrow y) \approx_? (\{x, y\}, y \rightarrow x)$}
-\only<2>{$([x, y], x \rightarrow y) \approx_? ([x, y], y \rightarrow x)$}
+\only<2>{$([x, y], x \rightarrow y) \approx_? ([x, y], y \rightarrow x)$}}
 \end{center}
 \begin{itemize}
-\item $\approx_{\text{set+}}$, $\approx_{\text{set}}$%
+\item \textcolor{blue}{$\approx_{\text{set+}}$, $\approx_{\text{set}}$%
-\only<2>{, \alert{$\not\approx_{\text{list}}$}}
+\only<2>{, \alert{$\not\approx_{\text{list}}$}}}
 \end{itemize}
 \only<1->{
 \begin{textblock}{4}(0.3,12)
 \begin{frame}<1-2>
 \frametitle{\begin{tabular}{c}Examples\end{tabular}}
 \mbox{}\\[-3mm]
 \begin{center}
-\only<1>{$(\{x\}, x) \approx_? (\{x, y\}, x)$}
+\textcolor{blue}{\only<1>{$(\{x\}, x) \approx_? (\{x, y\}, x)$}}
 \end{center}
 \begin{itemize}
-\item $\approx_{\text{set+}}$, $\not\approx_{\text{set}}$,
+\item \textcolor{blue}{$\approx_{\text{set+}}$, $\not\approx_{\text{set}}$,
-$\not\approx_{\text{list}}$
+$\not\approx_{\text{list}}$}
 \end{itemize}
 \only<1->{
 \begin{textblock}{4}(0.3,12)
 \end{itemize}
 \end{minipage}};
 \end{tikzpicture}
 \end{textblock}}
-\end{frame}}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-*}
-text_raw {*
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
-\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]{${}_{{}*{}}$}^{=,\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}_*$\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)\;^*$\\
-\end{tabular}}
-\end{center}
-\end{itemize}
-\only<1->{
-\begin{textblock}{8}(12,3.8)
-\footnotesize $^*$ set, set+, list
-\end{textblock}}
-\end{frame}}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-*}
-text_raw {*
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
-\begin{frame}<1>
-\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}
-\begin{itemize}
-\item we cannot represent this as\medskip
-\begin{center}
-$\text{let}\;[x_1,\ldots,x_n]\alert{.}s\;\;[t_1,\ldots,t_n]$
-\end{center}\bigskip
-because\medskip
-\begin{center}
-$\text{let}\;[x].s\;\;[t_1,t_2]$
-\end{center}
-\end{itemize}
 \end{frame}}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 *}
 text_raw {*
 *}
 text_raw {*
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \mode<presentation>{
-\begin{frame}<1-2>
+\begin{frame}<1>[c]
-\frametitle{\begin{tabular}{c}``Raw'' Definitions\end{tabular}}
+\frametitle{\begin{tabular}{c}Binding Functions\end{tabular}}
+\begin{center}
+\begin{tikzpicture}
+\node (A) at (-0.5,1) {Foo $(\lambda y. \lambda x. t)$};
+\node (B) at ( 1.5,1) {$s$};
+\onslide<1>{\node (C) at (0.5,-0.5) {$\{y, x\}$};}
+\onslide<1>{\draw[->,red,line width=1mm] (A) -- (C);}
+\onslide<1>{\draw[->,red,line width=1mm] (C) -- (B);}
+\end{tikzpicture}
+\end{center}
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+text_raw {*
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}<1->[t]
+\frametitle{\begin{tabular}{c}Binder Clauses\end{tabular}}
+\begin{itemize}
+\item We need for a bound variable to have a `clear scope', and bound
+variables should not be free and bound at the same time.\bigskip
+\end{itemize}
+\begin{center}
+\only<1>{
+\begin{tabular}{@ {\hspace{-5mm}}l}
+\alert{\bf shallow binders}\\
+\hspace{4mm}Lam x::name t::trm\hspace{4mm} \isacommand{bind} x \isacommand{in} t\\
+\hspace{4mm}All xs::name set T::ty\hspace{4mm} \isacommand{bind} xs \isacommand{in} T\\
+\hspace{4mm}Foo x::name t$_1$::trm t$_2$::trm\hspace{4mm}
+\isacommand{bind} x \isacommand{in} t$_1$, \isacommand{bind} x \isacommand{in} t$_2$\\
+\hspace{4mm}Bar x::name t$_1$::trm t$_2$::trm\hspace{4mm}
+\isacommand{bind} x \isacommand{in} t$_1$ t$_2$\\
+\end{tabular}}
+\only<2>{
+\begin{tabular}{@ {\hspace{-5mm}}l}
+\alert{\bf deep binders} \\
+\hspace{4mm}Let as::assns t::trm\hspace{4mm} \isacommand{bind} bn(as) \isacommand{in} t\\
+\hspace{4mm}Foo as::assns t$_1$::trm t$_2$::trm\\
+\hspace{20mm}\isacommand{bind} bn(as) \isacommand{in} t$_1$, \isacommand{bind} bn(as) \isacommand{in} t$_2$\\[4mm]
+\makebox[0mm][l]{\alert{$\times$}}\hspace{4mm}Bar as::assns t$_1$::trm t$_2$::trm\\
+\hspace{20mm}\isacommand{bind} bn$_1$(as) \isacommand{in} t$_1$, \isacommand{bind} bn$_2$(as) \isacommand{in} t$_2$\\
+\end{tabular}}
+\only<3>{
+\begin{tabular}{@ {\hspace{-5mm}}l}
+{\bf deep \alert{recursive} binders} \\
+\hspace{4mm}Let\_rec as::assns t::trm\hspace{4mm} \isacommand{bind} bn(as) \isacommand{in} t as\\[4mm]
+\makebox[0mm][l]{\alert{$\times$}}\hspace{4mm}Foo\_rec as::assns t$_1$::trm t$_2$::trm\hspace{4mm}\\
+\hspace{20mm}\isacommand{bind} bn(as) \isacommand{in} t$_1$ as, \isacommand{bind} bn(as) \isacommand{in} t$_2$\\
+\end{tabular}}
+\end{center}
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+text_raw {*
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}<2-5>
+\frametitle{\begin{tabular}{c}Our Work\end{tabular}}
 \mbox{}\\[-6mm]
-\mbox{}\hspace{10mm}
+\begin{center}
-\begin{tabular}{ll}
+\begin{tikzpicture}[scale=1.5]
-\multicolumn{2}{l}{\isacommand{datatype} trm $=$}\\
+%%%\draw[step=2mm] (-4,-1) grid (4,1);
-\hspace{5mm}\phantom{$|$} Var name\\
-\hspace{5mm}$|$ App trm trm\\
+\onslide<1>{\draw[very thick] (0.7,0.4) circle (4.25mm);}
-\hspace{5mm}$|$ Lam name trm\\
+\onslide<1>{\draw[rounded corners=1mm, very thick] ( 0.0,-0.8) rectangle ( 1.8, 0.9);}
-\hspace{5mm}$|$ Let assns trm\\
+\onslide<1->{\draw[rounded corners=1mm, very thick] (-1.95,0.85) rectangle (-2.85,-0.05);}
-\multicolumn{2}{l}{\isacommand{and} assns $=$}\\
-\multicolumn{2}{l}{\hspace{5mm}\phantom{$|$} ANil}\\
+\onslide<1>{\draw (-2.0, 0.845) --  (0.7,0.845);}
-\multicolumn{2}{l}{\hspace{5mm}$|$ ACons name trm assns}\\[5mm]
+\onslide<1>{\draw (-2.0,-0.045)  -- (0.7,-0.045);}
-\multicolumn{2}{l}{\isacommand{function} bn \isacommand{where}}\\
-\multicolumn{2}{l}{\hspace{5mm}\phantom{$|$} bn(ANil) $=$ $[]$}\\
+\onslide<1>{\alert{\draw ( 0.7, 0.4) node {\footnotesize\begin{tabular}{@ {}c@ {}}$\alpha$-\\[-1mm]classes\end{tabular}};}}
-\multicolumn{2}{l}{\hspace{5mm}$|$ bn(ACons a t as) $=$ $[$a$]$ @ bn(as)}\\
+\onslide<1->{\alert{\draw (-2.4, 0.4) node {\footnotesize\begin{tabular}{@ {}c@ {}}$\alpha$-eq.\\[-1mm]terms\end{tabular}};}}
-\end{tabular}
+\onslide<1>{\draw (1.8, 0.48) node[right=-0.1mm]
+{\footnotesize\begin{tabular}{@ {}l@ {}}existing\\[-1mm] type\\ \onslide<1>{\alert{(sets of raw terms)}}\end{tabular}};}
-\only<2>{
+\onslide<1>{\draw (0.9, -0.35) node {\footnotesize\begin{tabular}{@ {}l@ {}}non-empty\\[-1mm]subset\end{tabular}};}
-\begin{textblock}{5}(10,5)
+\onslide<1->{\draw (-3.25, 0.55) node {\footnotesize\begin{tabular}{@ {}l@ {}}new\\[-1mm]type\end{tabular}};}
-$+$ \begin{tabular}{l}automatically\\
-generate fv's\end{tabular}
+\onslide<1>{\draw[<->, very thick] (-1.8, 0.3) -- (-0.1,0.3);}
-\end{textblock}}
+\onslide<1>{\draw (-0.95, 0.3) node[above=0mm] {\footnotesize{}isomorphism};}
-\end{frame}}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\onslide<1>{\draw[->, line width=2mm, red] (-1.0,-0.4) -- (0.35,0.16);}
-*}
+\end{tikzpicture}
+\end{center}
-text_raw {*
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{textblock}{9.5}(6,3.5)
-\mode<presentation>{
+\begin{itemize}
-\begin{frame}<1>
+\item<1-> defined fv and $\alpha$
-\frametitle{\begin{tabular}{c}\LARGE``Raw'' Alpha-Equivalence\end{tabular}}
+\item<3-> derived a reasoning infrastructure ($\fresh$, distinctness, injectivity, cases,\ldots)
-\mbox{}\\[6mm]
+\item<4-> a (weak) induction principle
+\item<5-> derive a {\bf stronger} induction principle (Barendregt variable convention built in)\\
 \begin{center}
-Lam x::name t::trm \hspace{10mm}\isacommand{bind} x \isacommand{in} t\\
+\textcolor{blue}{Foo ($\lambda x. \lambda y. t$) ($\lambda u. \lambda v. s$)}
 \end{center}
+\end{itemize}
+\end{textblock}
-\[
-\infer[\text{Lam-}\!\approx_\alpha]
-{\text{Lam}\;x\;t \approx_\alpha \text{Lam}\;x'\;t'}
+\end{frame}}
-{([x], t) \approx\!\makebox[0mm][l]{${}_{\text{list}}$}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-^{\approx_\alpha,\text{fv}} ([x'], t')}
+*}
-\]
-\end{frame}}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-*}
-text_raw {*
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
-\begin{frame}<1>
-\frametitle{\begin{tabular}{c}\LARGE``Raw'' Alpha-Equivalence\end{tabular}}
-\mbox{}\\[6mm]
-\begin{center}
-Lam x::name y::name t::trm s::trm \hspace{5mm}\isacommand{bind} x y \isacommand{in} t s\\
-\end{center}
-\[
-\infer[\text{Lam-}\!\approx_\alpha]
-{\text{Lam}\;x\;y\;t\;s \approx_\alpha \text{Lam}\;x'\;y'\;t'\;s'}
-{([x, y], (t, s)) \approx\!\makebox[0mm][l]{${}_{\text{list}}$}
-^{R, fv} ([x', y'], (t', s'))}
-\]
-\footnotesize
-where $R =\;\approx_\alpha\times\approx_\alpha$ and $fv = \text{fv}\cup\text{fv}$
-\end{frame}}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-*}
-text_raw {*
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
-\begin{frame}<1-2>
-\frametitle{\begin{tabular}{c}\LARGE``Raw'' Alpha-Equivalence\end{tabular}}
-\mbox{}\\[6mm]
-\begin{center}
-Let as::assns t::trm \hspace{10mm}\isacommand{bind} bn(as) \isacommand{in} t\\
-\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'}}
-\]\bigskip
-\onslide<1->{\small{}bn-function $\Rightarrow$ \alert{deep binders}}
-\end{frame}}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-*}
-text_raw {*
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
-\begin{frame}<1->
-\frametitle{\begin{tabular}{c}\LARGE{}$\alpha$ for Binding Functions\end{tabular}}
-\mbox{}\\[-6mm]
-\mbox{}\hspace{10mm}
-\begin{tabular}{l}
-\ldots\\
-\isacommand{binder} bn \isacommand{where}\\
-\phantom{$|$} bn(ANil) $=$ $[]$\\
-$|$ bn(ACons a t as) $=$ $[$a$]$ @ bn(as)\\
-\end{tabular}\bigskip
-\begin{center}
-\mbox{\infer{\text{ANil} \approx_\alpha^{\text{bn}} \text{ANil}}{}}\bigskip
-\mbox{\infer{\text{ACons}\;a\;t\;as \approx_\alpha^{\text{bn}} \text{ACons}\;a'\;t'\;as'}
-{t \approx_\alpha t' & as \approx_\alpha^{bn} as'}}
-\end{center}
-\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::assns 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,\text{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 our quotient package to introduce the type(s)
-of $\alpha$-equated terms
-\[
-\infer
-{\text{Lam}\;x\;t \alert{=} \text{Lam}\;x'\;t'}
-{\only<1>{([x], t) \approx\!\makebox[0mm][l]{${}_{\text{list}}$}
-^{=,\text{supp}} ([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
-\end{itemize}
-\end{frame}}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-*}
-text_raw {*
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
-\begin{frame}<1>[t]
-\frametitle{\begin{tabular}{c}Runtime is Acceptable\end{tabular}}
-\mbox{}\\[-7mm]\mbox{}
-\footnotesize
-\begin{center}
-\begin{tikzpicture}
-\draw (0,0) node[inner sep=2mm, ultra thick, draw=fg, rounded corners=2mm]
-(A) {\begin{minipage}{0.8cm}bind.\\spec.\end{minipage}};
-\draw (2,0) node[inner sep=2mm, ultra thick, draw=fg, rounded corners=2mm]
-(B) {\begin{minipage}{0.8cm}raw\\terms\end{minipage}};
-\draw (4,0) node[inner sep=2mm, ultra thick, draw=fg, rounded corners=2mm]
-(C) {\begin{minipage}{0.8cm}$\alpha$-\\equiv.\end{minipage}};
-\draw (0,-2) node[inner sep=2mm, ultra thick, draw=fg, rounded corners=2mm]
-(D) {\begin{minipage}{0.8cm}quot.\\type\end{minipage}};
-\draw (2,-2) node[inner sep=2mm, ultra thick, draw=fg, rounded corners=2mm]
-(E) {\begin{minipage}{0.8cm}lift\\thms\end{minipage}};
-\draw (4,-2) node[inner sep=2mm, ultra thick, draw=fg, rounded corners=2mm]
-(F) {\begin{minipage}{0.8cm}add.\\thms\end{minipage}};
-\draw[->,fg!50,line width=1mm] (A) -- (B);
-\draw[->,fg!50,line width=1mm] (B) -- (C);
-\draw[->,fg!50,line width=1mm, line join=round, rounded corners=2mm]
-(C) -- (5,0) -- (5,-1) -- (-1,-1) -- (-1,-2) -- (D);
-\draw[->,fg!50,line width=1mm] (D) -- (E);
-\draw[->,fg!50,line width=1mm] (E) -- (F);
-\end{tikzpicture}
-\end{center}
-\begin{itemize}
-\item Core Haskell: 11 types, 49 term-constructors, 7 binding functions
-\begin{center}
-$\sim$ 2 mins
-\end{center}
-\end{itemize}
-\end{frame}}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-*}
-text_raw {*
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
-\begin{frame}<1->
-\frametitle{\begin{tabular}{c}Interesting Phenomenon\end{tabular}}
-\mbox{}\\[-6mm]
-\small
-\mbox{}\hspace{20mm}
-\begin{tabular}{ll}
-\multicolumn{2}{l}{\isacommand{nominal\_datatype} trm $=$}\\
-\hspace{5mm}\phantom{$|$} Var name\\
-\hspace{5mm}$|$ App trm trm\\
-\hspace{5mm}$|$ Lam x::name t::trm
-& \isacommand{bind} x \isacommand{in} t\\
-\hspace{5mm}$|$ Let as::assns t::trm
-& \isacommand{bind} bn(as) \isacommand{in} t\\
-\multicolumn{2}{l}{\isacommand{and} assns $=$}\\
-\multicolumn{2}{l}{\hspace{5mm}\phantom{$|$} ANil}\\
-\multicolumn{2}{l}{\hspace{5mm}$|$ ACons name trm assns}\\
-\multicolumn{2}{l}{\isacommand{binder} bn \isacommand{where}}\\
-\multicolumn{2}{l}{\hspace{5mm}\phantom{$|$} bn(ANil) $=$ $[]$}\\
-\multicolumn{2}{l}{\hspace{5mm}$|$ bn(ACons a t as) $=$ $[$a$]$ @ bn(as)}\\
-\end{tabular}\bigskip\medskip
-we cannot quotient assns: ACons a \ldots $\not\approx_\alpha$ ACons b \ldots
-\only<1->{
-\begin{textblock}{8}(0.2,7.3)
-\alert{\begin{tabular}{p{2.6cm}}
-\raggedright\footnotesize{}Should a ``naked'' assns be quotient?
-\end{tabular}\hspace{-3mm}
-$\begin{cases}
-\mbox{} \\ \mbox{}
-\end{cases}$}
-\end{textblock}}
-\end{frame}}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-*}
 text_raw {*
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \mode<presentation>{
 \begin{frame}<1->
 \item the user does not see anything of the raw level\medskip
 \only<1>{\begin{center}
 Lam a (Var a) \alert{$=$} Lam b (Var b)
 \end{center}\bigskip}
-\item<2-> we have not yet done function definitions (will come soon and
+\item<2-> it took quite some time to get here, but it seems worthwhile
-we hope to make improvements over the old way there too)\medskip
-\item<3-> it took quite some time to get here, but it seems worthwhile
 (Barendregt's variable convention is unsound in general,
-found bugs in two paper proofs, quotient package, POPL 2011 tutorial)\medskip
+found bugs in two paper proofs)\bigskip\medskip
-\end{itemize}
+\item<3-> \textcolor{blue}{http://isabelle.in.tum.de/nominal/}
+\end{itemize}
-\end{frame}}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-*}
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-text_raw {*
+*}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
-\begin{frame}<1->[c]
-\frametitle{\begin{tabular}{c}Future Work\end{tabular}}
-\mbox{}\\[-6mm]
-\begin{itemize}
-\item Function definitions
-\end{itemize}
-\end{frame}}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-*}
 text_raw {*
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \mode<presentation>{
 \mode<presentation>{
 \begin{frame}<1-2>[c]
 \frametitle{\begin{tabular}{c}Examples\end{tabular}}
 \mbox{}\\[-6mm]
+\textcolor{blue}{
 \begin{center}
 $(\{a,b\}, a \rightarrow b) \approx_\alpha (\{a, b\}, a \rightarrow b)$
 $(\{a,b\}, a \rightarrow b) \approx_\alpha (\{a, b\}, b \rightarrow a)$
-\end{center}
+\end{center}}
+\textcolor{blue}{
 \begin{center}
 $(\{a,b\}, (a \rightarrow b, a \rightarrow b))$\\
 \hspace{17mm}$\not\approx_\alpha (\{a, b\}, (a \rightarrow b, b \rightarrow a))$
-\end{center}
+\end{center}}
 \onslide<2->
 {1.) \hspace{3mm}\isacommand{bind (set)} as \isacommand{in} $\tau_1$,
 \isacommand{bind (set)} as \isacommand{in} $\tau_2$\medskip
 \end{frame}}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 *}
 (*<*)
 end
 (*>*)

changeset 2751	3b8232f56941
parent 2750	43283267737c
child 3224	cf451e182bf0