1 (*<*)

     2 theory Slides2

     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}{Cambridge, 9 November 2010}

    15   %\renewcommand{\slidecaption}{Nijmegen, 25 August 2011}

    16   \renewcommand{\slidecaption}{St Andrews, 19 November 2011}

    17   \newcommand{\bl}[1]{#1}                        

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

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

    20   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    21   \mode<presentation>{

    22   \begin{frame}

    23   \frametitle{%

    24   \begin{tabular}{@ {}c@ {}}

    25   \LARGE Formalising\\[-3mm] 

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

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

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

    29   \end{tabular}}

    30   

    31   \begin{center}

    32    Christian Urban\\

    33   \small King's College London

    34   \end{center}\bigskip

    35  

    36   \begin{center}

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

    38   University of Science and Technology in Nanjing

    39   \end{center}

    40 

    41   \end{frame}}

    42   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    43 *}

    44 

    45 text_raw {*

    46   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    47   \mode<presentation>{

    48   \begin{frame}[c]

    49   \frametitle{}

    50 

    51   \includegraphics[scale=0.5]{roy.jpg}\medskip

    52 

    53   Roy intertwined with my scientific life on many occasions, most 

    54   notably:\bigskip 

    55 

    56   \begin{itemize}

    57   \item he admitted me for M.Phil.~in St Andrews and\\ 

    58   made me like theory\smallskip

    59   \item sent me to Cambridge for Ph.D.\bigskip

    60   \item made me appreciate precision in proofs

    61   \end{itemize}

    62 

    63   \end{frame}}

    64   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

    65 *}

    66 

    67 text_raw {*

    68   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    69   \mode<presentation>{

    70   \begin{frame}[c]

    71   \frametitle{}

    72 

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

    74   \\[6mm]

    75   \begin{tabular}{c}

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

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

    78   {\footnotesize (CMU)}

    79   \end{tabular}

    80   \begin{tabular}{c}

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

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

    83   {\footnotesize (CMU)}

    84   \end{tabular} &

    85 

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

    87   \raggedright

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

    89   $\sim$31pp}

    90   \end{tabular}\\

    91 

    92   \pause

    93   \\[0mm]

    94   

    95   \begin{tabular}{c}

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

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

    98   {\footnotesize (Princeton)}

    99   \end{tabular} &

   100 

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

   102   \raggedright

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

   104   \end{tabular}

   105   \end{tabular}\medskip\pause

   106 

   107   \small

   108   \begin{minipage}{1.0\textwidth}

   109   (I also found an {\bf error} in my Ph.D.-thesis about cut-elimination

   110   examined by Henk Barendregt and Andy Pitts.)

   111   \end{minipage}

   112 

   113   \end{frame}}

   114   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   115 *}

   116 

   117 text_raw {*

   118   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   119   \mode<presentation>{

   120   \begin{frame}[t]

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

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

   123 

   124   \begin{center}

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

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

   127   \end{center}

   128 

   129   \begin{itemize}

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

   131   \item<2-> combining automata/graphs

   132 

   133   \onslide<2->{

   134   \begin{center}

   135   \begin{tabular}{ccc}

   136   \begin{tikzpicture}[scale=1]

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

   138   

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

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

   141 

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

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

   144   

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

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

   147 

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

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

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

   151 

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

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

   154   \end{tikzpicture}}

   155 

   156   & 

   157 

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

   159 

   160   &

   161 

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

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

   164   

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

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

   167 

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

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

   170   

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

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

   173 

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

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

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

   177   

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

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

   180 

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

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

   183   \end{tikzpicture}}

   184 

   185   \end{tabular}

   186   \end{center}\medskip

   187 

   188   \only<4-5>{

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

   190   disjoint union:\\[2mm]

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

   192   \end{tabular}}

   193   \end{itemize}

   194 

   195   \only<5>{

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

   197   \begin{block}{}

   198   \medskip

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

   200   Problems with definition for regularity:\bigskip\\

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

   202   \end{minipage}

   203   \end{block}

   204   \end{textblock}}

   205   \medskip

   206 

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

   208 

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

   210 

   211   \end{frame}}

   212   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   213 *}

   214 

   215 text_raw {*

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

   217   \mode<presentation>{

   218   \begin{frame}[t]

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

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

   221 

   222   \begin{center}

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

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

   225   \end{center}

   226 

   227   \begin{itemize}

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

   229   \hspace{2cm}requires absence of \alert{inaccessible states}

   230   \end{itemize}\bigskip\bigskip

   231 

   232   \begin{center}

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

   234   \end{center}

   235 

   236 

   237   \end{frame}}

   238   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   239 *}

   240 

   241 text_raw {*

   242   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   243   \mode<presentation>{

   244   \begin{frame}[t]

   245   \frametitle{}

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

   247 

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

   249   \begin{block}{}

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

   251   {\bf Definition:}\smallskip\\

   252   

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

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

   255   \end{minipage}

   256   \end{block}

   257   \end{textblock}\pause

   258   

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

   260 

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

   262 

   263   \begin{minipage}{1.1\textwidth}

   264   \begin{itemize}

   265   \item pumping lemma\pause

   266   \item closure under complementation\pause

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

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

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

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

   271   \end{itemize}

   272   \end{minipage}

   273 

   274   

   275   \end{frame}}

   276   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   277 

   278 *}

   279 

   280 

   281 text_raw {*

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

   283   \mode<presentation>{

   284   \begin{frame}[c]

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

   286 

   287   \begin{itemize}

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

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

   290 

   291   \item key is the equivalence relation:\medskip

   292   \begin{center}

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

   294   \end{center}

   295   \end{itemize}

   296 

   297  

   298   \end{frame}}

   299   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   300 

   301 *}

   302 

   303 text_raw {*

   304   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   305   \mode<presentation>{

   306   \begin{frame}[c]

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

   308 

   309   \begin{center}

   310   \only<1>{%

   311   \begin{tikzpicture}[scale=3]

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

   313   \end{tikzpicture}}%

   314   \only<2->{%

   315   \begin{tikzpicture}[scale=3]

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

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

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

   319   \end{tikzpicture}}

   320   \end{center}

   321   

   322   \begin{itemize}

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

   324   \end{itemize}

   325 

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

   327   \begin{tikzpicture}

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

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

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

   331   \end{tikzpicture}

   332   \end{textblock}

   333 

   334   \only<2->{%

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

   336   \begin{tikzpicture}

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

   338   {@{text "\<lbrakk>x\<rbrakk>"}$_{\approx_{A}}$};

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

   340   \end{tikzpicture}

   341   \end{textblock}}

   342 

   343   \only<3->{

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

   345   \begin{block}{}

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

   347   Two directions:\medskip\\

   348   \begin{tabular}{@ {}ll}

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

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

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

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

   353   \end{tabular}

   354 

   355   \end{minipage}

   356   \end{block}

   357   \end{textblock}}

   358 

   359   \end{frame}}

   360   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   361 

   362 *}

   363 

   364 

   365 text_raw {*

   366   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   367   \mode<presentation>{

   368   \begin{frame}[c]

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

   370 

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

   372   \textcolor{black}{Equivalence Classes}

   373   \end{textblock}

   374 

   375 

   376   \begin{center}

   377   \begin{tikzpicture}[scale=3]

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

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

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

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

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

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

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

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

   386   \end{tikzpicture}

   387   \end{center}

   388 

   389   \begin{itemize}

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

   391   \smallskip

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

   393   \end{itemize}

   394 

   395   \only<2->{%

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

   397   \begin{tikzpicture}

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

   399   {$[] \in X$};

   400   \end{tikzpicture}

   401   \end{textblock}}

   402 

   403   \only<3->{%

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

   405   \begin{tikzpicture}

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

   407   {a final};

   408   \end{tikzpicture}

   409   \end{textblock}}

   410 

   411   \end{frame}}

   412   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   413 *}

   414 

   415 

   416 text_raw {*

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

   418   \mode<presentation>{

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

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

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

   422 

   423   \begin{center}

   424   \begin{tikzpicture}[scale=3]

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

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

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

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

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

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

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

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

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

   434   \end{tikzpicture}

   435   \end{center}

   436 

   437   \begin{center}

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

   439   \end{center}

   440 

   441   \onslide<8>{

   442   \begin{tabular}{c}

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

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

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

   446   \end{tikzpicture}

   447   \end{tabular}}

   448 

   449   \end{frame}}

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

   451 *}

   452 

   453 

   454 text_raw {*

   455   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   456   \mode<presentation>{

   457   \begin{frame}[c]

   458   \frametitle{\LARGE Systems of Equations}

   459 

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

   461 

   462   \begin{center}

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

   464   \\[-13mm]

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

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

   467 

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

   469 

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

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

   472 

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

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

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

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

   477   \end{tikzpicture}\\

   478   \\[-13mm]

   479   \end{tabular}

   480   \end{center}

   481 

   482   \begin{center}

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

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

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

   486   \end{tabular}

   487   \end{center}

   488 

   489   \end{frame}}

   490   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   491 *}

   492 

   493 

   494 text_raw {*

   495   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   496   \mode<presentation>{

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

   498   \small

   499 

   500   \begin{center}

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

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

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

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

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

   506 

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

   508 

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

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

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

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

   513 

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

   515 

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

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

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

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

   520 

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

   522 

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

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

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

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

   527 

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

   529 

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

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

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

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

   534 

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

   536 

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

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

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

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

   541           \cdot a\cdot a^\star}}\\

   542   \end{tabular}

   543   \end{center}

   544 

   545   \only<8->{

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

   547   \begin{block}{}

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

   549   

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

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

   552 

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

   554 

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

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

   557 

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

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

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

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

   562   \end{tikzpicture}

   563 

   564   \end{minipage}

   565   \end{block}

   566   \end{textblock}}

   567 

   568   \only<1,2>{%

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

   570   \begin{tikzpicture}

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

   572   {\textcolor{red}{a}};

   573   \end{tikzpicture}

   574   \end{textblock}}

   575   \only<2>{%

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

   577   \begin{tikzpicture}

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

   579   {\textcolor{red}{a}};

   580   \end{tikzpicture}

   581   \end{textblock}}

   582   \only<4>{%

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

   584   \begin{tikzpicture}

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

   586   {\textcolor{red}{a}};

   587   \end{tikzpicture}

   588   \end{textblock}}

   589   \only<4>{%

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

   591   \begin{tikzpicture}

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

   593   {\textcolor{red}{a}};

   594   \end{tikzpicture}

   595   \end{textblock}}

   596   \only<5>{%

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

   598   \begin{tikzpicture}

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

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

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

   602   \end{tikzpicture}

   603   \end{textblock}}

   604   \only<5,6>{%

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

   606   \begin{tikzpicture}

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

   608   {\textcolor{red}{a}};

   609   \end{tikzpicture}

   610   \end{textblock}}

   611   \only<6>{%

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

   613   \begin{tikzpicture}

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

   615   {\textcolor{red}{a}};

   616   \end{tikzpicture}

   617   \end{textblock}}

   618   \only<7>{%

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

   620   \begin{tikzpicture}

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

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

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

   624   \end{tikzpicture}

   625   \end{textblock}}

   626 

   627   \end{frame}}

   628   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   629 *}

   630 

   631 

   632 text_raw {*

   633   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   634   \mode<presentation>{

   635   \begin{frame}[c]

   636   \frametitle{\LARGE The Other Direction}

   637 

   638   One has to prove

   639 

   640   \begin{center}

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

   642   \end{center}

   643 

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

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

   646 

   647   

   648   \begin{center}

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

   650   \begin{tikzpicture}[scale=1.1]

   651   %Circle

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

   653   \end{tikzpicture}

   654   &

   655   \begin{tikzpicture}[scale=1.1]

   656   %Circle

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

   658   %Main rays

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

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

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

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

   663   \end{tikzpicture}

   664   &

   665   \begin{tikzpicture}[scale=1.1]

   666   %Circle

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

   668   %Main rays

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

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

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

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

   673   \end{tikzpicture}\\

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

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

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

   677   \end{tabular}}

   678   \end{center}

   679 

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

   681   \begin{tikzpicture}

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

   683   \end{tikzpicture}

   684   \end{textblock}

   685   

   686 

   687   \end{frame}}

   688   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   689 *}

   690 

   691 text_raw {*

   692   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   693   \mode<presentation>{

   694   \begin{frame}[t]

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

   696 

   697   \begin{itemize}

   698   \item introduced by Brozowski~'64

   699   \item a regular expressions after a character has been parsed\\[-18mm]\mbox{}

   700   \end{itemize}

   701 

   702   \only<1>{%

   703   \textcolor{blue}{%

   704   \begin{center}

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

   706   der c $\varnothing$     & $\dn$ & $\varnothing$\\

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

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

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

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

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

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

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

   714   \end{tabular}

   715   \end{center}}}

   716   \only<2>{%

   717   \textcolor{blue}{%

   718   \begin{center}

   719   \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {}}

   720   pder c $\varnothing$     & $\dn$ & \alert{$\{\}$}\\

   721   pder c []                & $\dn$ & \alert{$\{\}$}\\

   722   pder c d                 & $\dn$ & if c $=$ d then $\{$[]$\}$ else $\{\}$\\

   723   pder c ($r_1 + r_2$)     & $\dn$ & (pder c $r_1$) \alert{$\cup$} (der c $r_2$)\\

   724   pder c ($r^\star$)       & $\dn$ & (pder c $r$) $\cdot$ $r^\star$\\

   725   pder c ($r_1 \cdot r_2$) & $\dn$ & if nullable $r_1$\\

   726                           &       & then (pder c $r_1$) $\cdot$ $r_2$ \alert{$\cup$} (pder c $r_2$)\\

   727                           &       & else (pder c $r_1$) $\cdot$ $r_2$\\

   728   \end{tabular}

   729   \end{center}}}

   730 

   731   \only<2>{

   732   \begin{textblock}{6}(8.5,4.7)

   733   \begin{block}{}

   734   \begin{quote}

   735   \begin{minipage}{6cm}\raggedright

   736   \begin{itemize}

   737   \item partial derivatives

   738   \item by Antimirov~'95

   739   \end{itemize}

   740   \end{minipage}

   741   \end{quote}

   742   \end{block}

   743   \end{textblock}}

   744 

   745   \end{frame}}

   746   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   747 *}

   748 

   749 

   750 text_raw {*

   751   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   752   \mode<presentation>{

   753   \begin{frame}[t]

   754   \frametitle{\LARGE Partial Derivatives}

   755 

   756   \mbox{}\\[0mm]\mbox{}

   757 

   758   \begin{itemize}

   759 

   760   \item \alt<1>{\smath{\text{pders $x$ $r$ \mbox{$=$} pders $y$ $r$}}}

   761             {\smath{\underbrace{\text{pders $x$ $r$ \mbox{$=$} pders $y$ $r$}}_{R}}} 

   762         refines \textcolor{blue}{$x$ $\approx_{{\cal L}(r)}$ $y$}\\[16mm]\pause

   763   \item \smath{\text{finite} (U\!N\!IV /\!/ R)} \bigskip\pause

   764   \item Therefore \smath{\text{finite} (U\!N\!IV /\!/ \approx_{{\cal L}(r)})}. Qed.

   765   \end{itemize}

   766   

   767   \only<2->{%

   768   \begin{textblock}{5}(3.9,7.2)

   769   \begin{tikzpicture}

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

   771   \draw (2.2,0) node {Antimirov '95};

   772   \end{tikzpicture}

   773   \end{textblock}}

   774 

   775   \end{frame}}

   776   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   777 *}

   778 

   779 

   780 

   781 text_raw {*

   782   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   783   \mode<presentation>{

   784   \begin{frame}[t]

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

   786 

   787   \begin{itemize}

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

   789   \medskip\pause

   790   \item regular languages are closed under complementation; this is now easy

   791   \begin{center}

   792   \smath{U\!N\!IV /\!/ \approx_A \;\;=\;\; U\!N\!IV /\!/ \approx_{\overline{A}}}

   793   \end{center}\pause\medskip

   794   

   795   \item non-regularity (\smath{a^nb^n})\medskip\pause\pause

   796 

   797   \item take \alert{\bf any} language; build the language of substrings\\

   798   \pause

   799 

   800   then this language \alert{\bf is} regular\;\; (\smath{a^nb^n} $\Rightarrow$ \smath{a^\star{}b^\star})

   801   

   802   \end{itemize}

   803 

   804 \only<2>{

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

   806 \small

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

   808 \end{textblock}} 

   809 

   810 \only<4>{

   811 \begin{textblock}{5}(2,8.6)

   812 \begin{minipage}{8.8cm}

   813 \begin{block}{}

   814 \begin{minipage}{8.6cm}

   815 If there exists a sufficiently large set \smath{B} (for example infinitely large), 

   816 such that

   817 

   818 \begin{center}

   819 \smath{\forall x,y \in B.\; x \not= y \;\Rightarrow\; x \not\approx_{A} y}. 

   820 \end{center}  

   821 

   822 then \smath{A} is not regular.\hspace{1.3cm}\small(\smath{B \dn \bigcup_n a^n})

   823 \end{minipage}

   824 \end{block}

   825 \end{minipage}

   826 \end{textblock}

   827 }

   828 

   829   \end{frame}}

   830   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   831 *}

   832 

   833 

   834 text_raw {*

   835   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   836   \mode<presentation>{

   837   \begin{frame}[c]

   838   \frametitle{\LARGE Conclusion}

   839 

   840   \begin{itemize}

   841   \item We have never seen a proof of Myhill-Nerode based on

   842   regular expressions.\smallskip\pause

   843 

   844   \item great source of examples (inductions)\smallskip\pause

   845 

   846   \item no need to fight the theorem prover:\\ 

   847   \begin{itemize}

   848   \item first direction (790 loc)\\

   849   \item second direction (400 / 390 loc)

   850   \end{itemize}

   851   \end{itemize}

   852 

   853   \end{frame}}

   854   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   855 *}

   856 

   857 text_raw {*

   858   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   859   \mode<presentation>{

   860   \begin{frame}[b]

   861   \frametitle{\mbox{}\\[2cm]\textcolor{red}{Thank you!\\[5mm]Questions?}}

   862 

   863   \end{frame}}

   864   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   865 *}

   866 

   867 (*<*)

   868 end

   869 (*>*)