
diff -r bef3af148df5 -r 6e5d17a808d1 Slides/Slides1.thy
--- a/Slides/Slides1.thy	Tue Aug 23 08:42:51 2011 +0000
+++ b/Slides/Slides1.thy	Tue Aug 23 11:53:25 2011 +0000
@@ -268,7 +268,7 @@
   
   {\noindent\large\bf\alert{\ldots{}and forget about automata}}\bigskip\bigskip\pause
 
-  Do we lose anything?\pause
+  Infrastructure for free. Do we lose anything?\pause
   \begin{itemize}
   \item pumping lemma\pause
   \item closure under complementation\pause
@@ -302,18 +302,7 @@
   \end{center}
   \end{itemize}
 
-  \only<2->
-  \begin{textblock}{9.9}(0.7,1.2)
-  \begin{block}{}
-  \begin{minipage}{9.4cm}\raggedright
-  Two directions:\smallskip\\
-
-  1.) \\
-  2.) \\
-  \end{minipage}
-  \end{block}
-  \end{textblock}}
-
+ 
   \end{frame}}
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
 
@@ -328,37 +317,25 @@
   \mbox{}\\[5cm]
 
   \begin{itemize}
-  \item \smath{\text{finite}\, (U\!N\!IV /\!/ \approx_L) \;\Leftrightarrow\; L\; \text{is regular}}
+  \item \smath{\text{finite}\, (U\!N\!IV /\!/ \approx_A) \;\Leftrightarrow\; A\; \text{is regular}}
   \end{itemize}
 
-  \end{frame}}
-  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
-
-*}
-
-
-text_raw {*
-  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-  \mode<presentation>{
-  \begin{frame}[c]
-  \frametitle{\LARGE Regular Languages}
+  \only<2->{
+  \begin{textblock}{11.9}(1.7,3)
+  \begin{block}{}
+  \begin{minipage}{11.4cm}\raggedright
+  Two directions:\medskip\\
 
-  \begin{itemize}
-  \item \smath{L} is regular \smath{\dn} if there is an automaton \smath{M} 
-  such that \smath{\mathbb{L}(M) = L}\\[1.5cm]
-
-  \item Myhill-Nerode:
+  \begin{tabular}{@ {}ll}
+  1.)\;finite $\Rightarrow$ regular\\
+  \;\;\;\smath{\text{finite}\,(U\!N\!IV /\!/ \approx_A) \Rightarrow \exists r.\;A = {\cal L}(r)}\\[3mm]
+  2.)\;regular $\Rightarrow$ finite\\
+  \;\;\;\smath{\text{finite}\, (U\!N\!IV /\!/ \approx_{{\cal L}(r)})}
+  \end{tabular}
 
-  \begin{center}
-  \begin{tabular}{l}
-  finite $\Rightarrow$ regular\\
-  \;\;\;\smath{\text{finite}\,(U\!N\!IV /\!/ \approx_L) \Rightarrow \exists r. L = \mathbb{L}(r)}\\[3mm]
-  regular $\Rightarrow$ finite\\
-  \;\;\;\smath{\text{finite}\, (U\!N\!IV /\!/ \approx_{\mathbb{L}(r)})}
-  \end{tabular}
-  \end{center}
-
-  \end{itemize}
+  \end{minipage}
+  \end{block}
+  \end{textblock}}
 
   \end{frame}}
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
@@ -375,10 +352,10 @@
   \mbox{}\\[3cm]
 
   \begin{itemize}
-  \item \smath{\text{final}_L\,X \dn}\\
-  \smath{\hspace{6mm}X \in (U\!N\!IV /\!/\approx_L) \;\wedge\; \forall s \in X.\; s \in L}
+  \item \smath{\text{final}_A\,X \dn}\\
+  \smath{\hspace{6mm}X \in (U\!N\!IV /\!/\approx_A) \;\wedge\; \forall s \in X.\; s \in A}
   \smallskip
-  \item we can prove: \smath{L = \bigcup \{X.\;\text{final}_L\,X\}}
+  \item we can prove: \smath{A = \bigcup \{X.\;\text{final}_A\,X\}}
 
   \end{itemize}
 
