(*<*)
theory Slides5
imports "~~/src/HOL/Library/LaTeXsugar"
begin
notation (latex output)
set ("_") and
Cons ("_::/_" [66,65] 65)
(*>*)
text_raw {*
\renewcommand{\slidecaption}{London, 29 August 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@ {}}
\\[-3mm]
\LARGE The Myhill-Nerode Theorem\\[-3mm]
\LARGE in a Theorem Prover\\[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}
\only<2->{
\begin{textblock}{6}(9,5.3)
\alert{\bf Isabelle/HOL}
\end{textblock}}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}<1->[c]
\frametitle{}
\mbox{}\\[2mm]
\begin{itemize}
\item my background is in
\begin{itemize}
\item \normalsize programming languages and theorem provers
\item \normalsize develop Nominal Isabelle
\end{itemize}\bigskip\bigskip\bigskip\bigskip\bigskip
\item<1->to formalise and mechanically check proofs from
programming language research, TCS \textcolor{gray}{and OS}\bigskip
\item<2->we found out that the variable convention can lead to
faulty proofs\ldots
\end{itemize}
\onslide<2->{
\begin{center}
\begin{block}{}
\color{gray}
\footnotesize
{\bf\mbox{}\hspace{-1.5mm}Variable Convention:}\\[0mm]
If $M_1,\ldots,M_n$ occur in a certain mathematical context
(e.g. definition, proof), then in these terms all bound variables
are chosen to be different from the free variables.\hfill Henk Barendregt
\end{block}
\end{center}}
\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 on LF 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\\ (proof-carrying code)}
\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)\bigskip
\item found flaws in a proof about a classic OS scheduling algorithm
--- helped us to implement\\ it correctly and ef$\!$ficiently\\
{\small\textcolor{gray}{(the existing literature ``proved''
correct an incorrect algorithm; used in the Mars Pathfinder mission)}}
\end{itemize}\bigskip\bigskip\pause
{\bf Conclusion:}\smallskip
Pencil-and-paper proofs in TCS are not foolproof,
not even expertproof.
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[t]
\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}\pause
\begin{tabular}{@ {}c@ {}}
Tobias Nipkow calls this the ``London Underground Phenomenon'':
\end{tabular}
\begin{center}
\begin{tabular}{ccc}
students & \;\;\raisebox{-8mm}{\includegraphics[scale=0.16]{gap.jpg}}\;\; & proofs
\end{tabular}
\end{center}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{}
\begin{textblock}{12.9}(1.5,2.0)
\begin{block}{}
\begin{minipage}{12.4cm}\raggedright
\large {\bf Motivation:}\\[2mm]I want to teach \alert{students} with
theorem\\ provers (especially for inductions).
\end{minipage}
\end{block}
\end{textblock}\pause
\mbox{}\\[35mm]\mbox{}
\begin{itemize}
\item \only<2>{\smath{\text{fib}}, \smath{\text{even}} and \smath{\text{odd}}}%
\only<3->{\sout{\smath{\text{fib}}, \smath{\text{even}} and \smath{\text{odd}}}}\medskip
\item<3-> formal language theory \\
\mbox{}\;\;@{text "\<Rightarrow>"} nice textbooks: Kozen, Hopcroft \& Ullman\ldots
\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 ($\varnothing$)} & \bl{$=$} & \bl{false} &\\
\bl{nullable ([])} & \bl{$=$} & \bl{true} &\\
\bl{nullable (c)} & \bl{$=$} & \bl{false} &\\
\bl{nullable (r$_1$ + r$_2$)} & \bl{$=$} & \bl{(nullable r$_1$) $\vee$ (nullable r$_2$)} & \\
\bl{nullable (r$_1$ $\cdot$ r$_2$)} & \bl{$=$} & \bl{(nullable r$_1$) $\wedge$ (nullable r$_2$)} & \\
\bl{nullable (r$^*$)} & \bl{$=$} & \bl{true} & \\
\end{tabular}\medskip\pause
\begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{-10mm}}l@ {}}
\bl{der c ($\varnothing$)} & \bl{$=$} & \bl{$\varnothing$} & \\
\bl{der c ([])} & \bl{$=$} & \bl{$\varnothing$} & \\
\bl{der c (d)} & \bl{$=$} & \bl{if c $=$ d then [] else $\varnothing$} & \\
\bl{der c (r$_1$ + r$_2$)} & \bl{$=$} & \bl{(der c r$_1$) + (der c r$_2$)} & \\
\bl{der c (r$_1$ $\cdot$ r$_2$)} & \bl{$=$} & \bl{((der c r$_1$) $\cdot$ r$_2$) + } & \\
& & \bl{\hspace{3mm}(if nullable r$_1$ then der c r$_2$ else $\varnothing$)}\\
\bl{der c (r$^*$)} & \bl{$=$} & \bl{(der c r) $\cdot$ (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}[c]
\frametitle{\LARGE Regular Expression Matching\\[-2mm] in Education}
\begin{itemize}
\item Harper in JFP'99: ``Functional Pearl: Proof- Directed Debugging''\medskip
\item Yi in JFP'06: ``Educational Pearl: `Proof-Directed Debugging' revisited
for a first-order version''\medskip\bigskip\bigskip\pause
\item Owens et al in JFP'09: ``Regular-expression derivatives re-examined''
\bigskip
\begin{quote}\small
``Unfortunately, regular expression derivatives have been lost in the
sands of time, and few computer scientists are aware of them.''
\end{quote}
\end{itemize}
\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>"}Brzozowski'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 Brzozowski~'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^*$) & $\dn$ & (der c $r$) $\cdot$ ($r^*$)\\
der c ($r_1 \cdot r_2$) & $\dn$ & ((der c $r_1$) $\cdot$ $r_2$) +\\
& & \hspace{-3mm}(if nullable $r_1$ then der c $r_2$ else $\varnothing$)\\
\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}
\only<2>{\mbox{\hspace{-22mm}}\smath{{\cal{L}}(\text{ders}~x~r) = {\cal{L}}(\text{ders}~y~r)
\Longleftrightarrow x \approx_{L(r)} y}}
\only<3>{\mbox{\hspace{-22mm}}\smath{\text{ders}~x~r = \text{ders}~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}Partial 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$ & (pder c $r_1$) $\cdot$ $r_2$ \alert{$\cup$}\\
& & \hspace{-4mm}if nullable $r_1$ then (pder c $r_2$) else $\varnothing$\\
\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}[c]
\frametitle{\LARGE Conclusion}
\begin{itemize}
\item we have never seen a proof of Myhill-Nerode based on
regular expressions only\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 quite dif$\!$ficult\pause\bigskip\medskip
\item parsing with derivatives of grammars\\ (Matt Might ICFP'11)
\end{itemize}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{\LARGE An Apology}
\begin{itemize}
\item This should all of course be done co-inductively
\end{itemize}
\footnotesize
\begin{tabular}{@ {\hspace{4mm}}l}
From: Jasmin Christian Blanchette\\
To: isabelle-dev@mailbroy.informatik.tu-muenchen.de\\
Subject: [isabelle-dev] NEWS\\
Date: \alert{\bf Tue, 28 Aug 2012} 17:40:55 +0200\\
\\
* {\bf HOL/Codatatype}: New (co)datatype package with support for mixed,\\
nested recursion and interesting non-free datatypes.\\
\\
* HOL/Ordinals\_and\_Cardinals: Theories of ordinals and cardinals\\
(supersedes the AFP entry of the same name).\\[2mm]
Kudos to Andrei and Dmitriy!\\
\\
Jasmin\\[-1mm]
------------------------------------\\
isabelle-dev mailing list\\
isabelle-dev@in.tum.de\\
\end{tabular}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[b]
\frametitle{\mbox{}\\[2cm]\textcolor{red}{Thank you very much!\\[5mm]Questions?}}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
(*<*)
end
(*>*)