% !TEX program = xelatex
\documentclass[dvipsnames,14pt,t,xelatex,aspectratio=169,xcolor={table}]{beamer}
\usepackage{../slides}
\usepackage{../graphicss}
\usepackage{../langs}
\usepackage{../data}

\usepackage{tcolorbox}
\newtcolorbox{mybox}{colback=red!5!white,colframe=red!75!black}
\newtcolorbox{mybox2}[1]{colback=red!5!white,colframe=red!75!black,fonttitle=\bfseries,title=#1}
\newtcolorbox{mybox3}[1]{colback=Cyan!5!white,colframe=Cyan!75!black,fonttitle=\bfseries,title=#1}



\hfuzz=220pt 

\lstset{language=Scala,
        style=mystyle,
        numbersep=0pt,
        numbers=none,
        xleftmargin=0mm}

\pgfplotsset{compat=1.17}

\newcommand{\bl}[1]{\textcolor{blue}{#1}}     

% beamer stuff 
\renewcommand{\slidecaption}{CFL 02, King's College London}


\begin{document}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[t]
\frametitle{%
  \begin{tabular}{@ {}c@ {}}
  \\[-3mm]
  \LARGE Compilers and \\[-1mm] 
  \LARGE Formal Languages\\[-5mm] 
  \end{tabular}}

  \normalsize
  \begin{center}
  \begin{tabular}{ll}
  Email:  & christian.urban at kcl.ac.uk\\
  Office Hour: & Friday 11:30 -- 12:30\\  
  Location: & N7.07 (North Wing, Bush House)\\
  Slides \& Progs: & KEATS\\
  \end{tabular}
  \end{center}

  \begin{center}
    \begin{tikzpicture}
      \node[drop shadow,fill=white,inner sep=0pt] 
      {\footnotesize\rowcolors{1}{capri!10}{white}
        \begin{tabular}{|p{4.8cm}|p{4.8cm}|}\hline
          1 Introduction, Languages          & 6 While-Language \\
          \cellcolor{blue!50}
          2 Regular Expressions, Derivatives & 7 Compilation, JVM \\
          3 Automata, Regular Languages      & 8 Compiling Functional Languages \\
          4 Lexing, Tokenising               & 9 Optimisations \\
          5 Grammars, Parsing                & 10 LLVM \\ \hline
        \end{tabular}%
      };
    \end{tikzpicture}
  \end{center}


  \begin{textblock}{5}(12,3)
  \includegraphics[scale=0.35]{qr01}\\
  \small{}Wifi: Lincoln's Inn\\
  \small{}Pwd: 0207\,4051\,393
  \end{textblock} 
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%\begin{frame}[c]
%
%\begin{mybox3}{From Pollev last week}\it    
%Will C++ users be publicly shamed and humiliated in front of the class?
%\end{mybox3}  
%
%\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]

\begin{center}
\begin{tabular}{c}
\includegraphics[scale=0.024]{awards.jpeg}\\
\small I try my best, but \ldots\ldots\ldots\ldots\textcolor{gray}{server, venue}
\end{tabular} 
\end{center} 
\mbox{}
\end{frame}

{
\setbeamercolor{background canvas}{bg=cream}
\begin{frame}<1-2>[c]
\end{frame}
}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[t]

\mbox{}\\[-20mm]\mbox{}

\tt
\begin{center}\large
\code{"if x = 42 then x := x + 1 else x := x - 1"}
\end{center}\small


\begin{tabular}{@{}l@{\hspace{18mm}}l}
KEYWORD: \\
\hspace{5mm}{if}, {then}, {else},\ldots\\ 
WHITESPACE:\\
\hspace{5mm}{" "}, {$\backslash$n}, {$\backslash$r}\\ 
IDENTIFIER:\\
\hspace{5mm}LETTER $\cdot$ (LETTER + DIGIT + {\_})$^*$ & LETTER: [a-zA-Z]\\ 
NUM: & DIGIT: [0-9]\\
\hspace{5mm}(NONZERODIGIT $\cdot$ DIGIT$^*$) + {0} & NONZERODIGIT: [1-9]\\
NUMBER:\\
\hspace{5mm}NUM +  (\texttt{"-"} $\cdot$ NUM)\\
OP:\\
\hspace{5mm}=, :=, +, -, *, \%, <, =<,\ldots\\
COMMENT:\\
\hspace{5mm}{$\slash$*} $\cdot$ $\sim$(ALL$^*$ $\cdot$ (*$\slash$) $\cdot$ ALL$^*$) $\cdot$ {*$\slash$}
\end{tabular}

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  

{
\setbeamercolor{background canvas}{bg=cream}
\begin{frame}<1-4>[c]
\end{frame}
}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[t]
  \frametitle{
    Let's Implement an Efficient\\[-2mm] 
    Regular Expression Matcher}

\footnotesize
\begin{center}
  {\normalsize Graphs: \bl{$a^{?\{n\}} \cdot a^{\{n\}}$} and strings \bl{$\underbrace{\,a\ldots a\,}_{n}$}}\\[-2mm]
\begin{tabular}{@{}cc@{}}
\begin{tikzpicture}
\begin{axis}[
    title={Graph: $\texttt{(a*)*\,b}$ and strings 
           $\underbrace{\texttt{a}\ldots \texttt{a}}_{n}$},
    xlabel={$n$},
    x label style={at={(1.05,0.0)}},
    ylabel={time in secs},
    enlargelimits=false,
    xtick={0,5,...,30},
    xmax=33,
    ymax=35,
    ytick={0,5,...,30},
    scaled ticks=false,
    axis lines=left,
    width=5.5cm,
    height=4.5cm, 
    legend entries={Python, Java 8, JavaScript, Swift},  
    legend pos=north west,
    legend cell align=left]
\addplot[blue,mark=*, mark options={fill=white}] table {re-python2.data};
\addplot[cyan,mark=*, mark options={fill=white}] table {re-java.data};
\addplot[red,mark=*, mark options={fill=white}] table {re-js.data};
\addplot[magenta,mark=*, mark options={fill=white}] table {re-swift.data};
\end{axis}
\end{tikzpicture}
&
\begin{tikzpicture}
  \begin{axis}[
    xlabel={$n$},
    x label style={at={(1.1,0.05)}},
    ylabel={time in secs},
    enlargelimits=false,
    xtick={0,5000,...,10000},
    xmax=11500,
    ymax=35,
    ytick={0,5,...,30},
    scaled ticks=false,
    axis lines=left,
    width=5cm,
    height=4.5cm,
    legend entries={Scala V2,Scala V3},
    legend pos=north east,
    legend cell align=left]
\addplot[green,mark=square*,mark options={fill=white}] table {re2.data};
\addplot[black,mark=square*,mark options={fill=white}] table {re3.data};
\end{axis}
\end{tikzpicture}
\end{tabular}
\end{center}

\small
\begin{textblock}{14}(1,14.6)
In the handouts is a similar graph for \bl{$(a^*)^* \cdot b$} and Java, 
JavaScript, Python and more.
\end{textblock}
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

{
\setbeamercolor{background canvas}{bg=cream}
\begin{frame}<1-4>[c]
\end{frame}
}



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%\begin{frame}[c]
%\frametitle{Evil Regular Expressions}
%
%\begin{itemize}
%\item \alert{R}egular \alert{e}xpression \alert{D}enial \alert{o}f \alert{S}ervice (ReDoS)\bigskip
%\item Evil regular expressions\medskip
%\begin{itemize}
%\item \bl{$a^{?\{n\}} \cdot a^{\{n\}}$}
%\item \bl{$(a^*)^*$}
%\item \bl{$([a$\,-\,$z]^+)^*$}
%\item \bl{$(a + a \cdot a)^*$}
%\item \bl{$(a + a^?)^*$}
%\end{itemize}
%
%\item sometimes also called \alert{catastrophic backtracking}\bigskip
%\item \small\ldots I hope you have watched the video by the
%  StackExchange engineer  
%\end{itemize}
%
%\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
\frametitle{(Basic) Regular Expressions}

Their inductive definition:

\begin{center}
  \begin{tabular}{@ {}rrl@ {\hspace{13mm}}l}
  \bl{$r$} & \bl{$::=$}  & \bl{$\ZERO$}  & nothing\\
         & \bl{$\mid$} & \bl{$\ONE$}       & empty string / \pcode{""} / $[]$\\
         & \bl{$\mid$} & \bl{$c$}                         & character\\
         & \bl{$\mid$} & \bl{$r_1 + r_2$}  & alternative / choice\\
         & \bl{$\mid$} & \bl{$r_1 \cdot r_2$} & sequence\\
         & \bl{$\mid$} & \bl{$r^*$}            & star (zero or more)\\
  \end{tabular}
\end{center}
\vspace{\fill}

%%Q: \;What about \;\bl{$r \cdot 0$} \; ?
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
  \frametitle{
   When Are Two Regular\\[-1mm]
   Expressions Equivalent?}
  
   \begin{bubble}[10cm]
    \large
    Two regular expressions \bl{$r_1$} and \bl{$r_2$} are
    \alert{\bf{}equivalent} 
    provided:\medskip 
    \begin{center}
      \bl{$r_1 \equiv r_2 \;\;\dn\;\; L(r_1) = L(r_2)$}  
    \end{center}\medskip
    \end{bubble}

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
  
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
\frametitle{Some Concrete Equivalences}

\begin{center}
\bl{\begin{tabular}{rcl}
$(a + b)  + c$ & $\equiv$ & $a + (b + c)$\\
$a + a$        & $\equiv$ & $a$\\
$a + b$        & $\equiv$ & $b + a$\\
$(a \cdot b) \cdot c$ & $\equiv$ & $a \cdot (b \cdot c)$\\
$c \cdot (a + b)$ & $\equiv$ & $(c \cdot a) + (c \cdot b)$\bigskip\bigskip\\\pause
$a \cdot a$       & $\not\equiv$ & $a$\\
$a + (b \cdot c)$ & $\not\equiv$ & $(a + b) \cdot (a + c)$\\
\end{tabular}}
\end{center}

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
\frametitle{Some Corner Cases}

\begin{center}
\bl{\begin{tabular}{rcl}
$a \cdot \ZERO$ & $\not\equiv$ & $a$\\
$a + \ONE$ & $\not\equiv$ & $a$\\
$\ONE$ & $\equiv$ & $\ZERO^*$\\
$\ONE^*$ & $\equiv$ & $\ONE$\\
$\ZERO^*$ & $\not\equiv$ & $\ZERO$\\
\end{tabular}}
\end{center}

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
  
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
\frametitle{Some Simplification Rules}
 
\begin{center}
\bl{\begin{tabular}{rcl}
$r + \ZERO$  & $\equiv$ & $r$\\
$\ZERO + r$  & $\equiv$ & $r$\\
$r \cdot \ONE$ & $\equiv$ & $r$\\
$\ONE \cdot r$     & $\equiv$ & $r$\\
$r \cdot \ZERO$ & $\equiv$ & $\ZERO$\\
$\ZERO \cdot r$ & $\equiv$ & $\ZERO$\\
$r + r$ & $\equiv$ & $r$
\end{tabular}}
\end{center}
 
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
  
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
\frametitle{Simplification Example}

%%Given \bl{$r \dn ((a \cdot b) + b)^*$}, you can simplify as follows

\begin{center}
\def\arraystretch{2}  
\begin{tabular}{@{}lcl}
  \bl{$((\ONE \cdot b) + \ZERO) \cdot r$}
    & \bl{$\Rightarrow$} & \bl{$((\underline{\ONE \cdot b}) + \ZERO) \cdot r$}\\
    & \bl{$=$} & \bl{$(\underline{b + \ZERO}) \cdot r$}\\
    & \bl{$=$} & \bl{$b \cdot r$}\\
\end{tabular}
\end{center}

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
\frametitle{Simplification Example}

%%Given \bl{$r \dn ((a \cdot b) + b)^*$}, you can simplify as follows

\begin{center}
\def\arraystretch{2}  
\begin{tabular}{@{}lcl}
  \bl{$((\ZERO \cdot b) + \ZERO) \cdot r$}
    & \bl{$\Rightarrow$} & \bl{$((\underline{\ZERO \cdot b}) + \ZERO) \cdot r$}\\
    & \bl{$=$} & \bl{$(\underline{\ZERO + \ZERO}) \cdot r$}\\
    & \bl{$=$} & \bl{$\ZERO \cdot r$}\\
    & \bl{$=$} & \bl{$\ZERO$}\\
\end{tabular}
\end{center}

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[t]
\frametitle{Semantic Derivative\\[5mm]}

\begin{itemize}
\item The \alert{\bf Semantic Derivative} of a 
\underline{language}\\ w.r.t.~to a character \bl{$c$}:
\bigskip

\begin{center}
\bl{$\Der\,c\,A \dn \{ s \;|\;  c\!::\!s \in A\}$ } 
\end{center}\bigskip

For \bl{$A = \{\mathit{foo}, \mathit{bar}, \mathit{frak}\}$} then

\begin{center}
\bl{\begin{tabular}{l@{\hspace{2mm}}c@{\hspace{2mm}}l}
$\Der\,f\,A$ & $=$ & $\{\mathit{oo}, \mathit{rak}\}$\\
$\Der\,b\,A$ & $=$ &  $\{\mathit{ar}\}$\\  
$\Der\,a\,A$ & $=$ & $\{\}$\pause
\end{tabular}}
\end{center}\medskip


We can extend this definition to strings
\[
\bl{\Ders\,s\,A = \{s'\;|\;s\,@\,s' \in A\}}
\]

\end{itemize}
 
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
\frametitle{The Specification for Matching}

\begin{bubble}[10cm]
\large
A regular expression \bl{$r$} matches a string~\bl{$s$} 
provided:
\begin{center}
\bl{$s \in L(r)$} 
\end{center}\medskip
\end{bubble}

\bigskip\bigskip

\ldots and the point of the this lecture is to decide this problem as
fast as possible (unlike Python, Ruby, Java etc)

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
\frametitle{\mbox{Brzozowski's Algorithm (1)}}


\ldots{}whether a regular expression can match the empty string:
\begin{center}
\begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {}}
\bl{$nullable(\ZERO)$}    & \bl{$\dn$} & \bl{\textit{false}}\\
\bl{$nullable(\ONE)$}       & \bl{$\dn$} & \bl{\textit{true}}\\
\bl{$nullable (c)$}             & \bl{$\dn$} & \bl{\textit{false}}\\
\bl{$nullable (r_1 + r_2)$}     & \bl{$\dn$} & \bl{$nullable(r_1) \vee nullable(r_2)$} \\ 
\bl{$nullable (r_1 \cdot r_2)$} & \bl{$\dn$} & \bl{$nullable(r_1) \wedge nullable(r_2)$} \\
\bl{$nullable (r^*)$}           & \bl{$\dn$} & \bl{\textit{true}}\\
\end{tabular}
\end{center}

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%\begin{frame}[c]
%
%\bl{$r ::= \ZERO \,\;|\;\, \ONE \,\;|\;\, c \,\;|\;\, r_1 + r_2 \,\;|\;\, r_1 \cdot r_2 \,\;|\;\, r^{*} \,\;|\;\, r^{\{n\}}$}  
%
%\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   




%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
\frametitle{The Derivative of a Rexp}

\large
If \bl{$r$} matches the string \bl{$c\!::\!s$}, what is a regular 
expression that matches just \bl{$s$}?\bigskip\bigskip\bigskip\bigskip

\small
\bl{$\der\,c\,r$} gives the answer, Brzozowski 1964
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
\frametitle{The Derivative of a Rexp}

\begin{center}
\begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{-10mm}}l@ {}}
  \bl{$\der\, c\, (\ZERO)$}      & \bl{$\dn$} & \bl{$\ZERO$} & \\
  \bl{$\der\, c\, (\ONE)$}           & \bl{$\dn$} & \bl{$\ZERO$} & \\
  \bl{$\der\, c\, (d)$}                     & \bl{$\dn$} & \bl{if $c = d$ then $\ONE$ else $\ZERO$} & \\
  \bl{$\der\, c\, (r_1 + r_2)$}        & \bl{$\dn$} & \bl{$\der\, c\, r_1 + \der\, c\, r_2$} & \\
  \bl{$\der\, c\, (r_1 \cdot r_2)$}  & \bl{$\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$}\\
  \bl{$\der\, c\, (r^*)$}  & \bl{$\dn$} & \bl{$(\der\,c\,r) \cdot (r^*)$} &\medskip\bigskip\\\pause

  \bl{$\ders\, []\, r$}     & \bl{$\dn$} & \bl{$r$} & \\
  \bl{$\ders\, (c\!::\!s)\, r$} & \bl{$\dn$} & \bl{$\ders\,s\,(\der\,c\,r)$} & \\
  \end{tabular}
\end{center}

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

{
\setbeamercolor{background canvas}{bg=cream}
\begin{frame}<1-6>[c]
\end{frame}
}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
\frametitle{Examples}

Given \bl{$r \dn ((a \cdot b) + b)^*$} what is

\begin{center}
\begin{tabular}{l}
\bl{$\der\,a\,r =\;?$}\\
\bl{$\der\,b\,r =\;?$}\\
\bl{$\der\,c\,r =\;?$}
\end{tabular}
\end{center}

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
\frametitle{Derivative Example}

Given \bl{$r \dn ((a \cdot b) + b)^*$} what is

\begin{center}
\def\arraystretch{1.5}  
\begin{tabular}{@{}lcl}
  \bl{$\der\,a\,((a \cdot b) + b)^*$}
    & \bl{$\Rightarrow$}& \bl{$\der\,a\, \underline{((a \cdot b) + b)^*}$}\\
    & \bl{$=$} & \bl{$(der\,a\,(\underline{(a \cdot b) + b})) \cdot r$}\\
    & \bl{$=$} & \bl{$((der\,a\,(\underline{a \cdot b})) + (der\,a\,b)) \cdot r$}\\
    & \bl{$=$} & \bl{$(((der\,a\,\underline{a}) \cdot b) + (der\,a\,b)) \cdot r$}\\
    & \bl{$=$} & \bl{$((\ONE \cdot b) + (der\,a\,\underline{b})) \cdot r$}\\
    & \bl{$=$} & \bl{$((\ONE \cdot b) + \ZERO) \cdot r$}
\end{tabular}
\end{center}

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
\frametitle{\mbox{The Brzozowski Algorithm}}

%\begin{center}
%\begin{tabular}{l} 
%\bl{$\textit{matcher}\,r\,s \dn \textit{nullable}(\ders\;s\;r)$}  
%\end{tabular}
%\end{center}

\begin{center}
\begin{mybox3}{}
\centering    
\bl{$\textit{matcher}\,r\,s \dn \textit{nullable}(\ders\;s\;r)$}
\end{mybox3}
\end{center}

\end{frame}
%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[t]
\frametitle{Brzozowski: An Example}

Does \bl{$r_1$} match \bl{$abc$}?
\begin{center}
\begin{tabular}{@{}rl@{}l@{}}
Step 1: & build derivative of \bl{$a$} and \bl{$r_1$} & \bl{$(r_2 = \der\,a\,r_1)$}\smallskip\\
Step 2: & build derivative of \bl{$b$} and \bl{$r_2$} & \bl{$(r_3 = \der\,b\,r_2)$}\smallskip\\
Step 3: & build derivative of \bl{$c$} and \bl{$r_3$} & \bl{$(r_4 = \der\,c\,r_3)$}\smallskip\\
Step 4: & the string is exhausted: & \bl{($nullable(r_4))$}\\
        & test whether \bl{$r_4$} can recognise\\
        & the empty string\medskip\\
Output: & result of the test\\
        & $\Rightarrow \bl{\textit{true}} \,\text{or}\, 
                       \bl{\textit{false}}$\\        
\end{tabular}
\end{center}


\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
\frametitle{The Idea of the Algorithm}

If we want to recognise the string \bl{$abc$} with regular 
expression \bl{$r_1$} then\medskip

\begin{enumerate}
\item \bl{$\Der\,a\,(L(r_1))$}\pause
\item \bl{$\Der\,b\,(\Der\,a\,(L(r_1)))$}\pause
\item \bl{$\Der\,c\,(\Der\,b\,(\Der\,a\,(L(r_1))))$}\bigskip
\item finally we test whether the empty string is in this 
set; same for  \bl{$\Ders\,abc\,(L(r_1))$}.\medskip
\end{enumerate}

The matching algorithm works similarly, just over regular expressions instead of sets.
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
\frametitle{The Idea with Derivatives}
  
Input: string \bl{$abc$} and regular expression \bl{$r$}\medskip 

\begin{enumerate}
\item \bl{$der\,a\,r$}
\item \bl{$der\,b\,(der\,a\,r)$}
\item \bl{$der\,c\,(der\,b\,(der\,a\,r))$}\bigskip\pause
\item finally check whether the last regular expression can match the empty string
\end{enumerate}

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
\frametitle{\boldmath\;$a^{?\{n\}} \cdot a^{\{n\}}$}

\begin{center}
\begin{tikzpicture}
\begin{axis}[
    xlabel={$n$},
    x label style={at={(1.05,0.0)}},
    ylabel={time in secs},
    enlargelimits=false,
    xtick={0,5,...,30},
    xmax=31,
    ytick={0,5,...,30},
    scaled ticks=false,
    axis lines=left,
    width=7cm,
    height=7cm, 
    legend entries={Python,Ruby},  
    legend pos=outer north east,
    legend cell align=left  
]
\addplot[blue,mark=*, mark options={fill=white}] 
  table {re-python.data};
\addplot[brown,mark=pentagon*, mark options={fill=white}] 
  table {re-ruby.data};    
\end{axis}
\end{tikzpicture}
\end{center}

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
\frametitle{Oops\ldots \boldmath\;$a^{?\{n\}} \cdot a^{\{n\}}$}

\begin{center}
\begin{tikzpicture}
\begin{axis}[
    xlabel={$n$},
    x label style={at={(1.05,0.0)}},
    ylabel={time in secs},
    enlargelimits=false,
    xtick={0,5,...,30},
    xmax=31,
    ytick={0,5,...,30},
    scaled ticks=false,
    axis lines=left,
    width=7cm,
    height=7cm, 
    legend entries={Python,Ruby,Scala V1},  
    legend pos=outer north east,
    legend cell align=left  
]
\addplot[blue,mark=*, mark options={fill=white}] 
  table {re-python.data};
\addplot[brown,mark=pentagon*, mark options={fill=white}] 
  table {re-ruby.data};  
\addplot[red,mark=triangle*,mark options={fill=white}] 
  table {re1.data};  
\end{axis}
\end{tikzpicture}
\end{center}

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[t]
\frametitle{A Problem\medskip}

We represented the ``n-times'' \bl{$a^{\{n\}}$} as a 
sequence regular expression:

\begin{center}
\begin{tabular}{rl}
0: & \bl{$\ONE$}\\    
1: & \bl{$a$}\\
2: & \bl{$a\cdot a$}\\
3: & \bl{$a\cdot a\cdot a$}\\
& \ldots\\
13: & \bl{$a\cdot a\cdot a\cdot a\cdot a\cdot a\cdot a\cdot a\cdot a\cdot a\cdot a\cdot a\cdot a$}\\
& \ldots\\
20:
\end{tabular}
\end{center}

This problem is aggravated with \bl{$a^?$} being represented 
as \bl{$a + \ONE$}.
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
\frametitle{Solving the Problem}

What happens if we extend our regular expressions with explicit 
constructors

\begin{center}
\begin{tabular}{rcl}
\bl{$r$} & \bl{$::=$} & \bl{\ldots}\\
             & \bl{$\mid$} & \bl{$r^{\{n\}}$}\\
             & \bl{$\mid$} & \bl{$r^?$} 
\end{tabular}
\end{center}

What is their meaning?\\
What are the cases for \bl{$nullable$} and \bl{$\der$}?
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
  \frametitle{$der$ for $n$-times}

Case \bl{$n = 2$} and \bl{$r \cdot r$}: 

\begin{center}
  \begin{tabular}{lcl}
    \bl{$der\,c\,(r\cdot r)$} & \bl{$\dn$} & \bl{if \; $nullable(r)$}\\
                              &   & \bl{then \; \alert<3>{$(der\,c\,r)\cdot r + der\,c\,r$}}\\
                              &   & \bl{else \; $(der\,c\,r)\cdot r$}\bigskip\pause\\
    my claim                  &   & \bl{$\equiv\;$} \bl{$(der\,c\,r)\cdot r$}\\
    (in this case)                                
  \end{tabular} 
\end{center}  

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[t]

We know \bl{$nullable(r)$} holds!\pause 

\begin{center}
  \begin{tabular}{@{}lcl}
    \bl{$(der\,c\,r)\cdot r + der\,c\,r$}\pause
    & \bl{$\equiv$} & \bl{$(der\,c\,r)\cdot r + (der\,c\,r) \cdot \ONE$}\medskip\pause\\
    & \bl{$\equiv$} & \bl{$(der\,c\,r)\cdot (r + \ONE)$}\medskip\pause\\
    & \bl{$\equiv$} & \bl{$(der\,c\,r)\cdot r$}\\
    \multicolumn{3}{r}{\small(remember \bl{$r$} is nullable)}
  \end{tabular} 
\end{center}\pause

\rule{13cm}{0.8mm}

\begin{textblock}{13}(2,10)
\only<6>{%
  \begin{tabular}{lcl}
    \bl{$der\,c\,(r\cdot r)$} & \bl{$\dn$} & \bl{if \; $nullable(r)$}\\
                          &   & \bl{then \; $(der\,c\,r)\cdot r + der\,c\,r$}\\
                          &   & \bl{else \; $(der\,c\,r)\cdot r$}                                
  \end{tabular}}
\only<7>{%
  \begin{tabular}{lcl}
    \bl{$der\,c\,(r\cdot r)$} & \bl{$\dn$} & \bl{if \; $nullable(r)$}\\
                          &   & \bl{then \; $(der\,c\,r)\cdot r$}\\
                          &   & \bl{else \; $(der\,c\,r)\cdot r$}                                
  \end{tabular}}
\only<8>{%
  \begin{tabular}{lcl}
    \bl{$der\,c\,(r\cdot r)$} & \bl{$\dn$} & \bl{$(der\,c\,r)\cdot r$}                                
  \end{tabular}}
\end{textblock}


\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]

\begin{center}
\begin{tabular}{ll@{\hspace{10mm}}l}
& \bl{$r\{n\}$} & \bl{$der$}\hspace{20mm}\mbox{}\\\hline\\[-4mm]    
\bl{$n = 0$} : & \bl{$\ONE$}           & \bl{$\ZERO$}\\
\bl{$n = 1$} : & \bl{$r$}              & \bl{$(der\,c\,r)$}\\
\bl{$n = 2$} : & \bl{$r\cdot r$}       & \bl{$(der\,c\,r)\cdot r$}\\
\bl{$n = 3$} : & \bl{$r\cdot r\cdot r$}& \only<1>{???}\only<2->{\bl{$(der\,c\,r)\cdot r\cdot r$}}\\
\quad\vdots  
\end{tabular} 
\end{center}

\begin{textblock}{13}(1,11)
\only<3->{%
  \begin{tabular}{rcl}
    \bl{$nullable(r\{n\})$} & \bl{$\dn$} &
                          \bl{if\; $n = 0$\; then\; $true$\; else\; $nullable(r)$}\\
    \bl{$der\,c\,(r\{n\})$} & \bl{$\dn$} &
                          \bl{if\; $n = 0$\; then\; $\ZERO$\; else\; $(der\,c\,r)\cdot r\{n - 1\}$}
  \end{tabular}}
\end{textblock}

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]

\begin{textblock}{13}(1.5,4)
  \only<1-6>{%
  \begin{tabular}{@{}lcl@{}}
    \bl{$der\,c\,(r\cdot r\cdot r)$}
    & \bl{$\dn$} & \bl{if $nullable(r)$}\medskip\\
    & & \only<1>{\bl{then\; $(der\,c\,r)\cdot r\cdot r + der\,c\,(r\cdot r)$}}%
        \only<2>{\bl{then\; $(der\,c\,r)\cdot r\cdot r + (der\,c\,r)\cdot r$}}%
        \only<3>{\bl{then\; $(der\,c\,r)\cdot (r\cdot r + r)$}}%
        \only<4>{\bl{then\; $(der\,c\,r)\cdot (r\cdot (r + \ONE))$}}%
        \only<5>{\bl{then\; $(der\,c\,r)\cdot (r\cdot r)$}}%
        \only<6>{\bl{then\; $(der\,c\,r)\cdot r\cdot r$}}\medskip\\
    & & \bl{else\; $(der\,c\,r)\cdot r\cdot r$}\\
  \end{tabular}}
  \only<7->{%
  \begin{tabular}{@{}lcl@{}}
    \bl{$der\,c\,(r\cdot r\cdot r)$}
    & \bl{$\dn$} & \bl{$(der\,c\,r)\cdot r\cdot r$}%
  \end{tabular}} 
\end{textblock}

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[t]
\frametitle{Brzozowski: \boldmath$a^{?\{n\}} \cdot a^{\{n\}}$}

\begin{center}
\begin{tikzpicture}
\begin{axis}[
    xlabel={$n$},
    x label style={at={(1.05,0.0)}},   
    ylabel={time in secs},
    enlargelimits=false,
    xtick={0,200,...,1100},
    xmax=1200,
    ytick={0,5,...,30},
    scaled ticks=false,
    axis lines=left,
    width=8cm,
    height=6.5cm, 
    legend entries={Python,Ruby,Scala V1,Scala V2},  
    legend pos=outer north east,
    legend cell align=left  
]
\addplot[blue,mark=*, mark options={fill=white}] table {re-python.data};
\addplot[brown,mark=pentagon*, mark options={fill=white}] table {re-ruby.data};  
\addplot[red,mark=triangle*,mark options={fill=white}] table {re1.data};  
\addplot[green,mark=square*,mark options={fill=white}] table {re2.data};
\end{axis}
\end{tikzpicture}
\end{center}

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
\frametitle{Examples}

Recall the example of \bl{$r \dn ((a \cdot b) + b)^*$} with

\begin{center}
\begin{tabular}{l}
\bl{$\der\,a\,r = ((\ONE \cdot b) + \ZERO) \cdot r$}\\
\bl{$\der\,b\,r = ((\ZERO \cdot b) + \ONE)\cdot r$}\\
\bl{$\der\,c\,r = ((\ZERO \cdot b) + \ZERO)\cdot r$}
\end{tabular}
\end{center}

What are these regular expressions equivalent to?

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
\frametitle{Simplification Rules}

\begin{center}
\bl{\begin{tabular}{rcl}
$r + \ZERO$       & $\Rightarrow$ & $r$\\
$\ZERO + r$       & $\Rightarrow$ & $r$\\
$r \cdot \ONE$    & $\Rightarrow$ & $r$\\
$\ONE \cdot r$    & $\Rightarrow$ & $r$\\
$r \cdot \ZERO$   & $\Rightarrow$ & $\ZERO$\\
$\ZERO \cdot r$   & $\Rightarrow$ & $\ZERO$\\
$r + r$           & $\Rightarrow$ & $r$
\end{tabular}}
\end{center}

\footnotesize
\lstinputlisting[firstline=22,lastline=26]{../progs/app6.scala}
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]

