--- 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}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%