afl-material: comparison slides/ssy.tex

equal deleted inserted replaced

-:64ec1884d860
+:c7009356ddd8
 \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}
+\setbeamersize{text margin left=2mm} % <- like this
 \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}{SSY, King's College London}
+\renewcommand{\slidecaption}{Christian Urban, SSY, King's College London}
 \begin{document}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[t]
+\frametitle{\begin{tabular}{@ {\hspace{8mm}}c@ {}}Fast Regular Expression Matching\end{tabular}}
+\mbox{}\\[1mm]
+\begin{columns}[t,onlytextwidth]
+\begin{column}{.2\textwidth}
+\raisebox{-10mm}{
+\begin{tikzpicture}
+\begin{axis}[
+xlabel={size of strings},
+x label style={at={(0.45,-0.16)}},
+ylabel={time in secs},
+enlargelimits=false,
+xtick={0,10,...,30},
+xmax=35,
+ymax=35,
+ytick={0,10,...,30},
+scaled ticks=false,
+axis lines=left,
+width=5cm,
+height=4.5cm,
+legend entries={Python,JavaScript,Swift,Dart},
+legend style={font=\footnotesize,at={(0.45,-0.48)},anchor=north},
+legend cell align=left]
+\addplot[blue,mark=*, mark options={fill=white}] table {re-python2.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{column}
+\end{columns}
+\begin{textblock}{4}(3.5,3.2)
+{\bl{\texttt{(a*)*$\cdot$b}}}
+\end{textblock}
+\begin{textblock}{7.5}(8,3)
+\begin{itemize}
+\item use \textbf{Brzozowski derivatives} for regex matching rather\\ than NFAs/DFAs% and lexing
+\item based on work by \textbf{Christian Urban} and \textbf{Roy Dyckhoff}\bigskip
+\item applications in network security (traffic filtering)
+\item formal verification of correctness and speed (\textbf{Isabelle} theorem prover)
+\end{itemize}
+\end{textblock}
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\end{document}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \begin{frame}[t]
 \frametitle{%
 \begin{tabular}{@ {}c@ {}}
 \\[8mm]
 \LARGE Derivative-Based\\
 \LARGE Regular Expression Matching\\[5mm]
 \normalsize\textcolor{gray}{Christian Urban, SSY Group}
 \end{tabular}}
 \end{frame}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \begin{frame}[c]
 \frametitle{A Bit of Background}
 \begin{textblock}{10}(2,2.5)
 \includegraphics[scale=0.4]{../pics/phd-1.jpg}
 \end{textblock}
 \begin{textblock}{11}(1.7,10)
 \begin{bubble}[9.6cm]
 PhD thesis on a particular term-rewriting system:\medskip\\
 Proved that all rewriting sequences are strongly normalising (terminate).
 \end{bubble}
 \end{textblock}
 \only<2->{%
 \begin{textblock}{3}(10,2.5)
 \begin{tabular}{rcl}
 \bl{$t$} & \bl{::=} & \bl{$x$}\\
 & \bl{|} & \bl{$\lambda x.\,t$}\\
 & \bl{|} & \bl{$t_1\;t_2$}\\
 & \bl{|} & \bl{...}
 \end{tabular}
 \end{bubble}
 \end{textblock}}
 \end{frame}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \begin{frame}[t]
 \frametitle{Quiz 1}
 \begin{bubble}[10cm]\it
 There are many, many regular expression libraries.\bigskip\\
 \textbf{Given a regular expression \bl{r} and a string \bl{s}, what is the
 difficulty / complexity of the problem deciding whether \bl{r} matches \bl{s}?}
 \end{bubble}
 \begin{textblock}{12}(2,9)
 \draw(7,-1) node[rotate=0]{\bl{$O(2^n)$}};
 \end{tikzpicture}
 \end{textblock}
 \end{frame}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \begin{frame}[t]
 \frametitle{Quiz 2}
 \begin{textblock}{12}(2,2.5)
 A regular expression for (some) email addresses:
 \begin{center}
 ($\underbrace{\bl{[a\mbox{-}z0\mbox{-}9\_\!\!\_\,.-]^+}}_{\textrm{name}}$)\bl{$\,@\,$}
 ($\underbrace{\bl{[a\mbox{-}z0\mbox{-}9\,-]^+}}_{\textrm{domain}}$) \bl{$\,.\,$}
 ($\underbrace{\bl{[a\mbox{-}z\,.]^{\{2..5\}}}}_{\textrm{top-level domain}}$)
 \end{center}
 \end{textblock}
 \only<2>{
 \begin{textblock}{10}(4,8)
 bounded regular expressions:\medskip\\
 \begin{tabular}{ll}
 \bl{$r^{\{n\}}$}     & exactly n-times \bl{$r$}\\
 \bl{$r^{\{n..m\}}$}  & between n and m-times\\
 \bl{$r^{\{n..\}}$}   & from n-times\\
 \bl{$r^{\{..m\}}$}   & upto m-times\\
 \end{tabular}\smallskip\\
 \footnotesize\hfill ${}^*$ in some applications the counters can be in the millions
 \end{textblock}}
 \end{frame}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \begin{frame}[t]
 \frametitle{Quiz 2}
 \begin{textblock}{12}(2,2.5)
 \onslide<1>{
 \begin{tikzpicture}[node distance=3mm,
 >=stealth',very thick,
 every state/.style={minimum size=3pt,draw=blue!50,very thick,fill=blue!20}]
 \node[state, initial]  (Q_0)  {$\mbox{}$};
 \node[state, initial]  (Q_01) [below=1mm of Q_0] {$\mbox{}$};
 \node[state, initial]  (Q_02) [above=1mm of Q_0] {$\mbox{}$};
 \node (R_1)  [right=of Q_0] {$\ldots$};
 \node[state, accepting]  (T_1)  [right=of R_1] {$\mbox{}$};
 \node[state, accepting]  (T_2)  [above=of T_1] {$\mbox{}$};
 \node[state, accepting]  (T_3)  [below=of T_1] {$\mbox{}$};
 \onslide<2>{
 \begin{tikzpicture}[node distance=3mm,
 >=stealth',very thick,
 every state/.style={minimum size=3pt,draw=blue!50,very thick,fill=blue!20},]
 \node[state, initial]  (Q_0)  {$\mbox{}$};
 \node[state, initial]  (Q_01) [below=1mm of Q_0] {$\mbox{}$};
 \node[state, initial]  (Q_02) [above=1mm of Q_0] {$\mbox{}$};
 \node (r_1)  [right=of Q_0] {$\ldots$};
 \node[state]  (t_1)  [right=of r_1] {$\mbox{}$};
 \node[state]  (t_2)  [above=of t_1] {$\mbox{}$};
 \node[state]  (t_3)  [below=of t_1] {$\mbox{}$};
 \path[->] (t_2) edge node [above]  {$\varepsilon$\footnotesize{}s} (A_01);
 \path[->] (t_3) edge (A_01);
 \path[->] (t_1) edge (A_02);
 \path[->] (t_2) edge (A_02);
 \path[->] (t_3) edge node [below]  {$\varepsilon$\footnotesize{}s} (A_02);
 \begin{pgfonlayer}{background}
 \node (3) [rounded corners, inner sep=1mm, thick,
 draw=black!60, fill=black!20, fit= (Q_0) (c_1) (c_2) (c_3)] {};
 \node [yshift=2mm] at (3.north) {$r_1\cdot r_2$};
 \end{pgfonlayer}
 \end{tikzpicture}}
 \end{textblock}
 \end{frame}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \begin{frame}[t]
 \frametitle{Quiz 2}
 \begin{textblock}{12}(2,2.5)
 \onslide<1->{Thompson construction: By recursion we have a NFA for $r$.\medskip\\
 \onslide<2->{For $r^*$:\bigskip}}
 \end{textblock}
 \begin{textblock}{12}(4,6)
 \onslide<1>{
 \begin{tikzpicture}[node distance=3mm,
 >=stealth',very thick,
 every state/.style={minimum size=3pt,draw=blue!50,very thick,fill=blue!20},
 baseline=(current bounding box.north)]
 \node (2)  {$\mbox{}$};
 \node[state, initial]  (4)  [above=1mm of 2] {$\mbox{}$};
 \node[state, initial]  (5)  [below=1mm of 2] {$\mbox{}$};
 \node (a)  [right=of 2] {$\ldots$};
 \node[state, accepting]  (a1)  [right=of a] {$\mbox{}$};
 \node[state, accepting]  (a2)  [above=of a1] {$\mbox{}$};
 \node[state, accepting]  (a3)  [below=of a1] {$\mbox{}$};
 \begin{pgfonlayer}{background}
 \end{pgfonlayer}
 \end{tikzpicture}}
 \end{textblock}
 \begin{textblock}{12}(2,6)
 \onslide<2->{
 \begin{tikzpicture}[node distance=3mm,
 >=stealth',very thick,
 every state/.style={minimum size=3pt,draw=blue!50,very thick,fill=blue!20},
 baseline=(current bounding box.north)]
 \node at (0,0) [state, initial,accepting]  (1)  {$\mbox{}$};
 \node (2)  [right=16mm of 1] {$\mbox{}$};
 \node[state]  (4)  [above=1mm of 2] {$\mbox{}$};
 \node[state]  (5)  [below=1mm of 2] {$\mbox{}$};
 \node (a)  [right=of 2] {$\ldots$};
 \node[state]  (a1)  [right=of a] {$\mbox{}$};
 \node[state]  (a2)  [above=of a1] {$\mbox{}$};
 \node[state]  (a3)  [below=of a1] {$\mbox{}$};
 \path[->] (1) edge node [below]  {$\varepsilon$} (4);
 \end{pgfonlayer}
 \end{tikzpicture}}
 \end{textblock}
 \begin{textblock}{12}(2,12)
 \onslide<3->{
 \begin{bubble}[9.5cm]\it
 Quiz:\smallskip\\
 \textbf{What is the Thompson Construction for \bl{$r^{\{n\}}$} ?}
 \end{bubble}}
 \end{textblock}
 \end{frame}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \begin{frame}[t]
 \frametitle{Quiz 3}
 Hierarchy of Languages:
 \begin{center}
 \begin{tikzpicture}
 [rect/.style={draw=black!50,
 top color=white,
 bottom color=black!20,
 rectangle,
 very thick,
 rounded corners}, scale=1.2]
 \draw (0,0) node [rect, text depth=39mm, text width=68mm] {all languages};
 \draw (0,-0.4) node [rect, text depth=28.5mm, text width=64mm] {decidable languages};
 \draw (0,-0.85) node [rect, text depth=17mm] {\;\;context sensitive languages\;\;};
 \draw (0,-1.14) node [rect, text depth=9mm, text width=50mm] {context-free languages};
 \draw (0,-1.4) node [rect] {regular languages};
 \end{tikzpicture}
 \end{center}
 \begin{textblock}{12}(2,11.5)
 \onslide<2->{
 \begin{bubble}[9.5cm]\it
 Quiz:\smallskip\\
 \textbf{Can we use standard parsing algorithms for matching / lexing\,?}
 Say CYK, LL, LR(k), PEG, \ldots
 \end{bubble}}
 \end{textblock}
 \end{frame}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \defverbatim{\foo}{\footnotesize%
 \begin{verbatim}
 (?:(?:\"|'|\]|\}|\\|\d|(?:nan|infinity|true|false|
 null|undefined|symbol|math)|\`|\-|\+)+[)]*;?((?:\s
 | -|~|!|{}|\|\||\+)*.*(?:.*=.*)))
 \end{verbatim}
 }
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \begin{frame}[t,fragile]
 \frametitle{Quiz 4}
 \begin{textblock}{12}(2,2.5)
 \begin{bubble}[9.5cm]\it
 Quiz:\smallskip\\
 Do regular expressions have any security relevance\,?
 \end{bubble}
 \end{textblock}
 \only<2->{
 \hspace{1.5cm}a global outage on 2 July 2019 (first one for six years)
 \color{blue}\foo\color{black}
 \end{textblock}
 }
 \end{frame}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \begin{frame}[t]
 \frametitle{Quiz 3}
 \begin{textblock}{12}(2,2)
 \begin{bubble}[9.5cm]\it
 Quiz:\smallskip\\
 \textbf{Can we use standard parsing algorithms for matching / lexing\,?}
 Say CYK, LL, LR(k), PEG, \ldots
 \end{bubble}
 \end{textblock}
 Lexing a string with  & \bl{$(r_{key} + r_{id})^*$}\medskip\\
 What should be & \\
 the result for:  & \bl{\texttt{"iffoo"}} \;\;\; \bl{\texttt{"if"}}\\
 \end{tabular}
 \end{textblock}
 \only<2->{
 \begin{textblock}{13.5}(1.5,4)
 \begin{mybox3}{POSIX rules}
 \begin{itemize}
 \item \textbf{The Longest Match Rule:} The longest initial
 substring matched by any regular expression is taken as next token.
 \item \textbf{Priority Rule:}  For a particular longest initial
 substring, the first (leftmost) regular expression that can match
 determines the token.
 \item \ldots
 \end{itemize}
 \begin{center}
 \bl{$(a + ab) \cdot (bc + c)$} \;\;and\;\; \bl{\texttt{"}$abc$\texttt{"}}
 \end{center}
 \end{mybox3}
 \end{textblock}}
 \end{frame}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \begin{frame}[t]
 \frametitle{Quiz 1}
 \begin{bubble}[10cm]\it
 There are many, many regular expression libraries.\bigskip\\
 \textbf{Given a regular expression \bl{r} and a string \bl{s}, what is the
 difficulty / complexity of the problem deciding whether \bl{r} matches \bl{s}?}
 \end{bubble}
 \begin{textblock}{12}(1,9)
 Python, Ruby, Swift, Dart, JavaScript & Rust, Go, RE2 & \textcolor{gray}{Snort, .Net7}\\
 \end{tabular}
 \end{textblock}
 \end{frame}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \begin{frame}[t]
 \mbox{}\\[10mm]
 \begin{columns}[t,onlytextwidth]
 \begin{column}{.2\textwidth}
 \raisebox{-10mm}{
 \begin{tikzpicture}
 \begin{axis}[
 xlabel={\bl{$n$} \pcode{a}s},
 %%x label style={at={(1.05,0.0)}},
 ylabel={time in secs},
 ymax=35,
 ytick={0,5,...,30},
 scaled ticks=false,
 axis lines=left,
 width=5cm,
 height=5cm,
 legend entries={Python,JavaScript,Swift,Dart},
 legend style={font=\small,at={(0.5,-0.39)},anchor=north},
 legend cell align=left]
 \addplot[blue,mark=*, mark options={fill=white}] table {re-python2.data};
 \addplot[red,mark=*, mark options={fill=white}] table {re-js.data};
 ymax=35,
 ytick={0,5,...,30},
 scaled ticks=false,
 axis lines=left,
 width=5cm,
 height=5cm,
 legend entries={Python,Ruby},
 legend style={font=\small,at={(0.5,-0.39)},anchor=north},
 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{column}
 \end{columns}
 \begin{textblock}{4}(9,1.7)
 \textbf{\bl{\texttt{(a?)\boldmath$^{\{n\}}\cdot$(a)\boldmath$^{\{n\}}$}}}
 \end{textblock}
 \begin{textblock}{4}(4,1.7)
 \textbf{\bl{\texttt{(a*)*$\cdot$b}}}
 \end{textblock}
 \begin{textblock}{3.4}(0.3,10)
 \small{}\textbf{matching with strings}
 \textbf{\bl{$\underbrace{\texttt{a}...\texttt{a}}_n$}}
 \end{textblock}
 \end{frame}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \begin{frame}[t]
 \frametitle{Quiz 1}
 \begin{bubble}[10cm]\it
 \textbf{Given a regular expression \bl{r} and a string \bl{s}, what is the
 difficulty / complexity of the problem deciding whether \bl{r} matches \bl{s}?}
 \begin{textblock}{12}(1.7,7)
 For \textbf{Perl-style} regular expression matchers (say Python, JavaScript, etc), the
 answer is:
 \only<2->{\begin{center}
 \fontspec{Hoefler Text Black}\textcolor{ProcessBlue}{\huge{}NP}
 \end{center}}
 \end{textblock}
 \begin{textblock}{12}(1.7,12)
 \only<3->{Backreferences: \bl{(\ldots)$\,\ldots{}\backslash{}n$}}
 \end{textblock}
 \end{frame}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \begin{frame}
 \frametitle{Quiz 2}
 \begin{textblock}{12}(2,2)
 \onslide<1->{
 \begin{bubble}[9.5cm]\it
 Quiz:\smallskip\\
 \textbf{What is the Thompson Construction for \bl{$r^{\{n\}}$} ?}
 \end{bubble}}
 \end{textblock}
 \only<2->{
 & \onslide<6->{$\Rightarrow$ \bl{$a^{\{0\}\{4294967295\}}$} ?}
 \end{tabular}
 \end{textblock}}
 \only<4>{
 \begin{textblock}{13.5}(1.5,4)
 \begin{mybox3}{From Rust's Regex Description}\it
 ``\ldots [the] syntax is similar to Perl-style regular expressions, but lacks a few features like look
 around and backreferences. In exchange, all searches execute in linear time with respect
 to the size of the regular expression and search text. \ldots''
 \end{mybox3}
 \end{textblock}}
 \end{frame}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \begin{frame}[t]
 \frametitle{Regular Expressions}
 & \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{textblock}
 \end{frame}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \begin{frame}[c]
 \frametitle{\begin{tabular}{l}The Derivative of a Rexp\end{tabular}}
 \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\medskip\\
 (lost in the sands of time, re-appeared in 2009)
 \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\\
 \end{tabular}
 \end{center}
 \end{frame}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \begin{frame}[t]
 \frametitle{\begin{tabular}{l}Brzozowski matcher\end{tabular}}
 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{\mbox{Nullable}}
 \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}[t]
 \frametitle{\begin{tabular}{l}Extensions\end{tabular}}
 \end{center}
 also works for lookarounds, various anchors, etc, but \textbf{not} for backreferences
 \begin{textblock}{3}(11,13)
 \onslide<2>{
 \begin{bubble}[3cm]
 \bl{$a^{\{0\}\{4294967295\}}$}
 \end{bubble}}
 \end{textblock}
 \end{frame}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \begin{frame}[t]
 \frametitle{\mbox{Problems with Ders}}
 & & $\qquad(\ZERO + \ZERO{}a + \ONE) \cdot (a + aa)^* + (\ONE + \ONE{}a) \cdot (a + aa)^*$\\
 & $\ll$ & \ldots\\ \hspace{15mm}
 \end{tabular}
 \end{center}}
 \begin{textblock}{13.5}(1.5,12)
 (regular expressions of sizes 98, 169, 283, 468, 767, \ldots)
 \end{textblock}
 \end{frame}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \begin{frame}[c]
 \frametitle{\mbox{Conclusion}}
 \begin{itemize}
 \item The beauty is that this only involves functional programs that can be conveniently reasoned about in theorem provers
 \item POSIX lexing can be done via an extension by Sulzmann and Lu, 2014 (our current work)\medskip\pause
 \item How surprising that one can still do new work on regular expressions.
 \end{itemize}
 \end{frame}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \begin{frame}<1-10>
 \end{frame}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \end{document}
 %%% Local Variables:
 %%% mode: latex
 %%% TeX-master: t
 %%% End:

changeset 960	c7009356ddd8
parent 913	eef6a56c185a