\footnotesize
\lstinputlisting[firstline=1,lastline=21]{../progs/app6.scala}

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[t]
\frametitle{Brzozowski: \boldmath$a^{?\{n\}} \cdot a^{\{n\}}$}

\begin{center}
\begin{tikzpicture}
\begin{axis}[
    xlabel={$n$},
    x label style={at={(1.05,0.0)}},     
    ylabel={time in secs},
    enlargelimits=false,
    xtick={0,5000,...,10000},
    xmax=11000,
    ymax=35,
    ytick={0,5,...,30},
    scaled ticks=false,
    axis lines=left,
    width=9cm,
    height=7cm,
    legend entries={Scala V2,Scala V3},  
    legend pos=north east
]
\addplot[green,mark=square*,mark options={fill=white}] table {re2.data};
\addplot[black,mark=square*,mark options={fill=white}] table {re3.data};
\end{axis}
\end{tikzpicture}
\end{center}

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[t]
\frametitle{Brzozowski: \boldmath$a^{?\{n\}} \cdot a^{\{n\}}$}

\begin{center}
\begin{tikzpicture}
\begin{axis}[
    xlabel={$n$},
    x label style={at={(1.05,0.0)}},     
    ylabel={time in secs},
    enlargelimits=false,
    xtick={0,5000,...,10000},
    xmax=11000,
    ymax=35,
    ytick={0,5,...,30},
    scaled ticks=false,
    axis lines=left,
    width=9cm,
    height=7cm,
    legend entries={Scala V2,Scala V3,Rust},  
    legend pos=north east
]
\addplot[green,mark=square*,mark options={fill=white}] table {re2.data};
\addplot[black,mark=square*,mark options={fill=white}] table {re3.data};
\addplot[pink,mark=triangle,mark options={fill=pink}] table {re-rust.data};
\end{axis}
\end{tikzpicture}
\end{center}

