(*<*)
theory Slides6
imports "~~/src/HOL/Library/LaTeXsugar"
begin
notation (latex output)
set ("_") and
Cons ("_::/_" [66,65] 65)
(*>*)
text_raw {*
\renewcommand{\slidecaption}{London, 3 October 2013}
\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 A Formalisation of the\\[-1mm]
\Large Myhill-Nerode Theorem using\\[-1mm]
\Large Regular Expressions only
\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{}\\[2mm]
\begin{itemize}
\item my background is in:
\begin{itemize}
\item \normalsize programming languages and
\item \normalsize theorem provers
\end{itemize}\medskip
\item \normalsize develop Nominal Isabelle for reasoning about programming languages\\[-10mm]\mbox{}
\end{itemize}
\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}\pause
\mbox{}\\[-19mm]\mbox{}
\begin{itemize}
\item found an error in an ACM journal paper by Bob Harper and Frank Pfenning
about LF (and fixed it in three ways)
\end{itemize}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{}
\begin{itemize}
\item found also fixable errors in my Ph.D.-thesis about cut-elimination
(examined by Henk Barendregt and Andy Pitts)\bigskip
\item formalised a classic OS scheduling algorithm (priority inversion
protocol)
\begin{itemize}
\item original algorithm was incorrect even being proved correct (with `pencil-and-paper')
\item helped us to implement this algorithm correctly and efficiently\\
\end{itemize}\bigskip\pause
\item used Isabelle to prove properties about access controls and OSes
\end{itemize}
\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}
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}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}<1-5>[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{if $nullable(r_1)$}\\
& & \bl{then $(der\,c\,r_1) \cdot r_2 + der\, c\, r_2$}\\
& & \bl{else $(der\, c\, r_1) \cdot r_2$}\\
\bl{$der\,c\,(r^*)$} & \bl{$=$} & \bl{$(der\,c\,r) \cdot r^*$} &\smallskip\\\pause
\bl{$deriv\,[]\,r$} & \bl{$=$} & \bl{$r$} & \\
\bl{$deriv\,(c::s)\,r$} & \bl{$=$} & \bl{$deriv\,s\,(der\,c\,r)$} & \\
\end{tabular}\medskip
\bl{$match\,r\,s = nullable (deriv\,s\,r)$}
\only<4>{
\begin{textblock}{10.5}(2,5)
\begin{tikzpicture}
\draw (0,0) node[inner sep=2mm,fill=cream, ultra thick, draw=red, rounded corners=2mm]
{\normalsize\color{darkgray}
\begin{minipage}{10.5cm}
\begin{center}
a)\;\; \bl{$nullable(r) \Leftrightarrow ""\in {\cal L}(r)$}\medskip
\end{center}
\begin{center}
b)\;\; \bl{${\cal L}(der\,c\,r) = Der\,c\,({\cal L}(r))$}
\end{center}
where
\begin{center}
\bl{$Der\,c\,A \dn \{s\,|\, c\!::\!s \in A\}$}
\end{center}\medskip\pause
\begin{center}
c)\;\; \bl{$match\,r\,s \Leftrightarrow s\in{\cal L}(r)$}
\end{center}
\end{minipage}};
\end{tikzpicture}
\end{textblock}}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[t]
\frametitle{\begin{tabular}{c}\bl{$(a?\{n\}) \cdot a\{n\}$}\end{tabular}}
\mbox{}\\[-13mm]
\begin{tikzpicture}[y=.2cm, x=.3cm]
%axis
\draw (0,0) -- coordinate (x axis mid) (30,0);
\draw (0,0) -- coordinate (y axis mid) (0,30);
%ticks
\foreach \x in {0,5,...,30}
\draw (\x,1pt) -- (\x,-3pt)
node[anchor=north] {\x};
\foreach \y in {0,5,...,30}
\draw (1pt,\y) -- (-3pt,\y)
node[anchor=east] {\y};
%labels
\node[below=0.6cm] at (x axis mid) {\bl{a}s};
\node[rotate=90, left=1.2cm] at (y axis mid) {secs};
%plots
\draw[color=blue] plot[mark=*, mark options={fill=white}]
file {re-python.data};
\draw[color=brown] plot[mark=pentagon*, mark options={fill=white} ]
file {re-ruby.data};
%legend
\begin{scope}[shift={(4,20)}]
\draw[color=blue] (0,0) --
plot[mark=*, mark options={fill=white}] (0.25,0) -- (0.5,0)
node[right]{\small Python};
\draw[yshift=-\baselineskip, color=brown] (0,0) --
plot[mark=pentagon*, mark options={fill=white}] (0.25,0) -- (0.5,0)
node[right]{\small Ruby};
\end{scope}
\end{tikzpicture}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[t]
\frametitle{\begin{tabular}{c}\bl{$(a?\{n\}) \cdot a\{n\}$}\end{tabular}}
\mbox{}\\[-13mm]
\begin{tabular}{@ {\hspace{-5mm}}l}
\begin{tikzpicture}[y=.2cm, x=.01cm]
%axis
\draw (0,0) -- coordinate (x axis mid) (1000,0);
\draw (0,0) -- coordinate (y axis mid) (0,30);
%ticks
\foreach \x in {0,200,...,1000}
\draw (\x,1pt) -- (\x,-3pt)
node[anchor=north] {\x};
\foreach \y in {0,5,...,30}
\draw (1pt,\y) -- (-3pt,\y)
node[anchor=east] {\y};
%labels
\node[below=0.6cm] at (x axis mid) {\bl{a}s};
\node[rotate=90, left=1.2cm] at (y axis mid) {secs};
%plots
\draw[color=blue] plot[mark=*, mark options={fill=white}]
file {re-python.data};
\draw[color=green] plot[mark=square*, mark options={fill=white} ]
file {re2c.data};
\draw[color=brown] plot[mark=pentagon*, mark options={fill=white} ]
file {re-ruby.data};
%legend
\begin{scope}[shift={(100,20)}]
\draw[color=blue] (0,0) --
plot[mark=*, mark options={fill=white}] (0.25,0) -- (50,0)
node[right]{\small Python};
\draw[yshift=-13, color=brown] (0,0) --
plot[mark=pentagon*, mark options={fill=white}] (0.25,0) -- (50,0)
node[right]{\small Ruby};
\draw[yshift=13, color=green] (0,0) --
plot[mark=square*, mark options={fill=white}] (0.25,0) -- (50,0)
node[right]{\small nullable + der};
\end{scope}
\end{tikzpicture}
\end{tabular}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw{*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[t]
\frametitle{\begin{tabular}{c}\bl{$(a?\{n\}) \cdot a\{n\}$}\end{tabular}}
\mbox{}\\[-9mm]
\begin{tabular}{@ {\hspace{-5mm}}l}
\begin{tikzpicture}[y=.2cm, x=.0008cm]
%axis
\draw (0,0) -- coordinate (x axis mid) (12000,0);
\draw (0,0) -- coordinate (y axis mid) (0,30);
%ticks
\foreach \x in {0,2000,...,12000}
\draw (\x,1pt) -- (\x,-3pt)
node[anchor=north] {\x};
\foreach \y in {0,5,...,30}
\draw (1pt,\y) -- (-3pt,\y)
node[anchor=east] {\y};
%labels
\node[below=0.6cm] at (x axis mid) {\bl{a}s};
\node[rotate=90, left=1.2cm] at (y axis mid) {secs};
%plots
\draw[color=green] plot[mark=square*, mark options={fill=white} ]
file {re2b.data};
\draw[color=black] plot[mark=square*, mark options={fill=white} ]
file {re3.data};
\draw[color=blue] plot[mark=*, mark options={fill=white}]
file {re-python.data};
\draw[color=brown] plot[mark=pentagon*, mark options={fill=white} ]
file {re-ruby.data};
%legend
\begin{scope}[shift={(2000,20)}]
\draw[color=blue] (0,0) --
plot[mark=*, mark options={fill=white}] (0.25,0) -- (50,0)
node[right]{\small Python};
\draw[yshift=-13, color=brown] (0,0) --
plot[mark=pentagon*, mark options={fill=white}] (0.25,0) -- (50,0)
node[right]{\small Ruby};
\draw[yshift=13, color=green] (0,0) --
plot[mark=square*, mark options={fill=white}] (0.25,0) -- (50,0)
node[right]{\small nullable + der};
\draw[yshift=26, color=black] (0,0) --
plot[mark=square*, mark options={fill=white}] (0.25,0) -- (50,0)
node[right]{\small nullable + der + simplification};
\end{scope}
\end{tikzpicture}
\end{tabular}
\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
Already problems with defining 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 apart!}
\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
Reasoning infrastructure is 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 the key notion 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\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$ & \bl{if $nullable(r_1)$}\\
& & \bl{then $(der\,c\,r_1) \cdot r_2 + der\, c\, r_2$}\\
& & \bl{else $(der\, c\, r_1) \cdot r_2$}\\
\end{tabular}
\end{center}}}
\only<2->{
\begin{textblock}{14.1}(1.5,5.7)
\begin{block}{}
\begin{quote}
\begin{minipage}{14.1cm}\raggedright\rm
derivatives refine \smath{x \approx_{{\cal{L}}(r)} y}\bigskip
\begin{center}
\only<2>{\mbox{\hspace{-22mm}}\smath{{\cal{L}}(deriv~x~r) = {\cal{L}}(deriv~y~r)
\Longleftrightarrow x \approx_{{\cal{L}}(r)} y}}
\only<3>{\mbox{\hspace{-22mm}}\smath{deriv~x~r = deriv~y~r
\Longrightarrow x \approx_{{\cal{L}}(r)} y}}
\end{center}\bigskip
\
\smath{\text{finite}(deriv~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\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} pder\,c\,r_2$\\
$pder\,c\,(r^\star)$ & $\dn$ & $(pder\,c\,r) \cdot r^\star$\\
$pder\,c\,(r_1 \cdot r_2)$ & $\dn$ & \bl{if $nullable(r_1)$}\\
& & \bl{then $(pder\,c\,r_1) \cdot r_2 \alert{\cup} pder\, c\, r_2$}\\
& & \bl{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}\rm\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{$pderiv\,x\,r = pderiv\,y\,r$}}}
{\smath{\underbrace{\text{$pderiv\,x\,r = pderiv\,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.\bigskip\pause
\item We also gave a direct proof, but not as beautiful.
\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{\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 proofs about
them are quite difficult in theorem provers\bigskip
\item \small our journal paper has just been accepted in JAR (see webpage)
\end{itemize}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{\LARGE Future Work}
\begin{itemize}
\item regular expression sub-matching with derivatives (Martin Sulzmann PPDP'12)\bigskip
\item parsing with derivatives of grammars\\ (Matt Might ICFP'11)
\end{itemize}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[b]
\frametitle{\mbox{}\\[2cm]\textcolor{red}{Thank you very much\\ for listening!\\[5mm]Questions?}}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
(*<*)
end
(*>*)