(*<*)
theory Slides4
imports "~~/src/HOL/Library/LaTeXsugar"
begin
notation (latex output)
set ("_") and
Cons ("_::/_" [66,65] 65)
(*>*)
text_raw {*
\renewcommand{\slidecaption}{Edinburgh, 21 February 2012}
\newcommand{\bl}[1]{\textcolor{blue}{#1}}
\newcommand{\sout}[1]{\tikz[baseline=(X.base), inner sep=-0.1pt, outer sep=0pt]
\node [cross out,red, ultra thick, draw] (X) {\textcolor{black}{#1}};}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}
\frametitle{%
\begin{tabular}{@ {}c@ {}}
\LARGE Formalising\\[-3mm]
\LARGE Regular Language Theory\\[-3mm]
\LARGE with Regular Expressions,\\[-3mm]
\LARGE \alert<2>{Only}\\[0mm]
\end{tabular}}
\begin{center}
Christian Urban\\
\small King's College London
\end{center}\bigskip
\begin{center}
\small joint work with Chunhan Wu and Xingyuan Zhang from the PLA
University of Science and Technology in Nanjing
\end{center}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}<1->[c]
\frametitle{}
\mbox{}\\[-10mm]
\begin{itemize}
\item My background is in
\begin{itemize}
\item \normalsize theorem provers
\item \normalsize develop Nominal Isabelle
\end{itemize}\bigskip\bigskip
\item<1->to formalise and mechanically check proofs from
programming language research and TCS\bigskip
\item<2->our biggest success story \ldots
\end{itemize}
\only<1->{
\begin{textblock}{6}(10.9,3.5)
\includegraphics[scale=0.23]{isabelle1.png}
\end{textblock}}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{}
\begin{tabular}{c@ {\hspace{2mm}}c}
\\[6mm]
\begin{tabular}{c}
\includegraphics[scale=0.11]{harper.jpg}\\[-2mm]
{\footnotesize Bob Harper}\\[-2.5mm]
{\footnotesize (CMU)}
\end{tabular}
\begin{tabular}{c}
\includegraphics[scale=0.37]{pfenning.jpg}\\[-2mm]
{\footnotesize Frank Pfenning}\\[-2.5mm]
{\footnotesize (CMU)}
\end{tabular} &
\begin{tabular}{p{6cm}}
\raggedright
\color{gray}{published a proof in\\ {\bf ACM Transactions on Computational Logic}, 2005,
$\sim$31pp}
\end{tabular}\\
\pause
\\[0mm]
\begin{tabular}{c}
\includegraphics[scale=0.36]{appel.jpg}\\[-2mm]
{\footnotesize Andrew Appel}\\[-2.5mm]
{\footnotesize (Princeton)}
\end{tabular} &
\begin{tabular}{p{6cm}}
\raggedright
\color{gray}{relied on their proof in a\\ {\bf security} critical application}
\end{tabular}
\end{tabular}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text {*
\tikzstyle{every node}=[node distance=25mm,text height=1.5ex, text depth=.25ex]
\tikzstyle{node1}=[rectangle, minimum size=10mm, rounded corners=3mm, very thick,
draw=black!50, top color=white, bottom color=black!20]
\tikzstyle{node2}=[rectangle, minimum size=12mm, rounded corners=3mm, very thick,
draw=red!70, top color=white, bottom color=red!50!black!20]
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}<2->[squeeze]
\frametitle{}
\begin{columns}
\begin{column}{0.8\textwidth}
\begin{textblock}{0}(1,2)
\begin{tikzpicture}
\matrix[ampersand replacement=\&,column sep=7mm, row sep=5mm]
{ \&[-10mm]
\node (def1) [node1] {\large\hspace{1mm}Spec\hspace{1mm}\mbox{}}; \&
\node (proof1) [node1] {\large Proof}; \&
\node (alg1) [node1] {\large\hspace{1mm}Alg\hspace{1mm}\mbox{}}; \\
\onslide<4->{\node {\begin{tabular}{c}\small 1st\\[-2.5mm] \footnotesize solution\end{tabular}};} \&
\onslide<4->{\node (def2) [node2] {\large Spec$^\text{+ex}$};} \&
\onslide<4->{\node (proof2) [node1] {\large Proof};} \&
\onslide<4->{\node (alg2) [node1] {\large\hspace{1mm}Alg\hspace{1mm}\mbox{}};} \\
\onslide<5->{\node {\begin{tabular}{c}\small 2nd\\[-2.5mm] \footnotesize solution\end{tabular}};} \&
\onslide<5->{\node (def3) [node1] {\large\hspace{1mm}Spec\hspace{1mm}\mbox{}};} \&
\onslide<5->{\node (proof3) [node1] {\large Proof};} \&
\onslide<5->{\node (alg3) [node2] {\large Alg$^\text{-ex}$};} \\
\onslide<6->{\node {\begin{tabular}{c}\small 3rd\\[-2.5mm] \footnotesize solution\end{tabular}};} \&
\onslide<6->{\node (def4) [node1] {\large\hspace{1mm}Spec\hspace{1mm}\mbox{}};} \&
\onslide<6->{\node (proof4) [node2] {\large\hspace{1mm}Proof\hspace{1mm}};} \&
\onslide<6->{\node (alg4) [node1] {\large\hspace{1mm}Alg\hspace{1mm}\mbox{}};} \\
};
\draw[->,black!50,line width=2mm] (proof1) -- (def1);
\draw[->,black!50,line width=2mm] (proof1) -- (alg1);
\onslide<4->{\draw[->,black!50,line width=2mm] (proof2) -- (def2);}
\onslide<4->{\draw[->,black!50,line width=2mm] (proof2) -- (alg2);}
\onslide<5->{\draw[->,black!50,line width=2mm] (proof3) -- (def3);}
\onslide<5->{\draw[->,black!50,line width=2mm] (proof3) -- (alg3);}
\onslide<6->{\draw[->,black!50,line width=2mm] (proof4) -- (def4);}
\onslide<6->{\draw[->,black!50,line width=2mm] (proof4) -- (alg4);}
\onslide<3->{\draw[white,line width=1mm] (1.1,3.2) -- (0.9,2.85) -- (1.1,2.35) -- (0.9,2.0);}
\end{tikzpicture}
\end{textblock}
\end{column}
\end{columns}
\begin{textblock}{3}(12,3.6)
\onslide<4->{
\begin{tikzpicture}
\node at (0,0) [single arrow, shape border rotate=270, fill=red,text=white]{2h};
\end{tikzpicture}}
\end{textblock}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{}
\begin{itemize}
\item I also found fixable errors in my Ph.D.-thesis about cut-elimination
(examined by Henk Barendregt and Andy Pitts)
\item flaws in PIP (OS); a theorem without a shred of evidence (algorithms)
\end{itemize}\bigskip\bigskip
{\bf Conclusion:}\smallskip
Pencil-and-paper proofs in TCS are not foolproof,
not even expertproof.
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[t]
\frametitle{\begin{tabular}{@ {}c@ {}}
\large Nipkow about Teaching Proofs in TCS:\hspace{3cm}\mbox{}\\[-4mm]
\large \textcolor{red}{``London Underground Phenomenon''}\\[-18mm]\mbox{}
\end{tabular}}
\begin{center}
\begin{tabular}{ccc}
students & \;\;\raisebox{-8mm}{\includegraphics[scale=0.16]{gap.jpg}}\;\; & proofs
\end{tabular}
\end{center}
\small Scott Aaronson (Berkeley/MIT):\\[-7mm]\mbox{}
\begin{center}
\begin{block}{}
\color{gray}
\small
``I still remember having to grade hundreds of exams where the
students started out by assuming what had to be proved, or filled
page after page with gibberish in the hope that, somewhere in the
mess, they might accidentally have said something
correct. \ldots{}innumerable examples of ``parrot proofs'' ---
NP-completeness reductions done in the wrong direction, arguments
that look more like LSD trips than coherent chains of logic \ldots{}''
\end{block}
\end{center}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{}
\begin{itemize}
\item part of the problem is teaching the obvious\medskip
\begin{center}
\smath{\infer{A \vdash A}{}}
\end{center}\bigskip\bigskip
\item teach proofs, not logic
\item students having too little practice and no good literature for how to do proofs\\
\textcolor{gray}{\small(Velleman is too mathematics oriented)}
\bigskip\bigskip\pause
\item proof assistants lead to abundant practice because they are
addictive like video games (Nipkow, Pierce)\\
\textcolor{gray}{\small(in the past they were just frustrating, but they got much better)}
\end{itemize}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}<1->[t]
\frametitle{Regular Expressions}
\begin{textblock}{6}(2,4)
\begin{tabular}{@ {}rrl}
\bl{r} & \bl{$::=$} & \bl{$\varnothing$}\\
& \bl{$\mid$} & \bl{[]}\\
& \bl{$\mid$} & \bl{c}\\
& \bl{$\mid$} & \bl{r$_1$ $\cdot$ r$_2$}\\
& \bl{$\mid$} & \bl{r$_1$ + r$_2$}\\
& \bl{$\mid$} & \bl{r$^*$}\\
\end{tabular}
\end{textblock}
\begin{textblock}{6}(8,3.5)
\includegraphics[scale=0.35]{Screen1.png}
\end{textblock}
\begin{textblock}{6}(10.2,2.8)
\footnotesize Isabelle:
\end{textblock}
\begin{textblock}{6}(7,12)
\footnotesize\textcolor{gray}{students have seen them and can be motivated about them}
\end{textblock}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}<1->[t]
\mbox{}\\[-2mm]
\small
\begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}ll@ {}}
\bl{nullable (NULL)} & \bl{$=$} & \bl{false} &\\
\bl{nullable (EMPTY)} & \bl{$=$} & \bl{true} &\\
\bl{nullable (CHAR c)} & \bl{$=$} & \bl{false} &\\
\bl{nullable (ALT r$_1$ r$_2$)} & \bl{$=$} & \bl{(nullable r$_1$) $\vee$ (nullable r$_2$)} & \\
\bl{nullable (SEQ r$_1$ r$_2$)} & \bl{$=$} & \bl{(nullable r$_1$) $\wedge$ (nullable r$_2$)} & \\
\bl{nullable (STAR r)} & \bl{$=$} & \bl{true} & \\
\end{tabular}\medskip\pause
\begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{-10mm}}l@ {}}
\bl{der c (NULL)} & \bl{$=$} & \bl{NULL} & \\
\bl{der c (EMPTY)} & \bl{$=$} & \bl{NULL} & \\
\bl{der c (CHAR d)} & \bl{$=$} & \bl{if c $=$ d then EMPTY else NULL} & \\
\bl{der c (ALT r$_1$ r$_2$)} & \bl{$=$} & \bl{ALT (der c r$_1$) (der c r$_2$)} & \\
\bl{der c (SEQ r$_1$ r$_2$)} & \bl{$=$} & \bl{ALT (SEQ (der c r$_1$) r$_2$)} & \\
& & \bl{\phantom{ALT} (if nullable r$_1$ then der c r$_2$ else NULL)}\\
\bl{der c (STAR r)} & \bl{$=$} & \bl{SEQ (der c r) (STAR r)} &\smallskip\\\pause
\bl{derivative [] r} & \bl{$=$} & \bl{r} & \\
\bl{derivative (c::s) r} & \bl{$=$} & \bl{derivative s (der c r)} & \\
\end{tabular}\medskip
\bl{matches r s $=$ nullable (derivative s r)}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[t]
\frametitle{\normalsize Formal language theory\ldots\hfill\mbox{}}
\mbox{}\\[-15mm]\mbox{}
\begin{center}
\huge\bf\textcolor{gray}{in Theorem Provers}\\
\footnotesize\textcolor{gray}{e.g.~Isabelle, Coq, HOL4, \ldots}
\end{center}
\begin{itemize}
\item automata @{text "\<Rightarrow>"} graphs, matrices, functions
\item<2-> combining automata / graphs
\onslide<2->{
\begin{center}
\begin{tabular}{ccc}
\begin{tikzpicture}[scale=1]
%\draw[step=2mm] (-1,-1) grid (1,1);
\draw[rounded corners=1mm, very thick] (-1.0,-0.3) rectangle (-0.2,0.3);
\draw[rounded corners=1mm, very thick] ( 0.2,-0.3) rectangle ( 1.0,0.3);
\node (A) at (-1.0,0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
\node (B) at ( 0.2,0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
\node (C) at (-0.2, 0.13) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
\node (D) at (-0.2,-0.13) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
\node (E) at (1.0, 0.2) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
\node (F) at (1.0,-0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
\node (G) at (1.0,-0.2) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
\draw (-0.6,0.0) node {\small$A_1$};
\draw ( 0.6,0.0) node {\small$A_2$};
\end{tikzpicture}}
&
\onslide<3->{\raisebox{1.1mm}{\bf\Large$\;\Rightarrow\,$}}
&
\onslide<3->{\begin{tikzpicture}[scale=1]
%\draw[step=2mm] (-1,-1) grid (1,1);
\draw[rounded corners=1mm, very thick] (-1.0,-0.3) rectangle (-0.2,0.3);
\draw[rounded corners=1mm, very thick] ( 0.2,-0.3) rectangle ( 1.0,0.3);
\node (A) at (-1.0,0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
\node (B) at ( 0.2,0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
\node (C) at (-0.2, 0.13) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
\node (D) at (-0.2,-0.13) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
\node (E) at (1.0, 0.2) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
\node (F) at (1.0,-0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
\node (G) at (1.0,-0.2) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
\draw [very thick, red] (C) to [bend left=45] (B);
\draw [very thick, red] (D) to [bend right=45] (B);
\draw (-0.6,0.0) node {\small$A_1$};
\draw ( 0.6,0.0) node {\small$A_2$};
\end{tikzpicture}}
\end{tabular}
\end{center}\medskip
\only<4-5>{
\begin{tabular}{@ {\hspace{-5mm}}l@ {}}
disjoint union:\\[2mm]
\smath{A_1\uplus A_2 \dn \{(1, x)\,|\, x \in A_1\} \,\cup\, \{(2, y)\,|\, y \in A_2\}}
\end{tabular}}
\end{itemize}
\only<5>{
\begin{textblock}{13.9}(0.7,7.7)
\begin{block}{}
\medskip
\begin{minipage}{14cm}\raggedright
Problems with definition for regularity:\bigskip\\
\smath{\;\text{is\_regular}(A) \dn \exists M.\;\text{is\_dfa}(M) \wedge {\cal L} (M) = A}\bigskip
\end{minipage}
\end{block}
\end{textblock}}
\medskip
\only<6->{\underline{A solution}:\;\;use \smath{\text{nat}}s \;@{text "\<Rightarrow>"}\; state nodes\medskip}
\only<7->{You have to \alert{rename} states!}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[t]
\frametitle{\normalsize Formal language theory\ldots\hfill\mbox{}}
\mbox{}\\[-15mm]\mbox{}
\begin{center}
\huge\bf\textcolor{gray}{in Theorem Provers}\\
\footnotesize\textcolor{gray}{e.g.~Isabelle, Coq, HOL4, \ldots}
\end{center}
\begin{itemize}
\item Kozen's paper proof of Myhill-Nerode:\\
requires absence of \alert{inaccessible states}
\item complementation of automata only works for \alert{complete} automata
(need sink states)\medskip
\end{itemize}\bigskip\bigskip
\begin{center}
\smath{\;\text{is\_regular}(A) \dn \exists M.\;\text{is\_dfa}(M) \wedge {\cal L} (M) = A}
\end{center}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[t]
\frametitle{}
\mbox{}\\[25mm]\mbox{}
\begin{textblock}{13.9}(0.7,1.2)
\begin{block}{}
\begin{minipage}{13.4cm}\raggedright
{\bf Definition:}\smallskip\\
A language \smath{A} is \alert{regular}, provided there exists a\\
\alert{regular expression} that matches all strings of \smath{A}.
\end{minipage}
\end{block}
\end{textblock}\pause
{\noindent\large\bf\alert{\ldots{}and forget about automata}}\bigskip\bigskip\pause
Infrastructure for free. But do we lose anything?\medskip\pause
\begin{minipage}{1.1\textwidth}
\begin{itemize}
\item pumping lemma\pause
\item closure under complementation\pause
\item \only<6>{regular expression matching}%
\only<7->{\sout{regular expression matching}
{\footnotesize(@{text "\<Rightarrow>"}Brozowski'64, Owens et al '09)}}
\item<8-> most textbooks are about automata
\end{itemize}
\end{minipage}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{\LARGE The Myhill-Nerode Theorem}
\begin{itemize}
\item provides necessary and suf\!ficient conditions\\ for a language
being regular\\ \textcolor{gray}{(pumping lemma only necessary)}\bigskip
\item key is the equivalence relation:\medskip
\begin{center}
\smath{x \approx_{A} y \,\dn\, \forall z.\; x @ z \in A \Leftrightarrow y @ z \in A}
\end{center}
\end{itemize}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{\LARGE The Myhill-Nerode Theorem}
\begin{center}
\only<1>{%
\begin{tikzpicture}[scale=3]
\draw[very thick] (0.5,0.5) circle (.6cm);
\end{tikzpicture}}%
\only<2->{%
\begin{tikzpicture}[scale=3]
\draw[very thick] (0.5,0.5) circle (.6cm);
\clip[draw] (0.5,0.5) circle (.6cm);
\draw[step=2mm, very thick] (-1.4,-1.4) grid (1.4,1.4);
\end{tikzpicture}}
\end{center}
\begin{itemize}
\item \smath{\text{finite}\, (U\!N\!IV /\!/ \approx_A) \;\Leftrightarrow\; A\; \text{is regular}}
\end{itemize}
\begin{textblock}{5}(2.1,5.3)
\begin{tikzpicture}
\node at (0,0) [single arrow, fill=red,text=white, minimum height=2cm]
{$U\!N\!IV$};
\draw (-0.3,-1.1) node {\begin{tabular}{l}set of all\\[-1mm] strings\end{tabular}};
\end{tikzpicture}
\end{textblock}
\only<2->{%
\begin{textblock}{5}(9.1,7.2)
\begin{tikzpicture}
\node at (0,0) [shape border rotate=180,single arrow, fill=red,text=white, minimum height=2cm]
{@{text "\<lbrakk>s\<rbrakk>"}$_{\approx_{A}}$};
\draw (0.9,-1.1) node {\begin{tabular}{l}an equivalence class\end{tabular}};
\end{tikzpicture}
\end{textblock}}
\only<3->{
\begin{textblock}{11.9}(1.7,3)
\begin{block}{}
\begin{minipage}{11.4cm}\raggedright
Two directions:\medskip\\
\begin{tabular}{@ {}ll}
1.)\;finite $\Rightarrow$ regular\\
\;\;\;\smath{\text{finite}\,(U\!N\!IV /\!/ \approx_A) \Rightarrow \exists r.\;A = {\cal L}(r)}\\[3mm]
2.)\;regular $\Rightarrow$ finite\\
\;\;\;\smath{\text{finite}\, (U\!N\!IV /\!/ \approx_{{\cal L}(r)})}
\end{tabular}
\end{minipage}
\end{block}
\end{textblock}}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{\LARGE Initial and Final {\sout{\textcolor{gray}{States}}}}
\begin{textblock}{8}(10, 2)
\textcolor{black}{Equivalence Classes}
\end{textblock}
\begin{center}
\begin{tikzpicture}[scale=3]
\draw[very thick] (0.5,0.5) circle (.6cm);
\clip[draw] (0.5,0.5) circle (.6cm);
\draw[step=2mm, very thick] (-1.4,-1.4) grid (1.4,1.4);
\only<2->{\draw[blue, fill] (0.0, 0.6) rectangle (0.2, 0.8);}
\only<3->{\draw[red, fill] (0.2, 0.2) rectangle (0.4, 0.4);
\draw[red, fill] (0.4, 0.8) rectangle (0.6, 1.0);
\draw[red, fill] (0.6, 0.0) rectangle (0.8, 0.2);
\draw[red, fill] (0.8, 0.4) rectangle (1.0, 0.6);}
\end{tikzpicture}
\end{center}
\begin{itemize}
\item \smath{\text{finals}\,A\,\dn \{[\!|s|\!]_{\approx_{A}}\;|\;s \in A\}}
\smallskip
\item we can prove: \smath{A = \bigcup \text{finals}\,A}
\end{itemize}
\only<2->{%
\begin{textblock}{5}(2.1,4.6)
\begin{tikzpicture}
\node at (0,0) [single arrow, fill=blue,text=white, minimum height=2cm]
{$[] \in X$};
\end{tikzpicture}
\end{textblock}}
\only<3->{%
\begin{textblock}{5}(10,7.4)
\begin{tikzpicture}
\node at (0,0) [shape border rotate=180,single arrow, fill=red,text=white, minimum height=2cm]
{a final};
\end{tikzpicture}
\end{textblock}}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}<-1>[c]
\frametitle{\begin{tabular}{@ {}l}\LARGE%
Transitions between Eq-Classes\end{tabular}}
\begin{center}
\begin{tikzpicture}[scale=3]
\draw[very thick] (0.5,0.5) circle (.6cm);
\clip[draw] (0.5,0.5) circle (.6cm);
\draw[step=2mm, very thick] (-1.4,-1.4) grid (1.4,1.4);
\draw[blue, fill] (0.0, 0.6) rectangle (0.2, 0.8);
\draw[blue, fill] (0.8, 0.4) rectangle (1.0, 0.6);
\draw[white] (0.1,0.7) node (X) {$X$};
\draw[white] (0.9,0.5) node (Y) {$Y$};
\draw[blue, ->, line width = 2mm, bend left=45] (X) -- (Y);
\node [inner sep=1pt,label=above:\textcolor{blue}{$c$}] at ($ (X)!.5!(Y) $) {};
\end{tikzpicture}
\end{center}
\begin{center}
\smath{X \stackrel{c}{\longrightarrow} Y \;\dn\; X ; c \subseteq Y}
\end{center}
\onslide<8>{
\begin{tabular}{c}
\begin{tikzpicture}[shorten >=1pt,node distance=2cm,auto, ultra thick]
\tikzstyle{state}=[circle,thick,draw=blue!75,fill=blue!20,minimum size=0mm]
\node[state,initial] (q_0) {$R_1$};
\end{tikzpicture}
\end{tabular}}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{\LARGE Systems of Equations}
Inspired by a method of Brzozowski\;'64:\bigskip\bigskip
\begin{center}
\begin{tabular}{@ {\hspace{-20mm}}c}
\\[-13mm]
\begin{tikzpicture}[shorten >=1pt,node distance=2cm,auto, ultra thick]
\tikzstyle{state}=[circle,thick,draw=blue!75,fill=blue!20,minimum size=0mm]
%\draw[help lines] (0,0) grid (3,2);
\node[state,initial] (p_0) {$X_1$};
\node[state,accepting] (p_1) [right of=q_0] {$X_2$};
\path[->] (p_0) edge [bend left] node {a} (p_1)
edge [loop above] node {b} ()
(p_1) edge [loop above] node {a} ()
edge [bend left] node {b} (p_0);
\end{tikzpicture}\\
\\[-13mm]
\end{tabular}
\end{center}
\begin{center}
\begin{tabular}{@ {\hspace{-6mm}}ll@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
& \smath{X_1} & \smath{=} & \smath{X_1;b + X_2;b \onslide<2->{\alert<2>{+ \lambda;[]}}}\\
& \smath{X_2} & \smath{=} & \smath{X_1;a + X_2;a}\medskip\\
\end{tabular}
\end{center}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}<1>[t]
\small
\begin{center}
\begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}ll}
\onslide<1->{\smath{X_1}} & \onslide<1->{\smath{=}}
& \onslide<1->{\smath{X_1; b + X_2; b + \lambda;[]}}\\
\onslide<1->{\smath{X_2}} & \onslide<1->{\smath{=}}
& \onslide<1->{\smath{X_1; a + X_2; a}}\\
& & & \onslide<2->{by Arden}\\
\onslide<2->{\smath{X_1}} & \onslide<2->{\smath{=}}
& \onslide<2->{\smath{X_1; b + X_2; b + \lambda;[]}}\\
\onslide<2->{\smath{X_2}} & \onslide<2->{\smath{=}}
& \only<2->{\smath{X_1; a\cdot a^\star}}\\
& & & \onslide<4->{by Arden}\\
\onslide<4->{\smath{X_1}} & \onslide<4->{\smath{=}}
& \onslide<4->{\smath{X_2; b \cdot b^\star+ \lambda;b^\star}}\\
\onslide<4->{\smath{X_2}} & \onslide<4->{\smath{=}}
& \onslide<4->{\smath{X_1; a\cdot a^\star}}\\
& & & \onslide<5->{by substitution}\\
\onslide<5->{\smath{X_1}} & \onslide<5->{\smath{=}}
& \onslide<5->{\smath{X_1; a\cdot a^\star \cdot b \cdot b^\star+ \lambda;b^\star}}\\
\onslide<5->{\smath{X_2}} & \onslide<5->{\smath{=}}
& \onslide<5->{\smath{X_1; a\cdot a^\star}}\\
& & & \onslide<6->{by Arden}\\
\onslide<6->{\smath{X_1}} & \onslide<6->{\smath{=}}
& \onslide<6->{\smath{\lambda;b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star}}\\
\onslide<6->{\smath{X_2}} & \onslide<6->{\smath{=}}
& \onslide<6->{\smath{X_1; a\cdot a^\star}}\\
& & & \onslide<7->{by substitution}\\
\onslide<7->{\smath{X_1}} & \onslide<7->{\smath{=}}
& \onslide<7->{\smath{\lambda;b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star}}\\
\onslide<7->{\smath{X_2}} & \onslide<7->{\smath{=}}
& \onslide<7->{\smath{\lambda; b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star
\cdot a\cdot a^\star}}\\
\end{tabular}
\end{center}
\only<8->{
\begin{textblock}{6}(2.5,4)
\begin{block}{}
\begin{minipage}{8cm}\raggedright
\begin{tikzpicture}[shorten >=1pt,node distance=2cm,auto, ultra thick, inner sep=1mm]
\tikzstyle{state}=[circle,thick,draw=blue!75,fill=blue!20,minimum size=0mm]
%\draw[help lines] (0,0) grid (3,2);
\node[state,initial] (p_0) {$X_1$};
\node[state,accepting] (p_1) [right of=q_0] {$X_2$};
\path[->] (p_0) edge [bend left] node {a} (p_1)
edge [loop above] node {b} ()
(p_1) edge [loop above] node {a} ()
edge [bend left] node {b} (p_0);
\end{tikzpicture}
\end{minipage}
\end{block}
\end{textblock}}
\only<1,2>{%
\begin{textblock}{3}(0.6,1.2)
\begin{tikzpicture}
\node at (0,0) [single arrow, fill=red,text=white, minimum height=0cm]
{\textcolor{red}{a}};
\end{tikzpicture}
\end{textblock}}
\only<2>{%
\begin{textblock}{3}(0.6,3.6)
\begin{tikzpicture}
\node at (0,0) [single arrow, fill=red,text=white, minimum height=0cm]
{\textcolor{red}{a}};
\end{tikzpicture}
\end{textblock}}
\only<4>{%
\begin{textblock}{3}(0.6,2.9)
\begin{tikzpicture}
\node at (0,0) [single arrow, fill=red,text=white, minimum height=0cm]
{\textcolor{red}{a}};
\end{tikzpicture}
\end{textblock}}
\only<4>{%
\begin{textblock}{3}(0.6,5.3)
\begin{tikzpicture}
\node at (0,0) [single arrow, fill=red,text=white, minimum height=0cm]
{\textcolor{red}{a}};
\end{tikzpicture}
\end{textblock}}
\only<5>{%
\begin{textblock}{3}(1.0,5.6)
\begin{tikzpicture}
\node at (0,0) (A) {};
\node at (0,1) (B) {};
\draw[<-, line width=2mm, red] (B) to (A);
\end{tikzpicture}
\end{textblock}}
\only<5,6>{%
\begin{textblock}{3}(0.6,7.7)
\begin{tikzpicture}
\node at (0,0) [single arrow, fill=red,text=white, minimum height=0cm]
{\textcolor{red}{a}};
\end{tikzpicture}
\end{textblock}}
\only<6>{%
\begin{textblock}{3}(0.6,10.1)
\begin{tikzpicture}
\node at (0,0) [single arrow, fill=red,text=white, minimum height=0cm]
{\textcolor{red}{a}};
\end{tikzpicture}
\end{textblock}}
\only<7>{%
\begin{textblock}{3}(1.0,10.3)
\begin{tikzpicture}
\node at (0,0) (A) {};
\node at (0,1) (B) {};
\draw[->, line width=2mm, red] (B) to (A);
\end{tikzpicture}
\end{textblock}}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{\LARGE A Variant of Arden's Lemma}
{\bf Arden's Lemma:}\smallskip
If \smath{[] \not\in A} then
\begin{center}
\smath{X = X; A + \text{something}}
\end{center}
has the (unique) solution
\begin{center}
\smath{X = \text{something} ; A^\star}
\end{center}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}<1-2,4->[t]
\small
\begin{center}
\begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}ll}
\onslide<1->{\smath{X_1}} & \onslide<1->{\smath{=}}
& \onslide<1->{\smath{X_1; b + X_2; b + \lambda;[]}}\\
\onslide<1->{\smath{X_2}} & \onslide<1->{\smath{=}}
& \onslide<1->{\smath{X_1; a + X_2; a}}\\
& & & \onslide<2->{by Arden}\\
\onslide<2->{\smath{X_1}} & \onslide<2->{\smath{=}}
& \onslide<2->{\smath{X_1; b + X_2; b + \lambda;[]}}\\
\onslide<2->{\smath{X_2}} & \onslide<2->{\smath{=}}
& \only<2->{\smath{X_1; a\cdot a^\star}}\\
& & & \onslide<4->{by Arden}\\
\onslide<4->{\smath{X_1}} & \onslide<4->{\smath{=}}
& \onslide<4->{\smath{X_2; b \cdot b^\star+ \lambda;b^\star}}\\
\onslide<4->{\smath{X_2}} & \onslide<4->{\smath{=}}
& \onslide<4->{\smath{X_1; a\cdot a^\star}}\\
& & & \onslide<5->{by substitution}\\
\onslide<5->{\smath{X_1}} & \onslide<5->{\smath{=}}
& \onslide<5->{\smath{X_1; a\cdot a^\star \cdot b \cdot b^\star+ \lambda;b^\star}}\\
\onslide<5->{\smath{X_2}} & \onslide<5->{\smath{=}}
& \onslide<5->{\smath{X_1; a\cdot a^\star}}\\
& & & \onslide<6->{by Arden}\\
\onslide<6->{\smath{X_1}} & \onslide<6->{\smath{=}}
& \onslide<6->{\smath{\lambda;b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star}}\\
\onslide<6->{\smath{X_2}} & \onslide<6->{\smath{=}}
& \onslide<6->{\smath{X_1; a\cdot a^\star}}\\
& & & \onslide<7->{by substitution}\\
\onslide<7->{\smath{X_1}} & \onslide<7->{\smath{=}}
& \onslide<7->{\smath{\lambda;b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star}}\\
\onslide<7->{\smath{X_2}} & \onslide<7->{\smath{=}}
& \onslide<7->{\smath{\lambda; b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star
\cdot a\cdot a^\star}}\\
\end{tabular}
\end{center}
\only<8->{
\begin{textblock}{6}(2.5,4)
\begin{block}{}
\begin{minipage}{8cm}\raggedright
\begin{tikzpicture}[shorten >=1pt,node distance=2cm,auto, ultra thick, inner sep=1mm]
\tikzstyle{state}=[circle,thick,draw=blue!75,fill=blue!20,minimum size=0mm]
%\draw[help lines] (0,0) grid (3,2);
\node[state,initial] (p_0) {$X_1$};
\node[state,accepting] (p_1) [right of=q_0] {$X_2$};
\path[->] (p_0) edge [bend left] node {a} (p_1)
edge [loop above] node {b} ()
(p_1) edge [loop above] node {a} ()
edge [bend left] node {b} (p_0);
\end{tikzpicture}
\end{minipage}
\end{block}
\end{textblock}}
\only<1,2>{%
\begin{textblock}{3}(0.6,1.2)
\begin{tikzpicture}
\node at (0,0) [single arrow, fill=red,text=white, minimum height=0cm]
{\textcolor{red}{a}};
\end{tikzpicture}
\end{textblock}}
\only<2>{%
\begin{textblock}{3}(0.6,3.6)
\begin{tikzpicture}
\node at (0,0) [single arrow, fill=red,text=white, minimum height=0cm]
{\textcolor{red}{a}};
\end{tikzpicture}
\end{textblock}}
\only<4>{%
\begin{textblock}{3}(0.6,2.9)
\begin{tikzpicture}
\node at (0,0) [single arrow, fill=red,text=white, minimum height=0cm]
{\textcolor{red}{a}};
\end{tikzpicture}
\end{textblock}}
\only<4>{%
\begin{textblock}{3}(0.6,5.3)
\begin{tikzpicture}
\node at (0,0) [single arrow, fill=red,text=white, minimum height=0cm]
{\textcolor{red}{a}};
\end{tikzpicture}
\end{textblock}}
\only<5>{%
\begin{textblock}{3}(1.0,5.6)
\begin{tikzpicture}
\node at (0,0) (A) {};
\node at (0,1) (B) {};
\draw[<-, line width=2mm, red] (B) to (A);
\end{tikzpicture}
\end{textblock}}
\only<5,6>{%
\begin{textblock}{3}(0.6,7.7)
\begin{tikzpicture}
\node at (0,0) [single arrow, fill=red,text=white, minimum height=0cm]
{\textcolor{red}{a}};
\end{tikzpicture}
\end{textblock}}
\only<6>{%
\begin{textblock}{3}(0.6,10.1)
\begin{tikzpicture}
\node at (0,0) [single arrow, fill=red,text=white, minimum height=0cm]
{\textcolor{red}{a}};
\end{tikzpicture}
\end{textblock}}
\only<7>{%
\begin{textblock}{3}(1.0,10.3)
\begin{tikzpicture}
\node at (0,0) (A) {};
\node at (0,1) (B) {};
\draw[->, line width=2mm, red] (B) to (A);
\end{tikzpicture}
\end{textblock}}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{\LARGE The Other Direction}
One has to prove
\begin{center}
\smath{\text{finite} (U\!N\!IV /\!/ \approx_{{\cal L}(r)})}
\end{center}
by induction on \smath{r}. Not trivial, but after a bit
of thinking, one can find a \alert{refined} relation:\bigskip
\begin{center}
\mbox{\begin{tabular}{c@ {\hspace{7mm}}c@ {\hspace{7mm}}c}
\begin{tikzpicture}[scale=1.1]
%Circle
\draw[thick] (0,0) circle (1.1);
\end{tikzpicture}
&
\begin{tikzpicture}[scale=1.1]
%Circle
\draw[thick] (0,0) circle (1.1);
%Main rays
\foreach \a in {0, 90,...,359}
\draw[very thick] (0, 0) -- (\a:1.1);
\foreach \a / \l in {45/1, 135/2, 225/3, 315/4}
\draw (\a: 0.65) node {\small$a_\l$};
\end{tikzpicture}
&
\begin{tikzpicture}[scale=1.1]
%Circle
\draw[red, thick] (0,0) circle (1.1);
%Main rays
\foreach \a in {0, 45,...,359}
\draw[red, very thick] (0, 0) -- (\a:1.1);
\foreach \a / \l in {22.5/1.1, 67.5/1.2, 112.5/2.1, 157.5/2.2, 202.4/3.1, 247.5/3.2, 292.5/4.1, 337.5/4.2}
\draw (\a: 0.77) node {\textcolor{red}{\footnotesize$a_{\l}$}};
\end{tikzpicture}\\
\small\smath{U\!N\!IV} &
\small\smath{U\!N\!IV /\!/ \approx_{{\cal L}(r)}} &
\small\smath{U\!N\!IV /\!/ \alert{R}}
\end{tabular}}
\end{center}
\begin{textblock}{5}(9.8,2.6)
\begin{tikzpicture}
\node at (0,0) [shape border rotate=270,single arrow, fill=red,text=white, minimum height=0cm]{\textcolor{red}{a}};
\end{tikzpicture}
\end{textblock}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[t]
\frametitle{\LARGE\begin{tabular}{c}Derivatives of RExps\end{tabular}}
\begin{itemize}
\item introduced by Brozowski~'64
\item produces a regular expression after a character has been parsed\\[-18mm]\mbox{}
\end{itemize}
\only<1->{%
\textcolor{blue}{%
\begin{center}
\begin{tabular}{@ {}lc@ {\hspace{3mm}}l@ {}}
der c $\varnothing$ & $\dn$ & $\varnothing$\\
der c [] & $\dn$ & $\varnothing$\\
der c d & $\dn$ & if c $=$ d then [] else $\varnothing$\\
der c ($r_1 + r_2$) & $\dn$ & (der c $r_1$) $+$ (der c $r_2$)\\
der c ($r^\star$) & $\dn$ & (der c $r$) $\cdot$ $r^\star$\\
der c ($r_1 \cdot r_2$) & $\dn$ & if nullable $r_1$\\
& & then (der c $r_1$) $\cdot$ $r_2$ $+$ (der c $r_2$)\\
& & else (der c $r_1$) $\cdot$ $r_2$\\
\end{tabular}
\end{center}}}
\only<2>{
\begin{textblock}{13}(1.5,5.7)
\begin{block}{}
\begin{quote}
\begin{minipage}{13cm}\raggedright
derivatives refine \smath{x \approx_{{\cal{L}}(r)} y}\bigskip
\begin{center}
\smath{\text{der}~x~r = \text{der}~y~r \Longrightarrow x \approx_{L(r)} y}
\end{center}\bigskip
\
\smath{\text{finite}(\text{ders}~A~r)}, but only modulo ACI
\begin{center}
\begin{tabular}{@ {\hspace{-10mm}}rcl}
\smath{(r_1 + r_2) + r_3} & \smath{\equiv} & \smath{r_1 + (r_2 + r_3)}\\
\smath{r_1 + r_2} & \smath{\equiv} & \smath{r_2 + r_1}\\
\smath{r + r} & \smath{\equiv} & \smath{r}\\
\end{tabular}
\end{center}
\end{minipage}
\end{quote}
\end{block}
\end{textblock}}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}<2>[t]
\frametitle{\LARGE\begin{tabular}{c}Derivatives of RExps\end{tabular}}
\only<2>{%
\textcolor{blue}{%
\begin{center}
\begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {}}
pder c $\varnothing$ & $\dn$ & \alert{$\{\}$}\\
pder c [] & $\dn$ & \alert{$\{\}$}\\
pder c d & $\dn$ & if c $=$ d then $\{$[]$\}$ else $\{\}$\\
pder c ($r_1 + r_2$) & $\dn$ & (pder c $r_1$) \alert{$\cup$} (der c $r_2$)\\
pder c ($r^\star$) & $\dn$ & (pder c $r$) $\cdot$ $r^\star$\\
pder c ($r_1 \cdot r_2$) & $\dn$ & if nullable $r_1$\\
& & then (pder c $r_1$) $\cdot$ $r_2$ \alert{$\cup$} (pder c $r_2$)\\
& & else (pder c $r_1$) $\cdot$ $r_2$\\
\end{tabular}
\end{center}}}
\only<2>{
\begin{textblock}{6}(8.5,2.7)
\begin{block}{}
\begin{quote}
\begin{minipage}{6cm}\raggedright
\begin{itemize}
\item partial derivatives
\item by Antimirov~'95
\end{itemize}
\end{minipage}
\end{quote}
\end{block}
\end{textblock}}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[t]
\frametitle{\LARGE Partial Derivatives}
\mbox{}\\[0mm]\mbox{}
\begin{itemize}
\item \alt<1>{\smath{\text{pders $x$ $r$ \mbox{$=$} pders $y$ $r$}}}
{\smath{\underbrace{\text{pders $x$ $r$ \mbox{$=$} pders $y$ $r$}}_{R}}}
refines \textcolor{blue}{$x$ $\approx_{{\cal L}(r)}$ $y$}\\[16mm]\pause
\item \smath{\text{finite} (U\!N\!IV /\!/ R)} \bigskip\pause
\item Therefore \smath{\text{finite} (U\!N\!IV /\!/ \approx_{{\cal L}(r)})}. Qed.
\end{itemize}
\only<2->{%
\begin{textblock}{5}(3.9,7.2)
\begin{tikzpicture}
\node at (0,0) [shape border rotate=270,single arrow, fill=red,text=white, minimum height=0cm]{\textcolor{red}{a}};
\draw (2.2,0) node {Antimirov '95};
\end{tikzpicture}
\end{textblock}}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[t]
\frametitle{\LARGE What Have We Achieved?}
\begin{itemize}
\item \smath{\text{finite}\, (U\!N\!IV /\!/ \approx_A) \;\Leftrightarrow\; A\; \text{is regular}}
\medskip\pause
\item regular languages are closed under complementation; this is now easy
\begin{center}
\smath{U\!N\!IV /\!/ \approx_A \;\;=\;\; U\!N\!IV /\!/ \approx_{\overline{A}}}
\end{center}\pause\medskip
\item non-regularity (\smath{a^nb^n})\medskip\pause\pause
\item take \alert{\bf any} language\\ build the language of substrings\\
\pause
then this language \alert{\bf is} regular\;\; (\smath{a^nb^n} $\Rightarrow$ \smath{a^\star{}b^\star})
\end{itemize}
\only<2>{
\begin{textblock}{10}(4,14)
\small
\smath{x \approx_{A} y \,\dn\, \forall z.\; x @ z \in A \Leftrightarrow y @ z \in A}
\end{textblock}}
\only<4>{
\begin{textblock}{5}(2,8.6)
\begin{minipage}{8.8cm}
\begin{block}{}
\begin{minipage}{8.6cm}
If there exists a sufficiently large set \smath{B} (for example infinitely large),
such that
\begin{center}
\smath{\forall x,y \in B.\; x \not= y \;\Rightarrow\; x \not\approx_{A} y}.
\end{center}
then \smath{A} is not regular.\hspace{1.3cm}\small(\smath{B \dn \bigcup_n a^n})
\end{minipage}
\end{block}
\end{minipage}
\end{textblock}
}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{\normalsize Formal language theory\ldots\hfill\mbox{}}
\begin{center}
\huge\bf\textcolor{gray}{in Nuprl}
\end{center}
\begin{itemize}
\item Constable, Jackson, Naumov, Uribe\medskip
\item \alert{18 months} for automata theory from Hopcroft \& Ullman chapters 1--11 (including Myhill-Nerode)
\end{itemize}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{\normalsize Formal language theory\ldots\hfill\mbox{}}
\begin{center}
\huge\bf\textcolor{gray}{in Coq}
\end{center}
\begin{itemize}
\item Filli\^atre, Briais, Braibant and others
\item multi-year effort; a number of results in automata theory, e.g.\medskip
\begin{itemize}
\item Kleene's thm.~by Filli\^atre (\alert{``rather big''})
\item automata theory by Briais (5400 loc)
\item Braibant ATBR library, including Myhill-Nerode\\ ($>$7000 loc)
\item Mirkin's partial derivative automaton construction (10600 loc)
\end{itemize}
\end{itemize}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}<1->[c]
\frametitle{}
\begin{center}
\includegraphics[scale=2.9]{numerals.jpg}
\end{center}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{\LARGE Conclusion}
\begin{itemize}
\item We have never seen a proof of Myhill-Nerode based on
regular expressions.\smallskip\pause
\item great source of examples (inductions)\smallskip\pause
\item no need to fight the theorem prover:\\
\begin{itemize}
\item first direction (790 loc)\\
\item second direction (400 / 390 loc)
\end{itemize}
\item I am not saying automata are bad; just formal proofs about
them are shockingly difficult.
\end{itemize}
\only<4->{
\begin{textblock}{13.8}(1,4)
\begin{block}{}\mbox{}\hspace{3mm}
\begin{minipage}{11cm}\raggedright
\large
{\bf Bold Claim: }\alert{(not proved!)}\medskip
{\bf 95\%} of regular language theory can be done without
automata!\medskip\\\ldots and this is much more tasteful ;o)
\end{minipage}
\end{block}
\end{textblock}}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[b]
\frametitle{\mbox{}\\[2cm]\textcolor{red}{Thank you very much!\\[5mm]Questions?}}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
(*<*)
end
(*>*)