code by Archie Collard

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
  \frametitle{Another Example \boldmath$(a^*)^* \cdot b$}

\bigskip    
\begin{center}
\begin{tikzpicture}
  \begin{axis}[
    xlabel={$n$},
    x label style={at={(1.05,0.0)}},
    ylabel={time in secs},
    enlargelimits=false,
    xtick={0,5,...,30},
    xmax=33,
    ymax=35,
    ytick={0,10,...,30},
    scaled ticks=false,
    axis lines=left,
    width=9cm,
    height=5.5cm, 
    legend entries={Java 8,Python,JavaScript,Swift,Dart},  
    legend pos=outer north east,
    legend cell align=left]
\addplot[blue,mark=*, mark options={fill=white}] table {re-python2.data};
\addplot[cyan,mark=*, mark options={fill=white}] table {re-java.data};
\addplot[red,mark=*, mark options={fill=white}] table {re-js.data};
\addplot[magenta,mark=*, mark options={fill=white}] table {re-swift.data};
\addplot[brown,mark=*, mark options={fill=white}] table {re-dart.data};
\end{axis}
\end{tikzpicture}
\end{center}

Regex: \bl{$(a^*)^* \cdot b$}

Strings of the form \bl{$\underbrace{\,a\ldots a\,}_{n}$}

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
\frametitle{Same Example in Java 9+}

