slides/slides02.tex
author Christian Urban <urbanc@in.tum.de>
Wed, 27 Sep 2017 14:46:20 +0100
changeset 507 fdbc7d0ec04f
parent 500 c502933be072
child 510 25580bf89ac0
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
398
c8ce95067c1a updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 345
diff changeset
    15
\pgfplotsset{compat=1.12}
263
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 
429
7e71c947ec69 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
    20
\renewcommand{\slidecaption}{CFL 02, King's College London}
258
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]
429
7e71c947ec69 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
    30
  \LARGE Compilers and \\[-1mm] 
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\\
500
c502933be072 updated
Christian Urban <urbanc@in.tum.de>
parents: 442
diff changeset
    38
  Office: & N7.07 (North Wing, Bush House)\\
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]
335
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
    48
\frametitle{\begin{tabular}{@ {}c@ {}}
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
    49
    An Efficient Regular\\[-1mm] 
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    50
    Expression Matcher\end{tabular}}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    51
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    52
\footnotesize
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    53
\begin{center}
433
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
    54
  {\normalsize Graphs: \bl{$a^{?\{n\}} \cdot a^{\{n\}}$} and strings \bl{$\underbrace{\,a\ldots a\,}_{n}$}}\\
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    55
\begin{tabular}{@{}cc@{}}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    56
\begin{tikzpicture}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    57
\begin{axis}[
433
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
    58
    xlabel={$n$},
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
    59
    x label style={at={(1.05,0.0)}},
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    60
    ylabel={time in secs},
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    61
    enlargelimits=false,
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    62
    xtick={0,5,...,30},
433
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
    63
    xmax=33,
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    64
    ymax=35,
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    65
    ytick={0,5,...,30},
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    66
    scaled ticks=false,
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    67
    axis lines=left,
433
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
    68
    width=5cm,
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    69
    height=4.5cm, 
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    70
    legend entries={Python,Ruby},  
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    71
    legend pos=north west,
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    72
    legend cell align=left  
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    73
]
433
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
    74
\addplot[blue,mark=*, mark options={fill=white}] table {re-python.data};
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
    75
\addplot[brown,mark=pentagon*, mark options={fill=white}] table {re-ruby.data};  
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    76
\end{axis}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    77
\end{tikzpicture}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    78
&
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    79
\begin{tikzpicture}
433
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
    80
  \begin{axis}[
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
    81
    xlabel={$n$},
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
    82
    x label style={at={(1.1,0.05)}},
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    83
    ylabel={time in secs},
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    84
    enlargelimits=false,
442
84d6714840c9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 436
diff changeset
    85
    xtick={0,5000,...,10000},
84d6714840c9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 436
diff changeset
    86
    xmax=11500,
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    87
    ymax=35,
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    88
    ytick={0,5,...,30},
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    89
    scaled ticks=false,
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    90
    axis lines=left,
433
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
    91
    width=5cm,
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    92
    height=4.5cm
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    93
]
433
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
    94
\addplot[green,mark=square*,mark options={fill=white}] table {re2.data};
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    95
\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
    96
\end{axis}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    97
\end{tikzpicture}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    98
\end{tabular}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
    99
\end{center}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   100
433
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   101
\small
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   102
In the handouts is a similar graph with \bl{$(a^*)^* \cdot b$} for Java.
263
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
\end{frame}
433
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   105
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   106
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   107
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   108
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   109
\begin{frame}[c]
335
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   110
\frametitle{Languages}
16
Christian Urban <urbanc@in.tum.de>
parents: 15
diff changeset
   111
261
24531cfaa36a updated handouts
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 258
diff changeset
   112
\begin{itemize}
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   113
433
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   114
\item A \alert{\bf Language} is a set of strings, for example\medskip
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   115
\begin{center}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   116
\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
   117
\end{center}\bigskip
16
Christian Urban <urbanc@in.tum.de>
parents: 15
diff changeset
   118
332
4755ad4b457b updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 325
diff changeset
   119
\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
   120
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   121
\begin{center}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   122
\begin{tabular}{rcl}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   123
\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
   124
\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
   125
\end{tabular}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   126
\end{center}
335
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   127
\bigskip
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   128
335
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   129
\small
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   130
\item [] For example \bl{$A = \{foo, bar\}$}, \bl{$B = \{a, b\}$}
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   131
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   132
\[
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   133
\bl{A \,@\, B = \{fooa, foob, bara, barb\}}
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   134
\]
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   135
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   136
\end{itemize}  
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   137
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   138
\end{frame}
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   139
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   140
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   141
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   142
\begin{frame}[c]
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   143
\frametitle{The Power Operation}
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   144
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   145
\begin{itemize}
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   146
\item The \alert{\bf Power} of a language:
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   147
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   148
\begin{center}
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   149
\begin{tabular}{lcl}
431
c7d4ee344451 updated
Christian Urban <urbanc@in.tum.de>
parents: 429
diff changeset
   150
\bl{$A^0$}    & \bl{$\dn$} & \bl{$\{[]\}$}\\
335
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   151
\bl{$A^{n+1}$} & \bl{$\dn$} & \bl{$A \,@\, A^n$}
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   152
\end{tabular}
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   153
\end{center}\bigskip
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   154
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   155
\item[] For example
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   156
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   157
\begin{center}
431
c7d4ee344451 updated
Christian Urban <urbanc@in.tum.de>
parents: 429
diff changeset
   158
\begin{tabular}{lcl}
c7d4ee344451 updated
Christian Urban <urbanc@in.tum.de>
parents: 429
diff changeset
   159
\bl{$A^4$} & \bl{$=$} & \bl{$A \,@\, A \,@\, A \,@\, A$}\\
c7d4ee344451 updated
Christian Urban <urbanc@in.tum.de>
parents: 429
diff changeset
   160
\bl{$A^1$} & \bl{$=$} & \bl{$A$}\\
c7d4ee344451 updated
Christian Urban <urbanc@in.tum.de>
parents: 429
diff changeset
   161
\bl{$A^0$} & \bl{$=$} & \bl{$\{[]\}$}\\
335
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   162
\end{tabular}
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   163
\end{center}
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   164
261
24531cfaa36a updated handouts
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 258
diff changeset
   165
\end{itemize}  
24531cfaa36a updated handouts
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 258
diff changeset
   166
24531cfaa36a updated handouts
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 258
diff changeset
   167
\end{frame}
16
Christian Urban <urbanc@in.tum.de>
parents: 15
diff changeset
   168
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
Christian Urban <urbanc@in.tum.de>
parents: 15
diff changeset
   169
335
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   170
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   171
\begin{frame}[c]
336
7c80b9b6f713 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 335
diff changeset
   172
\frametitle{Homework Question}
7c80b9b6f713 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 335
diff changeset
   173
7c80b9b6f713 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 335
diff changeset
   174
\begin{itemize}
7c80b9b6f713 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 335
diff changeset
   175
\item Say \bl{$A = \{[a],[b],[c],[d]\}$}.\bigskip
7c80b9b6f713 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 335
diff changeset
   176
7c80b9b6f713 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 335
diff changeset
   177
\begin{center}
7c80b9b6f713 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 335
diff changeset
   178
How many strings are in \bl{$A^4$}?
7c80b9b6f713 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 335
diff changeset
   179
