slides/slides02.tex
author Christian Urban <christian dot urban at kcl dot ac dot uk>
Fri, 25 Sep 2015 20:59:24 +0100
changeset 332 4755ad4b457b
parent 325 794c599cee53
child 335 2d112a7b29eb
permissions -rw-r--r--
updated
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
7
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     1
\documentclass[dvipsnames,14pt,t]{beamer}
258
1e4da6d2490c updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
     2
\usepackage{../slides}
1e4da6d2490c updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
     3
\usepackage{../graphics}
215
828303e8e4af updated slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 133
diff changeset
     4
\usepackage{../langs}
828303e8e4af updated slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 133
diff changeset
     5
\usepackage{../data}
7
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     6
258
1e4da6d2490c updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
     7
\hfuzz=220pt 
1e4da6d2490c updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
     8
1e4da6d2490c updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
     9
\lstset{language=Scala,
1e4da6d2490c updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    10
        style=mystyle,
1e4da6d2490c updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    11
        numbersep=0pt,
1e4da6d2490c updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    12
        numbers=none,
1e4da6d2490c updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    13
        xleftmargin=0mm}
1e4da6d2490c updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    14
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    15
\pgfplotsset{compat=1.11}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    16
258
1e4da6d2490c updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    17
\newcommand{\bl}[1]{\textcolor{blue}{#1}}     
117
25999de692b2 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
    18
7
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    19
% beamer stuff 
258
1e4da6d2490c updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    20
\renewcommand{\slidecaption}{AFL 02, King's College London}
1e4da6d2490c updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    21
7
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    22
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    23
\begin{document}
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    24
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    25
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
261
24531cfaa36a updated handouts
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 258
diff changeset
    26
\begin{frame}[t]
7
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    27
\frametitle{%
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    28
  \begin{tabular}{@ {}c@ {}}
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    29
  \\[-3mm]
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    30
  \LARGE Automata and \\[-2mm] 
16
Christian Urban <urbanc@in.tum.de>
parents: 15
diff changeset
    31
  \LARGE Formal Languages (2)\\[3mm] 
7
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    32
  \end{tabular}}
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    33
261
24531cfaa36a updated handouts
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 258
diff changeset
    34
  \normalsize
7
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    35
  \begin{center}
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    36
  \begin{tabular}{ll}
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    37
  Email:  & christian.urban at kcl.ac.uk\\
117
25999de692b2 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
    38
  Office: & S1.27 (1st floor Strand Building)\\
16
Christian Urban <urbanc@in.tum.de>
parents: 15
diff changeset
    39
  Slides: & KEATS 
7
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    40
  \end{tabular}
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    41
  \end{center}
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    42
261
24531cfaa36a updated handouts
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 258
diff changeset
    43
\end{frame}
24531cfaa36a updated handouts
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 258
diff changeset
    44
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
7
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    45
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    46
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
16
Christian Urban <urbanc@in.tum.de>
parents: 15
diff changeset
    47
\begin{frame}[c]
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    48
\frametitle{\begin{tabular}{@ {}c@ {}}An Efficient Regular\\[-1mm] 
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    49
    Expression Matcher\end{tabular}}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    50
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    51
\footnotesize
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    52
\begin{center}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    53
\begin{tabular}{@{}cc@{}}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    54
\begin{tikzpicture}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    55
\begin{axis}[
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    56
    xlabel={\pcode{a}s},
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    57
    ylabel={time in secs},
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    58
    enlargelimits=false,
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    59
    xtick={0,5,...,30},
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    60
    xmax=30,
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    61
    ymax=35,
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    62
    ytick={0,5,...,30},
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    63
    scaled ticks=false,
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    64
    axis lines=left,
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    65
    width=4.5cm,
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    66
    height=4.5cm, 
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    67
    legend entries={Python,Ruby},  
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    68
    legend pos=north west,
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    69
    legend cell align=left  
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    70
]
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    71
\addplot[blue,mark=*, mark options={fill=white}] 
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    72
  table {re-python.data};
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    73
\addplot[brown,mark=pentagon*, mark options={fill=white}] 
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    74
  table {re-ruby.data};  
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    75
\end{axis}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    76
\end{tikzpicture}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    77
&
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    78
\begin{tikzpicture}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    79
\begin{axis}[
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    80
    xlabel={\pcode{a}s},
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    81
    ylabel={time in secs},
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    82
    enlargelimits=false,
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    83
    xtick={0,3000,...,12000},
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    84
    xmax=12000,
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    85
    ymax=35,
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    86
    ytick={0,5,...,30},
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    87
    scaled ticks=false,
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    88
    axis lines=left,
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    89
    width=5.5cm,
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    90
    height=4.5cm
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    91
]
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    92
\addplot[green,mark=square*,mark options={fill=white}] table {re2b.data};
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    93
\addplot[black,mark=square*,mark options={fill=white}] table {re3.data};
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    94
\end{axis}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    95
\end{tikzpicture}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    96
\end{tabular}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    97
\end{center}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    98
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    99
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   100
\end{frame}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   101
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   102
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   103
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   104
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   105
\begin{frame}[c]
261
24531cfaa36a updated handouts
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 258
diff changeset
   106
\frametitle{Languages, Strings}
16
Christian Urban <urbanc@in.tum.de>
parents: 15
diff changeset
   107
261
24531cfaa36a updated handouts
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 258
diff changeset
   108
\begin{itemize}
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   109
\item \alert{\bf Strings} are lists of characters, for example
261
24531cfaa36a updated handouts
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 258
diff changeset
   110
\begin{center}
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   111
\bl{$[]$},\;\bl{$abc$}  \hspace{2cm}(Pattern match: \bl{$c\!::\!s$})
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   112
\end{center}\bigskip
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   113
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   114
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   115
\item A \alert{\bf language} is a set of strings, for example\medskip
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   116
\begin{center}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   117
\bl{$\{[], hello, \textit{foobar}, a, abc\}$}
261
24531cfaa36a updated handouts
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 258
diff changeset
   118
\end{center}\bigskip
16
Christian Urban <urbanc@in.tum.de>
parents: 15
diff changeset
   119
332
4755ad4b457b updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 325
diff changeset
   120
\item \alert{\bf Concatenation} of strings and languages
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   121
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   122
\begin{center}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   123
\begin{tabular}{rcl}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   124
\bl{$\textit{foo}\;@\;bar$} & \bl{$=$} & \bl{$\textit{foobar}$}\medskip\\
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   125
\bl{$A\;@\;B$} & \bl{$\dn$} & \bl{$\{ s_1\,@\,s_2 \;\mid\; s_1 \in A \wedge s_2 \in B\}$}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   126
\end{tabular}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   127
\end{center}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   128
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   129
%\item The \alert{\bf meaning} of a regular expression is a set of 
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   130
%  strings, or language.
261
24531cfaa36a updated handouts
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 258
diff changeset
   131
\end{itemize}  
24531cfaa36a updated handouts
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 258
diff changeset
   132
24531cfaa36a updated handouts
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 258
diff changeset
   133
\end{frame}
16
Christian Urban <urbanc@in.tum.de>
parents: 15
diff changeset
   134
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
Christian Urban <urbanc@in.tum.de>
parents: 15
diff changeset
   135
117
25999de692b2 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   136
25999de692b2 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   137
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
25999de692b2 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   138
\begin{frame}[t]
7
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   139
\frametitle{\begin{tabular}{c}Regular Expressions\end{tabular}}
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   140
15
Christian Urban <urbanc@in.tum.de>
parents: 11
diff changeset
   141
Their inductive definition:
Christian Urban <urbanc@in.tum.de>
parents: 11
diff changeset
   142
Christian Urban <urbanc@in.tum.de>
parents: 11
diff changeset
   143
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   144
\begin{textblock}{6}(2,7.5)
7
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   145
  \begin{tabular}{@ {}rrl@ {\hspace{13mm}}l}
119
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   146
  \bl{$r$} & \bl{$::=$}  & \bl{$\varnothing$}  & null\\
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   147
         & \bl{$\mid$} & \bl{$\epsilon$}       & empty string / \pcode{""} / $[]$\\
119
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   148
         & \bl{$\mid$} & \bl{$c$}                         & character\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   149
         & \bl{$\mid$} & \bl{$r_1 \cdot r_2$} & sequence\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   150
         & \bl{$\mid$} & \bl{$r_1 + r_2$}  & alternative / choice\\
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   151
         & \bl{$\mid$} & \bl{$r^*$}            & star (zero or more)\\
7
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   152
  \end{tabular}
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   153
  \end{textblock}
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   154
  
332
4755ad4b457b updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 325
diff changeset
   155
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   156
\end{frame}
16
Christian Urban <urbanc@in.tum.de>
parents: 15
diff changeset
   157
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
Christian Urban <urbanc@in.tum.de>
parents: 15
diff changeset
   158
Christian Urban <urbanc@in.tum.de>
parents: 15
diff changeset
   159
Christian Urban <urbanc@in.tum.de>
parents: 15
diff changeset
   160
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
7
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   161
\begin{frame}[c]
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   162
\frametitle{\begin{tabular}{c}The Meaning of a\\[-2mm] Regular Expression\end{tabular}}
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   163
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   164
\begin{textblock}{15}(1,4)
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   165
 \begin{tabular}{@ {}rcl}
117
25999de692b2 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   166
 \bl{$L(\varnothing)$}     & \bl{$\dn$} & \bl{$\varnothing$}\\
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   167
 \bl{$L(\epsilon)$}        & \bl{$\dn$} & \bl{$\{$[]$\}$}\\
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   168
 \bl{$L(c)$}               & \bl{$\dn$} & \bl{$\{[c]\}$}\\
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   169
 \bl{$L(r_1 + r_2)$}       & \bl{$\dn$} & \bl{$L(r_1) \cup L(r_2)$}\\
117
25999de692b2 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   170
 \bl{$L(r_1 \cdot r_2)$}  & \bl{$\dn$} & \bl{$L(r_1) \,@\, L(r_2)$}\\
25999de692b2 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   171
 \bl{$L(r^*)$}                   & \bl{$\dn$} & \bl{$\bigcup_{n \ge 0} L(r)^n$}\\
7
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   172
  \end{tabular}\bigskip
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   173
  
117
25999de692b2 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   174
\only<2->{  
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   175
\hspace{5mm}\textcolor{blue}{$L(r)^0 \;\dn\; \{[]\}$}\\
117
25999de692b2 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   176
\textcolor{blue}{$L(r)^{n+1} \;\dn\; L(r) \,@\, L(r)^n$}}  
11
5353d405e4e6 added slides 2
Christian Urban <urbanc@in.tum.de>
parents: 7
diff changeset
   177
\end{textblock}
7
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   178
117
25999de692b2 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   179
\only<1->{
16
Christian Urban <urbanc@in.tum.de>
parents: 15
diff changeset
   180
\begin{textblock}{6}(9,12)\small
Christian Urban <urbanc@in.tum.de>
parents: 15
diff changeset
   181
\bl{$L$} is a function from regular expressions to sets of strings\\
117
25999de692b2 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   182
\bl{$L$ : Rexp $\Rightarrow$ Set$[$String$]$}
16
Christian Urban <urbanc@in.tum.de>
parents: 15
diff changeset
   183
\end{textblock}}
Christian Urban <urbanc@in.tum.de>
parents: 15
diff changeset
   184
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   185
\end{frame}
7
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   186
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   187
16
Christian Urban <urbanc@in.tum.de>
parents: 15
diff changeset
   188
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <urbanc@in.tum.de>
parents: 15
diff changeset
   189
\begin{frame}[c]
Christian Urban <urbanc@in.tum.de>
parents: 15
diff changeset
   190
Christian Urban <urbanc@in.tum.de>
parents: 15
diff changeset
   191
\large
Christian Urban <urbanc@in.tum.de>
parents: 15
diff changeset
   192
\begin{center}
117
25999de692b2 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   193
What is \bl{$L(a^*)$}?
16
Christian Urban <urbanc@in.tum.de>
parents: 15
diff changeset
   194
\end{center}  
Christian Urban <urbanc@in.tum.de>
parents: 15
diff changeset
   195
  
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   196
\end{frame}
16
Christian Urban <urbanc@in.tum.de>
parents: 15
diff changeset
   197
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
Christian Urban <urbanc@in.tum.de>
parents: 15
diff changeset
   198
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   199
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
332
4755ad4b457b updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 325
diff changeset
   200
\begin{frame}[c]
4755ad4b457b updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 325
diff changeset
   201
\frametitle{\begin{tabular}{c}
4755ad4b457b updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 325
diff changeset
   202
 When Are Two Regular\\
4755ad4b457b updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 325
diff changeset
   203
 Expressions Equivalent?\end{tabular}}
4755ad4b457b updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 325
diff changeset
   204
\large
4755ad4b457b updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 325
diff changeset
   205
\begin{center}
4755ad4b457b updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 325
diff changeset
   206
\bl{$r_1 \equiv r_2 \;\;\dn\;\; L(r_1) = L(r_2)$}
4755ad4b457b updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 325
diff changeset
   207
\end{center}  
4755ad4b457b updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 325
diff changeset
   208
  
4755ad4b457b updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 325
diff changeset
   209
\end{frame}
4755ad4b457b updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 325
diff changeset
   210
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
4755ad4b457b updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 325
diff changeset
   211
4755ad4b457b updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 325
diff changeset
   212
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   213
\begin{frame}[t]
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   214
\frametitle{\begin{tabular}{c}Concrete Equivalences\end{tabular}}
16
Christian Urban <urbanc@in.tum.de>
parents: 15
diff changeset
   215
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   216
\begin{center}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   217
\bl{\begin{tabular}{rcl}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   218
$(a + b)  + c$ & $\equiv$ & $a + (b + c)$\\
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   219
$a + a$        & $\equiv$ & $a$\\
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   220
$a + b$        & $\equiv$ & $b + a$\\
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   221
$(a \cdot b) \cdot c$ & $\equiv$ & $a \cdot (b \cdot c)$\\
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   222
$c \cdot (a + b)$ & $\equiv$ & $(c \cdot a) + (c \cdot b)$\bigskip\bigskip\\\pause
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   223
$a \cdot a$       & $\not\equiv$ & $a$\\
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   224
$a + (b \cdot c)$ & $\not\equiv$ & $(a + b) \cdot (a + c)$\\
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   225
\end{tabular}}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   226
\end{center}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   227
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   228
\end{frame}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   229
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   230
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   231
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   232
\begin{frame}[t]
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   233
\frametitle{\begin{tabular}{c}Corner Cases\end{tabular}}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   234
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   235
\begin{center}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   236
\bl{\begin{tabular}{rcl}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   237
$a \cdot \varnothing$ & $\not\equiv$ & $a$\\
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   238
$a + \epsilon$ & $\not\equiv$ & $a$\\
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   239
$\epsilon$ & $\equiv$ & $\varnothing^*$\\
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   240
$\epsilon^*$ & $\equiv$ & $\epsilon$\\
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   241
$\varnothing^*$ & $\not\equiv$ & $\varnothing$\\
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   242
\end{tabular}}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   243
\end{center}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   244
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   245
\end{frame}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   246
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   247
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   248
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   249
\begin{frame}[t]
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   250
\frametitle{\begin{tabular}{c}Simplification Rules\end{tabular}}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   251
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   252
\begin{center}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   253
\bl{\begin{tabular}{rcl}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   254
$r + \varnothing$  & $\equiv$ & $r$\\
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   255
$\varnothing + r$  & $\equiv$ & $r$\\
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   256
$r \cdot \epsilon$ & $\equiv$ & $r$\\
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   257
$\epsilon \cdot r$     & $\equiv$ & $r$\\
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   258
$r \cdot \varnothing$ & $\equiv$ & $\varnothing$\\
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   259
$\varnothing \cdot r$ & $\equiv$ & $\varnothing$\\
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   260
$r + r$ & $\equiv$ & $r$
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   261
\end{tabular}}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   262
\end{center}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   264
\end{frame}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   265
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
16
Christian Urban <urbanc@in.tum.de>
parents: 15
diff changeset
   266
11
5353d405e4e6 added slides 2
Christian Urban <urbanc@in.tum.de>
parents: 7
diff changeset
   267
\newcommand{\YES}{\textcolor{gray}{yes}}
5353d405e4e6 added slides 2
Christian Urban <urbanc@in.tum.de>
parents: 7
diff changeset
   268
\newcommand{\NO}{\textcolor{gray}{no}}
5353d405e4e6 added slides 2
Christian Urban <urbanc@in.tum.de>
parents: 7
diff changeset
   269
\newcommand{\FORALLR}{\textcolor{gray}{$\forall$ r.}}
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   270
7
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   271
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   272
\begin{frame}[c]
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   273
\frametitle{\begin{tabular}{c}The Specification\\[-1mm] for Matching\end{tabular}}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   274
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   275
\large
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   276
A regular expression \bl{$r$} matches a string \bl{$s$}\\ if and only if
7
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   277
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   278
\begin{center}
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   279
\bl{$s \in L(r)$}\\ 
7
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   280
\end{center}
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   281
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   282
\end{frame}
7
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   283
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   284
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   285
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   286
\mode<presentation>{
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   287
\begin{frame}[c]
117
25999de692b2 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   288
\frametitle{\begin{tabular}{c}\bl{$(a?\{n\}) \cdot a\{n\}$}\end{tabular}}
25999de692b2 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   289
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   290
\begin{center}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   291
\begin{tikzpicture}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   292
\begin{axis}[
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   293
    xlabel={\pcode{a}s},
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   294
    ylabel={time in secs},
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   295
    enlargelimits=false,
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   296
    xtick={0,5,...,30},
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   297
    xmax=30,
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   298
    ymax=35,
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   299
    ytick={0,5,...,30},
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   300
    scaled ticks=false,
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   301
    axis lines=left,
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   302
    width=9cm,
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   303
    height=7cm, 
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   304
    legend entries={Python,Ruby},  
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   305
    legend pos=north west,
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   306
    legend cell align=left  
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   307
]
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   308
\addplot[blue,mark=*, mark options={fill=white}] 
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   309
  table {re-python.data};
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   310
\addplot[brown,mark=pentagon*, mark options={fill=white}] 
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   311
  table {re-ruby.data};  
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   312
\end{axis}
117
25999de692b2 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   313
\end{tikzpicture}
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   314
\end{center}
11
5353d405e4e6 added slides 2
Christian Urban <urbanc@in.tum.de>
parents: 7
diff changeset
   315
5353d405e4e6 added slides 2
Christian Urban <urbanc@in.tum.de>
parents: 7
diff changeset
   316
\end{frame}}
5353d405e4e6 added slides 2
Christian Urban <urbanc@in.tum.de>
parents: 7
diff changeset
   317
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
5353d405e4e6 added slides 2
Christian Urban <urbanc@in.tum.de>
parents: 7
diff changeset
   318
5353d405e4e6 added slides 2
Christian Urban <urbanc@in.tum.de>
parents: 7
diff changeset
   319
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
5353d405e4e6 added slides 2
Christian Urban <urbanc@in.tum.de>
parents: 7
diff changeset
   320
\mode<presentation>{
118
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 117
diff changeset
   321
\begin{frame}[c]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 117
diff changeset
   322
\frametitle{\begin{tabular}{c}Evil Regular Expressions\end{tabular}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 117
diff changeset
   323
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 117
diff changeset
   324
\begin{itemize}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 117
diff changeset
   325
\item \alert{R}egular \alert{e}xpression \alert{D}enial \alert{o}f \alert{S}ervice (ReDoS)\bigskip
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 117
diff changeset
   326
\item Evil regular expressions\medskip
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 117
diff changeset
   327
\begin{itemize}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 117
diff changeset
   328
\item \bl{$(a?\{n\}) \cdot a\{n\}$}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 117
diff changeset
   329
\item \bl{$(a^+)^+$}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 117
diff changeset
   330
\item \bl{$([a$\,-\,$z]^+)^*$}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 117
diff changeset
   331
\item \bl{$(a + a \cdot a)^+$}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 117
diff changeset
   332
\item \bl{$(a + a?)^+$}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 117
diff changeset
   333
\end{itemize}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 117
diff changeset
   334
\end{itemize}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 117
diff changeset
   335
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 117
diff changeset
   336
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 117
diff changeset
   337
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 117
diff changeset
   338
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 117
diff changeset
   339
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 117
diff changeset
   340
\mode<presentation>{
11
5353d405e4e6 added slides 2
Christian Urban <urbanc@in.tum.de>
parents: 7
diff changeset
   341
\begin{frame}[t]
5353d405e4e6 added slides 2
Christian Urban <urbanc@in.tum.de>
parents: 7
diff changeset
   342
\frametitle{\begin{tabular}{c}A Matching Algorithm\end{tabular}}
5353d405e4e6 added slides 2
Christian Urban <urbanc@in.tum.de>
parents: 7
diff changeset
   343
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   344
117
25999de692b2 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   345
\ldots{}whether a regular expression can match the empty string:
11
5353d405e4e6 added slides 2
Christian Urban <urbanc@in.tum.de>
parents: 7
diff changeset
   346
\begin{center}
117
25999de692b2 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   347
\begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {}}
25999de692b2 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   348
\bl{$nullable(\varnothing)$}      & \bl{$\dn$} & \bl{$f\!\/alse$}\\
25999de692b2 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   349
\bl{$nullable(\epsilon)$}           & \bl{$\dn$} &  \bl{$true$}\\
25999de692b2 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   350
\bl{$nullable (c)$}                    & \bl{$\dn$} &  \bl{$f\!alse$}\\
25999de692b2 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   351
\bl{$nullable (r_1 + r_2)$}       & \bl{$\dn$} &  \bl{$nullable(r_1) \vee nullable(r_2)$} \\ 
25999de692b2 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   352
\bl{$nullable (r_1 \cdot r_2)$} & \bl{$\dn$} &  \bl{$nullable(r_1) \wedge nullable(r_2)$} \\
25999de692b2 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   353
\bl{$nullable (r^*)$}                 & \bl{$\dn$} & \bl{$true$} \\
25999de692b2 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   354
\end{tabular}
16
Christian Urban <urbanc@in.tum.de>
parents: 15
diff changeset
   355
\end{center}
Christian Urban <urbanc@in.tum.de>
parents: 15
diff changeset
   356
11
5353d405e4e6 added slides 2
Christian Urban <urbanc@in.tum.de>
parents: 7
diff changeset
   357
\end{frame}}
5353d405e4e6 added slides 2
Christian Urban <urbanc@in.tum.de>
parents: 7
diff changeset
   358
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
5353d405e4e6 added slides 2
Christian Urban <urbanc@in.tum.de>
parents: 7
diff changeset
   359
5353d405e4e6 added slides 2
Christian Urban <urbanc@in.tum.de>
parents: 7
diff changeset
   360
5353d405e4e6 added slides 2
Christian Urban <urbanc@in.tum.de>
parents: 7
diff changeset
   361
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
5353d405e4e6 added slides 2
Christian Urban <urbanc@in.tum.de>
parents: 7
diff changeset
   362
\mode<presentation>{
5353d405e4e6 added slides 2
Christian Urban <urbanc@in.tum.de>
parents: 7
diff changeset
   363
\begin{frame}[c]
15
Christian Urban <urbanc@in.tum.de>
parents: 11
diff changeset
   364
\frametitle{\begin{tabular}{c}The Derivative of a Rexp\end{tabular}}
7
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   365
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   366
\large
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   367
If \bl{$r$} matches the string \bl{$c\!::\!s$}, what is a regular 
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   368
expression that matches \bl{$s$}?\bigskip\bigskip\bigskip\bigskip
7
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   369
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   370
\small
325
794c599cee53 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 263
diff changeset
   371
\bl{$der\,c\,r$} gives the answer, Brzozowski 1964
7
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   372
\end{frame}}
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   373
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   374
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   375
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   376
\mode<presentation>{
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   377
\begin{frame}[c]
19
Christian Urban <urbanc@in.tum.de>
parents: 17
diff changeset
   378
\frametitle{\begin{tabular}{c}The Derivative of a Rexp (2)\end{tabular}}
7
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   379
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   380
\begin{center}
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   381
\begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{-10mm}}l@ {}}
117
25999de692b2 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   382
  \bl{$der\, c\, (\varnothing)$}      & \bl{$\dn$} & \bl{$\varnothing$} & \\
25999de692b2 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   383
  \bl{$der\, c\, (\epsilon)$}           & \bl{$\dn$} & \bl{$\varnothing$} & \\
25999de692b2 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   384
  \bl{$der\, c\, (d)$}                     & \bl{$\dn$} & \bl{if $c = d$ then $\epsilon$ else $\varnothing$} & \\
25999de692b2 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   385
  \bl{$der\, c\, (r_1 + r_2)$}        & \bl{$\dn$} & \bl{$der\, c\, r_1 + der\, c\, r_2$} & \\
25999de692b2 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   386
  \bl{$der\, c\, (r_1 \cdot r_2)$}  & \bl{$\dn$}  & \bl{if $nullable (r_1)$}\\
25999de692b2 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   387
  & & \bl{then $(der\,c\,r_1) \cdot r_2 + der\, c\, r_2$}\\ 
25999de692b2 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   388
  & & \bl{else $(der\, c\, r_1) \cdot r_2$}\\
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   389
  \bl{$der\, c\, (r^*)$}          & \bl{$\dn$} & \bl{$(der\,c\,r) \cdot (r^*)$} &\medskip\\\pause
7
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   390
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   391
  \bl{$\textit{ders}\, []\, r$}     & \bl{$\dn$} & \bl{$r$} & \\
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   392
  \bl{$\textit{ders}\, (c\!::\!s)\, r$} & \bl{$\dn$} & \bl{$\textit{ders}\,s\,(der\,c\,r)$} & \\
7
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   393
  \end{tabular}
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   394
\end{center}
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   395
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   396
\end{frame}}
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   397
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   398
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   399
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   400
\mode<presentation>{
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   401
\begin{frame}[c]
119
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   402
\frametitle{\begin{tabular}{c}Examples\end{tabular}}
7
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   403
119
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   404
Given \bl{$r \dn ((a \cdot b) + b)^*$} what is
7
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   405
119
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   406
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   407
\begin{tabular}{l}
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   408
\bl{$der\,a\,r =?$}\\
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   409
\bl{$der\,b\,r =?$}\\
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   410
\bl{$der\,c\,r =?$}
119
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   411
\end{tabular}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   412
\end{center}
7
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   413
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   414
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   415
\end{frame}}
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   416
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   417
17
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   418
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   419
\mode<presentation>{
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   420
\begin{frame}[t]
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   421
\frametitle{The Algorithm}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   422
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   423
\begin{center}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   424
\begin{tabular}{@{}rll@{}}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   425
Input: & \bl{$r_1$}, \bl{$abc$}\medskip\\
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   426
Step 1: & build derivative of \bl{$a$} and \bl{$r_1$} & \bl{$(r_2 = der\,a\,r_1)$}\smallskip\\
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   427
Step 2: & build derivative of \bl{$b$} and \bl{$r_2$} & \bl{$(r_3 = der\,b\,r_2)$}\smallskip\\
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   428
Step 3: & build derivative of \bl{$c$} and \bl{$r_3$} & \bl{$(r_4 = der\,b\,r_3)$}\smallskip\\
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   429
Step 4: & the string is exhausted; test & (\bl{$nullable(r_4)$})\\
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   430
        & whether \bl{$r_4$} can recognise\\
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   431
        & the empty string\smallskip\\
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   432
Output: & result of the test\\
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   433
        & $\Rightarrow true \,\text{or}\, \textit{false}$\\        
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   434
\end{tabular}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   435
\end{center}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   436
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   437
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   438
\end{frame}}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   439
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   440
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   441
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   442
\mode<presentation>{
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   443
\begin{frame}[c]
119
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   444
\frametitle{\begin{tabular}{c}\bl{$(a?\{n\}) \cdot a\{n\}$}\end{tabular}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   445
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   446
\begin{center}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   447
\begin{tikzpicture}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   448
\begin{axis}[
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   449
    xlabel={\pcode{a}s},
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   450
    ylabel={time in secs},
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   451
    enlargelimits=false,
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   452
    xtick={0,5,...,30},
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   453
    xmax=30,
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   454
    ytick={0,5,...,30},
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   455
    scaled ticks=false,
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   456
    axis lines=left,
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   457
    width=7cm,
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   458
    height=7cm, 
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   459
    legend entries={Python,Ruby,Scala V1},  
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   460
    legend pos=outer north east,
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   461
    legend cell align=left  
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   462
]
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   463
\addplot[blue,mark=*, mark options={fill=white}] 
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   464
  table {re-python.data};
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   465
\addplot[brown,mark=pentagon*, mark options={fill=white}] 
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   466
  table {re-ruby.data};  
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   467
\addplot[red,mark=triangle*,mark options={fill=white}] 
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   468
  table {re1.data};  
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   469
\end{axis}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   470
\end{tikzpicture}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   471
\end{center}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   472
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   473
\end{frame}}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   474
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   475
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   476
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   477
\mode<presentation>{
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   478
\begin{frame}[c]
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   479
\frametitle{\begin{tabular}{c}A Problem\end{tabular}}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   480
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   481
We represented the ``n-times'' \bl{$a\{n\}$} as a sequence regular expression:
119
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   482
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   483
\begin{center}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   484
\begin{tabular}{rl}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   485
1: & \bl{$a$}\\
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   486
2: & \bl{$a\cdot a$}\\
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   487
3: & \bl{$a\cdot a\cdot a$}\\
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   488
& \ldots\\
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   489
13: & \bl{$a\cdot a\cdot a\cdot a\cdot a\cdot a\cdot a\cdot a\cdot a\cdot a\cdot a\cdot a\cdot a$}\\
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   490
& \ldots\\
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   491
20:
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   492
\end{tabular}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   493
\end{center}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   494
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   495
This problem is aggravated with \bl{$a?$} being represented as \bl{$\epsilon + a$}.
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   496
\end{frame}}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   497
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   498
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   499
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   500
\mode<presentation>{
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   501
\begin{frame}[c]
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   502
\frametitle{\begin{tabular}{c}Solving the Problem\end{tabular}}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   503
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   504
What happens if we extend our regular expressions
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   505
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   506
\begin{center}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   507
\begin{tabular}{rcl}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   508
\bl{$r$} & \bl{$::=$} & \bl{\ldots}\\
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   509
             & \bl{$\mid$} & \bl{$r\{n\}$}\\
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   510
             & \bl{$\mid$} & \bl{$r?$} 
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   511
\end{tabular}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   512
\end{center}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   513
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   514
What is their meaning? What are the cases for \bl{$nullable$} and \bl{$der$}?
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   515
\end{frame}}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   516
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   517
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   518
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   519
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   520
\mode<presentation>{
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   521
\begin{frame}[t]
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   522
\frametitle{\begin{tabular}{c}\bl{$(a?\{n\}) \cdot a\{n\}$}\end{tabular}}
119
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   523
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   524
\begin{center}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   525
\begin{tikzpicture}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   526
\begin{axis}[
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   527
    xlabel={\pcode{a}s},
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   528
    ylabel={time in secs},
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   529
    enlargelimits=false,
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   530
    xtick={0,200,...,1000},
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   531
    xmax=1000,
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   532
    ytick={0,5,...,30},
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   533
    scaled ticks=false,
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   534
    axis lines=left,
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   535
    width=9.5cm,
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   536
    height=7cm, 
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   537
    legend entries={Python,Ruby,Scala V1,Scala V2},  
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   538
    legend pos=north west,
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   539
    legend cell align=left  
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   540
]
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   541
\addplot[blue,mark=*, mark options={fill=white}] 
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   542
  table {re-python.data};
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   543
\addplot[brown,mark=pentagon*, mark options={fill=white}] 
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   544
  table {re-ruby.data};  
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   545
\addplot[red,mark=triangle*,mark options={fill=white}] 
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   546
  table {re1.data};  
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   547
\addplot[green,mark=square*,mark options={fill=white}] 
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   548
  table {re2b.data};
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   549
\end{axis}
119
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   550
\end{tikzpicture}
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   551
\end{center}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   552
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   553
\end{frame}}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   554
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   555
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   556
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   557
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   558
\mode<presentation>{
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   559
\begin{frame}[c]
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   560
\frametitle{\begin{tabular}{c}Examples\end{tabular}}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   561
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   562
Recall the example of \bl{$r \dn ((a \cdot b) + b)^*$} with
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   563
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   564
\begin{center}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   565
\begin{tabular}{l}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   566
\bl{$der\,a\,r = ((\epsilon \cdot b) + \varnothing) \cdot r$}\\
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   567
\bl{$der\,b\,r = ((\varnothing \cdot b) + \epsilon)\cdot r$}\\
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   568
\bl{$der\,c\,r = ((\varnothing \cdot b) + \varnothing)\cdot r$}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   569
\end{tabular}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   570
\end{center}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   571
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   572
What are these regular expressions equivalent to?
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   573
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   574
\end{frame}}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   575
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   576
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   577
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   578
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   579
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   580
\mode<presentation>{
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   581
\begin{frame}[t]
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   582
\frametitle{\begin{tabular}{c}\bl{$(a?\{n\}) \cdot a\{n\}$}\end{tabular}}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   583
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   584
\begin{center}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   585
\begin{tikzpicture}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   586
\begin{axis}[
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   587
    xlabel={\pcode{a}s},
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   588
    ylabel={time in secs},
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   589
    enlargelimits=false,
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   590
    xtick={0,3000,...,12000},
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   591
    xmax=12000,
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   592
    ymax=35,
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   593
    ytick={0,5,...,30},
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   594
    scaled ticks=false,
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   595
    axis lines=left,
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   596
    width=9cm,
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   597
    height=7cm
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   598
]
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   599
\addplot[green,mark=square*,mark options={fill=white}] table {re2b.data};
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   600
\addplot[black,mark=square*,mark options={fill=white}] table {re3.data};
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   601
\end{axis}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   602
\end{tikzpicture}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   603
\end{center}
119
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   604
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   605
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   606
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   607
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   608
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   609
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   610
\begin{frame}[t]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   611
\frametitle{\begin{tabular}{c}Proofs about Rexps\end{tabular}}
17
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   612
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   613
Remember their inductive definition:\\[5cm]
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   614
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   615
\begin{textblock}{6}(5,5)
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   616
  \begin{tabular}{@ {}rrl}
119
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   617
  \bl{$r$} & \bl{$::=$}  & \bl{$\varnothing$}\\
17
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   618
         & \bl{$\mid$} & \bl{$\epsilon$}       \\
119
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   619
         & \bl{$\mid$} & \bl{$c$}                        \\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   620
         & \bl{$\mid$} & \bl{$r_1 \cdot r_2$}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   621
         & \bl{$\mid$} & \bl{$r_1 + r_2$}  \\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   622
         & \bl{$\mid$} & \bl{$r^*$}                  \\
17
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   623
  \end{tabular}
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   624
  \end{textblock}
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   625
119
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   626
If we want to prove something, say a property \bl{$P(r)$}, for all regular expressions \bl{$r$} then \ldots
17
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   627
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   628
\end{frame}}
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   629
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   630
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   631
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   632
\mode<presentation>{
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   633
\begin{frame}[c]
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   634
\frametitle{\begin{tabular}{c}Proofs about Rexp (2)\end{tabular}}
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   635
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   636
\begin{itemize}
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   637
\item \bl{$P$} holds for \bl{$\varnothing$}, \bl{$\epsilon$} and \bl{c}\bigskip
119
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   638
\item \bl{$P$} holds for \bl{$r_1 + r_2$} under the assumption that \bl{$P$} already
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   639
holds for \bl{$r_1$} and \bl{$r_2$}.\bigskip
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   640
\item \bl{$P$} holds for \bl{$r_1 \cdot r_2$} under the assumption that \bl{$P$} already
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   641
holds for \bl{$r_1$} and \bl{$r_2$}.\bigskip
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   642
\item \bl{$P$} holds for \bl{$r^*$} under the assumption that \bl{$P$} already
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   643
holds for \bl{$r$}.
17
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   644
\end{itemize}
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   645
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   646
\end{frame}}
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   647
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   648
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   649
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   650
\mode<presentation>{
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   651
\begin{frame}[c]
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   652
\frametitle{\begin{tabular}{c}Proofs about Rexp (3)\end{tabular}}
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   653
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   654
Assume \bl{$P(r)$} is the property:
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   655
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   656
\begin{center}
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   657
\bl{$nullable(r)$} if and only if \bl{$[] \in L(r)$}
17
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   658
\end{center}
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   659
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   660
\end{frame}}
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   661
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   662
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   663
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   664
\mode<presentation>{
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   665
\begin{frame}[c]
119
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   666
\frametitle{\begin{tabular}{c}Proofs about Rexp (4)\end{tabular}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   667
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   668
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   669
\begin{center}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   670
\bl{\begin{tabular}{r@{\hspace{1mm}}c@{\hspace{1mm}}l}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   671
$rev(\varnothing)$   & $\dn$ & $\varnothing$\\
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   672
$rev(\epsilon)$         & $\dn$ & $\epsilon$\\
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   673
$rev(c)$                      & $\dn$ & $c$\\
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   674
$rev(r_1 + r_2)$        & $\dn$ & $rev(r_1) + rev(r_2)$\\
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   675
$rev(r_1 \cdot r_2)$  & $\dn$ & $rev(r_2) \cdot rev(r_1)$\\
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   676
$rev(r^*)$                   & $\dn$ & $rev(r)^*$\\
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   677
\end{tabular}}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   678
\end{center}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   679
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   680
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   681
We can prove
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   682
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   683
\begin{center}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   684
\bl{$L(rev(r)) = \{s^{-1} \;|\; s \in L(r)\}$}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   685
\end{center}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   686
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   687
by induction on \bl{$r$}.
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   688
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   689
\end{frame}}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   690
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   691
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   692
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   693
\mode<presentation>{
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   694
\begin{frame}[c]
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   695
\frametitle{\begin{tabular}{c}Proofs about Rexp (5)\end{tabular}}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   696
119
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   697
Let \bl{$Der\,c\,A$} be the set defined as
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   698
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   699
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   700
\bl{$Der\,c\,A \dn \{ s \;|\;  c\!::\!s \in A\}$ } 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   701
\end{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   702
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   703
We can prove
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   704
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   705
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   706
\bl{$L(der\,c\,r) = Der\,c\,(L(r))$}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   707
\end{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   708
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   709
by induction on \bl{$r$}.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   710
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   711
\end{frame}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   712
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   713
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   714
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   715
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   716
\mode<presentation>{
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   717
\begin{frame}[c]
17
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   718
\frametitle{\begin{tabular}{c}Proofs about Strings\end{tabular}}
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   719
119
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   720
If we want to prove something, say a property \bl{$P(s)$}, for all strings \bl{$s$} then \ldots\bigskip
17
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   721
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   722
\begin{itemize}
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   723
\item \bl{$P$} holds for the empty string, and\medskip
119
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   724
\item \bl{$P$} holds for the string \bl{$c\!::\!s$} under the assumption that \bl{$P$}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   725
already holds for \bl{$s$}
17
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   726
\end{itemize}
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   727
\end{frame}}
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   728
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   729
19
Christian Urban <urbanc@in.tum.de>
parents: 17
diff changeset
   730
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <urbanc@in.tum.de>
parents: 17
diff changeset
   731
\mode<presentation>{
Christian Urban <urbanc@in.tum.de>
parents: 17
diff changeset
   732
\begin{frame}[c]
Christian Urban <urbanc@in.tum.de>
parents: 17
diff changeset
   733
\frametitle{\begin{tabular}{c}Proofs about Strings (2)\end{tabular}}
Christian Urban <urbanc@in.tum.de>
parents: 17
diff changeset
   734
119
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   735
We can finally prove
19
Christian Urban <urbanc@in.tum.de>
parents: 17
diff changeset
   736
Christian Urban <urbanc@in.tum.de>
parents: 17
diff changeset
   737
\begin{center}
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   738
\bl{$matches(r, s)$}  if and only if  \bl{$s \in L(r)$} 
19
Christian Urban <urbanc@in.tum.de>
parents: 17
diff changeset
   739
\end{center}
Christian Urban <urbanc@in.tum.de>
parents: 17
diff changeset
   740
Christian Urban <urbanc@in.tum.de>
parents: 17
diff changeset
   741
Christian Urban <urbanc@in.tum.de>
parents: 17
diff changeset
   742
\end{frame}}
Christian Urban <urbanc@in.tum.de>
parents: 17
diff changeset
   743
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
17
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   744
7
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   745
\end{document}
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   746
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   747
%%% Local Variables:  
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   748
%%% mode: latex
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   749
%%% TeX-master: t
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   750
%%% End: 
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   751