\begin{center}
\begin{tikzpicture}
  \begin{axis}[
    xlabel={$n$},
    x label style={at={(1.09,-0.15)}},
    ylabel={time in secs},
    scaled x ticks=false,
    enlargelimits=false,
    xtick distance=10000,
    xmax=44000, 
    ytick={0,10,...,30}, 
    ymax=35, 
    axis lines=left,
    width=9cm,
    height=5cm, 
    legend entries={Java \liningnums{9}+},
    legend pos=north west,
    legend cell align=left]
\addplot[blue,mark=square*,mark options={fill=white}] table {re-java9.data};
\end{axis}
\end{tikzpicture}
\end{center}

Regex: \bl{$(a^*)^* \cdot b$}

Strings of the form \bl{$\underbrace{\,a\ldots a\,}_{n}$}

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
\frametitle{\ldots{}and with Brzozowski}

\begin{center}
\begin{tikzpicture}
  \begin{axis}[
    xlabel={$n$},
    x label style={at={(1.09,0.0)}},
    ylabel={time in secs},
    scaled x ticks=false,
    xtick distance=2000000,
    enlargelimits=false,
    xmax=6400000, 
    ytick={0,10,...,30},
    ymax=35,
    axis lines=left,
    width=9cm,
    height=5cm, 
    legend entries={Scala V3},
    legend pos=north west,
    legend cell align=left]
