(*<*)
theory Slides7
imports "~~/src/HOL/Library/LaTeXsugar" "Main"
begin
declare [[show_question_marks = false]]
notation (latex output)
set ("_") and
Cons ("_::/_" [66,65] 65)
(*>*)
text_raw {*
\renewcommand{\slidecaption}{Beijing, 29.~April 2011}
\newcommand{\abst}[2]{#1.#2}% atom-abstraction
\newcommand{\pair}[2]{\langle #1,#2\rangle} % pairing
\newcommand{\susp}{{\boldsymbol{\cdot}}}% for suspensions
\newcommand{\unit}{\langle\rangle}% unit
\newcommand{\app}[2]{#1\,#2}% application
\newcommand{\eqprob}{\mathrel{{\approx}?}}
\newcommand{\freshprob}{\mathrel{\#?}}
\newcommand{\redu}[1]{\stackrel{#1}{\Longrightarrow}}% reduction
\newcommand{\id}{\varepsilon}% identity substitution
\newcommand{\bl}[1]{\textcolor{blue}{#1}}
\newcommand{\gr}[1]{\textcolor{gray}{#1}}
\newcommand{\rd}[1]{\textcolor{red}{#1}}
\newcommand{\ok}{\includegraphics[scale=0.07]{ok.png}}
\newcommand{\notok}{\includegraphics[scale=0.07]{notok.png}}
\newcommand{\largenotok}{\includegraphics[scale=1]{notok.png}}
\renewcommand{\Huge}{\fontsize{61.92}{77}\selectfont}
\newcommand{\veryHuge}{\fontsize{74.3}{93}\selectfont}
\newcommand{\VeryHuge}{\fontsize{89.16}{112}\selectfont}
\newcommand{\VERYHuge}{\fontsize{107}{134}\selectfont}
\newcommand{\LL}{$\mathbb{L}\,$}
\pgfdeclareradialshading{smallbluesphere}{\pgfpoint{0.5mm}{0.5mm}}%
{rgb(0mm)=(0,0,0.9);
rgb(0.9mm)=(0,0,0.7);
rgb(1.3mm)=(0,0,0.5);
rgb(1.4mm)=(1,1,1)}
\def\myitemi{\begin{pgfpicture}{-1ex}{-0.55ex}{1ex}{1ex}
\usebeamercolor[fg]{subitem projected}
{\pgftransformscale{0.8}\pgftext{\normalsize\pgfuseshading{bigsphere}}}
\pgftext{%
\usebeamerfont*{subitem projected}}
\end{pgfpicture}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}<1>[t]
\frametitle{%
\begin{tabular}{@ {\hspace{-3mm}}c@ {}}
\\
\LARGE Verifying a Regular Expression\\[-1mm]
\LARGE Matcher and Formal Language\\[-1mm]
\LARGE Theory\\[5mm]
\end{tabular}}
\begin{center}
Christian Urban\\
\small Technical University of Munich, Germany
\end{center}
\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{This Talk: 3 Points}
\large
\begin{itemize}
\item It is easy to make mistakes.\bigskip
\item Theorem provers can prevent mistakes, {\bf if} the problem
is formulated so that it is suitable for theorem provers.\bigskip
\item This re-formulation can be done, even in domains where
we least expect it.
\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$ + r$_2$}\\
& \bl{$\mid$} & \bl{r$_1$ $\cdot$ 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}
\only<2>{
\begin{textblock}{9}(3.6,11.8)
\bl{matches r s $\;\Longrightarrow\;$ true $\vee$ false}\\[3.5mm]
\hspace{10mm}\begin{tikzpicture}
\coordinate (m1) at (0.4,1);
\draw (0,0.3) node (m2) {\small\color{gray}rexp};
\path[overlay, ->, line width = 0.5mm, shorten <=-1mm, draw = gray] (m2) edge (m1);
\coordinate (s1) at (0.81,1);
\draw (1.3,0.3) node (s2) {\small\color{gray} string};
\path[overlay, ->, line width = 0.5mm, shorten <=-1mm, draw = gray] (s2) edge (s1);
\end{tikzpicture}
\end{textblock}}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}<1->[t]
\frametitle{Specification}
\small
\begin{textblock}{6}(0,3.5)
\begin{tabular}{r@ {\hspace{0.5mm}}r@ {\hspace{1.5mm}}c@ {\hspace{1.5mm}}l}
\multicolumn{4}{c}{rexp $\Rightarrow$ set of strings}\bigskip\\
&\bl{\LL ($\varnothing$)} & \bl{$\dn$} & \bl{$\varnothing$}\\
&\bl{\LL ([])} & \bl{$\dn$} & \bl{\{[]\}}\\
&\bl{\LL (c)} & \bl{$\dn$} & \bl{\{c\}}\\
&\bl{\LL (r$_1$ + r$_2$)} & \bl{$\dn$} & \bl{\LL (r$_1$) $\cup$ \LL (r$_2$)}\\
\rd{$\Rightarrow$} &\bl{\LL (r$_1$ $\cdot$ r$_2$)} & \bl{$\dn$} & \bl{\LL (r$_1$) ;; \LL (r$_2$)}\\
\rd{$\Rightarrow$} &\bl{\LL (r$^*$)} & \bl{$\dn$} & \bl{(\LL (r))$^\star$}\\
\end{tabular}
\end{textblock}
\begin{textblock}{9}(7.3,3)
{\mbox{}\hspace{2cm}\footnotesize Isabelle:\smallskip}
\includegraphics[scale=0.325]{Screen3.png}
\end{textblock}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}<1->[t]
\frametitle{Version 1}
\small
\mbox{}\\[-8mm]\mbox{}
\begin{center}\def\arraystretch{1.05}
\begin{tabular}{@ {\hspace{-5mm}}l@ {\hspace{2.5mm}}c@ {\hspace{2.5mm}}l@ {}}
\bl{match [] []} & \bl{$=$} & \bl{true}\\
\bl{match [] (c::s)} & \bl{$=$} & \bl{false}\\
\bl{match ($\varnothing$::rs) s} & \bl{$=$} & \bl{false}\\
\bl{match ([]::rs) s} & \bl{$=$} & \bl{match rs s}\\
\bl{match (c::rs) []} & \bl{$=$} & \bl{false}\\
\bl{match (c::rs) (d::s)} & \bl{$=$} & \bl{if c = d then match rs s else false}\\
\bl{match (r$_1$ + r$_2$::rs) s} & \bl{$=$} & \bl{match (r$_1$::rs) s $\vee$ match (r$_2$::rs) s}\\
\bl{match (r$_1$ $\cdot$ r$_2$::rs) s} & \bl{$=$} & \bl{match (r$_1$::r$_2$::rs) s}\\
\bl{match (r$^*$::rs) s} & \bl{$=$} & \bl{match rs s $\vee$ match (r::r$^*$::rs) s}\\
\end{tabular}
\end{center}
\begin{textblock}{9}(0.2,1.6)
\hspace{10mm}\begin{tikzpicture}
\coordinate (m1) at (0.44,-0.5);
\draw (0,0.3) node (m2) {\small\color{gray}\mbox{}\hspace{-9mm}list of rexps};
\path[overlay, ->, line width = 0.5mm, shorten <=-1mm, draw = gray] (m2) edge (m1);
\coordinate (s1) at (0.86,-0.5);
\draw (1.5,0.3) node (s2) {\small\color{gray} string};
\path[overlay, ->, line width = 0.5mm, shorten <=-1mm, draw = gray] (s2) edge (s1);
\end{tikzpicture}
\end{textblock}
\begin{textblock}{9}(2.8,11.8)
\bl{matches$_1$ r s $\;=\;$ match [r] s}
\end{textblock}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}<1->[c]
\frametitle{Testing}
\small
Every good programmer should do thourough tests:
\begin{center}
\begin{tabular}{@ {\hspace{-20mm}}lcl}
\bl{matches$_1$ (a$\cdot$b)$^*\;$ []} & \bl{$\mapsto$} & \bl{true}\\
\bl{matches$_1$ (a$\cdot$b)$^*\;$ ab} & \bl{$\mapsto$} & \bl{true}\\
\bl{matches$_1$ (a$\cdot$b)$^*\;$ aba} & \bl{$\mapsto$} & \bl{false}\\
\bl{matches$_1$ (a$\cdot$b)$^*\;$ abab} & \bl{$\mapsto$} & \bl{true}\\
\bl{matches$_1$ (a$\cdot$b)$^*\;$ abaa} & \bl{$\mapsto$} & \bl{false}\medskip\\
\onslide<2->{\bl{matches$_1$ x$\cdot$(0$|$1)$^*\;$ x} & \bl{$\mapsto$} & \bl{true}}\\
\onslide<2->{\bl{matches$_1$ x$\cdot$(0$|$1)$^*\;$ x0} & \bl{$\mapsto$} & \bl{true}}\\
\onslide<2->{\bl{matches$_1$ x$\cdot$(0$|$1)$^*\;$ x3} & \bl{$\mapsto$} & \bl{false}}
\end{tabular}
\end{center}
\onslide<3->
{Looks OK \ldots let's ship it to customers\hspace{5mm}
\raisebox{-5mm}{\includegraphics[scale=0.05]{sun.png}}}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}<1->[c]
\frametitle{Version 1}
\only<1->{Several hours later\ldots}\pause
\begin{center}
\begin{tabular}{@ {\hspace{0mm}}lcl}
\bl{matches$_1$ []$^*$ s} & \bl{$\mapsto$} & loops\\
\onslide<4->{\bl{matches$_1$ ([] + \ldots)$^*$ s} & \bl{$\mapsto$} & loops\\}
\end{tabular}
\end{center}
\small
\onslide<3->{
\begin{center}
\begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {}}
\ldots\\
\bl{match ([]::rs) s} & \bl{$=$} & \bl{match rs s}\\
\ldots\\
\bl{match (r$^*$::rs) s} & \bl{$=$} & \bl{match rs s $\vee$ match (r::r$^*$::rs) s}\\
\end{tabular}
\end{center}}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}<1->[t]
\frametitle{Testing}
\begin{itemize}
\item While testing is an important part in the process of programming development\pause\ldots
\item we can only test a {\bf finite} amount of examples.\bigskip\pause
\begin{center}
\colorbox{cream}
{\gr{\begin{minipage}{10cm}
``Testing can only show the presence of errors, never their
absence.'' (Edsger W.~Dijkstra)
\end{minipage}}}
\end{center}\bigskip\pause
\item In a theorem prover we can establish properties that apply to
{\bf all} input and {\bf all} output.
\end{itemize}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}<1->[t]
\frametitle{Version 2}
\mbox{}\\[-14mm]\mbox{}
\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
\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{\;\;\;\;+ (if nullable r$_1$ then der c r$_2$ else $\varnothing$)}\\
\bl{der c (r$^*$)} & \bl{$=$} & \bl{(der c r) $\cdot$ r$^*$} &\smallskip\\
\bl{derivative r []} & \bl{$=$} & \bl{r} & \\
\bl{derivative r (c::s)} & \bl{$=$} & \bl{derivative (der c r) s} & \\
\end{tabular}\medskip
\bl{matches$_2$ r s $=$ nullable (derivative r s)}
\begin{textblock}{6}(9.5,0.9)
\begin{flushright}
\color{gray}``if r matches []''
\end{flushright}
\end{textblock}
\begin{textblock}{6}(9.5,6.18)
\begin{flushright}
\color{gray}``derivative w.r.t.~a char''
\end{flushright}
\end{textblock}
\begin{textblock}{6}(9.5,12.1)
\begin{flushright}
\color{gray}``deriv.~w.r.t.~a string''
\end{flushright}
\end{textblock}
\begin{textblock}{6}(9.5,13.98)
\begin{flushright}
\color{gray}``main''
\end{flushright}
\end{textblock}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}<1->[t]
\frametitle{Is the Matcher Error-Free?}
We expect that
\begin{center}
\begin{tabular}{lcl}
\bl{matches$_2$ r s = true} & \only<1>{\rd{$\Longrightarrow\,\,$}}\only<2>{\rd{$\Longleftarrow\,\,$}}%
\only<3->{\rd{$\Longleftrightarrow$}} & \bl{s $\in$ \LL(r)}\\
\bl{matches$_2$ r s = false} & \only<1>{\rd{$\Longrightarrow\,\,$}}\only<2>{\rd{$\Longleftarrow\,\,$}}%
\only<3->{\rd{$\Longleftrightarrow$}} & \bl{s $\notin$ \LL(r)}\\
\end{tabular}
\end{center}
\pause\pause\bigskip
By \alert<4->{induction}, we can {\bf prove} these properties.\bigskip
\begin{tabular}{lrcl}
Lemmas: & \bl{nullable (r)} & \bl{$\Longleftrightarrow$} & \bl{[] $\in$ \LL (r)}\\
& \bl{s $\in$ \LL (der c r)} & \bl{$\Longleftrightarrow$} & \bl{(c::s) $\in$ \LL (r)}\\
\end{tabular}
\only<4->{
\begin{textblock}{3}(0.9,4.5)
\rd{\huge$\forall$\large{}r s.}
\end{textblock}}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}<1>[c]
\frametitle{
\begin{tabular}{c}
\mbox{}\\[23mm]
\LARGE Demo
\end{tabular}}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}<1->[t]
\mbox{}\\[-2mm]
\small
\begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}ll@ {}}
\bl{nullable (NULL)} & \bl{$=$} & \bl{false} &\\
\bl{nullable (EMPTY)} & \bl{$=$} & \bl{true} &\\
\bl{nullable (CHR c)} & \bl{$=$} & \bl{false} &\\
\bl{nullable (ALT r$_1$ r$_2$)} & \bl{$=$} & \bl{(nullable r$_1$) orelse (nullable r$_2$)} & \\
\bl{nullable (SEQ r$_1$ r$_2$)} & \bl{$=$} & \bl{(nullable r$_1$) andalso (nullable r$_2$)} & \\
\bl{nullable (STAR r)} & \bl{$=$} & \bl{true} & \\
\end{tabular}\medskip
\begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{-10mm}}l@ {}}
\bl{der c (NULL)} & \bl{$=$} & \bl{NULL} & \\
\bl{der c (EMPTY)} & \bl{$=$} & \bl{NULL} & \\
\bl{der c (CHR d)} & \bl{$=$} & \bl{if c=d then EMPTY else NULL} & \\
\bl{der c (ALT r$_1$ r$_2$)} & \bl{$=$} & \bl{ALT (der c r$_1$) (der c r$_2$)} & \\
\bl{der c (SEQ r$_1$ r$_2$)} & \bl{$=$} & \bl{ALT (SEQ (der c r$_1$) r$_2$)} & \\
& & \bl{\phantom{ALT} (if nullable r$_1$ then der c r$_2$ else NULL)}\\
\bl{der c (STAR r)} & \bl{$=$} & \bl{SEQ (der c r) (STAR r)} &\smallskip\\
\bl{derivative r []} & \bl{$=$} & \bl{r} & \\
\bl{derivative r (c::s)} & \bl{$=$} & \bl{derivative (der c r) s} & \\
\end{tabular}\medskip
\bl{matches r s $=$ nullable (derivative r s)}
\only<2>{
\begin{textblock}{8}(1.5,4)
\includegraphics[scale=0.3]{approved.png}
\end{textblock}}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{No Automata?}
You might be wondering why I did not use any automata?
\begin{itemize}
\item {\bf Def.:} A \alert{regular language} is one where there is a DFA that
recognises it.\bigskip\pause
\end{itemize}
There are many reasons why this is a good definition:\medskip
\begin{itemize}
\item pumping lemma
\item closure properties of regular languages\\ (e.g.~closure under complement)
\end{itemize}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[t]
\frametitle{Really Bad News!}
DFAs are bad news for formalisations in theorem provers. They might
be represented as:
\begin{itemize}
\item graphs
\item matrices
\item partial functions
\end{itemize}
All constructions are messy to reason about.\bigskip\bigskip
\pause
\small
\only<2>{
Constable et al needed (on and off) 18 months for a 3-person team
to formalise automata theory in Nuprl including Myhill-Nerode. There is
only very little other formalised work on regular languages I know of
in Coq, Isabelle and HOL.}
\only<3>{Typical textbook reasoning goes like: ``\ldots if \smath{M} and \smath{N} are any two
automata with no inaccessible states \ldots''
}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{}
\large
\begin{center}
\begin{tabular}{p{9cm}}
My point:\bigskip\\
The theory about regular languages can be reformulated
to be more\\ suitable for theorem proving.
\end{tabular}
\end{center}
\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 (pumping lemma only necessary)\medskip
\item will help with closure properties of regular languages\bigskip\pause
\item key is the equivalence relation:\smallskip
\begin{center}
\smath{x \approx_{L} y \,\dn\, \forall z.\; x @ z \in L \Leftrightarrow y @ z \in L}
\end{center}
\end{itemize}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{\LARGE The Myhill-Nerode Theorem}
\mbox{}\\[5cm]
\begin{itemize}
\item \smath{\text{finite}\, (U\!N\!IV /\!/ \approx_L) \;\Leftrightarrow\; L\; \text{is regular}}
\end{itemize}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{\LARGE Equivalence Classes}
\begin{itemize}
\item \smath{L = []}
\begin{center}
\smath{\Big\{\{[]\},\; U\!N\!IV - \{[]\}\Big\}}
\end{center}\bigskip\bigskip
\item \smath{L = [c]}
\begin{center}
\smath{\Big\{\{[]\},\; \{[c]\},\; U\!N\!IV - \{[], [c]\}\Big\}}
\end{center}\bigskip\bigskip
\item \smath{L = \varnothing}
\begin{center}
\smath{\Big\{U\!N\!IV\Big\}}
\end{center}
\end{itemize}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{\LARGE Regular Languages}
\begin{itemize}
\item \smath{L} is regular \smath{\dn} if there is an automaton \smath{M}
such that \smath{\mathbb{L}(M) = L}\\[1.5cm]
\item Myhill-Nerode:
\begin{center}
\begin{tabular}{l}
finite $\Rightarrow$ regular\\
\;\;\;\smath{\text{finite}\,(U\!N\!IV /\!/ \approx_L) \Rightarrow \exists r.\; L = \mathbb{L}(r)}\\[3mm]
regular $\Rightarrow$ finite\\
\;\;\;\smath{\text{finite}\, (U\!N\!IV /\!/ \approx_{\mathbb{L}(r)})}
\end{tabular}
\end{center}
\end{itemize}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{\LARGE Final Equiv.~Classes}
\mbox{}\\[3cm]
\begin{itemize}
\item \smath{\text{finals}\,L \dn
\{{\lbrack\mkern-2mu\lbrack{s}\rbrack\mkern-2mu\rbrack}_\approx\;|\; s \in L\}}\\
\medskip
\item we can prove: \smath{L = \bigcup (\text{finals}\,L)}
\end{itemize}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{\LARGE Transitions between ECs}
\smath{L = \{[c]\}}
\begin{tabular}{@ {\hspace{-7mm}}cc}
\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]
%\draw[help lines] (0,0) grid (3,2);
\node[state,initial] (q_0) {$R_1$};
\node[state,accepting] (q_1) [above right of=q_0] {$R_2$};
\node[state] (q_2) [below right of=q_0] {$R_3$};
\path[->] (q_0) edge node {c} (q_1)
edge node [swap] {$\Sigma-{c}$} (q_2)
(q_2) edge [loop below] node {$\Sigma$} ()
(q_1) edge node {$\Sigma$} (q_2);
\end{tikzpicture}
\end{tabular}
&
\begin{tabular}[t]{ll}
\\[-20mm]
\multicolumn{2}{l}{\smath{U\!N\!IV /\!/\approx_L} produces}\\[4mm]
\smath{R_1}: & \smath{\{[]\}}\\
\smath{R_2}: & \smath{\{[c]\}}\\
\smath{R_3}: & \smath{U\!N\!IV - \{[], [c]\}}\\[6mm]
\multicolumn{2}{l}{\onslide<2->{\smath{X \stackrel{c}{\longrightarrow} Y \dn X ;; [c] \subseteq Y}}}
\end{tabular}
\end{tabular}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{\LARGE Systems of Equations}
Inspired by a method of Brzozowski\;'64, we can build an equational system
characterising the equivalence classes:
\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) {$R_1$};
\node[state,accepting] (p_1) [right of=q_0] {$R_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{R_1} & \smath{\equiv} & \smath{R_1;b + R_2;b \onslide<2->{\alert<2>{+ \lambda;[]}}}\\
& \smath{R_2} & \smath{\equiv} & \smath{R_1;a + R_2;a}\medskip\\
\onslide<3->{we can prove}
& \onslide<3->{\smath{R_1}} & \onslide<3->{\smath{=}}
& \onslide<3->{\smath{R_1;; \mathbb{L}(b) \,\cup\, R_2;;\mathbb{L}(b) \,\cup\, \{[]\}}}\\
& \onslide<3->{\smath{R_2}} & \onslide<3->{\smath{=}}
& \onslide<3->{\smath{R_1;; \mathbb{L}(a) \,\cup\, R_2;;\mathbb{L}(a)}}\\
\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{R_1}} & \onslide<1->{\smath{=}}
& \onslide<1->{\smath{R_1; b + R_2; b + \lambda;[]}}\\
\onslide<1->{\smath{R_2}} & \onslide<1->{\smath{=}}
& \onslide<1->{\smath{R_1; a + R_2; a}}\\
& & & \onslide<2->{by Arden}\\
\onslide<2->{\smath{R_1}} & \onslide<2->{\smath{=}}
& \onslide<2->{\smath{R_1; b + R_2; b + \lambda;[]}}\\
\onslide<2->{\smath{R_2}} & \onslide<2->{\smath{=}}
& \only<2>{\smath{R_1; a + R_2; a}}%
\only<3->{\smath{R_1; a\cdot a^\star}}\\
& & & \onslide<4->{by Arden}\\
\onslide<4->{\smath{R_1}} & \onslide<4->{\smath{=}}
& \onslide<4->{\smath{R_2; b \cdot b^\star+ \lambda;b^\star}}\\
\onslide<4->{\smath{R_2}} & \onslide<4->{\smath{=}}
& \onslide<4->{\smath{R_1; a\cdot a^\star}}\\
& & & \onslide<5->{by substitution}\\
\onslide<5->{\smath{R_1}} & \onslide<5->{\smath{=}}
& \onslide<5->{\smath{R_1; a\cdot a^\star \cdot b \cdot b^\star+ \lambda;b^\star}}\\
\onslide<5->{\smath{R_2}} & \onslide<5->{\smath{=}}
& \onslide<5->{\smath{R_1; a\cdot a^\star}}\\
& & & \onslide<6->{by Arden}\\
\onslide<6->{\smath{R_1}} & \onslide<6->{\smath{=}}
& \onslide<6->{\smath{\lambda;b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star}}\\
\onslide<6->{\smath{R_2}} & \onslide<6->{\smath{=}}
& \onslide<6->{\smath{R_1; a\cdot a^\star}}\\
& & & \onslide<7->{by substitution}\\
\onslide<7->{\smath{R_1}} & \onslide<7->{\smath{=}}
& \onslide<7->{\smath{\lambda;b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star}}\\
\onslide<7->{\smath{R_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}
\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->[t]
\small
\begin{center}
\begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}ll}
\onslide<1->{\smath{R_1}} & \onslide<1->{\smath{=}}
& \onslide<1->{\smath{R_1; b + R_2; b + \lambda;[]}}\\
\onslide<1->{\smath{R_2}} & \onslide<1->{\smath{=}}
& \onslide<1->{\smath{R_1; a + R_2; a}}\\
& & & \onslide<2->{by Arden}\\
\onslide<2->{\smath{R_1}} & \onslide<2->{\smath{=}}
& \onslide<2->{\smath{R_1; b + R_2; b + \lambda;[]}}\\
\onslide<2->{\smath{R_2}} & \onslide<2->{\smath{=}}
& \only<2>{\smath{R_1; a + R_2; a}}%
\only<3->{\smath{R_1; a\cdot a^\star}}\\
& & & \onslide<4->{by Arden}\\
\onslide<4->{\smath{R_1}} & \onslide<4->{\smath{=}}
& \onslide<4->{\smath{R_2; b \cdot b^\star+ \lambda;b^\star}}\\
\onslide<4->{\smath{R_2}} & \onslide<4->{\smath{=}}
& \onslide<4->{\smath{R_1; a\cdot a^\star}}\\
& & & \onslide<5->{by substitution}\\
\onslide<5->{\smath{R_1}} & \onslide<5->{\smath{=}}
& \onslide<5->{\smath{R_1; a\cdot a^\star \cdot b \cdot b^\star+ \lambda;b^\star}}\\
\onslide<5->{\smath{R_2}} & \onslide<5->{\smath{=}}
& \onslide<5->{\smath{R_1; a\cdot a^\star}}\\
& & & \onslide<6->{by Arden}\\
\onslide<6->{\smath{R_1}} & \onslide<6->{\smath{=}}
& \onslide<6->{\smath{\lambda;b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star}}\\
\onslide<6->{\smath{R_2}} & \onslide<6->{\smath{=}}
& \onslide<6->{\smath{R_1; a\cdot a^\star}}\\
& & & \onslide<7->{by substitution}\\
\onslide<7->{\smath{R_1}} & \onslide<7->{\smath{=}}
& \onslide<7->{\smath{\lambda;b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star}}\\
\onslide<7->{\smath{R_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) {$R_1$};
\node[state,accepting] (p_1) [right of=q_0] {$R_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}}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{\LARGE The Equ's Solving Algorithm}
\begin{itemize}
\item The algorithm must terminate: Arden makes one equation smaller;
substitution deletes one variable from the right-hand sides.\bigskip
\item We need to maintain the invariant that Arden is applicable
(if \smath{[] \not\in A} then \ldots):\medskip
\begin{center}\small
\begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}ll}
\smath{R_1} & \smath{=} & \smath{R_1; b + R_2; b + \lambda;[]}\\
\smath{R_2} & \smath{=} & \smath{R_1; a + R_2; a}\\
& & & by Arden\\
\smath{R_1} & \smath{=} & \smath{R_1; b + R_2; b + \lambda;[]}\\
\smath{R_2} & \smath{=} & \smath{R_1; a\cdot a^\star}\\
\end{tabular}
\end{center}
\end{itemize}
\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_{\mathbb{L}(r)})}
\end{center}
by induction on \smath{r}. This is straightforward for \\the base cases:\small
\begin{center}
\begin{tabular}{l@ {\hspace{1mm}}l}
\smath{U\!N\!IV /\!/ \!\approx_{\emptyset}} & \smath{= \{U\!N\!IV\}}\smallskip\\
\smath{U\!N\!IV /\!/ \!\approx_{\{[]\}}} & \smath{\subseteq \{\{[]\}, U\!N\!IV - \{[]\}\}}\smallskip\\
\smath{U\!N\!IV /\!/ \!\approx_{\{[c]\}}} & \smath{\subseteq \{\{[]\}, \{[c]\}, U\!N\!IV - \{[], [c]\}\}}
\end{tabular}
\end{center}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[t]
\frametitle{\LARGE The Other Direction}
More complicated are the inductive cases:\\ one needs to prove that if
\begin{center}
\smath{\text{finite} (U\!N\!IV /\!/ \approx_{\mathbb{L}(r_1)})}\hspace{3mm}
\smath{\text{finite} (U\!N\!IV /\!/ \approx_{\mathbb{L}(r_2)})}
\end{center}
then
\begin{center}
\smath{\text{finite} (U\!N\!IV /\!/ \approx_{\mathbb{L}(r_1) \,\cup\, \mathbb{L}(r_2)})}
\end{center}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[t]
\frametitle{\LARGE Helper Lemma}
\begin{center}
\begin{tabular}{p{10cm}}
%If \smath{\text{finite} (f\;' A)} and \smath{f} is injective
%(on \smath{A}),\\ then \smath{\text{finite}\,A}.
Given two equivalence relations \smath{R_1} and \smath{R_2} with
\smath{R_1} refining \smath{R_2} (\smath{R_1 \subseteq R_2}).\\
Then\medskip\\
\smath{\;\;\text{finite} (U\!N\!IV /\!/ R_1) \Rightarrow \text{finite} (U\!N\!IV /\!/ R_2)}
\end{tabular}
\end{center}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{\Large Derivatives and Left-Quotients}
\small
Work by Brozowski ('64) and Antimirov ('96):\pause\smallskip
\begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{-10mm}}l@ {}}
\multicolumn{4}{@ {}l}{Left-Quotient:}\\
\multicolumn{4}{@ {}l}{\bl{$\text{Ders}\;\text{s}\,A \dn \{\text{s'} \;|\; \text{s @ s'} \in A\}$}}\bigskip\\
\multicolumn{4}{@ {}l}{Derivative:}\\
\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{\;\;\;\;+ (if nullable r$_1$ then der c r$_2$ else $\varnothing$)}\\
\bl{der c (r$^*$)} & \bl{$=$} & \bl{(der c r) $\cdot$ r$^*$} &\smallskip\\
\bl{ders [] r} & \bl{$=$} & \bl{r} & \\
\bl{ders (s @ [c]) r} & \bl{$=$} & \bl{der c (ders s r)} & \\
\end{tabular}\pause
\begin{center}
\alert{$\Rightarrow$}\smath{\;\;\text{Ders}\,\text{s}\,(\mathbb{L}(\text{r})) = \mathbb{L} (\text{ders s r})}
\end{center}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{\LARGE Left-Quotients and MN-Rels}
\begin{itemize}
\item \smath{x \approx_{A} y \,\dn\, \forall z.\; x @ z \in A \Leftrightarrow y @ z \in A}\medskip
\item \bl{$\text{Ders}\;s\,A \dn \{s' \;|\; s @ s' \in A\}$}
\end{itemize}\bigskip
\begin{center}
\smath{x \approx_A y \Longleftrightarrow \text{Ders}\;x\;A = \text{Ders}\;y\;A}
\end{center}\bigskip\pause\small
which means
\begin{center}
\smath{x \approx_{\mathbb{L}(r)} y \Longleftrightarrow
\mathbb{L}(\text{ders}\;x\;r) = \mathbb{L}(\text{ders}\;y\;r)}
\end{center}\pause
\hspace{8.8mm}or
\smath{\;x \approx_{\mathbb{L}(r)} y \Longleftarrow
\text{ders}\;x\;r = \text{ders}\;y\;r}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{\LARGE Partial Derivatives}
Antimirov: \bl{pder : rexp $\Rightarrow$ rexp set}\bigskip
\begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{-10mm}}l@ {}}
\bl{pder c ($\varnothing$)} & \bl{$=$} & \bl{\{$\varnothing$\}} & \\
\bl{pder c ([])} & \bl{$=$} & \bl{\{$\varnothing$\}} & \\
\bl{pder c (d)} & \bl{$=$} & \bl{if c = d then \{[]\} else \{$\varnothing$\}} & \\
\bl{pder c (r$_1$ + r$_2$)} & \bl{$=$} & \bl{(pder c r$_1$) $\cup$ (pder c r$_2$)} & \\
\bl{pder c (r$_1$ $\cdot$ r$_2$)} & \bl{$=$} & \bl{(pder c r$_1$) $\odot$ r$_2$} & \\
& & \bl{\hspace{-10mm}$\cup$ (if nullable r$_1$ then pder c r$_2$ else $\varnothing$)}\\
\bl{pder c (r$^*$)} & \bl{$=$} & \bl{(pder c r) $\odot$ r$^*$} &\smallskip\\
\end{tabular}
\begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{-10mm}}l@ {}}
\bl{pders [] r} & \bl{$=$} & \bl{r} & \\
\bl{pders (s @ [c]) r} & \bl{$=$} & \bl{pder c (pders s r)} & \\
\end{tabular}\pause
\begin{center}
\alert{$\Rightarrow$}\smath{\;\;\text{Ders}\,\text{s}\,(\mathbb{L}(\text{r})) = \bigcup (\mathbb{L}\;`\; (\text{pders s r}))}
\end{center}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[t]
\frametitle{\LARGE Final Result}
\mbox{}\\[7mm]
\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_1}}}
refines \bl{x $\approx_{\mathbb{L}(\text{r})}$ y}\pause
\item \smath{\text{finite} (U\!N\!IV /\!/ R_1)} \bigskip\pause
\item Therefore \smath{\text{finite} (U\!N\!IV /\!/ \approx_{\mathbb{L}(r)})}. Qed.
\end{itemize}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{\LARGE What Have We Achieved?}
\begin{itemize}
\item \smath{\text{finite}\, (U\!N\!IV /\!/ \approx_L) \;\Leftrightarrow\; L\; \text{is regular}}
\bigskip\pause
\item regular languages are closed under complementation; this is now easy\medskip
\begin{center}
\smath{U\!N\!IV /\!/ \approx_L \;\;=\;\; U\!N\!IV /\!/ \approx_{-L}}
\end{center}
\end{itemize}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{\LARGE Examples}
\begin{itemize}
\item \smath{L \equiv \Sigma^\star 0 \Sigma} is regular
\begin{quote}\small
\begin{tabular}{lcl}
\smath{A_1} & \smath{=} & \smath{\Sigma^\star 00}\\
\smath{A_2} & \smath{=} & \smath{\Sigma^\star 01}\\
\smath{A_3} & \smath{=} & \smath{\Sigma^\star 10 \cup \{0\}}\\
\smath{A_4} & \smath{=} & \smath{\Sigma^\star 11 \cup \{1\} \cup \{[]\}}\\
\end{tabular}
\end{quote}
\item \smath{L \equiv \{ 0^n 1^n \,|\, n \ge 0\}} is not regular
\begin{quote}\small
\begin{tabular}{lcl}
\smath{B_0} & \smath{=} & \smath{\{0^n 1^n \,|\, n \ge 0\}}\\
\smath{B_1} & \smath{=} & \smath{\{0^n 1^{(n-1)} \,|\, n \ge 1\}}\\
\smath{B_2} & \smath{=} & \smath{\{0^n 1^{(n-2)} \,|\, n \ge 2\}}\\
\smath{B_3} & \smath{=} & \smath{\{0^n 1^{(n-3)} \,|\, n \ge 3\}}\\
& \smath{\vdots} &\\
\end{tabular}
\end{quote}
\end{itemize}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{\LARGE What We Have Not Achieved}
\begin{itemize}
\item regular expressions are not good if you look for a minimal
one for a language (DFAs have this notion)\pause\bigskip
\item Is there anything to be said about context free languages:\medskip
\begin{quote}
A context free language is where every string can be recognised by
a pushdown automaton.\bigskip
\end{quote}
\end{itemize}
\textcolor{gray}{\footnotesize Yes. Derivatives also work for c-f grammars. Ongoing work.}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{\LARGE Conclusion}
\begin{itemize}
\item We formalised the Myhill-Nerode theorem based on
regular expressions only (DFAs are difficult to deal with in a theorem prover).\smallskip
\item Seems to be a common theme: algorithms need to be reformulated
to better suit formal treatment.\smallskip
\item The most interesting aspect is that we are able to
implement the matcher directly inside the theorem prover
(ongoing work).\smallskip
\item Parsing is a vast field which seem to offer new results.
\end{itemize}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}<1>[b]
\frametitle{
\begin{tabular}{c}
\mbox{}\\[13mm]
\alert{\LARGE Thank you very much!}\\
\alert{\Large Questions?}
\end{tabular}}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
(*<*)
end
(*>*)