\end{center}\bigskip\medskip\pause
7c80b9b6f713 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 335
diff changeset
   180
7c80b9b6f713 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 335
diff changeset
   181
7c80b9b6f713 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 335
diff changeset
   182
\begin{center}
7c80b9b6f713 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 335
diff changeset
   183
\begin{tabular}{l}
7c80b9b6f713 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 335
diff changeset
   184
What if \bl{$A = \{[a],[b],[c],[]\}$};\\ 
7c80b9b6f713 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 335
diff changeset
   185
how many strings are then in \bl{$A^4$}?
7c80b9b6f713 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 335
diff changeset
   186
\end{tabular}
7c80b9b6f713 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 335
diff changeset
   187
\end{center}
7c80b9b6f713 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 335
diff changeset
   188
\end{itemize}  
7c80b9b6f713 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 335
diff changeset
   189
7c80b9b6f713 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 335
diff changeset
   190
\end{frame}
7c80b9b6f713 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 335
diff changeset
   191
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
7c80b9b6f713 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 335
diff changeset
   192
7c80b9b6f713 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 335
diff changeset
   193
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
7c80b9b6f713 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 335
diff changeset
   194
\begin{frame}[c]
335
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   195
\frametitle{The Star Operation}
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   196
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   197
\begin{itemize}
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   198
\item The \alert{\bf Star} of a \underline{language}:
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   199
\bigskip
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   200
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   201
\begin{center}
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   202
\begin{tabular}{c}
431
c7d4ee344451 updated
Christian Urban <urbanc@in.tum.de>
parents: 429
diff changeset
   203
\bl{$A\star \dn \bigcup_{0\le n} A^n$}
335
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   204
\end{tabular}
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   205
\end{center}\bigskip
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   206
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   207
\item[] This expands to 
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   208
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   209
\[
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   210
\bl{A^0 \cup A^1 \cup A^2 \cup A^3 \cup A^4 \cup \ldots}
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   211
\]
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   212
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   213
\small
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   214
\[
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   215
\bl{\{[]\} \;\cup\; A \;\cup\; A\,@\,A \;\cup\; 
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   216
  A\,@\,A\,@\,A \;\cup\; A\,@\,A\,@\,A\,@\,A \cup \ldots}
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   217
\]
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   218
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   219
\end{itemize}  
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   220
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   221
\end{frame}
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   222
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   223
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   224
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   225
\begin{frame}[c]
507
fdbc7d0ec04f updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   226
\frametitle{\begin{tabular}{c}The Meaning of a\\[-2mm] 
fdbc7d0ec04f updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   227
  Regular Expression\end{tabular}}
fdbc7d0ec04f updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   228
fdbc7d0ec04f updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   229
\begin{textblock}{15}(1,4)
fdbc7d0ec04f updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   230
 \begin{tabular}{rcl}
fdbc7d0ec04f updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   231
 \bl{$L(\ZERO)$}  & \bl{$\dn$} & \bl{$\{\}$}\\
fdbc7d0ec04f updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   232
 \bl{$L(\ONE)$}     & \bl{$\dn$} & \bl{$\{[]\}$}\\
fdbc7d0ec04f updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   233
 \bl{$L(c)$}            & \bl{$\dn$} & \bl{$\{[c]\}$}\\
fdbc7d0ec04f updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   234
 \bl{$L(r_1 + r_2)$}    & \bl{$\dn$} & \bl{$L(r_1) \cup L(r_2)$}\\
fdbc7d0ec04f updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   235
 \bl{$L(r_1 \cdot r_2)$} & \bl{$\dn$} & \bl{$\{ s_1 \,@\, s_2 \;|\; s_1 \in L(r_1) \wedge s_2 \in L(r_2) \}$}\\
fdbc7d0ec04f updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   236
 \bl{$L(r^*)$}           & \bl{$\dn$} & \bl{$(L(r))\star \quad\dn \bigcup_{0 \le n} L(r)^n$}\\
fdbc7d0ec04f updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   237
  \end{tabular}
fdbc7d0ec04f updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   238
\end{textblock}
fdbc7d0ec04f updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   239
fdbc7d0ec04f updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   240
\begin{textblock}{6}(9,12)\small
fdbc7d0ec04f updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   241
\bl{$L$} is a function from regular expressions to 
fdbc7d0ec04f updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   242
sets of strings\\
fdbc7d0ec04f updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   243
\bl{$L$ : Rexp $\Rightarrow$ Set$[$String$]$}
fdbc7d0ec04f updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   244
\end{textblock}
fdbc7d0ec04f updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   245
fdbc7d0ec04f updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   246
\end{frame}
fdbc7d0ec04f updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   247
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
fdbc7d0ec04f updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   248
fdbc7d0ec04f updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   249
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
fdbc7d0ec04f updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   250
\begin{frame}[c]
fdbc7d0ec04f updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   251
\frametitle{\begin{tabular}{c}The Specification\\ of Matching\end{tabular}}
fdbc7d0ec04f updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   252
fdbc7d0ec04f updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   253
\begin{bubble}[10cm]
fdbc7d0ec04f updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   254
\large
fdbc7d0ec04f updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   255
A regular expression \bl{$r$} matches a string~\bl{$s$} 
fdbc7d0ec04f updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   256
provided
fdbc7d0ec04f updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   257
fdbc7d0ec04f updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   258
\begin{center}
fdbc7d0ec04f updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   259
\bl{$s \in L(r)$}\\ 
fdbc7d0ec04f updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   260
\end{center}
fdbc7d0ec04f updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   261
\end{bubble}\bigskip\bigskip
fdbc7d0ec04f updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   262
fdbc7d0ec04f updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   263
\ldots and the point of the this lecture is 
fdbc7d0ec04f updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   264
to decide this problem as fast as possible 
fdbc7d0ec04f updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   265
(unlike Python, Ruby, Java etc)
fdbc7d0ec04f updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   266
fdbc7d0ec04f updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   267
\end{frame}
fdbc7d0ec04f updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   268
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
fdbc7d0ec04f updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   269
fdbc7d0ec04f updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   270
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
fdbc7d0ec04f updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
   271
\begin{frame}[c]
335
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   272
\frametitle{Semantic Derivative}
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   273
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   274
\begin{itemize}
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   275
\item The \alert{\bf Semantic Derivative} of a 
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   276
\underline{language}\\ wrt to a character \bl{$c$}:
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   277
\bigskip
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   278
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   279
\begin{center}
433
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   280
\bl{$\Der\,c\,A \dn \{ s \;|\;  c\!::\!s \in A\}$ } 
345
0922b3e01289 updated slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 342
diff changeset
   281
\end{center}\bigskip\bigskip\bigskip
335
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   282
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   283
For \bl{$A = \{\textit{foo}, \textit{bar}, \textit{frak}\}$} then
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   284
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   285
\begin{center}
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   286
\bl{\begin{tabular}{l@{\hspace{2mm}}c@{\hspace{2mm}}l}
433
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   287
$\Der\,f\,A$ & $=$ & $\{\textit{oo}, \textit{rak}\}$\\
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   288
$\Der\,b\,A$ & $=$ &  $\{\textit{ar}\}$\\  
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   289
$\Der\,a\,A$ & $=$ & $\{\}$\\\pause
335
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   290
\end{tabular}}
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   291
\end{center}
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   292
338
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
   293
