--- a/Slides/Slides1.thy Thu Nov 18 11:39:17 2010 +0000
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,699 +0,0 @@
-(*<*)
-theory Slides1
-imports "LaTeXsugar"
-begin
-
-notation (latex output)
- set ("_") and
- Cons ("_::/_" [66,65] 65)
-
-(*>*)
-
-
-text_raw {*
- \renewcommand{\slidecaption}{Cambridge, 9 November 2010}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}
- \frametitle{%
- \begin{tabular}{@ {}c@ {}}
- \LARGE A Formalisation of the\\[-3mm]
- \LARGE Myhill-Nerode Theorem\\[-3mm]
- \LARGE based on Regular Expressions\\[-3mm]
- \large \onslide<2>{\alert{or, Regular Languages Done Right}}\\
- \end{tabular}}
-
- \begin{center}
- Christian Urban
- \end{center}
-
-
- \begin{center}
- joint work with Chunhan Wu and Xingyuan Zhang from the PLA
- University of Science and Technology in Nanjing
- \end{center}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-*}
-
-text_raw {*
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{In Textbooks\ldots}
-
- \begin{itemize}
- \item A \alert{regular language} is one where there is DFA that
- recognises it.\pause
- \item Pumping lemma, closure properties of regular languages (closed
- under ``negation'') etc are all described and proved in terms of DFAs.\pause
-
- \item Similarly the Myhill-Nerode theorem, which gives necessary and sufficient
- conditions for a language being regular (also describes a minimal DFA for a language).
-
- \end{itemize}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-*}
-
-
-text_raw {*
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[t]
- \frametitle{Really Bad News!}
-
- This is bad news for formalisations in theorem provers. DFAs might
- be represented as
-
- \begin{itemize}
- \item graphs
- \item matrices
- \item partial functions
- \end{itemize}
-
- All constructions are difficult to reason about.\bigskip\bigskip
- \pause
-
- \small
- \only<2>{
- Constable et al needed (on and off) 18 months for a 3-person team
- to formalise automata theory in Nuprl including Myhill-Nerode. There is
- only very little other formalised work on regular languages I know of
- in Coq, Isabelle and HOL.}
- \only<3>{typical textbook reasoning goes like: ``\ldots if \smath{M} and \smath{N} are any two
- automata with no inaccessible states \ldots''
- }
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-*}
-
-text_raw {*
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[t]
- \frametitle{Regular Expressions}
-
- \ldots are a simple datatype:
-
- \only<1>{
- \begin{center}\color{blue}
- \begin{tabular}{rcl}
- rexp & $::=$ & NULL\\
- & $\mid$ & EMPTY\\
- & $\mid$ & CHR c\\
- & $\mid$ & ALT rexp rexp\\
- & $\mid$ & SEQ rexp rexp\\
- & $\mid$ & STAR rexp
- \end{tabular}
- \end{center}}
- \only<2->{
- \begin{center}
- \begin{tabular}{rcl}
- \smath{r} & \smath{::=} & \smath{0} \\
- & \smath{\mid} & \smath{[]}\\
- & \smath{\mid} & \smath{c}\\
- & \smath{\mid} & \smath{r_1 + r_2}\\
- & \smath{\mid} & \smath{r_1 \cdot r_2}\\
- & \smath{\mid} & \smath{r^\star}
- \end{tabular}
- \end{center}}
-
- \only<3->{Induction and recursion principles come for free.}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-*}
-
-
-text_raw {*
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{Semantics of Rexps}
-
- \begin{center}
- \begin{tabular}{rcl}
- \smath{\mathbb{L}(0)} & \smath{=} & \smath{\varnothing}\\
- \smath{\mathbb{L}([])} & \smath{=} & \smath{\{[]\}}\\
- \smath{\mathbb{L}(c)} & \smath{=} & \smath{\{[c]\}}\\
- \smath{\mathbb{L}(r_1 + r_2)} & \smath{=} & \smath{\mathbb{L}(r_1) \cup \mathbb{L}(r_2)}\\
- \smath{\mathbb{L}(r_1 \cdot r_2)} & \smath{=} & \smath{\mathbb{L}(r_1)\; ;\; \mathbb{L} (r_2)}\\
- \smath{\mathbb{L}(r^\star)} & \smath{=} & \smath{\mathbb{L}(r)^\star}
- \end{tabular}
- \end{center}
-
- \small
- \begin{center}
- \begin{tabular}{rcl}
- \smath{L_1 ; L_2} & \smath{\dn} & \smath{\{ s_1 @ s_2 \mid s_1 \in L_1 \wedge s_2 \in L_2\}}\bigskip\\
- \multicolumn{3}{c}{
- \smath{\infer{[] \in L^\star}{}} \hspace{10mm}
- \smath{\infer{s_1 @ s_2 \in L^\star}{s_1 \in L & s_2 \in L^\star}}
- }
- \end{tabular}
- \end{center}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-*}
-
-text_raw {*
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{\LARGE Regular Expression Matching}
-
- \begin{itemize}
- \item Harper in JFP'99: ``Functional Pearl: Proof- Directed Debugging''\medskip
- \item Yi in JFP'06: ``Educational Pearl: `Proof-Directed Debugging' revisited
- for a first-order version''\medskip
- \item Owens et al in JFP'09: ``Regular-expression derivatives re-examined''\bigskip\pause
-
- \begin{quote}\small
- ``Unfortunately, regular expression derivatives have been lost in the
- sands of time, and few computer scientists are aware of them.''
- \end{quote}
- \end{itemize}
-
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-*}
-
-text_raw {*
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
-
- \begin{center}
- \huge\bf Demo
- \end{center}
-
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-*}
-
-text_raw {*
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{\LARGE The Myhill-Nerode Theorem}
-
- \begin{itemize}
- \item will help with closure properties of regular languages and
- with the pumping lemma.\medskip
-
- \item provides necessary and suf\!ficient conditions for a language being
- regular\bigskip\pause
-
- \begin{center}
- \smath{x \approx_{L} y \,\dn\, \forall z.\; x @ z \in L \Leftrightarrow y @ z \in L}
- \end{center}
- \end{itemize}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-*}
-
-text_raw {*
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{\LARGE The Myhill-Nerode Theorem}
-
- \mbox{}\\[5cm]
-
- \begin{itemize}
- \item \smath{\text{finite}\, (U\!N\!IV /\!/ \approx_L) \;\Leftrightarrow\; L\; \text{is regular}}
- \end{itemize}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-*}
-
-
-text_raw {*
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{\LARGE Equivalence Classes}
-
- \begin{itemize}
- \item \smath{L = []}
- \begin{center}
- \smath{\Big\{\{[]\},\; U\!N\!IV - \{[]\}\Big\}}
- \end{center}\bigskip\bigskip
-
- \item \smath{L = [c]}
- \begin{center}
- \smath{\Big\{\{[]\},\; \{[c]\},\; U\!N\!IV - \{[], [c]\}\Big\}}
- \end{center}\bigskip\bigskip
-
- \item \smath{L = \varnothing}
- \begin{center}
- \smath{\Big\{U\!N\!IV\Big\}}
- \end{center}
-
- \end{itemize}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-*}
-
-
-text_raw {*
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{\LARGE Regular Languages}
-
- \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{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{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-*}
-
-
-text_raw {*
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{\LARGE Final States}
-
- \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}
- \smallskip
- \item we can prove: \smath{L = \bigcup \{X.\;\text{final}_L\,X\}}
-
- \end{itemize}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-*}
-
-
-text_raw {*
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{\LARGE Transitions between\\[-3mm] Equivalence Classes}
-
- \smath{L = \{[c]\}}
-
- \begin{tabular}{@ {\hspace{-7mm}}cc}
- \begin{tabular}{c}
- \begin{tikzpicture}[shorten >=1pt,node distance=2cm,auto, ultra thick]
- \tikzstyle{state}=[circle,thick,draw=blue!75,fill=blue!20,minimum size=0mm]
-
- %\draw[help lines] (0,0) grid (3,2);
-
- \node[state,initial] (q_0) {$R_1$};
- \node[state,accepting] (q_1) [above right of=q_0] {$R_2$};
- \node[state] (q_2) [below right of=q_0] {$R_3$};
-
- \path[->] (q_0) edge node {c} (q_1)
- edge node [swap] {$\Sigma-{c}$} (q_2)
- (q_2) edge [loop below] node {$\Sigma$} ();
- \end{tikzpicture}
- \end{tabular}
- &
- \begin{tabular}[t]{ll}
- \\[-20mm]
- \multicolumn{2}{l}{\smath{U\!N\!IV /\!/\approx_L} produces}\\[4mm]
-
- \smath{R_1}: & \smath{\{[]\}}\\
- \smath{R_2}: & \smath{\{[c]\}}\\
- \smath{R_3}: & \smath{U\!N\!IV - \{[], [c]\}}\\[6mm]
- \multicolumn{2}{l}{\onslide<2->{\smath{X \stackrel{c}{\longrightarrow} Y \dn X ; [c] \subseteq Y}}}
- \end{tabular}
-
- \end{tabular}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-*}
-
-
-text_raw {*
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{\LARGE Systems of Equations}
-
- Inspired by a method of Brzozowski\;'64, we can build an equational system
- characterising the equivalence classes:
-
- \begin{center}
- \begin{tabular}{@ {\hspace{-20mm}}c}
- \\[-13mm]
- \begin{tikzpicture}[shorten >=1pt,node distance=2cm,auto, ultra thick]
- \tikzstyle{state}=[circle,thick,draw=blue!75,fill=blue!20,minimum size=0mm]
-
- %\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$};
-
- \path[->] (p_0) edge [bend left] node {a} (p_1)
- edge [loop above] node {b} ()
- (p_1) edge [loop above] node {a} ()
- edge [bend left] node {b} (p_0);
- \end{tikzpicture}\\
- \\[-13mm]
- \end{tabular}
- \end{center}
-
- \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\\
- \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}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-*}
-
-text_raw {*
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}<1>[t]
- \small
-
- \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<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 + R_2; a}}%
- \only<3->{\smath{R_1; a\cdot a^\star}}\\
-
- & & & \onslide<3->{by Arden}\\
-
- \onslide<3->{\smath{R_1}} & \onslide<3->{\smath{=}}
- & \onslide<3->{\smath{R_2; b \cdot b^\star+ \lambda;b^\star}}\\
- \onslide<3->{\smath{R_2}} & \onslide<3->{\smath{=}}
- & \onslide<3->{\smath{R_1; a\cdot a^\star}}\\
-
- & & & \onslide<4->{by substitution}\\
-
- \onslide<4->{\smath{R_1}} & \onslide<4->{\smath{=}}
- & \onslide<4->{\smath{R_1; a\cdot a^\star \cdot 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<5->{by Arden}\\
-
- \onslide<5->{\smath{R_1}} & \onslide<5->{\smath{=}}
- & \onslide<5->{\smath{\lambda;b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star}}\\
- \onslide<5->{\smath{R_2}} & \onslide<5->{\smath{=}}
- & \onslide<5->{\smath{R_1; a\cdot a^\star}}\\
-
- & & & \onslide<6->{by substitution}\\
-
- \onslide<6->{\smath{R_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{\lambda; b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star
- \cdot a\cdot a^\star}}\\
- \end{tabular}
- \end{center}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-*}
-
-text_raw {*
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{\LARGE A Variant of Arden's Lemma}
-
- {\bf Arden's Lemma:}
-
- If \smath{[] \not\in A} then
- \begin{center}
- \smath{X = X; A + \text{something}}
- \end{center}
- has the (unique) solution
- \begin{center}
- \smath{X = \text{something} ; A^\star}
- \end{center}
-
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-*}
-
-
-text_raw {*
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}<1->[t]
- \small
-
- \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<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 + R_2; a}}%
- \only<3->{\smath{R_1; a\cdot a^\star}}\\
-
- & & & \onslide<3->{by Arden}\\
-
- \onslide<3->{\smath{R_1}} & \onslide<3->{\smath{=}}
- & \onslide<3->{\smath{R_2; b \cdot b^\star+ \lambda;b^\star}}\\
- \onslide<3->{\smath{R_2}} & \onslide<3->{\smath{=}}
- & \onslide<3->{\smath{R_1; a\cdot a^\star}}\\
-
- & & & \onslide<4->{by substitution}\\
-
- \onslide<4->{\smath{R_1}} & \onslide<4->{\smath{=}}
- & \onslide<4->{\smath{R_1; a\cdot a^\star \cdot 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<5->{by Arden}\\
-
- \onslide<5->{\smath{R_1}} & \onslide<5->{\smath{=}}
- & \onslide<5->{\smath{\lambda;b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star}}\\
- \onslide<5->{\smath{R_2}} & \onslide<5->{\smath{=}}
- & \onslide<5->{\smath{R_1; a\cdot a^\star}}\\
-
- & & & \onslide<6->{by substitution}\\
-
- \onslide<6->{\smath{R_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{\lambda; b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star
- \cdot a\cdot a^\star}}\\
-
- & & & \onslide<7->{\alert{solved form}}\\
- \end{tabular}
- \end{center}
-
- \only<8->{
- \begin{textblock}{6}(2.5,4)
- \begin{block}{}
- \begin{minipage}{8cm}\raggedright
-
- \begin{tikzpicture}[shorten >=1pt,node distance=2cm,auto, ultra thick, inner sep=1mm]
- \tikzstyle{state}=[circle,thick,draw=blue!75,fill=blue!20,minimum size=0mm]
-
- %\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$};
-
- \path[->] (p_0) edge [bend left] node {a} (p_1)
- edge [loop above] node {b} ()
- (p_1) edge [loop above] node {a} ()
- edge [bend left] node {b} (p_0);
- \end{tikzpicture}
-
- \end{minipage}
- \end{block}
- \end{textblock}}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-*}
-
-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 This is still a bit hairy to formalise because of our set-representation
- for equations:
-
- \begin{center}
- \begin{tabular}{ll}
- \smath{\big\{ (X, \{(Y_1, r_1), (Y_2, r_2), \ldots\}),}\\
- \mbox{}\hspace{5mm}\smath{\ldots}\\
- & \smath{\big\}}
- \end{tabular}
- \end{center}\pause
-
- \small
- They are generated from \smath{U\!N\!IV /\!/ \approx_L}
-
- \end{itemize}
-
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-*}
-
-text_raw {*
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{\LARGE Other Direction}
-
- One has to prove
-
- \begin{center}
- \smath{\text{finite} (U\!N\!IV /\!/ \approx_{\mathbb{L}(r)})}
- \end{center}
-
- by induction on \smath{r}. Not trivial, but after a bit
- of thinking (by Chunhan), one can prove that if
-
- \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)})}
- \end{center}
-
- then
-
- \begin{center}
- \smath{\text{finite} (U\!N\!IV /\!/ \approx_{\mathbb{L}(r_1) \,\cup\, \mathbb{L}(r_2)})}
- \end{center}
-
-
-
- \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_L) \;\Leftrightarrow\; L\; \text{is regular}}
- \bigskip\pause
- \item regular languages are closed under `inversion'
- \begin{center}
- \smath{U\!N\!IV /\!/ \approx_L \;\;=\;\; U\!N\!IV /\!/ \approx_{-L}}
- \end{center}\pause\bigskip
-
- \item regular expressions are not good if you look for a minimal
- one of a language (DFA have this notion)\pause\bigskip
-
- \item if you want to do regular expression matching (see Scott's paper)
- \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}
- \end{textblock}
- }
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-*}
-
-text_raw {*
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{\LARGE Conclusion}
-
- \begin{itemize}
- \item on balance regular expression are superior to DFAs\bigskip
-
- \item I cannot think of a reason to not teach regular languages
- to students this way\bigskip
-
- \item I have never ever seen a proof of Myhill-Nerode based on
- regular expressions\bigskip
-
- \item no application, but a lot of fun\bigskip
-
- \item great source of examples
-
- \end{itemize}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-*}
-
-(*<*)
-end
-(*>*)
\ No newline at end of file