20   \Large A Formalisation of the\\[-5mm] 

    20   \LARGE A Formalisation of the\\[-3mm] 

    21   \Large Myhill-Nerode Theorem\\[-5mm] 

    21   \LARGE Myhill-Nerode Theorem\\[-3mm] 

    22   \Large based on Regular Expressions\\[-3mm] 

    22   \LARGE based on Regular Expressions\\[-3mm] 

    23   \large \onslide<2>{or, Regular Languages Done Right}\\

    23   \large \onslide<2>{\alert{or, Regular Languages Done Right}}\\

    52   under ``negation'') etc are all described and proved in terms of DFAs\pause

    51   under ``negation'') etc are all described and proved in terms of DFAs.\pause

    53 

    52 

    54   \item similarly the Myhill-Nerode theorem, which gives necessary and sufficient

    53   \item Similarly the Myhill-Nerode theorem, which gives necessary and sufficient

    55   conditions for a language being regular (also describes a minimal DFA for a language)

    54   conditions for a language being regular (also describes a minimal DFA for a language).

    56 

    55 

    57   \end{itemize}

    56   \end{itemize}

    58 

    57 

    59   \end{frame}}

    58   \end{frame}}

    60   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

    59   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

    61 

    60 

    62 *}

    61 *}

    63 

    62 

    64 

    63 

    65 text_raw {*

    64 text_raw {*

    66   \renewcommand{\slidecaption}{Cambridge, 9 November 2010}

    65   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    67   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    66   \mode<presentation>{

    68   \mode<presentation>{

    67   \begin{frame}[t]

    69   \begin{frame}[c]

    88   in Coq, Isabelle and HOL.

    87   in Coq, Isabelle and HOL.}

    89 

    88   \only<3>{typical textbook reasoning goes like: ``\ldots if \smath{M} and \smath{N} are any two

    90 

    89   automata with no inaccessible states \ldots''

    91   

    90   }

    92   \end{frame}}

    91   

    93   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

    92   \end{frame}}

    94 

    93   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

    95 *}

    94 

    96 

    95 *}

    97 text_raw {*

    96 

    98   \renewcommand{\slidecaption}{Cambridge, 9 November 2010}

    97 text_raw {*

    99   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    98   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   100   \mode<presentation>{

    99   \mode<presentation>{

   101   \begin{frame}[c]

   100   \begin{frame}[t]

   104   \ldots are a simple datatype defined as:

   103   \ldots are a simple datatype:

   120   \smath{r} & \smath{::=}  & \smath{\varepsilon} \\

   119   \smath{r} & \smath{::=}  & \smath{0} \\

   124             & \smath{\mid} & \smath{r_1 ; r_2}\\

   123             & \smath{\mid} & \smath{r_1 \cdot r_2}\\

   129   \end{frame}}

   128   \only<3->{Induction and recursion principles come for free.}

   130   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   129 

   131 

   130   \end{frame}}

   132 *}

   131   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   133 

   132 

   133 *}

   134 

   135 

   136 text_raw {*

   137   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   138   \mode<presentation>{

   139   \begin{frame}[c]

   140   \frametitle{Semantics of Rexps}

   141 

   142   \begin{center}

   143   \begin{tabular}{rcl}

   144   \smath{\mathbb{L}(0)}             & \smath{=} & \smath{\varnothing}\\

   145   \smath{\mathbb{L}([])}            & \smath{=} & \smath{\{[]\}}\\

   146   \smath{\mathbb{L}(c)}             & \smath{=} & \smath{\{[c]\}}\\

   147   \smath{\mathbb{L}(r_1 + r_2)}     & \smath{=} & \smath{\mathbb{L}(r_1) \cup \mathbb{L}(r_2)}\\

   148   \smath{\mathbb{L}(r_1 \cdot r_2)} & \smath{=} & \smath{\mathbb{L}(r_1)\; ;\; \mathbb{L} (r_2)}\\

   149   \smath{\mathbb{L}(r^\star)}       & \smath{=} & \smath{\mathbb{L}(r)^\star}

   150   \end{tabular}

   151   \end{center}

   152 

   153   \small

   154   \begin{center}

   155   \begin{tabular}{rcl}

   156   \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\\

   157   \multicolumn{3}{c}{

   158   \smath{\infer{[] \in L^\star}{}} \hspace{10mm}

   159   \smath{\infer{s_1 @ s_2 \in L^\star}{s_1 \in L & s_2 \in L^\star}}

   160   }

   161   \end{tabular}

   162   \end{center}

   163 

   164   \end{frame}}

   165   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   166 

   167 *}

   168 

   169 text_raw {*

   170   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   171   \mode<presentation>{

   172   \begin{frame}[c]

   173   \frametitle{\LARGE Regular Expression Matching}

   174 

   175   \begin{itemize}

   176   \item Harper in JFP'99: ``Functional Pearl: Proof- Directed Debugging''\medskip

   177   \item Yi in JFP'06: ``Educational Pearl: `Proof-Directed Debugging' revisited 

   178   for a first-order version''\medskip

   179   \item Owens et al in JFP'09: ``Regular-expression derivatives re-examined''\bigskip\pause

   180 

   181   \begin{quote}\small

   182   ``Unfortunately, regular expression derivatives have been lost in the 

   183   sands of time, and few computer scientists are aware of them.''

   184   \end{quote}

   185   \end{itemize}

   186   

   187 

   188   \end{frame}}

   189   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   190 

   191 *}

   192 

   193 text_raw {*

   194   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   195   \mode<presentation>{

   196   \begin{frame}[c]

   197 

   198   \begin{center}

   199   \huge\bf Demo

   200   \end{center}

   201   

   202 

   203   \end{frame}}

   204   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   205 

   206 *}

   207 

   208 text_raw {*

   209   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   210   \mode<presentation>{

   211   \begin{frame}[c]

   212   \frametitle{\LARGE The Myhill-Nerode Theorem}

   213 

   214   \begin{itemize}

   215   \item will help with closure properties of regular languages and

   216   with the pumping lemma.\medskip

   217   

   218   \item provides necessary and suf\!ficient conditions for a language being 

   219   regular\bigskip\pause

   220 

   221   \begin{center}

   222   \smath{x \approx_{L} y \,\dn\, \forall z.\; x @ z \in L \Leftrightarrow y @ z \in L}

   223   \end{center}

   224   \end{itemize}

   225 

   226   \end{frame}}

   227   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   228 

   229 *}

   230 

   231 text_raw {*

   232   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   233   \mode<presentation>{

   234   \begin{frame}[c]

   235   \frametitle{\LARGE The Myhill-Nerode Theorem}

   236 

   237   \mbox{}\\[5cm]

   238 

   239   \begin{itemize}

   240   \item \smath{\text{finite}\, (U\!N\!IV /\!/ \approx_L) \;\Leftrightarrow\; L\; \text{is regular}}

   241   \end{itemize}

   242 

   243   \end{frame}}

   244   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   245 

   246 *}

   247 

   248 

   249 text_raw {*

   250   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   251   \mode<presentation>{

   252   \begin{frame}[c]

   253   \frametitle{\LARGE Equivalence Classes}

   254 

   255   \begin{itemize}

   256   \item \smath{L = []}

   257   \begin{center}

   258   \smath{\Big\{\{[]\},\; U\!N\!IV - \{[]\}\Big\}}

   259   \end{center}\bigskip\bigskip

   260 

   261   \item \smath{L = [c]}

   262   \begin{center}

   263   \smath{\Big\{\{[]\},\; \{[c]\},\; U\!N\!IV - \{[], [c]\}\Big\}}

   264   \end{center}\bigskip\bigskip

   265 

   266   \item \smath{L = \varnothing}

   267   \begin{center}

   268   \smath{\Big\{U\!N\!IV\Big\}}

   269   \end{center}

   270 

   271   \end{itemize}

   272 

   273   \end{frame}}

   274   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   275 

   276 *}

   277 

   278 

   279 text_raw {*

   280   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   281   \mode<presentation>{

   282   \begin{frame}[c]

   283   \frametitle{\LARGE Regular Languages}

   284 

   285   \begin{itemize}

   286   \item \smath{L} is regular \smath{\dn} if there is an automaton \smath{M} 

   287   such that \smath{\mathbb{L}(M) = L}\\[1.5cm]

   288 

   289   \item Myhill-Nerode:

   290 

   291   \begin{center}

   292   \begin{tabular}{l}

   293   finite $\Rightarrow$ regular\\

   294   \;\;\;\smath{\text{finite}\,(U\!N\!IV /\!/ \approx_L) \Rightarrow \exists r. L = \mathbb{L}(r)}\\[3mm]

   295   regular $\Rightarrow$ finite\\

   296   \;\;\;\smath{\text{finite}\, (U\!N\!IV /\!/ \approx_{\mathbb{L}(r)})}

   297   \end{tabular}

   298   \end{center}

   299 

   300   \end{itemize}

   301 

   302   \end{frame}}

   303   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   304 

   305 *}

   306 

   307 

   308 text_raw {*

   309   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   310   \mode<presentation>{

   311   \begin{frame}[c]

   312   \frametitle{\LARGE Final States}

   313 

   314   \mbox{}\\[3cm]

   315 

   316   \begin{itemize}

   317   \item \smath{\text{final}_L\,X \dn}\\

   318   \smath{\hspace{6mm}X \in (U\!N\!IV /\!/\approx_L) \;\wedge\; \forall s \in X.\; s \in L}

   319   \smallskip

   320   \item we can prove: \smath{L = \bigcup \{X.\;\text{final}_L\,X\}}

   321 

   322   \end{itemize}

   323 

   324   \end{frame}}

   325   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   326 *}

   327 

   328 

   329 text_raw {*

   330   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   331   \mode<presentation>{

   332   \begin{frame}[c]

   333   \frametitle{\LARGE Transitions between\\[-3mm] Equivalence Classes}

   334 

   335   \smath{L = \{[c]\}}

   336 

   337   \begin{tabular}{@ {\hspace{-7mm}}cc}

   338   \begin{tabular}{c}

   339   \begin{tikzpicture}[shorten >=1pt,node distance=2cm,auto, ultra thick]

   340   \tikzstyle{state}=[circle,thick,draw=blue!75,fill=blue!20,minimum size=0mm]

   341 

   342   %\draw[help lines] (0,0) grid (3,2);

   343 

   344   \node[state,initial]   (q_0)                        {$R_1$};

   345   \node[state,accepting] (q_1) [above right of=q_0]   {$R_2$};

   346   \node[state]           (q_2) [below right of=q_0]   {$R_3$};

   347 

   348   \path[->] (q_0) edge                node        {c} (q_1)

   349                   edge                node [swap] {$\Sigma-{c}$} (q_2)

   350             (q_2) edge [loop below]   node        {$\Sigma$} ();

   351   \end{tikzpicture}

   352   \end{tabular}

   353   &

   354   \begin{tabular}[t]{ll}

   355   \\[-20mm]

   356   \multicolumn{2}{l}{\smath{U\!N\!IV /\!/\approx_L} produces}\\[4mm]

   357 

   358   \smath{R_1}: & \smath{\{[]\}}\\

   359   \smath{R_2}: & \smath{\{[c]\}}\\

   360   \smath{R_3}: & \smath{U\!N\!IV - \{[], [c]\}}\\[6mm]

   361   \multicolumn{2}{l}{\onslide<2->{\smath{X \stackrel{c}{\longrightarrow} Y \dn X ; [c] \subseteq Y}}}

   362   \end{tabular}

   363 

   364   \end{tabular}

   365 

   366   \end{frame}}

   367   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   368 *}

   369 

   370 

   371 text_raw {*

   372   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   373   \mode<presentation>{

   374   \begin{frame}[c]

   375   \frametitle{\LARGE Systems of Equations}

   376 

   377   Inspired by a method of Brzozowski\;'64, we can build an equational system

   378   characterising the equivalence classes:

   379 

   380   \begin{center}

   381   \begin{tabular}{@ {\hspace{-20mm}}c}

   382   \\[-13mm]

   383   \begin{tikzpicture}[shorten >=1pt,node distance=2cm,auto, ultra thick]

   384   \tikzstyle{state}=[circle,thick,draw=blue!75,fill=blue!20,minimum size=0mm]

   385 

   386   %\draw[help lines] (0,0) grid (3,2);

   387 

   388   \node[state,initial]   (p_0)                  {$R_1$};

   389   \node[state,accepting] (p_1) [right of=q_0]   {$R_2$};

   390 

   391   \path[->] (p_0) edge [bend left]   node        {a} (p_1)

   392                   edge [loop above]   node       {b} ()

   393             (p_1) edge [loop above]   node       {a} ()

   394                   edge [bend left]   node        {b} (p_0);

   395   \end{tikzpicture}\\

   396   \\[-13mm]

   397   \end{tabular}

   398   \end{center}

   399 

   400   \begin{center}

   401   \begin{tabular}{@ {\hspace{-6mm}}ll@ {\hspace{1mm}}c@ {\hspace{1mm}}l}

   402   & \smath{R_1} & \smath{\equiv} & \smath{R_1;b + R_2;b \onslide<2->{\alert<2>{+ \lambda;[]}}}\\

   403   & \smath{R_2} & \smath{\equiv} & \smath{R_1;a + R_2;a}\medskip\\

   404   \onslide<3->{we can prove} 

   405   & \onslide<3->{\smath{R_1}} & \onslide<3->{\smath{=}} 

   406       & \onslide<3->{\smath{R_1; \mathbb{L}(b) \,\cup\, R_2;\mathbb{L}(b) \,\cup\, \{[]\};\{[]\}}}\\

   407   & \onslide<3->{\smath{R_2}} & \onslide<3->{\smath{=}}    

   408       & \onslide<3->{\smath{R_1; \mathbb{L}(a) \,\cup\, R_2;\mathbb{L}(a)}}\\

   409   \end{tabular}

   410   \end{center}

   411 

   412   \end{frame}}

   413   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   414 *}

   415 

   416 text_raw {*

   417   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   418   \mode<presentation>{

   419   \begin{frame}<1>[t]

   420   \small

   421 

   422   \begin{center}

   423   \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}ll}

   424   \onslide<1->{\smath{R_1}} & \onslide<1->{\smath{=}} 

   425       & \onslide<1->{\smath{R_1; b + R_2; b + \lambda;[]}}\\

   426   \onslide<1->{\smath{R_2}} & \onslide<1->{\smath{=}}    

   427       & \onslide<1->{\smath{R_1; a + R_2; a}}\\

   428 

   429   & & & \onslide<2->{by Arden}\\

   430 

   431   \onslide<2->{\smath{R_1}} & \onslide<2->{\smath{=}} 

   432       & \onslide<2->{\smath{R_1; b + R_2; b + \lambda;[]}}\\

   433   \onslide<2->{\smath{R_2}} & \onslide<2->{\smath{=}}    

   434       & \only<2>{\smath{R_1; a + R_2; a}}%

   435         \only<3->{\smath{R_1; a\cdot a^\star}}\\

   436 

   437   & & & \onslide<3->{by Arden}\\

   438 

   439   \onslide<3->{\smath{R_1}} & \onslide<3->{\smath{=}} 

   440       & \onslide<3->{\smath{R_2; b \cdot b^\star+ \lambda;b^\star}}\\

   441   \onslide<3->{\smath{R_2}} & \onslide<3->{\smath{=}}    

   442       & \onslide<3->{\smath{R_1; a\cdot a^\star}}\\

   443 

   444   & & & \onslide<4->{by substitution}\\

   445 

   446   \onslide<4->{\smath{R_1}} & \onslide<4->{\smath{=}} 

   447       & \onslide<4->{\smath{R_1; a\cdot a^\star \cdot b \cdot b^\star+ \lambda;b^\star}}\\

   448   \onslide<4->{\smath{R_2}} & \onslide<4->{\smath{=}}    

   449       & \onslide<4->{\smath{R_1; a\cdot a^\star}}\\

   450 

   451   & & & \onslide<5->{by Arden}\\

   452 

   453   \onslide<5->{\smath{R_1}} & \onslide<5->{\smath{=}} 

   454       & \onslide<5->{\smath{\lambda;b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star}}\\

   455   \onslide<5->{\smath{R_2}} & \onslide<5->{\smath{=}}    

   456       & \onslide<5->{\smath{R_1; a\cdot a^\star}}\\

   457 

   458   & & & \onslide<6->{by substitution}\\

   459 

   460   \onslide<6->{\smath{R_1}} & \onslide<6->{\smath{=}} 

   461       & \onslide<6->{\smath{\lambda;b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star}}\\

   462   \onslide<6->{\smath{R_2}} & \onslide<6->{\smath{=}}    

   463       & \onslide<6->{\smath{\lambda; b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star 

   464           \cdot a\cdot a^\star}}\\

   465   \end{tabular}

   466   \end{center}

   467 

   468   \end{frame}}

   469   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   470 *}

   471 

   472 text_raw {*

   473   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   474   \mode<presentation>{

   475   \begin{frame}[c]

   476   \frametitle{\LARGE A Variant of Arden's Lemma}

   477 

   478   {\bf Arden's Lemma:} 

   479 

   480   If \smath{[] \not\in A} then

   481   \begin{center}

   482   \smath{X = X; A + \text{something}}

   483   \end{center}

   484   has the (unique) solution

   485   \begin{center}

   486   \smath{X = \text{something} ; A^\star}

   487   \end{center}

   488 

   489 

   490   \end{frame}}

   491   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   492 *}

   493 

   494 

   495 text_raw {*

   496   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   497   \mode<presentation>{

   498   \begin{frame}<1->[t]

   499   \small

   500 

   501   \begin{center}

   502   \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}ll}

   503   \onslide<1->{\smath{R_1}} & \onslide<1->{\smath{=}} 

   504       & \onslide<1->{\smath{R_1; b + R_2; b + \lambda;[]}}\\

   505   \onslide<1->{\smath{R_2}} & \onslide<1->{\smath{=}}    

   506       & \onslide<1->{\smath{R_1; a + R_2; a}}\\

   507 

   508   & & & \onslide<2->{by Arden}\\

   509 

   510   \onslide<2->{\smath{R_1}} & \onslide<2->{\smath{=}} 

   511       & \onslide<2->{\smath{R_1; b + R_2; b + \lambda;[]}}\\

   512   \onslide<2->{\smath{R_2}} & \onslide<2->{\smath{=}}    

   513       & \only<2>{\smath{R_1; a + R_2; a}}%

   514         \only<3->{\smath{R_1; a\cdot a^\star}}\\

   515 

   516   & & & \onslide<3->{by Arden}\\

   517 

   518   \onslide<3->{\smath{R_1}} & \onslide<3->{\smath{=}} 

   519       & \onslide<3->{\smath{R_2; b \cdot b^\star+ \lambda;b^\star}}\\

   520   \onslide<3->{\smath{R_2}} & \onslide<3->{\smath{=}}    

   521       & \onslide<3->{\smath{R_1; a\cdot a^\star}}\\

   522 

   523   & & & \onslide<4->{by substitution}\\

   524 

   525   \onslide<4->{\smath{R_1}} & \onslide<4->{\smath{=}} 

   526       & \onslide<4->{\smath{R_1; a\cdot a^\star \cdot b \cdot b^\star+ \lambda;b^\star}}\\

   527   \onslide<4->{\smath{R_2}} & \onslide<4->{\smath{=}}    

   528       & \onslide<4->{\smath{R_1; a\cdot a^\star}}\\

   529 

   530   & & & \onslide<5->{by Arden}\\

   531 

   532   \onslide<5->{\smath{R_1}} & \onslide<5->{\smath{=}} 

   533       & \onslide<5->{\smath{\lambda;b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star}}\\

   534   \onslide<5->{\smath{R_2}} & \onslide<5->{\smath{=}}    

   535       & \onslide<5->{\smath{R_1; a\cdot a^\star}}\\

   536 

   537   & & & \onslide<6->{by substitution}\\

   538 

   539   \onslide<6->{\smath{R_1}} & \onslide<6->{\smath{=}} 

   540       & \onslide<6->{\smath{\lambda;b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star}}\\

   541   \onslide<6->{\smath{R_2}} & \onslide<6->{\smath{=}}    

   542       & \onslide<6->{\smath{\lambda; b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star 

   543           \cdot a\cdot a^\star}}\\

   544 

   545   & & & \onslide<7->{\alert{solved form}}\\

   546   \end{tabular}

   547   \end{center}

   548 

   549   \only<8->{

   550   \begin{textblock}{6}(2.5,4)

   551   \begin{block}{}

   552   \begin{minipage}{8cm}\raggedright

   553   

   554   \begin{tikzpicture}[shorten >=1pt,node distance=2cm,auto, ultra thick, inner sep=1mm]

   555   \tikzstyle{state}=[circle,thick,draw=blue!75,fill=blue!20,minimum size=0mm]

   556 

   557   %\draw[help lines] (0,0) grid (3,2);

   558 

   559   \node[state,initial]   (p_0)                  {$R_1$};

   560   \node[state,accepting] (p_1) [right of=q_0]   {$R_2$};

   561 

   562   \path[->] (p_0) edge [bend left]   node        {a} (p_1)

   563                   edge [loop above]   node       {b} ()

   564             (p_1) edge [loop above]   node       {a} ()

   565                   edge [bend left]   node        {b} (p_0);

   566   \end{tikzpicture}

   567 

   568   \end{minipage}

   569   \end{block}

   570   \end{textblock}}

   571 

   572   \end{frame}}

   573   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   574 *}

   575 

   576 text_raw {*

   577   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   578   \mode<presentation>{

   579   \begin{frame}[c]

   580   \frametitle{\LARGE The Equ's Solving Algorithm}

   581 

   582   \begin{itemize}

   583   \item The algorithm must terminate: Arden makes one equation smaller; 

   584   substitution deletes one variable from the right-hand sides.\bigskip

   585 

   586   \item This is still a bit hairy to formalise because of our set-representation

   587   for equations:

   588   

   589   \begin{center}

   590   \begin{tabular}{ll}

   591   \smath{\big\{ (X, \{(Y_1, r_1), (Y_2, r_2), \ldots\}),}\\

   592   \mbox{}\hspace{5mm}\smath{\ldots}\\

   593   & \smath{\big\}}

   594   \end{tabular}

   595   \end{center}\pause

   596 

   597   \small

   598   They are generated from \smath{U\!N\!IV /\!/ \approx_L}

   599 

   600   \end{itemize}

   601 

   602 

   603   \end{frame}}

   604   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   605 *}

   606 

   607 text_raw {*

   608   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   609   \mode<presentation>{

   610   \begin{frame}[c]

   611   \frametitle{\LARGE Other Direction}

   612 

   613   One has to prove

   614 

   615   \begin{center}

   616   \smath{\text{finite} (U\!N\!IV /\!/ \approx_{\mathbb{L}(r)})}

   617   \end{center}

   618 

   619   by induction on \smath{r}. Not trivial, but after a bit 

   620   of thinking (by Chunhan), one can prove that if

   621 

   622   \begin{center}

   623   \smath{\text{finite} (U\!N\!IV /\!/ \approx_{\mathbb{L}(r_1)})}\hspace{5mm}

   624   \smath{\text{finite} (U\!N\!IV /\!/ \approx_{\mathbb{L}(r_2)})}

   625   \end{center}

   626 

   627   then

   628 

   629   \begin{center}

   630   \smath{\text{finite} (U\!N\!IV /\!/ \approx_{\mathbb{L}(r_1) \,\cup\, \mathbb{L}(r_2)})}

   631   \end{center}

   632   

   633   

   634 

   635   \end{frame}}

   636   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   637 *}

   638 

   639 text_raw {*

   640   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   641   \mode<presentation>{

   642   \begin{frame}[c]

   643   \frametitle{\LARGE What Have We Achieved?}

   644 

   645   \begin{itemize}

   646   \item \smath{\text{finite}\, (U\!N\!IV /\!/ \approx_L) \;\Leftrightarrow\; L\; \text{is regular}}

   647   \bigskip\pause

   648   \item regular languages are closed under `inversion'

   649   \begin{center}

   650   \smath{U\!N\!IV /\!/ \approx_L \;\;=\;\; U\!N\!IV /\!/ \approx_{-L}}

   651   \end{center}\pause\bigskip

   652   

   653   \item regular expressions are not good if you look for a minimal

   654   one of a language (DFA have this notion)\pause\bigskip

   655 

   656   \item if you want to do regular expression matching (see Scott's paper) 

   657   \end{itemize}

   658 

   659 

   660 

   661   \only<2>{

   662   \begin{textblock}{10}(4,14)

   663   \small

   664   \smath{x \approx_{L} y \,\dn\, \forall z.\; x @ z \in L \Leftrightarrow y @ z \in L}

   665   \end{textblock}

   666   }

   667 

   668   \end{frame}}

   669   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   670 *}

   671 

   672 text_raw {*

   673   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   674   \mode<presentation>{

   675   \begin{frame}[c]

   676   \frametitle{\LARGE Conclusion}

   677 

   678   \begin{itemize}

   679   \item on balance regular expression are superior to DFAs\bigskip

   680 

   681   \item I cannot think of a reason to not teach regular languages

   682   to students this way\bigskip

   683 

   684   \item I have never ever seen a proof of Myhill-Nerode based on

   685   regular expressions\bigskip

   686 

   687   \item no application, but a lot of fun\bigskip

   688 

   689   \item great source of examples

   690 

   691   \end{itemize}

   692 

   693   \end{frame}}

   694   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   695 *}