\small
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
   294
We can extend this definition to strings
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
   295
\[
433
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   296
\bl{\Ders\,s\,A = \{s'\;|\;s\,@\,s' \in A\}}
338
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
   297
\]
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
   298
335
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   299
\end{itemize}
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   300
 
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   301
\end{frame}
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   302
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
117
25999de692b2 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   303
25999de692b2 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   304
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
25999de692b2 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   305
\begin{frame}[t]
335
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   306
\frametitle{Regular Expressions}
7
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   307
15
Christian Urban <urbanc@in.tum.de>
parents: 11
diff changeset
   308
Their inductive definition:
Christian Urban <urbanc@in.tum.de>
parents: 11
diff changeset
   309
Christian Urban <urbanc@in.tum.de>
parents: 11
diff changeset
   310
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   311
\begin{textblock}{6}(2,7.5)
7
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   312
  \begin{tabular}{@ {}rrl@ {\hspace{13mm}}l}
429
7e71c947ec69 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   313
  \bl{$r$} & \bl{$::=$}  & \bl{$\ZERO$}  & null\\
7e71c947ec69 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   314
         & \bl{$\mid$} & \bl{$\ONE$}       & empty string / \pcode{""} / $[]$\\
335
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   315
         & \bl{$\mid$} & \bl{$c$}              & character\\
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   316
         & \bl{$\mid$} & \bl{$r_1 \cdot r_2$}  & sequence\\
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   317
         & \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
   318
         & \bl{$\mid$} & \bl{$r^*$}            & star (zero or more)\\
7
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   319
  \end{tabular}
336
7c80b9b6f713 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 335
diff changeset
   320
\end{textblock}
7
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   321
  
337
885ac2b6c27d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 336
diff changeset
   322
\only<2->{\footnotesize
885ac2b6c27d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 336
diff changeset
   323
\begin{textblock}{9}(2,0.5)
885ac2b6c27d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 336
diff changeset
   324
\begin{bubble}[9.8cm]
885ac2b6c27d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 336
diff changeset
   325
\lstinputlisting{../progs/app01.scala}
885ac2b6c27d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 336
diff changeset
   326
\end{bubble}
885ac2b6c27d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 336
diff changeset
   327
\end{textblock}}  
885ac2b6c27d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 336
diff changeset
   328
  
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   329
\end{frame}
16
Christian Urban <urbanc@in.tum.de>
parents: 15
diff changeset
   330
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
Christian Urban <urbanc@in.tum.de>
parents: 15
diff changeset
   331
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   332
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
332
4755ad4b457b updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 325
diff changeset
   333
\begin{frame}[c]
4755ad4b457b updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 325
diff changeset
   334
\frametitle{\begin{tabular}{c}
335
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   335
 When Are Two Regular\\[-1mm]
332
4755ad4b457b updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 325
diff changeset
   336
 Expressions Equivalent?\end{tabular}}
4755ad4b457b updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 325
diff changeset
   337
\large
4755ad4b457b updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 325
diff changeset
   338
\begin{center}
4755ad4b457b updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 325
diff changeset
   339
\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
   340
\end{center}  
4755ad4b457b updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 325
diff changeset
   341
  
4755ad4b457b updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 325
diff changeset
   342
\end{frame}
4755ad4b457b updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 325
diff changeset
   343
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
4755ad4b457b updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 325
diff changeset
   344
4755ad4b457b updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 325
diff changeset
   345
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   346
\begin{frame}[t]
336
7c80b9b6f713 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 335
diff changeset
   347
