slides/ssy.tex
changeset 960 c7009356ddd8
parent 913 eef6a56c185a
--- a/slides/ssy.tex	Wed Feb 21 09:14:12 2024 +0000
+++ b/slides/ssy.tex	Wed May 29 13:25:30 2024 +0100
@@ -13,8 +13,8 @@
 \newtcolorbox{mybox3}[1]{colback=Cyan!5!white,colframe=Cyan!75!black,fonttitle=\bfseries,title=#1}
 
 
-
-\hfuzz=220pt 
+\setbeamersize{text margin left=2mm} % <- like this
+\hfuzz=220pt
 
 \lstset{language=Scala,
         style=mystyle,
@@ -22,20 +22,74 @@
         numbers=none,
         xleftmargin=0mm}
 
-\pgfplotsset{compat=1.17}      
+\pgfplotsset{compat=1.17}
 
-\newcommand{\bl}[1]{\textcolor{blue}{#1}}     
- 
-% beamer stuff 
-\renewcommand{\slidecaption}{SSY, King's College London}
+\newcommand{\bl}[1]{\textcolor{blue}{#1}}
+
+% beamer stuff
+\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{%  
+\frametitle{%
   \begin{tabular}{@ {}c@ {}}
     \\[8mm]
     \LARGE Derivative-Based\\
@@ -46,7 +100,7 @@
 \end{frame}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%      
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \begin{frame}[c]
 \frametitle{A Bit of Background}
 
@@ -57,7 +111,7 @@
 \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). 
+  Proved that all rewriting sequences are strongly normalising (terminate).
 \end{bubble}
 \end{textblock}
 
@@ -69,8 +123,8 @@
          & \bl{|} & \bl{$\lambda x.\,t$}\\
          & \bl{|} & \bl{$t_1\;t_2$}\\
          & \bl{|} & \bl{...}
-\end{tabular}  
-\end{bubble}  
+\end{tabular}
+\end{bubble}
 \end{textblock}}
 
 \end{frame}
@@ -78,14 +132,14 @@
 
 
 
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%      
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \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}
@@ -102,9 +156,9 @@
 \end{textblock}
 
 \end{frame}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%      
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \begin{frame}[t]
 \frametitle{Quiz 2}
 
@@ -114,13 +168,13 @@
   ($\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{center}
 \end{textblock}
 
 \only<2>{
 \begin{textblock}{10}(4,8)
 bounded regular expressions:\medskip\\
-\begin{tabular}{ll}    
+\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\\
@@ -128,12 +182,12 @@
 \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}
 
@@ -149,8 +203,8 @@
     >=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[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{}$};
@@ -181,8 +235,8 @@
     >=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[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{}$};
@@ -202,7 +256,7 @@
 \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)] {};
@@ -213,9 +267,9 @@
 
 
 \end{frame}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%      
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \begin{frame}[t]
 \frametitle{Quiz 2}
 
@@ -225,14 +279,14 @@
 \end{textblock}
 
 \begin{textblock}{12}(4,6)
-\onslide<1>{  
+\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[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{}$};
@@ -245,7 +299,7 @@
 \end{textblock}
 
 \begin{textblock}{12}(2,6)
-\onslide<2->{  
+\onslide<2->{
 \begin{tikzpicture}[node distance=3mm,
     >=stealth',very thick,
     every state/.style={minimum size=3pt,draw=blue!50,very thick,fill=blue!20},
@@ -253,7 +307,7 @@
 \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[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{}$};
@@ -271,30 +325,30 @@
 \end{textblock}
 
 \begin{textblock}{12}(2,12)
-\onslide<3->{ 
+\onslide<3->{
   \begin{bubble}[9.5cm]\it
-  Quiz:\smallskip\\  
+  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:  
+Hierarchy of Languages:
 
 \begin{center}
 \begin{tikzpicture}
-[rect/.style={draw=black!50, 
+[rect/.style={draw=black!50,
               top color=white,
-              bottom color=black!20, 
-              rectangle, 
-              very thick, 
+              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};
@@ -303,36 +357,36 @@
 \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}  
+\end{center}
 
 \begin{textblock}{12}(2,11.5)
-\onslide<2->{ 
+\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\\    
+  Quiz:\smallskip\\
   Do regular expressions have any security relevance\,?
 \end{bubble}
 \end{textblock}
@@ -361,18 +415,18 @@
    \end{textblock}
 }
 
-    
+
 \end{frame}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%      
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \begin{frame}[t]
   \frametitle{Quiz 3}
 
-\begin{textblock}{12}(2,2) 
+\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}
@@ -390,11 +444,11 @@
 
   What should be & \\
   the result for:  & \bl{\texttt{"iffoo"}} \;\;\; \bl{\texttt{"if"}}\\
-\end{tabular}  
+\end{tabular}
 \end{textblock}
 
 \only<2->{
-\begin{textblock}{13.5}(1.5,4) 
+\begin{textblock}{13.5}(1.5,4)
   \begin{mybox3}{POSIX rules}
     \begin{itemize}
     \item \textbf{The Longest Match Rule:} The longest initial
@@ -402,23 +456,23 @@
     \item \textbf{Priority Rule:}  For a particular longest initial
       substring, the first (leftmost) regular expression that can match
       determines the token.
-    \item \ldots  
+    \item \ldots
     \end{itemize}
     \begin{center}
     \bl{$(a + ab) \cdot (bc + c)$} \;\;and\;\; \bl{\texttt{"}$abc$\texttt{"}}
-    \end{center}  
+    \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}
@@ -431,16 +485,16 @@
 \end{textblock}
 
 \end{frame}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%      
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \begin{frame}[t]
 
-\mbox{}\\[10mm]  
+\mbox{}\\[10mm]
 
-\begin{columns}[t,onlytextwidth]  
+\begin{columns}[t,onlytextwidth]
 \begin{column}{.2\textwidth}
-\raisebox{-10mm}{    
+\raisebox{-10mm}{
 \begin{tikzpicture}
   \begin{axis}[
     xlabel={\bl{$n$} \pcode{a}s},
@@ -454,7 +508,7 @@
     scaled ticks=false,
     axis lines=left,
     width=5cm,
-    height=5cm, 
+    height=5cm,
     legend entries={Python,JavaScript,Swift,Dart},
     legend style={font=\small,at={(0.5,-0.39)},anchor=north},
     legend cell align=left]
@@ -479,34 +533,34 @@
     scaled ticks=false,
     axis lines=left,
     width=5cm,
-    height=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};  
+\addplot[brown,mark=pentagon*, mark options={fill=white}] table {re-ruby.data};
 \end{axis}
-\end{tikzpicture}  
-\end{column}  
+\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)  
+\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$}}  
+\textbf{\bl{$\underbrace{\texttt{a}...\texttt{a}}_n$}}
 \end{textblock}
 
 \end{frame}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%      
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \begin{frame}[t]
 \frametitle{Quiz 1}
 \begin{bubble}[10cm]\it
@@ -519,25 +573,25 @@
 answer is:
 \only<2->{\begin{center}
 \fontspec{Hoefler Text Black}\textcolor{ProcessBlue}{\huge{}NP}
-\end{center}}  
+\end{center}}
 \end{textblock}
 
 \begin{textblock}{12}(1.7,12)
 \only<3->{Backreferences: \bl{(\ldots)$\,\ldots{}\backslash{}n$}}
-\end{textblock}  
+\end{textblock}
 \end{frame}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 
 
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \begin{frame}
 \frametitle{Quiz 2}
 
 \begin{textblock}{12}(2,2)
-\onslide<1->{ 
+\onslide<1->{
   \begin{bubble}[9.5cm]\it
-  Quiz:\smallskip\\  
+  Quiz:\smallskip\\
   \textbf{What is the Thompson Construction for \bl{$r^{\{n\}}$} ?}
 \end{bubble}}
 \end{textblock}
@@ -552,8 +606,8 @@
 \end{textblock}}
 
 \only<4>{
-\begin{textblock}{13.5}(1.5,4) 
-  \begin{mybox3}{From Rust's Regex Description}\it 
+\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''
@@ -561,7 +615,7 @@
 \end{textblock}}
 
 
-\end{frame}  
+\end{frame}
 
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -578,16 +632,16 @@
          & \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 
+If \bl{$r$} matches the string \bl{$c\!::\!s$}, what is a regular
 expression that matches just \bl{$s$}?\bigskip\bigskip\bigskip\bigskip
 
 \small
@@ -607,14 +661,14 @@
   \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{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]
@@ -630,14 +684,14 @@
         & 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}}$\\        
+        & $\Rightarrow \bl{\textit{true}} \,\text{or}\,
+                       \bl{\textit{false}}$\\
 \end{tabular}
 \end{center}
 
 
 \end{frame}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \begin{frame}[c]
@@ -650,14 +704,14 @@
 \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 + 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]
@@ -679,14 +733,14 @@
 also works for lookarounds, various anchors, etc, but \textbf{not} for backreferences
 
 \begin{textblock}{3}(11,13)
-\onslide<2>{ 
+\onslide<2>{
   \begin{bubble}[3cm]
   \bl{$a^{\{0\}\{4294967295\}}$}
 \end{bubble}}
 \end{textblock}
 
 \end{frame}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \begin{frame}[t]
@@ -705,38 +759,37 @@
 \end{tabular}
 \end{center}}
 
-\begin{textblock}{13.5}(1.5,12) 
+\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 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} 
+\item How surprising that one can still do new work on regular expressions.
+\end{itemize}
 
 \end{frame}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 \begin{frame}<1-10>
-\end{frame}  
+\end{frame}
 
 
 
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \end{document}
 
-%%% Local Variables:  
+%%% Local Variables:
 %%% mode: latex
 %%% TeX-master: t
-%%% End: 
-
+%%% End: