# HG changeset patch # User urbanc # Date 1314224334 0 # Node ID dda2e90de8a2a3f22973df1d4ddfdb05322768dc # Parent 3629680a20a271c4e357d4f2f56a8fd69e325f70 final slides diff -r 3629680a20a2 -r dda2e90de8a2 Slides/Slides1.thy --- a/Slides/Slides1.thy Wed Aug 24 10:01:24 2011 +0000 +++ b/Slides/Slides1.thy Wed Aug 24 22:18:54 2011 +0000 @@ -13,8 +13,8 @@ text_raw {* %\renewcommand{\slidecaption}{Cambridge, 9 November 2010} \renewcommand{\slidecaption}{Nijmegen, 25 August 2011} - %%\renewcommand{\ULthickness}{2pt} - \newcommand{\sout}[1]{\tikz[baseline=(X.base), inner sep=0pt, outer sep=0pt] + \newcommand{\bl}[1]{#1} + \newcommand{\sout}[1]{\tikz[baseline=(X.base), inner sep=-0.1pt, outer sep=0pt] \node [cross out,red, ultra thick, draw] (X) {\textcolor{black}{#1}};} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \mode{ @@ -59,8 +59,8 @@ \begin{textblock}{12.9}(1.5,3.2) \begin{block}{} \begin{minipage}{12.4cm}\raggedright - \large I want to teach \alert{students} with\\ - theorem provers (especially inductions). + \large I want to teach \alert{students} with + theorem\\ provers (especially for inductions). \end{minipage} \end{block} \end{textblock}\pause @@ -71,7 +71,7 @@ \item \only<2>{\smath{\text{fib}}, \smath{\text{even}} and \smath{\text{odd}}}% \only<3->{\sout{\smath{\text{fib}}, \smath{\text{even}} and \smath{\text{odd}}}}\medskip \item<3-> formal language theory \\ - \mbox{}\;\;@{text "\"} nice textbooks: Kozen, Hopcroft \& Ullman + \mbox{}\;\;@{text "\"} nice textbooks: Kozen, Hopcroft \& Ullman\ldots \end{itemize} \end{frame}} @@ -92,7 +92,7 @@ \begin{itemize} \item Constable, Jackson, Naumov, Uribe\medskip - \item \alert{18 months} for automata theory, Hopcroft \& Ullman chapters 1--11 (including Myhill-Nerode) + \item \alert{18 months} for automata theory from Hopcroft \& Ullman chapters 1--11 (including Myhill-Nerode) \end{itemize} \end{frame}} @@ -215,7 +215,7 @@ \end{textblock}} \medskip - \only<6->{A solution:\;\;\smath{\text{nat}} \;@{text "\"}\; state nodes\medskip} + \only<6->{A solution:\;\;use \smath{\text{nat}} \;@{text "\"}\; state nodes\medskip} \only<7->{You have to \alert{\underline{rename}} states!} @@ -268,12 +268,12 @@ {\noindent\large\bf\alert{\ldots{}and forget about automata}}\bigskip\bigskip\pause - Infrastructure for free. Do we lose anything?\pause + Infrastructure for free. But do we lose anything?\pause \begin{itemize} \item pumping lemma\pause \item closure under complementation\pause \item \only<6>{regular expression matching}% - \only<7->{\sout{regular expression matching}} + \only<7->{\sout{regular expression matching} \;\;(@{text "\"}Owens et al)} \item<8-> most textbooks are about automata \end{itemize} @@ -395,9 +395,9 @@ \end{center} \begin{itemize} - \item \smath{\text{final}_A\,X \dn \{[\!|x|\!]_{\approx_{A}}\;|\;x \in A\}} + \item \smath{\text{finals}\,A\,\dn \{[\!|x|\!]_{\approx_{A}}\;|\;x \in A\}} \smallskip - \item we can prove: \smath{A = \bigcup \{X.\;\text{final}_A\,X\}} + \item we can prove: \smath{A = \bigcup \text{finals}\,A} \end{itemize} \only<2->{% @@ -435,8 +435,10 @@ \draw[step=2mm, very thick] (-1.4,-1.4) grid (1.4,1.4); \draw[blue, fill] (0.0, 0.6) rectangle (0.2, 0.8); \draw[blue, fill] (0.8, 0.4) rectangle (1.0, 0.6); - \draw[white] (0.1,0.7) node {$X$}; - \draw[white] (0.9,0.5) node {$Y$}; + \draw[white] (0.1,0.7) node (X) {$X$}; + \draw[white] (0.9,0.5) node (Y) {$Y$}; + \draw[blue, ->, line width = 2mm, bend left=45] (X) -- (Y); + \node [inner sep=1pt,label=above:\textcolor{blue}{$c$}] at ($ (X)!.5!(Y) $) {}; \end{tikzpicture} \end{center} @@ -473,8 +475,8 @@ %\draw[help lines] (0,0) grid (3,2); - \node[state,initial] (p_0) {$R_1$}; - \node[state,accepting] (p_1) [right of=q_0] {$R_2$}; + \node[state,initial] (p_0) {$X_1$}; + \node[state,accepting] (p_1) [right of=q_0] {$X_2$}; \path[->] (p_0) edge [bend left] node {a} (p_1) edge [loop above] node {b} () @@ -487,8 +489,8 @@ \begin{center} \begin{tabular}{@ {\hspace{-6mm}}ll@ {\hspace{1mm}}c@ {\hspace{1mm}}l} - & \smath{R_1} & \smath{\equiv} & \smath{R_1;b + R_2;b \onslide<2->{\alert<2>{+ \lambda;[]}}}\\ - & \smath{R_2} & \smath{\equiv} & \smath{R_1;a + R_2;a}\medskip\\ + & \smath{X_1} & \smath{=} & \smath{X_1;b + X_2;b \onslide<2->{\alert<2>{+ \lambda;[]}}}\\ + & \smath{X_2} & \smath{=} & \smath{X_1;a + X_2;a}\medskip\\ \end{tabular} \end{center} @@ -505,44 +507,44 @@ \begin{center} \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}ll} - \onslide<1->{\smath{R_1}} & \onslide<1->{\smath{=}} - & \onslide<1->{\smath{R_1; b + R_2; b + \lambda;[]}}\\ - \onslide<1->{\smath{R_2}} & \onslide<1->{\smath{=}} - & \onslide<1->{\smath{R_1; a + R_2; a}}\\ + \onslide<1->{\smath{X_1}} & \onslide<1->{\smath{=}} + & \onslide<1->{\smath{X_1; b + X_2; b + \lambda;[]}}\\ + \onslide<1->{\smath{X_2}} & \onslide<1->{\smath{=}} + & \onslide<1->{\smath{X_1; a + X_2; a}}\\ & & & \onslide<2->{by Arden}\\ - \onslide<2->{\smath{R_1}} & \onslide<2->{\smath{=}} - & \onslide<2->{\smath{R_1; b + R_2; b + \lambda;[]}}\\ - \onslide<2->{\smath{R_2}} & \onslide<2->{\smath{=}} - & \only<2->{\smath{R_1; a\cdot a^\star}}\\ + \onslide<2->{\smath{X_1}} & \onslide<2->{\smath{=}} + & \onslide<2->{\smath{X_1; b + X_2; b + \lambda;[]}}\\ + \onslide<2->{\smath{X_2}} & \onslide<2->{\smath{=}} + & \only<2->{\smath{X_1; a\cdot a^\star}}\\ & & & \onslide<4->{by Arden}\\ - \onslide<4->{\smath{R_1}} & \onslide<4->{\smath{=}} - & \onslide<4->{\smath{R_2; b \cdot b^\star+ \lambda;b^\star}}\\ - \onslide<4->{\smath{R_2}} & \onslide<4->{\smath{=}} - & \onslide<4->{\smath{R_1; a\cdot a^\star}}\\ + \onslide<4->{\smath{X_1}} & \onslide<4->{\smath{=}} + & \onslide<4->{\smath{X_2; b \cdot b^\star+ \lambda;b^\star}}\\ + \onslide<4->{\smath{X_2}} & \onslide<4->{\smath{=}} + & \onslide<4->{\smath{X_1; a\cdot a^\star}}\\ & & & \onslide<5->{by substitution}\\ - \onslide<5->{\smath{R_1}} & \onslide<5->{\smath{=}} - & \onslide<5->{\smath{R_1; a\cdot a^\star \cdot b \cdot b^\star+ \lambda;b^\star}}\\ - \onslide<5->{\smath{R_2}} & \onslide<5->{\smath{=}} - & \onslide<5->{\smath{R_1; a\cdot a^\star}}\\ + \onslide<5->{\smath{X_1}} & \onslide<5->{\smath{=}} + & \onslide<5->{\smath{X_1; a\cdot a^\star \cdot b \cdot b^\star+ \lambda;b^\star}}\\ + \onslide<5->{\smath{X_2}} & \onslide<5->{\smath{=}} + & \onslide<5->{\smath{X_1; a\cdot a^\star}}\\ & & & \onslide<6->{by Arden}\\ - \onslide<6->{\smath{R_1}} & \onslide<6->{\smath{=}} + \onslide<6->{\smath{X_1}} & \onslide<6->{\smath{=}} & \onslide<6->{\smath{\lambda;b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star}}\\ - \onslide<6->{\smath{R_2}} & \onslide<6->{\smath{=}} - & \onslide<6->{\smath{R_1; a\cdot a^\star}}\\ + \onslide<6->{\smath{X_2}} & \onslide<6->{\smath{=}} + & \onslide<6->{\smath{X_1; a\cdot a^\star}}\\ & & & \onslide<7->{by substitution}\\ - \onslide<7->{\smath{R_1}} & \onslide<7->{\smath{=}} + \onslide<7->{\smath{X_1}} & \onslide<7->{\smath{=}} & \onslide<7->{\smath{\lambda;b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star}}\\ - \onslide<7->{\smath{R_2}} & \onslide<7->{\smath{=}} + \onslide<7->{\smath{X_2}} & \onslide<7->{\smath{=}} & \onslide<7->{\smath{\lambda; b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star \cdot a\cdot a^\star}}\\ \end{tabular} @@ -558,8 +560,8 @@ %\draw[help lines] (0,0) grid (3,2); - \node[state,initial] (p_0) {$R_1$}; - \node[state,accepting] (p_1) [right of=q_0] {$R_2$}; + \node[state,initial] (p_0) {$X_1$}; + \node[state,accepting] (p_1) [right of=q_0] {$X_2$}; \path[->] (p_0) edge [bend left] node {a} (p_1) edge [loop above] node {b} () @@ -571,6 +573,65 @@ \end{block} \end{textblock}} + \only<1,2>{% + \begin{textblock}{3}(0.6,1.2) + \begin{tikzpicture} + \node at (0,0) [single arrow, fill=red,text=white, minimum height=0cm] + {\textcolor{red}{a}}; + \end{tikzpicture} + \end{textblock}} + \only<2>{% + \begin{textblock}{3}(0.6,3.6) + \begin{tikzpicture} + \node at (0,0) [single arrow, fill=red,text=white, minimum height=0cm] + {\textcolor{red}{a}}; + \end{tikzpicture} + \end{textblock}} + \only<4>{% + \begin{textblock}{3}(0.6,2.9) + \begin{tikzpicture} + \node at (0,0) [single arrow, fill=red,text=white, minimum height=0cm] + {\textcolor{red}{a}}; + \end{tikzpicture} + \end{textblock}} + \only<4>{% + \begin{textblock}{3}(0.6,5.3) + \begin{tikzpicture} + \node at (0,0) [single arrow, fill=red,text=white, minimum height=0cm] + {\textcolor{red}{a}}; + \end{tikzpicture} + \end{textblock}} + \only<5>{% + \begin{textblock}{3}(1.0,5.6) + \begin{tikzpicture} + \node at (0,0) (A) {}; + \node at (0,1) (B) {}; + \draw[<-, line width=2mm, red] (B) to (A); + \end{tikzpicture} + \end{textblock}} + \only<5,6>{% + \begin{textblock}{3}(0.6,7.7) + \begin{tikzpicture} + \node at (0,0) [single arrow, fill=red,text=white, minimum height=0cm] + {\textcolor{red}{a}}; + \end{tikzpicture} + \end{textblock}} + \only<6>{% + \begin{textblock}{3}(0.6,10.1) + \begin{tikzpicture} + \node at (0,0) [single arrow, fill=red,text=white, minimum height=0cm] + {\textcolor{red}{a}}; + \end{tikzpicture} + \end{textblock}} + \only<7>{% + \begin{textblock}{3}(1.0,10.3) + \begin{tikzpicture} + \node at (0,0) (A) {}; + \node at (0,1) (B) {}; + \draw[->, line width=2mm, red] (B) to (A); + \end{tikzpicture} + \end{textblock}} + \end{frame}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *} @@ -580,7 +641,7 @@ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \mode{ \begin{frame}[c] - \frametitle{\LARGE Other Direction} + \frametitle{\LARGE The Other Direction} One has to prove @@ -624,7 +685,11 @@ \end{tabular}} \end{center} - + \begin{textblock}{5}(9.8,2.6) + \begin{tikzpicture} + \node at (0,0) [shape border rotate=270,single arrow, fill=red,text=white, minimum height=0cm]{\textcolor{red}{a}}; + \end{tikzpicture} + \end{textblock} \end{frame}} @@ -634,13 +699,45 @@ text_raw {* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \mode{ + \begin{frame}[t] + \frametitle{\LARGE Partial Derivatives} + + \begin{itemize} + \item \ldots (set of) regular expressions after a string + has been parsed\\[10mm] + + + \item \alt<1>{\smath{\text{pders x r \mbox{$=$} pders y r}}} + {\smath{\underbrace{\text{pders x r \mbox{$=$} pders y r}}_{R_1}}} + refines \textcolor{blue}{x $\approx_{{\cal L}(\text{r})}$ y}\\[16mm]\pause + \item \smath{\text{finite} (U\!N\!IV /\!/ R_1)} \bigskip\pause + \item Therefore \smath{\text{finite} (U\!N\!IV /\!/ \approx_{{\cal L}(r)})}. Qed. + \end{itemize} + + \only<2->{% + \begin{textblock}{5}(3.8,8.3) + \begin{tikzpicture} + \node at (0,0) [shape border rotate=270,single arrow, fill=red,text=white, minimum height=0cm]{\textcolor{red}{a}}; + \draw (2.2,0) node {Antimirov '95}; + \end{tikzpicture} + \end{textblock}} + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + + + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ \begin{frame}[c] \frametitle{\LARGE What Have We Achieved?} \begin{itemize} \item \smath{\text{finite}\, (U\!N\!IV /\!/ \approx_A) \;\Leftrightarrow\; A\; \text{is regular}} \bigskip\pause - \item regular languages are closed under complementation; this is easy + \item regular languages are closed under complementation; this is now easy \begin{center} \smath{U\!N\!IV /\!/ \approx_A \;\;=\;\; U\!N\!IV /\!/ \approx_{\overline{A}}} \end{center}\pause\bigskip @@ -651,7 +748,7 @@ \begin{minipage}{8.8cm} \begin{block}{} \begin{minipage}{8.6cm} - If there exists a sufficiently large set \smath{B} (for example infinite), + If there exists a sufficiently large set \smath{B} (for example infinitely large), such that \begin{center} @@ -663,7 +760,7 @@ \end{block} \end{minipage}\medskip\pause - \small(\smath{A \dn \bigcup_i a^i}) + \small(\smath{A \dn \bigcup_n a^n}) \end{quote} \end{itemize} @@ -700,7 +797,7 @@ \item second direction (400 / 390 loc)\pause \end{itemize}\smallskip - \item I have \alert{\bf not} yet used it for teaching of undergraduates.\pause + \item I have \alert{\bf not} yet used it in teaching for undergraduates.\pause \end{itemize} @@ -710,10 +807,10 @@ \begin{minipage}{11cm}\raggedright \large - {\bf Bold Claim }\alert{(not proved!)}\medskip + {\bf Bold Claim: }\alert{(not proved!)}\medskip {\bf 95\%} of regular language theory can be done without - automata\medskip\\\ldots this is much more tasteful. ;o) + automata!\medskip\\\ldots and this is much more tasteful ;o) \end{minipage} \end{block} @@ -726,10 +823,8 @@ text_raw {* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \mode{ - \begin{frame}[c] - \frametitle{\mbox{}\\[2cm]\textcolor{red}{Questions?}} - - + \begin{frame}[b] + \frametitle{\mbox{}\\[2cm]\textcolor{red}{Thank you!\\[5mm]Questions?}} \end{frame}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% diff -r 3629680a20a2 -r dda2e90de8a2 Slides/document/root.tex --- a/Slides/document/root.tex Wed Aug 24 10:01:24 2011 +0000 +++ b/Slides/document/root.tex Wed Aug 24 22:18:54 2011 +0000 @@ -16,6 +16,7 @@ \usetikzlibrary{automata} \usetikzlibrary{shapes} \usetikzlibrary{shadows} +\usetikzlibrary{calc} % Isabelle configuration %%\urlstyle{rm}