\frametitle{Concrete Equivalences}
16
Christian Urban <urbanc@in.tum.de>
parents: 15
diff changeset
   348
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   349
\begin{center}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   350
\bl{\begin{tabular}{rcl}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   351
$(a + b)  + c$ & $\equiv$ & $a + (b + c)$\\
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   352
$a + a$        & $\equiv$ & $a$\\
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   353
$a + b$        & $\equiv$ & $b + a$\\
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   354
$(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
   355
$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
   356
$a \cdot a$       & $\not\equiv$ & $a$\\
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   357
$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
   358
\end{tabular}}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   359
\end{center}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   360
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   361
\end{frame}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   362
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   363
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   364
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   365
\begin{frame}[t]
336
7c80b9b6f713 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 335
diff changeset
   366
\frametitle{Corner Cases}
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   367
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   368
\begin{center}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   369
\bl{\begin{tabular}{rcl}
429
7e71c947ec69 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   370
$a \cdot \ZERO$ & $\not\equiv$ & $a$\\
7e71c947ec69 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   371
$a + \ONE$ & $\not\equiv$ & $a$\\
7e71c947ec69 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   372
$\ONE$ & $\equiv$ & $\ZERO^*$\\
7e71c947ec69 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   373
$\ONE^*$ & $\equiv$ & $\ONE$\\
7e71c947ec69 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   374
$\ZERO^*$ & $\not\equiv$ & $\ZERO$\\
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   375
\end{tabular}}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   376
\end{center}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   377
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   378
\end{frame}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   379
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   380
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   381
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   382
\begin{frame}[t]
336
7c80b9b6f713 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 335
diff changeset
   383
\frametitle{Simplification Rules}
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   384
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   385
\begin{center}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   386
\bl{\begin{tabular}{rcl}
429
7e71c947ec69 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   387
$r + \ZERO$  & $\equiv$ & $r$\\
7e71c947ec69 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   388
$\ZERO + r$  & $\equiv$ & $r$\\
7e71c947ec69 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   389
$r \cdot \ONE$ & $\equiv$ & $r$\\
7e71c947ec69 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   390
$\ONE \cdot r$     & $\equiv$ & $r$\\
7e71c947ec69 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   391
$r \cdot \ZERO$ & $\equiv$ & $\ZERO$\\
7e71c947ec69 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   392
$\ZERO \cdot r$ & $\equiv$ & $\ZERO$\\
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   393
$r + r$ & $\equiv$ & $r$
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   394
\end{tabular}}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   395
\end{center}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   396
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   397
\end{frame}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   398
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
16
Christian Urban <urbanc@in.tum.de>
parents: 15
diff changeset
   399
335
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   400
%\newcommand{\YES}{\textcolor{gray}{yes}}
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   401
%\newcommand{\NO}{\textcolor{gray}{no}}
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   402
%\newcommand{\FORALLR}{\textcolor{gray}{$\forall$ r.}}
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   403
7
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   404
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   405
\begin{frame}[c]
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   406
\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
   407
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   408
\large
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   409
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
   410
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   411
\begin{center}
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   412
\bl{$s \in L(r)$}\\ 
7
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   413
\end{center}
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   414
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   415
\end{frame}
7
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   416
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   417
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   418
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   419
\begin{frame}[c]
433
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   420
\frametitle{\bl{$(a^{?\{n\}}) \cdot a^{\{n\}}$} and \bl{$(a^*)^* \cdot b$}}
117
25999de692b2 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   421
433
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   422
\begin{center}\footnotesize
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   423
\begin{tabular}{@{}c@{\hspace{-2mm}}c@{}}
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   424
\begin{tikzpicture}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   425
\begin{axis}[
433
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   426
    xlabel={$n$},
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   427
    x label style={at={(1.05,0.0)}},
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   428
    ylabel={time in secs},
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   429
    enlargelimits=false,
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   430
    xtick={0,5,...,30},
433
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   431
    xmax=33,
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   432
    ymax=35,
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   433
    ytick={0,5,...,30},
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   434
    scaled ticks=false,
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   435
    axis lines=left,
433
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   436
    width=5.5cm,
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   437
    height=4.5cm, 
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   438
    legend entries={Python,Ruby},  
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   439
    legend pos=north west,
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   440
    legend cell align=left  
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
\addplot[blue,mark=*, mark options={fill=white}] 
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   443
  table {re-python.data};
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   444
\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
   445
  table {re-ruby.data};  
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   446
\end{axis}
117
25999de692b2 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   447
\end{tikzpicture}
433
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   448
&
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   449
\begin{tikzpicture}
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   450
\begin{axis}[
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   451
    xlabel={$n$},
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   452
    x label style={at={(1.05,0.0)}},
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   453
    ylabel={time in secs},
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   454
    enlargelimits=false,
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   455
    xtick={0,5,...,30},
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   456
    xmax=33,
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   457
    ymax=35,
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   458
    ytick={0,5,...,30},
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   459
    scaled ticks=false,
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   460
    axis lines=left,
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   461
    width=5.5cm,
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   462
    height=4.5cm, 
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   463
    legend entries={Java},  
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   464
    legend pos=north west,
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   465
    legend cell align=left]
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   466
\addplot[cyan,mark=*, mark options={fill=white}] table {re-java.data};
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   467
\end{axis}
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   468
\end{tikzpicture}
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   469
\end{tabular}
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   470
\end{center}
11
5353d405e4e6 added slides 2
Christian Urban <urbanc@in.tum.de>
parents: 7
diff changeset
   471
335
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   472
\end{frame}
11
5353d405e4e6 added slides 2
Christian Urban <urbanc@in.tum.de>
parents: 7
diff changeset
   473
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
5353d405e4e6 added slides 2
Christian Urban <urbanc@in.tum.de>
parents: 7
diff changeset
   474
5353d405e4e6 added slides 2
Christian Urban <urbanc@in.tum.de>
parents: 7
diff changeset
   475
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
118
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 117
diff changeset
   476
\begin{frame}[c]
335
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   477
\frametitle{Evil Regular Expressions}
118
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 117
diff changeset
   478
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 117
diff changeset
   479
\begin{itemize}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 117
diff changeset
   480
\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
   481
\item Evil regular expressions\medskip
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 117
diff changeset
   482
\begin{itemize}
431
c7d4ee344451 updated
Christian Urban <urbanc@in.tum.de>
parents: 429
diff changeset
   483
\item \bl{$(a^{?\{n\}}) \cdot a^{\{n\}}$}
433
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   484
\item \bl{$(a^*)^*$}
118
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 117
diff changeset
   485
\item \bl{$([a$\,-\,$z]^+)^*$}
433
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   486
\item \bl{$(a + a \cdot a)^*$}
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   487
\item \bl{$(a + a?)^*$}
118
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 117
diff changeset
   488
\end{itemize}
435
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   489
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   490
\item sometimes also called \alert{catastrophic backtracking}
118
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 117
diff changeset
   491
\end{itemize}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 117
diff changeset
   492
335
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   493
\end{frame}
118
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 117
diff changeset
   494
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 117
diff changeset
   495
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 117
diff changeset
   496
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
11
5353d405e4e6 added slides 2
Christian Urban <urbanc@in.tum.de>
parents: 7
diff changeset
   497
\begin{frame}[t]
335
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   498
\frametitle{A Matching Algorithm}
11
5353d405e4e6 added slides 2
Christian Urban <urbanc@in.tum.de>
parents: 7
diff changeset
   499
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   500
117
25999de692b2 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   501
\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
   502
\begin{center}
117
25999de692b2 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   503
\begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {}}
429
7e71c947ec69 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   504
\bl{$nullable(\ZERO)$}    & \bl{$\dn$} & \bl{\textit{false}}\\
7e71c947ec69 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   505
\bl{$nullable(\ONE)$}       & \bl{$\dn$} & \bl{\textit{true}}\\
335
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   506
\bl{$nullable (c)$}             & \bl{$\dn$} & \bl{\textit{false}}\\
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   507
\bl{$nullable (r_1 + r_2)$}     & \bl{$\dn$} & \bl{$nullable(r_1) \vee nullable(r_2)$} \\ 
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   508
\bl{$nullable (r_1 \cdot r_2)$} & \bl{$\dn$} & \bl{$nullable(r_1) \wedge nullable(r_2)$} \\
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   509
\bl{$nullable (r^*)$}           & \bl{$\dn$} & \bl{\textit{true}}\\
117
25999de692b2 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 93
diff changeset
   510
\end{tabular}
16
Christian Urban <urbanc@in.tum.de>
parents: 15
diff changeset
   511
\end{center}
Christian Urban <urbanc@in.tum.de>
parents: 15
diff changeset
   512
335
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   513
\end{frame}
11
5353d405e4e6 added slides 2
Christian Urban <urbanc@in.tum.de>
parents: 7
diff changeset
   514
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
5353d405e4e6 added slides 2
Christian Urban <urbanc@in.tum.de>
parents: 7
diff changeset
   515
5353d405e4e6 added slides 2
Christian Urban <urbanc@in.tum.de>
parents: 7
diff changeset
   516
5353d405e4e6 added slides 2
Christian Urban <urbanc@in.tum.de>
parents: 7
diff changeset
   517
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
5353d405e4e6 added slides 2
Christian Urban <urbanc@in.tum.de>
parents: 7
diff changeset
   518
\begin{frame}[c]
335
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   519
\frametitle{The Derivative of a Rexp}
7
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   520
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   521
\large
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   522
If \bl{$r$} matches the string \bl{$c\!::\!s$}, what is a regular 
335
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   523
expression that matches just \bl{$s$}?\bigskip\bigskip\bigskip\bigskip
7
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   524
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   525
\small
433
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   526
\bl{$\der\,c\,r$} gives the answer, Brzozowski 1964
335
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   527
\end{frame}
7
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   528
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   529
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   530
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   531
\begin{frame}[c]
335
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   532
\frametitle{The Derivative of a Rexp}
7
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   533
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   534
\begin{center}
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   535
\begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{-10mm}}l@ {}}
433
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   536
  \bl{$\der\, c\, (\ZERO)$}      & \bl{$\dn$} & \bl{$\ZERO$} & \\
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   537
  \bl{$\der\, c\, (\ONE)$}           & \bl{$\dn$} & \bl{$\ZERO$} & \\
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   538
  \bl{$\der\, c\, (d)$}                     & \bl{$\dn$} & \bl{if $c = d$ then $\ONE$ else $\ZERO$} & \\
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   539
  \bl{$\der\, c\, (r_1 + r_2)$}        & \bl{$\dn$} & \bl{$\der\, c\, r_1 + \der\, c\, r_2$} & \\
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   540
  \bl{$\der\, c\, (r_1 \cdot r_2)$}  & \bl{$\dn$}  & \bl{if $nullable (r_1)$}\\
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   541
  & & \bl{then $(\der\,c\,r_1) \cdot r_2 + \der\, c\, r_2$}\\ 
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   542
  & & \bl{else $(\der\, c\, r_1) \cdot r_2$}\\
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   543
  \bl{$\der\, c\, (r^*)$}          & \bl{$\dn$} & \bl{$(\der\,c\,r) \cdot (r^*)$} &\bigskip\\\pause
