1 (*<*)

     2 theory Slides8

     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}{Copenhagen, 23rd~May 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: 4 Points}

    87   \large

    88   \begin{itemize}

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

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

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

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

    93   we least expect it.\medskip 

    94   \item Where theorem provers are superior to the {\color{gray}{(best)}} human reasoners. ;o)

    95   \end{itemize}

    96 

    97   \end{frame}}

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

    99 *}

   100 

   101 

   102 text_raw {*

   103 

   104   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   105   \mode<presentation>{

   106   \begin{frame}[c]

   107   \frametitle{}

   108 

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

   110   \\[6mm]

   111   \begin{tabular}{c}

   112   \includegraphics[scale=0.12]{harper.jpg}\\[-2mm]

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

   114   {\footnotesize (CMU)}

   115   \end{tabular}

   116   \begin{tabular}{c}

   117   \includegraphics[scale=0.36]{pfenning.jpg}\\[-2mm]

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

   119   {\footnotesize (CMU)}

   120   \end{tabular} &

   121 

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

   123   \raggedright

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

   125   $\sim$31pp}

   126   \end{tabular}\\

   127 

   128   \pause

   129   \\[0mm]

   130   

   131   \begin{tabular}{c}

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

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

   134   {\footnotesize (Princeton)}

   135   \end{tabular} &

   136 

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

   138   \raggedright

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

   140   \end{tabular}

   141   \end{tabular}

   142 

   143 

   144   

   145 

   146 

   147   \end{frame}}

   148   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   149 

   150 *}

   151 

   152 text_raw {*

   153 

   154   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   155   \mode<presentation>{

   156   \begin{frame}

   157   \frametitle{Proof-Carrying Code}

   158 

   159   \begin{textblock}{10}(2.5,2.2)

   160   \begin{block}{Idea:}

   161   \begin{center}

   162   \begin{tikzpicture}

   163   \draw[help lines,cream] (0,0.2) grid (8,4);

   164   

   165   \draw[line width=1mm, red] (5.5,0.6) rectangle (7.5,4);

   166   \node[anchor=base] at (6.5,2.8) 

   167      {\small\begin{tabular}{@ {}p{1.9cm}@ {}}\centering  user: untrusted code\end{tabular}};

   168 

   169   \draw[line width=1mm, red] (0.5,0.6) rectangle (2.5,4);

   170   \node[anchor=base] at (1.5,2.3) 

   171      {\small\begin{tabular}{@ {}p{1.9cm}@ {}}\centering  developer ---\\ web server\end{tabular}};

   172   

   173   \onslide<3->{

   174   \draw[line width=1mm, red, fill=red] (5.5,0.6) rectangle (7.5,1.8);

   175   \node[anchor=base,white] at (6.5,1.1) 

   176      {\small\begin{tabular}{@ {}p{1.9cm}@ {}}\bf\centering proof- checker\end{tabular}};}

   177 

   178   \node at (3.8,3.0) [single arrow, fill=red,text=white, minimum height=3cm]{\bf code};

   179   \onslide<2->{

   180   \node at (3.8,1.3) [single arrow, fill=red,text=white, minimum height=3cm]{\bf certificate};

   181   \node at (3.8,1.9) {\small\color{gray}{\mbox{}\hspace{-1mm}a proof in LF}};

   182   }

   183 

   184   

   185   \end{tikzpicture}

   186   \end{center}

   187   \end{block}

   188   \end{textblock}

   189 

   190   %\begin{textblock}{15}(2,12)

   191   %\small

   192   %\begin{itemize}

   193   %\item<4-> Appel's checker is $\sim$2700 lines of code (1865 loc of\\ LF definitions; 

   194   %803 loc in C including 2 library functions)\\[-3mm]

   195   %\item<5-> 167 loc in C implement a type-checker

   196   %\end{itemize}

   197   %\end{textblock}

   198 

   199   \end{frame}}

   200   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   201 

   202 *}

   203 

   204 text {*

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

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

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

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

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

   210   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   211   \mode<presentation>{

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

   213   \frametitle{} 

   214   

   215   \begin{columns}

   216   

   217   \begin{column}{0.8\textwidth}

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

   219 

   220   \begin{tikzpicture}

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

   222   { \&[-10mm] 

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

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

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

   226     

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

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

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

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

   231      

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

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

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

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

   236 

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

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

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

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

   241   };

   242 

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

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

   245   

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

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

   248 

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

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

   251   

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

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

   254 

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

   256   \end{tikzpicture}

   257 

   258   \end{textblock}

   259   \end{column}

   260   \end{columns}

   261 

   262 

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

   264   \onslide<4->{

   265   \begin{tikzpicture}

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

   267   \end{tikzpicture}}

   268   \end{textblock}

   269 

   270   \end{frame}}

   271   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   272 

   273 *}

   274 

   275 

   276 (*<*)

   277 atom_decl name

   278 

   279 nominal_datatype lam = 

   280     Var "name"

   281   | App "lam" "lam"

   282   | Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam [_]._" [100,100] 100)

   283 

   284 nominal_primrec

   285   subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"  ("_[_::=_]")

   286 where

   287   "(Var x)[y::=s] = (if x=y then s else (Var x))"

   288 | "(App t\<^isub>1 t\<^isub>2)[y::=s] = App (t\<^isub>1[y::=s]) (t\<^isub>2[y::=s])"

   289 | "x\<sharp>(y,s) \<Longrightarrow> (Lam [x].t)[y::=s] = Lam [x].(t[y::=s])"

   290 apply(finite_guess)+

   291 apply(rule TrueI)+

   292 apply(simp add: abs_fresh)

   293 apply(fresh_guess)+

   294 done

   295 

   296 lemma  subst_eqvt[eqvt]:

   297   fixes pi::"name prm"

   298   shows "pi\<bullet>(t1[x::=t2]) = (pi\<bullet>t1)[(pi\<bullet>x)::=(pi\<bullet>t2)]"

   299 by (nominal_induct t1 avoiding: x t2 rule: lam.strong_induct)

   300    (auto simp add: perm_bij fresh_atm fresh_bij)

   301 

   302 lemma fresh_fact:

   303   fixes z::"name"

   304   shows "\<lbrakk>z\<sharp>s; (z=y \<or> z\<sharp>t)\<rbrakk> \<Longrightarrow> z\<sharp>t[y::=s]"

   305 by (nominal_induct t avoiding: z y s rule: lam.strong_induct)

   306    (auto simp add: abs_fresh fresh_prod fresh_atm)

   307 

   308 lemma forget: 

   309   assumes asm: "x\<sharp>L"

   310   shows "L[x::=P] = L"

   311   using asm 

   312 by (nominal_induct L avoiding: x P rule: lam.strong_induct)

   313    (auto simp add: abs_fresh fresh_atm)

   314 (*>*)

   315 

   316 text_raw {*

   317   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   318   \mode<presentation>{

   319   \begin{frame}

   320 

   321   \begin{textblock}{16}(1,1)

   322   \renewcommand{\isasymbullet}{$\cdot$}

   323   \tiny\color{black}

   324 *}

   325 lemma substitution_lemma_not_to_be_tried_at_home: 

   326   assumes asm: "x\<noteq>y" "x\<sharp>L"

   327   shows "M[x::=N][y::=L] = M[y::=L][x::=N[y::=L]]"

   328 using asm

   329 proof (induct M arbitrary: x y N L rule: lam.induct)

   330   case (Lam z M1) 

   331   have ih: "\<And>x y N L. \<lbrakk>x\<noteq>y; x\<sharp>L\<rbrakk> \<Longrightarrow> M1[x::=N][y::=L] = M1[y::=L][x::=N[y::=L]]" by fact

   332   have "x\<noteq>y" by fact

   333   have "x\<sharp>L" by fact

   334   obtain z'::"name" where fc: "z'\<sharp>(x,y,z,M1,N,L)" by (rule exists_fresh) (auto simp add: fs_name1)

   335   have eq: "Lam [z'].([(z',z)]\<bullet>M1) = Lam [z].M1" using fc 

   336     by (auto simp add: lam.inject alpha fresh_prod fresh_atm)

   337   have fc': "z'\<sharp>N[y::=L]" using fc by (simp add: fresh_fact fresh_prod)

   338   have "([(z',z)]\<bullet>x) \<noteq> ([(z',z)]\<bullet>y)" using `x\<noteq>y` by (auto simp add: calc_atm)

   339   moreover

   340   have "([(z',z)]\<bullet>x)\<sharp>([(z',z)]\<bullet>L)" using `x\<sharp>L` by (simp add: fresh_bij)

   341   ultimately 

   342   have "M1[([(z',z)]\<bullet>x)::=([(z',z)]\<bullet>N)][([(z',z)]\<bullet>y)::=([(z',z)]\<bullet>L)] 

   343         = M1[([(z',z)]\<bullet>y)::=([(z',z)]\<bullet>L)][([(z',z)]\<bullet>x)::=([(z',z)]\<bullet>N)[([(z',z)]\<bullet>y)::=([(z',z)]\<bullet>L)]]"

   344     using ih by simp

   345   then have "[(z',z)]\<bullet>(M1[([(z',z)]\<bullet>x)::=([(z',z)]\<bullet>N)][([(z',z)]\<bullet>y)::=([(z',z)]\<bullet>L)] 

   346         = M1[([(z',z)]\<bullet>y)::=([(z',z)]\<bullet>L)][([(z',z)]\<bullet>x)::=([(z',z)]\<bullet>N)[([(z',z)]\<bullet>y)::=([(z',z)]\<bullet>L)]])"

   347     by (simp add: perm_bool)

   348   then have ih': "([(z',z)]\<bullet>M1)[x::=N][y::=L] = ([(z',z)]\<bullet>M1)[y::=L][x::=N[y::=L]]"

   349     by (simp add: eqvts perm_swap)

   350   show "(Lam [z].M1)[x::=N][y::=L] = (Lam [z].M1)[y::=L][x::=N[y::=L]]" (is "?LHS=?RHS") 

   351   proof - 

   352     have "?LHS = (Lam [z'].([(z',z)]\<bullet>M1))[x::=N][y::=L]" using eq by simp

   353     also have "\<dots> = Lam [z'].(([(z',z)]\<bullet>M1)[x::=N][y::=L])" using fc by (simp add: fresh_prod)

   354     also from ih have "\<dots> = Lam [z'].(([(z',z)]\<bullet>M1)[y::=L][x::=N[y::=L]])" sorry 

   355     also have "\<dots> = (Lam [z'].([(z',z)]\<bullet>M1))[y::=L][x::=N[y::=L]]" using fc fc' by (simp add: fresh_prod)

   356     also have "\<dots> = ?RHS" using eq by simp

   357     finally show "?LHS = ?RHS" .

   358   qed

   359 qed (auto simp add: forget)

   360 text_raw {*

   361   \end{textblock}

   362   \mbox{}

   363 

   364   \only<2->{

   365   \begin{textblock}{11.5}(4,2.3)

   366   \begin{minipage}{9.3cm}

   367   \begin{block}{}\footnotesize

   368 *}

   369 lemma substitution_lemma\<iota>:

   370   assumes asm: "x \<noteq> y" "x \<sharp> L"

   371   shows "M[x::=N][y::=L] = M[y::=L][x::=N[y::=L]]"

   372   using asm

   373 by (nominal_induct M avoiding: x y N L rule: lam.strong_induct)

   374      (auto simp add: forget fresh_fact)

   375 text_raw {*  

   376   \end{block}

   377   \end{minipage}

   378   \end{textblock}}

   379   \end{frame}}

   380   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   381 *}

   382 

   383 

   384 text_raw {*

   385   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   386   \mode<presentation>{

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

   388   \frametitle{Regular Expressions}

   389 

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

   391   \begin{tabular}{@ {}rrl}

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

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

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

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

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

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

   398   \end{tabular}

   399   \end{textblock}

   400 

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

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

   403   \end{textblock}

   404 

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

   406   \footnotesize Isabelle:

   407   \end{textblock}

   408   

   409   \only<2>{

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

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

   412 

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

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

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

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

   417   

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

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

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

   421   \end{tikzpicture}

   422   \end{textblock}}

   423 

   424 

   425 

   426   \end{frame}}

   427   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   428 *}

   429 

   430 text_raw {*

   431   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   432   \mode<presentation>{

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

   434   \frametitle{Specification}

   435 

   436   \small

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

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

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

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

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

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

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

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

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

   446   \end{tabular}

   447   \end{textblock}

   448 

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

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

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

   452   \end{textblock}

   453 

   454   \end{frame}}

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

   456 *}

   457 

   458 

   459 text_raw {*

   460   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   461   \mode<presentation>{

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

   463   \frametitle{Version 1}

   464   \small

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

   466 

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

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

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

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

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

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

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

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

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

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

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

   478   \end{tabular}

   479   \end{center}

   480 

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

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

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

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

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

   486   

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

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

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

   490   \end{tikzpicture}

   491   \end{textblock}

   492 

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

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

   495   \end{textblock}

   496 

   497   \end{frame}}

   498   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   499 *}

   500 

   501 text_raw {*

   502   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   503   \mode<presentation>{

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

   505   \frametitle{Testing}

   506   

   507   \small

   508   Every good programmer should do thourough tests: 

   509 

   510   \begin{center}

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

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

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

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

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

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

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

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

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

   520   \end{tabular}

   521   \end{center}

   522  

   523   \onslide<3->

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

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

   526   

   527   \end{frame}}

   528   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   529 *}

   530 

   531 text_raw {*

   532   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   533   \mode<presentation>{

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

   535   \frametitle{Version 1}

   536 

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

   538 

   539 

   540   \begin{center}

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

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

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

   544   \end{tabular}

   545   \end{center}

   546 

   547   \small

   548   \onslide<3->{

   549   \begin{center}

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

   551   \ldots\\

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

   553   \ldots\\

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

   555   \end{tabular}

   556   \end{center}}

   557   

   558 

   559   \end{frame}}

   560   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   561 *}

   562 

   563 

   564 text_raw {*

   565   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   566   \mode<presentation>{

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

   568   \frametitle{Testing}

   569 

   570   \begin{itemize}

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

   572 

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

   574 

   575   \begin{center}

   576   \colorbox{cream}

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

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

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

   580   \end{minipage}}}

   581   \end{center}\bigskip\pause

   582 

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

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

   585 

   586   \end{itemize}

   587 

   588   \end{frame}}

   589   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   590 *}

   591 

   592 

   593 text_raw {*

   594   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   595   \mode<presentation>{

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

   597   \frametitle{Version 2}

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

   599 

   600   \small

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

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

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

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

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

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

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

   608   \end{tabular}\medskip

   609 

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

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

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

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

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

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

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

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

   618 

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

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

   621   \end{tabular}\medskip

   622 

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

   624 

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

   626   \begin{flushright}

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

   628   \end{flushright}

   629   \end{textblock}

   630 

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

   632   \begin{flushright}

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

   634   \end{flushright}

   635   \end{textblock}

   636 

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

   638   \begin{flushright}

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

   640   \end{flushright}

   641   \end{textblock}

   642 

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

   644   \begin{flushright}

   645   \color{gray}``main'' 

   646   \end{flushright}

   647   \end{textblock}

   648 

   649   \end{frame}}

   650   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   651 *}

   652 

   653 text_raw {*

   654   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   655   \mode<presentation>{

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

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

   658 

   659   We expect that

   660 

   661   \begin{center}

   662   \begin{tabular}{lcl}

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

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

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

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

   667   \end{tabular}

   668   \end{center}

   669   \pause\pause\bigskip

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

   671 

   672   \begin{tabular}{lrcl}

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

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

   675   \end{tabular}

   676   

   677   \only<4->{

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

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

   680   \end{textblock}}

   681   \end{frame}}

   682   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   683 *}

   684 

   685 text_raw {*

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

   687   \mode<presentation>{

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

   689   \frametitle{

   690   \begin{tabular}{c}

   691   \mbox{}\\[23mm]

   692   \LARGE Demo

   693   \end{tabular}}

   694   

   695   \end{frame}}

   696   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   697 *}

   698 

   699 

   700 text_raw {*

   701   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   702   \mode<presentation>{

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

   704 

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

   706 

   707   \small

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

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

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

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

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

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

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

   715   \end{tabular}\medskip

   716 

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

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

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

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

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

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

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

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

   725 

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

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

   728   \end{tabular}\medskip

   729 

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

   731   

   732   \only<2>{

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

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

   735   \end{textblock}}

   736   

   737   \end{frame}}

   738   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   739 *}

   740 

   741 

   742 text_raw {*

   743   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   744   \mode<presentation>{

   745   \begin{frame}[c]

   746   \frametitle{No Automata?}

   747 

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

   749 

   750   \begin{itemize}

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

   752   recognises it.\bigskip\pause

   753   \end{itemize}

   754 

   755 

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

   757   \begin{itemize}

   758   \item pumping lemma

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

   760   \end{itemize}

   761 

   762   \end{frame}}

   763   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   764 

   765 *}

   766 

   767 text_raw {*

   768   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   769   \mode<presentation>{

   770   \begin{frame}[t]

   771   \frametitle{Really Bad News!}

   772 

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

   774   be represented as:

   775 

   776   \begin{itemize}

   777   \item graphs

   778   \item matrices

   779   \item partial functions

   780   \end{itemize}

   781 

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

   783   \pause

   784 

   785   \small

   786   \only<2>{

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

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

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

   790   in Coq, Isabelle and HOL.}

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

   792   automata with no inaccessible states \ldots''

   793   }

   794   

   795   \end{frame}}

   796   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   797 

   798 *}

   799 

   800 text_raw {*

   801   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   802   \mode<presentation>{

   803   \begin{frame}[c]

   804   \frametitle{}

   805   \large

   806   \begin{center}

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

   808   My point:\bigskip\\

   809 

   810   The theory about regular languages can be reformulated 

   811   to be more\\ suitable for theorem proving.

   812   \end{tabular}

   813   \end{center}

   814   \end{frame}}

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

   816 *}

   817 

   818 text_raw {*

   819   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   820   \mode<presentation>{

   821   \begin{frame}[c]

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

   823 

   824   \begin{itemize}

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

   826   being regular (pumping lemma only necessary)\medskip

   827 

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

   829 

   830   \item key is the equivalence relation:\smallskip

   831   \begin{center}

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

   833   \end{center}

   834   \end{itemize}

   835 

   836   \end{frame}}

   837   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   838 *}

   839 

   840 text_raw {*

   841   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   842   \mode<presentation>{

   843   \begin{frame}[c]

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

   845 

   846   \mbox{}\\[5cm]

   847 

   848   \begin{itemize}

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

   850   \end{itemize}

   851 

   852   \end{frame}}

   853   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   854 

   855 *}

   856 

   857 text_raw {*

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

   859   \mode<presentation>{

   860   \begin{frame}[c]

   861   \frametitle{\LARGE Equivalence Classes}

   862 

   863   \begin{itemize}

   864   \item \smath{L = []}

   865   \begin{center}

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

   867   \end{center}\bigskip\bigskip

   868 

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

   870   \begin{center}

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

   872   \end{center}\bigskip\bigskip

   873 

   874   \item \smath{L = \varnothing}

   875   \begin{center}

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

   877   \end{center}

   878 

   879   \end{itemize}

   880 

   881   \end{frame}}

   882   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   883 

   884 *}

   885 

   886 text_raw {*

   887   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   888   \mode<presentation>{

   889   \begin{frame}[c]

   890   \frametitle{\LARGE Regular Languages}

   891 

   892   \begin{itemize}

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

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

   895 

   896   \item Myhill-Nerode:

   897 

   898   \begin{center}

   899   \begin{tabular}{l}

   900   finite $\Rightarrow$ regular\\

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

   902   regular $\Rightarrow$ finite\\

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

   904   \end{tabular}

   905   \end{center}

   906 

   907   \end{itemize}

   908 

   909   \end{frame}}

   910   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   911 

   912 *}

   913 

   914 text_raw {*

   915   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   916   \mode<presentation>{

   917   \begin{frame}[c]

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

   919 

   920   \mbox{}\\[3cm]

   921 

   922   \begin{itemize}

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

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

   925   \medskip

   926 

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

   928 

   929   \end{itemize}

   930 

   931   \end{frame}}

   932   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   933 *}

   934 

   935 text_raw {*

   936   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   937   \mode<presentation>{

   938   \begin{frame}[c]

   939   \frametitle{\LARGE Transitions between ECs}

   940 

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

   942 

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

   944   \begin{tabular}{c}

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

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

   947 

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

   949 

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

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

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

   953 

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

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

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

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

   958   \end{tikzpicture}

   959   \end{tabular}

   960   &

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

   962   \\[-20mm]

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

   964 

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

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

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

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

   969   \end{tabular}

   970 

   971   \end{tabular}

   972 

   973   \end{frame}}

   974   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   975 *}

   976 

   977 

   978 text_raw {*

   979   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   980   \mode<presentation>{

   981   \begin{frame}[c]

   982   \frametitle{\LARGE Systems of Equations}

   983 

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

   985   characterising the equivalence classes:

   986 

   987   \begin{center}

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

   989   \\[-13mm]

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

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

   992 

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

   994 

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

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

   997 

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

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

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

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

  1002   \end{tikzpicture}\\

  1003   \\[-13mm]

  1004   \end{tabular}

  1005   \end{center}

  1006 

  1007   \begin{center}

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

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

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

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

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

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

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

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

  1016   \end{tabular}

  1017   \end{center}

  1018 

  1019   \end{frame}}

  1020   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

  1021 *}

  1022 

  1023 

  1024 text_raw {*

  1025   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1026   \mode<presentation>{

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

  1028   \small

  1029 

  1030   \begin{center}

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

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

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

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

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

  1036 

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

  1038 

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

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

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

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

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

  1044 

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

  1046 

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

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

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

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

  1051 

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

  1053 

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

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

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

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

  1058 

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

  1060 

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

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

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

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

  1065 

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

  1067 

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

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

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

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

  1072           \cdot a\cdot a^\star}}\\

  1073   \end{tabular}

  1074   \end{center}

  1075 

  1076   \end{frame}}

  1077   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

  1078 *}

  1079 

  1080 text_raw {*

  1081   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1082   \mode<presentation>{

  1083   \begin{frame}[c]

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

  1085 

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

  1087 

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

  1089   \begin{center}

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

  1091   \end{center}

  1092   has the (unique) solution

  1093   \begin{center}

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

  1095   \end{center}

  1096 

  1097 

  1098   \end{frame}}

  1099   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

  1100 *}

  1101 

  1102 

  1103 text_raw {*

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

  1105   \mode<presentation>{

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

  1107   \small

  1108 

  1109   \begin{center}

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

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

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

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

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

  1115 

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

  1117 

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

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

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

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

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

  1123 

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

  1125 

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

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

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

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

  1130 

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

  1132 

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

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

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