Slides/Slides8.thy
branchNominal2-Isabelle2011-1
changeset 3070 4b4742aa43f2
parent 3069 78d828f43cdf
child 3071 11f6a561eb4b
equal deleted inserted replaced
3069:78d828f43cdf 3070:4b4742aa43f2
     1 (*<*)
       
     2 theory Slides8
       
     3 imports "~~/src/HOL/Library/LaTeXsugar" "Nominal"
       
     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->[c]
       
   388   \frametitle{Lesson Learned}
       
   389 
       
   390   \begin{textblock}{11.5}(1.2,5)
       
   391   \begin{minipage}{10.5cm}
       
   392   \begin{block}{}
       
   393   Theorem provers can keep large proofs and definitions consistent and
       
   394   make them modifiable.
       
   395    \end{block}
       
   396   \end{minipage}
       
   397   \end{textblock}
       
   398 
       
   399   
       
   400   \end{frame}}
       
   401   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
       
   402 *}
       
   403 
       
   404 text_raw {*
       
   405   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
   406   \mode<presentation>{
       
   407   \begin{frame}
       
   408   \frametitle{}
       
   409 
       
   410   \begin{textblock}{11.5}(0.8,2.3)
       
   411   \begin{minipage}{11.2cm}
       
   412   In most papers/books: 
       
   413   \begin{block}{}
       
   414   \color{darkgray}
       
   415   ``\ldots this necessary hygienic discipline is somewhat swept under the carpet via
       
   416   the so-called `{\bf variable convention}' \ldots
       
   417   The {\color{black}{\bf belief}} that this is {\bf sound} came from the calculus 
       
   418   with nameless binders in de Bruijn'' 
       
   419   \end{block}\medskip
       
   420   \end{minipage}
       
   421   \end{textblock}
       
   422 
       
   423   \begin{textblock}{11.5}(0.8,10)
       
   424   \includegraphics[scale=0.25]{LambdaBook.jpg}\hspace{-3mm}\includegraphics[scale=0.3]{barendregt.jpg}
       
   425   \end{textblock}
       
   426   \end{frame}}
       
   427   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
       
   428 *}
       
   429 
       
   430 
       
   431 text_raw {*
       
   432   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
   433   \mode<presentation>{
       
   434   \begin{frame}<1->[t]
       
   435   \frametitle{Regular Expressions}
       
   436 
       
   437   \begin{textblock}{6}(2,4)
       
   438   \begin{tabular}{@ {}rrl}
       
   439   \bl{r} & \bl{$::=$}  & \bl{$\varnothing$}\\
       
   440          & \bl{$\mid$} & \bl{[]}\\
       
   441          & \bl{$\mid$} & \bl{c}\\
       
   442          & \bl{$\mid$} & \bl{r$_1$ + r$_2$}\\
       
   443          & \bl{$\mid$} & \bl{r$_1$ $\cdot$ r$_2$}\\
       
   444          & \bl{$\mid$} & \bl{r$^*$}\\
       
   445   \end{tabular}
       
   446   \end{textblock}
       
   447 
       
   448   \begin{textblock}{6}(8,3.5)
       
   449   \includegraphics[scale=0.35]{Screen1.png}
       
   450   \end{textblock}
       
   451 
       
   452   \begin{textblock}{6}(10.2,2.8)
       
   453   \footnotesize Isabelle:
       
   454   \end{textblock}
       
   455   
       
   456   \only<2>{
       
   457   \begin{textblock}{9}(3.6,11.8)
       
   458   \bl{matches r s $\;\Longrightarrow\;$ true $\vee$ false}\\[3.5mm]
       
   459 
       
   460   \hspace{10mm}\begin{tikzpicture}
       
   461   \coordinate (m1) at (0.4,1);
       
   462   \draw (0,0.3) node (m2) {\small\color{gray}rexp};
       
   463   \path[overlay, ->, line width = 0.5mm, shorten <=-1mm, draw = gray] (m2) edge (m1);
       
   464   
       
   465   \coordinate (s1) at (0.81,1);
       
   466   \draw (1.3,0.3) node (s2) {\small\color{gray} string};
       
   467   \path[overlay, ->, line width = 0.5mm, shorten <=-1mm, draw = gray] (s2) edge (s1);
       
   468   \end{tikzpicture}
       
   469   \end{textblock}}
       
   470 
       
   471 
       
   472 
       
   473   \end{frame}}
       
   474   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
       
   475 *}
       
   476 
       
   477 text_raw {*
       
   478   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
   479   \mode<presentation>{
       
   480   \begin{frame}<1->[t]
       
   481   \frametitle{Specification}
       
   482 
       
   483   \small
       
   484   \begin{textblock}{6}(0,3.5)
       
   485   \begin{tabular}{r@ {\hspace{0.5mm}}r@ {\hspace{1.5mm}}c@ {\hspace{1.5mm}}l}
       
   486   \multicolumn{4}{c}{rexp $\Rightarrow$ set of strings}\bigskip\\
       
   487   &\bl{\LL ($\varnothing$)}   & \bl{$\dn$} & \bl{$\varnothing$}\\
       
   488   &\bl{\LL ([])}              & \bl{$\dn$} & \bl{\{[]\}}\\
       
   489   &\bl{\LL (c)}               & \bl{$\dn$} & \bl{\{c\}}\\
       
   490   &\bl{\LL (r$_1$ + r$_2$)}   & \bl{$\dn$} & \bl{\LL (r$_1$) $\cup$ \LL (r$_2$)}\\
       
   491   \rd{$\Rightarrow$} &\bl{\LL (r$_1$ $\cdot$ r$_2$)} & \bl{$\dn$} & \bl{\LL (r$_1$) ;; \LL (r$_2$)}\\
       
   492   \rd{$\Rightarrow$} &\bl{\LL (r$^*$)}           & \bl{$\dn$} & \bl{(\LL (r))$^\star$}\\
       
   493   \end{tabular}
       
   494   \end{textblock}
       
   495 
       
   496   \begin{textblock}{9}(7.3,3)
       
   497   {\mbox{}\hspace{2cm}\footnotesize Isabelle:\smallskip}
       
   498   \includegraphics[scale=0.325]{Screen3.png}
       
   499   \end{textblock}
       
   500 
       
   501   \end{frame}}
       
   502   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
       
   503 *}
       
   504 
       
   505 
       
   506 text_raw {*
       
   507   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
   508   \mode<presentation>{
       
   509   \begin{frame}<1->[t]
       
   510   \frametitle{Version 1}
       
   511   \small
       
   512   \mbox{}\\[-8mm]\mbox{}
       
   513 
       
   514   \begin{center}\def\arraystretch{1.05}
       
   515   \begin{tabular}{@ {\hspace{-5mm}}l@ {\hspace{2.5mm}}c@ {\hspace{2.5mm}}l@ {}}
       
   516   \bl{match [] []}                   & \bl{$=$} & \bl{true}\\
       
   517   \bl{match [] (c::s)}               & \bl{$=$} & \bl{false}\\
       
   518   \bl{match ($\varnothing$::rs) s}   & \bl{$=$} & \bl{false}\\
       
   519   \bl{match ([]::rs) s}              & \bl{$=$} & \bl{match rs s}\\
       
   520   \bl{match (c::rs) []}              & \bl{$=$} & \bl{false}\\
       
   521   \bl{match (c::rs) (d::s)}          & \bl{$=$} & \bl{if c = d then match rs s else false}\\     
       
   522   \bl{match (r$_1$ + r$_2$::rs) s} & \bl{$=$} & \bl{match (r$_1$::rs) s $\vee$ match (r$_2$::rs) s}\\ 
       
   523   \bl{match (r$_1$ $\cdot$ r$_2$::rs) s} & \bl{$=$} & \bl{match (r$_1$::r$_2$::rs) s}\\
       
   524   \bl{match (r$^*$::rs) s}          & \bl{$=$} & \bl{match rs s $\vee$ match (r::r$^*$::rs) s}\\
       
   525   \end{tabular}
       
   526   \end{center}
       
   527 
       
   528   \begin{textblock}{9}(0.2,1.6)
       
   529   \hspace{10mm}\begin{tikzpicture}
       
   530   \coordinate (m1) at (0.44,-0.5);
       
   531   \draw (0,0.3) node (m2) {\small\color{gray}\mbox{}\hspace{-9mm}list of rexps};
       
   532   \path[overlay, ->, line width = 0.5mm, shorten <=-1mm, draw = gray] (m2) edge (m1);
       
   533   
       
   534   \coordinate (s1) at (0.86,-0.5);
       
   535   \draw (1.5,0.3) node (s2) {\small\color{gray} string};
       
   536   \path[overlay, ->, line width = 0.5mm, shorten <=-1mm, draw = gray] (s2) edge (s1);
       
   537   \end{tikzpicture}
       
   538   \end{textblock}
       
   539 
       
   540   \begin{textblock}{9}(2.8,11.8)
       
   541   \bl{matches$_1$ r s $\;=\;$ match [r] s}
       
   542   \end{textblock}
       
   543 
       
   544   \end{frame}}
       
   545   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
       
   546 *}
       
   547 
       
   548 text_raw {*
       
   549   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
   550   \mode<presentation>{
       
   551   \begin{frame}<1->[c]
       
   552   \frametitle{Testing}
       
   553   
       
   554   \small
       
   555   Every good programmer should do thourough tests: 
       
   556 
       
   557   \begin{center}
       
   558   \begin{tabular}{@ {\hspace{-20mm}}lcl}
       
   559   \bl{matches$_1$ (a$\cdot$b)$^*\;$ []}     & \bl{$\mapsto$} & \bl{true}\\
       
   560   \bl{matches$_1$ (a$\cdot$b)$^*\;$ ab}   & \bl{$\mapsto$} & \bl{true}\\ 
       
   561   \bl{matches$_1$ (a$\cdot$b)$^*\;$ aba}  & \bl{$\mapsto$} & \bl{false}\\
       
   562   \bl{matches$_1$ (a$\cdot$b)$^*\;$ abab} & \bl{$\mapsto$} & \bl{true}\\ 
       
   563   \bl{matches$_1$ (a$\cdot$b)$^*\;$ abaa} & \bl{$\mapsto$} & \bl{false}\medskip\\
       
   564   \onslide<2->{\bl{matches$_1$ x$\cdot$(0$|$1)$^*\;$ x}   & \bl{$\mapsto$} & \bl{true}}\\
       
   565   \onslide<2->{\bl{matches$_1$ x$\cdot$(0$|$1)$^*\;$ x0}  & \bl{$\mapsto$} & \bl{true}}\\
       
   566   \onslide<2->{\bl{matches$_1$ x$\cdot$(0$|$1)$^*\;$ x3}  & \bl{$\mapsto$} & \bl{false}}
       
   567   \end{tabular}
       
   568   \end{center}
       
   569  
       
   570   \onslide<3->
       
   571   {Looks OK \ldots let's ship it to customers\hspace{5mm} 
       
   572    \raisebox{-5mm}{\includegraphics[scale=0.05]{sun.png}}}
       
   573   
       
   574   \end{frame}}
       
   575   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
       
   576 *}
       
   577 
       
   578 text_raw {*
       
   579   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
   580   \mode<presentation>{
       
   581   \begin{frame}<1->[c]
       
   582   \frametitle{Version 1}
       
   583 
       
   584   \only<1->{Several hours later\ldots}\pause
       
   585 
       
   586 
       
   587   \begin{center}
       
   588   \begin{tabular}{@ {\hspace{0mm}}lcl}
       
   589   \bl{matches$_1$ []$^*$ s}     & \bl{$\mapsto$} & loops\\
       
   590   \onslide<4->{\bl{matches$_1$ ([] + \ldots)$^*$ s}   & \bl{$\mapsto$} & loops\\} 
       
   591   \end{tabular}
       
   592   \end{center}
       
   593 
       
   594   \small
       
   595   \onslide<3->{
       
   596   \begin{center}
       
   597   \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {}}
       
   598   \ldots\\
       
   599   \bl{match ([]::rs) s}           & \bl{$=$} & \bl{match rs s}\\
       
   600   \ldots\\
       
   601   \bl{match (r$^*$::rs) s}        & \bl{$=$} & \bl{match rs s $\vee$ match (r::r$^*$::rs) s}\\
       
   602   \end{tabular}
       
   603   \end{center}}
       
   604   
       
   605 
       
   606   \end{frame}}
       
   607   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
       
   608 *}
       
   609 
       
   610 
       
   611 text_raw {*
       
   612   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
   613   \mode<presentation>{
       
   614   \begin{frame}<1->[c]
       
   615   \frametitle{Testing}
       
   616 
       
   617   \begin{itemize}
       
   618   \item We can only test a {\bf finite} amount of examples:\bigskip
       
   619 
       
   620   \begin{center}
       
   621   \colorbox{cream}
       
   622   {\gr{\begin{minipage}{10cm}
       
   623   ``Testing can only show the presence of errors, never their
       
   624   absence.'' (Edsger W.~Dijkstra)
       
   625   \end{minipage}}}
       
   626   \end{center}\bigskip\pause
       
   627 
       
   628   \item In a theorem prover we can establish properties that apply to 
       
   629   {\bf all} input and {\bf all} output. 
       
   630 
       
   631   \end{itemize}
       
   632 
       
   633   \end{frame}}
       
   634   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
       
   635 *}
       
   636 
       
   637 
       
   638 text_raw {*
       
   639   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
   640   \mode<presentation>{
       
   641   \begin{frame}<1->[t]
       
   642   \frametitle{Version 2}
       
   643   \mbox{}\\[-14mm]\mbox{}
       
   644 
       
   645   \small
       
   646   \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}ll@ {}}
       
   647   \bl{nullable ($\varnothing$)}   & \bl{$=$} & \bl{false} &\\
       
   648   \bl{nullable ([])}              & \bl{$=$} & \bl{true}  &\\
       
   649   \bl{nullable (c)}               & \bl{$=$} & \bl{false} &\\
       
   650   \bl{nullable (r$_1$ + r$_2$)}   & \bl{$=$} & \bl{nullable r$_1$ $\vee$ nullable r$_2$} & \\ 
       
   651   \bl{nullable (r$_1$ $\cdot$ r$_2$)} & \bl{$=$} & \bl{nullable r$_1$ $\wedge$ nullable r$_2$} & \\
       
   652   \bl{nullable (r$^*$)}           & \bl{$=$} & \bl{true} & \\
       
   653   \end{tabular}\medskip
       
   654 
       
   655   \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{-10mm}}l@ {}}
       
   656   \bl{der c ($\varnothing$)}       & \bl{$=$} & \bl{$\varnothing$} & \\
       
   657   \bl{der c ([])}                  & \bl{$=$} & \bl{$\varnothing$} & \\
       
   658   \bl{der c (d)}                   & \bl{$=$} & \bl{if c = d then [] else $\varnothing$} & \\
       
   659   \bl{der c (r$_1$ + r$_2$)}       & \bl{$=$} & \bl{(der c r$_1$) + (der c r$_2$)} & \\
       
   660   \bl{der c (r$_1$ $\cdot$ r$_2$)} & \bl{$=$} & \bl{((der c r$_1$) $\cdot$ r$_2$)} & \\
       
   661        &          & \bl{\;\;\;\;+ (if nullable r$_1$ then der c r$_2$ else $\varnothing$)}\\
       
   662   \bl{der c (r$^*$)}          & \bl{$=$} & \bl{(der c r) $\cdot$ r$^*$} &\smallskip\\
       
   663 
       
   664   \bl{derivative r []}     & \bl{$=$} & \bl{r} & \\
       
   665   \bl{derivative r (c::s)} & \bl{$=$} & \bl{derivative (der c r) s} & \\
       
   666   \end{tabular}\medskip
       
   667 
       
   668   \bl{matches$_2$ r s $=$ nullable (derivative r s)}
       
   669 
       
   670   \begin{textblock}{6}(9.5,0.9)
       
   671   \begin{flushright}
       
   672   \color{gray}``if r matches []'' 
       
   673   \end{flushright}
       
   674   \end{textblock}
       
   675 
       
   676   \begin{textblock}{6}(9.5,6.18)
       
   677   \begin{flushright}
       
   678   \color{gray}``derivative w.r.t.~a char'' 
       
   679   \end{flushright}
       
   680   \end{textblock}
       
   681 
       
   682   \begin{textblock}{6}(9.5,12.1)
       
   683   \begin{flushright}
       
   684   \color{gray}``deriv.~w.r.t.~a string'' 
       
   685   \end{flushright}
       
   686   \end{textblock}
       
   687 
       
   688   \begin{textblock}{6}(9.5,13.98)
       
   689   \begin{flushright}
       
   690   \color{gray}``main'' 
       
   691   \end{flushright}
       
   692   \end{textblock}
       
   693 
       
   694   \end{frame}}
       
   695   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
       
   696 *}
       
   697 
       
   698 text_raw {*
       
   699   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
   700   \mode<presentation>{
       
   701   \begin{frame}<1->[t]
       
   702   \frametitle{Is the Matcher Error-Free?}
       
   703 
       
   704   We expect that
       
   705 
       
   706   \begin{center}
       
   707   \begin{tabular}{lcl}
       
   708   \bl{matches$_2$ r s = true}  & \only<1>{\rd{$\Longrightarrow\,\,$}}\only<2>{\rd{$\Longleftarrow\,\,$}}% 
       
   709   \only<3->{\rd{$\Longleftrightarrow$}} & \bl{s $\in$ \LL(r)}\\
       
   710   \bl{matches$_2$ r s = false} & \only<1>{\rd{$\Longrightarrow\,\,$}}\only<2>{\rd{$\Longleftarrow\,\,$}}%
       
   711   \only<3->{\rd{$\Longleftrightarrow$}} & \bl{s $\notin$ \LL(r)}\\
       
   712   \end{tabular}
       
   713   \end{center}
       
   714   \pause\pause\bigskip
       
   715   By \alert<4->{induction}, we can {\bf prove} these properties.\bigskip
       
   716 
       
   717   \begin{tabular}{lrcl}
       
   718   Lemmas:  & \bl{nullable (r)}          & \bl{$\Longleftrightarrow$} & \bl{[] $\in$ \LL (r)}\\
       
   719            & \bl{s $\in$ \LL (der c r)} & \bl{$\Longleftrightarrow$} & \bl{(c::s) $\in$ \LL (r)}\\
       
   720   \end{tabular}
       
   721   
       
   722   \only<4->{
       
   723   \begin{textblock}{3}(0.9,4.5)
       
   724   \rd{\huge$\forall$\large{}r s.}
       
   725   \end{textblock}}
       
   726   \end{frame}}
       
   727   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
       
   728 *}
       
   729 
       
   730 text_raw {*
       
   731   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
   732   \mode<presentation>{
       
   733   \begin{frame}<1>[c]
       
   734   \frametitle{
       
   735   \begin{tabular}{c}
       
   736   \mbox{}\\[23mm]
       
   737   \LARGE Demo
       
   738   \end{tabular}}
       
   739   
       
   740   \end{frame}}
       
   741   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
       
   742 *}
       
   743 
       
   744 
       
   745 text_raw {*
       
   746   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
   747   \mode<presentation>{
       
   748   \begin{frame}<1->[t]
       
   749 
       
   750   \mbox{}\\[-2mm]
       
   751 
       
   752   \small
       
   753   \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}ll@ {}}
       
   754   \bl{nullable (NULL)}            & \bl{$=$} & \bl{false} &\\
       
   755   \bl{nullable (EMPTY)}           & \bl{$=$} & \bl{true}  &\\
       
   756   \bl{nullable (CHR c)}           & \bl{$=$} & \bl{false} &\\
       
   757   \bl{nullable (ALT r$_1$ r$_2$)} & \bl{$=$} & \bl{(nullable r$_1$) orelse (nullable r$_2$)} & \\ 
       
   758   \bl{nullable (SEQ r$_1$ r$_2$)} & \bl{$=$} & \bl{(nullable r$_1$) andalso (nullable r$_2$)} & \\
       
   759   \bl{nullable (STAR r)}          & \bl{$=$} & \bl{true} & \\
       
   760   \end{tabular}\medskip
       
   761 
       
   762   \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{-10mm}}l@ {}}
       
   763   \bl{der c (NULL)}            & \bl{$=$} & \bl{NULL} & \\
       
   764   \bl{der c (EMPTY)}           & \bl{$=$} & \bl{NULL} & \\
       
   765   \bl{der c (CHR d)}           & \bl{$=$} & \bl{if c=d then EMPTY else NULL} & \\
       
   766   \bl{der c (ALT r$_1$ r$_2$)} & \bl{$=$} & \bl{ALT (der c r$_1$) (der c r$_2$)} & \\
       
   767   \bl{der c (SEQ r$_1$ r$_2$)} & \bl{$=$} & \bl{ALT (SEQ (der c r$_1$) r$_2$)} & \\
       
   768        &          & \bl{\phantom{ALT} (if nullable r$_1$ then der c r$_2$ else NULL)}\\
       
   769   \bl{der c (STAR r)}          & \bl{$=$} & \bl{SEQ (der c r) (STAR r)} &\smallskip\\
       
   770 
       
   771   \bl{derivative r []}     & \bl{$=$} & \bl{r} & \\
       
   772   \bl{derivative r (c::s)} & \bl{$=$} & \bl{derivative (der c r) s} & \\
       
   773   \end{tabular}\medskip
       
   774 
       
   775   \bl{matches r s $=$ nullable (derivative r s)}
       
   776   
       
   777   \only<2>{
       
   778   \begin{textblock}{8}(1.5,4)
       
   779   \includegraphics[scale=0.3]{approved.png}
       
   780   \end{textblock}}
       
   781   
       
   782   \end{frame}}
       
   783   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
       
   784 *}
       
   785 
       
   786 
       
   787 text_raw {*
       
   788   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
   789   \mode<presentation>{
       
   790   \begin{frame}[c]
       
   791   \frametitle{No Automata?}
       
   792 
       
   793   You might be wondering why I did not use any automata?
       
   794 
       
   795   \begin{itemize}
       
   796   \item {\bf Def.:} A \alert{regular language} is one where there is a DFA that 
       
   797   recognises it.\bigskip\pause
       
   798   \end{itemize}
       
   799 
       
   800 
       
   801   There are many reasons why this is a good definition:\medskip
       
   802   \begin{itemize}
       
   803   \item pumping lemma
       
   804   \item closure properties of regular languages\\ (e.g.~closure under complement)
       
   805   \end{itemize}
       
   806 
       
   807   \end{frame}}
       
   808   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
       
   809 
       
   810 *}
       
   811 
       
   812 text_raw {*
       
   813   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
   814   \mode<presentation>{
       
   815   \begin{frame}[t]
       
   816   \frametitle{Really Bad News!}
       
   817 
       
   818   DFAs are bad news for formalisations in theorem provers. They might
       
   819   be represented as:
       
   820 
       
   821   \begin{itemize}
       
   822   \item graphs
       
   823   \item matrices
       
   824   \item partial functions
       
   825   \end{itemize}
       
   826 
       
   827   All constructions are messy to reason about.\bigskip\bigskip 
       
   828   \pause
       
   829 
       
   830   \small
       
   831   \only<2>{
       
   832   Constable et al needed (on and off) 18 months for a 3-person team 
       
   833   to formalise automata theory in Nuprl including Myhill-Nerode. There is 
       
   834   only very little other formalised work on regular languages I know of
       
   835   in Coq, Isabelle and HOL.}
       
   836   \only<3>{Typical textbook reasoning goes like: ``\ldots if \smath{M} and \smath{N} are any two
       
   837   automata with no inaccessible states \ldots''
       
   838   }
       
   839   
       
   840   \end{frame}}
       
   841   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
       
   842 
       
   843 *}
       
   844 
       
   845 text_raw {*
       
   846   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
   847   \mode<presentation>{
       
   848   \begin{frame}[c]
       
   849   \frametitle{}
       
   850   \large
       
   851   \begin{center}
       
   852   \begin{tabular}{p{9cm}}
       
   853   My point:\bigskip\\
       
   854 
       
   855   The theory about regular languages can be reformulated 
       
   856   to be more\\ suitable for theorem proving.
       
   857   \end{tabular}
       
   858   \end{center}
       
   859   \end{frame}}
       
   860   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
       
   861 *}
       
   862 
       
   863 text_raw {*
       
   864   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
   865   \mode<presentation>{
       
   866   \begin{frame}[c]
       
   867   \frametitle{\LARGE The Myhill-Nerode Theorem}
       
   868 
       
   869   \begin{itemize}
       
   870   \item provides necessary and suf\!ficient conditions for a language 
       
   871   being regular (pumping lemma only necessary)\medskip
       
   872 
       
   873   \item will help with closure properties of regular languages\bigskip\pause
       
   874 
       
   875   \item key is the equivalence relation:\smallskip
       
   876   \begin{center}
       
   877   \smath{x \approx_{L} y \,\dn\, \forall z.\; x @ z \in L \Leftrightarrow y @ z \in L}
       
   878   \end{center}
       
   879   \end{itemize}
       
   880 
       
   881   \end{frame}}
       
   882   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
       
   883 *}
       
   884 
       
   885 text_raw {*
       
   886   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
   887   \mode<presentation>{
       
   888   \begin{frame}[c]
       
   889   \frametitle{\LARGE The Myhill-Nerode Theorem}
       
   890 
       
   891   \mbox{}\\[5cm]
       
   892 
       
   893   \begin{itemize}
       
   894   \item \smath{\text{finite}\, (U\!N\!IV /\!/ \approx_L) \;\Leftrightarrow\; L\; \text{is regular}}
       
   895   \end{itemize}
       
   896 
       
   897   \end{frame}}
       
   898   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
       
   899 
       
   900 *}
       
   901 
       
   902 text_raw {*
       
   903   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
   904   \mode<presentation>{
       
   905   \begin{frame}[c]
       
   906   \frametitle{\LARGE Equivalence Classes}
       
   907 
       
   908   \begin{itemize}
       
   909   \item \smath{L = []}
       
   910   \begin{center}
       
   911   \smath{\Big\{\{[]\},\; U\!N\!IV - \{[]\}\Big\}}
       
   912   \end{center}\bigskip\bigskip
       
   913 
       
   914   \item \smath{L = [c]}
       
   915   \begin{center}
       
   916   \smath{\Big\{\{[]\},\; \{[c]\},\; U\!N\!IV - \{[], [c]\}\Big\}}
       
   917   \end{center}\bigskip\bigskip
       
   918 
       
   919   \item \smath{L = \varnothing}
       
   920   \begin{center}
       
   921   \smath{\Big\{U\!N\!IV\Big\}}
       
   922   \end{center}
       
   923 
       
   924   \end{itemize}
       
   925 
       
   926   \end{frame}}
       
   927   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
       
   928 
       
   929 *}
       
   930 
       
   931 text_raw {*
       
   932   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
   933   \mode<presentation>{
       
   934   \begin{frame}[c]
       
   935   \frametitle{\LARGE Regular Languages}
       
   936 
       
   937   \begin{itemize}
       
   938   \item \smath{L} is regular \smath{\dn} if there is an automaton \smath{M} 
       
   939   such that \smath{\mathbb{L}(M) = L}\\[1.5cm]
       
   940 
       
   941   \item Myhill-Nerode:
       
   942 
       
   943   \begin{center}
       
   944   \begin{tabular}{l}
       
   945   finite $\Rightarrow$ regular\\
       
   946   \;\;\;\smath{\text{finite}\,(U\!N\!IV /\!/ \approx_L) \Rightarrow \exists r.\; L = \mathbb{L}(r)}\\[3mm]
       
   947   regular $\Rightarrow$ finite\\
       
   948   \;\;\;\smath{\text{finite}\, (U\!N\!IV /\!/ \approx_{\mathbb{L}(r)})}
       
   949   \end{tabular}
       
   950   \end{center}
       
   951 
       
   952   \end{itemize}
       
   953 
       
   954   \end{frame}}
       
   955   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
       
   956 
       
   957 *}
       
   958 
       
   959 text_raw {*
       
   960   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
   961   \mode<presentation>{
       
   962   \begin{frame}[c]
       
   963   \frametitle{\LARGE Final Equiv.~Classes}
       
   964 
       
   965   \mbox{}\\[3cm]
       
   966 
       
   967   \begin{itemize}
       
   968   \item \smath{\text{finals}\,L \dn 
       
   969      \{{\lbrack\mkern-2mu\lbrack{s}\rbrack\mkern-2mu\rbrack}_\approx\;|\; s \in L\}}\\
       
   970   \medskip
       
   971 
       
   972   \item we can prove: \smath{L = \bigcup (\text{finals}\,L)}
       
   973 
       
   974   \end{itemize}
       
   975 
       
   976   \end{frame}}
       
   977   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
       
   978 *}
       
   979 
       
   980 text_raw {*
       
   981   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
   982   \mode<presentation>{
       
   983   \begin{frame}[c]
       
   984   \frametitle{\LARGE Transitions between ECs}
       
   985 
       
   986   \smath{L = \{[c]\}}
       
   987 
       
   988   \begin{tabular}{@ {\hspace{-7mm}}cc}
       
   989   \begin{tabular}{c}
       
   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]   (q_0)                        {$R_1$};
       
   996   \node[state,accepting] (q_1) [above right of=q_0]   {$R_2$};
       
   997   \node[state]           (q_2) [below right of=q_0]   {$R_3$};
       
   998 
       
   999   \path[->] (q_0) edge                node        {c} (q_1)
       
  1000                   edge                node [swap] {$\Sigma-{c}$} (q_2)
       
  1001             (q_2) edge [loop below]   node        {$\Sigma$} ()
       
  1002             (q_1) edge                node        {$\Sigma$} (q_2);
       
  1003   \end{tikzpicture}
       
  1004   \end{tabular}
       
  1005   &
       
  1006   \begin{tabular}[t]{ll}
       
  1007   \\[-20mm]
       
  1008   \multicolumn{2}{l}{\smath{U\!N\!IV /\!/\approx_L} produces}\\[4mm]
       
  1009 
       
  1010   \smath{R_1}: & \smath{\{[]\}}\\
       
  1011   \smath{R_2}: & \smath{\{[c]\}}\\
       
  1012   \smath{R_3}: & \smath{U\!N\!IV - \{[], [c]\}}\\[6mm]
       
  1013   \multicolumn{2}{l}{\onslide<2->{\smath{X \stackrel{c}{\longrightarrow} Y \dn X ;; [c] \subseteq Y}}}
       
  1014   \end{tabular}
       
  1015 
       
  1016   \end{tabular}
       
  1017 
       
  1018   \end{frame}}
       
  1019   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
       
  1020 *}
       
  1021 
       
  1022 
       
  1023 text_raw {*
       
  1024   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
  1025   \mode<presentation>{
       
  1026   \begin{frame}[c]
       
  1027   \frametitle{\LARGE Systems of Equations}
       
  1028 
       
  1029   Inspired by a method of Brzozowski\;'64, we can build an equational system
       
  1030   characterising the equivalence classes:
       
  1031 
       
  1032   \begin{center}
       
  1033   \begin{tabular}{@ {\hspace{-20mm}}c}
       
  1034   \\[-13mm]
       
  1035   \begin{tikzpicture}[shorten >=1pt,node distance=2cm,auto, ultra thick]
       
  1036   \tikzstyle{state}=[circle,thick,draw=blue!75,fill=blue!20,minimum size=0mm]
       
  1037 
       
  1038   %\draw[help lines] (0,0) grid (3,2);
       
  1039 
       
  1040   \node[state,initial]   (p_0)                  {$R_1$};
       
  1041   \node[state,accepting] (p_1) [right of=q_0]   {$R_2$};
       
  1042 
       
  1043   \path[->] (p_0) edge [bend left]   node        {a} (p_1)
       
  1044                   edge [loop above]   node       {b} ()
       
  1045             (p_1) edge [loop above]   node       {a} ()
       
  1046                   edge [bend left]   node        {b} (p_0);
       
  1047   \end{tikzpicture}\\
       
  1048   \\[-13mm]
       
  1049   \end{tabular}
       
  1050   \end{center}
       
  1051 
       
  1052   \begin{center}
       
  1053   \begin{tabular}{@ {\hspace{-6mm}}ll@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
       
  1054   & \smath{R_1} & \smath{\equiv} & \smath{R_1;b + R_2;b \onslide<2->{\alert<2>{+ \lambda;[]}}}\\
       
  1055   & \smath{R_2} & \smath{\equiv} & \smath{R_1;a + R_2;a}\medskip\\
       
  1056   \onslide<3->{we can prove} 
       
  1057   & \onslide<3->{\smath{R_1}} & \onslide<3->{\smath{=}} 
       
  1058       & \onslide<3->{\smath{R_1;; \mathbb{L}(b) \,\cup\, R_2;;\mathbb{L}(b) \,\cup\, \{[]\}}}\\
       
  1059   & \onslide<3->{\smath{R_2}} & \onslide<3->{\smath{=}}    
       
  1060       & \onslide<3->{\smath{R_1;; \mathbb{L}(a) \,\cup\, R_2;;\mathbb{L}(a)}}\\
       
  1061   \end{tabular}
       
  1062   \end{center}
       
  1063 
       
  1064   \end{frame}}
       
  1065   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
       
  1066 *}
       
  1067 
       
  1068 
       
  1069 text_raw {*
       
  1070   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
  1071   \mode<presentation>{
       
  1072   \begin{frame}<1>[t]
       
  1073   \small
       
  1074 
       
  1075   \begin{center}
       
  1076   \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}ll}
       
  1077   \onslide<1->{\smath{R_1}} & \onslide<1->{\smath{=}} 
       
  1078       & \onslide<1->{\smath{R_1; b + R_2; b + \lambda;[]}}\\
       
  1079   \onslide<1->{\smath{R_2}} & \onslide<1->{\smath{=}}    
       
  1080       & \onslide<1->{\smath{R_1; a + R_2; a}}\\
       
  1081 
       
  1082   & & & \onslide<2->{by Arden}\\
       
  1083 
       
  1084   \onslide<2->{\smath{R_1}} & \onslide<2->{\smath{=}} 
       
  1085       & \onslide<2->{\smath{R_1; b + R_2; b + \lambda;[]}}\\
       
  1086   \onslide<2->{\smath{R_2}} & \onslide<2->{\smath{=}}    
       
  1087       & \only<2>{\smath{R_1; a + R_2; a}}%
       
  1088         \only<3->{\smath{R_1; a\cdot a^\star}}\\
       
  1089 
       
  1090   & & & \onslide<4->{by Arden}\\
       
  1091 
       
  1092   \onslide<4->{\smath{R_1}} & \onslide<4->{\smath{=}} 
       
  1093       & \onslide<4->{\smath{R_2; b \cdot b^\star+ \lambda;b^\star}}\\
       
  1094   \onslide<4->{\smath{R_2}} & \onslide<4->{\smath{=}}    
       
  1095       & \onslide<4->{\smath{R_1; a\cdot a^\star}}\\
       
  1096 
       
  1097   & & & \onslide<5->{by substitution}\\
       
  1098 
       
  1099   \onslide<5->{\smath{R_1}} & \onslide<5->{\smath{=}} 
       
  1100       & \onslide<5->{\smath{R_1; a\cdot a^\star \cdot b \cdot b^\star+ \lambda;b^\star}}\\
       
  1101   \onslide<5->{\smath{R_2}} & \onslide<5->{\smath{=}}    
       
  1102       & \onslide<5->{\smath{R_1; a\cdot a^\star}}\\
       
  1103 
       
  1104   & & & \onslide<6->{by Arden}\\
       
  1105 
       
  1106   \onslide<6->{\smath{R_1}} & \onslide<6->{\smath{=}} 
       
  1107       & \onslide<6->{\smath{\lambda;b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star}}\\
       
  1108   \onslide<6->{\smath{R_2}} & \onslide<6->{\smath{=}}    
       
  1109       & \onslide<6->{\smath{R_1; a\cdot a^\star}}\\
       
  1110 
       
  1111   & & & \onslide<7->{by substitution}\\
       
  1112 
       
  1113   \onslide<7->{\smath{R_1}} & \onslide<7->{\smath{=}} 
       
  1114       & \onslide<7->{\smath{\lambda;b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star}}\\
       
  1115   \onslide<7->{\smath{R_2}} & \onslide<7->{\smath{=}}    
       
  1116       & \onslide<7->{\smath{\lambda; b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star 
       
  1117           \cdot a\cdot a^\star}}\\
       
  1118   \end{tabular}
       
  1119   \end{center}
       
  1120 
       
  1121   \end{frame}}
       
  1122   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
       
  1123 *}
       
  1124 
       
  1125 text_raw {*
       
  1126   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
  1127   \mode<presentation>{
       
  1128   \begin{frame}[c]
       
  1129   \frametitle{\LARGE A Variant of Arden's Lemma}
       
  1130 
       
  1131   {\bf Arden's Lemma:}\smallskip 
       
  1132 
       
  1133   If \smath{[] \not\in A} then
       
  1134   \begin{center}
       
  1135   \smath{X = X; A + \text{something}}
       
  1136   \end{center}
       
  1137   has the (unique) solution
       
  1138   \begin{center}
       
  1139   \smath{X = \text{something} ; A^\star}
       
  1140   \end{center}
       
  1141 
       
  1142 
       
  1143   \end{frame}}
       
  1144   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
       
  1145 *}
       
  1146 
       
  1147 
       
  1148 text_raw {*
       
  1149   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
  1150   \mode<presentation>{
       
  1151   \begin{frame}<1->[t]
       
  1152   \small
       
  1153 
       
  1154   \begin{center}
       
  1155   \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}ll}
       
  1156   \onslide<1->{\smath{R_1}} & \onslide<1->{\smath{=}} 
       
  1157       & \onslide<1->{\smath{R_1; b + R_2; b + \lambda;[]}}\\
       
  1158   \onslide<1->{\smath{R_2}} & \onslide<1->{\smath{=}}    
       
  1159       & \onslide<1->{\smath{R_1; a + R_2; a}}\\
       
  1160 
       
  1161   & & & \onslide<2->{by Arden}\\
       
  1162 
       
  1163   \onslide<2->{\smath{R_1}} & \onslide<2->{\smath{=}} 
       
  1164       & \onslide<2->{\smath{R_1; b + R_2; b + \lambda;[]}}\\
       
  1165   \onslide<2->{\smath{R_2}} & \onslide<2->{\smath{=}}    
       
  1166       & \only<2>{\smath{R_1; a + R_2; a}}%
       
  1167         \only<3->{\smath{R_1; a\cdot a^\star}}\\
       
  1168 
       
  1169   & & & \onslide<4->{by Arden}\\
       
  1170 
       
  1171   \onslide<4->{\smath{R_1}} & \onslide<4->{\smath{=}} 
       
  1172       & \onslide<4->{\smath{R_2; b \cdot b^\star+ \lambda;b^\star}}\\
       
  1173   \onslide<4->{\smath{R_2}} & \onslide<4->{\smath{=}}    
       
  1174       & \onslide<4->{\smath{R_1; a\cdot a^\star}}\\
       
  1175 
       
  1176   & & & \onslide<5->{by substitution}\\
       
  1177 
       
  1178   \onslide<5->{\smath{R_1}} & \onslide<5->{\smath{=}} 
       
  1179       & \onslide<5->{\smath{R_1; a\cdot a^\star \cdot b \cdot b^\star+ \lambda;b^\star}}\\
       
  1180   \onslide<5->{\smath{R_2}} & \onslide<5->{\smath{=}}    
       
  1181       & \onslide<5->{\smath{R_1; a\cdot a^\star}}\\
       
  1182 
       
  1183   & & & \onslide<6->{by Arden}\\
       
  1184 
       
  1185   \onslide<6->{\smath{R_1}} & \onslide<6->{\smath{=}} 
       
  1186       & \onslide<6->{\smath{\lambda;b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star}}\\
       
  1187   \onslide<6->{\smath{R_2}} & \onslide<6->{\smath{=}}    
       
  1188       & \onslide<6->{\smath{R_1; a\cdot a^\star}}\\
       
  1189 
       
  1190   & & & \onslide<7->{by substitution}\\
       
  1191 
       
  1192   \onslide<7->{\smath{R_1}} & \onslide<7->{\smath{=}} 
       
  1193       & \onslide<7->{\smath{\lambda;b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star}}\\
       
  1194   \onslide<7->{\smath{R_2}} & \onslide<7->{\smath{=}}    
       
  1195       & \onslide<7->{\smath{\lambda; b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star 
       
  1196           \cdot a\cdot a^\star}}\\
       
  1197   \end{tabular}
       
  1198   \end{center}
       
  1199 
       
  1200   \only<8->{
       
  1201   \begin{textblock}{6}(2.5,4)
       
  1202   \begin{block}{}
       
  1203   \begin{minipage}{8cm}\raggedright
       
  1204   
       
  1205   \begin{tikzpicture}[shorten >=1pt,node distance=2cm,auto, ultra thick, inner sep=1mm]
       
  1206   \tikzstyle{state}=[circle,thick,draw=blue!75,fill=blue!20,minimum size=0mm]
       
  1207 
       
  1208   %\draw[help lines] (0,0) grid (3,2);
       
  1209 
       
  1210   \node[state,initial]   (p_0)                  {$R_1$};
       
  1211   \node[state,accepting] (p_1) [right of=q_0]   {$R_2$};
       
  1212 
       
  1213   \path[->] (p_0) edge [bend left]   node        {a} (p_1)
       
  1214                   edge [loop above]   node       {b} ()
       
  1215             (p_1) edge [loop above]   node       {a} ()
       
  1216                   edge [bend left]   node        {b} (p_0);
       
  1217   \end{tikzpicture}
       
  1218 
       
  1219   \end{minipage}
       
  1220   \end{block}
       
  1221   \end{textblock}}
       
  1222 
       
  1223   \end{frame}}
       
  1224   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
       
  1225 *}
       
  1226 
       
  1227 
       
  1228 text_raw {*
       
  1229   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
  1230   \mode<presentation>{
       
  1231   \begin{frame}[c]
       
  1232   \frametitle{\LARGE The Equ's Solving Algorithm}
       
  1233 
       
  1234   \begin{itemize}
       
  1235   \item The algorithm must terminate: Arden makes one equation smaller; 
       
  1236   substitution deletes one variable from the right-hand sides.\bigskip
       
  1237 
       
  1238   \item We need to maintain the invariant that Arden is applicable
       
  1239   (if \smath{[] \not\in A} then \ldots):\medskip
       
  1240 
       
  1241   \begin{center}\small
       
  1242   \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}ll}
       
  1243   \smath{R_1} & \smath{=} & \smath{R_1; b + R_2; b + \lambda;[]}\\
       
  1244   \smath{R_2} & \smath{=} & \smath{R_1; a + R_2; a}\\
       
  1245 
       
  1246   & & & by Arden\\
       
  1247 
       
  1248   \smath{R_1} & \smath{=} & \smath{R_1; b + R_2; b + \lambda;[]}\\
       
  1249   \smath{R_2} & \smath{=} & \smath{R_1; a\cdot a^\star}\\
       
  1250   \end{tabular}
       
  1251   \end{center}
       
  1252 
       
  1253   \end{itemize}
       
  1254 
       
  1255 
       
  1256   \end{frame}}
       
  1257   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
       
  1258 *}
       
  1259 
       
  1260 
       
  1261 
       
  1262 
       
  1263 text_raw {*
       
  1264   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
  1265   \mode<presentation>{
       
  1266   \begin{frame}[c]
       
  1267   \frametitle{\LARGE Other Direction}
       
  1268 
       
  1269   One has to prove
       
  1270 
       
  1271   \begin{center}
       
  1272   \smath{\text{finite} (U\!N\!IV /\!/ \approx_{\mathbb{L}(r)})}
       
  1273   \end{center}
       
  1274 
       
  1275   by induction on \smath{r}. Not trivial, but after a bit 
       
  1276   of thinking, one can prove that if
       
  1277 
       
  1278   \begin{center}
       
  1279   \smath{\text{finite} (U\!N\!IV /\!/ \approx_{\mathbb{L}(r_1)})}\hspace{5mm}
       
  1280   \smath{\text{finite} (U\!N\!IV /\!/ \approx_{\mathbb{L}(r_2)})}
       
  1281   \end{center}
       
  1282 
       
  1283   then
       
  1284 
       
  1285   \begin{center}
       
  1286   \smath{\text{finite} (U\!N\!IV /\!/ \approx_{\mathbb{L}(r_1) \,\cup\, \mathbb{L}(r_2)})}
       
  1287   \end{center}
       
  1288   
       
  1289   
       
  1290 
       
  1291   \end{frame}}
       
  1292   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
       
  1293 *}
       
  1294 
       
  1295 
       
  1296 
       
  1297 text_raw {*
       
  1298   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
  1299   \mode<presentation>{
       
  1300   \begin{frame}[c]
       
  1301   \frametitle{\LARGE What Have We Achieved?}
       
  1302 
       
  1303   \begin{itemize}
       
  1304   \item \smath{\text{finite}\, (U\!N\!IV /\!/ \approx_L) \;\Leftrightarrow\; L\; \text{is regular}}
       
  1305   \bigskip\pause
       
  1306   \item regular languages are closed under complementation; this is now easy\medskip
       
  1307   \begin{center}
       
  1308   \smath{U\!N\!IV /\!/ \approx_L \;\;=\;\; U\!N\!IV /\!/ \approx_{-L}}
       
  1309   \end{center}
       
  1310   \end{itemize}
       
  1311 
       
  1312   
       
  1313   \end{frame}}
       
  1314   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
       
  1315 *}
       
  1316 
       
  1317 text_raw {*
       
  1318   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
  1319   \mode<presentation>{
       
  1320   \begin{frame}[c]
       
  1321   \frametitle{\LARGE Examples}
       
  1322 
       
  1323   \begin{itemize}
       
  1324   \item \smath{L \equiv \Sigma^\star 0 \Sigma} is regular
       
  1325   \begin{quote}\small
       
  1326   \begin{tabular}{lcl}
       
  1327   \smath{A_1} & \smath{=} & \smath{\Sigma^\star 00}\\
       
  1328   \smath{A_2} & \smath{=} & \smath{\Sigma^\star 01}\\
       
  1329   \smath{A_3} & \smath{=} & \smath{\Sigma^\star 10 \cup \{0\}}\\
       
  1330   \smath{A_4} & \smath{=} & \smath{\Sigma^\star 11 \cup \{1\} \cup \{[]\}}\\
       
  1331   \end{tabular}
       
  1332   \end{quote}
       
  1333 
       
  1334   \item \smath{L \equiv \{ 0^n 1^n \,|\, n \ge 0\}} is not regular
       
  1335   \begin{quote}\small
       
  1336   \begin{tabular}{lcl}
       
  1337   \smath{B_0} & \smath{=} & \smath{\{0^n 1^n \,|\,     n \ge 0\}}\\
       
  1338   \smath{B_1} & \smath{=} & \smath{\{0^n 1^{(n-1)} \,|\, n \ge 1\}}\\
       
  1339   \smath{B_2} & \smath{=} & \smath{\{0^n 1^{(n-2)} \,|\, n \ge 2\}}\\
       
  1340   \smath{B_3} & \smath{=} & \smath{\{0^n 1^{(n-3)} \,|\, n \ge 3\}}\\
       
  1341               & \smath{\vdots} &\\
       
  1342   \end{tabular}
       
  1343   \end{quote}
       
  1344   \end{itemize}
       
  1345 
       
  1346   \end{frame}}
       
  1347   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
       
  1348 *}
       
  1349 
       
  1350 
       
  1351 text_raw {*
       
  1352   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
  1353   \mode<presentation>{
       
  1354   \begin{frame}[c]
       
  1355   \frametitle{\LARGE What We Have Not Achieved}
       
  1356 
       
  1357   \begin{itemize}
       
  1358   \item regular expressions are not good if you look for a minimal
       
  1359   one for a language (DFAs have this notion)\pause\bigskip
       
  1360 
       
  1361   \item Is there anything to be said about context free languages:\medskip
       
  1362   
       
  1363   \begin{quote}
       
  1364   A context free language is where every string can be recognised by
       
  1365   a pushdown automaton.\bigskip
       
  1366   \end{quote}
       
  1367   \end{itemize}
       
  1368 
       
  1369   \textcolor{gray}{\footnotesize Yes. Derivatives also work for c-f grammars. Ongoing work.}
       
  1370 
       
  1371   \end{frame}}
       
  1372   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
       
  1373 *}
       
  1374 
       
  1375 
       
  1376 text_raw {*
       
  1377   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
  1378   \mode<presentation>{
       
  1379   \begin{frame}[c]
       
  1380   \frametitle{\LARGE Conclusion}
       
  1381 
       
  1382   \begin{itemize}
       
  1383   \item We formalised the Myhill-Nerode theorem based on 
       
  1384   regular expressions only (DFAs are difficult to deal with in a theorem prover).\smallskip
       
  1385 
       
  1386   \item Seems to be a common theme: algorithms need to be reformulated
       
  1387   to better suit formal treatment.\smallskip
       
  1388 
       
  1389   \item The most interesting aspect is that we are able to
       
  1390   implement the matcher directly inside the theorem prover
       
  1391   (ongoing work).\smallskip
       
  1392 
       
  1393   \item Parsing is a vast field which seem to offer new results. 
       
  1394   \end{itemize}
       
  1395 
       
  1396   \end{frame}}
       
  1397   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
       
  1398 *}
       
  1399 
       
  1400 text_raw {*
       
  1401   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
  1402   \mode<presentation>{
       
  1403   \begin{frame}<1>[b]
       
  1404   \frametitle{
       
  1405   \begin{tabular}{c}
       
  1406   \mbox{}\\[13mm]
       
  1407   \alert{\LARGE Thank you very much!}\\
       
  1408   \alert{\Large Questions?}
       
  1409   \end{tabular}}
       
  1410 
       
  1411   \end{frame}}
       
  1412   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
  1413 *}
       
  1414 
       
  1415 
       
  1416 
       
  1417 (*<*)
       
  1418 end
       
  1419 (*>*)