7
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   544
433
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   545
  \bl{$\ders\, []\, r$}     & \bl{$\dn$} & \bl{$r$} & \\
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   546
  \bl{$\ders\, (c\!::\!s)\, r$} & \bl{$\dn$} & \bl{$\ders\,s\,(\der\,c\,r)$} & \\
7
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   547
  \end{tabular}
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   548
\end{center}
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   549
337
885ac2b6c27d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 336
diff changeset
   550
\end{frame}
7
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   551
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   552
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   553
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   554
\begin{frame}[c]
335
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   555
\frametitle{Examples}
7
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   556
119
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   557
Given \bl{$r \dn ((a \cdot b) + b)^*$} what is
7
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   558
119
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   559
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   560
\begin{tabular}{l}
433
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   561
\bl{$\der\,a\,r =\;?$}\\
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   562
\bl{$\der\,b\,r =\;?$}\\
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   563
\bl{$\der\,c\,r =\;?$}
119
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   564
\end{tabular}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   565
\end{center}
7
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   566
335
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   567
\end{frame}
7
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   568
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   569
17
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   570
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
431
c7d4ee344451 updated
Christian Urban <urbanc@in.tum.de>
parents: 429
diff changeset
   571
\begin{frame}[c]
c7d4ee344451 updated
Christian Urban <urbanc@in.tum.de>
parents: 429
diff changeset
   572
\frametitle{The Algorithm}
c7d4ee344451 updated
Christian Urban <urbanc@in.tum.de>
parents: 429
diff changeset
   573
c7d4ee344451 updated
Christian Urban <urbanc@in.tum.de>
parents: 429
diff changeset
   574
\begin{center}
433
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   575
\begin{tabular}{l} 
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   576
\bl{$\textit{matches}\,r\,s \dn \textit{nullable}(\ders\,r\,s)$}  
431
c7d4ee344451 updated
Christian Urban <urbanc@in.tum.de>
parents: 429
diff changeset
   577
\end{tabular}
c7d4ee344451 updated
Christian Urban <urbanc@in.tum.de>
parents: 429
diff changeset
   578
\end{center}
c7d4ee344451 updated
Christian Urban <urbanc@in.tum.de>
parents: 429
diff changeset
   579
c7d4ee344451 updated
Christian Urban <urbanc@in.tum.de>
parents: 429
diff changeset
   580
c7d4ee344451 updated
Christian Urban <urbanc@in.tum.de>
parents: 429
diff changeset
   581
\end{frame}
c7d4ee344451 updated
Christian Urban <urbanc@in.tum.de>
parents: 429
diff changeset
   582
%%%%%%%%%%%%%%%%%
c7d4ee344451 updated
Christian Urban <urbanc@in.tum.de>
parents: 429
diff changeset
   583
c7d4ee344451 updated
Christian Urban <urbanc@in.tum.de>
parents: 429
diff changeset
   584
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
17
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   585
\begin{frame}[t]
433
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   586
\frametitle{An Example}
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   587
433
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   588
Does \bl{$r_1$} match \bl{$abc$}?
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   589
\begin{center}
433
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   590
\begin{tabular}{@{}rl@{}l@{}}
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   591
Step 1: & build derivative of \bl{$a$} and \bl{$r_1$} & \bl{$(r_2 = \der\,a\,r_1)$}\smallskip\\
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   592
Step 2: & build derivative of \bl{$b$} and \bl{$r_2$} & \bl{$(r_3 = \der\,b\,r_2)$}\smallskip\\
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   593
Step 3: & build derivative of \bl{$c$} and \bl{$r_3$} & \bl{$(r_4 = \der\,c\,r_3)$}\smallskip\\
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   594
Step 4: & the string is exhausted: & \bl{($nullable(r_4))$}\\
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   595
        & test whether \bl{$r_4$} can recognise\\
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   596
        & the empty string\smallskip\\
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   597
Output: & result of the test\\
335
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   598
        & $\Rightarrow \bl{\textit{true}} \,\text{or}\, 
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   599
                       \bl{\textit{false}}$\\        
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   600
\end{tabular}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   601
\end{center}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   602
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   603
337
885ac2b6c27d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 336
diff changeset
   604
\end{frame}
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   605
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   606
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   607
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
335
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   608
\begin{frame}[c]
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   609
\frametitle{The Idea of the Algorithm}
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   610
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   611
If we want to recognise the string \bl{$abc$} with regular 
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   612
expression \bl{$r_1$} then\medskip
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   613
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   614
\begin{enumerate}
433
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   615
\item \bl{$\Der\,a\,(L(r_1))$}\pause
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   616
\item \bl{$\Der\,b\,(\Der\,a\,(L(r_1)))$}\pause
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   617
\item \bl{$\Der\,c\,(\Der\,b\,(\Der\,a\,(L(r_1))))$}\bigskip
342
c235e0aeb8df updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 338
diff changeset
   618
\item finally we test whether the empty string is in this 
433
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   619
set; same for  \bl{$\Ders\,abc\,(L(r_1))$}.\medskip
335
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   620
\end{enumerate}
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   621
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   622
The matching algorithm works similarly, just over regular expressions instead of sets.
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   623
\end{frame}
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   624
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   625
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   626
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   627
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   628
\begin{frame}[c]
433
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   629
\frametitle{Oops\ldots\bl{$(a^{?\{n\}}) \cdot a^{\{n\}}$}}
119
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   630
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   631
\begin{center}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   632
\begin{tikzpicture}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   633
\begin{axis}[
433
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   634
    xlabel={$n$},
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   635
    x label style={at={(1.05,0.0)}},
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   636
    ylabel={time in secs},
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   637
    enlargelimits=false,
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   638
    xtick={0,5,...,30},
433
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   639
    xmax=31,
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   640
    ytick={0,5,...,30},
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   641
    scaled ticks=false,
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   642
    axis lines=left,
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   643
    width=7cm,
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   644
    height=7cm, 
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   645
    legend entries={Python,Ruby,Scala V1},  
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   646
    legend pos=outer north east,
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   647
    legend cell align=left  
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   648
]
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   649
\addplot[blue,mark=*, mark options={fill=white}] 
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   650
  table {re-python.data};
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   651
\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
   652
  table {re-ruby.data};  
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   653
\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
   654
  table {re1.data};  
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   655
\end{axis}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   656
\end{tikzpicture}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   657
\end{center}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   658
335
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   659
\end{frame}
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   660
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   661
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   662
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   663
\begin{frame}[c]
335
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   664
\frametitle{A Problem}
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   665
345
0922b3e01289 updated slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 342
diff changeset
   666
