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