%\addplot[green,mark=square*,mark options={fill=white}] table {re2a.data};
\addplot[black,mark=square*,mark options={fill=white}] table {re3a.data};
\end{axis}
\end{tikzpicture}
\end{center}

Regex: \bl{$(a^*)^* \cdot b$}

Strings of the form \bl{$\underbrace{\,a\ldots a\,}_{n}$}

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
\frametitle{\mbox{What is good about this Alg.}}

\begin{itemize}
\item extends to most regular expressions, for example
\bl{$\sim r$} (next slide)

\item is easy to implement in a functional language

\item the algorithm is already quite old; there is still
  work to be done to use it as a tokenizer (that is relatively new work)

\item we can prove its correctness\ldots (another video)
\end{itemize}

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
\frametitle{Negation of Regular Expr's}

\begin{itemize}
\item \bl{$\sim{}r$}  \hspace{6mm} (everything that \bl{$r$} cannot recognise)\medskip
\item \bl{$L(\sim{}r) \dn UNIV - L(r)$}\medskip
\item \bl{$nullable (\sim{}r) \dn not\, (nullable(r))$}\medskip
\item \bl{$der\,c\,(\sim{}r) \dn \;\sim{}(der\,c\,r)$}
\end{itemize}\bigskip\bigskip\medskip\pause

Used often for recognising comments:
\[
\bl{/ \cdot * \cdot (\sim{}([a\mbox{-}z]^* \cdot * \cdot / \cdot [a\mbox{-}z]^*)) \cdot * \cdot /}
\]

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
\frametitle{The Specification for Matching}

\begin{bubble}[10cm]
\large
A regular expression \bl{$r$} matches a string~\bl{$s$} 
provided:
\begin{center}
\bl{$s \in L(r)$} 
\end{center}\medskip
\end{bubble}


\begin{center}
\onslide<2>{\bl{\large$\forall\,r\,s.\;$}}
\bl{$matcher\,s\,r$}  \;if and only if\  \bl{$s \in L(r)$} 
\end{center}


\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
  
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
\frametitle{nullable and \boldmath$der$}

The central properties:\bigskip\bigskip

\large
\begin{quote}
  \onslide<3>{\bl{$\forall r.\phantom{\,c}\;$}}%
  \bl{$nullable(r)$} \;if and only if\; \bl{$[] \in L(r)$}
\end{quote}\bigskip\bigskip\pause

\begin{quote}
  \onslide<3>{\bl{$\forall r\,c.\;$}}%
  \bl{$L(der\,c\,r) \;=\; Der\,c\,(L(r))$}
\end{quote}

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
  
  

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
\begin{frame}[t]
\frametitle{Proofs about Rexps}

Remember their inductive definition:\\[5cm]

\begin{textblock}{6}(5,5)
  \begin{tabular}{@ {}rrl}
  \bl{$r$} & \bl{$::=$}  & \bl{$\ZERO$}\\
         & \bl{$\mid$} & \bl{$\ONE$}     \\
         & \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}

