1 (*<*)

     2 theory Slides7

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

     4 begin

     5 

     6 declare [[show_question_marks = false]]

     7 

     8 notation (latex output)

     9   set ("_") and

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

    11 

    12 (*>*)

    13 

    14 text_raw {*

    15   \renewcommand{\slidecaption}{Beijing, 29.~April 2011}

    16 

    17   \newcommand{\abst}[2]{#1.#2}% atom-abstraction

    18   \newcommand{\pair}[2]{\langle #1,#2\rangle} % pairing

    19   \newcommand{\susp}{{\boldsymbol{\cdot}}}% for suspensions

    20   \newcommand{\unit}{\langle\rangle}% unit

    21   \newcommand{\app}[2]{#1\,#2}% application

    22   \newcommand{\eqprob}{\mathrel{{\approx}?}}

    23   \newcommand{\freshprob}{\mathrel{\#?}}

    24   \newcommand{\redu}[1]{\stackrel{#1}{\Longrightarrow}}% reduction

    25   \newcommand{\id}{\varepsilon}% identity substitution

    26   

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

    28   \newcommand{\gr}[1]{\textcolor{gray}{#1}}

    29   \newcommand{\rd}[1]{\textcolor{red}{#1}}

    30 

    31   \newcommand{\ok}{\includegraphics[scale=0.07]{ok.png}}

    32   \newcommand{\notok}{\includegraphics[scale=0.07]{notok.png}}

    33   \newcommand{\largenotok}{\includegraphics[scale=1]{notok.png}}

    34 

    35   \renewcommand{\Huge}{\fontsize{61.92}{77}\selectfont}

    36   \newcommand{\veryHuge}{\fontsize{74.3}{93}\selectfont}

    37   \newcommand{\VeryHuge}{\fontsize{89.16}{112}\selectfont}

    38   \newcommand{\VERYHuge}{\fontsize{107}{134}\selectfont}

    39 

    40   \newcommand{\LL}{$\mathbb{L}\,$}

    41 

    42 

    43   \pgfdeclareradialshading{smallbluesphere}{\pgfpoint{0.5mm}{0.5mm}}%

    44   {rgb(0mm)=(0,0,0.9);

    45   rgb(0.9mm)=(0,0,0.7);

    46   rgb(1.3mm)=(0,0,0.5);

    47   rgb(1.4mm)=(1,1,1)}

    48 

    49   \def\myitemi{\begin{pgfpicture}{-1ex}{-0.55ex}{1ex}{1ex}

    50     \usebeamercolor[fg]{subitem projected}

    51     {\pgftransformscale{0.8}\pgftext{\normalsize\pgfuseshading{bigsphere}}}

    52     \pgftext{%

    53       \usebeamerfont*{subitem projected}}

    54   \end{pgfpicture}}

    55 

    56   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    57   \mode<presentation>{

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

    59   \frametitle{%

    60   \begin{tabular}{@ {\hspace{-3mm}}c@ {}}

    61   \\

    62   \LARGE Verifying a Regular Expression\\[-1mm] 

    63   \LARGE Matcher and Formal Language\\[-1mm]

    64   \LARGE Theory\\[5mm]

    65   \end{tabular}}

    66   \begin{center}

    67   Christian Urban\\

    68   \small Technical University of Munich, Germany

    69   \end{center}

    70 

    71 

    72   \begin{center}

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

    74   University of Science and Technology in Nanjing

    75   \end{center}

    76   \end{frame}}

    77   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

    78 

    79 *}

    80 

    81 

    82 text_raw {*

    83   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    84   \mode<presentation>{

    85   \begin{frame}[c]

    86   \frametitle{This Talk: 3 Points}

    87   \large

    88   \begin{itemize}

    89   \item It is easy to make mistakes.\bigskip

    90   \item Theorem provers can prevent mistakes, {\bf if} the problem

    91   is formulated so that it is suitable for theorem provers.\bigskip

    92   \item This re-formulation can be done, even in domains where

    93   we least expect it.

    94   \end{itemize}

    95 

    96   \end{frame}}

    97   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

    98 *}

    99 

   100 text_raw {*

   101   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   102   \mode<presentation>{

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

   104   \frametitle{Regular Expressions}

   105 

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

   107   \begin{tabular}{@ {}rrl}

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

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

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

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

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

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

   114   \end{tabular}

   115   \end{textblock}

   116 

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

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

   119   \end{textblock}

   120 

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

   122   \footnotesize Isabelle:

   123   \end{textblock}

   124   

   125   \only<2>{

   126   \begin{textblock}{9}(3.6,11.8)

   127   \bl{matches r s $\;\Longrightarrow\;$ true $\vee$ false}\\[3.5mm]

   128 

   129   \hspace{10mm}\begin{tikzpicture}

   130   \coordinate (m1) at (0.4,1);

   131   \draw (0,0.3) node (m2) {\small\color{gray}rexp};

   132   \path[overlay, ->, line width = 0.5mm, shorten <=-1mm, draw = gray] (m2) edge (m1);

   133   

   134   \coordinate (s1) at (0.81,1);

   135   \draw (1.3,0.3) node (s2) {\small\color{gray} string};

   136   \path[overlay, ->, line width = 0.5mm, shorten <=-1mm, draw = gray] (s2) edge (s1);

   137   \end{tikzpicture}

   138   \end{textblock}}

   139 

   140 

   141 

   142   \end{frame}}

   143   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   144 *}

   145 

   146 text_raw {*

   147   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   148   \mode<presentation>{

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

   150   \frametitle{Specification}

   151 

   152   \small

   153   \begin{textblock}{6}(0,3.5)

   154   \begin{tabular}{r@ {\hspace{0.5mm}}r@ {\hspace{1.5mm}}c@ {\hspace{1.5mm}}l}

   155   \multicolumn{4}{c}{rexp $\Rightarrow$ set of strings}\bigskip\\

   156   &\bl{\LL ($\varnothing$)}   & \bl{$\dn$} & \bl{$\varnothing$}\\

   157   &\bl{\LL ([])}              & \bl{$\dn$} & \bl{\{[]\}}\\

   158   &\bl{\LL (c)}               & \bl{$\dn$} & \bl{\{c\}}\\

   159   &\bl{\LL (r$_1$ + r$_2$)}   & \bl{$\dn$} & \bl{\LL (r$_1$) $\cup$ \LL (r$_2$)}\\

   160   \rd{$\Rightarrow$} &\bl{\LL (r$_1$ $\cdot$ r$_2$)} & \bl{$\dn$} & \bl{\LL (r$_1$) ;; \LL (r$_2$)}\\

   161   \rd{$\Rightarrow$} &\bl{\LL (r$^*$)}           & \bl{$\dn$} & \bl{(\LL (r))$^\star$}\\

   162   \end{tabular}

   163   \end{textblock}

   164 

   165   \begin{textblock}{9}(7.3,3)

   166   {\mbox{}\hspace{2cm}\footnotesize Isabelle:\smallskip}

   167   \includegraphics[scale=0.325]{Screen3.png}

   168   \end{textblock}

   169 

   170   \end{frame}}

   171   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   172 *}

   173 

   174 

   175 text_raw {*

   176   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   177   \mode<presentation>{

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

   179   \frametitle{Version 1}

   180   \small

   181   \mbox{}\\[-8mm]\mbox{}

   182 

   183   \begin{center}\def\arraystretch{1.05}

   184   \begin{tabular}{@ {\hspace{-5mm}}l@ {\hspace{2.5mm}}c@ {\hspace{2.5mm}}l@ {}}

   185   \bl{match [] []}                   & \bl{$=$} & \bl{true}\\

   186   \bl{match [] (c::s)}               & \bl{$=$} & \bl{false}\\

   187   \bl{match ($\varnothing$::rs) s}   & \bl{$=$} & \bl{false}\\

   188   \bl{match ([]::rs) s}              & \bl{$=$} & \bl{match rs s}\\

   189   \bl{match (c::rs) []}              & \bl{$=$} & \bl{false}\\

   190   \bl{match (c::rs) (d::s)}          & \bl{$=$} & \bl{if c = d then match rs s else false}\\     

   191   \bl{match (r$_1$ + r$_2$::rs) s} & \bl{$=$} & \bl{match (r$_1$::rs) s $\vee$ match (r$_2$::rs) s}\\ 

   192   \bl{match (r$_1$ $\cdot$ r$_2$::rs) s} & \bl{$=$} & \bl{match (r$_1$::r$_2$::rs) s}\\

   193   \bl{match (r$^*$::rs) s}          & \bl{$=$} & \bl{match rs s $\vee$ match (r::r$^*$::rs) s}\\

   194   \end{tabular}

   195   \end{center}

   196 

   197   \begin{textblock}{9}(0.2,1.6)

   198   \hspace{10mm}\begin{tikzpicture}

   199   \coordinate (m1) at (0.44,-0.5);

   200   \draw (0,0.3) node (m2) {\small\color{gray}\mbox{}\hspace{-9mm}list of rexps};

   201   \path[overlay, ->, line width = 0.5mm, shorten <=-1mm, draw = gray] (m2) edge (m1);

   202   

   203   \coordinate (s1) at (0.86,-0.5);

   204   \draw (1.5,0.3) node (s2) {\small\color{gray} string};

   205   \path[overlay, ->, line width = 0.5mm, shorten <=-1mm, draw = gray] (s2) edge (s1);

   206   \end{tikzpicture}

   207   \end{textblock}

   208 

   209   \begin{textblock}{9}(2.8,11.8)

   210   \bl{matches$_1$ r s $\;=\;$ match [r] s}

   211   \end{textblock}

   212 

   213   \end{frame}}

   214   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   215 *}

   216 

   217 text_raw {*

   218   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   219   \mode<presentation>{

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

   221   \frametitle{Testing}

   222   

   223   \small

   224   Every good programmer should do thourough tests: 

   225 

   226   \begin{center}

   227   \begin{tabular}{@ {\hspace{-20mm}}lcl}

   228   \bl{matches$_1$ (a$\cdot$b)$^*\;$ []}     & \bl{$\mapsto$} & \bl{true}\\

   229   \bl{matches$_1$ (a$\cdot$b)$^*\;$ ab}   & \bl{$\mapsto$} & \bl{true}\\ 

   230   \bl{matches$_1$ (a$\cdot$b)$^*\;$ aba}  & \bl{$\mapsto$} & \bl{false}\\

   231   \bl{matches$_1$ (a$\cdot$b)$^*\;$ abab} & \bl{$\mapsto$} & \bl{true}\\ 

   232   \bl{matches$_1$ (a$\cdot$b)$^*\;$ abaa} & \bl{$\mapsto$} & \bl{false}\medskip\\

   233   \onslide<2->{\bl{matches$_1$ x$\cdot$(0$|$1)$^*\;$ x}   & \bl{$\mapsto$} & \bl{true}}\\

   234   \onslide<2->{\bl{matches$_1$ x$\cdot$(0$|$1)$^*\;$ x0}  & \bl{$\mapsto$} & \bl{true}}\\

   235   \onslide<2->{\bl{matches$_1$ x$\cdot$(0$|$1)$^*\;$ x3}  & \bl{$\mapsto$} & \bl{false}}

   236   \end{tabular}

   237   \end{center}

   238  

   239   \onslide<3->

   240   {Looks OK \ldots let's ship it to customers\hspace{5mm} 

   241    \raisebox{-5mm}{\includegraphics[scale=0.05]{sun.png}}}

   242   

   243   \end{frame}}

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

   245 *}

   246 

   247 text_raw {*

   248   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   249   \mode<presentation>{

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

   251   \frametitle{Version 1}

   252 

   253   \only<1->{Several hours later\ldots}\pause

   254 

   255 

   256   \begin{center}

   257   \begin{tabular}{@ {\hspace{0mm}}lcl}

   258   \bl{matches$_1$ []$^*$ s}     & \bl{$\mapsto$} & loops\\

   259   \onslide<4->{\bl{matches$_1$ ([] + \ldots)$^*$ s}   & \bl{$\mapsto$} & loops\\} 

   260   \end{tabular}

   261   \end{center}

   262 

   263   \small

   264   \onslide<3->{

   265   \begin{center}

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

   267   \ldots\\

   268   \bl{match ([]::rs) s}           & \bl{$=$} & \bl{match rs s}\\

   269   \ldots\\

   270   \bl{match (r$^*$::rs) s}        & \bl{$=$} & \bl{match rs s $\vee$ match (r::r$^*$::rs) s}\\

   271   \end{tabular}

   272   \end{center}}

   273   

   274 

   275   \end{frame}}

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

   277 *}

   278 

   279 

   280 text_raw {*

   281   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   282   \mode<presentation>{

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

   284   \frametitle{Testing}

   285 

   286   \begin{itemize}

   287   \item While testing is an important part in the process of programming development\pause\ldots

   288 

   289   \item we can only test a {\bf finite} amount of examples.\bigskip\pause

   290 

   291   \begin{center}

   292   \colorbox{cream}

   293   {\gr{\begin{minipage}{10cm}

   294   ``Testing can only show the presence of errors, never their

   295   absence.'' (Edsger W.~Dijkstra)

   296   \end{minipage}}}

   297   \end{center}\bigskip\pause

   298 

   299   \item In a theorem prover we can establish properties that apply to 

   300   {\bf all} input and {\bf all} output. 

   301 

   302   \end{itemize}

   303 

   304   \end{frame}}

   305   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   306 *}

   307 

   308 

   309 text_raw {*

   310   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   311   \mode<presentation>{

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

   313   \frametitle{Version 2}

   314   \mbox{}\\[-14mm]\mbox{}

   315 

   316   \small

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

   318   \bl{nullable ($\varnothing$)}   & \bl{$=$} & \bl{false} &\\

   319   \bl{nullable ([])}              & \bl{$=$} & \bl{true}  &\\

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

   321   \bl{nullable (r$_1$ + r$_2$)}   & \bl{$=$} & \bl{nullable r$_1$ $\vee$ nullable r$_2$} & \\ 

   322   \bl{nullable (r$_1$ $\cdot$ r$_2$)} & \bl{$=$} & \bl{nullable r$_1$ $\wedge$ nullable r$_2$} & \\

   323   \bl{nullable (r$^*$)}           & \bl{$=$} & \bl{true} & \\

   324   \end{tabular}\medskip

   325 

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

   327   \bl{der c ($\varnothing$)}       & \bl{$=$} & \bl{$\varnothing$} & \\

   328   \bl{der c ([])}                  & \bl{$=$} & \bl{$\varnothing$} & \\

   329   \bl{der c (d)}                   & \bl{$=$} & \bl{if c = d then [] else $\varnothing$} & \\

   330   \bl{der c (r$_1$ + r$_2$)}       & \bl{$=$} & \bl{(der c r$_1$) + (der c r$_2$)} & \\

   331   \bl{der c (r$_1$ $\cdot$ r$_2$)} & \bl{$=$} & \bl{((der c r$_1$) $\cdot$ r$_2$)} & \\

   332        &          & \bl{\;\;\;\;+ (if nullable r$_1$ then der c r$_2$ else $\varnothing$)}\\

   333   \bl{der c (r$^*$)}          & \bl{$=$} & \bl{(der c r) $\cdot$ r$^*$} &\smallskip\\

   334 

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

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

   337   \end{tabular}\medskip

   338 

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

   340 

   341   \begin{textblock}{6}(9.5,0.9)

   342   \begin{flushright}

   343   \color{gray}``if r matches []'' 

   344   \end{flushright}

   345   \end{textblock}

   346 

   347   \begin{textblock}{6}(9.5,6.18)

   348   \begin{flushright}

   349   \color{gray}``derivative w.r.t.~a char'' 

   350   \end{flushright}

   351   \end{textblock}

   352 

   353   \begin{textblock}{6}(9.5,12.1)

   354   \begin{flushright}

   355   \color{gray}``deriv.~w.r.t.~a string'' 

   356   \end{flushright}

   357   \end{textblock}

   358 

   359   \begin{textblock}{6}(9.5,13.98)

   360   \begin{flushright}

   361   \color{gray}``main'' 

   362   \end{flushright}

   363   \end{textblock}

   364 

   365   \end{frame}}

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

   367 *}

   368 

   369 text_raw {*

   370   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   371   \mode<presentation>{

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

   373   \frametitle{Is the Matcher Error-Free?}

   374 

   375   We expect that

   376 

   377   \begin{center}

   378   \begin{tabular}{lcl}

   379   \bl{matches$_2$ r s = true}  & \only<1>{\rd{$\Longrightarrow\,\,$}}\only<2>{\rd{$\Longleftarrow\,\,$}}% 

   380   \only<3->{\rd{$\Longleftrightarrow$}} & \bl{s $\in$ \LL(r)}\\

   381   \bl{matches$_2$ r s = false} & \only<1>{\rd{$\Longrightarrow\,\,$}}\only<2>{\rd{$\Longleftarrow\,\,$}}%

   382   \only<3->{\rd{$\Longleftrightarrow$}} & \bl{s $\notin$ \LL(r)}\\

   383   \end{tabular}

   384   \end{center}

   385   \pause\pause\bigskip

   386   By \alert<4->{induction}, we can {\bf prove} these properties.\bigskip

   387 

   388   \begin{tabular}{lrcl}

   389   Lemmas:  & \bl{nullable (r)}          & \bl{$\Longleftrightarrow$} & \bl{[] $\in$ \LL (r)}\\

   390            & \bl{s $\in$ \LL (der c r)} & \bl{$\Longleftrightarrow$} & \bl{(c::s) $\in$ \LL (r)}\\

   391   \end{tabular}

   392   

   393   \only<4->{

   394   \begin{textblock}{3}(0.9,4.5)

   395   \rd{\huge$\forall$\large{}r s.}

   396   \end{textblock}}

   397   \end{frame}}

   398   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   399 *}

   400 

   401 text_raw {*

   402   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   403   \mode<presentation>{

   404   \begin{frame}<1>[c]

   405   \frametitle{

   406   \begin{tabular}{c}

   407   \mbox{}\\[23mm]

   408   \LARGE Demo

   409   \end{tabular}}

   410   

   411   \end{frame}}

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

   413 *}

   414 

   415 

   416 text_raw {*

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

   418   \mode<presentation>{

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

   420 

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

   422 

   423   \small

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

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

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

   427   \bl{nullable (CHR c)}           & \bl{$=$} & \bl{false} &\\

   428   \bl{nullable (ALT r$_1$ r$_2$)} & \bl{$=$} & \bl{(nullable r$_1$) orelse (nullable r$_2$)} & \\ 

   429   \bl{nullable (SEQ r$_1$ r$_2$)} & \bl{$=$} & \bl{(nullable r$_1$) andalso (nullable r$_2$)} & \\

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

   431   \end{tabular}\medskip

   432 

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

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

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

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

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

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

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

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

   441 

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

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

   444   \end{tabular}\medskip

   445 

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

   447   

   448   \only<2>{

   449   \begin{textblock}{8}(1.5,4)

   450   \includegraphics[scale=0.3]{approved.png}

   451   \end{textblock}}

   452   

   453   \end{frame}}

   454   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   455 *}

   456 

   457 

   458 text_raw {*

   459   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   460   \mode<presentation>{

   461   \begin{frame}[c]

   462   \frametitle{No Automata?}

   463 

   464   You might be wondering why I did not use any automata?

   465 

   466   \begin{itemize}

   467   \item {\bf Def.:} A \alert{regular language} is one where there is a DFA that 

   468   recognises it.\bigskip\pause

   469   \end{itemize}

   470 

   471 

   472   There are many reasons why this is a good definition:\medskip

   473   \begin{itemize}

   474   \item pumping lemma

   475   \item closure properties of regular languages\\ (e.g.~closure under complement)

   476   \end{itemize}

   477 

   478   \end{frame}}

   479   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   480 

   481 *}

   482 

   483 text_raw {*

   484   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   485   \mode<presentation>{

   486   \begin{frame}[t]

   487   \frametitle{Really Bad News!}

   488 

   489   DFAs are bad news for formalisations in theorem provers. They might

   490   be represented as:

   491 

   492   \begin{itemize}

   493   \item graphs

   494   \item matrices

   495   \item partial functions

   496   \end{itemize}

   497 

   498   All constructions are messy to reason about.\bigskip\bigskip 

   499   \pause

   500 

   501   \small

   502   \only<2>{

   503   Constable et al needed (on and off) 18 months for a 3-person team 

   504   to formalise automata theory in Nuprl including Myhill-Nerode. There is 

   505   only very little other formalised work on regular languages I know of

   506   in Coq, Isabelle and HOL.}

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

   508   automata with no inaccessible states \ldots''

   509   }

   510   

   511   \end{frame}}

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

   513 

   514 *}

   515 

   516 text_raw {*

   517   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   518   \mode<presentation>{

   519   \begin{frame}[c]

   520   \frametitle{}

   521   \large

   522   \begin{center}

   523   \begin{tabular}{p{9cm}}

   524   My point:\bigskip\\

   525 

   526   The theory about regular languages can be reformulated 

   527   to be more\\ suitable for theorem proving.

   528   \end{tabular}

   529   \end{center}

   530   \end{frame}}

   531   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   532 *}

   533 

   534 text_raw {*

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

   536   \mode<presentation>{

   537   \begin{frame}[c]

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

   539 

   540   \begin{itemize}

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

   542   being regular (pumping lemma only necessary)\medskip

   543 

   544   \item will help with closure properties of regular languages\bigskip\pause

   545 

   546   \item key is the equivalence relation:\smallskip

   547   \begin{center}

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

   549   \end{center}

   550   \end{itemize}

   551 

   552   \end{frame}}

   553   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   554 *}

   555 

   556 text_raw {*

   557   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   558   \mode<presentation>{

   559   \begin{frame}[c]

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

   561 

   562   \mbox{}\\[5cm]

   563 

   564   \begin{itemize}

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

   566   \end{itemize}

   567 

   568   \end{frame}}

   569   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   570 

   571 *}

   572 

   573 text_raw {*

   574   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   575   \mode<presentation>{

   576   \begin{frame}[c]

   577   \frametitle{\LARGE Equivalence Classes}

   578 

   579   \begin{itemize}

   580   \item \smath{L = []}

   581   \begin{center}

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

   583   \end{center}\bigskip\bigskip

   584 

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

   586   \begin{center}

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

   588   \end{center}\bigskip\bigskip

   589 

   590   \item \smath{L = \varnothing}

   591   \begin{center}

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

   593   \end{center}

   594 

   595   \end{itemize}

   596 

   597   \end{frame}}

   598   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   599 

   600 *}

   601 

   602 text_raw {*

   603   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   604   \mode<presentation>{

   605   \begin{frame}[c]

   606   \frametitle{\LARGE Regular Languages}

   607 

   608   \begin{itemize}

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

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

   611 

   612   \item Myhill-Nerode:

   613 

   614   \begin{center}

   615   \begin{tabular}{l}

   616   finite $\Rightarrow$ regular\\

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

   618   regular $\Rightarrow$ finite\\

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

   620   \end{tabular}

   621   \end{center}

   622 

   623   \end{itemize}

   624 

   625   \end{frame}}

   626   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   627 

   628 *}

   629 

   630 text_raw {*

   631   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   632   \mode<presentation>{

   633   \begin{frame}[c]

   634   \frametitle{\LARGE Final Equiv.~Classes}

   635 

   636   \mbox{}\\[3cm]

   637 

   638   \begin{itemize}

   639   \item \smath{\text{finals}\,L \dn 

   640      \{{\lbrack\mkern-2mu\lbrack{s}\rbrack\mkern-2mu\rbrack}_\approx\;|\; s \in L\}}\\

   641   \medskip

   642 

   643   \item we can prove: \smath{L = \bigcup (\text{finals}\,L)}

   644 

   645   \end{itemize}

   646 

   647   \end{frame}}

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

   649 *}

   650 

   651 text_raw {*

   652   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   653   \mode<presentation>{

   654   \begin{frame}[c]

   655   \frametitle{\LARGE Transitions between ECs}

   656 

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

   658 

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

   660   \begin{tabular}{c}

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

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

   663 

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

   665 

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

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

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

   669 

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

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

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

   673             (q_1) edge                node        {$\Sigma$} (q_2);

   674   \end{tikzpicture}

   675   \end{tabular}

   676   &

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

   678   \\[-20mm]

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

   680 

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

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

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

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

   685   \end{tabular}

   686 

   687   \end{tabular}

   688 

   689   \end{frame}}

   690   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   691 *}

   692 

   693 

   694 text_raw {*

   695   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   696   \mode<presentation>{

   697   \begin{frame}[c]

   698   \frametitle{\LARGE Systems of Equations}

   699 

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

   701   characterising the equivalence classes:

   702 

   703   \begin{center}

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

   705   \\[-13mm]

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

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

   708 

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

   710 

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

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

   713 

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

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

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

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

   718   \end{tikzpicture}\\

   719   \\[-13mm]

   720   \end{tabular}

   721   \end{center}

   722 

   723   \begin{center}

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

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

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

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

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

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

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

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

   732   \end{tabular}

   733   \end{center}

   734 

   735   \end{frame}}

   736   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   737 *}

   738 

   739 

   740 text_raw {*

   741   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   742   \mode<presentation>{

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

   744   \small

   745 

   746   \begin{center}

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

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

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

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

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

   752 

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

   754 

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

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

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

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

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

   760 

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

   762 

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

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

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

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

   767 

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

   769 

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

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

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

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

   774 

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

   776 

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

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

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

   780       & \onslide<6->{\smath{R_1; a\cdot a^\star}}\\

   781 

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

   783 

   784   \onslide<7->{\smath{R_1}} & \onslide<7->{\smath{=}} 

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

   786   \onslide<7->{\smath{R_2}} & \onslide<7->{\smath{=}}    

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

   788           \cdot a\cdot a^\star}}\\

   789   \end{tabular}

   790   \end{center}

   791 

   792   \end{frame}}

   793   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   794 *}

   795 

   796 text_raw {*

   797   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   798   \mode<presentation>{

   799   \begin{frame}[c]

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

   801 

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

   803 

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

   805   \begin{center}

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

   807   \end{center}

   808   has the (unique) solution

   809   \begin{center}

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

   811   \end{center}

   812 

   813 

   814   \end{frame}}

   815   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   816 *}

   817 

   818 

   819 text_raw {*

   820   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   821   \mode<presentation>{

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

   823   \small

   824 

   825   \begin{center}

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

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

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

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

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

   831 

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

   833 

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

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

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

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

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

   839 

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

   841 

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

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

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

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

   846 

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

   848 

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

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

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

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

   853 

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

   855 

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

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

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

   859       & \onslide<6->{\smath{R_1; a\cdot a^\star}}\\

   860 

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

   862 

   863   \onslide<7->{\smath{R_1}} & \onslide<7->{\smath{=}} 

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

   865   \onslide<7->{\smath{R_2}} & \onslide<7->{\smath{=}}    

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

   867           \cdot a\cdot a^\star}}\\

   868   \end{tabular}

   869   \end{center}

   870 

   871   \only<8->{

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

   873   \begin{block}{}

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

   875   

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

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

   878 

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

   880 

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

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

   883 

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

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

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

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

   888   \end{tikzpicture}

   889 

   890   \end{minipage}

   891   \end{block}

   892   \end{textblock}}

   893 

   894   \end{frame}}

   895   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   896 *}

   897 

   898 

   899 text_raw {*

   900   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   901   \mode<presentation>{

   902   \begin{frame}[c]

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

   904 

   905   \begin{itemize}

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

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

   908 

   909   \item We need to maintain the invariant that Arden is applicable

   910   (if \smath{[] \not\in A} then \ldots):\medskip

   911 

   912   \begin{center}\small

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

   914   \smath{R_1} & \smath{=} & \smath{R_1; b + R_2; b + \lambda;[]}\\

   915   \smath{R_2} & \smath{=} & \smath{R_1; a + R_2; a}\\

   916 

   917   & & & by Arden\\

   918 

   919   \smath{R_1} & \smath{=} & \smath{R_1; b + R_2; b + \lambda;[]}\\

   920   \smath{R_2} & \smath{=} & \smath{R_1; a\cdot a^\star}\\

   921   \end{tabular}

   922   \end{center}

   923 

   924   \end{itemize}

   925 

   926 

   927   \end{frame}}

   928   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   929 *}

   930 

   931 

   932 

   933 text_raw {*

   934   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   935   \mode<presentation>{

   936   \begin{frame}[c]

   937   \frametitle{\LARGE The Other Direction}

   938   

   939   One has to prove

   940 

   941   \begin{center}

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

   943   \end{center}

   944 

   945   by induction on \smath{r}. This is straightforward for \\the base cases:\small

   946 

   947   \begin{center}

   948   \begin{tabular}{l@ {\hspace{1mm}}l}

   949   \smath{U\!N\!IV /\!/ \!\approx_{\emptyset}} & \smath{= \{U\!N\!IV\}}\smallskip\\

   950   \smath{U\!N\!IV /\!/ \!\approx_{\{[]\}}} & \smath{\subseteq \{\{[]\}, U\!N\!IV - \{[]\}\}}\smallskip\\

   951   \smath{U\!N\!IV /\!/ \!\approx_{\{[c]\}}} & \smath{\subseteq \{\{[]\}, \{[c]\}, U\!N\!IV - \{[], [c]\}\}}

   952   \end{tabular}

   953   \end{center}

   954 

   955   

   956   \end{frame}}

   957   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   958 *}

   959 

   960 

   961 text_raw {*

   962   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   963   \mode<presentation>{

   964   \begin{frame}[t]

   965   \frametitle{\LARGE The Other Direction}

   966 

   967   More complicated are the inductive cases:\\ one needs to prove that if

   968 

   969   \begin{center}

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

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

   972   \end{center}

   973 

   974   then

   975 

   976   \begin{center}

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

   978   \end{center}

   979   

   980   \end{frame}}

   981   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   982 *}

   983 

   984 

   985 text_raw {*

   986   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   987   \mode<presentation>{

   988   \begin{frame}[t]

   989   \frametitle{\LARGE Helper Lemma}

   990 

   991   \begin{center}

   992   \begin{tabular}{p{10cm}}

   993   %If \smath{\text{finite} (f\;' A)} and \smath{f} is injective 

   994   %(on \smath{A}),\\ then \smath{\text{finite}\,A}.

   995   Given two equivalence relations \smath{R_1} and \smath{R_2} with

   996   \smath{R_1} refining \smath{R_2} (\smath{R_1 \subseteq R_2}).\\ 

   997   Then\medskip\\

   998   \smath{\;\;\text{finite} (U\!N\!IV /\!/ R_1) \Rightarrow \text{finite} (U\!N\!IV /\!/ R_2)}

   999   \end{tabular}

  1000   \end{center}

  1001   

  1002   \end{frame}}

  1003   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

  1004 *}

  1005 

  1006 text_raw {*

  1007   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1008   \mode<presentation>{

  1009   \begin{frame}[c]

  1010   \frametitle{\Large Derivatives and Left-Quotients}

  1011   \small

  1012   Work by Brozowski ('64) and Antimirov ('96):\pause\smallskip

  1013 

  1014 

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

  1016   \multicolumn{4}{@ {}l}{Left-Quotient:}\\

  1017   \multicolumn{4}{@ {}l}{\bl{$\text{Ders}\;\text{s}\,A \dn \{\text{s'} \;|\; \text{s @ s'} \in A\}$}}\bigskip\\

  1018 

  1019   \multicolumn{4}{@ {}l}{Derivative:}\\

  1020   \bl{der c ($\varnothing$)}       & \bl{$=$} & \bl{$\varnothing$} & \\

  1021   \bl{der c ([])}                  & \bl{$=$} & \bl{$\varnothing$} & \\

  1022   \bl{der c (d)}                   & \bl{$=$} & \bl{if c = d then [] else $\varnothing$} & \\

  1023   \bl{der c (r$_1$ + r$_2$)}       & \bl{$=$} & \bl{(der c r$_1$) + (der c r$_2$)} & \\

  1024   \bl{der c (r$_1$ $\cdot$ r$_2$)} & \bl{$=$} & \bl{((der c r$_1$) $\cdot$ r$_2$)} & \\

  1025        &          & \bl{\;\;\;\;+ (if nullable r$_1$ then der c r$_2$ else $\varnothing$)}\\

  1026   \bl{der c (r$^*$)}          & \bl{$=$} & \bl{(der c r) $\cdot$ r$^*$} &\smallskip\\

  1027 

  1028   \bl{ders [] r}     & \bl{$=$} & \bl{r} & \\

  1029   \bl{ders (s @ [c]) r} & \bl{$=$} & \bl{der c (ders s r)} & \\

  1030   \end{tabular}\pause

  1031 

  1032   \begin{center}

  1033   \alert{$\Rightarrow$}\smath{\;\;\text{Ders}\,\text{s}\,(\mathbb{L}(\text{r})) = \mathbb{L} (\text{ders s r})}

  1034   \end{center}

  1035   

  1036   \end{frame}}

  1037   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

  1038 *}

  1039 

  1040 text_raw {*

  1041   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1042   \mode<presentation>{

  1043   \begin{frame}[c]

  1044   \frametitle{\LARGE Left-Quotients and MN-Rels}

  1045 

  1046   \begin{itemize}

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

  1048   \item \bl{$\text{Ders}\;s\,A \dn \{s' \;|\; s @ s' \in A\}$}

  1049   \end{itemize}\bigskip

  1050 

  1051   \begin{center}

  1052   \smath{x \approx_A y  \Longleftrightarrow \text{Ders}\;x\;A = \text{Ders}\;y\;A}

  1053   \end{center}\bigskip\pause\small

  1054 

  1055   which means

  1056 

  1057   \begin{center}

  1058   \smath{x \approx_{\mathbb{L}(r)} y  \Longleftrightarrow 

  1059   \mathbb{L}(\text{ders}\;x\;r) = \mathbb{L}(\text{ders}\;y\;r)}

  1060   \end{center}\pause

  1061 

  1062   \hspace{8.8mm}or

  1063   \smath{\;x \approx_{\mathbb{L}(r)} y  \Longleftarrow 

  1064   \text{ders}\;x\;r = \text{ders}\;y\;r}

  1065 

  1066   

  1067 

  1068   \end{frame}}

  1069   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

  1070 *}

  1071 

  1072 text_raw {*

  1073   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1074   \mode<presentation>{

  1075   \begin{frame}[c]

  1076   \frametitle{\LARGE Partial Derivatives}

  1077 

  1078   Antimirov: \bl{pder : rexp $\Rightarrow$ rexp set}\bigskip

  1079 

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

  1081   \bl{pder c ($\varnothing$)}       & \bl{$=$} & \bl{\{$\varnothing$\}} & \\

  1082   \bl{pder c ([])}                  & \bl{$=$} & \bl{\{$\varnothing$\}} & \\

  1083   \bl{pder c (d)}                   & \bl{$=$} & \bl{if c = d then \{[]\} else \{$\varnothing$\}} & \\

  1084   \bl{pder c (r$_1$ + r$_2$)}       & \bl{$=$} & \bl{(pder c r$_1$) $\cup$ (pder c r$_2$)} & \\

  1085   \bl{pder c (r$_1$ $\cdot$ r$_2$)} & \bl{$=$} & \bl{(pder c r$_1$) $\odot$ r$_2$} & \\

  1086        &          & \bl{\hspace{-10mm}$\cup$ (if nullable r$_1$ then pder c r$_2$ else $\varnothing$)}\\

  1087   \bl{pder c (r$^*$)}          & \bl{$=$} & \bl{(pder c r) $\odot$ r$^*$} &\smallskip\\

  1088   \end{tabular}

  1089 

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

  1091   \bl{pders [] r}     & \bl{$=$} & \bl{r} & \\

  1092   \bl{pders (s @ [c]) r} & \bl{$=$} & \bl{pder c (pders s r)} & \\

  1093   \end{tabular}\pause

  1094 

  1095   \begin{center}

  1096   \alert{$\Rightarrow$}\smath{\;\;\text{Ders}\,\text{s}\,(\mathbb{L}(\text{r})) = \bigcup (\mathbb{L}\;`\; (\text{pders s r}))}

  1097   \end{center}

  1098 

  1099   \end{frame}}

  1100   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

  1101 *}

  1102 

  1103 text_raw {*

  1104   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1105   \mode<presentation>{

  1106   \begin{frame}[t]

  1107   \frametitle{\LARGE Final Result}

  1108   

  1109   \mbox{}\\[7mm]

  1110 

  1111   \begin{itemize}

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

  1113             {\smath{\underbrace{\text{pders x r \mbox{$=$} pders y r}}_{R_1}}} 

  1114         refines \bl{x $\approx_{\mathbb{L}(\text{r})}$ y}\pause

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

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

  1117   \end{itemize}

  1118   

  1119   \end{frame}}

  1120   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

  1121 *}

  1122 

  1123 

  1124 text_raw {*

  1125   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1126   \mode<presentation>{

  1127   \begin{frame}[c]

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

  1129 

  1130   \begin{itemize}

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

  1132   \bigskip\pause

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

  1134   \begin{center}