@@ -391,7 +368,7 @@
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \mode<presentation>{
   \begin{frame}[c]
-  \frametitle{\LARGE Transitions between\\[-3mm] Equivalence Classes}
+  \frametitle{\LARGE Transitions between Eq-Classes}
 
   \smath{L = \{[c]\}}
 
@@ -463,11 +440,6 @@
   \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\\
-  \onslide<3->{we can prove} 
-  & \onslide<3->{\smath{R_1}} & \onslide<3->{\smath{=}} 
-      & \onslide<3->{\smath{R_1; \mathbb{L}(b) \,\cup\, R_2;\mathbb{L}(b) \,\cup\, \{[]\};\{[]\}}}\\
-  & \onslide<3->{\smath{R_2}} & \onslide<3->{\smath{=}}    
-      & \onslide<3->{\smath{R_1; \mathbb{L}(a) \,\cup\, R_2;\mathbb{L}(a)}}\\
   \end{tabular}
   \end{center}
 
@@ -537,7 +509,7 @@
   \begin{frame}[c]
   \frametitle{\LARGE A Variant of Arden's Lemma}
 
-  {\bf Arden's Lemma:}\smallskip 
+  {\bf ``Reversed'' Arden's Lemma:}\medskip 
 
   If \smath{[] \not\in A} then
   \begin{center}
@@ -633,38 +605,6 @@
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
 *}
 
-text_raw {*
-  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-  \mode<presentation>{
-  \begin{frame}[c]
-  \frametitle{\LARGE The Equ's Solving Algorithm}
-
-  \begin{itemize}
-  \item The algorithm must terminate: Arden makes one equation smaller; 
-  substitution deletes one variable from the right-hand sides.\bigskip
-
-  \item We need to maintain the invariant that Arden is applicable
-  (if \smath{[] \not\in A} then \ldots):\medskip
-
-  \begin{center}\small
-  \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}ll}
-  \smath{R_1} & \smath{=} & \smath{R_1; b + R_2; b + \lambda;[]}\\
-  \smath{R_2} & \smath{=} & \smath{R_1; a + R_2; a}\\
-
-  & & & by Arden\\
-
-  \smath{R_1} & \smath{=} & \smath{R_1; b + R_2; b + \lambda;[]}\\
-  \smath{R_2} & \smath{=} & \smath{R_1; a\cdot a^\star}\\
-  \end{tabular}
-  \end{center}
-
-  \end{itemize}
-
-
-  \end{frame}}
-  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
-*}
-
 
 text_raw {*
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -675,22 +615,45 @@
   One has to prove
 
   \begin{center}
-  \smath{\text{finite} (U\!N\!IV /\!/ \approx_{\mathbb{L}(r)})}
+  \smath{\text{finite} (U\!N\!IV /\!/ \approx_{{\cal L}(r)})}
   \end{center}
 
   by induction on \smath{r}. Not trivial, but after a bit 
-  of thinking (by Chunhan), one can prove that if
+  of thinking, one can find a \alert{refined} relation:\bigskip
 
+  
   \begin{center}
-  \smath{\text{finite} (U\!N\!IV /\!/ \approx_{\mathbb{L}(r_1)})}\hspace{5mm}
-  \smath{\text{finite} (U\!N\!IV /\!/ \approx_{\mathbb{L}(r_2)})}
+  \mbox{\begin{tabular}{c@ {\hspace{7mm}}c@ {\hspace{7mm}}c}
+  \begin{tikzpicture}[scale=1.1]
+  %Circle
+  \draw[thick] (0,0) circle (1.1);    
+  \end{tikzpicture}
+  &
+  \begin{tikzpicture}[scale=1.1]
+  %Circle
+  \draw[thick] (0,0) circle (1.1);    
+  %Main rays
+  \foreach \a in {0, 90,...,359}
+    \draw[very thick] (0, 0) -- (\a:1.1);
+  \foreach \a / \l in {45/1, 135/2, 225/3, 315/4}
+      \draw (\a: 0.65) node {\small$a_\l$};
+  \end{tikzpicture}
+  &
+  \begin{tikzpicture}[scale=1.1]
+  %Circle
+  \draw[red, thick] (0,0) circle (1.1);    
+  %Main rays
+  \foreach \a in {0, 45,...,359}
+     \draw[red, very thick] (0, 0) -- (\a:1.1);
+  \foreach \a / \l in {22.5/1.1, 67.5/1.2, 112.5/2.1, 157.5/2.2, 202.4/3.1, 247.5/3.2, 292.5/4.1, 337.5/4.2}
+      \draw (\a: 0.77) node {\textcolor{red}{\footnotesize$a_{\l}$}};
+  \end{tikzpicture}\\
+  \small\smath{U\!N\!IV} & 
+  \small\smath{U\!N\!IV /\!/ \approx_{{\cal L}(r)}} &
+  \small\smath{U\!N\!IV /\!/ \alert{R}}
+  \end{tabular}}
   \end{center}
 
-  then
-
-  \begin{center}
-  \smath{\text{finite} (U\!N\!IV /\!/ \approx_{\mathbb{L}(r_1) \,\cup\, \mathbb{L}(r_2)})}
-  \end{center}
   
   
 
@@ -705,22 +668,40 @@
   \frametitle{\LARGE What Have We Achieved?}
 
   \begin{itemize}
-  \item \smath{\text{finite}\, (U\!N\!IV /\!/ \approx_L) \;\Leftrightarrow\; L\; \text{is regular}}
+  \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
   \begin{center}
-  \smath{U\!N\!IV /\!/ \approx_L \;\;=\;\; U\!N\!IV /\!/ \approx_{-L}}
+  \smath{U\!N\!IV /\!/ \approx_A \;\;=\;\; U\!N\!IV /\!/ \approx_{\overline{A}}}
   \end{center}\pause\bigskip
   
-  \item if you want to do regular expression matching (see Scott's paper)\pause\bigskip
+  \item non-regularity (\smath{a^nb^n})
+
+  \begin{quote}
+  \begin{minipage}{8.8cm}
+  \begin{block}{}
+  \begin{minipage}{8.6cm}
+  If there exists a sufficiently large set \smath{B} (for example infinite), 
+  such that
 
-  \item I cannot yet give definite numbers
+  \begin{center}
+  \smath{\forall x,y \in B.\; x \not= y \;\Rightarrow\; x \not\approx_{A} y}. 
+  \end{center}  
+
+  then \smath{A} is not regular.
+  \end{minipage}
+  \end{block}
+  \end{minipage}\medskip\pause
+
+  \small(\smath{A \dn \bigcup_i a^i})
+  \end{quote}
+
   \end{itemize}
 
   \only<2>{
   \begin{textblock}{10}(4,14)
   \small
-  \smath{x \approx_{L} y \,\dn\, \forall z.\; x @ z \in L \Leftrightarrow y @ z \in L}
+  \smath{x \approx_{A} y \,\dn\, \forall z.\; x @ z \in A \Leftrightarrow y @ z \in A}
   \end{textblock}
   }
 
@@ -731,30 +712,6 @@
 *}
 
 
-
-text_raw {*
-  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-  \mode<presentation>{
-  \begin{frame}[c]
-  \frametitle{\LARGE What We Have Not Achieved}
-
-  \begin{itemize}
-  \item regular expressions are not good if you look for a minimal
-  one for a language (DFAs have this notion)\pause\bigskip
-
-  \item Is there anything to be said about context free languages:\medskip
-  
-  \begin{quote}
-  A context free language is where every string can be recognised by
-  a pushdown automaton.
-  \end{quote}
-  \end{itemize}
-
-  \end{frame}}
-  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
-*}
-
-
 text_raw {*
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \mode<presentation>{
@@ -762,21 +719,48 @@
   \frametitle{\LARGE Conclusion}
 
   \begin{itemize}
-  \item on balance regular expression are superior 
-  to DFAs, in my opinion\bigskip
+  \item We have never ever seen a proof of Myhill-Nerode based on
+  regular expressions.\smallskip\pause
 
-  \item I cannot think of a reason to not teach regular languages
-  to students this way (!?)\bigskip
+  \item great source of examples (inductions)\smallskip\pause
 
-  \item I have never ever seen a proof of Myhill-Nerode based on
-  regular expressions\bigskip
+  \item no need to fight the theorem prover:\\ 
+  \begin{itemize}
+  \item first direction (790 loc)\\
+  \item second direction (400 / 390 loc)\pause
+  \end{itemize}\smallskip
 
-  \item no application, but lots of fun\bigskip
-
-  \item great source of examples
+  \item I have \alert{\bf not} yet used it for teaching of undergraduates.\pause
 
   \end{itemize}
 
+  \only<5->{
+  \begin{textblock}{13.8}(1,4)
+  \begin{block}{}\mbox{}\hspace{3mm}
+  \begin{minipage}{11cm}\raggedright
+  \large 
+
+  {\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)
+
+  \end{minipage}
+  \end{block}
+  \end{textblock}}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}[c]
+  \frametitle{\mbox{}\\[2cm]\textcolor{red}{Questions?}}
+
+
+
   \end{frame}}
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
 *}