If we want to prove something, say a property \bl{$P(r)$}, for all regular expressions \bl{$r$} then \ldots

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
\frametitle{Proofs about Rexp (2)}

\begin{itemize}
\item \bl{$P$} holds for \bl{$\ZERO$}, \bl{$\ONE$} and \bl{c}\bigskip
\item \bl{$P$} holds for \bl{$r_1 + r_2$} under the assumption that \bl{$P$} already
holds for \bl{$r_1$} and \bl{$r_2$}.\bigskip
\item \bl{$P$} holds for \bl{$r_1 \cdot r_2$} under the assumption that \bl{$P$} already
holds for \bl{$r_1$} and \bl{$r_2$}.\bigskip
\item \bl{$P$} holds for \bl{$r^*$} under the assumption that \bl{$P$} already
holds for \bl{$r$}.
\end{itemize}

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
\frametitle{Proofs about Rexp}

Assume \bl{$P(r)$} is the property:

\begin{center}
\bl{$nullable(r)$} if and only if \bl{$[] \in L(r)$}
\end{center}

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

% begin{frame}[c]
% \begin{mybox3}{}
%   der c (r*) def = (der c r) $\cdot$ (r*)\smallskip\\
%   Why in the example (slide 19) the first step is:
%   der a ((a $\cdot$ b) + b)* = (der a ((a $\cdot$ b) + b)) $\cdot$ r\smallskip\\
%   and not\smallskip\\
%   der a ((a $\cdot$ b) + b) = (der a ((a $\cdot$ b) + b)) · (r*)
% \end{mybox3}
% \end{frame}

