(*<*)+ −
theory SlidesB+ −
imports "~~/src/HOL/Library/LaTeXsugar" "../Nominal/Nominal2"+ −
begin+ −
+ −
notation (latex output)+ −
set ("_") and+ −
Cons ("_::/_" [66,65] 65) + −
+ −
(*>*)+ −
+ −
+ −
text_raw {*+ −
%% was \begin{colormixin}{20!averagebackgroundcolor}+ −
%% + −
%% is \begin{colormixin}{50!averagebackgroundcolor}+ −
\renewcommand{\slidecaption}{Dagstuhl, 14 October 2013}+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
\mode<presentation>{+ −
\begin{frame}+ −
\frametitle{%+ −
\begin{tabular}{@ {}c@ {}}+ −
\Huge Nominal Isabelle\\[0mm]+ −
\Large or, How Not to be Intimidated by\\[-3mm]+ −
\Large the Variable Convention\\[-5mm]+ −
\end{tabular}}+ −
+ −
\begin{center}+ −
Christian Urban\\[1mm]+ −
King's College London\\[-4mm]\mbox{}+ −
\end{center}+ −
+ −
\begin{center}+ −
\begin{block}{}+ −
\color{gray}+ −
\small+ −
{\bf\mbox{}\hspace{-1.5mm}Variable Convention:}\\[1mm] + −
If $M_1,\ldots,M_n$ occur in a certain mathematical context+ −
(e.g. definition, proof), then in these terms all bound variables + −
are chosen to be different from the free variables.\\[2mm]+ −
+ −
\footnotesize\hfill Henk Barendregt in ``The Lambda-Calculus: Its Syntax and Semantics''+ −
\end{block}+ −
\end{center}+ −
+ −
\end{frame}}+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + −
+ −
*}+ −
+ −
text_raw {*+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
\mode<presentation>{+ −
\begin{frame}<1->[c]+ −
\frametitle{}+ −
+ −
\begin{center}+ −
\begin{tabular}{@ {\hspace{-2mm}}c@ {}}+ −
\includegraphics[scale=0.36]{phd-2.jpg}\,+ −
\includegraphics[scale=0.36]{phd-1.jpg}\\+ −
\hfill\textcolor{gray}{\small dinner after my PhD examination}+ −
\end{tabular}+ −
\end{center}+ −
+ −
\end{frame}}+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + −
*}+ −
+ −
text_raw {*+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
\mode<presentation>{+ −
\begin{frame}<1->[c]+ −
\frametitle{}+ −
+ −
\begin{itemize}+ −
\item \normalsize Aim: develop Nominal Isabelle for reasoning formally about + −
programming languages\\[-10mm]\mbox{}+ −
\end{itemize}+ −
+ −
\begin{center}+ −
\begin{block}{}+ −
\color{gray}+ −
\footnotesize+ −
{\bf\mbox{}\hspace{-1.5mm}Variable Convention:}\\[0mm] + −
If $M_1,\ldots,M_n$ occur in a certain mathematical context+ −
(e.g. definition, proof), then in these terms all bound variables + −
are chosen to be different from the free variables.\hfill ---Henk Barendregt+ −
\end{block}+ −
\end{center}\pause+ −
+ −
\mbox{}\\[-19mm]\mbox{}+ −
+ −
\begin{itemize}+ −
\item found an error in an ACM journal paper by Bob Harper and Frank Pfenning + −
about LF (and fixed it in three ways)+ −
\item found also fixable errors in my Ph.D.-thesis about cut-elimination+ −
(examined by Henk Barendregt and Andy Pitts)+ −
\item found that the variable convention can in principle be used for proving false+ −
\end{itemize}+ −
+ −
\end{frame}}+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + −
*}+ −
+ −
+ −
text_raw {*+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
\mode<presentation>{+ −
\begin{frame}<1->[c]+ −
\frametitle{Nominal Techniques}+ −
+ −
\begin{itemize}+ −
\item Andy Pitts showed me that permutations\\ preserve $\alpha$-equivalence:+ −
\begin{center}+ −
\smath{t_1 \approx_{\alpha} t_2 \quad \Rightarrow\quad \pi \act t_1 \approx_{\alpha} \pi \act t_2} + −
\end{center}+ −
+ −
\item also permutations and substitutions commute, if you suspend permutations+ −
in front of variables+ −
\begin{center}+ −
\smath{\pi\act\sigma(t) = \sigma(\pi\act t)}+ −
\end{center}\medskip\medskip+ −
+ −
\item this allowed us to define as simple Nominal Unification algorithm\medskip+ −
\begin{center}+ −
\smath{\nabla \vdash t \approx^?_{\alpha} t'}\hspace{2cm}+ −
\smath{\nabla \vdash a \fresh^? t}+ −
\end{center}+ −
\end{itemize}+ −
+ −
%\begin{textblock}{3}(13.1,1.3)+ −
%\includegraphics[scale=0.26]{andrewpitts.jpg}+ −
%\end{textblock}+ −
+ −
\end{frame}}+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + −
*}+ −
+ −
text_raw {*+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
\mode<presentation>{+ −
\begin{frame}[c]+ −
\frametitle{Nominal Isabelle}+ −
+ −
\begin{itemize}+ −
\item a general theory about atoms and permutations\medskip+ −
\begin{itemize}+ −
\item sorted atoms and+ −
\item sort-respecting permutations\bigskip+ −
\end{itemize}+ −
+ −
\item support and freshness+ −
\begin{center}+ −
\begin{tabular}{l}+ −
\smath{\textit{supp}(x) \dn \{ a \mid \textit{infinite}\,\{ b \mid \swap{a}{b}\act x \not= x\}\}}\\[2mm]+ −
\smath{a \fresh x \dn a \notin \textit{supp}(x)}+ −
\end{tabular}+ −
\end{center}\bigskip\pause+ −
+ −
\item allow users to reason about alpha-equivalence classes as if they were + −
syntax trees+ −
%+ −
%\item $\alpha$-equivalence+ −
%\begin{center}+ −
%\begin{tabular}{l}+ −
%\smath{as.x \approx_\alpha bs.y \dn}\\[2mm]+ −
%\hspace{2cm}\smath{\exists \pi.\;\text{supp}(x) - as = \text{supp}(y) - bs}\\ + −
%\hspace{2cm}\smath{\;\wedge\; \text{supp}(x) - as \fresh \pi}\\+ −
%\hspace{2cm}\smath{\;\wedge\; \pi \act x = y}+ −
%\end{tabular}+ −
%\end{center}+ −
\end{itemize}+ −
+ −
\end{frame}}+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + −
*}+ −
+ −
text_raw {*+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
\mode<presentation>{+ −
\begin{frame}<1-7>+ −
\frametitle{New Types in HOL}+ −
+ −
\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 \boldmath$\alpha$-equivalence}}+ −
\end{center}+ −
+ −
\begin{textblock}{9}(2.8,12.5)+ −
\only<7>{+ −
\begin{tikzpicture}+ −
\draw (0,0) node[fill=cream, text width=8.5cm, thick, draw=red, rounded corners=1mm] (nn)+ −
{The ``new types mechanism'' is the reason why there is no Nominal Coq.};+ −
\end{tikzpicture}}+ −
\end{textblock}+ −
+ −
\end{frame}}+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + −
*}+ −
+ −
text_raw {*+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
\mode<presentation>{+ −
\begin{frame}<1-3>[c]+ −
\frametitle{HOL vs.~Nominal}+ −
+ −
\begin{itemize}+ −
\item Nominal logic by Pitts is incompatible + −
with choice principles\medskip+ −
+ −
\item but HOL includes Hilbert's epsilon\pause\bigskip+ −
+ −
\item The solution: Do not require that everything has finite support\medskip+ −
+ −
\begin{center}+ −
\smath{\onslide<1-2>{\textit{finite}(\textit{supp}(x)) \quad\Rightarrow\quad} a \fresh a.x}+ −
\end{center}+ −
\end{itemize}+ −
+ −
\end{frame}}+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + −
*}+ −
+ −
text_raw {*+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
\mode<presentation>{+ −
\begin{frame}<1-5>+ −
\frametitle{\begin{tabular}{c}Our Work\end{tabular}}+ −
\mbox{}\\[-6mm]+ −
+ −
\begin{center}+ −
\begin{tikzpicture}[scale=1.5]+ −
%%%\draw[step=2mm] (-4,-1) grid (4,1);+ −
+ −
\onslide<1>{\draw[very thick] (0.7,0.4) circle (4.25mm);}+ −
\onslide<1>{\draw[rounded corners=1mm, very thick] ( 0.0,-0.8) rectangle ( 1.8, 0.9);}+ −
\onslide<1->{\draw[rounded corners=1mm, very thick] (-1.95,0.85) rectangle (-2.85,-0.05);}+ −
+ −
\onslide<1>{\draw (-2.0, 0.845) -- (0.7,0.845);}+ −
\onslide<1>{\draw (-2.0,-0.045) -- (0.7,-0.045);}+ −
+ −
\onslide<1>{\alert{\draw ( 0.7, 0.4) node {\footnotesize\begin{tabular}{@ {}c@ {}}$\alpha$-\\[-1mm]classes\end{tabular}};}}+ −
\onslide<1->{\alert{\draw (-2.4, 0.4) node {\footnotesize\begin{tabular}{@ {}c@ {}}$\alpha$-eq.\\[-1mm]terms\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}};}+ −
\onslide<1>{\draw (0.9, -0.35) node {\footnotesize\begin{tabular}{@ {}l@ {}}non-empty\\[-1mm]subset\end{tabular}};}+ −
\onslide<1->{\draw (-3.25, 0.55) node {\footnotesize\begin{tabular}{@ {}l@ {}}new\\[-1mm]type\end{tabular}};}+ −
+ −
\onslide<1>{\draw[<->, very thick] (-1.8, 0.3) -- (-0.1,0.3);}+ −
\onslide<1>{\draw (-0.95, 0.3) node[above=0mm] {\footnotesize{}isomorphism};}+ −
+ −
%%\onslide<1>{\draw[->, line width=2mm, red] (-1.0,-0.4) -- (0.35,0.16);}+ −
\end{tikzpicture}+ −
\end{center}+ −
+ −
\begin{textblock}{9.5}(6,3.5)+ −
\begin{itemize}+ −
\item<1-> define fv and $\alpha$+ −
\item<2-> build quotient / new type+ −
\item<3-> derive a reasoning infrastructure ($\fresh$, distinctness, injectivity, cases,\ldots) + −
\item<4-> derive a {\bf stronger} cases lemma+ −
\item<5-> from this, a {\bf stronger} induction principle (Barendregt variable convention built in)\\+ −
\begin{center}+ −
\textcolor{blue}{Foo ($\lambda x. \lambda y. t$) ($\lambda u. \lambda v. s$)} + −
\end{center}+ −
\end{itemize}+ −
\end{textblock}+ −
+ −
+ −
\end{frame}}+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + −
*}+ −
+ −
text_raw {*+ −
+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
\mode<presentation>{+ −
\begin{frame}+ −
\frametitle{Nominal Isabelle} + −
+ −
\begin{itemize}+ −
\item Users can for example define lambda-terms as:+ −
\end{itemize}+ −
*}+ −
+ −
atom_decl name text_raw {*\medskip\isanewline *}+ −
nominal_datatype lam =+ −
Var name+ −
| App lam lam + −
| Lam x::name t::lam binds x in t ("Lam _. _")+ −
+ −
+ −
text_raw {*+ −
\mbox{}\bigskip+ −
+ −
\begin{itemize}+ −
\item These are \underline{\bf named} alpha-equivalence classes, for example+ −
\end{itemize}+ −
+ −
\begin{center}+ −
\gb{@{text "Lam a.(Var a)"}} \alert{$\,=\,$} \gb{@{text "Lam b.(Var b)"}}+ −
\end{center}+ −
+ −
\end{frame}}+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + −
+ −
*}+ −
+ −
text_raw {*+ −
+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
\mode<presentation>{+ −
\begin{frame}+ −
\frametitle{\Large (Weak) Induction Principles} + −
+ −
\begin{itemize}+ −
\item The usual induction principle for lambda-terms is as follows:+ −
+ −
\begin{center}+ −
\mbox{}\hspace{-1mm}\begin{beamercolorbox}[sep=1mm, wd=9cm]{boxcolor}+ −
\centering\smath{%+ −
\infer{P\,t}+ −
{\begin{array}{l}+ −
\forall x.\;P\,x\\[2mm]+ −
\forall t_1\,t_2.\;P\,t_1\wedge P\,t_2\Rightarrow P\,(t_1\;t_2)\\[2mm]+ −
\forall x\,t.\;P\,t\Rightarrow P\,(\lambda x.t)\\+ −
\end{array}+ −
}}+ −
\end{beamercolorbox}+ −
\end{center}+ −
+ −
\item It requires us in the lambda-case to show the property \smath{P} for+ −
all binders \smath{x}.\medskip\\ + −
+ −
(This nearly always requires renamings and they can be + −
tricky to automate.)+ −
\end{itemize}+ −
+ −
\end{frame}}+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + −
+ −
*}+ −
+ −
+ −
text_raw {*+ −
+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
\mode<presentation>{+ −
\begin{frame}+ −
\frametitle{\Large Strong Induction Principles} + −
+ −
\begin{itemize}+ −
\item Therefore we introduced the following strong induction principle:+ −
+ −
\begin{center}+ −
\mbox{}\hspace{-2mm}\begin{beamercolorbox}[sep=1mm, wd=11.5cm]{boxcolor}+ −
\centering\smath{%+ −
\infer{\tikz[remember picture] \node[inner sep=1mm] (n1a) {\alert<4>{$P$}};%+ −
\tikz[remember picture] \node[inner sep=1mm] (n2a) {\alert<3>{$c$}};%+ −
\tikz[remember picture] \node[inner sep=1mm] (n3a) {\alert<2>{$t$}};}+ −
{\begin{array}{l}+ −
\forall x\,c.\;P\,c\;x\\[2mm]+ −
\forall t_1\,t_2\,c.\;(\forall d.\,P d\,t_1)\wedge (\forall d. P\,d\,t_2)+ −
\Rightarrow P\,c\;(t_1\,t_2)\\[2mm]+ −
\forall x\,t\,c.\;\alert<1>{x\fresh \alert<3>{c}} + −
\wedge (\forall d. P\,d\,t)\Rightarrow P\,c\;(\lambda x.t)+ −
\end{array}+ −
}}+ −
\end{beamercolorbox}+ −
\end{center}+ −
\end{itemize}+ −
+ −
\begin{textblock}{11}(0.9,10.9)+ −
\only<2>{+ −
\begin{tikzpicture}[remember picture]+ −
\draw (0,0) node[fill=cream, text width=10.5cm, thick, draw=red, rounded corners=1mm] (n3b)+ −
{ The variable over which the induction proceeds:\\[2mm]+ −
\hspace{3mm}``\ldots By induction over the structure of \smath{M}\ldots''};+ −
+ −
\path[overlay, ->, ultra thick, red] (n3b) edge[out=90, in=-110] (n3a);+ −
\end{tikzpicture}}+ −
+ −
\only<3>{+ −
\begin{tikzpicture}[remember picture]+ −
\draw (0,0) node[fill=cream, text width=11cm, thick, draw=red, rounded corners=1mm] (n2b)+ −
{The {\bf context} of the induction; i.e.~what the binder should be fresh for+ −
$\quad\Rightarrow$ \smath{(x,y,N,L)}:\\[2mm]+ −
``\ldots By the variable convention we can assume \mbox{\smath{z\not\equiv x,y}} + −
and \smath{z} not free in \smath{N}$\!$,\,\smath{L}\ldots''};+ −
+ −
\path[overlay, ->, ultra thick, red] (n2b) edge[out=90, in=-100] (n2a);+ −
\end{tikzpicture}}+ −
+ −
\only<4>{+ −
\begin{tikzpicture}[remember picture]+ −
\draw (0,0) node[fill=cream, text width=11cm, thick, draw=red, rounded corners=1mm] (n1b)+ −
{The property to be proved by induction:\\[-3mm]+ −
\begin{center}\small+ −
\begin{tabular}{l}+ −
\smath{\!\!\lambda+ −
(x,\!y,\!N\!,\!L).\,\lambda M.\;\,x\not=y\,\wedge\,x\fresh L\,\Rightarrow}\\[1mm]+ −
\hspace{8mm}+ −
\smath{M[x\!:=\!N][y\!:=\!L] = M[y\!:=\!L][x\!:=\!N[y\!:=\!L]]} + −
\end{tabular}+ −
\end{center}};+ −
+ −
\path[overlay, ->, ultra thick, red] (n1b) edge[out=90, in=-70] (n1a);+ −
\end{tikzpicture}}+ −
\end{textblock}+ −
+ −
\end{frame}}+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + −
+ −
*}+ −
+ −
text_raw {*+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
\mode<presentation>{+ −
\begin{frame}<1-4>+ −
\frametitle{\begin{tabular}{c}Binding Sets of Names\end{tabular}}+ −
\mbox{}\\[-3mm]+ −
+ −
\begin{itemize}+ −
\item binding sets of names has some interesting properties:\medskip+ −
+ −
\begin{center}+ −
\begin{tabular}{l}+ −
\textcolor{blue}{$\forall\{x, y\}.\, x \rightarrow y \;\;\approx_\alpha\;\; \forall\{y, x\}.\, y \rightarrow x$}+ −
\bigskip\smallskip\\+ −
+ −
\onslide<2->{%+ −
\textcolor{blue}{$\forall\{x, y\}.\, x \rightarrow y \;\;\not\approx_\alpha\;\; \forall\{z\}.\, z \rightarrow z$}+ −
}\bigskip\smallskip\\+ −
+ −
\onslide<3->{%+ −
\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{textblock}{8}(2,14.5)+ −
\footnotesize $^*$ $x$, $y$, $z$ are assumed to be distinct+ −
\end{textblock}+ −
+ −
\only<4>{+ −
\begin{textblock}{6}(2.5,4)+ −
\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.+ −
\end{minipage}};+ −
\end{tikzpicture}+ −
\end{textblock}}+ −
\end{frame}}+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + −
*}+ −
+ −
text_raw {*+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
\mode<presentation>{+ −
\begin{frame}<1-3>+ −
\frametitle{\begin{tabular}{c}Other Binding Modes\end{tabular}}+ −
\mbox{}\\[-3mm]+ −
+ −
\begin{itemize}+ −
\item alpha-equivalence being preserved under vacuous binders is \underline{not} always+ −
wanted:\bigskip\bigskip\normalsize+ −
+ −
\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{itemize}+ −
+ −
\end{frame}}+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + −
*}+ −
+ −
text_raw {*+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
\mode<presentation>{+ −
\begin{frame}<1>+ −
\frametitle{\begin{tabular}{c}\Large{}Even Another Binding Mode\end{tabular}}+ −
\mbox{}\\[-3mm]+ −
+ −
\begin{itemize}+ −
\item sometimes one wants to abstract more than one name, but the order \underline{does} matter\bigskip+ −
+ −
\begin{center}+ −
\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{center}+ −
+ −
+ −
\end{itemize}+ −
+ −
\end{frame}}+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + −
*}+ −
+ −
+ −
text_raw {*+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
\mode<presentation>{+ −
\begin{frame}<2-3>+ −
\frametitle{\begin{tabular}{c}Specification of Binding\end{tabular}}+ −
\mbox{}\\[-6mm]+ −
+ −
\mbox{}\hspace{10mm}+ −
\begin{tabular}{ll}+ −
\multicolumn{2}{l}{\isacommand{nominal\_datatype} trm $=$}\\+ −
\hspace{5mm}\phantom{$|$} Var name\\+ −
\hspace{5mm}$|$ App trm trm\\+ −
\hspace{5mm}$|$ Lam \only<2->{x::}name \only<2->{t::}trm+ −
& \onslide<2->{\isacommand{bind} x \isacommand{in} t}\\+ −
\hspace{5mm}$|$ Let \only<2->{as::}assns \only<2->{t::}trm+ −
& \onslide<2->{\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}{\onslide<3->{\isacommand{binder} bn \isacommand{where}}}\\+ −
\multicolumn{2}{l}{\onslide<3->{\hspace{5mm}\phantom{$|$} bn(ANil) $=$ $[]$}}\\+ −
\multicolumn{2}{l}{\onslide<3->{\hspace{5mm}$|$ bn(ACons a t as) $=$ $[$a$]$ @ bn(as)}}\\+ −
\end{tabular}+ −
+ −
+ −
+ −
\end{frame}}+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + −
*}+ −
+ −
+ −
text_raw {*+ −
+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
\mode<presentation>{+ −
\begin{frame}+ −
\frametitle{So Far So Good}+ −
+ −
\begin{itemize}+ −
\item A Faulty Lemma with the Variable Convention?\\[-8mm]\mbox{}+ −
\end{itemize}+ −
+ −
\begin{center}+ −
\begin{block}{}+ −
\color{gray}+ −
\small%+ −
{\bf\mbox{}\hspace{-1.5mm}Variable Convention:}\\[1mm] + −
If $M_1,\ldots,M_n$ occur in a certain mathematical context+ −
(e.g. definition, proof), then in these terms all bound variables + −
are chosen to be different from the free variables.\\[2mm]+ −
+ −
\footnotesize\hfill Barendregt in ``The Lambda-Calculus: Its Syntax and Semantics''+ −
\end{block}+ −
\end{center}+ −
+ −
\mbox{}\\[-18mm]\mbox{}+ −
+ −
\begin{columns}+ −
\begin{column}[t]{4.7cm}+ −
Inductive Definitions:\\+ −
\begin{center}+ −
\smath{\infer{\text{concl}}{\text{prem}_1 \ldots \text{prem}_n\;\text{scs}}}+ −
\end{center}+ −
\end{column}+ −
\begin{column}[t]{7cm}+ −
Rule Inductions:\\[2mm]+ −
\begin{tabular}{l@ {\hspace{2mm}}p{5.5cm}}+ −
1.) & Assume the property for\\ & the premises. Assume \\ & the side-conditions.\\[1mm]+ −
2.) & Show the property for\\ & the conclusion.\\+ −
\end{tabular}+ −
\end{column}+ −
\end{columns}+ −
+ −
\end{frame}}+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + −
+ −
*}+ −
+ −
text_raw {*+ −
+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
\mode<presentation>{+ −
\setbeamerfont{itemize/enumerate subbody}{size=\normalsize}+ −
\begin{frame}[sqeeze]+ −
\frametitle{Faulty Reasoning} + −
+ −
%\mbox{}+ −
+ −
\begin{itemize}+ −
\item Consider the two-place relation \smath{\text{foo}}:\medskip+ −
\begin{center}+ −
\begin{tabular}{ccc}+ −
\raisebox{2.5mm}{\colorbox{cream}{%+ −
\smath{\;\infer{x\mapsto x}{}}}}\hspace{2mm}+ −
&+ −
\raisebox{2mm}{\colorbox{cream}{%+ −
\smath{\infer{t_1\;t_2\mapsto t_1\;t_2}{}}}}\hspace{2mm}+ −
&+ −
\colorbox{cream}{%+ −
\smath{\infer{\lambda x.t\mapsto t'}{t\mapsto t'}}}\\[5mm]+ −
\end{tabular}+ −
\end{center}+ −
+ −
\pause+ −
+ −
\item The lemma we going to prove:\smallskip+ −
\begin{center}+ −
Let \smath{t\mapsto t'}. If \smath{y\fresh t} then \smath{y\fresh t'}.+ −
\end{center}\bigskip+ −
+ −
\only<3>{+ −
\item Cases 1 and 2 are trivial:\medskip+ −
\begin{itemize}+ −
\item If \smath{y\fresh x} then \smath{y\fresh x}.+ −
\item If \smath{y\fresh t_1\,t_2} then \smath{y\fresh t_1\,t_2}.+ −
\end{itemize}+ −
}+ −
+ −
\only<4->{+ −
\item Case 3:+ −
\begin{itemize}+ −
\item We know \tikz[remember picture,baseline=(ta.base)] \node (ta) {\smath{y\fresh \lambda x.t}.}; + −
We have to show \smath{y\fresh t'}.$\!\!\!\!$ + −
\item The IH says: if \smath{y\fresh t} then \smath{y\fresh t'}.+ −
\item<7,8> So we have \smath{y\fresh t}. Hence \smath{y\fresh t'} by IH. Done!+ −
\end{itemize}+ −
}+ −
\end{itemize}+ −
+ −
\begin{textblock}{11.3}(0.7,0.6)+ −
\only<5-7>{+ −
\begin{tikzpicture}+ −
\draw (0,0) node[fill=cream, text width=11.2cm, thick, draw=red, rounded corners=1mm] (nn)+ −
{{\bf Variable Convention:}\\[2mm] + −
\small+ −
If $M_1,\ldots,M_n$ occur in a certain mathematical context+ −
(e.g. definition, proof), then in these terms all bound variables + −
are chosen to be different from the free variables.\smallskip+ −
+ −
\normalsize+ −
{\bf In our case:}\\[2mm]+ −
The free variables are \smath{y} and \smath{t'}; the bound one is + −
\smath{x}.\medskip+ −
+ −
By the variable convention we conclude that \smath{x\not= y}.+ −
};+ −
\end{tikzpicture}}+ −
\end{textblock}+ −
+ −
\begin{textblock}{9.2}(3.6,9.2)+ −
\only<6,7>{+ −
\begin{tikzpicture}[remember picture]+ −
\draw (0,0) node[fill=cream, text width=9cm, thick, draw=red, rounded corners=1mm] (tb)+ −
{\small\smath{y\!\not\in\! \text{fv}(\lambda x.t) \Longleftrightarrow+ −
y\!\not\in\! \text{fv}(t)\!-\!\{x\}+ −
\stackrel{x\not=y}{\Longleftrightarrow}+ −
y\!\not\in\! \text{fv}(t)}};+ −
+ −
\path[overlay, ->, ultra thick, red] (tb) edge[out=-120, in=75] (ta);+ −
\end{tikzpicture}}+ −
\end{textblock}+ −
+ −
\end{frame}}+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + −
+ −
*}+ −
+ −
+ −
text_raw {*+ −
+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
\mode<presentation>{+ −
\begin{frame}+ −
\frametitle{Conclusions} + −
+ −
\begin{itemize}+ −
\item The user does not see anything of the ``raw'' level.+ −
\item The Nominal Isabelle automatically derives the strong structural+ −
induction principle for \underline{\bf all} nominal datatypes (not just the + −
lambda-calculus)+ −
+ −
\item They are easy to use: you just have to think carefully what the variable+ −
convention should be.+ −
+ −
\item We can explore the \colorbox{black}{\textcolor{white}{dark}} corners + −
of the variable convention: when and where it can be used safely.+ −
+ −
\item<2> \alert{\bf Main Point:} Actually these proofs using the+ −
variable convention are all trivial / obvious / routine\ldots {\bf provided} + −
you use Nominal Isabelle. ;o)+ −
+ −
\end{itemize}+ −
+ −
+ −
\end{frame}}+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + −
+ −
*}+ −
+ −
text_raw {*+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
\mode<presentation>{+ −
\begin{frame}<1>[b]+ −
\frametitle{+ −
\begin{tabular}{c}+ −
\mbox{}\\[13mm]+ −
\alert{\LARGE Thank you very much!}\\+ −
\alert{\Large Questions?}+ −
\end{tabular}}+ −
+ −
+ −
\end{frame}}+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + −
*}+ −
+ −
(*<*)+ −
end+ −
(*>*)+ −