We represented the ``n-times'' \bl{$a^{\{n\}}$} as a 
335
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   667
sequence regular expression:
119
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   668
263
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
\begin{tabular}{rl}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   671
1: & \bl{$a$}\\
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   672
2: & \bl{$a\cdot a$}\\
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   673
3: & \bl{$a\cdot a\cdot a$}\\
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   674
& \ldots\\
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   675
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
   676
& \ldots\\
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   677
20:
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   678
\end{tabular}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   679
\end{center}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   680
345
0922b3e01289 updated slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 342
diff changeset
   681
This problem is aggravated with \bl{$a^?$} being represented 
433
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   682
as \bl{$a + \ONE$}.
335
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   683
\end{frame}
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   684
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   685
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
\begin{frame}[c]
335
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   688
\frametitle{Solving the Problem}
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   689
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   690
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
   691
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   692
\begin{center}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   693
\begin{tabular}{rcl}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   694
\bl{$r$} & \bl{$::=$} & \bl{\ldots}\\
342
c235e0aeb8df updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 338
diff changeset
   695
             & \bl{$\mid$} & \bl{$r^{\{n\}}$}\\
345
0922b3e01289 updated slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 342
diff changeset
   696
             & \bl{$\mid$} & \bl{$r^?$} 
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   697
\end{tabular}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   698
\end{center}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   699
433
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   700
What is their meaning?\\
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   701
What are the cases for \bl{$nullable$} and \bl{$\der$}?
335
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   702
\end{frame}
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   703
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   704
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   705
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   706
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   707
\begin{frame}[t]
431
c7d4ee344451 updated
Christian Urban <urbanc@in.tum.de>
parents: 429
diff changeset
   708
\frametitle{\bl{$(a^{?\{n\}}) \cdot a^{\{n\}}$}}
119
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   709
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   710
\begin{center}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   711
\begin{tikzpicture}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   712
\begin{axis}[
433
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   713
    xlabel={$n$},
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   714
    x label style={at={(1.05,0.0)}},   
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   715
    ylabel={time in secs},
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   716
    enlargelimits=false,
434
8664ff87cd77 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 433
diff changeset
   717
    xtick={0,200,...,1100},
8664ff87cd77 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 433
diff changeset
   718
    xmax=1200,
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   719
    ytick={0,5,...,30},
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   720
    scaled ticks=false,
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   721
    axis lines=left,
435
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   722
    width=8cm,
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   723
    height=6.5cm, 
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   724
    legend entries={Python,Ruby,Scala V1,Scala V2},  
435
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   725
    legend pos=outer north east,
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   726
    legend cell align=left  
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   727
]
434
8664ff87cd77 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 433
diff changeset
   728
\addplot[blue,mark=*, mark options={fill=white}] table {re-python.data};
8664ff87cd77 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 433
diff changeset
   729
\addplot[brown,mark=pentagon*, mark options={fill=white}] table {re-ruby.data};  
8664ff87cd77 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 433
diff changeset
   730
\addplot[red,mark=triangle*,mark options={fill=white}] table {re1.data};  
8664ff87cd77 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 433
diff changeset
   731
\addplot[green,mark=square*,mark options={fill=white}] table {re2.data};
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   732
\end{axis}
119
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   733
\end{tikzpicture}
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   734
\end{center}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   735
335
2d112a7b29eb updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   736
\end{frame}
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   737
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   738
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   739
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   740
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   741
\begin{frame}[c]
337
885ac2b6c27d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 336
diff changeset
   742
\frametitle{Examples}
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   743
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   744
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
   745
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   746
\begin{center}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   747
\begin{tabular}{l}
433
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   748
\bl{$\der\,a\,r = ((\ONE \cdot b) + \ZERO) \cdot r$}\\
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   749
\bl{$\der\,b\,r = ((\ZERO \cdot b) + \ONE)\cdot r$}\\
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   750
\bl{$\der\,c\,r = ((\ZERO \cdot b) + \ZERO)\cdot r$}
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   751
\end{tabular}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   752
\end{center}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   753
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   754
What are these regular expressions equivalent to?
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   755
337
885ac2b6c27d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 336
diff changeset
   756
\end{frame}
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   757
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   758
435
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   759
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   760
\begin{frame}[c]
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   761
\frametitle{Simplifiaction}
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   762
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   763
\begin{center}
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   764
\bl{\begin{tabular}{rcl}
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   765
$r + \ZERO$       & $\Rightarrow$ & $r$\\
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   766
$\ZERO + r$       & $\Rightarrow$ & $r$\\
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   767
$r \cdot \ONE$    & $\Rightarrow$ & $r$\\
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   768
$\ONE \cdot r$    & $\Rightarrow$ & $r$\\
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   769
$r \cdot \ZERO$   & $\Rightarrow$ & $\ZERO$\\
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   770
$\ZERO \cdot r$   & $\Rightarrow$ & $\ZERO$\\
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   771
$r + r$           & $\Rightarrow$ & $r$
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   772
\end{tabular}}
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   773
\end{center}
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   774
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   775
\footnotesize
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   776
\lstinputlisting{../progs/app60.scala}
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   777
\end{frame}
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   778
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   779
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   780
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   781
\begin{frame}[c]
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   782
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   783
\footnotesize
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   784
\lstinputlisting{../progs/app6.scala}
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   785
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   786
\end{frame}
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   787
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   788
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   789
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   790
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   791
\begin{frame}[t]
431
c7d4ee344451 updated
Christian Urban <urbanc@in.tum.de>
parents: 429
diff changeset
   792
\frametitle{\bl{$(a^{?\{n\}}) \cdot a^{\{n\}}$}}
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   793
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   794
\begin{center}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   795
\begin{tikzpicture}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   796
\begin{axis}[
433
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   797
    xlabel={$n$},
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   798
    x label style={at={(1.05,0.0)}},     
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   799
    ylabel={time in secs},
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   800
    enlargelimits=false,
442
84d6714840c9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 436
diff changeset
   801
    xtick={0,5000,...,10000},
84d6714840c9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 436
diff changeset
   802
    xmax=11000,
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   803
    ymax=35,
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   804
    ytick={0,5,...,30},
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   805
    scaled ticks=false,
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   806
    axis lines=left,
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   807
    width=9cm,
433
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   808
    height=7cm,
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   809
    legend entries={Scala V2,Scala V3},  
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   810
    legend pos=north east
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   811
]
434
8664ff87cd77 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 433
diff changeset
   812
\addplot[green,mark=square*,mark options={fill=white}] table {re2.data};
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   813
\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
   814
\end{axis}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   815
\end{tikzpicture}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   816
\end{center}
119
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   817
337
885ac2b6c27d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 336
diff changeset
   818
\end{frame}
119
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   819
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   820
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   821
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
433
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   822
\begin{frame}[c]
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   823
\frametitle{\bl{$(a^*)^* \cdot b$}}
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   824
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   825
\begin{center}
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   826
\begin{tikzpicture}
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   827
  \begin{axis}[
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   828
    xlabel={$n$},
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   829
    x label style={at={(1.09,0.0)}},
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   830
    ylabel={time in secs},
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   831
    enlargelimits=false,
442
84d6714840c9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 436
diff changeset
   832
    xmax=27,
84d6714840c9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 436
diff changeset
   833
    xtick={0,5,...,20},
84d6714840c9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 436
diff changeset
   834
    ytick={0,5,...,25},
84d6714840c9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 436
diff changeset
   835
    ymax=13,
433
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   836
    scaled ticks=false,
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   837
    axis lines=left,
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   838
    width=9cm,
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   839
    height=5cm, 
434
8664ff87cd77 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 433
diff changeset
   840
    legend entries={Scala V2},
433
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   841
    legend pos=north west,
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   842
    legend cell align=left]
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   843
\addplot[green,mark=square*,mark options={fill=white}] table {re2a.data};
434
8664ff87cd77 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 433
diff changeset
   844