% \begin{frame}[c]
% \begin{mybox3}{}
%   Would it be possible to find and go over a few examples from the
%   Brzozowski Algorithm, as it doesn't seem to be as simple as it
%   sounds?
% \end{mybox3}
% \end{frame}

% \begin{frame}[c]
% \begin{mybox3}{}
%   Is it possible to make a visual example of how using simp() function
%   on a (a*)*.b regular expression reduces its runtime? If not it's
%   fine. I am just very surprised that it is so efficient.
% \end{mybox3}
% \end{frame}

% \begin{frame}[c]
% \begin{mybox3}{}
%   Do you think the algorithm can be still improved (made faster)?
% \end{mybox3}
% \end{frame}

% \begin{frame}[c]
% \begin{mybox3}{}
%   Do the regular expression matchers in Python and Java 8 have more
%   features than the one implemented in this module? Or is there
%   another reason for their inefficiency?
% \end{mybox3}
% \end{frame}

% \begin{frame}[c]
% \begin{mybox3}{}
%   Will we discuss the broader Chomsky hierarchy of languages at some
%   point?
% \end{mybox3}
% \end{frame}

\begin{frame}<1-8>[c]
\end{frame}

\begin{frame}[c]
\end{frame}

\begin{frame}[c]
\end{frame}

\begin{frame}[c]
\end{frame}

\begin{frame}<1-10>[c]
\end{frame}

  
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]

\begin{center}
\begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {}}
\bl{$nullable(\ZERO)$}    & \bl{$\dn$} & \bl{\textit{false}}\\
\bl{$nullable(\ONE)$}       & \bl{$\dn$} & \bl{\textit{true}}\\
\bl{$nullable (c)$}             & \bl{$\dn$} & \bl{\textit{false}}\\
\bl{$nullable (r_1 + r_2)$}     & \bl{$\dn$} & \bl{$nullable(r_1) \vee nullable(r_2)$} \\ 
\bl{$nullable (r_1 \cdot r_2)$} & \bl{$\dn$} & \bl{$nullable(r_1) \wedge nullable(r_2)$} \\
\bl{$nullable (r^*)$}           & \bl{$\dn$} & \bl{\textit{true}}\\
\bl{$nullable (r^{\{n\}})$}      & \bl{$\dn$} & \bl{if $n = 0$ then \textit{true} else $nullable(r)$}\\  
\end{tabular}
\end{center}

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]

\begin{center}
\begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{-10mm}}l@ {}}
  \bl{$\der\, c\, (\ZERO)$}      & \bl{$\dn$} & \bl{$\ZERO$} & \\
  \bl{$\der\, c\, (\ONE)$}           & \bl{$\dn$} & \bl{$\ZERO$} & \\
  \bl{$\der\, c\, (d)$}                     & \bl{$\dn$} & \bl{if $c = d$ then $\ONE$ else $\ZERO$} & \\
  \bl{$\der\, c\, (r_1 + r_2)$}        & \bl{$\dn$} & \bl{$\der\, c\, r_1 + \der\, c\, r_2$} & \\
  \bl{$\der\, c\, (r_1 \cdot r_2)$}  & \bl{$\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$}\\
  \bl{$\der\, c\, (r^*)$}  & \bl{$\dn$} & \bl{$(\der\,c\,r) \cdot (r^*)$}\\

  \bl{$\der\, c\, (r^{\{n\}})$}  & \bl{$\dn$} & \bl{if $n = 0$ then $\ZERO$ else $(\der\,c\,r) \cdot r^{\{n-1\}}$}\\
                                                
  \end{tabular}
\end{center}

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   


%%\end{document}
% below are slides for proving.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
\frametitle{Proofs about Rexp (4)}

\begin{center}
\bl{\begin{tabular}{r@{\hspace{2mm}}c@{\hspace{2mm}}l}
$rev(\ZERO)$   & $\dn$ & $\ZERO$\\
$rev(\ONE)$      & $\dn$ & $\ONE$\\
$rev(c)$             & $\dn$ & $c$\\
$rev(r_1 + r_2)$     & $\dn$ & $rev(r_1) + rev(r_2)$\\
$rev(r_1 \cdot r_2)$ & $\dn$ & $rev(r_2) \cdot rev(r_1)$\\
$rev(r^*)$           & $\dn$ & $rev(r)^*$\\
\end{tabular}}
\end{center}

We can prove

\begin{center}
\bl{$L(rev(r)) = \{s^{-1} \;|\; s \in L(r)\}$}
\end{center}

by induction on \bl{$r$}.

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
\frametitle{Correctness Proof \\[-1mm]
            for our Matcher}

\begin{itemize}
\item We started from

\begin{center}
\begin{tabular}{rp{4cm}}
  & \bl{$s \in L(r)$}\medskip\\
\bl{$\Leftrightarrow$} & \bl{$[] \in \Ders\,s\,(L(r))$}\pause  
\end{tabular}
\end{center}\bigskip

\item if we can show \bl{$\Ders\, s\,(L(r)) = L(\ders\,s\,r)$} we 
have\bigskip

\begin{center}
\begin{tabular}{rp{4cm}}
\bl{$\Leftrightarrow$} & \bl{$[] \in L(\ders\,s\,r)$}\medskip\\
\bl{$\Leftrightarrow$} & \bl{$nullable(\ders\,s\,r)$}\medskip\\
\bl{$\dn$} & \bl{$matcher\,s\,r$}
\end{tabular}
\end{center}

\end{itemize}

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
\frametitle{Proofs about Rexp (5)}

Let \bl{$Der\,c\,A$} be the set defined as

\begin{center}
\bl{$\Der\,c\,A \dn \{ s \;|\;  c\!::\!s \in A\}$ } 
\end{center}

We can prove

\begin{center}
\bl{$L(\der\,c\,r) = \Der\,c\,(L(r))$}
\end{center}

by induction on \bl{$r$}.

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
\frametitle{Proofs about Strings}

If we want to prove something, say a property \bl{$P(s)$}, for all strings \bl{$s$} then \ldots\bigskip

\begin{itemize}
\item \bl{$P$} holds for the empty string, and\medskip
\item \bl{$P$} holds for the string \bl{$c\!::\!s$} under the assumption that \bl{$P$}
already holds for \bl{$s$}
\end{itemize}
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
\frametitle{Proofs about Strings (2)}

We can then prove

\begin{center}
\bl{$\Ders\,s\,(L(r)) = L(\ders\,s\,r)$}  
\end{center}


