
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<presentation>{
@@ -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 "\<Rightarrow>"} nice textbooks: Kozen, Hopcroft \& Ullman
+  \mbox{}\;\;@{text "\<Rightarrow>"} 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 "\<Rightarrow>"}\; state nodes\medskip}
+  \only<6->{A solution:\;\;use \smath{\text{nat}} \;@{text "\<Rightarrow>"}\; 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 "\<Rightarrow>"}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<presentation>{
   \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<presentation>{
+  \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<presentation>{
   \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<presentation>{
-  \begin{frame}[c]
-  \frametitle{\mbox{}\\[2cm]\textcolor{red}{Questions?}}
-
-
+  \begin{frame}[b]
+  \frametitle{\mbox{}\\[2cm]\textcolor{red}{Thank you!\\[5mm]Questions?}}
 
   \end{frame}}
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     