%% still needs to be done
8664ff87cd77 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 433
diff changeset
   845
%%\addplot[black,mark=square*,mark options={fill=white}] table {re3a.data};
433
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   846
\end{axis}
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   847
\end{tikzpicture}
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   848
\end{center}
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   849
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   850
\end{frame}
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   851
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   852
435
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   853
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   854
\begin{frame}[c]
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   855
\frametitle{\bl{$(a^*)^* \cdot b$}}
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   856
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   857
\begin{center}
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   858
\begin{tikzpicture}
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   859
  \begin{axis}[
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   860
    xlabel={$n$},
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   861
    x label style={at={(1.09,0.0)}},
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   862
    ylabel={time in secs},
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   863
    enlargelimits=false,
442
84d6714840c9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 436
diff changeset
   864
    ytick={0,10,...,60},
84d6714840c9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 436
diff changeset
   865
    ymax=65,
435
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   866
    axis lines=left,
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   867
    width=9cm,
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   868
    height=5cm, 
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   869
    legend entries={Scala V3},
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   870
    legend pos=north west,
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   871
    legend cell align=left]
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   872
\addplot[green,mark=square*,mark options={fill=white}] table {re2a.data};
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   873
\addplot[black,mark=square*,mark options={fill=white}] table {re3a.data};
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   874
\end{axis}
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   875
\end{tikzpicture}
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   876
\end{center}
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   877
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   878
\end{frame}
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   879
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
e08431a78f66 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 434
diff changeset
   880
433
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   881
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   882
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   883
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
119
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   884
\begin{frame}[t]
342
c235e0aeb8df updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 338
diff changeset
   885
\frametitle{What is good about this Alg.}
c235e0aeb8df updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 338
diff changeset
   886
c235e0aeb8df updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 338
diff changeset
   887
\begin{itemize}
c235e0aeb8df updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 338
diff changeset
   888
\item extends to most regular expressions, for example
c235e0aeb8df updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 338
diff changeset
   889
\bl{$\sim r$}
c235e0aeb8df updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 338
diff changeset
   890
c235e0aeb8df updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 338
diff changeset
   891
\item is easy to implement in a functional language
c235e0aeb8df updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 338
diff changeset
   892
c235e0aeb8df updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 338
diff changeset
   893
\item the algorithm is already quite old; there is still
c235e0aeb8df updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 338
diff changeset
   894
  work to be done to use it as a tokenizer (that is brand new work)
c235e0aeb8df updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 338
diff changeset
   895
c235e0aeb8df updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 338
diff changeset
   896
\item we can prove its correctness\ldots
c235e0aeb8df updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 338
diff changeset
   897
\end{itemize}
c235e0aeb8df updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 338
diff changeset
   898
c235e0aeb8df updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 338
diff changeset
   899
\end{frame}
c235e0aeb8df updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 338
diff changeset
   900
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
c235e0aeb8df updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 338
diff changeset
   901
c235e0aeb8df updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 338
diff changeset
   902
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
c235e0aeb8df updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 338
diff changeset
   903
\begin{frame}[t]
337
885ac2b6c27d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 336
diff changeset
   904
\frametitle{Proofs about Rexps}
17
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   905
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   906
Remember their inductive definition:\\[5cm]
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   907
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   908
\begin{textblock}{6}(5,5)
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   909
  \begin{tabular}{@ {}rrl}
429
7e71c947ec69 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   910
  \bl{$r$} & \bl{$::=$}  & \bl{$\ZERO$}\\
7e71c947ec69 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   911
         & \bl{$\mid$} & \bl{$\ONE$}     \\
337
885ac2b6c27d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 336
diff changeset
   912
         & \bl{$\mid$} & \bl{$c$}            \\
119
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   913
         & \bl{$\mid$} & \bl{$r_1 \cdot r_2$}\\
337
885ac2b6c27d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 336
diff changeset
   914
         & \bl{$\mid$} & \bl{$r_1 + r_2$}    \\
885ac2b6c27d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 336
diff changeset
   915
         & \bl{$\mid$} & \bl{$r^*$}          \\
17
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   916
  \end{tabular}
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   917
  \end{textblock}
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   918
119
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   919
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
   920
337
885ac2b6c27d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 336
diff changeset
   921
\end{frame}
17
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   922
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   923
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   924
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   925
\begin{frame}[c]
337
885ac2b6c27d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 336
diff changeset
   926
\frametitle{Proofs about Rexp (2)}
17
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   927
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   928
\begin{itemize}
429
7e71c947ec69 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   929
\item \bl{$P$} holds for \bl{$\ZERO$}, \bl{$\ONE$} and \bl{c}\bigskip
119
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
   930
\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
   931
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
   932
\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
   933
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
   934
\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
   935
holds for \bl{$r$}.
17
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   936
\end{itemize}
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   937
337
885ac2b6c27d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 336
diff changeset
   938
\end{frame}
17
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   939
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   940
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   941
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   942
\begin{frame}[c]
337
885ac2b6c27d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 336
diff changeset
   943
\frametitle{Proofs about Rexp (3)}
17
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   944
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   945
Assume \bl{$P(r)$} is the property:
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   946
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   947
\begin{center}
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   948
\bl{$nullable(r)$} if and only if \bl{$[] \in L(r)$}
17
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   949
\end{center}
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   950
337
885ac2b6c27d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 336
diff changeset
   951
\end{frame}
17
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   952
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   953
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   954
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   955
\begin{frame}[c]
337
885ac2b6c27d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 336
diff changeset
   956
\frametitle{Proofs about Rexp (4)}
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   957
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   958
\begin{center}
338
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
   959
\bl{\begin{tabular}{r@{\hspace{2mm}}c@{\hspace{2mm}}l}
429
7e71c947ec69 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   960
$rev(\ZERO)$   & $\dn$ & $\ZERO$\\
7e71c947ec69 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   961
$rev(\ONE)$      & $\dn$ & $\ONE$\\
338
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
   962
$rev(c)$             & $\dn$ & $c$\\
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
   963
$rev(r_1 + r_2)$     & $\dn$ & $rev(r_1) + rev(r_2)$\\
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
   964
$rev(r_1 \cdot r_2)$ & $\dn$ & $rev(r_2) \cdot rev(r_1)$\\
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
   965
$rev(r^*)$           & $\dn$ & $rev(r)^*$\\
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   966
\end{tabular}}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   967
\end{center}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   968
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   969
We can prove
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   970
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   971
\begin{center}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   972
\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
   973
\end{center}
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   974
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   975
by induction on \bl{$r$}.
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   976
337
885ac2b6c27d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 336
diff changeset
   977
\end{frame}
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   978
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
   979
338
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
   980
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
   981
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
   982
\begin{frame}[c]
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
   983