We can finally prove

\begin{center}
\bl{$matcher\,s\,r$}  if and only if  \bl{$s \in L(r)$} 
\end{center}


\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
\frametitle{Coursework 1}

%%\underline{Strand 1:}

\begin{itemize}
\item Submission on Friday 16 October @ 18:00\medskip
\item source code needs to be submitted as well\medskip
\item you can re-use my Scala code from KEATS \\
  and use any programming language you like\medskip
\item \small https://nms.kcl.ac.uk/christian.urban/ProgInScala2ed.pdf\normalsize
\end{itemize}  

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
\frametitle{Epilogue}

\footnotesize
\begin{center}
\begin{tabular}{cc}
\begin{tikzpicture}
\begin{axis}[
    title={\small{}Graph: \bl{$a^{?\{n\}} \cdot a^{\{n\}}$}},
    xlabel={$n$},
    x label style={at={(1.04,0.0)}},
    ylabel={time in secs},
    enlargelimits=false,
    xmax=7100000,
    ytick={0,5,...,30},
    ymax=33,
    %scaled ticks=false,
    axis lines=left,
    width=5cm,
    height=5cm, 
    legend entries={Scala V3, Scala V4},
    legend style={at={(0.1,-0.2)},anchor=north}]
\addplot[black,mark=square*,mark options={fill=white}] table {re3.data};
\addplot[purple,mark=square*,mark options={fill=white}] table {re4.data};
\end{axis}
\end{tikzpicture}
&
\begin{tikzpicture}
\begin{axis}[
    title={\small{}Graph: \bl{$(a^*)^* \cdot b$}},
    xlabel={$n$},
    x label style={at={(1.09,0.0)}},
    ylabel={time in secs},
    enlargelimits=false,
    xmax=8100000,
    ytick={0,5,...,30},
    ymax=33,
    %scaled ticks=false,
    axis lines=left,
    width=5cm,
    height=5cm, 
    legend entries={Scala V3, Scala V4},
    legend style={at={(0.1,-0.2)},anchor=north}]
\addplot[black,mark=square*,mark options={fill=white}] table {re3a.data};
\addplot[purple,mark=square*,mark options={fill=white}] table {re4a.data};
\end{axis}
\end{tikzpicture}
\end{tabular}
\end{center}

\only<2->{\footnotesize
\begin{textblock}{9}(0.5,8)
\begin{bubble}[11.8cm]
\lstinputlisting[numbers=none]{../progs/app52.scala}
\end{bubble}
\end{textblock}} 
 

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
  \frametitle{Another Homework Question}
  
  \begin{itemize}
  \item How many basic regular expressions are there to match
    the string \bl{$abcd$}\,?\pause
  \item How many if they cannot include
    \bl{$\ONE$} and \bl{$\ZERO$}\/?\pause
  \item How many if they are also not
    allowed to contain stars?\pause
  \item How many if they are also
        not allowed to contain \bl{$\_ + \_$}\/? 
  \end{itemize}  
  
  \end{frame}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
\frametitle{\begin{tabular}{c}\\[3cm]\huge\alert{Questions?}\end{tabular}}

%\bigskip
%homework (written exam 80\%)\\
%coursework (20\%; first one today)\\
%submission Fridays @ 18:00 -- accepted until Mondays
\mbox{}
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
  



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
\frametitle{Last Week}

Last week I showed you a regular expression matcher 
that works provably correct in all cases (we only
started with the proving part though)

\begin{center}
\bl{$matcher\,s\,r$} \;\;if and only if \;\; \bl{$s \in L(r)$}
\end{center}\bigskip\bigskip 

\small
\textcolor{gray}{\mbox{}\hfill{}by Janusz Brzozowski (1964)}

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   





 

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
  \frametitle{Proofs about Rexp}
  
  \begin{itemize}
  \item \bl{$P$} holds for \bl{$\ZERO$}, \bl{$\ONE$} and \bl{c}\bigskip
  \item \bl{$P$} holds for \bl{$r_1 + r_2$} under the assumption that \bl{$P$} already
  holds for \bl{$r_1$} and \bl{$r_2$}.\bigskip
  \item \bl{$P$} holds for \bl{$r_1 \cdot r_2$} under the assumption that \bl{$P$} already
  holds for \bl{$r_1$} and \bl{$r_2$}.\bigskip
  \item \bl{$P$} holds for \bl{$r^*$} under the assumption that \bl{$P$} already
  holds for \bl{$r$}.
  \end{itemize}
  
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
  

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]

We proved

\begin{center}
\bl{$nullable(r)$} \;if and only if\;  \bl{$[] \in L(r)$}
\end{center}

by induction on the regular expression \bl{$r$}.\bigskip\pause

\begin{center}
{\huge\bf\alert{Any Questions?}}
\end{center}

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
\frametitle{\begin{tabular}{c}Proofs about Natural\\[-1mm] Numbers and Strings\end{tabular}}

\begin{itemize}
\item \bl{$P$} holds for \bl{$0$} and
\item \bl{$P$} holds for \bl{$n + 1$} under the assumption that \bl{$P$} already
holds for \bl{$n$}
\end{itemize}\bigskip

\begin{itemize}
\item \bl{$P$} holds for \bl{$[]$} and
\item \bl{$P$} holds for \bl{$c\!::\!s$} under the assumption that \bl{$P$} already
holds for \bl{$s$}
\end{itemize}

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

  
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
  \frametitle{Correctness Proof \\[-1mm]
              for our Matcher}
  
  \begin{itemize}
  \item We started from
  
  \begin{center}
  \begin{tabular}{rp{4cm}}
    & \bl{$s \in L(r)$}\medskip\\
  \bl{$\Leftrightarrow$} & \bl{$[] \in \Ders\,s\,(L(r))$}\pause  
  \end{tabular}
  \end{center}\bigskip
  
  \item \textbf{\alert{if}} we can show \bl{$\Ders\, s\,(L(r)) = L(\ders\,s\,r)$} we 
  have\bigskip
  
  \begin{center}
  \begin{tabular}{rp{4cm}}
  \bl{$\Leftrightarrow$} & \bl{$[] \in L(\ders\,s\,r)$}\medskip\\
  \bl{$\Leftrightarrow$} & \bl{$nullable(\ders\,s\,r)$}\medskip\\
  \bl{$\dn$} & \bl{$matcher\,s\,r$}
  \end{tabular}
  \end{center}
  
  \end{itemize}
  
  \end{frame}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]

We need to prove

\begin{center}
\bl{$L(der\,c\,r) = Der\,c\,(L(r))$}
\end{center}

also by induction on the regular expression \bl{$r$}.
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   




\end{document}

%%% Local Variables:  
%%% mode: latex
%%% TeX-master: t
%%% End: 

