diff -r fb201e383f1b -r da575186d492 Slides/SlidesA.thy --- a/Slides/SlidesA.thy Tue Feb 19 05:38:46 2013 +0000 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,1648 +0,0 @@ -(*<*) -theory SlidesA -imports "~~/src/HOL/Library/LaTeXsugar" "Nominal" -begin - -notation (latex output) - set ("_") and - Cons ("_::/_" [66,65] 65) - -(*>*) - - -text_raw {* - %% was \begin{colormixin}{20!averagebackgroundcolor} - %% - %% is \begin{colormixin}{50!averagebackgroundcolor} - \renewcommand{\slidecaption}{Warsaw, 9 February 2012} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame} - \frametitle{% - \begin{tabular}{@ {}c@ {}} - \Huge Nominal Techniques\\[0mm] - \Huge in Isabelle\\ - \Large or, How Not to be Intimidated by the\\[-3mm] - \Large Variable Convention\\[-5mm] - \end{tabular}} - - \begin{center} - Christian Urban\\[1mm] - King's College London\\[-6mm]\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 Barendregt in ``The Lambda-Calculus: Its Syntax and Semantics'' - \end{block} - \end{center} - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -*} - -text_raw {* - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}<1->[c] - \frametitle{Nominal Techniques} - - \begin{itemize} - \item Andy Pitts found out 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 Nominal Unification\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.1) - \includegraphics[scale=0.26]{andrewpitts.jpg} - \end{textblock} - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -*} - -text_raw {* - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}[c] - \frametitle{Nominal Isabelle} - - \begin{itemize} - \item a theory about atoms and permutations\medskip - - \item support and freshness - \begin{center} - \smath{\text{supp}(x) \dn \{ a \mid \text{infinite}\,\{ b \mid \swap{a}{b}\act x \not= x\}\}} - \end{center}\bigskip\pause - - \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{ - \begin{frame}<1-6> - \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 $\alpha$-equivalence}} - \end{center} - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -*} - -text_raw {* - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}<1-3>[c] - \frametitle{HOL vs.~Nominal} - - \begin{itemize} - \item Nominal logic / nominal sets by Pitts are incompatible - with choice principles\medskip - - \item HOL includes Hilbert's epsilon\pause\bigskip - - \item Solution: Do not require that everything has finite support\medskip - - \begin{center} - \smath{\onslide<1-2>{\text{finite}(\text{supp}(x)) \quad\Rightarrow\quad} a \fresh a.x} - \end{center} - \end{itemize} - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -*} - -text_raw {* - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}[c] - \frametitle{} - - \begin{tabular}{c@ {\hspace{2mm}}c} - \\[6mm] - \begin{tabular}{c} - \includegraphics[scale=0.11]{harper.jpg}\\[-2mm] - {\footnotesize Bob Harper}\\[-2.5mm] - {\footnotesize (CMU)} - \end{tabular} - \begin{tabular}{c} - \includegraphics[scale=0.37]{pfenning.jpg}\\[-2mm] - {\footnotesize Frank Pfenning}\\[-2.5mm] - {\footnotesize (CMU)} - \end{tabular} & - - \begin{tabular}{p{6cm}} - \raggedright - \color{gray}{published a proof in\\ {\bf ACM Transactions on Computational Logic}, 2005, - $\sim$31pp} - \end{tabular}\\ - - \pause - \\[0mm] - - \begin{tabular}{c} - \includegraphics[scale=0.36]{appel.jpg}\\[-2mm] - {\footnotesize Andrew Appel}\\[-2.5mm] - {\footnotesize (Princeton)} - \end{tabular} & - - \begin{tabular}{p{6cm}} - \raggedright - \color{gray}{relied on their proof in a\\ {\bf security} critical application} - \end{tabular} - \end{tabular}\medskip\pause - - \small - \begin{minipage}{1.0\textwidth} - (I also found an {\bf error} in my Ph.D.-thesis about cut-elimination - examined by Henk Barendregt and Andy Pitts.) - \end{minipage} - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -*} - - - -text_raw {* - - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}<1,2,3,4>[squeeze] - \frametitle{Formalisation of LF} - - - \begin{center} - \begin{tabular}{@ {\hspace{-16mm}}lc} - \mbox{}\\[-6mm] - - \textcolor{white}{\raisebox{4mm}{1.~Solution}} & - \begin{tikzpicture} - [node distance=25mm, - text height=1.5ex, - text depth=.25ex, - node1/.style={ - rectangle, minimum size=10mm, rounded corners=3mm, very thick, - draw=black!50, top color=white, bottom color=black!20}, - ] - - \node (proof) [node1] {\large Proof}; - \node (def) [node1, left of=proof] {\large$\,\;\dn\;\,$}; - \node (alg) [node1, right of=proof] {\large\hspace{1mm}Alg.\hspace{1mm}\mbox{}}; - - \draw[->,black!50,line width=2mm] (proof) -- (def); - \draw[->,black!50,line width=2mm] (proof) -- (alg); - - \onslide<2->{\draw[white,line width=1mm] (0.1,0.6) -- (-0.1,0.25) -- (0.1,-0.25) -- (-0.1,-0.6);} - \end{tikzpicture} - \\[2mm] - - \onslide<3->{% - \raisebox{4mm}{\textcolor{white}{1st Solution}} & - \begin{tikzpicture} - [node distance=25mm, - text height=1.5ex, - text depth=.25ex, - node1/.style={ - rectangle, minimum size=10mm, rounded corners=3mm, very thick, - draw=black!50, top color=white, bottom color=black!20}, - node2/.style={ - rectangle, minimum size=12mm, rounded corners=3mm, very thick, - draw=red!70, top color=white, bottom color=red!50!black!20} - ] - - \node (proof) [node1] {\large Proof}; - \node (def) [node2, left of=proof] {\large$\dn{}\!\!^\text{+ex}$}; - \node (alg) [node1, right of=proof] {\large\hspace{1mm}Alg.\hspace{1mm}\mbox{}}; - - \draw[->,black!50,line width=2mm] (proof) -- (def); - \draw[->,black!50,line width=2mm] (proof) -- (alg); - - \end{tikzpicture} - \\[2mm]} - - \end{tabular} - \end{center} - - \begin{textblock}{3}(13.2,5.1) - \onslide<3->{ - \begin{tikzpicture} - \node at (0,0) [single arrow, shape border rotate=270, fill=red,text=white]{2h}; - \end{tikzpicture} - } - \end{textblock} - - - \begin{textblock}{11}(1.4,14.3) - \only<1->{\footnotesize (one needs to check $\sim$31pp~of informal paper proofs from - ACM Transactions on Computational Logic, 2005)} - \end{textblock} - - \only<4->{ - \begin{textblock}{9}(10,11.5) - \begin{tikzpicture}[remember picture, overlay] - \draw (0,0) node[fill=cream, text width=5.3cm, thick, draw=red, rounded corners=1mm] (n2) - {\raggedright I also found \mbox{(fixable)} mistakes in my Ph.D.~thesis. - }; - \end{tikzpicture} - \end{textblock}} - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -*} - -text_raw {* - - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}[c] - \frametitle{\LARGE\begin{tabular}{c}Nominal Isabelle\end{tabular}} - - - \begin{itemize} - \item \ldots{}is a tool on top of the theorem prover - Isabelle; bound variables have names (no de Bruijn - indices).\medskip - - \item It can be used to, for example, represent lambda terms - - \begin{center} - \smath{M ::= x\;\mid\; M\,N \;\mid\; \lambda x.M} - \end{center} - \end{itemize} - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -*} - -text_raw {* - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame} - \small - \begin{beamercolorbox}[sep=1mm, wd=11cm]{boxcolor} - {\bf Substitution Lemma:} - If \smath{x\not\equiv y} and - \smath{x\not\in \text{fv}(L)}, then\\ - \mbox{}\hspace{5mm}\smath{M[x:=N][y:=L]\equiv M[y:=L][x:=N[y:=L]]} - \end{beamercolorbox} - - {\bf Proof:} \alert<4>{By induction on the structure of \smath{M}.} - \begin{itemize} - \item {\bf Case 1:} \smath{M} is a variable. - - \begin{tabular}{@ {}l@ {\hspace{1mm}}p{9cm}@ {}} - Case 1.1. & \smath{M\equiv x}. Then both sides \alert<3,4>{equal} - \smath{N[y:=L]} since \smath{x\not\equiv y}.\\[1mm] - Case 1.2. & \smath{M\equiv y}. Then both sides \alert<3,4>{equal} - \smath{L}, for \smath{x\not\in \text{fv}(L)}\\ - & implies \smath{L[x:=\ldots]\equiv L}.\\[1mm] - Case 1.3. & \smath{M\equiv z\not\equiv x,y}. Then both sides \alert<3,4>{equal} \smath{z}.\\[1mm] - \end{tabular} - - \item {\bf Case 2:} \smath{M\equiv \lambda z.M_1}. - \alert<2>{By the variable convention we may assume that \smath{z\not\equiv x,y} - and \smath{z} is not free in \smath{N,L}.} - - \begin{tabular}{@ {}r@ {\hspace{1mm}}l@ {}} - \smath{(\lambda z.M_1)[x\!:=\!N][y\!:=\!L]} - \smath{\equiv} & \smath{\lambda z.(M_1[x\!:=\!N][y\!:=\!L])}\\ - \smath{\equiv} & \smath{\lambda z.(M_1[y\!:=\!L][x\!:=\!N[y\!:=\!L]])}\\ - \smath{\equiv} & \smath{(\lambda z.M_1)[y\!:=\!L][x\!:=\!N[y\!:=\!L]]}.\\ - \end{tabular} - - \item {\bf Case 3:} \smath{M\equiv M_1 M_2}. - The statement follows again from the induction hypothesis. \hfill$\,\Box\,$ - \end{itemize} - - \begin{textblock}{11}(4,3) - \begin{block}<5>{} - Remember only if \smath{y\not=x} and \smath{x\not\in \text{fv}(N)} then\\[2mm] - \smath{\quad(\lambda y.M)[x:=N]=\lambda y.(M[x:=N])}\\[4mm] - - \begin{tabular}{c@ {\hspace{2mm}}l@ {\hspace{2mm}}l@ {}} - & \smath{(\lambda z.M_1)[x:=N][y:=L]}\\[1.3mm] - \smath{\equiv} & \smath{(\lambda z.(M_1[x:=N]))[y:=L]} & $\stackrel{1}{\leftarrow}$\\[1.3mm] - \smath{\equiv} & \smath{\lambda z.(M_1[x:=N][y:=L])} & $\stackrel{2}{\leftarrow}$\\[1.3mm] - \smath{\equiv} & \smath{\lambda z.(M_1[y:=L][x:=N[y:=L]])} & IH\\[1.3mm] - \smath{\equiv} & \smath{(\lambda z.(M_1[y:=L]))[x:=N[y:=L]])} - & $\stackrel{2}{\rightarrow}$ \alert{\bf\;!}\\[1.3mm] - \smath{\equiv} & \smath{(\lambda z.M_1)[y:=L][x:=N[y:=L]]}. & - $\stackrel{1}{\rightarrow}$\\[1.3mm] - \end{tabular} - \end{block} - \end{textblock} - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -*} - -text_raw {* - - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame} - \frametitle{Nominal Isabelle} - - \begin{itemize} - \item Define lambda-terms as: - \end{itemize} -*} - - atom_decl name text_raw {*\medskip\isanewline *} - nominal_datatype lam = - Var "name" - | App "lam" "lam" - | Lam "\name\lam" ("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}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -*} - -(*<*) - -nominal_primrec - subst :: "lam \ name \ lam \ lam" ("_[_::=_]" [100,100,100] 100) -where - "(Var x)[y::=s] = (if x=y then s else (Var x))" -| "(App t\<^isub>1 t\<^isub>2)[y::=s] = App (t\<^isub>1[y::=s]) (t\<^isub>2[y::=s])" -| "x\(y,s) \ (SlidesA.Lam x t)[y::=s] = SlidesA.Lam x (t[y::=s])" -apply(finite_guess)+ -apply(rule TrueI)+ -apply(simp add: abs_fresh)+ -apply(fresh_guess)+ -done - -(*>*) - -text_raw {* - - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame} - %%\frametitle{\large Formal Proof of the Substitution Lemma} - - \small - \begin{tabular}{@ {\hspace{-4mm}}c @ {}} - \begin{minipage}{1.1\textwidth} -*} - -lemma forget: - assumes a: "x \ L" - shows "L[x::=P] = L" -using a by (nominal_induct L avoiding: x P rule: lam.strong_induct) - (auto simp add: abs_fresh fresh_atm) - -lemma fresh_fact: - fixes z::"name" - assumes a: "z \ N" "z \ L" - shows "z \ N[y::=L]" -using a by (nominal_induct N avoiding: z y L rule: lam.strong_induct) - (auto simp add: abs_fresh fresh_atm) - -lemma substitution_lemma: - assumes a: "x \ y" "x \ L" -- {* \mbox{}\hspace{-2mm}\tikz[remember picture] \node (n1) {}; *} - shows "M[x::=N][y::=L] = M[y::=L][x::=N[y::=L]]" -using a -by (nominal_induct M avoiding: x y N L rule: lam.strong_induct) - (auto simp add: fresh_fact forget) - -text_raw {* - \end{minipage} - \end{tabular} - - \begin{textblock}{6}(11,9) - \only<2>{ - \begin{tikzpicture}[remember picture, overlay] - \draw (0,0) node[fill=cream, text width=5.5cm, thick, draw=red, rounded corners=1mm] (n2) - {\setlength\leftmargini{6mm}% - \begin{itemize} - \item stands for \smath{x\not\in \text{fv}(L)}\\[-2mm] - \item reads as ``\smath{x} fresh for \smath{L}'' - \end{itemize} - }; - - \path[overlay, ->, very thick, red] (n2) edge[out=-90, in=0] (n1); - \end{tikzpicture}} - \end{textblock} - - \only<1-3>{} - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -*} - -text_raw {* - - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \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}.\smallskip\\ - - (This nearly always requires renamings and they can be - tricky to automate.) - \end{itemize} - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -*} - - -text_raw {* - - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame} - \frametitle{\LARGE Strong Induction Principles} - - \begin{itemize} - \item Therefore we will use 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{ - \begin{frame} - \frametitle{\LARGE Strong Induction Principles} - - \begin{center} - \mbox{}\hspace{-2mm}\begin{beamercolorbox}[sep=1mm, wd=11.5cm]{boxcolor} - \centering\smath{% - \infer{P\,\alert{c}\;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.\;x\fresh c \wedge (\forall d. P\,d\,t)\Rightarrow P\,c\;(\lambda x.t) - \end{array} - }} - \end{beamercolorbox} - \end{center} - - - \only<1>{ - \begin{textblock}{14}(1.2,9.2) - \begin{itemize} - \item There is a condition for when Barendregt's variable convention - is applicable---it is almost always satisfied, but not always:\\[2mm] - - The induction context \smath{c} needs to be finitely supported - (is not allowed to mention all names as free). - \end{itemize} - \end{textblock}} - - \only<2>{ - \begin{itemize} - \item In the case of the substitution lemma:\\[2mm] - - \begin{textblock}{16.5}(0.7,11.5) - \small -*} - -(*<*) -lemma - assumes a: "x\y" "x \ L" - shows "M[x::=N][y::=L] = M[y::=L][x::=N[y::=L]]" -using a -(*>*) -proof (nominal_induct M avoiding: x y N L rule: lam.strong_induct) -txt_raw {* \isanewline$\ldots$ *} -(*<*)oops(*>*) - -text_raw {* - \end{textblock} - \end{itemize}} - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -*} - - -text_raw {* - - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame} - \frametitle{\Large \mbox{Same Problem with Rule Inductions}} - - \begin{itemize} - \item We can specify typing-rules for lambda-terms as: - - \begin{center} - \begin{tabular}{@ {\hspace{-6mm}}c@ {}} - \colorbox{cream}{ - \smath{\infer{\Gamma\vdash x:\tau}{(x\!:\!\tau)\in\Gamma\;\;\text{valid}\;\Gamma}}} - \;\; - \colorbox{cream}{ - \smath{\infer{\Gamma\vdash t_1\;t_2:\tau} - {\Gamma\vdash t_1:\sigma\!\rightarrow\!\tau & \Gamma\vdash t_2:\sigma}}}\\[4mm] - - \colorbox{cream}{ - \smath{\infer{\Gamma\vdash \lambda x.t:\sigma\!\rightarrow\!\tau} - {x\fresh \Gamma & (x\!:\!\sigma)\!::\!\Gamma\vdash t:\tau}}}\\[6mm] - - \colorbox{cream}{ - \smath{\infer{\text{valid}\;[]}{}}} - \;\;\;\; - \colorbox{cream}{ - \smath{\infer{\text{valid}\;(x\!:\!\tau)\!::\!\Gamma}{x\fresh\Gamma & \text{valid}\;\Gamma}}}\\[8mm] - \end{tabular} - \end{center} - - \item If \smath{\Gamma_1\vdash t:\tau} and \smath{\text{valid}\;\Gamma_2}, - \smath{\Gamma_1\subseteq \Gamma_2} then \smath{\Gamma_2\vdash t:\tau}.$\!\!\!\!\!$ - - \end{itemize} - - - \begin{textblock}{11}(1.3,4) - \only<2>{ - \begin{tikzpicture} - \draw (0,0) node[fill=cream, text width=10.5cm, thick, draw=red, rounded corners=1mm] (nn) - {The proof of the weakening lemma is said to be trivial / obvious / routine - /\ldots{} in many places.\\[2mm] - - (I am actually still looking for a place in the literature where a - trivial / obvious / routine /\ldots{} proof is spelled out --- I know of - proofs by Gallier, McKinna \& Pollack and Pitts, but I would not - call them trivial / obvious / routine /\ldots)}; - \end{tikzpicture}} - \end{textblock} - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -*} - -text_raw {* - - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}[c] - \frametitle{Recall: Rule Inductions} - - \begin{center}\large - \colorbox{cream}{ - \smath{\infer[\text{rule}]{\text{concl}}{\text{prem}_1 \ldots \text{prem}_n\;\text{scs}}}} - \end{center}\bigskip - - \begin{tabular}[t]{l} - Rule Inductions:\\[1mm] - \begin{tabular}{l@ {\hspace{2mm}}p{8.4cm}} - 1.) & Assume the property for the premises. Assume the side-conditions.\\[1mm] - 2.) & Show the property for the conclusion.\\ - \end{tabular} - \end{tabular} - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -*} - -text_raw {* - - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame} - \frametitle{\LARGE\mbox{Induction Principle for Typing}} - - \begin{itemize} - \item The induction principle that comes with the typing definition is as follows:\\[-13mm] - \mbox{} - \end{itemize} - - \begin{center} - \begin{tabular}{@ {\hspace{-5mm}}c@ {}} - \colorbox{cream}{ - \smath{ - \infer{\Gamma\vdash t:\tau \Rightarrow P\,\Gamma\,t\,\tau} - {\begin{array}{l} - \forall \Gamma\,x\,\tau.\,\;(x\!:\!\tau)\in\Gamma\wedge - \text{valid}\,\Gamma\Rightarrow P\,\Gamma\,(x)\,\tau\\[4mm] - \forall \Gamma\,t_1\,t_2\,\sigma\,\tau.\\ - P\,\Gamma\,t_1\,(\sigma\!\rightarrow\!\tau)\wedge - P\,\Gamma\,t_2\,\sigma - \Rightarrow P\,\Gamma\,(t_1\,t_2)\,\tau\\[4mm] - \forall \Gamma\,x\,t\,\sigma\,\tau.\\ - x\fresh\Gamma\wedge - P\,((x\!:\!\sigma)\!::\!\Gamma)\,t\,\tau - \Rightarrow P\,\Gamma (\lambda x.t)\,(\sigma\!\rightarrow\!\tau)\\[2mm] - \end{array} - } - }} - \end{tabular} - \end{center} - - \begin{textblock}{4}(9,13.8) - \begin{tikzpicture} - \draw (0,0) node[fill=cream, text width=3.9cm, thick, draw=red, rounded corners=1mm] (nn) - {\small Note the quantifiers!}; - \end{tikzpicture} - \end{textblock} - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -*} - -text_raw {* - - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame} - \frametitle{\LARGE \mbox{Proof of Weakening Lemma}} - \mbox{}\\[-18mm]\mbox{} - - \begin{center} - \colorbox{cream}{ - \smath{\infer{\Gamma\vdash \lambda x.t:\sigma\!\rightarrow\!\tau} - {x\fresh \Gamma & (x\!:\!\sigma)\!::\!\Gamma\vdash t:\tau}}} - \end{center} - - \begin{minipage}{1.1\textwidth} - \begin{itemize} - \item If \smath{\Gamma_1\!\vdash\! t\!:\!\tau} then - \smath{\alert<1>{\forall \Gamma_2}.\,\text{valid}\,\Gamma_2 \wedge \Gamma_1\!\subseteq\! - \Gamma_2\!\Rightarrow\! \Gamma_2\!\vdash\! t\!:\!\tau} - \end{itemize} - - \pause - - \mbox{}\hspace{-5mm} - \underline{For all \smath{\Gamma_1}, \smath{x}, \smath{t}, \smath{\sigma} and \smath{\tau}}: - - \begin{itemize} - \item We know:\\ - \smath{\forall \alert<4->{\Gamma_2}.\,\text{valid}\,\alert<4->{\Gamma_2} \wedge - (x\!:\!\sigma)\!::\!\Gamma_1\!\subseteq\! \alert<4->{\Gamma_2} \Rightarrow \!\! - \tikz[remember picture, baseline=(ea.base)] - \node (ea) {\smath{\alert<4->{\Gamma_2}}};\!\vdash\! t\!:\!\tau}\\ - \smath{x\fresh\Gamma_1}\\ - \onslide<3->{\smath{\text{valid}\,\Gamma_2 \wedge \Gamma_1\!\subseteq\!\Gamma_2 - \only<6->{\Rightarrow (x\!:\!\sigma)\!::\!\Gamma_1\!\subseteq\! - (x\!:\!\sigma)\!::\!\Gamma_2}}}\\ - \onslide<3->{\smath{\textcolor{white}{\text{valid}\,\Gamma_2 \wedge \Gamma_1\!\subseteq\!\Gamma_2 - \Rightarrow} \only<7->{\;\alert{\text{valid}\,(x\!:\!\sigma)\!::\!\Gamma_2\;\;\text{\bf ???}}}}} - - \item We have to show:\\ - \only<2>{ - \smath{\forall \Gamma_2.\,\text{valid}\,\Gamma_2 \wedge - \Gamma_1\!\subseteq\!\Gamma_2 \Rightarrow \Gamma_2\!\vdash\! - \lambda x.t\!:\!\sigma\!\rightarrow\!\tau}} - \only<3->{ - \smath{\Gamma_2\!\vdash\!\lambda x.t\!:\!\sigma\!\rightarrow\!\tau}} - - \end{itemize} - \end{minipage} - - \begin{textblock}{4}(10,6.5) - \only<5->{ - \begin{tikzpicture}[remember picture] - \draw (0,0) node[fill=cream, text width=4cm, thick, draw=red, rounded corners=1mm] (eb) - {\smath{\Gamma_2\mapsto (x\!:\!\sigma)\!::\!\Gamma_2}}; - - \path[overlay, ->, ultra thick, red] (eb) edge[out=-90, in=80] (ea); - \end{tikzpicture}} - \end{textblock} - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -*} - -text_raw {* - - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame} - - \begin{textblock}{14.8}(0.7,0.5) - \begin{itemize} - \item The usual proof of strong normalisation for simply- typed lambda-terms - establishes first:\\[1mm] - - \colorbox{cream}{% - \begin{tabular}{@ {}p{11cm}} - Lemma: If for all reducible \smath{s}, \smath{t[x\!:=\!s]} is reducible, then - \smath{\lambda x.t} is reducible. - \end{tabular}}\smallskip - - \item Then one shows for a closing (simultaneous) substitution:\\[2mm] - - \colorbox{cream}{% - \begin{tabular}{@ {}p{11cm}} - Theorem: If \smath{\Gamma\vdash t:\tau}, then for all closing - substitutions \smath{\theta} containing reducible terms only, - \smath{\theta(t)} is reducible. - \end{tabular}} - - \mbox{}\\[1mm] - - Lambda-Case: By ind.~we know \smath{(x\!\mapsto\! s\cup\theta)(t)} - is reducible with \smath{s} being reducible. This is equal\alert{$^*$} to - \smath{(\theta(t))[x\!:=\!s]}. Therefore, we can apply the lemma and get \smath{\lambda - x.(\theta(t))} is reducible. Because this is equal\alert{$^*$} to - \smath{\theta(\lambda x.t)}, we are done. - \hfill\footnotesize\alert{$^*$}you have to take a deep breath - \end{itemize} - \end{textblock} - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -*} - - -text_raw {* - - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame} - \frametitle{\LARGE \mbox{Proof of Weakening Lemma}} - \mbox{}\\[-18mm]\mbox{} - - \begin{center} - \colorbox{cream}{ - \smath{\infer{\Gamma\vdash \lambda x.t:\sigma\!\rightarrow\!\tau} - {x\fresh \Gamma & (x\!:\!\sigma)\!::\!\Gamma\vdash t:\tau}}} - \end{center} - - \begin{minipage}{1.1\textwidth} - \begin{itemize} - \item If \smath{\Gamma_1\!\vdash\! t\!:\!\tau} then - \smath{\text{valid}\,\Gamma_2 \wedge \Gamma_1\!\subseteq\! - \Gamma_2\!\Rightarrow\! \Gamma_2\!\vdash\! t\!:\!\tau} - \end{itemize} - - \mbox{}\hspace{-5mm} - \underline{For all \smath{\Gamma_1}, \smath{x}, \smath{t}, \smath{\sigma} and \smath{\tau}}: - - \begin{itemize} - \item We know:\\ - \smath{\forall \Gamma_2.\,\text{valid}\,\Gamma_2 \wedge - (x\!:\!\sigma)\!::\!\Gamma_1\!\subseteq\! \Gamma_2 \Rightarrow \!\! - \Gamma_2\!\vdash\! t\!:\!\tau}\\ - \smath{x\fresh\Gamma_1}\\ - \begin{tabular}{@ {}ll@ {}} - \smath{\text{valid}\,\Gamma_2 \wedge \Gamma_1\!\subseteq\!\Gamma_2} & - \only<2->{\smath{\alert{\Rightarrow (x\!:\!\sigma)\!::\!\Gamma_1\!\subseteq\! - (x\!:\!\sigma)\!::\!\Gamma_2}}}\\ - \smath{\alert{x\fresh\Gamma_2}} & - \only<2->{\smath{\alert{\Rightarrow \text{valid}\,(x\!:\!\sigma)\!::\!\Gamma_2}}} - \end{tabular} - - \item We have to show:\\ - \smath{\Gamma_2\!\vdash\!\lambda x.t\!:\!\sigma\!\rightarrow\!\tau} - - \end{itemize} - \end{minipage} - - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -*} - - - -text_raw {* - - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame} - \frametitle{SN (Again)} - \mbox{}\\[-8mm] - - \colorbox{cream}{% - \begin{tabular}{@ {}p{10.5cm}} - Theorem: If \smath{\Gamma\vdash t:\tau}, then for all closing - substitutions \smath{\theta} containing reducible terms only, - \smath{\theta(t)} is reducible. - \end{tabular}}\medskip - - \begin{itemize} - \item - Since we say that the strong induction should avoid \smath{\theta}, we - get the assumption \alert{$x\fresh\theta$} then:\\[2mm] - - \begin{tabular}{@ {}p{10.5cm}}\raggedright - Lambda-Case: By ind.~we know \smath{(x\!\mapsto\! s\cup\theta)(t)} is reducible - with - \smath{s} being reducible. This is {\bf equal} to - \smath{(\theta(t))[x\!:=\!s]}. Therefore, we can apply the lemma and get - \smath{\lambda x.(\theta(t))} is reducible. Because this is {\bf equal} to - \smath{\theta(\lambda x.t)}, we are done. - \end{tabular}\smallskip - - \begin{center} - \begin{tabular}{rl} - \smath{x\fresh\theta\Rightarrow} & - \smath{(x\!\mapsto\! s\cup\theta)(t) \;\alert{=}\;(\theta(t))[x\!:=\!s]}\\[1mm] - & - \smath{\theta(\lambda x.t) \;\alert{=}\; \lambda x.(\theta(t))} - \end{tabular} - \end{center} - \end{itemize} - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -*} - -text_raw {* - - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \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{ - \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) - \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{ - \setbeamerfont{itemize/enumerate subbody}{size=\normalsize} - \begin{frame} - \frametitle{VC-Compatibility} - - \begin{itemize} - \item We introduced two conditions that make the VC safe to use in rule inductions: - - \begin{itemize} - \item the relation needs to be \alert{\bf equivariant}, and - \item the binder is not allowed to occur in the \alert{\bf support} of - the conclusion (not free in the conclusion)\bigskip - \end{itemize} - - \item Once a relation satisfies these two conditions, then Nominal - Isabelle derives the strong induction principle automatically. - \end{itemize} - - \begin{textblock}{11.3}(0.7,6) - \only<2>{ - \begin{tikzpicture} - \draw (0,0) node[fill=cream, text width=11cm, thick, draw=red, rounded corners=1mm] (nn) - {A relation \smath{R} is {\bf equivariant} iff - % - \begin{center} - \smath{% - \begin{array}[t]{l} - \forall \pi\,t_1\ldots t_n\\[1mm] - \;\;\;\;R\,t_1\ldots t_n \Rightarrow R (\pi\act t_1)\ldots(\pi\act t_n) - \end{array}} - \end{center} - % - This means the relation has to be invariant under permutative renaming of - variables.\smallskip - - \small - (This property can be checked automatically if the inductive definition is composed of - equivariant ``things''.) - }; - \end{tikzpicture}} - \end{textblock} - - \only<3>{} - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -*} - -text_raw {* - - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame} - \frametitle{\mbox{Honest Toil, No Theft!}} - - \begin{itemize} - \item The \underline{sacred} principle of HOL: - - \begin{block}{} - ``The method of `postulating' what we want has many advantages; they are - the same as the advantages of theft over honest toil.''\\[2mm] - \hfill{}\footnotesize B.~Russell, Introduction of Mathematical Philosophy - \end{block}\bigskip\medskip - - \item I will show next that the \underline{weak} structural induction - principle implies the \underline{strong} structural induction principle.\\[3mm] - - \textcolor{gray}{(I am only going to show the lambda-case.)} - \end{itemize} - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -*} - -text_raw {* - - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame} - \frametitle{Permutations} - - A permutation \alert{\bf acts} on variable names as follows: - - \begin{center} - \begin{tabular}{rcl} - $\smath{{[]}\act a}$ & $\smath{\dn}$ & $\smath{a}$\\ - $\smath{(\swap{a_1}{a_2}\!::\!\pi)\act a}$ & $\smath{\dn}$ & - $\smath{\begin{cases} - a_1 &\text{if $\pi\act a = a_2$}\\ - a_2 &\text{if $\pi\act a = a_1$}\\ - \pi\act a &\text{otherwise} - \end{cases}}$ - \end{tabular} - \end{center} - - \begin{itemize} - \item $\smath{[]}$ stands for the empty list (the identity permutation), and\smallskip - \item $\smath{\swap{a_1}{a_2}\!::\!\pi}$ stands for the permutation $\smath{\pi}$ - followed by the swapping $\smath{\swap{a_1}{a_2}}$. - \end{itemize} - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -*} - -text_raw {* - - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame} - \frametitle{\Large\mbox{Permutations on Lambda-Terms}} - - \begin{itemize} - \item Permutations act on lambda-terms as follows: - - \begin{center} - \begin{tabular}{rcl} - $\smath{\pi\act\,x}$ & $\smath{\dn}$ & ``action on variables''\\ - $\smath{\pi\act\, (t_1~t_2)}$ & $\smath{\dn}$ & $\smath{(\pi\act t_1)~(\pi\act t_2)}$\\ - $\smath{\pi\act(\lambda x.t)}$ & $\smath{\dn}$ & $\smath{\lambda (\pi\act x).(\pi\act t)}$\\ - \end{tabular} - \end{center}\medskip - - \item Alpha-equivalence can be defined as: - - \begin{center} - \begin{tabular}{c} - \colorbox{cream}{\smath{\infer{\lambda x.t_1 = \lambda x.t_2}{t_1=t_2}}}\\[3mm] - \colorbox{cream}{\smath{\infer{\lambda x.t_1 - \tikz[baseline=-3pt,remember picture] \node (e1) {\alert<2>{$=$}}; - \lambda y.t_2} - {x\not=y & t_1 = \swap{x}{y}\act t_2 & x\fresh t_2}}} - \end{tabular} - \end{center} - - \end{itemize} - - - \begin{textblock}{4}(8.3,14.2) - \only<2>{ - \begin{tikzpicture}[remember picture] - \draw (0,0) node[fill=cream, text width=5.5cm, thick, draw=red, rounded corners=1mm] (e2) - {\small Notice, I wrote equality here!}; - - \path[overlay, ->, ultra thick, red] (e2) edge[out=180, in=-90] (e1); - \end{tikzpicture}} - \end{textblock} - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -*} - -text_raw {* - - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame} - \frametitle{My Claim} - - \begin{center} - \colorbox{cream}{% - \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} - }}}\medskip - - \begin{tikzpicture} - \node at (0,0) [single arrow, single arrow tip angle=140, - shape border rotate=270, fill=red,text=white]{implies}; - \end{tikzpicture}\medskip - - \colorbox{cream}{% - \smath{% - \infer{P c\,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.\; - x\fresh c \wedge (\forall d.\,P d\,t)\Rightarrow P c\,(\lambda x.t) - \end{array}}}} - - \end{center} - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -*} - -text_raw {* - - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame} - \frametitle{\large\mbox{Proof for the Strong Induction Principle}} - - \begin{textblock}{14}(1.2,1.7) - \begin{itemize} - \item<1-> We prove \alt<1>{\smath{P c\,t}}{\smath{\forall \pi\,c.\;P c\,(\pi\act t)}} - by induction on \smath{t}. - - \item<3-> I.e., we have to show \alt<3>{\smath{P c\,(\pi\act(\lambda x.t))}} - {\smath{P c\,\lambda(\pi\act x).(\pi\act t)}}. - - \item<5-> We have \smath{\forall \pi\,c.\;P c\,(\pi\act t)} by induction. - - - \item<6-> Our weaker precondition says that:\\ - \begin{center} - \smath{\forall x\,t\,c.\,x\fresh c \wedge (\forall c.\,P c\,t) \Rightarrow P c\,(\lambda x.t)} - \end{center} - - \item<7-> We choose a fresh \smath{y} such that \smath{y\fresh (\pi\act x,\pi\act t,c)}. - - \item<8-> Now we can use - \alt<8>{\smath{\forall c.\;P c\,((\swap{y}{\,\pi\act x}\!::\!\pi)\act t)}} - {\smath{\forall c.\;P c\,(\swap{y}{\,\pi\act x}\act\pi\act t)}} \only<10->{to infer} - - \only<10->{ - \begin{center} - \smath{P\,c\,\lambda y.(\swap{y}{\,\pi\act x}\act\pi\act t)} - \end{center}} - - \item<11-> However - \begin{center} - \smath{\lambda y.(\swap{y}{\,\pi\act x}\act\pi\act t) - \textcolor{red}{\;=\;}\lambda (\pi\act x).(\pi\act t)} - \end{center} - - \item<12> Therefore \smath{P\,c\,\lambda (\pi\act x).(\pi\act t)} and we are done. - \end{itemize} - \end{textblock} - - \only<11->{ - \begin{textblock}{9}(7,6) - \begin{tikzpicture}[remember picture, overlay] - \draw (0,0) node[fill=cream, text width=7cm, thick, draw=red, rounded corners=1mm] (n2) - {\centering - \smath{\infer{\lambda y.t_1=\lambda x.t_2}{x\not=y & t_1=\swap{x}{y}\act t_2 & - y\fresh t_2}} - }; - \end{tikzpicture} - \end{textblock}} - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -*} - -text_raw {* - - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}<3->[squeeze] - \frametitle{Formalisation of LF} - - - \begin{center} - \begin{tabular}{@ {\hspace{-16mm}}lc} - \mbox{}\\[-6mm] - - \textcolor{white}{\raisebox{4mm}{1.~Solution}} & - \begin{tikzpicture} - [node distance=25mm, - text height=1.5ex, - text depth=.25ex, - node1/.style={ - rectangle, minimum size=10mm, rounded corners=3mm, very thick, - draw=black!50, top color=white, bottom color=black!20}, - ] - - \node (proof) [node1] {\large Proof}; - \node (def) [node1, left of=proof] {\large$\,\;\dn\;\,$}; - \node (alg) [node1, right of=proof] {\large\hspace{1mm}Alg.\hspace{1mm}\mbox{}}; - - \draw[->,black!50,line width=2mm] (proof) -- (def); - \draw[->,black!50,line width=2mm] (proof) -- (alg); - - \onslide<2->{\draw[white,line width=1mm] (0.1,0.6) -- (-0.1,0.25) -- (0.1,-0.25) -- (-0.1,-0.6);} - \end{tikzpicture} - \\[2mm] - - \onslide<3->{% - \raisebox{4mm}{1st Solution} & - \begin{tikzpicture} - [node distance=25mm, - text height=1.5ex, - text depth=.25ex, - node1/.style={ - rectangle, minimum size=10mm, rounded corners=3mm, very thick, - draw=black!50, top color=white, bottom color=black!20}, - node2/.style={ - rectangle, minimum size=12mm, rounded corners=3mm, very thick, - draw=red!70, top color=white, bottom color=red!50!black!20} - ] - - \node (proof) [node1] {\large Proof}; - \node (def) [node2, left of=proof] {\large$\dn{}\!\!^\text{+ex}$}; - \node (alg) [node1, right of=proof] {\large\hspace{1mm}Alg.\hspace{1mm}\mbox{}}; - - \draw[->,black!50,line width=2mm] (proof) -- (def); - \draw[->,black!50,line width=2mm] (proof) -- (alg); - - \end{tikzpicture} - \\[2mm]} - - \onslide<4->{% - \raisebox{4mm}{\hspace{-1mm}2nd Solution} & - \begin{tikzpicture} - [node distance=25mm, - text height=1.5ex, - text depth=.25ex, - node1/.style={ - rectangle, minimum size=10mm, rounded corners=3mm, very thick, - draw=black!50, top color=white, bottom color=black!20}, - node2/.style={ - rectangle, minimum size=12mm, rounded corners=3mm, very thick, - draw=red!70, top color=white, bottom color=red!50!black!20} - ] - - \node (proof) [node1] {\large Proof}; - \node (def) [node1, left of=proof] {\large$\,\;\dn\;\,$}; - \node (alg) [node2, right of=proof] {\large Alg.$\!^\text{-ex}$}; - - \draw[->,black!50,line width=2mm] (proof) -- (def); - \draw[->,black!50,line width=2mm] (proof) -- (alg); - - \end{tikzpicture} - \\[2mm]} - - \onslide<5->{% - \raisebox{4mm}{\hspace{-1mm}3rd Solution} & - \begin{tikzpicture} - [node distance=25mm, - text height=1.5ex, - text depth=.25ex, - node1/.style={ - rectangle, minimum size=10mm, rounded corners=3mm, very thick, - draw=black!50, top color=white, bottom color=black!20}, - node2/.style={ - rectangle, minimum size=12mm, rounded corners=3mm, very thick, - draw=red!70, top color=white, bottom color=red!50!black!20} - ] - - \node (proof) [node2] {\large Proof}; - \node (def) [node1, left of=proof] {\large$\,\;\dn\;\,$}; - \node (alg) [node1, right of=proof] {\large\hspace{1mm}Alg.\hspace{1mm}\mbox{}}; - - \draw[->,black!50,line width=2mm] (proof) -- (def); - \draw[->,black!50,line width=2mm] (proof) -- (alg); - - \end{tikzpicture} - \\} - - \end{tabular} - \end{center} - - \begin{textblock}{3}(13.2,5.1) - \onslide<3->{ - \begin{tikzpicture} - \node at (0,0) [single arrow, shape border rotate=270, fill=red,text=white]{2h}; - \end{tikzpicture} - } - \end{textblock} - - - \begin{textblock}{13}(1.4,15) - \only<3->{\footnotesize (each time one needs to check $\sim$31pp~of informal paper proofs)} - \end{textblock} - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -*} - - -text_raw {* - - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame} - \frametitle{Conclusions} - - \begin{itemize} - \item The Nominal Isabelle automatically derives the strong structural - induction principle for \underline{\bf all} nominal datatypes (not just the - lambda-calculus); - - \item also for rule inductions (though they have to satisfy the vc-condition). - - \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{ - \begin{frame} - \frametitle{\begin{tabular}{c}Nominal Meets\\[-2mm] Automata Theory\end{tabular}} - - \begin{itemize} - \item<1-> So what?\bigskip\medskip - - \item<2-> I can give you a good argument why regular expressions - are much, much better than automata. \textcolor{darkgray}{(over dinner?)}\medskip - - \item<3-> Nominal automata?\bigskip\bigskip\medskip - \end{itemize} - - - \onslide<2->{ - \footnotesize\textcolor{darkgray}{A Formalisation of the Myhill-Nerode Theorem based on - Regular Expressions (by Wu, Zhang and Urban)} - } - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -*} - - - -text_raw {* - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame} - \frametitle{Quiz} - %%%\small - \mbox{}\\[-9mm] - - Imagine\ldots\\[2mm] - - \begin{tabular}{@ {\hspace{1cm}}l} - \textcolor{blue}{Var\;``name''} \\ - \textcolor{blue}{App\;``lam''\;''lam''}\\ - \textcolor{blue}{Lam\;``\flqq{}name\frqq{}lam''} \\ - \textcolor{red}{Foo\;``\flqq{}name\frqq{}\flqq{}name\frqq{}lam''\;`` - \flqq{}name\frqq{}\flqq{}name\frqq{}lam''}\\[2mm] - \end{tabular} - - That means roughly:\\[2mm] - - \begin{tabular}{@ {\hspace{1cm}}l} - \alert{Foo\;($\lambda x.y.t_1$)\;($\lambda z.u.t_2$)} - \end{tabular} - - \begin{itemize} - \item What does the variable convention look like for \alert{Foo}? - \item What does the clause for capture-avoiding substitution look like? - \end{itemize} - - \footnotesize - Answers: Download Nominal Isabelle and try it out\\ - \textcolor{white}{Answers:} http://isabelle.in.tum.de/nominal\\ - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -*} - -text_raw {* - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}<1>[b] - \frametitle{ - \begin{tabular}{c} - \mbox{}\\[13mm] - \alert{\LARGE Thank you very much!}\\ - \alert{\Large Questions?} - \end{tabular}} - - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -*} - -(*<*) -end -(*>*) \ No newline at end of file