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