\frametitle{\begin{tabular}{c}
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
   984
  Correctness Proof\\[-1mm] for our Matcher\end{tabular}}
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
   985
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
   986
\begin{itemize}
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
   987
\item We started from
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
   988
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
   989
\begin{center}
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
   990
\begin{tabular}{rp{4cm}}
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
   991
  & \bl{$s \in L(r)$}\medskip\\
433
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   992
\bl{$\Leftrightarrow$} & \bl{$[] \in \Ders\,s\,(L(r))$}\pause  
338
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
   993
\end{tabular}
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
   994
\end{center}
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
   995
433
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
   996
\item if we can show \bl{$\Ders\, s\,(L(r)) = L(\ders\,s\,r)$} we 
338
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
   997
have
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
   998
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
   999
\begin{center}
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
  1000
\begin{tabular}{rp{4cm}}
433
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
  1001
\bl{$\Leftrightarrow$} & \bl{$[] \in L(\ders\,s\,r)$}\medskip\\
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
  1002
\bl{$\Leftrightarrow$} & \bl{$nullable(\ders\,s\,r)$}\medskip\\
338
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
  1003
\bl{$\dn$} & \bl{$matches\,s\,r$}
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
  1004
\end{tabular}
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
  1005
\end{center}
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
  1006
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
  1007
\end{itemize}
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
  1008
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
  1009
\end{frame}
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
  1010
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
  1011
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
  1012
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
  1013
\begin{frame}[c]
337
885ac2b6c27d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 336
diff changeset
  1014
\frametitle{Proofs about Rexp (5)}
263
92e6985018ae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 261
diff changeset
  1015
119
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
  1016
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
  1017
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
  1018
\begin{center}
433
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
  1019
\bl{$\Der\,c\,A \dn \{ s \;|\;  c\!::\!s \in A\}$ } 
119
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
  1020
\end{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
  1021
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
  1022
We can prove
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
  1023
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
  1024
\begin{center}
433
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
  1025
\bl{$L(\der\,c\,r) = \Der\,c\,(L(r))$}
119
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
  1026
\end{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
  1027
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
  1028
by induction on \bl{$r$}.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
  1029
337
885ac2b6c27d updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 336
diff changeset
  1030
\end{frame}
119
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
  1031
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
  1032
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
  1033
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
  1034
\begin{frame}[c]
338
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
  1035
\frametitle{Proofs about Strings}
17
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
  1036
119
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
  1037
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
  1038
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
  1039
\begin{itemize}
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
  1040
\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
  1041
\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
  1042
already holds for \bl{$s$}
17
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
  1043
\end{itemize}
338
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
  1044
\end{frame}
17
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
  1045
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
  1046
19
Christian Urban <urbanc@in.tum.de>
parents: 17
diff changeset
  1047
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <urbanc@in.tum.de>
parents: 17
diff changeset
  1048
\begin{frame}[c]
338
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
  1049
\frametitle{Proofs about Strings (2)}
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
  1050
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
  1051
We can then prove
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
  1052
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
  1053
\begin{center}
433
c08290ee4f1f updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 431
diff changeset
  1054
\bl{$\Ders\,s\,(L(r)) = L(\ders\,s\,r)$}  
338
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
  1055
\end{center}
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
  1056
19
Christian Urban <urbanc@in.tum.de>
parents: 17
diff changeset
  1057
119
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 118
diff changeset
  1058
We can finally prove
19
Christian Urban <urbanc@in.tum.de>
parents: 17
diff changeset
  1059
Christian Urban <urbanc@in.tum.de>
parents: 17
diff changeset
  1060
\begin{center}
345
0922b3e01289 updated slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 342
diff changeset
  1061
\bl{$matches\,s\,r$}  if and only if  \bl{$s \in L(r)$} 
19
Christian Urban <urbanc@in.tum.de>
parents: 17
diff changeset
  1062
\end{center}
Christian Urban <urbanc@in.tum.de>
parents: 17
diff changeset
  1063
Christian Urban <urbanc@in.tum.de>
parents: 17
diff changeset
  1064
338
f16120cb4e19 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 337
diff changeset
  1065
\end{frame}
19
Christian Urban <urbanc@in.tum.de>
parents: 17
diff changeset
  1066
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
17
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
  1067
436
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1068
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1069
\begin{frame}[c]
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1070
\frametitle{Epilogue}
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1071
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1072
\footnotesize
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1073
\begin{center}
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1074
\begin{tabular}{cc}
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1075
\begin{tikzpicture}
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1076
\begin{axis}[
442
84d6714840c9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 436
diff changeset
  1077
    title={\small{}Graph: \bl{$a^{?\{n\}} \cdot a^{\{n\}}$}},
436
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1078
    xlabel={$n$},
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1079
    x label style={at={(1.04,0.0)}},
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1080
    ylabel={time in secs},
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1081
    enlargelimits=false,
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1082
    xmax=7100000,
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1083
    ytick={0,5,...,30},
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1084
    ymax=33,
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1085
    %scaled ticks=false,
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1086
    axis lines=left,
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1087
    width=5cm,
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1088
    height=5cm, 
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1089
    legend entries={Scala V3, Scala V4},
442
84d6714840c9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 436
diff changeset
  1090
    legend style={at={(0.1,-0.2)},anchor=north}]
436
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1091
\addplot[black,mark=square*,mark options={fill=white}] table {re3.data};
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1092
\addplot[purple,mark=square*,mark options={fill=white}] table {re4.data};
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1093
\end{axis}
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1094
\end{tikzpicture}
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1095
&
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1096
\begin{tikzpicture}
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1097
\begin{axis}[
442
84d6714840c9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 436
diff changeset
  1098
    title={\small{}Graph: \bl{$(a^*)^* \cdot b$}},
436
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1099
    xlabel={$n$},
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1100
    x label style={at={(1.09,0.0)}},
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1101
    ylabel={time in secs},
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1102
    enlargelimits=false,
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1103
    xmax=8100000,
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1104
    ytick={0,5,...,30},
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1105
    ymax=33,
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1106
    %scaled ticks=false,
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1107
    axis lines=left,
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1108
    width=5cm,
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1109
    height=5cm, 
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1110
    legend entries={Scala V3, Scala V4},
442
84d6714840c9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 436
diff changeset
  1111
    legend style={at={(0.1,-0.2)},anchor=north}]
436
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1112
\addplot[black,mark=square*,mark options={fill=white}] table {re3a.data};
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1113
\addplot[purple,mark=square*,mark options={fill=white}] table {re4a.data};
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1114
\end{axis}
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1115
\end{tikzpicture}
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1116
\end{tabular}
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1117
\end{center}
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1118
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1119
\only<2->{\footnotesize
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1120
\begin{textblock}{9}(0.5,8)
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1121
\begin{bubble}[11.8cm]
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1122
\lstinputlisting[numbers=none]{../progs/app52.scala}
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1123
\end{bubble}
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1124
\end{textblock}} 
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1125
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1126
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1127
\end{frame}
9213b8298ca9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 435
diff changeset
  1128
7
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1129
\end{document}
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1130
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1131
%%% Local Variables:  
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1132
%%% mode: latex
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1133
%%% TeX-master: t
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1134
%%% End: 
73cf4406b773 updated
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1135