--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Slides/Slides2.thy Sun Nov 20 22:53:50 2011 +0000
@@ -0,0 +1,869 @@
+(*<*)
+theory Slides2
+imports "~~/src/HOL/Library/LaTeXsugar"
+begin
+
+notation (latex output)
+ set ("_") and
+ Cons ("_::/_" [66,65] 65)
+
+(*>*)
+
+
+text_raw {*
+ %\renewcommand{\slidecaption}{Cambridge, 9 November 2010}
+ %\renewcommand{\slidecaption}{Nijmegen, 25 August 2011}
+ \renewcommand{\slidecaption}{St Andrews, 19 November 2011}
+ \newcommand{\bl}[1]{#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}[c]
+ \frametitle{}
+
+ \includegraphics[scale=0.5]{roy.jpg}\medskip
+
+ Roy intertwined with my scientific life on many occasions, most
+ notably:\bigskip
+
+ \begin{itemize}
+ \item he admitted me for M.Phil.~in St Andrews and\\
+ made me like theory\smallskip
+ \item sent me to Cambridge for Ph.D.\bigskip
+ \item made me appreciate precision in proofs
+ \end{itemize}
+
+ \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}\medskip\pause
+
+ \small
+ \begin{minipage}{1.0\textwidth}
+ (I also found an {\bf error} in my Ph.D.-thesis about cut-elimination
+ examined by Henk Barendregt and Andy Pitts.)
+ \end{minipage}
+
+ \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 (C) to [red, very thick, bend left=45] (B);
+ \draw (D) to [red, very thick, 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:\\
+ \hspace{2cm}requires absence of \alert{inaccessible states}
+ \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>x\<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 \{[\!|x|\!]_{\approx_{A}}\;|\;x \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-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 a regular expressions 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>{%
+ \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,4.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{\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}
+ \end{itemize}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[b]
+ \frametitle{\mbox{}\\[2cm]\textcolor{red}{Thank you!\\[5mm]Questions?}}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+(*<*)
+end
+(*>*)
\ No newline at end of file