Slides/Slides1.thy
changeset 213 dda2e90de8a2
parent 212 3629680a20a2
child 215 5709254e004f
equal deleted inserted replaced
212:3629680a20a2 213:dda2e90de8a2
    11 
    11 
    12 
    12 
    13 text_raw {*
    13 text_raw {*
    14   %\renewcommand{\slidecaption}{Cambridge, 9 November 2010}
    14   %\renewcommand{\slidecaption}{Cambridge, 9 November 2010}
    15   \renewcommand{\slidecaption}{Nijmegen, 25 August 2011}
    15   \renewcommand{\slidecaption}{Nijmegen, 25 August 2011}
    16   %%\renewcommand{\ULthickness}{2pt}
    16   \newcommand{\bl}[1]{#1}                        
    17   \newcommand{\sout}[1]{\tikz[baseline=(X.base), inner sep=0pt, outer sep=0pt]
    17   \newcommand{\sout}[1]{\tikz[baseline=(X.base), inner sep=-0.1pt, outer sep=0pt]
    18   \node [cross out,red, ultra thick, draw] (X) {\textcolor{black}{#1}};}
    18   \node [cross out,red, ultra thick, draw] (X) {\textcolor{black}{#1}};}
    19   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    19   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    20   \mode<presentation>{
    20   \mode<presentation>{
    21   \begin{frame}
    21   \begin{frame}
    22   \frametitle{%
    22   \frametitle{%
    57   \frametitle{}
    57   \frametitle{}
    58 
    58 
    59   \begin{textblock}{12.9}(1.5,3.2)
    59   \begin{textblock}{12.9}(1.5,3.2)
    60   \begin{block}{}
    60   \begin{block}{}
    61   \begin{minipage}{12.4cm}\raggedright
    61   \begin{minipage}{12.4cm}\raggedright
    62   \large I want to teach \alert{students} with\\ 
    62   \large I want to teach \alert{students} with
    63   theorem provers (especially inductions).
    63   theorem\\ provers (especially for inductions).
    64   \end{minipage}
    64   \end{minipage}
    65   \end{block}
    65   \end{block}
    66   \end{textblock}\pause
    66   \end{textblock}\pause
    67 
    67 
    68   \mbox{}\\[35mm]\mbox{}
    68   \mbox{}\\[35mm]\mbox{}
    69 
    69 
    70   \begin{itemize}
    70   \begin{itemize}
    71   \item \only<2>{\smath{\text{fib}}, \smath{\text{even}} and \smath{\text{odd}}}%
    71   \item \only<2>{\smath{\text{fib}}, \smath{\text{even}} and \smath{\text{odd}}}%
    72         \only<3->{\sout{\smath{\text{fib}}, \smath{\text{even}} and \smath{\text{odd}}}}\medskip
    72         \only<3->{\sout{\smath{\text{fib}}, \smath{\text{even}} and \smath{\text{odd}}}}\medskip
    73   \item<3-> formal language theory \\
    73   \item<3-> formal language theory \\
    74   \mbox{}\;\;@{text "\<Rightarrow>"} nice textbooks: Kozen, Hopcroft \& Ullman
    74   \mbox{}\;\;@{text "\<Rightarrow>"} nice textbooks: Kozen, Hopcroft \& Ullman\ldots
    75   \end{itemize}
    75   \end{itemize}
    76 
    76 
    77   \end{frame}}
    77   \end{frame}}
    78   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
    78   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
    79 
    79 
    90   \huge\bf\textcolor{gray}{in Nuprl}
    90   \huge\bf\textcolor{gray}{in Nuprl}
    91   \end{center}
    91   \end{center}
    92 
    92 
    93   \begin{itemize}
    93   \begin{itemize}
    94   \item Constable, Jackson, Naumov, Uribe\medskip
    94   \item Constable, Jackson, Naumov, Uribe\medskip
    95   \item \alert{18 months} for automata theory, Hopcroft \& Ullman chapters 1--11 (including Myhill-Nerode)
    95   \item \alert{18 months} for automata theory from Hopcroft \& Ullman chapters 1--11 (including Myhill-Nerode)
    96   \end{itemize}
    96   \end{itemize}
    97 
    97 
    98   \end{frame}}
    98   \end{frame}}
    99   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
    99   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
   100 
   100 
   213   \end{minipage}
   213   \end{minipage}
   214   \end{block}
   214   \end{block}
   215   \end{textblock}}
   215   \end{textblock}}
   216   \medskip
   216   \medskip
   217 
   217 
   218   \only<6->{A solution:\;\;\smath{\text{nat}} \;@{text "\<Rightarrow>"}\; state nodes\medskip}
   218   \only<6->{A solution:\;\;use \smath{\text{nat}} \;@{text "\<Rightarrow>"}\; state nodes\medskip}
   219 
   219 
   220   \only<7->{You have to \alert{\underline{rename}} states!}
   220   \only<7->{You have to \alert{\underline{rename}} states!}
   221 
   221 
   222   \end{frame}}
   222   \end{frame}}
   223   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
   223   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
   266   \end{block}
   266   \end{block}
   267   \end{textblock}\pause
   267   \end{textblock}\pause
   268   
   268   
   269   {\noindent\large\bf\alert{\ldots{}and forget about automata}}\bigskip\bigskip\pause
   269   {\noindent\large\bf\alert{\ldots{}and forget about automata}}\bigskip\bigskip\pause
   270 
   270 
   271   Infrastructure for free. Do we lose anything?\pause
   271   Infrastructure for free. But do we lose anything?\pause
   272   \begin{itemize}
   272   \begin{itemize}
   273   \item pumping lemma\pause
   273   \item pumping lemma\pause
   274   \item closure under complementation\pause
   274   \item closure under complementation\pause
   275   \item \only<6>{regular expression matching}%
   275   \item \only<6>{regular expression matching}%
   276        \only<7->{\sout{regular expression matching}}
   276        \only<7->{\sout{regular expression matching} \;\;(@{text "\<Rightarrow>"}Owens et al)}
   277   \item<8-> most textbooks are about automata
   277   \item<8-> most textbooks are about automata
   278   \end{itemize}
   278   \end{itemize}
   279 
   279 
   280   
   280   
   281   \end{frame}}
   281   \end{frame}}
   393   \draw[red, fill] (0.8, 0.4) rectangle (1.0, 0.6);}
   393   \draw[red, fill] (0.8, 0.4) rectangle (1.0, 0.6);}
   394   \end{tikzpicture}
   394   \end{tikzpicture}
   395   \end{center}
   395   \end{center}
   396 
   396 
   397   \begin{itemize}
   397   \begin{itemize}
   398   \item \smath{\text{final}_A\,X \dn \{[\!|x|\!]_{\approx_{A}}\;|\;x \in A\}}
   398   \item \smath{\text{finals}\,A\,\dn \{[\!|x|\!]_{\approx_{A}}\;|\;x \in A\}}
   399   \smallskip
   399   \smallskip
   400   \item we can prove: \smath{A = \bigcup \{X.\;\text{final}_A\,X\}}
   400   \item we can prove: \smath{A = \bigcup \text{finals}\,A}
   401   \end{itemize}
   401   \end{itemize}
   402 
   402 
   403   \only<2->{%
   403   \only<2->{%
   404   \begin{textblock}{5}(2.1,4.6)
   404   \begin{textblock}{5}(2.1,4.6)
   405   \begin{tikzpicture}
   405   \begin{tikzpicture}
   433   \draw[very thick] (0.5,0.5) circle (.6cm);
   433   \draw[very thick] (0.5,0.5) circle (.6cm);
   434   \clip[draw] (0.5,0.5) circle (.6cm);
   434   \clip[draw] (0.5,0.5) circle (.6cm);
   435   \draw[step=2mm, very thick] (-1.4,-1.4) grid (1.4,1.4);
   435   \draw[step=2mm, very thick] (-1.4,-1.4) grid (1.4,1.4);
   436   \draw[blue, fill] (0.0, 0.6) rectangle (0.2, 0.8);
   436   \draw[blue, fill] (0.0, 0.6) rectangle (0.2, 0.8);
   437   \draw[blue, fill] (0.8, 0.4) rectangle (1.0, 0.6);
   437   \draw[blue, fill] (0.8, 0.4) rectangle (1.0, 0.6);
   438   \draw[white] (0.1,0.7) node {$X$};
   438   \draw[white] (0.1,0.7) node (X) {$X$};
   439   \draw[white] (0.9,0.5) node {$Y$};
   439   \draw[white] (0.9,0.5) node (Y) {$Y$};
       
   440   \draw[blue, ->, line width = 2mm, bend left=45] (X) -- (Y);
       
   441   \node [inner sep=1pt,label=above:\textcolor{blue}{$c$}] at ($ (X)!.5!(Y) $) {};
   440   \end{tikzpicture}
   442   \end{tikzpicture}
   441   \end{center}
   443   \end{center}
   442 
   444 
   443   \begin{center}
   445   \begin{center}
   444   \smath{X \stackrel{c}{\longrightarrow} Y \;\dn\; X ; c \subseteq Y}
   446   \smath{X \stackrel{c}{\longrightarrow} Y \;\dn\; X ; c \subseteq Y}
   471   \begin{tikzpicture}[shorten >=1pt,node distance=2cm,auto, ultra thick]
   473   \begin{tikzpicture}[shorten >=1pt,node distance=2cm,auto, ultra thick]
   472   \tikzstyle{state}=[circle,thick,draw=blue!75,fill=blue!20,minimum size=0mm]
   474   \tikzstyle{state}=[circle,thick,draw=blue!75,fill=blue!20,minimum size=0mm]
   473 
   475 
   474   %\draw[help lines] (0,0) grid (3,2);
   476   %\draw[help lines] (0,0) grid (3,2);
   475 
   477 
   476   \node[state,initial]   (p_0)                  {$R_1$};
   478   \node[state,initial]   (p_0)                  {$X_1$};
   477   \node[state,accepting] (p_1) [right of=q_0]   {$R_2$};
   479   \node[state,accepting] (p_1) [right of=q_0]   {$X_2$};
   478 
   480 
   479   \path[->] (p_0) edge [bend left]   node        {a} (p_1)
   481   \path[->] (p_0) edge [bend left]   node        {a} (p_1)
   480                   edge [loop above]   node       {b} ()
   482                   edge [loop above]   node       {b} ()
   481             (p_1) edge [loop above]   node       {a} ()
   483             (p_1) edge [loop above]   node       {a} ()
   482                   edge [bend left]   node        {b} (p_0);
   484                   edge [bend left]   node        {b} (p_0);
   485   \end{tabular}
   487   \end{tabular}
   486   \end{center}
   488   \end{center}
   487 
   489 
   488   \begin{center}
   490   \begin{center}
   489   \begin{tabular}{@ {\hspace{-6mm}}ll@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
   491   \begin{tabular}{@ {\hspace{-6mm}}ll@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
   490   & \smath{R_1} & \smath{\equiv} & \smath{R_1;b + R_2;b \onslide<2->{\alert<2>{+ \lambda;[]}}}\\
   492   & \smath{X_1} & \smath{=} & \smath{X_1;b + X_2;b \onslide<2->{\alert<2>{+ \lambda;[]}}}\\
   491   & \smath{R_2} & \smath{\equiv} & \smath{R_1;a + R_2;a}\medskip\\
   493   & \smath{X_2} & \smath{=} & \smath{X_1;a + X_2;a}\medskip\\
   492   \end{tabular}
   494   \end{tabular}
   493   \end{center}
   495   \end{center}
   494 
   496 
   495   \end{frame}}
   497   \end{frame}}
   496   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
   498   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
   503   \begin{frame}<1-2,4->[t]
   505   \begin{frame}<1-2,4->[t]
   504   \small
   506   \small
   505 
   507 
   506   \begin{center}
   508   \begin{center}
   507   \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}ll}
   509   \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}ll}
   508   \onslide<1->{\smath{R_1}} & \onslide<1->{\smath{=}} 
   510   \onslide<1->{\smath{X_1}} & \onslide<1->{\smath{=}} 
   509       & \onslide<1->{\smath{R_1; b + R_2; b + \lambda;[]}}\\
   511       & \onslide<1->{\smath{X_1; b + X_2; b + \lambda;[]}}\\
   510   \onslide<1->{\smath{R_2}} & \onslide<1->{\smath{=}}    
   512   \onslide<1->{\smath{X_2}} & \onslide<1->{\smath{=}}    
   511       & \onslide<1->{\smath{R_1; a + R_2; a}}\\
   513       & \onslide<1->{\smath{X_1; a + X_2; a}}\\
   512 
   514 
   513   & & & \onslide<2->{by Arden}\\
   515   & & & \onslide<2->{by Arden}\\
   514 
   516 
   515   \onslide<2->{\smath{R_1}} & \onslide<2->{\smath{=}} 
   517   \onslide<2->{\smath{X_1}} & \onslide<2->{\smath{=}} 
   516       & \onslide<2->{\smath{R_1; b + R_2; b + \lambda;[]}}\\
   518       & \onslide<2->{\smath{X_1; b + X_2; b + \lambda;[]}}\\
   517   \onslide<2->{\smath{R_2}} & \onslide<2->{\smath{=}}    
   519   \onslide<2->{\smath{X_2}} & \onslide<2->{\smath{=}}    
   518       & \only<2->{\smath{R_1; a\cdot a^\star}}\\
   520       & \only<2->{\smath{X_1; a\cdot a^\star}}\\
   519 
   521 
   520   & & & \onslide<4->{by Arden}\\
   522   & & & \onslide<4->{by Arden}\\
   521 
   523 
   522   \onslide<4->{\smath{R_1}} & \onslide<4->{\smath{=}} 
   524   \onslide<4->{\smath{X_1}} & \onslide<4->{\smath{=}} 
   523       & \onslide<4->{\smath{R_2; b \cdot b^\star+ \lambda;b^\star}}\\
   525       & \onslide<4->{\smath{X_2; b \cdot b^\star+ \lambda;b^\star}}\\
   524   \onslide<4->{\smath{R_2}} & \onslide<4->{\smath{=}}    
   526   \onslide<4->{\smath{X_2}} & \onslide<4->{\smath{=}}    
   525       & \onslide<4->{\smath{R_1; a\cdot a^\star}}\\
   527       & \onslide<4->{\smath{X_1; a\cdot a^\star}}\\
   526 
   528 
   527   & & & \onslide<5->{by substitution}\\
   529   & & & \onslide<5->{by substitution}\\
   528 
   530 
   529   \onslide<5->{\smath{R_1}} & \onslide<5->{\smath{=}} 
   531   \onslide<5->{\smath{X_1}} & \onslide<5->{\smath{=}} 
   530       & \onslide<5->{\smath{R_1; a\cdot a^\star \cdot b \cdot b^\star+ \lambda;b^\star}}\\
   532       & \onslide<5->{\smath{X_1; a\cdot a^\star \cdot b \cdot b^\star+ \lambda;b^\star}}\\
   531   \onslide<5->{\smath{R_2}} & \onslide<5->{\smath{=}}    
   533   \onslide<5->{\smath{X_2}} & \onslide<5->{\smath{=}}    
   532       & \onslide<5->{\smath{R_1; a\cdot a^\star}}\\
   534       & \onslide<5->{\smath{X_1; a\cdot a^\star}}\\
   533 
   535 
   534   & & & \onslide<6->{by Arden}\\
   536   & & & \onslide<6->{by Arden}\\
   535 
   537 
   536   \onslide<6->{\smath{R_1}} & \onslide<6->{\smath{=}} 
   538   \onslide<6->{\smath{X_1}} & \onslide<6->{\smath{=}} 
   537       & \onslide<6->{\smath{\lambda;b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star}}\\
   539       & \onslide<6->{\smath{\lambda;b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star}}\\
   538   \onslide<6->{\smath{R_2}} & \onslide<6->{\smath{=}}    
   540   \onslide<6->{\smath{X_2}} & \onslide<6->{\smath{=}}    
   539       & \onslide<6->{\smath{R_1; a\cdot a^\star}}\\
   541       & \onslide<6->{\smath{X_1; a\cdot a^\star}}\\
   540 
   542 
   541   & & & \onslide<7->{by substitution}\\
   543   & & & \onslide<7->{by substitution}\\
   542 
   544 
   543   \onslide<7->{\smath{R_1}} & \onslide<7->{\smath{=}} 
   545   \onslide<7->{\smath{X_1}} & \onslide<7->{\smath{=}} 
   544       & \onslide<7->{\smath{\lambda;b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star}}\\
   546       & \onslide<7->{\smath{\lambda;b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star}}\\
   545   \onslide<7->{\smath{R_2}} & \onslide<7->{\smath{=}}    
   547   \onslide<7->{\smath{X_2}} & \onslide<7->{\smath{=}}    
   546       & \onslide<7->{\smath{\lambda; b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star 
   548       & \onslide<7->{\smath{\lambda; b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star 
   547           \cdot a\cdot a^\star}}\\
   549           \cdot a\cdot a^\star}}\\
   548   \end{tabular}
   550   \end{tabular}
   549   \end{center}
   551   \end{center}
   550 
   552 
   556   \begin{tikzpicture}[shorten >=1pt,node distance=2cm,auto, ultra thick, inner sep=1mm]
   558   \begin{tikzpicture}[shorten >=1pt,node distance=2cm,auto, ultra thick, inner sep=1mm]
   557   \tikzstyle{state}=[circle,thick,draw=blue!75,fill=blue!20,minimum size=0mm]
   559   \tikzstyle{state}=[circle,thick,draw=blue!75,fill=blue!20,minimum size=0mm]
   558 
   560 
   559   %\draw[help lines] (0,0) grid (3,2);
   561   %\draw[help lines] (0,0) grid (3,2);
   560 
   562 
   561   \node[state,initial]   (p_0)                  {$R_1$};
   563   \node[state,initial]   (p_0)                  {$X_1$};
   562   \node[state,accepting] (p_1) [right of=q_0]   {$R_2$};
   564   \node[state,accepting] (p_1) [right of=q_0]   {$X_2$};
   563 
   565 
   564   \path[->] (p_0) edge [bend left]   node        {a} (p_1)
   566   \path[->] (p_0) edge [bend left]   node        {a} (p_1)
   565                   edge [loop above]   node       {b} ()
   567                   edge [loop above]   node       {b} ()
   566             (p_1) edge [loop above]   node       {a} ()
   568             (p_1) edge [loop above]   node       {a} ()
   567                   edge [bend left]   node        {b} (p_0);
   569                   edge [bend left]   node        {b} (p_0);
   569 
   571 
   570   \end{minipage}
   572   \end{minipage}
   571   \end{block}
   573   \end{block}
   572   \end{textblock}}
   574   \end{textblock}}
   573 
   575 
   574   \end{frame}}
   576   \only<1,2>{%
   575   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
   577   \begin{textblock}{3}(0.6,1.2)
   576 *}
   578   \begin{tikzpicture}
   577 
   579   \node at (0,0) [single arrow, fill=red,text=white, minimum height=0cm]
   578 
   580   {\textcolor{red}{a}};
   579 text_raw {*
   581   \end{tikzpicture}
   580   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   582   \end{textblock}}
   581   \mode<presentation>{
   583   \only<2>{%
   582   \begin{frame}[c]
   584   \begin{textblock}{3}(0.6,3.6)
   583   \frametitle{\LARGE Other Direction}
   585   \begin{tikzpicture}
       
   586   \node at (0,0) [single arrow, fill=red,text=white, minimum height=0cm]
       
   587   {\textcolor{red}{a}};
       
   588   \end{tikzpicture}
       
   589   \end{textblock}}
       
   590   \only<4>{%
       
   591   \begin{textblock}{3}(0.6,2.9)
       
   592   \begin{tikzpicture}
       
   593   \node at (0,0) [single arrow, fill=red,text=white, minimum height=0cm]
       
   594   {\textcolor{red}{a}};
       
   595   \end{tikzpicture}
       
   596   \end{textblock}}
       
   597   \only<4>{%
       
   598   \begin{textblock}{3}(0.6,5.3)
       
   599   \begin{tikzpicture}
       
   600   \node at (0,0) [single arrow, fill=red,text=white, minimum height=0cm]
       
   601   {\textcolor{red}{a}};
       
   602   \end{tikzpicture}
       
   603   \end{textblock}}
       
   604   \only<5>{%
       
   605   \begin{textblock}{3}(1.0,5.6)
       
   606   \begin{tikzpicture}
       
   607   \node at (0,0) (A) {};
       
   608   \node at (0,1) (B) {};
       
   609   \draw[<-, line width=2mm, red] (B) to  (A);
       
   610   \end{tikzpicture}
       
   611   \end{textblock}}
       
   612   \only<5,6>{%
       
   613   \begin{textblock}{3}(0.6,7.7)
       
   614   \begin{tikzpicture}
       
   615   \node at (0,0) [single arrow, fill=red,text=white, minimum height=0cm]
       
   616   {\textcolor{red}{a}};
       
   617   \end{tikzpicture}
       
   618   \end{textblock}}
       
   619   \only<6>{%
       
   620   \begin{textblock}{3}(0.6,10.1)
       
   621   \begin{tikzpicture}
       
   622   \node at (0,0) [single arrow, fill=red,text=white, minimum height=0cm]
       
   623   {\textcolor{red}{a}};
       
   624   \end{tikzpicture}
       
   625   \end{textblock}}
       
   626   \only<7>{%
       
   627   \begin{textblock}{3}(1.0,10.3)
       
   628   \begin{tikzpicture}
       
   629   \node at (0,0) (A) {};
       
   630   \node at (0,1) (B) {};
       
   631   \draw[->, line width=2mm, red] (B) to  (A);
       
   632   \end{tikzpicture}
       
   633   \end{textblock}}
       
   634 
       
   635   \end{frame}}
       
   636   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
       
   637 *}
       
   638 
       
   639 
       
   640 text_raw {*
       
   641   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
   642   \mode<presentation>{
       
   643   \begin{frame}[c]
       
   644   \frametitle{\LARGE The Other Direction}
   584 
   645 
   585   One has to prove
   646   One has to prove
   586 
   647 
   587   \begin{center}
   648   \begin{center}
   588   \smath{\text{finite} (U\!N\!IV /\!/ \approx_{{\cal L}(r)})}
   649   \smath{\text{finite} (U\!N\!IV /\!/ \approx_{{\cal L}(r)})}
   622   \small\smath{U\!N\!IV /\!/ \approx_{{\cal L}(r)}} &
   683   \small\smath{U\!N\!IV /\!/ \approx_{{\cal L}(r)}} &
   623   \small\smath{U\!N\!IV /\!/ \alert{R}}
   684   \small\smath{U\!N\!IV /\!/ \alert{R}}
   624   \end{tabular}}
   685   \end{tabular}}
   625   \end{center}
   686   \end{center}
   626 
   687 
   627   
   688   \begin{textblock}{5}(9.8,2.6)
   628   
   689   \begin{tikzpicture}
   629 
   690   \node at (0,0) [shape border rotate=270,single arrow, fill=red,text=white, minimum height=0cm]{\textcolor{red}{a}};
   630   \end{frame}}
   691   \end{tikzpicture}
   631   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
   692   \end{textblock}
   632 *}
   693   
       
   694 
       
   695   \end{frame}}
       
   696   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
       
   697 *}
       
   698 
       
   699 text_raw {*
       
   700   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       
   701   \mode<presentation>{
       
   702   \begin{frame}[t]
       
   703   \frametitle{\LARGE Partial Derivatives}
       
   704 
       
   705   \begin{itemize}
       
   706   \item \ldots (set of) regular expressions after a string 
       
   707    has been parsed\\[10mm]
       
   708 
       
   709 
       
   710   \item \alt<1>{\smath{\text{pders x r \mbox{$=$} pders y r}}}
       
   711             {\smath{\underbrace{\text{pders x r \mbox{$=$} pders y r}}_{R_1}}} 
       
   712         refines \textcolor{blue}{x $\approx_{{\cal L}(\text{r})}$ y}\\[16mm]\pause
       
   713   \item \smath{\text{finite} (U\!N\!IV /\!/ R_1)} \bigskip\pause
       
   714   \item Therefore \smath{\text{finite} (U\!N\!IV /\!/ \approx_{{\cal L}(r)})}. Qed.
       
   715   \end{itemize}
       
   716   
       
   717   \only<2->{%
       
   718   \begin{textblock}{5}(3.8,8.3)
       
   719   \begin{tikzpicture}
       
   720   \node at (0,0) [shape border rotate=270,single arrow, fill=red,text=white, minimum height=0cm]{\textcolor{red}{a}};
       
   721   \draw (2.2,0) node {Antimirov '95};
       
   722   \end{tikzpicture}
       
   723   \end{textblock}}
       
   724 
       
   725   \end{frame}}
       
   726   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
       
   727 *}
       
   728 
       
   729 
   633 
   730 
   634 text_raw {*
   731 text_raw {*
   635   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   732   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   636   \mode<presentation>{
   733   \mode<presentation>{
   637   \begin{frame}[c]
   734   \begin{frame}[c]
   638   \frametitle{\LARGE What Have We Achieved?}
   735   \frametitle{\LARGE What Have We Achieved?}
   639 
   736 
   640   \begin{itemize}
   737   \begin{itemize}
   641   \item \smath{\text{finite}\, (U\!N\!IV /\!/ \approx_A) \;\Leftrightarrow\; A\; \text{is regular}}
   738   \item \smath{\text{finite}\, (U\!N\!IV /\!/ \approx_A) \;\Leftrightarrow\; A\; \text{is regular}}
   642   \bigskip\pause
   739   \bigskip\pause
   643   \item regular languages are closed under complementation; this is easy
   740   \item regular languages are closed under complementation; this is now easy
   644   \begin{center}
   741   \begin{center}
   645   \smath{U\!N\!IV /\!/ \approx_A \;\;=\;\; U\!N\!IV /\!/ \approx_{\overline{A}}}
   742   \smath{U\!N\!IV /\!/ \approx_A \;\;=\;\; U\!N\!IV /\!/ \approx_{\overline{A}}}
   646   \end{center}\pause\bigskip
   743   \end{center}\pause\bigskip
   647   
   744   
   648   \item non-regularity (\smath{a^nb^n})
   745   \item non-regularity (\smath{a^nb^n})
   649 
   746 
   650   \begin{quote}
   747   \begin{quote}
   651   \begin{minipage}{8.8cm}
   748   \begin{minipage}{8.8cm}
   652   \begin{block}{}
   749   \begin{block}{}
   653   \begin{minipage}{8.6cm}
   750   \begin{minipage}{8.6cm}
   654   If there exists a sufficiently large set \smath{B} (for example infinite), 
   751   If there exists a sufficiently large set \smath{B} (for example infinitely large), 
   655   such that
   752   such that
   656 
   753 
   657   \begin{center}
   754   \begin{center}
   658   \smath{\forall x,y \in B.\; x \not= y \;\Rightarrow\; x \not\approx_{A} y}. 
   755   \smath{\forall x,y \in B.\; x \not= y \;\Rightarrow\; x \not\approx_{A} y}. 
   659   \end{center}  
   756   \end{center}  
   661   then \smath{A} is not regular.
   758   then \smath{A} is not regular.
   662   \end{minipage}
   759   \end{minipage}
   663   \end{block}
   760   \end{block}
   664   \end{minipage}\medskip\pause
   761   \end{minipage}\medskip\pause
   665 
   762 
   666   \small(\smath{A \dn \bigcup_i a^i})
   763   \small(\smath{A \dn \bigcup_n a^n})
   667   \end{quote}
   764   \end{quote}
   668 
   765 
   669   \end{itemize}
   766   \end{itemize}
   670 
   767 
   671   \only<2>{
   768   \only<2>{
   698   \begin{itemize}
   795   \begin{itemize}
   699   \item first direction (790 loc)\\
   796   \item first direction (790 loc)\\
   700   \item second direction (400 / 390 loc)\pause
   797   \item second direction (400 / 390 loc)\pause
   701   \end{itemize}\smallskip
   798   \end{itemize}\smallskip
   702 
   799 
   703   \item I have \alert{\bf not} yet used it for teaching of undergraduates.\pause
   800   \item I have \alert{\bf not} yet used it in teaching for undergraduates.\pause
   704 
   801 
   705   \end{itemize}
   802   \end{itemize}
   706 
   803 
   707   \only<5->{
   804   \only<5->{
   708   \begin{textblock}{13.8}(1,4)
   805   \begin{textblock}{13.8}(1,4)
   709   \begin{block}{}\mbox{}\hspace{3mm}
   806   \begin{block}{}\mbox{}\hspace{3mm}
   710   \begin{minipage}{11cm}\raggedright
   807   \begin{minipage}{11cm}\raggedright
   711   \large 
   808   \large 
   712 
   809 
   713   {\bf Bold Claim }\alert{(not proved!)}\medskip
   810   {\bf Bold Claim: }\alert{(not proved!)}\medskip
   714 
   811 
   715   {\bf 95\%} of regular language theory can be done without
   812   {\bf 95\%} of regular language theory can be done without
   716   automata\medskip\\\ldots this is much more tasteful. ;o)
   813   automata!\medskip\\\ldots and this is much more tasteful ;o)
   717 
   814 
   718   \end{minipage}
   815   \end{minipage}
   719   \end{block}
   816   \end{block}
   720   \end{textblock}}
   817   \end{textblock}}
   721 
   818 
   724 *}
   821 *}
   725 
   822 
   726 text_raw {*
   823 text_raw {*
   727   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   824   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   728   \mode<presentation>{
   825   \mode<presentation>{
   729   \begin{frame}[c]
   826   \begin{frame}[b]
   730   \frametitle{\mbox{}\\[2cm]\textcolor{red}{Questions?}}
   827   \frametitle{\mbox{}\\[2cm]\textcolor{red}{Thank you!\\[5mm]Questions?}}
   731 
       
   732 
       
   733 
   828 
   734   \end{frame}}
   829   \end{frame}}
   735   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
   830   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
   736 *}
   831 *}
   737 
   832