1 (*<*)

     2 theory Slides4

     3 imports "~~/src/HOL/Library/LaTeXsugar"

     4 begin

     5 

     6 notation (latex output)

     7   set ("_") and

     8   Cons  ("_::/_" [66,65] 65) 

     9 

    10 (*>*)

    11 

    12 

    13 text_raw {*

    14   \renewcommand{\slidecaption}{Edinburgh, 21 February 2012}

    15   \newcommand{\bl}[1]{\textcolor{blue}{#1}}                        

    16   \newcommand{\sout}[1]{\tikz[baseline=(X.base), inner sep=-0.1pt, outer sep=0pt]

    17   \node [cross out,red, ultra thick, draw] (X) {\textcolor{black}{#1}};}

    18   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    19   \mode<presentation>{

    20   \begin{frame}

    21   \frametitle{%

    22   \begin{tabular}{@ {}c@ {}}

    23   \LARGE Formalising\\[-3mm] 

    24   \LARGE Regular Language Theory\\[-3mm] 

    25   \LARGE with Regular Expressions,\\[-3mm] 

    26   \LARGE \alert<2>{Only}\\[0mm] 

    27   \end{tabular}}

    28   

    29   \begin{center}

    30    Christian Urban\\

    31   \small King's College London

    32   \end{center}\bigskip

    33  

    34   \begin{center}

    35   \small joint work with Chunhan Wu and Xingyuan Zhang from the PLA

    36   University of Science and Technology in Nanjing

    37   \end{center}

    38 

    39   \end{frame}}

    40   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    41 *}

    42 

    43 text_raw {*

    44   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    45   \mode<presentation>{

    46   \begin{frame}<1->[c]

    47   \frametitle{}

    48 

    49   \mbox{}\\[-10mm]

    50   \begin{itemize}

    51   \item My background is in 

    52   \begin{itemize}

    53   \item \normalsize theorem provers

    54   \item \normalsize develop Nominal Isabelle

    55   \end{itemize}\bigskip\bigskip  

    56 

    57   \item<1->to formalise and mechanically check proofs from 

    58   programming language research and TCS\bigskip

    59 

    60   \item<2->our biggest success story \ldots 

    61   \end{itemize}

    62   

    63   \only<1->{

    64   \begin{textblock}{6}(10.9,3.5)

    65   \includegraphics[scale=0.23]{isabelle1.png}

    66   \end{textblock}}

    67   

    68 

    69 

    70   \end{frame}}

    71   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

    72 *}

    73 

    74 

    75 

    76 

    77 text_raw {*

    78   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    79   \mode<presentation>{

    80   \begin{frame}[c]

    81   \frametitle{}

    82 

    83   \begin{tabular}{c@ {\hspace{2mm}}c}

    84   \\[6mm]

    85   \begin{tabular}{c}

    86   \includegraphics[scale=0.11]{harper.jpg}\\[-2mm]

    87   {\footnotesize Bob Harper}\\[-2.5mm]

    88   {\footnotesize (CMU)}

    89   \end{tabular}

    90   \begin{tabular}{c}

    91   \includegraphics[scale=0.37]{pfenning.jpg}\\[-2mm]

    92   {\footnotesize Frank Pfenning}\\[-2.5mm]

    93   {\footnotesize (CMU)}

    94   \end{tabular} &

    95 

    96   \begin{tabular}{p{6cm}}

    97   \raggedright

    98   \color{gray}{published a proof in\\ {\bf ACM Transactions on Computational Logic}, 2005,

    99   $\sim$31pp}

   100   \end{tabular}\\

   101 

   102   \pause

   103   \\[0mm]

   104   

   105   \begin{tabular}{c}

   106   \includegraphics[scale=0.36]{appel.jpg}\\[-2mm] 

   107   {\footnotesize Andrew Appel}\\[-2.5mm]

   108   {\footnotesize (Princeton)}

   109   \end{tabular} &

   110 

   111   \begin{tabular}{p{6cm}}

   112   \raggedright

   113   \color{gray}{relied on their proof in a\\ {\bf security} critical application}

   114   \end{tabular}

   115   \end{tabular}

   116 

   117   

   118 

   119   \end{frame}}

   120   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   121 *}

   122 

   123 

   124 

   125 text {*

   126   \tikzstyle{every node}=[node distance=25mm,text height=1.5ex, text depth=.25ex]

   127   \tikzstyle{node1}=[rectangle, minimum size=10mm, rounded corners=3mm, very thick, 

   128                      draw=black!50, top color=white, bottom color=black!20]

   129   \tikzstyle{node2}=[rectangle, minimum size=12mm, rounded corners=3mm, very thick, 

   130                      draw=red!70, top color=white, bottom color=red!50!black!20]

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

   132   \mode<presentation>{

   133   \begin{frame}<2->[squeeze]

   134   \frametitle{} 

   135   

   136   \begin{columns}

   137   

   138   \begin{column}{0.8\textwidth}

   139   \begin{textblock}{0}(1,2)

   140 

   141   \begin{tikzpicture}

   142   \matrix[ampersand replacement=\&,column sep=7mm, row sep=5mm]

   143   { \&[-10mm] 

   144     \node (def1)   [node1] {\large\hspace{1mm}Spec\hspace{1mm}\mbox{}}; \&

   145     \node (proof1) [node1] {\large Proof}; \&

   146     \node (alg1)   [node1] {\large\hspace{1mm}Alg\hspace{1mm}\mbox{}}; \\

   147     

   148     \onslide<4->{\node {\begin{tabular}{c}\small 1st\\[-2.5mm] \footnotesize solution\end{tabular}};} \&

   149     \onslide<4->{\node (def2)   [node2] {\large Spec$^\text{+ex}$};} \&

   150     \onslide<4->{\node (proof2) [node1] {\large Proof};} \&

   151     \onslide<4->{\node (alg2)   [node1] {\large\hspace{1mm}Alg\hspace{1mm}\mbox{}};} \\

   152      

   153     \onslide<5->{\node {\begin{tabular}{c}\small 2nd\\[-2.5mm] \footnotesize solution\end{tabular}};} \&

   154     \onslide<5->{\node (def3)   [node1] {\large\hspace{1mm}Spec\hspace{1mm}\mbox{}};} \&

   155     \onslide<5->{\node (proof3) [node1] {\large Proof};} \&

   156     \onslide<5->{\node (alg3)   [node2] {\large Alg$^\text{-ex}$};} \\

   157 

   158     \onslide<6->{\node {\begin{tabular}{c}\small 3rd\\[-2.5mm] \footnotesize solution\end{tabular}};} \&

   159     \onslide<6->{\node (def4)   [node1] {\large\hspace{1mm}Spec\hspace{1mm}\mbox{}};} \&

   160     \onslide<6->{\node (proof4) [node2] {\large\hspace{1mm}Proof\hspace{1mm}};} \&

   161     \onslide<6->{\node (alg4)   [node1] {\large\hspace{1mm}Alg\hspace{1mm}\mbox{}};} \\

   162   };

   163 

   164   \draw[->,black!50,line width=2mm] (proof1) -- (def1);

   165   \draw[->,black!50,line width=2mm] (proof1) -- (alg1);

   166   

   167   \onslide<4->{\draw[->,black!50,line width=2mm] (proof2) -- (def2);}

   168   \onslide<4->{\draw[->,black!50,line width=2mm] (proof2) -- (alg2);}

   169 

   170   \onslide<5->{\draw[->,black!50,line width=2mm] (proof3) -- (def3);}

   171   \onslide<5->{\draw[->,black!50,line width=2mm] (proof3) -- (alg3);}

   172   

   173   \onslide<6->{\draw[->,black!50,line width=2mm] (proof4) -- (def4);}

   174   \onslide<6->{\draw[->,black!50,line width=2mm] (proof4) -- (alg4);}

   175 

   176   \onslide<3->{\draw[white,line width=1mm] (1.1,3.2) -- (0.9,2.85) -- (1.1,2.35) -- (0.9,2.0);} 

   177   \end{tikzpicture}

   178 

   179   \end{textblock}

   180   \end{column}

   181   \end{columns}

   182 

   183 

   184   \begin{textblock}{3}(12,3.6)

   185   \onslide<4->{

   186   \begin{tikzpicture}

   187   \node at (0,0) [single arrow, shape border rotate=270, fill=red,text=white]{2h};

   188   \end{tikzpicture}}

   189   \end{textblock}

   190 

   191   \end{frame}}

   192   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   193 

   194 *}

   195 

   196 

   197 text_raw {*

   198   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   199   \mode<presentation>{

   200   \begin{frame}[c]

   201   \frametitle{}

   202 

   203   \begin{itemize}

   204   \item I also found fixable errors in my Ph.D.-thesis about cut-elimination

   205   (examined by Henk Barendregt and Andy Pitts)

   206   \item flaws in PIP (OS); a theorem without a shred of evidence (algorithms)

   207   \end{itemize}\bigskip\bigskip

   208 

   209 

   210   {\bf Conclusion:}\smallskip

   211 

   212   Pencil-and-paper proofs in TCS are not foolproof, 

   213   not even expertproof.

   214 

   215   \end{frame}}

   216   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   217 *}

   218 

   219 

   220 text_raw {*

   221   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   222   \mode<presentation>{

   223   \begin{frame}[t]

   224   \frametitle{\begin{tabular}{@ {}c@ {}}

   225   \large Nipkow about Teaching Proofs in TCS:\hspace{3cm}\mbox{}\\[-4mm]

   226   \large \textcolor{red}{``London Underground Phenomenon''}\\[-18mm]\mbox{}

   227   \end{tabular}}

   228 

   229   \begin{center}

   230   \begin{tabular}{ccc}

   231   students & \;\;\raisebox{-8mm}{\includegraphics[scale=0.16]{gap.jpg}}\;\; & proofs

   232   \end{tabular}

   233   \end{center}

   234 

   235   \small Scott Aaronson (Berkeley/MIT):\\[-7mm]\mbox{}

   236   \begin{center}

   237   \begin{block}{}

   238   \color{gray}

   239   \small

   240   ``I still remember having to grade hundreds of exams where the

   241   students started out by assuming what had to be proved, or filled

   242   page after page with gibberish in the hope that, somewhere in the

   243   mess, they might accidentally have said something

   244   correct. \ldots{}innumerable examples of ``parrot proofs'' ---

   245   NP-completeness reductions done in the wrong direction, arguments

   246   that look more like LSD trips than coherent chains of logic \ldots{}''

   247   \end{block}

   248   \end{center}

   249 

   250   \end{frame}}

   251   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   252 *}

   253 

   254 text_raw {*

   255   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   256   \mode<presentation>{

   257   \begin{frame}[c]

   258   \frametitle{}

   259 

   260   \begin{itemize}

   261   \item part of the problem is teaching the obvious\medskip

   262   \begin{center}

   263   \smath{\infer{A \vdash A}{}}

   264   \end{center}\bigskip\bigskip

   265   \item teach proofs, not logic

   266   \item students having too little practice and no good literature for how to do proofs\\

   267   \textcolor{gray}{\small(Velleman is too mathematics oriented)}

   268   \bigskip\bigskip\pause

   269 

   270   \item proof assistants lead to abundant practice because they are 

   271   addictive like video games (Nipkow, Pierce)\\

   272    \textcolor{gray}{\small(in the past they were just frustrating, but they got much better)}

   273   \end{itemize}

   274 

   275 

   276 

   277   \end{frame}}

   278   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   279 *}

   280 

   281 text_raw {*

   282   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   283   \mode<presentation>{

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

   285   \frametitle{Regular Expressions}

   286 

   287   \begin{textblock}{6}(2,4)

   288   \begin{tabular}{@ {}rrl}

   289   \bl{r} & \bl{$::=$}  & \bl{$\varnothing$}\\

   290          & \bl{$\mid$} & \bl{[]}\\

   291          & \bl{$\mid$} & \bl{c}\\

   292          & \bl{$\mid$} & \bl{r$_1$ $\cdot$ r$_2$}\\

   293          & \bl{$\mid$} & \bl{r$_1$ + r$_2$}\\

   294          & \bl{$\mid$} & \bl{r$^*$}\\

   295   \end{tabular}

   296   \end{textblock}

   297 

   298   \begin{textblock}{6}(8,3.5)

   299   \includegraphics[scale=0.35]{Screen1.png}

   300   \end{textblock}

   301 

   302   \begin{textblock}{6}(10.2,2.8)

   303   \footnotesize Isabelle:

   304   \end{textblock}

   305 

   306   \begin{textblock}{6}(7,12)

   307   \footnotesize\textcolor{gray}{students have seen them and can be motivated about them}

   308   \end{textblock}

   309   

   310   \end{frame}}

   311   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   312 *}

   313 

   314 text_raw {*

   315   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   316   \mode<presentation>{

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

   318 

   319   \mbox{}\\[-2mm]

   320 

   321   \small

   322   \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}ll@ {}}

   323   \bl{nullable (NULL)}            & \bl{$=$} & \bl{false} &\\

   324   \bl{nullable (EMPTY)}           & \bl{$=$} & \bl{true}  &\\

   325   \bl{nullable (CHAR c)}           & \bl{$=$} & \bl{false} &\\

   326   \bl{nullable (ALT r$_1$ r$_2$)} & \bl{$=$} & \bl{(nullable r$_1$) $\vee$ (nullable r$_2$)} & \\ 

   327   \bl{nullable (SEQ r$_1$ r$_2$)} & \bl{$=$} & \bl{(nullable r$_1$) $\wedge$ (nullable r$_2$)} & \\

   328   \bl{nullable (STAR r)}          & \bl{$=$} & \bl{true} & \\

   329   \end{tabular}\medskip\pause

   330 

   331   \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{-10mm}}l@ {}}

   332   \bl{der c (NULL)}            & \bl{$=$} & \bl{NULL} & \\

   333   \bl{der c (EMPTY)}           & \bl{$=$} & \bl{NULL} & \\

   334   \bl{der c (CHAR d)}           & \bl{$=$} & \bl{if c $=$ d then EMPTY else NULL} & \\

   335   \bl{der c (ALT r$_1$ r$_2$)} & \bl{$=$} & \bl{ALT (der c r$_1$) (der c r$_2$)} & \\

   336   \bl{der c (SEQ r$_1$ r$_2$)} & \bl{$=$} & \bl{ALT (SEQ (der c r$_1$) r$_2$)} & \\

   337        &          & \bl{\phantom{ALT} (if nullable r$_1$ then der c r$_2$ else NULL)}\\

   338   \bl{der c (STAR r)}          & \bl{$=$} & \bl{SEQ (der c r) (STAR r)} &\smallskip\\\pause

   339 

   340   \bl{derivative [] r}     & \bl{$=$} & \bl{r} & \\

   341   \bl{derivative (c::s) r} & \bl{$=$} & \bl{derivative s (der c r)} & \\

   342   \end{tabular}\medskip

   343 

   344   \bl{matches r s $=$ nullable (derivative s r)}

   345   

   346   \end{frame}}

   347   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   348 *}

   349 

   350 

   351 text_raw {*

   352   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   353   \mode<presentation>{

   354   \begin{frame}[t]

   355   \frametitle{\normalsize Formal language theory\ldots\hfill\mbox{}}

   356   \mbox{}\\[-15mm]\mbox{}

   357 

   358   \begin{center}

   359   \huge\bf\textcolor{gray}{in Theorem Provers}\\

   360   \footnotesize\textcolor{gray}{e.g.~Isabelle, Coq, HOL4, \ldots}

   361   \end{center}

   362 

   363   \begin{itemize}

   364   \item automata @{text "\<Rightarrow>"} graphs, matrices, functions

   365   \item<2-> combining automata / graphs

   366 

   367   \onslide<2->{

   368   \begin{center}

   369   \begin{tabular}{ccc}

   370   \begin{tikzpicture}[scale=1]

   371   %\draw[step=2mm] (-1,-1) grid (1,1);

   372   

   373   \draw[rounded corners=1mm, very thick] (-1.0,-0.3) rectangle (-0.2,0.3);

   374   \draw[rounded corners=1mm, very thick] ( 0.2,-0.3) rectangle ( 1.0,0.3);

   375 

   376   \node (A) at (-1.0,0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};

   377   \node (B) at ( 0.2,0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};

   378   

   379   \node (C) at (-0.2, 0.13) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};

   380   \node (D) at (-0.2,-0.13) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};

   381 

   382   \node (E) at (1.0, 0.2) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};

   383   \node (F) at (1.0,-0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};

   384   \node (G) at (1.0,-0.2) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};

   385 

   386   \draw (-0.6,0.0) node {\small$A_1$};

   387   \draw ( 0.6,0.0) node {\small$A_2$};

   388   \end{tikzpicture}}

   389 

   390   & 

   391 

   392   \onslide<3->{\raisebox{1.1mm}{\bf\Large$\;\Rightarrow\,$}}

   393 

   394   &

   395 

   396   \onslide<3->{\begin{tikzpicture}[scale=1]

   397   %\draw[step=2mm] (-1,-1) grid (1,1);

   398   

   399   \draw[rounded corners=1mm, very thick] (-1.0,-0.3) rectangle (-0.2,0.3);

   400   \draw[rounded corners=1mm, very thick] ( 0.2,-0.3) rectangle ( 1.0,0.3);

   401 

   402   \node (A) at (-1.0,0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};

   403   \node (B) at ( 0.2,0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};

   404   

   405   \node (C) at (-0.2, 0.13) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};

   406   \node (D) at (-0.2,-0.13) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};

   407 

   408   \node (E) at (1.0, 0.2) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};

   409   \node (F) at (1.0,-0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};

   410   \node (G) at (1.0,-0.2) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};

   411   

   412   \draw [very thick, red] (C) to [bend left=45] (B);

   413   \draw [very thick, red] (D) to [bend right=45] (B);

   414 

   415   \draw (-0.6,0.0) node {\small$A_1$};

   416   \draw ( 0.6,0.0) node {\small$A_2$};

   417   \end{tikzpicture}}

   418 

   419   \end{tabular}

   420   \end{center}\medskip

   421 

   422   \only<4-5>{

   423   \begin{tabular}{@ {\hspace{-5mm}}l@ {}}

   424   disjoint union:\\[2mm]

   425   \smath{A_1\uplus A_2 \dn \{(1, x)\,|\, x \in A_1\} \,\cup\, \{(2, y)\,|\, y \in A_2\}}

   426   \end{tabular}}

   427   \end{itemize}

   428 

   429   \only<5>{

   430   \begin{textblock}{13.9}(0.7,7.7)

   431   \begin{block}{}

   432   \medskip

   433   \begin{minipage}{14cm}\raggedright

   434   Problems with definition for regularity:\bigskip\\

   435   \smath{\;\text{is\_regular}(A) \dn \exists M.\;\text{is\_dfa}(M) \wedge {\cal L} (M) = A}\bigskip

   436   \end{minipage}

   437   \end{block}

   438   \end{textblock}}

   439   \medskip

   440 

   441   \only<6->{\underline{A solution}:\;\;use \smath{\text{nat}}s \;@{text "\<Rightarrow>"}\; state nodes\medskip}

   442 

   443   \only<7->{You have to \alert{rename} states!}

   444 

   445   \end{frame}}

   446   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   447 *}

   448 

   449 text_raw {*

   450   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   451   \mode<presentation>{

   452   \begin{frame}[t]

   453   \frametitle{\normalsize Formal language theory\ldots\hfill\mbox{}}

   454   \mbox{}\\[-15mm]\mbox{}

   455 

   456   \begin{center}

   457   \huge\bf\textcolor{gray}{in Theorem Provers}\\

   458   \footnotesize\textcolor{gray}{e.g.~Isabelle, Coq, HOL4, \ldots}

   459   \end{center}

   460 

   461   \begin{itemize}

   462   \item Kozen's paper proof of Myhill-Nerode:\\ 

   463   requires absence of \alert{inaccessible states}

   464   \item complementation of automata only works for \alert{complete} automata

   465   (need sink states)\medskip

   466   \end{itemize}\bigskip\bigskip

   467 

   468   \begin{center}

   469   \smath{\;\text{is\_regular}(A) \dn \exists M.\;\text{is\_dfa}(M) \wedge {\cal L} (M) = A}

   470   \end{center}

   471 

   472 

   473   \end{frame}}

   474   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   475 *}

   476 

   477 text_raw {*

   478   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   479   \mode<presentation>{

   480   \begin{frame}[t]

   481   \frametitle{}

   482   \mbox{}\\[25mm]\mbox{}

   483 

   484   \begin{textblock}{13.9}(0.7,1.2)

   485   \begin{block}{}

   486   \begin{minipage}{13.4cm}\raggedright

   487   {\bf Definition:}\smallskip\\

   488   

   489   A language \smath{A} is \alert{regular}, provided there exists a\\ 

   490   \alert{regular expression} that matches all strings of \smath{A}.

   491   \end{minipage}

   492   \end{block}

   493   \end{textblock}\pause

   494   

   495   {\noindent\large\bf\alert{\ldots{}and forget about automata}}\bigskip\bigskip\pause

   496 

   497   Infrastructure for free. But do we lose anything?\medskip\pause

   498 

   499   \begin{minipage}{1.1\textwidth}

   500   \begin{itemize}

   501   \item pumping lemma\pause

   502   \item closure under complementation\pause

   503   \item \only<6>{regular expression matching}%

   504        \only<7->{\sout{regular expression matching}

   505   {\footnotesize(@{text "\<Rightarrow>"}Brozowski'64, Owens et al '09)}}

   506   \item<8-> most textbooks are about automata

   507   \end{itemize}

   508   \end{minipage}

   509 

   510   

   511   \end{frame}}

   512   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   513 

   514 *}

   515 

   516 

   517 text_raw {*

   518   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   519   \mode<presentation>{

   520   \begin{frame}[c]

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

   522 

   523   \begin{itemize}

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

   525   being regular\\ \textcolor{gray}{(pumping lemma only necessary)}\bigskip

   526 

   527   \item key is the equivalence relation:\medskip

   528   \begin{center}

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

   530   \end{center}

   531   \end{itemize}

   532 

   533  

   534   \end{frame}}

   535   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   536 

   537 *}

   538 

   539 text_raw {*

   540   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   541   \mode<presentation>{

   542   \begin{frame}[c]

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

   544 

   545   \begin{center}

   546   \only<1>{%

   547   \begin{tikzpicture}[scale=3]

   548   \draw[very thick] (0.5,0.5) circle (.6cm);

   549   \end{tikzpicture}}%

   550   \only<2->{%

   551   \begin{tikzpicture}[scale=3]

   552   \draw[very thick] (0.5,0.5) circle (.6cm);

   553   \clip[draw] (0.5,0.5) circle (.6cm);

   554   \draw[step=2mm, very thick] (-1.4,-1.4) grid (1.4,1.4);

   555   \end{tikzpicture}}

   556   \end{center}

   557   

   558   \begin{itemize}

   559   \item \smath{\text{finite}\, (U\!N\!IV /\!/ \approx_A) \;\Leftrightarrow\; A\; \text{is regular}}

   560   \end{itemize}

   561 

   562   \begin{textblock}{5}(2.1,5.3)

   563   \begin{tikzpicture}

   564   \node at (0,0) [single arrow, fill=red,text=white, minimum height=2cm]

   565   {$U\!N\!IV$};

   566   \draw (-0.3,-1.1) node {\begin{tabular}{l}set of all\\[-1mm] strings\end{tabular}};

   567   \end{tikzpicture}

   568   \end{textblock}

   569 

   570   \only<2->{%

   571   \begin{textblock}{5}(9.1,7.2)

   572   \begin{tikzpicture}

   573   \node at (0,0) [shape border rotate=180,single arrow, fill=red,text=white, minimum height=2cm]

   574   {@{text "\<lbrakk>s\<rbrakk>"}$_{\approx_{A}}$};

   575   \draw (0.9,-1.1) node {\begin{tabular}{l}an equivalence class\end{tabular}};

   576   \end{tikzpicture}

   577   \end{textblock}}

   578 

   579   \only<3->{

   580   \begin{textblock}{11.9}(1.7,3)

   581   \begin{block}{}

   582   \begin{minipage}{11.4cm}\raggedright

   583   Two directions:\medskip\\

   584   \begin{tabular}{@ {}ll}

   585   1.)\;finite $\Rightarrow$ regular\\

   586   \;\;\;\smath{\text{finite}\,(U\!N\!IV /\!/ \approx_A) \Rightarrow \exists r.\;A = {\cal L}(r)}\\[3mm]

   587   2.)\;regular $\Rightarrow$ finite\\

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

   589   \end{tabular}

   590 

   591   \end{minipage}

   592   \end{block}

   593   \end{textblock}}

   594 

   595   \end{frame}}

   596   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   597 

   598 *}

   599 

   600 

   601 text_raw {*

   602   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   603   \mode<presentation>{

   604   \begin{frame}[c]

   605   \frametitle{\LARGE Initial and Final {\sout{\textcolor{gray}{States}}}}

   606 

   607   \begin{textblock}{8}(10, 2)

   608   \textcolor{black}{Equivalence Classes}

   609   \end{textblock}

   610 

   611 

   612   \begin{center}

   613   \begin{tikzpicture}[scale=3]

   614   \draw[very thick] (0.5,0.5) circle (.6cm);

   615   \clip[draw] (0.5,0.5) circle (.6cm);

   616   \draw[step=2mm, very thick] (-1.4,-1.4) grid (1.4,1.4);

   617   \only<2->{\draw[blue, fill] (0.0, 0.6) rectangle (0.2, 0.8);}

   618   \only<3->{\draw[red, fill] (0.2, 0.2) rectangle (0.4, 0.4);

   619   \draw[red, fill] (0.4, 0.8) rectangle (0.6, 1.0);

   620   \draw[red, fill] (0.6, 0.0) rectangle (0.8, 0.2);

   621   \draw[red, fill] (0.8, 0.4) rectangle (1.0, 0.6);}

   622   \end{tikzpicture}

   623   \end{center}

   624 

   625   \begin{itemize}

   626   \item \smath{\text{finals}\,A\,\dn \{[\!|s|\!]_{\approx_{A}}\;|\;s \in A\}}

   627   \smallskip

   628   \item we can prove: \smath{A = \bigcup \text{finals}\,A}

   629   \end{itemize}

   630 

   631   \only<2->{%

   632   \begin{textblock}{5}(2.1,4.6)

   633   \begin{tikzpicture}

   634   \node at (0,0) [single arrow, fill=blue,text=white, minimum height=2cm]

   635   {$[] \in X$};

   636   \end{tikzpicture}

   637   \end{textblock}}

   638 

   639   \only<3->{%

   640   \begin{textblock}{5}(10,7.4)

   641   \begin{tikzpicture}

   642   \node at (0,0) [shape border rotate=180,single arrow, fill=red,text=white, minimum height=2cm]

   643   {a final};

   644   \end{tikzpicture}

   645   \end{textblock}}

   646 

   647   \end{frame}}

   648   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   649 *}

   650 

   651 

   652 text_raw {*

   653   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   654   \mode<presentation>{

   655   \begin{frame}<-1>[c]

   656   \frametitle{\begin{tabular}{@ {}l}\LARGE% 

   657   Transitions between Eq-Classes\end{tabular}}

   658 

   659   \begin{center}

   660   \begin{tikzpicture}[scale=3]

   661   \draw[very thick] (0.5,0.5) circle (.6cm);

   662   \clip[draw] (0.5,0.5) circle (.6cm);

   663   \draw[step=2mm, very thick] (-1.4,-1.4) grid (1.4,1.4);

   664   \draw[blue, fill] (0.0, 0.6) rectangle (0.2, 0.8);

   665   \draw[blue, fill] (0.8, 0.4) rectangle (1.0, 0.6);

   666   \draw[white] (0.1,0.7) node (X) {$X$};

   667   \draw[white] (0.9,0.5) node (Y) {$Y$};

   668   \draw[blue, ->, line width = 2mm, bend left=45] (X) -- (Y);

   669   \node [inner sep=1pt,label=above:\textcolor{blue}{$c$}] at ($ (X)!.5!(Y) $) {};

   670   \end{tikzpicture}

   671   \end{center}

   672 

   673   \begin{center}

   674   \smath{X \stackrel{c}{\longrightarrow} Y \;\dn\; X ; c \subseteq Y}

   675   \end{center}

   676 

   677   \onslide<8>{

   678   \begin{tabular}{c}

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

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

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

   682   \end{tikzpicture}

   683   \end{tabular}}

   684 

   685   \end{frame}}

   686   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   687 *}

   688 

   689 

   690 text_raw {*

   691   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   692   \mode<presentation>{

   693   \begin{frame}[c]

   694   \frametitle{\LARGE Systems of Equations}

   695 

   696   Inspired by a method of Brzozowski\;'64:\bigskip\bigskip

   697 

   698   \begin{center}

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

   700   \\[-13mm]

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

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

   703 

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

   705 

   706   \node[state,initial]   (p_0)                  {$X_1$};

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

   708 

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

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

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

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

   713   \end{tikzpicture}\\

   714   \\[-13mm]

   715   \end{tabular}

   716   \end{center}

   717 

   718   \begin{center}

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

   720   & \smath{X_1} & \smath{=} & \smath{X_1;b + X_2;b \onslide<2->{\alert<2>{+ \lambda;[]}}}\\

   721   & \smath{X_2} & \smath{=} & \smath{X_1;a + X_2;a}\medskip\\

   722   \end{tabular}

   723   \end{center}

   724 

   725   \end{frame}}

   726   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   727 *}

   728 

   729 text_raw {*

   730   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   731   \mode<presentation>{

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

   733   \small

   734 

   735   \begin{center}

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

   737   \onslide<1->{\smath{X_1}} & \onslide<1->{\smath{=}} 

   738       & \onslide<1->{\smath{X_1; b + X_2; b + \lambda;[]}}\\

   739   \onslide<1->{\smath{X_2}} & \onslide<1->{\smath{=}}    

   740       & \onslide<1->{\smath{X_1; a + X_2; a}}\\

   741 

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

   743 

   744   \onslide<2->{\smath{X_1}} & \onslide<2->{\smath{=}} 

   745       & \onslide<2->{\smath{X_1; b + X_2; b + \lambda;[]}}\\

   746   \onslide<2->{\smath{X_2}} & \onslide<2->{\smath{=}}    

   747       & \only<2->{\smath{X_1; a\cdot a^\star}}\\

   748 

   749   & & & \onslide<4->{by Arden}\\

   750 

   751   \onslide<4->{\smath{X_1}} & \onslide<4->{\smath{=}} 

   752       & \onslide<4->{\smath{X_2; b \cdot b^\star+ \lambda;b^\star}}\\

   753   \onslide<4->{\smath{X_2}} & \onslide<4->{\smath{=}}    

   754       & \onslide<4->{\smath{X_1; a\cdot a^\star}}\\

   755 

   756   & & & \onslide<5->{by substitution}\\

   757 

   758   \onslide<5->{\smath{X_1}} & \onslide<5->{\smath{=}} 

   759       & \onslide<5->{\smath{X_1; a\cdot a^\star \cdot b \cdot b^\star+ \lambda;b^\star}}\\

   760   \onslide<5->{\smath{X_2}} & \onslide<5->{\smath{=}}    

   761       & \onslide<5->{\smath{X_1; a\cdot a^\star}}\\

   762 

   763   & & & \onslide<6->{by Arden}\\

   764 

   765   \onslide<6->{\smath{X_1}} & \onslide<6->{\smath{=}} 

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

   767   \onslide<6->{\smath{X_2}} & \onslide<6->{\smath{=}}    

   768       & \onslide<6->{\smath{X_1; a\cdot a^\star}}\\

   769 

   770   & & & \onslide<7->{by substitution}\\

   771 

   772   \onslide<7->{\smath{X_1}} & \onslide<7->{\smath{=}} 

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

   774   \onslide<7->{\smath{X_2}} & \onslide<7->{\smath{=}}    

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

   776           \cdot a\cdot a^\star}}\\

   777   \end{tabular}

   778   \end{center}

   779 

   780   \only<8->{

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

   782   \begin{block}{}

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

   784   

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

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

   787 

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

   789 

   790   \node[state,initial]   (p_0)                  {$X_1$};

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

   792 

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

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

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

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

   797   \end{tikzpicture}

   798 

   799   \end{minipage}

   800   \end{block}

   801   \end{textblock}}

   802 

   803   \only<1,2>{%

   804   \begin{textblock}{3}(0.6,1.2)

   805   \begin{tikzpicture}

   806   \node at (0,0) [single arrow, fill=red,text=white, minimum height=0cm]

   807   {\textcolor{red}{a}};

   808   \end{tikzpicture}

   809   \end{textblock}}

   810   \only<2>{%

   811   \begin{textblock}{3}(0.6,3.6)

   812   \begin{tikzpicture}

   813   \node at (0,0) [single arrow, fill=red,text=white, minimum height=0cm]

   814   {\textcolor{red}{a}};

   815   \end{tikzpicture}

   816   \end{textblock}}

   817   \only<4>{%

   818   \begin{textblock}{3}(0.6,2.9)

   819   \begin{tikzpicture}

   820   \node at (0,0) [single arrow, fill=red,text=white, minimum height=0cm]

   821   {\textcolor{red}{a}};

   822   \end{tikzpicture}

   823   \end{textblock}}

   824   \only<4>{%

   825   \begin{textblock}{3}(0.6,5.3)

   826   \begin{tikzpicture}

   827   \node at (0,0) [single arrow, fill=red,text=white, minimum height=0cm]

   828   {\textcolor{red}{a}};

   829   \end{tikzpicture}

   830   \end{textblock}}

   831   \only<5>{%

   832   \begin{textblock}{3}(1.0,5.6)

   833   \begin{tikzpicture}

   834   \node at (0,0) (A) {};

   835   \node at (0,1) (B) {};

   836   \draw[<-, line width=2mm, red] (B) to  (A);

   837   \end{tikzpicture}

   838   \end{textblock}}

   839   \only<5,6>{%

   840   \begin{textblock}{3}(0.6,7.7)

   841   \begin{tikzpicture}

   842   \node at (0,0) [single arrow, fill=red,text=white, minimum height=0cm]

   843   {\textcolor{red}{a}};

   844   \end{tikzpicture}

   845   \end{textblock}}

   846   \only<6>{%

   847   \begin{textblock}{3}(0.6,10.1)

   848   \begin{tikzpicture}

   849   \node at (0,0) [single arrow, fill=red,text=white, minimum height=0cm]

   850   {\textcolor{red}{a}};

   851   \end{tikzpicture}

   852   \end{textblock}}

   853   \only<7>{%

   854   \begin{textblock}{3}(1.0,10.3)

   855   \begin{tikzpicture}

   856   \node at (0,0) (A) {};

   857   \node at (0,1) (B) {};

   858   \draw[->, line width=2mm, red] (B) to  (A);

   859   \end{tikzpicture}

   860   \end{textblock}}

   861 

   862   \end{frame}}

   863   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   864 *}

   865 

   866 

   867 text_raw {*

   868   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   869   \mode<presentation>{

   870   \begin{frame}[c]

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

   872 

   873   {\bf Arden's Lemma:}\smallskip 

   874 

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

   876   \begin{center}

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

   878   \end{center}

   879   has the (unique) solution

   880   \begin{center}

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

   882   \end{center}

   883 

   884 

   885   \end{frame}}

   886   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   887 *}

   888 

   889 

   890 text_raw {*

   891   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   892   \mode<presentation>{

   893   \begin{frame}<1-2,4->[t]

   894   \small

   895 

   896   \begin{center}

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

   898   \onslide<1->{\smath{X_1}} & \onslide<1->{\smath{=}} 

   899       & \onslide<1->{\smath{X_1; b + X_2; b + \lambda;[]}}\\

   900   \onslide<1->{\smath{X_2}} & \onslide<1->{\smath{=}}    

   901       & \onslide<1->{\smath{X_1; a + X_2; a}}\\

   902 

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

   904 

   905   \onslide<2->{\smath{X_1}} & \onslide<2->{\smath{=}} 

   906       & \onslide<2->{\smath{X_1; b + X_2; b + \lambda;[]}}\\

   907   \onslide<2->{\smath{X_2}} & \onslide<2->{\smath{=}}    

   908       & \only<2->{\smath{X_1; a\cdot a^\star}}\\

   909 

   910   & & & \onslide<4->{by Arden}\\

   911 

   912   \onslide<4->{\smath{X_1}} & \onslide<4->{\smath{=}} 

   913       & \onslide<4->{\smath{X_2; b \cdot b^\star+ \lambda;b^\star}}\\

   914   \onslide<4->{\smath{X_2}} & \onslide<4->{\smath{=}}    

   915       & \onslide<4->{\smath{X_1; a\cdot a^\star}}\\

   916 

   917   & & & \onslide<5->{by substitution}\\

   918 

   919   \onslide<5->{\smath{X_1}} & \onslide<5->{\smath{=}} 

   920       & \onslide<5->{\smath{X_1; a\cdot a^\star \cdot b \cdot b^\star+ \lambda;b^\star}}\\

   921   \onslide<5->{\smath{X_2}} & \onslide<5->{\smath{=}}    

   922       & \onslide<5->{\smath{X_1; a\cdot a^\star}}\\

   923 

   924   & & & \onslide<6->{by Arden}\\

   925 

   926   \onslide<6->{\smath{X_1}} & \onslide<6->{\smath{=}} 

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

   928   \onslide<6->{\smath{X_2}} & \onslide<6->{\smath{=}}    

   929       & \onslide<6->{\smath{X_1; a\cdot a^\star}}\\

   930 

   931   & & & \onslide<7->{by substitution}\\

   932 

   933   \onslide<7->{\smath{X_1}} & \onslide<7->{\smath{=}} 

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

   935   \onslide<7->{\smath{X_2}} & \onslide<7->{\smath{=}}    

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

   937           \cdot a\cdot a^\star}}\\

   938   \end{tabular}

   939   \end{center}

   940 

   941   \only<8->{

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

   943   \begin{block}{}

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

   945   

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

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

   948 

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

   950 

   951   \node[state,initial]   (p_0)                  {$X_1$};

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

   953 

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

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

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

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

   958   \end{tikzpicture}

   959 

   960   \end{minipage}

   961   \end{block}

   962   \end{textblock}}

   963 

   964   \only<1,2>{%

   965   \begin{textblock}{3}(0.6,1.2)

   966   \begin{tikzpicture}

   967   \node at (0,0) [single arrow, fill=red,text=white, minimum height=0cm]

   968   {\textcolor{red}{a}};

   969   \end{tikzpicture}

   970   \end{textblock}}

   971   \only<2>{%

   972   \begin{textblock}{3}(0.6,3.6)

   973   \begin{tikzpicture}

   974   \node at (0,0) [single arrow, fill=red,text=white, minimum height=0cm]

   975   {\textcolor{red}{a}};

   976   \end{tikzpicture}

   977   \end{textblock}}

   978   \only<4>{%

   979   \begin{textblock}{3}(0.6,2.9)

   980   \begin{tikzpicture}

   981   \node at (0,0) [single arrow, fill=red,text=white, minimum height=0cm]

   982   {\textcolor{red}{a}};

   983   \end{tikzpicture}

   984   \end{textblock}}

   985   \only<4>{%

   986   \begin{textblock}{3}(0.6,5.3)

   987   \begin{tikzpicture}

   988   \node at (0,0) [single arrow, fill=red,text=white, minimum height=0cm]

   989   {\textcolor{red}{a}};

   990   \end{tikzpicture}

   991   \end{textblock}}

   992   \only<5>{%

   993   \begin{textblock}{3}(1.0,5.6)

   994   \begin{tikzpicture}

   995   \node at (0,0) (A) {};

   996   \node at (0,1) (B) {};

   997   \draw[<-, line width=2mm, red] (B) to  (A);

   998   \end{tikzpicture}

   999   \end{textblock}}

  1000   \only<5,6>{%

  1001   \begin{textblock}{3}(0.6,7.7)

  1002   \begin{tikzpicture}

  1003   \node at (0,0) [single arrow, fill=red,text=white, minimum height=0cm]

  1004   {\textcolor{red}{a}};

  1005   \end{tikzpicture}

  1006   \end{textblock}}

  1007   \only<6>{%

  1008   \begin{textblock}{3}(0.6,10.1)

  1009   \begin{tikzpicture}

  1010   \node at (0,0) [single arrow, fill=red,text=white, minimum height=0cm]

  1011   {\textcolor{red}{a}};

  1012   \end{tikzpicture}

  1013   \end{textblock}}

  1014   \only<7>{%

  1015   \begin{textblock}{3}(1.0,10.3)

  1016   \begin{tikzpicture}

  1017   \node at (0,0) (A) {};

  1018   \node at (0,1) (B) {};

  1019   \draw[->, line width=2mm, red] (B) to  (A);

  1020   \end{tikzpicture}

  1021   \end{textblock}}

  1022 

  1023   \end{frame}}

  1024   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

  1025 *}

  1026 

  1027 

  1028 text_raw {*

  1029   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1030   \mode<presentation>{

  1031   \begin{frame}[c]

  1032   \frametitle{\LARGE The Other Direction}

  1033 

  1034   One has to prove

  1035 

  1036   \begin{center}

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

  1038   \end{center}

  1039 

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

  1041   of thinking, one can find a \alert{refined} relation:\bigskip

  1042 

  1043   

  1044   \begin{center}

  1045   \mbox{\begin{tabular}{c@ {\hspace{7mm}}c@ {\hspace{7mm}}c}

  1046   \begin{tikzpicture}[scale=1.1]

  1047   %Circle

  1048   \draw[thick] (0,0) circle (1.1);    

  1049   \end{tikzpicture}

  1050   &

  1051   \begin{tikzpicture}[scale=1.1]

  1052   %Circle

  1053   \draw[thick] (0,0) circle (1.1);    

  1054   %Main rays

  1055   \foreach \a in {0, 90,...,359}

  1056     \draw[very thick] (0, 0) -- (\a:1.1);

  1057   \foreach \a / \l in {45/1, 135/2, 225/3, 315/4}

  1058       \draw (\a: 0.65) node {\small$a_\l$};

  1059   \end{tikzpicture}

  1060   &

  1061   \begin{tikzpicture}[scale=1.1]

  1062   %Circle

  1063   \draw[red, thick] (0,0) circle (1.1);    

  1064   %Main rays

  1065   \foreach \a in {0, 45,...,359}

  1066      \draw[red, very thick] (0, 0) -- (\a:1.1);

  1067   \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}

  1068       \draw (\a: 0.77) node {\textcolor{red}{\footnotesize$a_{\l}$}};

  1069   \end{tikzpicture}\\

  1070   \small\smath{U\!N\!IV} & 

  1071   \small\smath{U\!N\!IV /\!/ \approx_{{\cal L}(r)}} &

  1072   \small\smath{U\!N\!IV /\!/ \alert{R}}

  1073   \end{tabular}}

  1074   \end{center}

  1075 

  1076   \begin{textblock}{5}(9.8,2.6)

  1077   \begin{tikzpicture}

  1078   \node at (0,0) [shape border rotate=270,single arrow, fill=red,text=white, minimum height=0cm]{\textcolor{red}{a}};

  1079   \end{tikzpicture}

  1080   \end{textblock}

  1081   

  1082 

  1083   \end{frame}}

  1084   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

  1085 *}

  1086 

  1087 text_raw {*

  1088   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1089   \mode<presentation>{

  1090   \begin{frame}[t]

  1091   \frametitle{\LARGE\begin{tabular}{c}Derivatives of RExps\end{tabular}}

  1092 

  1093   \begin{itemize}

  1094   \item introduced by Brozowski~'64

  1095   \item produces a regular expression after a character has been parsed\\[-18mm]\mbox{}

  1096   \end{itemize}

  1097 

  1098   \only<1->{%

  1099   \textcolor{blue}{%

  1100   \begin{center}

  1101   \begin{tabular}{@ {}lc@ {\hspace{3mm}}l@ {}}

  1102   der c $\varnothing$     & $\dn$ & $\varnothing$\\

  1103   der c []                & $\dn$ & $\varnothing$\\

  1104   der c d                 & $\dn$ & if c $=$ d then [] else $\varnothing$\\

  1105   der c ($r_1 + r_2$)     & $\dn$ & (der c $r_1$) $+$ (der c $r_2$)\\

  1106   der c ($r^\star$)       & $\dn$ & (der c $r$) $\cdot$ $r^\star$\\

  1107   der c ($r_1 \cdot r_2$) & $\dn$ & if nullable $r_1$\\

  1108                           &       & then (der c $r_1$) $\cdot$ $r_2$ $+$ (der c $r_2$)\\

  1109                           &       & else (der c $r_1$) $\cdot$ $r_2$\\

  1110   \end{tabular}

  1111   \end{center}}}

  1112 

  1113   \only<2>{

  1114   \begin{textblock}{13}(1.5,5.7)

  1115   \begin{block}{}

  1116   \begin{quote}

  1117   \begin{minipage}{13cm}\raggedright

  1118   derivatives refine \smath{x \approx_{{\cal{L}}(r)} y}\bigskip

  1119   \begin{center}

  1120   \smath{\text{der}~x~r = \text{der}~y~r \Longrightarrow x \approx_{L(r)} y}

  1121   \end{center}\bigskip

  1122   \

  1123   \smath{\text{finite}(\text{ders}~A~r)}, but only modulo ACI

  1124 

  1125   \begin{center}

  1126   \begin{tabular}{@ {\hspace{-10mm}}rcl}

  1127   \smath{(r_1 + r_2) + r_3} & \smath{\equiv} & \smath{r_1 + (r_2 + r_3)}\\

  1128   \smath{r_1 + r_2} &         \smath{\equiv} & \smath{r_2 + r_1}\\

  1129   \smath{r + r} &             \smath{\equiv} & \smath{r}\\

  1130   \end{tabular}

  1131   \end{center}

  1132   \end{minipage}

  1133   \end{quote}

  1134   \end{block}

  1135   \end{textblock}}