slides/ssy.tex
author Christian Urban <christian.urban@kcl.ac.uk>
Wed, 29 May 2024 13:25:30 +0100
changeset 960 c7009356ddd8
parent 913 eef6a56c185a
permissions -rw-r--r--
updated
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
876
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
     1
% !TEX program = xelatex
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
     2
\documentclass[dvipsnames,14pt,t,xelatex,xcolor={table}]{beamer}
876
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
     3
\usepackage{../slides}
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
     4
\usepackage{../graphicss}
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
     5
\usepackage{../langs}
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
     6
\usepackage{../data}
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
     7
\usetikzlibrary{cd}
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
     8
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
     9
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
    10
\usepackage{tcolorbox}
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
    11
\newtcolorbox{mybox}{colback=red!5!white,colframe=red!75!black}
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
    12
\newtcolorbox{mybox2}[1]{colback=red!5!white,colframe=red!75!black,fonttitle=\bfseries,title=#1}
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
    13
\newtcolorbox{mybox3}[1]{colback=Cyan!5!white,colframe=Cyan!75!black,fonttitle=\bfseries,title=#1}
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
    14
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
    15
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
    16
\setbeamersize{text margin left=2mm} % <- like this
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
    17
\hfuzz=220pt
876
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
    18
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
    19
\lstset{language=Scala,
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
    20
        style=mystyle,
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
    21
        numbersep=0pt,
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
    22
        numbers=none,
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
    23
        xleftmargin=0mm}
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
    24
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
    25
\pgfplotsset{compat=1.17}
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
    26
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
    27
\newcommand{\bl}[1]{\textcolor{blue}{#1}}
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
    28
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
    29
% beamer stuff
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
    30
\renewcommand{\slidecaption}{Christian Urban, SSY, King's College London}
876
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
    31
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
    32
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
    33
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
    34
\begin{document}
876
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
    35
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
    36
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
    37
\begin{frame}[t]
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
    38
\frametitle{\begin{tabular}{@ {\hspace{8mm}}c@ {}}Fast Regular Expression Matching\end{tabular}}
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
    39
\mbox{}\\[1mm]
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
    40
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
    41
\begin{columns}[t,onlytextwidth]
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
    42
\begin{column}{.2\textwidth}
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
    43
\raisebox{-10mm}{
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
    44
\begin{tikzpicture}
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
    45
  \begin{axis}[
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
    46
    xlabel={size of strings},
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
    47
    x label style={at={(0.45,-0.16)}},
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
    48
    ylabel={time in secs},
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
    49
    enlargelimits=false,
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
    50
    xtick={0,10,...,30},
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
    51
    xmax=35,
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
    52
    ymax=35,
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
    53
    ytick={0,10,...,30},
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
    54
    scaled ticks=false,
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
    55
    axis lines=left,
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
    56
    width=5cm,
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
    57
    height=4.5cm,
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
    58
    legend entries={Python,JavaScript,Swift,Dart},
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
    59
    legend style={font=\footnotesize,at={(0.45,-0.48)},anchor=north},
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
    60
    legend cell align=left]
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
    61
\addplot[blue,mark=*, mark options={fill=white}] table {re-python2.data};
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
    62
\addplot[red,mark=*, mark options={fill=white}] table {re-js.data};
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
    63
\addplot[magenta,mark=*, mark options={fill=white}] table {re-swift.data};
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
    64
\addplot[brown,mark=*, mark options={fill=white}] table {re-dart.data};
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
    65
\end{axis}
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
    66
\end{tikzpicture}}
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
    67
\end{column}
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
    68
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
    69
\end{columns}
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
    70
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
    71
\begin{textblock}{4}(3.5,3.2)
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
    72
{\bl{\texttt{(a*)*$\cdot$b}}}
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
    73
\end{textblock}
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
    74
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
    75
\begin{textblock}{7.5}(8,3)
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
    76
\begin{itemize}
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
    77
\item use \textbf{Brzozowski derivatives} for regex matching rather\\ than NFAs/DFAs% and lexing
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
    78
\item based on work by \textbf{Christian Urban} and \textbf{Roy Dyckhoff}\bigskip
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
    79
\item applications in network security (traffic filtering)
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
    80
\item formal verification of correctness and speed (\textbf{Isabelle} theorem prover)
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
    81
\end{itemize}
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
    82
\end{textblock}
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
    83
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
    84
\end{frame}
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
    85
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
    86
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
    87
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
    88
\end{document}
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
    89
876
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
    90
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
    91
\begin{frame}[t]
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
    92
\frametitle{%
876
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
    93
  \begin{tabular}{@ {}c@ {}}
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
    94
    \\[8mm]
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
    95
    \LARGE Derivative-Based\\
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
    96
    \LARGE Regular Expression Matching\\[5mm]
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
    97
    \normalsize\textcolor{gray}{Christian Urban, SSY Group}
876
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
    98
  \end{tabular}}
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
    99
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
   100
\end{frame}
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
   101
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
   102
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   103
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   104
\begin{frame}[c]
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   105
\frametitle{A Bit of Background}
876
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
   106
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   107
\begin{textblock}{10}(2,2.5)
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   108
\includegraphics[scale=0.4]{../pics/phd-1.jpg}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   109
\end{textblock}
876
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
   110
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   111
\begin{textblock}{11}(1.7,10)
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   112
\begin{bubble}[9.6cm]
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   113
  PhD thesis on a particular term-rewriting system:\medskip\\
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   114
  Proved that all rewriting sequences are strongly normalising (terminate).
876
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
   115
\end{bubble}
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   116
\end{textblock}
876
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
   117
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   118
\only<2->{%
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   119
\begin{textblock}{3}(10,2.5)
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   120
\begin{bubble}[3cm]
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   121
\begin{tabular}{rcl}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   122
  \bl{$t$} & \bl{::=} & \bl{$x$}\\
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   123
         & \bl{|} & \bl{$\lambda x.\,t$}\\
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   124
         & \bl{|} & \bl{$t_1\;t_2$}\\
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   125
         & \bl{|} & \bl{...}
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   126
\end{tabular}
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   127
\end{bubble}
876
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
   128
\end{textblock}}
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
   129
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
   130
\end{frame}
879
ad9d4a01e072 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 876
diff changeset
   131
ad9d4a01e072 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 876
diff changeset
   132
ad9d4a01e072 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 876
diff changeset
   133
876
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
   134
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   135
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   136
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   137
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   138
\begin{frame}[t]
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   139
\frametitle{Quiz 1}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   140
\begin{bubble}[10cm]\it
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   141
  There are many, many regular expression libraries.\bigskip\\
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   142
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   143
  \textbf{Given a regular expression \bl{r} and a string \bl{s}, what is the
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   144
  difficulty / complexity of the problem deciding whether \bl{r} matches \bl{s}?}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   145
\end{bubble}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   146
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   147
\begin{textblock}{12}(2,9)
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   148
\begin{tikzpicture}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   149
  \draw(0,0)  node[rotate=20]{linear};
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   150
  \draw(3,0)  node[rotate=-20]{\bl{$O(n \log n)$}};
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   151
  \draw(3,-2) node[rotate=10]{quadratic};
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   152
  \draw(6,0) node[rotate=20]{P};
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   153
  \draw(7,0) node[rotate=-20]{NP};
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   154
  \draw(7,-1) node[rotate=0]{\bl{$O(2^n)$}};
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   155
\end{tikzpicture}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   156
\end{textblock}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   157
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   158
\end{frame}
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   159
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   160
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   161
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   162
\begin{frame}[t]
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   163
\frametitle{Quiz 2}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   164
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   165
\begin{textblock}{12}(2,2.5)
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   166
A regular expression for (some) email addresses:
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   167
\begin{center}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   168
  ($\underbrace{\bl{[a\mbox{-}z0\mbox{-}9\_\!\!\_\,.-]^+}}_{\textrm{name}}$)\bl{$\,@\,$}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   169
  ($\underbrace{\bl{[a\mbox{-}z0\mbox{-}9\,-]^+}}_{\textrm{domain}}$) \bl{$\,.\,$}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   170
  ($\underbrace{\bl{[a\mbox{-}z\,.]^{\{2..5\}}}}_{\textrm{top-level domain}}$)
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   171
\end{center}
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   172
\end{textblock}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   173
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   174
\only<2>{
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   175
\begin{textblock}{10}(4,8)
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   176
bounded regular expressions:\medskip\\
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   177
\begin{tabular}{ll}
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   178
  \bl{$r^{\{n\}}$}     & exactly n-times \bl{$r$}\\
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   179
  \bl{$r^{\{n..m\}}$}  & between n and m-times\\
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   180
  \bl{$r^{\{n..\}}$}   & from n-times\\
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   181
  \bl{$r^{\{..m\}}$}   & upto m-times\\
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   182
\end{tabular}\smallskip\\
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   183
\footnotesize\hfill ${}^*$ in some applications the counters can be in the millions
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   184
\end{textblock}}
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   185
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   186
\end{frame}
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   187
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   188
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   189
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   190
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   191
\begin{frame}[t]
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   192
\frametitle{Quiz 2}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   193
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   194
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   195
\begin{textblock}{12}(2,2.5)
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   196
  \onslide<1->{Thompson construction: By recursion we are given two NFAs for $r_1$ and $r_2$.\medskip\\
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   197
    \onslide<2->{For $r_1\cdot r_2$:}\bigskip}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   198
\end{textblock}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   199
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   200
\begin{textblock}{12}(2,6)
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   201
\onslide<1>{
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   202
\begin{tikzpicture}[node distance=3mm,
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   203
    >=stealth',very thick,
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   204
    every state/.style={minimum size=3pt,draw=blue!50,very thick,fill=blue!20}]
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   205
\node[state, initial]  (Q_0)  {$\mbox{}$};
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   206
\node[state, initial]  (Q_01) [below=1mm of Q_0] {$\mbox{}$};
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   207
\node[state, initial]  (Q_02) [above=1mm of Q_0] {$\mbox{}$};
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   208
\node (R_1)  [right=of Q_0] {$\ldots$};
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   209
\node[state, accepting]  (T_1)  [right=of R_1] {$\mbox{}$};
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   210
\node[state, accepting]  (T_2)  [above=of T_1] {$\mbox{}$};
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   211
\node[state, accepting]  (T_3)  [below=of T_1] {$\mbox{}$};
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   212
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   213
\node (A_0)  [right=2.5cm of T_1] {$\mbox{}$};
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   214
\node[state, initial]  (A_01)  [above=1mm of A_0] {$\mbox{}$};
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   215
\node[state, initial]  (A_02)  [below=1mm of A_0] {$\mbox{}$};
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   216
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   217
\node (b_1)  [right=of A_0] {$\ldots$};
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   218
\node[state, accepting]  (c_1)  [right=of b_1] {$\mbox{}$};
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   219
\node[state, accepting]  (c_2)  [above=of c_1] {$\mbox{}$};
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   220
\node[state, accepting]  (c_3)  [below=of c_1] {$\mbox{}$};
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   221
\begin{pgfonlayer}{background}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   222
  \node (1) [rounded corners, inner sep=1mm, thick,
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   223
    draw=black!60, fill=black!20, fit= (Q_0) (R_1) (T_1) (T_2) (T_3)] {};
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   224
  \node (2) [rounded corners, inner sep=1mm, thick,
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   225
    draw=black!60, fill=black!20, fit= (A_0) (b_1) (c_1) (c_2) (c_3)] {};
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   226
\node [yshift=2mm] at (1.north) {$r_1$};
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   227
\node [yshift=2mm] at (2.north) {$r_2$};
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   228
\end{pgfonlayer}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   229
\end{tikzpicture}}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   230
\end{textblock}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   231
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   232
\begin{textblock}{12}(2,6)
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   233
\onslide<2>{
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   234
\begin{tikzpicture}[node distance=3mm,
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   235
    >=stealth',very thick,
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   236
    every state/.style={minimum size=3pt,draw=blue!50,very thick,fill=blue!20},]
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   237
\node[state, initial]  (Q_0)  {$\mbox{}$};
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   238
\node[state, initial]  (Q_01) [below=1mm of Q_0] {$\mbox{}$};
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   239
\node[state, initial]  (Q_02) [above=1mm of Q_0] {$\mbox{}$};
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   240
\node (r_1)  [right=of Q_0] {$\ldots$};
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   241
\node[state]  (t_1)  [right=of r_1] {$\mbox{}$};
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   242
\node[state]  (t_2)  [above=of t_1] {$\mbox{}$};
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   243
\node[state]  (t_3)  [below=of t_1] {$\mbox{}$};
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   244
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   245
\node  (A_0)  [right=2.5cm of t_1] {$\mbox{}$};
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   246
\node[state]  (A_01)  [above=1mm of A_0] {$\mbox{}$};
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   247
\node[state]  (A_02)  [below=1mm of A_0] {$\mbox{}$};
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   248
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   249
\node (b_1)  [right=of A_0] {$\ldots$};
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   250
\node[state, accepting]  (c_1)  [right=of b_1] {$\mbox{}$};
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   251
\node[state, accepting]  (c_2)  [above=of c_1] {$\mbox{}$};
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   252
\node[state, accepting]  (c_3)  [below=of c_1] {$\mbox{}$};
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   253
\path[->] (t_1) edge (A_01);
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   254
\path[->] (t_2) edge node [above]  {$\varepsilon$\footnotesize{}s} (A_01);
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   255
\path[->] (t_3) edge (A_01);
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   256
\path[->] (t_1) edge (A_02);
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   257
\path[->] (t_2) edge (A_02);
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   258
\path[->] (t_3) edge node [below]  {$\varepsilon$\footnotesize{}s} (A_02);
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   259
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   260
\begin{pgfonlayer}{background}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   261
  \node (3) [rounded corners, inner sep=1mm, thick,
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   262
    draw=black!60, fill=black!20, fit= (Q_0) (c_1) (c_2) (c_3)] {};
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   263
\node [yshift=2mm] at (3.north) {$r_1\cdot r_2$};
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   264
\end{pgfonlayer}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   265
\end{tikzpicture}}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   266
\end{textblock}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   267
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   268
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   269
\end{frame}
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   270
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   271
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   272
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   273
\begin{frame}[t]
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   274
\frametitle{Quiz 2}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   275
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   276
\begin{textblock}{12}(2,2.5)
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   277
  \onslide<1->{Thompson construction: By recursion we have a NFA for $r$.\medskip\\
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   278
  \onslide<2->{For $r^*$:\bigskip}}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   279
\end{textblock}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   280
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   281
\begin{textblock}{12}(4,6)
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   282
\onslide<1>{
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   283
\begin{tikzpicture}[node distance=3mm,
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   284
    >=stealth',very thick,
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   285
    every state/.style={minimum size=3pt,draw=blue!50,very thick,fill=blue!20},
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   286
    baseline=(current bounding box.north)]
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   287
\node (2)  {$\mbox{}$};
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   288
\node[state, initial]  (4)  [above=1mm of 2] {$\mbox{}$};
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   289
\node[state, initial]  (5)  [below=1mm of 2] {$\mbox{}$};
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   290
\node (a)  [right=of 2] {$\ldots$};
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   291
\node[state, accepting]  (a1)  [right=of a] {$\mbox{}$};
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   292
\node[state, accepting]  (a2)  [above=of a1] {$\mbox{}$};
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   293
\node[state, accepting]  (a3)  [below=of a1] {$\mbox{}$};
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   294
\begin{pgfonlayer}{background}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   295
\node (1) [rounded corners, inner sep=1mm, thick, draw=black!60, fill=black!20, fit= (2) (a1) (a2) (a3)] {};
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   296
\node [yshift=3mm] at (1.north) {$r$};
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   297
\end{pgfonlayer}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   298
\end{tikzpicture}}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   299
\end{textblock}
876
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
   300
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   301
\begin{textblock}{12}(2,6)
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   302
\onslide<2->{
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   303
\begin{tikzpicture}[node distance=3mm,
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   304
    >=stealth',very thick,
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   305
    every state/.style={minimum size=3pt,draw=blue!50,very thick,fill=blue!20},
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   306
    baseline=(current bounding box.north)]
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   307
\node at (0,0) [state, initial,accepting]  (1)  {$\mbox{}$};
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   308
\node (2)  [right=16mm of 1] {$\mbox{}$};
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   309
\node[state]  (4)  [above=1mm of 2] {$\mbox{}$};
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   310
\node[state]  (5)  [below=1mm of 2] {$\mbox{}$};
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   311
\node (a)  [right=of 2] {$\ldots$};
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   312
\node[state]  (a1)  [right=of a] {$\mbox{}$};
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   313
\node[state]  (a2)  [above=of a1] {$\mbox{}$};
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   314
\node[state]  (a3)  [below=of a1] {$\mbox{}$};
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   315
\path[->] (1) edge node [below]  {$\varepsilon$} (4);
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   316
\path[->] (1) edge node [below]  {$\varepsilon$} (5);
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   317
\path[->] (a1) edge [bend left=45] node [below]  {$\varepsilon$} (1);
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   318
\path[->] (a2) edge [bend right] node [below]  {$\varepsilon$} (1);
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   319
\path[->] (a3) edge [bend left=45] node [below]  {$\varepsilon$} (1);
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   320
\begin{pgfonlayer}{background}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   321
\node (2) [rounded corners, inner sep=1mm, thick, draw=black!60, fill=black!20, fit= (1) (a2) (a3)] {};
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   322
\node [yshift=3mm] at (2.north) {$r^*$};
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   323
\end{pgfonlayer}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   324
\end{tikzpicture}}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   325
\end{textblock}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   326
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   327
\begin{textblock}{12}(2,12)
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   328
\onslide<3->{
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   329
  \begin{bubble}[9.5cm]\it
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   330
  Quiz:\smallskip\\
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   331
  \textbf{What is the Thompson Construction for \bl{$r^{\{n\}}$} ?}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   332
\end{bubble}}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   333
\end{textblock}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   334
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   335
\end{frame}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   336
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   337
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   338
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   339
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   340
\begin{frame}[t]
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   341
  \frametitle{Quiz 3}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   342
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   343
Hierarchy of Languages:
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   344
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   345
\begin{center}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   346
\begin{tikzpicture}
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   347
[rect/.style={draw=black!50,
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   348
              top color=white,
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   349
              bottom color=black!20,
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   350
              rectangle,
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   351
              very thick,
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   352
              rounded corners}, scale=1.2]
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   353
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   354
\draw (0,0) node [rect, text depth=39mm, text width=68mm] {all languages};
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   355
\draw (0,-0.4) node [rect, text depth=28.5mm, text width=64mm] {decidable languages};
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   356
\draw (0,-0.85) node [rect, text depth=17mm] {\;\;context sensitive languages\;\;};
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   357
\draw (0,-1.14) node [rect, text depth=9mm, text width=50mm] {context-free languages};
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   358
\draw (0,-1.4) node [rect] {regular languages};
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   359
\end{tikzpicture}
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   360
\end{center}
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   361
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   362
\begin{textblock}{12}(2,11.5)
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   363
\onslide<2->{
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   364
  \begin{bubble}[9.5cm]\it
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   365
    Quiz:\smallskip\\
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   366
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   367
    \textbf{Can we use standard parsing algorithms for matching / lexing\,?}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   368
    Say CYK, LL, LR(k), PEG, \ldots
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   369
\end{bubble}}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   370
\end{textblock}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   371
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   372
\end{frame}
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   373
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   374
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   375
\defverbatim{\foo}{\footnotesize%
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   376
\begin{verbatim}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   377
(?:(?:\"|'|\]|\}|\\|\d|(?:nan|infinity|true|false|
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   378
null|undefined|symbol|math)|\`|\-|\+)+[)]*;?((?:\s
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   379
| -|~|!|{}|\|\||\+)*.*(?:.*=.*)))
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   380
\end{verbatim}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   381
}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   382
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   383
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   384
\begin{frame}[t,fragile]
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   385
\frametitle{Quiz 4}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   386
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   387
\begin{textblock}{12}(2,2.5)
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   388
\begin{bubble}[9.5cm]\it
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   389
  Quiz:\smallskip\\
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   390
  Do regular expressions have any security relevance\,?
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   391
\end{bubble}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   392
\end{textblock}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   393
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   394
\only<2->{
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   395
\begin{textblock}{2}(1,6)
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   396
\includegraphics[scale=0.8]{../pics/zeek.png}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   397
\includegraphics[scale=0.17]{../pics/snort.png}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   398
\end{textblock}}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   399
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   400
\only<3->{
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   401
\begin{textblock}{7}(7,5.6)
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   402
  \includegraphics[scale=0.14]{../pics/cloudflare.png}\\
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   403
    \footnotesize
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   404
    It serves more web traffic than Twitter, Amazon, Apple,
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   405
    Instagram, Bing \& Wikipedia combined.\medskip\\
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   406
    Web Application Firewall filters out
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   407
    SQL injection attacks, XSS attacks etc
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   408
\end{textblock}}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   409
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   410
\only<3->{
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   411
  \begin{textblock}{13}(4,12.3)
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   412
  \footnotesize
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   413
  \hspace{1.5cm}a global outage on 2 July 2019 (first one for six years)
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   414
  \color{blue}\foo\color{black}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   415
   \end{textblock}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   416
}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   417
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   418
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   419
\end{frame}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   420
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   421
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   422
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   423
\begin{frame}[t]
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   424
  \frametitle{Quiz 3}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   425
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   426
\begin{textblock}{12}(2,2)
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   427
  \begin{bubble}[9.5cm]\it
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   428
    Quiz:\smallskip\\
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   429
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   430
    \textbf{Can we use standard parsing algorithms for matching / lexing\,?}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   431
    Say CYK, LL, LR(k), PEG, \ldots
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   432
\end{bubble}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   433
\end{textblock}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   434
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   435
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   436
\begin{textblock}{12}(1,7)
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   437
\textbf{POSIX lexing}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   438
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   439
\begin{tabular}{@ {}ll}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   440
  Assume you have: & \bl{$r_{key} \dn \texttt{if} + \texttt{then} + \texttt{while} \ldots$}\\
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   441
                   & \bl{$r_{id\;} \,\dn \texttt{[a-z]} \cdot \texttt{[a-z0-9\_]}^*$}\medskip\\
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   442
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   443
  Lexing a string with  & \bl{$(r_{key} + r_{id})^*$}\medskip\\
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   444
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   445
  What should be & \\
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   446
  the result for:  & \bl{\texttt{"iffoo"}} \;\;\; \bl{\texttt{"if"}}\\
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   447
\end{tabular}
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   448
\end{textblock}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   449
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   450
\only<2->{
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   451
\begin{textblock}{13.5}(1.5,4)
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   452
  \begin{mybox3}{POSIX rules}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   453
    \begin{itemize}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   454
    \item \textbf{The Longest Match Rule:} The longest initial
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   455
      substring matched by any regular expression is taken as next token.
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   456
    \item \textbf{Priority Rule:}  For a particular longest initial
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   457
      substring, the first (leftmost) regular expression that can match
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   458
      determines the token.
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   459
    \item \ldots
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   460
    \end{itemize}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   461
    \begin{center}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   462
    \bl{$(a + ab) \cdot (bc + c)$} \;\;and\;\; \bl{\texttt{"}$abc$\texttt{"}}
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   463
    \end{center}
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   464
  \end{mybox3}
876
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
   465
\end{textblock}}
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
   466
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
   467
\end{frame}
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
   468
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
   469
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   470
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   471
\begin{frame}[t]
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   472
\frametitle{Quiz 1}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   473
\begin{bubble}[10cm]\it
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   474
  There are many, many regular expression libraries.\bigskip\\
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   475
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   476
  \textbf{Given a regular expression \bl{r} and a string \bl{s}, what is the
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   477
  difficulty / complexity of the problem deciding whether \bl{r} matches \bl{s}?}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   478
\end{bubble}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   479
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   480
\begin{textblock}{12}(1,9)
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   481
  \begin{tabular}{p{4cm}|p{4cm}|p{2cm}}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   482
    atrociously slow (s't) & pretty lazy (s't) & \textcolor{gray}{OTBT}\medskip\\
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   483
    Python, Ruby, Swift, Dart, JavaScript & Rust, Go, RE2 & \textcolor{gray}{Snort, .Net7}\\
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   484
  \end{tabular}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   485
\end{textblock}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   486
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   487
\end{frame}
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   488
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   489
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   490
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   491
\begin{frame}[t]
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   492
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   493
\mbox{}\\[10mm]
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   494
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   495
\begin{columns}[t,onlytextwidth]
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   496
\begin{column}{.2\textwidth}
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   497
\raisebox{-10mm}{
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   498
\begin{tikzpicture}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   499
  \begin{axis}[
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   500
    xlabel={\bl{$n$} \pcode{a}s},
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   501
    %%x label style={at={(1.05,0.0)}},
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   502
    ylabel={time in secs},
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   503
    enlargelimits=false,
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   504
    xtick={0,10,...,30},
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   505
    xmax=35,
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   506
    ymax=35,
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   507
    ytick={0,5,...,30},
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   508
    scaled ticks=false,
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   509
    axis lines=left,
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   510
    width=5cm,
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   511
    height=5cm,
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   512
    legend entries={Python,JavaScript,Swift,Dart},
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   513
    legend style={font=\small,at={(0.5,-0.39)},anchor=north},
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   514
    legend cell align=left]
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   515
\addplot[blue,mark=*, mark options={fill=white}] table {re-python2.data};
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   516
\addplot[red,mark=*, mark options={fill=white}] table {re-js.data};
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   517
\addplot[magenta,mark=*, mark options={fill=white}] table {re-swift.data};
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   518
\addplot[brown,mark=*, mark options={fill=white}] table {re-dart.data};
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   519
\end{axis}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   520
\end{tikzpicture}}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   521
\end{column}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   522
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   523
\begin{column}{.2\textwidth}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   524
\begin{tikzpicture}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   525
  \begin{axis}[
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   526
    xlabel={\bl{$n$} \pcode{a}s},
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   527
    %ylabel={time in secs},
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   528
    enlargelimits=false,
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   529
    xtick={0,10,...,30},
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   530
    xmax=35,
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   531
    ymax=35,
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   532
    ytick={0,5,...,30},
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   533
    scaled ticks=false,
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   534
    axis lines=left,
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   535
    width=5cm,
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   536
    height=5cm,
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   537
    legend entries={Python,Ruby},
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   538
    legend style={font=\small,at={(0.5,-0.39)},anchor=north},
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   539
    legend cell align=left]
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   540
\addplot[blue,mark=*, mark options={fill=white}] table {re-python.data};
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   541
\addplot[brown,mark=pentagon*, mark options={fill=white}] table {re-ruby.data};
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   542
\end{axis}
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   543
\end{tikzpicture}
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   544
\end{column}
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   545
\end{columns}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   546
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   547
\begin{textblock}{4}(9,1.7)
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   548
\textbf{\bl{\texttt{(a?)\boldmath$^{\{n\}}\cdot$(a)\boldmath$^{\{n\}}$}}}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   549
\end{textblock}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   550
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   551
\begin{textblock}{4}(4,1.7)
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   552
\textbf{\bl{\texttt{(a*)*$\cdot$b}}}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   553
\end{textblock}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   554
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   555
\begin{textblock}{3.4}(0.3,10)
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   556
\small{}\textbf{matching with strings}
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   557
\textbf{\bl{$\underbrace{\texttt{a}...\texttt{a}}_n$}}
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   558
\end{textblock}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   559
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   560
\end{frame}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   561
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   562
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   563
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   564
\begin{frame}[t]
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   565
\frametitle{Quiz 1}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   566
\begin{bubble}[10cm]\it
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   567
  \textbf{Given a regular expression \bl{r} and a string \bl{s}, what is the
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   568
  difficulty / complexity of the problem deciding whether \bl{r} matches \bl{s}?}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   569
\end{bubble}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   570
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   571
\begin{textblock}{12}(1.7,7)
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   572
For \textbf{Perl-style} regular expression matchers (say Python, JavaScript, etc), the
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   573
answer is:
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   574
\only<2->{\begin{center}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   575
\fontspec{Hoefler Text Black}\textcolor{ProcessBlue}{\huge{}NP}
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   576
\end{center}}
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   577
\end{textblock}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   578
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   579
\begin{textblock}{12}(1.7,12)
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   580
\only<3->{Backreferences: \bl{(\ldots)$\,\ldots{}\backslash{}n$}}
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   581
\end{textblock}
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   582
\end{frame}
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   583
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   584
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   585
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   586
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   587
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   588
\begin{frame}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   589
\frametitle{Quiz 2}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   590
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   591
\begin{textblock}{12}(2,2)
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   592
\onslide<1->{
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   593
  \begin{bubble}[9.5cm]\it
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   594
  Quiz:\smallskip\\
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   595
  \textbf{What is the Thompson Construction for \bl{$r^{\{n\}}$} ?}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   596
\end{bubble}}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   597
\end{textblock}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   598
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   599
\only<2->{
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   600
\begin{textblock}{12}(1,6)
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   601
\begin{tabular}{ll}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   602
  Google's RE2 lib & $\Rightarrow$ \bl{$a^{\{1001\}}$} is too big\\
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   603
  \onslide<3->{Rust Regex lib}    & \onslide<5->{$\Rightarrow$ \bl{$a^{\{1000\}\{100\}\{5\}}$} too big}\\
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   604
                    & \onslide<6->{$\Rightarrow$ \bl{$a^{\{0\}\{4294967295\}}$} ?}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   605
\end{tabular}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   606
\end{textblock}}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   607
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   608
\only<4>{
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   609
\begin{textblock}{13.5}(1.5,4)
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   610
  \begin{mybox3}{From Rust's Regex Description}\it
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   611
    ``\ldots [the] syntax is similar to Perl-style regular expressions, but lacks a few features like look
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   612
    around and backreferences. In exchange, all searches execute in linear time with respect
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   613
    to the size of the regular expression and search text. \ldots''
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   614
  \end{mybox3}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   615
\end{textblock}}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   616
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   617
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   618
\end{frame}
876
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
   619
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
   620
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
   621
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   622
\begin{frame}[t]
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   623
\frametitle{Regular Expressions}
876
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
   624
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   625
\begin{textblock}{6}(2,5)
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   626
  \begin{tabular}{@ {}rrl@ {\hspace{13mm}}l}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   627
  \bl{$r$} & \bl{$::=$}  & \bl{$\ZERO$}  & nothing\\
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   628
         & \bl{$\mid$} & \bl{$\ONE$}       & empty string / \pcode{""} \\
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   629
         & \bl{$\mid$} & \bl{$c, d, \ldots$}                         & characters\\
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   630
         & \bl{$\mid$} & \bl{$r_1 + r_2$}  & alternative / choice\\
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   631
         & \bl{$\mid$} & \bl{$r_1 \cdot r_2$} & sequence\\
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   632
         & \bl{$\mid$} & \bl{$r^*$}            & star (zero or more)\\
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   633
  \end{tabular}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   634
  \end{textblock}
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   635
876
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
   636
\end{frame}
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   637
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
876
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
   638
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
   639
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
   640
\begin{frame}[c]
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   641
\frametitle{\begin{tabular}{l}The Derivative of a Rexp\end{tabular}}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   642
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   643
\large
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   644
If \bl{$r$} matches the string \bl{$c\!::\!s$}, what is a regular
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   645
expression that matches just \bl{$s$}?\bigskip\bigskip\bigskip\bigskip
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   646
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   647
\small
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   648
\bl{$\der\,c\,r$} gives the answer, Brzozowski 1964\medskip\\
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   649
(lost in the sands of time, re-appeared in 2009)
876
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
   650
\end{frame}
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
   651
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
   652
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
   653
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
   654
\begin{frame}[c]
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   655
\frametitle{\begin{tabular}{l}The Derivative of a Rexp\end{tabular}}
876
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
   656
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   657
\begin{center}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   658
\begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{-10mm}}l@ {}}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   659
  \bl{$\der\, c\, (\ZERO)$}      & \bl{$\dn$} & \bl{$\ZERO$} & \\
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   660
  \bl{$\der\, c\, (\ONE)$}           & \bl{$\dn$} & \bl{$\ZERO$} & \\
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   661
  \bl{$\der\, c\, (d)$}                     & \bl{$\dn$} & \bl{if $c = d$ then $\ONE$ else $\ZERO$} & \\
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   662
  \bl{$\der\, c\, (r_1 + r_2)$}        & \bl{$\dn$} & \bl{$\der\, c\, r_1 + \der\, c\, r_2$} & \\
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   663
  \bl{$\der\, c\, (r_1 \cdot r_2)$}  & \bl{$\dn$}  & \bl{if $nullable (r_1)$}\\
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   664
  & & \bl{then $(\der\,c\,r_1) \cdot r_2 + \der\, c\, r_2$}\\
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   665
  & & \bl{else $(\der\, c\, r_1) \cdot r_2$}\\
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   666
  \bl{$\der\, c\, (r^*)$}  & \bl{$\dn$} & \bl{$(\der\,c\,r) \cdot (r^*)$} &\medskip\bigskip\\
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   667
  \end{tabular}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   668
\end{center}
876
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
   669
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
   670
\end{frame}
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   671
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
876
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
   672
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
   673
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   674
\begin{frame}[t]
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   675
\frametitle{\begin{tabular}{l}Brzozowski matcher\end{tabular}}
876
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
   676
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   677
Does \bl{$r_1$} match \bl{"$abc$"}?
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   678
\begin{center}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   679
\begin{tabular}{@{}rl@{}l@{}}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   680
Step 1: & build derivative of \bl{$a$} and \bl{$r_1$} & \bl{$(r_2 = \der\,a\,r_1)$}\smallskip\\
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   681
Step 2: & build derivative of \bl{$b$} and \bl{$r_2$} & \bl{$(r_3 = \der\,b\,r_2)$}\smallskip\\
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   682
Step 3: & build derivative of \bl{$c$} and \bl{$r_3$} & \bl{$(r_4 = \der\,c\,r_3)$}\smallskip\\
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   683
Step 4: & the string is exhausted: & \bl{($nullable(r_4))$}\\
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   684
        & test whether \bl{$r_4$} can recognise\\
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   685
        & the empty string\medskip\\
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   686
Output: & result of the test\\
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   687
        & $\Rightarrow \bl{\textit{true}} \,\text{or}\,
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   688
                       \bl{\textit{false}}$\\
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   689
\end{tabular}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   690
\end{center}
876
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
   691
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   692
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   693
\end{frame}
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   694
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   695
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   696
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   697
\begin{frame}[c]
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   698
\frametitle{\mbox{Nullable}}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   699
876
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
   700
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   701
\ldots{}whether a regular expression can match the empty string:
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   702
\begin{center}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   703
\begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {}}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   704
\bl{$nullable(\ZERO)$}    & \bl{$\dn$} & \bl{\textit{false}}\\
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   705
\bl{$nullable(\ONE)$}       & \bl{$\dn$} & \bl{\textit{true}}\\
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   706
\bl{$nullable (c)$}             & \bl{$\dn$} & \bl{\textit{false}}\\
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   707
\bl{$nullable (r_1 + r_2)$}     & \bl{$\dn$} & \bl{$nullable(r_1) \vee nullable(r_2)$} \\
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   708
\bl{$nullable (r_1 \cdot r_2)$} & \bl{$\dn$} & \bl{$nullable(r_1) \wedge nullable(r_2)$} \\
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   709
\bl{$nullable (r^*)$}           & \bl{$\dn$} & \bl{\textit{true}}\\
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   710
\end{tabular}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   711
\end{center}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   712
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   713
\end{frame}
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   714
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   715
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   716
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   717
\begin{frame}[t]
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   718
\frametitle{\begin{tabular}{l}Extensions\end{tabular}}
876
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
   719
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   720
\begin{center}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   721
\begin{tabular}{@ {\hspace{-4mm}}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{-10mm}}l@ {}}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   722
  \bl{$\der\, c\, (r^{\{n\}})$}      & \bl{$\dn$} & \bl{$if\;n=0\;then\;\ZERO\;else\; (der\,c\,r)\cdot r^{\{n-1\}}$} & \\
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   723
  \bl{$\der\, c\, (r^{\{..n\}})$}    & \bl{$\dn$} & \bl{$if\;n=0\;then\;\ZERO\;else\; (der\,c\,r)\cdot r^{\{n-1\}}$} & \\
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   724
  \bl{$\der\, c\, (r^{\{n..\}})$}    & \bl{$\dn$} & \bl{$if\;n=0\;then\;(der\,c\,r)\cdot r^*$} \\
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   725
                                    &            & \bl{$else\; (der\,c\,r)\cdot r^{\{n-1\}}$} & \\
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   726
  \bl{$\der\, c\, (r^{\{n..m\}})$}   & \bl{$\dn$} & \bl{$if\;n=0 \wedge m=0\;then\;\ZERO\;else$} & \\
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   727
                                     &           & \bl{$if \;n=0 \wedge 0<m\; then\;(der\,c\,r)\cdot r^{\{..m-1\}}$} & \\
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   728
                                     &           & \bl{$else\; (der\,c\,r)\cdot r^{\{n-1..m-1\}}$} & \\
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   729
  \bl{$\der\, c\, (\neg{}r)$}            & \bl{$\dn$}  & \bl{$\neg(der\,c\,r)$}\\
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   730
  \end{tabular}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   731
\end{center}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   732
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   733
also works for lookarounds, various anchors, etc, but \textbf{not} for backreferences
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   734
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   735
\begin{textblock}{3}(11,13)
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   736
\onslide<2>{
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   737
  \begin{bubble}[3cm]
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   738
  \bl{$a^{\{0\}\{4294967295\}}$}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   739
\end{bubble}}
876
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
   740
\end{textblock}
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
   741
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
   742
\end{frame}
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   743
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
876
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
   744
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
   745
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   746
\begin{frame}[t]
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   747
\frametitle{\mbox{Problems with Ders}}
876
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
   748
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   749
\textcolor{blue}{
876
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
   750
\small
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   751
\def\ll{\stackrel{der\,a}{\longrightarrow}}
876
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
   752
\begin{center}
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   753
\begin{tabular}{@{\hspace{-5mm}}rll}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   754
$(a + aa)^*$ & $\ll$ & $(\ONE + \ONE{}a) \cdot (a + aa)^*$\\
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   755
& $\ll$ & $(\ZERO + \ZERO{}a + \ONE) \cdot (a + aa)^* \;+\; (\ONE + \ONE{}a) \cdot (a + aa)^*$\\
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   756
& $\ll$ & $(\ZERO + \ZERO{}a + \ZERO) \cdot (a + aa)^* + (\ONE + \ONE{}a) \cdot (a + aa)^* \;+\; $\\
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   757
& & $\qquad(\ZERO + \ZERO{}a + \ONE) \cdot (a + aa)^* + (\ONE + \ONE{}a) \cdot (a + aa)^*$\\
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   758
& $\ll$ & \ldots\\ \hspace{15mm}
876
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
   759
\end{tabular}
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   760
\end{center}}
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   761
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   762
\begin{textblock}{13.5}(1.5,12)
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   763
(regular expressions of sizes 98, 169, 283, 468, 767, \ldots)
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   764
\end{textblock}
876
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
   765
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
   766
\end{frame}
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   767
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
876
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
   768
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
   769
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
   770
\begin{frame}[c]
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   771
\frametitle{\mbox{Conclusion}}
876
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
   772
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
   773
\begin{itemize}
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   774
\item The beauty is that this only involves functional programs that can be conveniently reasoned about in theorem provers
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   775
\item POSIX lexing can be done via an extension by Sulzmann and Lu, 2014 (our current work)\medskip\pause
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   776
\item How surprising that one can still do new work on regular expressions.
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   777
\end{itemize}
876
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
   778
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
   779
\end{frame}
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   780
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
876
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
   781
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   782
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
876
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
   783
913
eef6a56c185a updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 906
diff changeset
   784
\begin{frame}<1-10>
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   785
\end{frame}
876
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
   786
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
   787
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
   788
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   789
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
876
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
   790
\end{document}
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
   791
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   792
%%% Local Variables:
876
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
   793
%%% mode: latex
771396fa6cc4 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 871
diff changeset
   794
%%% TeX-master: t
960
c7009356ddd8 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 913
diff changeset
   795
%%% End: