handouts/ho01.tex
author Christian Urban <urbanc@in.tum.de>
Sat, 07 Jan 2017 14:52:26 +0000
changeset 471 9476086849ad
parent 452 b93f4d2aeee1
child 473 dc528091eb70
child 503 f2d7b885b3e3
permissions -rw-r--r--
updated
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
105
397ecdafefd8 added handouts
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     1
\documentclass{article}
237
370c0647a9bf more material
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 217
diff changeset
     2
\usepackage{../style}
217
cd6066f1056a updated handouts
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 123
diff changeset
     3
\usepackage{../langs}
242
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
     4
\usepackage{../graphics}
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
     5
\usepackage{../data}
108
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 107
diff changeset
     6
306
fecffce112fa updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 291
diff changeset
     7
%%http://regexcrossword.com/challenges/cities/puzzles/1
398
c8ce95067c1a updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 395
diff changeset
     8
%%https://jex.im/regulex/
c8ce95067c1a updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 395
diff changeset
     9
%%https://www.reddit.com/r/ProgrammingLanguages/comments/42dlem/mona_compiler_development_part_2_parsing/
c8ce95067c1a updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 395
diff changeset
    10
%%https://www.reddit.com/r/ProgrammingLanguages/comments/43wlkq/formal_grammar_for_csh_tsch_sh_or_bash/
112
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 111
diff changeset
    11
403
564f7584eff1 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 399
diff changeset
    12
%% regex displayers
564f7584eff1 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 399
diff changeset
    13
%% https://regexper.com/#a%7Ca
564f7584eff1 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 399
diff changeset
    14
%% https://www.debuggex.com
564f7584eff1 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 399
diff changeset
    15
%% https://jex.im/regulex/#!embed=false&flags=&re=%5E(a%7Cb)*%3F%24
564f7584eff1 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 399
diff changeset
    16
564f7584eff1 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 399
diff changeset
    17
%% email validator
564f7584eff1 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 399
diff changeset
    18
%% http://www.ex-parrot.com/%7Epdw/Mail-RFC822-Address.html
564f7584eff1 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 399
diff changeset
    19
564f7584eff1 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 399
diff changeset
    20
%% regex testers
564f7584eff1 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 399
diff changeset
    21
% https://regex101.com
564f7584eff1 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 399
diff changeset
    22
% http://regexr.com
564f7584eff1 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 399
diff changeset
    23
564f7584eff1 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 399
diff changeset
    24
%% emacs regexes
564f7584eff1 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 399
diff changeset
    25
%% https://www.gnu.org/software/emacs/manual/html_node/elisp/Regular-Expressions.html
564f7584eff1 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 399
diff changeset
    26
415
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
    27
%%  reasons for a new prgramming language
403
564f7584eff1 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 399
diff changeset
    28
%% http://beautifulracket.com
564f7584eff1 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 399
diff changeset
    29
418
010c5a03dca2 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 417
diff changeset
    30
% compiler explorer
010c5a03dca2 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 417
diff changeset
    31
% https://gcc.godbolt.org
010c5a03dca2 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 417
diff changeset
    32
010c5a03dca2 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 417
diff changeset
    33
105
397ecdafefd8 added handouts
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    34
\begin{document}
471
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
    35
\fnote{\copyright{} Christian Urban, King's College London, 2014, 2015, 2016, 2017}
105
397ecdafefd8 added handouts
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    36
397ecdafefd8 added handouts
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    37
\section*{Handout 1}
397ecdafefd8 added handouts
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    38
242
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
    39
This module is about text processing, be it for web-crawlers,
471
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
    40
compilers, dictionaries, DNA-data and so on. When looking for a
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
    41
particular string, like $abc$ in a large text we can use the
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
    42
Knuth-Morris-Pratt algorithm, which is currently the most efficient
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
    43
general string search algorithm. But often we do \emph{not} just look
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
    44
for a particular string, but for string patterns. For example in
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
    45
program code we need to identify what are the keywords (if, then,
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
    46
while, etc), what are the identifiers (variable names). A pattern for
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
    47
identifiers could be stated as: they start with a letter, followed by
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
    48
zero or more letters, numbers and underscores.  Also often we face the
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
    49
problem that we are given a string (for example some user input) and
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
    50
want to know whether it matches a particular pattern---be it an email
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
    51
address, for example. In this way we can exclude user input that would
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
    52
otherwise have nasty effects on our program (crashing it or making it
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
    53
go into an infinite loop, if not worse). The point is that the fast
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
    54
Knuth-Morris-Pratt algorithm for strings is not good enough for such
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
    55
string patterns.\smallskip
291
201c2c6d8696 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
    56
201c2c6d8696 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
    57
\defn{Regular expressions} help with conveniently specifying
201c2c6d8696 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
    58
such patterns. The idea behind regular expressions is that
201c2c6d8696 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
    59
they are a simple method for describing languages (or sets of
201c2c6d8696 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
    60
strings)\ldots at least languages we are interested in in
201c2c6d8696 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
    61
computer science. For example there is no convenient regular
201c2c6d8696 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
    62
expression for describing the English language short of
201c2c6d8696 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
    63
enumerating all English words. But they seem useful for
399
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
    64
describing for example simple email addresses.\footnote{See
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
    65
``8 Regular Expressions You Should Know''
291
201c2c6d8696 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
    66
\url{http://goo.gl/5LoVX7}} Consider the following regular
201c2c6d8696 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
    67
expression
242
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
    68
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
    69
\begin{equation}\label{email}
416
357c395ae838 updated
Christian Urban <urbanc@in.tum.de>
parents: 415
diff changeset
    70
\texttt{[a-z0-9\_.-]+} \;\;\texttt{@}\;\; \texttt{[a-z0-9.-]+} \;\;\texttt{.}\;\; \texttt{[a-z.]\{2,6\}}
242
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
    71
\end{equation}
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
    72
416
357c395ae838 updated
Christian Urban <urbanc@in.tum.de>
parents: 415
diff changeset
    73
\noindent where the first part, the user name, matches one or more lowercase
242
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
    74
letters (\pcode{a-z}), digits (\pcode{0-9}), underscores, dots
404
245d302791c7 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 403
diff changeset
    75
and hyphens. The \pcode{+} at the end of the brackets ensures
471
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
    76
the ``one or more''. Then comes the email \pcode{@}-sign, followed
404
245d302791c7 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 403
diff changeset
    77
by the domain name which must be one or more lowercase
245d302791c7 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 403
diff changeset
    78
letters, digits, underscores, dots or hyphens. Note there
245d302791c7 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 403
diff changeset
    79
cannot be an underscore in the domain name. Finally there must
245d302791c7 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 403
diff changeset
    80
be a dot followed by the toplevel domain. This toplevel domain
245d302791c7 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 403
diff changeset
    81
must be 2 to 6 lowercase letters including the dot. Example
245d302791c7 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 403
diff changeset
    82
strings which follow this pattern are:
242
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
    83
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
    84
\begin{lstlisting}[language={},numbers=none,keywordstyle=\color{black}]
243
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
    85
niceandsimple@example.org
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
    86
very.common@example.co.uk
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
    87
a.little.lengthy.but.fine@dept.example.ac.uk
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
    88
other.email-with-dash@example.edu
242
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
    89
\end{lstlisting}
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
    90
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
    91
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
    92
\noindent
399
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
    93
But for example the following two do not
242
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
    94
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
    95
\begin{lstlisting}[language={},numbers=none,keywordstyle=\color{black}]
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
    96
user@localserver
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
    97
disposable.style.email.with+symbol@example.com
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
    98
\end{lstlisting}
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
    99
471
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
   100
\noindent according to the regular expression we specified in line
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
   101
\eqref{email} above. Whether this is intended or not is a different
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
   102
question (the second email above is actually an acceptable email
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
   103
address acording to the RFC 5322 standard for email addresses).
399
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   104
 
327
9470cd124667 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 318
diff changeset
   105
As mentioned above, identifiers, or variables, in program code
9470cd124667 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 318
diff changeset
   106
are often required to satisfy the constraints that they start
9470cd124667 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 318
diff changeset
   107
with a letter and then can be followed by zero or more letters
9470cd124667 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 318
diff changeset
   108
or numbers and also can include underscores, but not as the
9470cd124667 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 318
diff changeset
   109
first character. Such identifiers can be recognised with the
9470cd124667 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 318
diff changeset
   110
regular expression
242
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   111
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   112
\begin{center}
243
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   113
\pcode{[a-zA-Z] [a-zA-Z0-9_]*}
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   114
\end{center}
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   115
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   116
\noindent Possible identifiers that match this regular expression 
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   117
are \pcode{x}, \pcode{foo}, \pcode{foo_bar_1}, \pcode{A_very_42_long_object_name},
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   118
but not \pcode{_i} and also not \pcode{4you}.
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   119
404
245d302791c7 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 403
diff changeset
   120
Many programming languages offer libraries that can be used to
243
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   121
validate such strings against regular expressions. Also there
248
ce767ca23244 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 245
diff changeset
   122
are some common, and I am sure very familiar, ways of how to
404
245d302791c7 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 403
diff changeset
   123
construct regular expressions. For example in Scala we have
245d302791c7 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 403
diff changeset
   124
a library implementing the following regular expressions: 
243
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   125
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   126
\begin{center}
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   127
\begin{tabular}{lp{9cm}}
242
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   128
\pcode{re*} & matches 0 or more occurrences of preceding 
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   129
expression\\
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   130
\pcode{re+} & matches 1 or more occurrences of preceding
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   131
expression\\
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   132
\pcode{re?} &	 matches 0 or 1 occurrence of preceding 
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   133
expression\\
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   134
\pcode{re\{n\}}	& matches exactly \pcode{n} number of 
243
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   135
occurrences of preceding  expression\\
242
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   136
\pcode{re\{n,m\}} & matches at least \pcode{n} and at most {\tt m}
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   137
occurences of the preceding expression\\
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   138
\pcode{[...]} & matches any single character inside the 
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   139
brackets\\
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   140
\pcode{[^...]} & matches any single character not inside the 
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   141
brackets\\
250
b79e704acb72 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 248
diff changeset
   142
\pcode{...-...} & character ranges\\
b79e704acb72 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 248
diff changeset
   143
\pcode{\\d} & matches digits; equivalent to \pcode{[0-9]}\\
b79e704acb72 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 248
diff changeset
   144
\pcode{.} & matches every character except newline\\
b79e704acb72 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 248
diff changeset
   145
\pcode{(re)}	& groups regular expressions and remembers 
b79e704acb72 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 248
diff changeset
   146
matched text
243
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   147
\end{tabular}
242
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   148
\end{center}
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   149
243
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   150
\noindent With this table you can figure out the purpose of
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   151
the regular expressions in the web-crawlers shown Figures
250
b79e704acb72 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 248
diff changeset
   152
\ref{crawler1}, \ref{crawler2} and
416
357c395ae838 updated
Christian Urban <urbanc@in.tum.de>
parents: 415
diff changeset
   153
\ref{crawler3}. Note, however, the regular expression for
332
4755ad4b457b updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 327
diff changeset
   154
http-addresses in web-pages in Figure~\ref{crawler1}, Line 15,
4755ad4b457b updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 327
diff changeset
   155
is intended to be
242
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   156
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   157
\[
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   158
\pcode{"https?://[^"]*"}
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   159
\]
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   160
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   161
\noindent It specifies that web-addresses need to start with a
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   162
double quote, then comes \texttt{http} followed by an optional
332
4755ad4b457b updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 327
diff changeset
   163
\texttt{s} and so on until the closing double quote comes.
4755ad4b457b updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 327
diff changeset
   164
Usually we would have to escape the double quotes in order to
4755ad4b457b updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 327
diff changeset
   165
make sure we interpret the double quote as character, not as
4755ad4b457b updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 327
diff changeset
   166
double quote for a string. But Scala's trick with triple
4755ad4b457b updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 327
diff changeset
   167
quotes allows us to omit this kind of escaping. As a result we
4755ad4b457b updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 327
diff changeset
   168
can just write:
242
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   169
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   170
\[
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   171
\pcode{""""https?://[^"]*"""".r}
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   172
\]
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   173
243
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   174
\noindent Note also that the convention in Scala is that
242
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   175
\texttt{.r} converts a string into a regular expression. I
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   176
leave it to you to ponder whether this regular expression
243
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   177
really captures all possible web-addresses.
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   178
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   179
\subsection*{Why Study Regular Expressions?}
242
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   180
471
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
   181
Regular expressions were introduced by Kleene in the 1950ies and they
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
   182
have been object of intense study since then. They are nowadays pretty
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
   183
much ubiquitous in computer science. There are many libraries
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
   184
implementing regular expressions. I am sure you have come across them
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
   185
before (remember the PRA module?). Why on earth then is there any
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
   186
interest in studying them again in depth in this module? Well, one
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
   187
answer is in the following two graphs about regular expression
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
   188
matching in Python, Ruby and Java.
242
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   189
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   190
\begin{center}
416
357c395ae838 updated
Christian Urban <urbanc@in.tum.de>
parents: 415
diff changeset
   191
\begin{tabular}{@{\hspace{-1mm}}c@{\hspace{-1mm}}c@{}}
291
201c2c6d8696 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   192
\begin{tikzpicture}
399
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   193
\begin{axis}[
415
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   194
    title={Graph: $\texttt{a?\{n\}\,a{\{n\}}}$ and strings 
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   195
           $\underbrace{\texttt{a}\ldots \texttt{a}}_{n}$},
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   196
    xlabel={$n$},
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   197
    x label style={at={(1.05,0.0)}},
399
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   198
    ylabel={time in secs},
291
201c2c6d8696 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   199
    enlargelimits=false,
201c2c6d8696 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   200
    xtick={0,5,...,30},
201c2c6d8696 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   201
    xmax=33,
201c2c6d8696 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   202
    ymax=35,
201c2c6d8696 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   203
    ytick={0,5,...,30},
201c2c6d8696 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   204
    scaled ticks=false,
201c2c6d8696 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   205
    axis lines=left,
415
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   206
    width=5.5cm,
318
7975e4f0d4de updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 306
diff changeset
   207
    height=4.5cm, 
291
201c2c6d8696 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   208
    legend entries={Python,Ruby},  
201c2c6d8696 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   209
    legend pos=north west,
201c2c6d8696 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   210
    legend cell align=left]
448
96129128d0f1 updated
Christian Urban <urbanc@in.tum.de>
parents: 443
diff changeset
   211
\addplot[blue,mark=*, mark options={fill=white}] table {re-python.data};
96129128d0f1 updated
Christian Urban <urbanc@in.tum.de>
parents: 443
diff changeset
   212
\addplot[brown,mark=triangle*, mark options={fill=white}] table {re-ruby.data};  
291
201c2c6d8696 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   213
\end{axis}
242
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   214
\end{tikzpicture}
415
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   215
&
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   216
\begin{tikzpicture}
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   217
\begin{axis}[
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   218
    title={Graph: $\texttt{(a*)*\,b}$ and strings 
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   219
           $\underbrace{\texttt{a}\ldots \texttt{a}}_{n}$},
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   220
    xlabel={$n$},
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   221
    x label style={at={(1.05,0.0)}},
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   222
    ylabel={time in secs},
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   223
    enlargelimits=false,
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   224
    xtick={0,5,...,30},
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   225
    xmax=33,
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   226
    ymax=35,
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   227
    ytick={0,5,...,30},
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   228
    scaled ticks=false,
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   229
    axis lines=left,
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   230
    width=5.5cm,
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   231
    height=4.5cm, 
448
96129128d0f1 updated
Christian Urban <urbanc@in.tum.de>
parents: 443
diff changeset
   232
    legend entries={Python, Java},  
415
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   233
    legend pos=north west,
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   234
    legend cell align=left]
448
96129128d0f1 updated
Christian Urban <urbanc@in.tum.de>
parents: 443
diff changeset
   235
\addplot[blue,mark=*, mark options={fill=white}] table {re-python2.data};
415
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   236
\addplot[cyan,mark=*, mark options={fill=white}] table {re-java.data};
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   237
\end{axis}
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   238
\end{tikzpicture}
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   239
\end{tabular}
242
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   240
\end{center}
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   241
415
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   242
\noindent This first graph shows that Python needs approximately 29
448
96129128d0f1 updated
Christian Urban <urbanc@in.tum.de>
parents: 443
diff changeset
   243
seconds for finding out whether a string of 28 \texttt{a}s matches the
96129128d0f1 updated
Christian Urban <urbanc@in.tum.de>
parents: 443
diff changeset
   244
regular expression \texttt{a?\{28\}\,a\{28\}}.  Ruby is even slightly
96129128d0f1 updated
Christian Urban <urbanc@in.tum.de>
parents: 443
diff changeset
   245
worse.\footnote{In this example Ruby uses the slightly different
96129128d0f1 updated
Christian Urban <urbanc@in.tum.de>
parents: 443
diff changeset
   246
  regular expression \texttt{a?a?a?...a?a?aaa...aa}, where the
96129128d0f1 updated
Christian Urban <urbanc@in.tum.de>
parents: 443
diff changeset
   247
  \texttt{a?} and \texttt{a} each occur $n$ times. More such test
96129128d0f1 updated
Christian Urban <urbanc@in.tum.de>
parents: 443
diff changeset
   248
  cases can be found at \url{http://www.computerbytesman.com/redos/}.}
96129128d0f1 updated
Christian Urban <urbanc@in.tum.de>
parents: 443
diff changeset
   249
Simlarly, Python and Java needs approximately 30 seconds to find out
96129128d0f1 updated
Christian Urban <urbanc@in.tum.de>
parents: 443
diff changeset
   250
that the regular expression $\texttt{(a*)*\,b}$ does not match strings
96129128d0f1 updated
Christian Urban <urbanc@in.tum.de>
parents: 443
diff changeset
   251
of 28 \texttt{a}s.  Admittedly, these regular expressions are
96129128d0f1 updated
Christian Urban <urbanc@in.tum.de>
parents: 443
diff changeset
   252
carefully chosen to exhibit this exponential behaviour, but similar
96129128d0f1 updated
Christian Urban <urbanc@in.tum.de>
parents: 443
diff changeset
   253
ones occur more often than one wants in ``real life''. For example, on
96129128d0f1 updated
Christian Urban <urbanc@in.tum.de>
parents: 443
diff changeset
   254
20 July 2016 a similar regular expression brought the webpage
407
4b454a6d1814 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 404
diff changeset
   255
\href{http://stackexchange.com}{Stack Exchange} to its knees:
4b454a6d1814 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 404
diff changeset
   256
4b454a6d1814 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 404
diff changeset
   257
\begin{center}
4b454a6d1814 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 404
diff changeset
   258
\url{http://stackstatus.net/post/147710624694/outage-postmortem-july-20-2016}
4b454a6d1814 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 404
diff changeset
   259
\end{center}
4b454a6d1814 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 404
diff changeset
   260
417
e74c696821a2 updated
Christian Urban <urbanc@in.tum.de>
parents: 416
diff changeset
   261
\noindent I can also highly recommend a cool webtalk from an engineer
e74c696821a2 updated
Christian Urban <urbanc@in.tum.de>
parents: 416
diff changeset
   262
from Stack Exchange on the same subject:
e74c696821a2 updated
Christian Urban <urbanc@in.tum.de>
parents: 416
diff changeset
   263
e74c696821a2 updated
Christian Urban <urbanc@in.tum.de>
parents: 416
diff changeset
   264
\begin{center}
e74c696821a2 updated
Christian Urban <urbanc@in.tum.de>
parents: 416
diff changeset
   265
\url{https://vimeo.com/112065252}
e74c696821a2 updated
Christian Urban <urbanc@in.tum.de>
parents: 416
diff changeset
   266
\end{center}
e74c696821a2 updated
Christian Urban <urbanc@in.tum.de>
parents: 416
diff changeset
   267
407
4b454a6d1814 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 404
diff changeset
   268
\noindent
417
e74c696821a2 updated
Christian Urban <urbanc@in.tum.de>
parents: 416
diff changeset
   269
A similar problem also occured in the Atom editor:
416
357c395ae838 updated
Christian Urban <urbanc@in.tum.de>
parents: 415
diff changeset
   270
357c395ae838 updated
Christian Urban <urbanc@in.tum.de>
parents: 415
diff changeset
   271
\begin{center}
357c395ae838 updated
Christian Urban <urbanc@in.tum.de>
parents: 415
diff changeset
   272
\url{http://davidvgalbraith.com/how-i-fixed-atom/}
357c395ae838 updated
Christian Urban <urbanc@in.tum.de>
parents: 415
diff changeset
   273
\end{center}
357c395ae838 updated
Christian Urban <urbanc@in.tum.de>
parents: 415
diff changeset
   274
357c395ae838 updated
Christian Urban <urbanc@in.tum.de>
parents: 415
diff changeset
   275
\noindent
415
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   276
Such troublesome regular expressions are sometimes called \emph{evil
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   277
  regular expressions} because they have the potential to make regular
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   278
expression matching engines to topple over, like in Python, Ruby and
416
357c395ae838 updated
Christian Urban <urbanc@in.tum.de>
parents: 415
diff changeset
   279
Java. This ``toppling over'' is also sometimes called \emph{catastrophic
415
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   280
  backtracking}.  The problem with evil regular expressions is that
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   281
they can have some serious consequences, for example, if you use them
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   282
in your web-application. The reason is that hackers can look for these
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   283
instances where the matching engine behaves badly and then mount a
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   284
nice DoS-attack against your application. These attacks are already
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   285
have their own name: \emph{Regular Expression Denial of Service
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   286
  Attacks (ReDoS)}.
242
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   287
243
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   288
It will be instructive to look behind the ``scenes'' to find
242
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   289
out why Python and Ruby (and others) behave so badly when
416
357c395ae838 updated
Christian Urban <urbanc@in.tum.de>
parents: 415
diff changeset
   290
matching strings with evil regular expressions. But we will also look
242
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   291
at a relatively simple algorithm that solves this problem much
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   292
better than Python and Ruby do\ldots actually it will be two
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   293
versions of the algorithm: the first one will be able to
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   294
process strings of approximately 1,000 \texttt{a}s in 30
243
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   295
seconds, while the second version will even be able to process
443
cd43d8c6eb84 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 418
diff changeset
   296
up to 7,000(!) in 30 seconds, see the graph below:
242
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   297
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   298
\begin{center}
291
201c2c6d8696 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   299
\begin{tikzpicture}
399
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   300
  \begin{axis}[
415
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   301
    title={Graph: $\texttt{a?\{n\}\,a{\{n\}}}$ and strings 
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   302
           $\underbrace{\texttt{a}\ldots \texttt{a}}_{n}$},
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   303
    xlabel={$n$},
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   304
    x label style={at={(1.05,0.0)}},
399
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   305
    ylabel={time in secs},
291
201c2c6d8696 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   306
    enlargelimits=false,
443
cd43d8c6eb84 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 418
diff changeset
   307
    xtick={0,3000,...,9000},
cd43d8c6eb84 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 418
diff changeset
   308
    xmax=10000,
cd43d8c6eb84 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 418
diff changeset
   309
    ymax=32,
cd43d8c6eb84 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 418
diff changeset
   310
    ytick={0,5,...,30},
291
201c2c6d8696 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   311
    scaled ticks=false,
201c2c6d8696 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   312
    axis lines=left,
415
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   313
    width=7cm,
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   314
    height=4.5cm,
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   315
    legend entries={Our Algorithm V1, Our Algorithm V2},
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   316
    legend pos=outer north east]
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   317
\addplot[green,mark=square*,mark options={fill=white}] table {re2.data};
291
201c2c6d8696 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   318
\addplot[black,mark=square*,mark options={fill=white}] table {re3.data};
201c2c6d8696 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   319
\end{axis}
242
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   320
\end{tikzpicture}
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   321
\end{center}
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   322
415
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   323
\noindent And in the case of the regular expression $\texttt{(a*)*\,b}$
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   324
and strings of \texttt{a}s we will beat Java by factor of
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   325
approximately 1,000,000 (note the scale on the $x$-axis). 
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   326
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   327
\begin{center}
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   328
\begin{tikzpicture}
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   329
  \begin{axis}[
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   330
    title={Graph: $\texttt{(a*)*\,b}$ and strings 
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   331
           $\underbrace{\texttt{a}\ldots \texttt{a}}_{n}$},
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   332
    xlabel={$n$},
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   333
    x label style={at={(1.05,0.0)}},
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   334
    ylabel={time in secs},
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   335
    enlargelimits=false,
443
cd43d8c6eb84 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 418
diff changeset
   336
    ymax=32,
cd43d8c6eb84 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 418
diff changeset
   337
    ytick={0,5,...,30},
415
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   338
    axis lines=left,
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   339
    width=7cm,
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   340
    height=4.5cm,
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   341
    legend entries={Our Algorithm V2},
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   342
    legend pos=outer north east]
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   343
\addplot[black,mark=square*,mark options={fill=white}] table {re3a.data};
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   344
\end{axis}
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   345
\end{tikzpicture}
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   346
\end{center}
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   347
242
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   348
\subsection*{Basic Regular Expressions}
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   349
399
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   350
The regular expressions shown earlier for Scala, we
243
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   351
will call \emph{extended regular expressions}. The ones we
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   352
will mainly study in this module are \emph{basic regular
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   353
expressions}, which by convention we will just call
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   354
\emph{regular expressions}, if it is clear what we mean. The
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   355
attraction of (basic) regular expressions is that many
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   356
features of the extended ones are just syntactic sugar.
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   357
(Basic) regular expressions are defined by the following
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   358
grammar:
242
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   359
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   360
\begin{center}
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   361
\begin{tabular}{r@{\hspace{1mm}}r@{\hspace{1mm}}l@{\hspace{13mm}}l}
399
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   362
  $r$ & $::=$ &    $\ZERO$          & null language\\
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   363
        & $\mid$ & $\ONE$           & empty string / \texttt{""} / []\\
242
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   364
        & $\mid$ & $c$                  & single character\\
243
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   365
        & $\mid$ & $r_1 + r_2$          & alternative / choice\\
242
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   366
        & $\mid$ & $r_1 \cdot r_2$      & sequence\\
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   367
        & $\mid$ & $r^*$                & star (zero or more)\\
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   368
  \end{tabular}
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   369
\end{center}
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   370
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   371
\noindent Because we overload our notation, there are some
243
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   372
subtleties you should be aware of. When regular expressions
404
245d302791c7 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 403
diff changeset
   373
are referred to, then $\ZERO$ (in bold font) does not stand for
399
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   374
the number zero: rather it is a particular pattern that does
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   375
not match any string. Similarly, in the context of regular
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   376
expressions, $\ONE$ does not stand for the number one but for
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   377
a regular expression that matches the empty string. The letter
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   378
$c$ stands for any character from the alphabet at hand. Again
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   379
in the context of regular expressions, it is a particular
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   380
pattern that can match the specified character. You should
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   381
also be careful with our overloading of the star: assuming you
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   382
have read the handout about our basic mathematical notation,
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   383
you will see that in the context of languages (sets of
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   384
strings) the star stands for an operation on languages. Here
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   385
$r^*$ stands for a regular expression, which is different from
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   386
the operation on sets is defined as
242
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   387
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   388
\[
399
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   389
A\star\dn \bigcup_{0\le n} A^n
242
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   390
\]
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   391
334
fd89a63e9db3 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   392
242
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   393
We will use parentheses to disambiguate regular expressions.
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   394
Parentheses are not really part of a regular expression, and
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   395
indeed we do not need them in our code because there the tree
243
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   396
structure of regular expressions is always clear. But for
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   397
writing them down in a more mathematical fashion, parentheses
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   398
will be helpful. For example we will write $(r_1 + r_2)^*$,
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   399
which is different from, say $r_1 + (r_2)^*$. The former means
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   400
roughly zero or more times $r_1$ or $r_2$, while the latter
248
ce767ca23244 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 245
diff changeset
   401
means $r_1$ or zero or more times $r_2$. This will turn out to
ce767ca23244 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 245
diff changeset
   402
be two different patterns, which match in general different
243
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   403
strings. We should also write $(r_1 + r_2) + r_3$, which is
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   404
different from the regular expression $r_1 + (r_2 + r_3)$, but
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   405
in case of $+$ and $\cdot$ we actually do not care about the
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   406
order and just write $r_1 + r_2 + r_3$, or $r_1 \cdot r_2
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   407
\cdot r_3$, respectively. The reasons for this will become
399
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   408
clear shortly. 
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   409
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   410
In the literature you will often find that the choice $r_1 +
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   411
r_2$ is written as $r_1\mid{}r_2$ or $r_1\mid\mid{}r_2$. Also,
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   412
often our $\ZERO$ and $\ONE$ are written $\varnothing$ and
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   413
$\epsilon$, respectively. Following the convention in the
243
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   414
literature, we will often omit the $\cdot$ all together. This
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   415
is to make some concrete regular expressions more readable.
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   416
For example the regular expression for email addresses shown
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   417
in \eqref{email} would look like
242
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   418
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   419
\[
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   420
\texttt{[...]+} \;\cdot\;  \texttt{@} \;\cdot\; 
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   421
\texttt{[...]+} \;\cdot\; \texttt{.} \;\cdot\; 
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   422
\texttt{[...]\{2,6\}}
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   423
\]
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   424
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   425
\noindent
471
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
   426
which is much less readable than the regular expression in
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
   427
\eqref{email}. Similarly for the regular expression that matches the
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
   428
string $hello$ we should write
242
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   429
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   430
\[
248
ce767ca23244 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 245
diff changeset
   431
h \cdot e \cdot l \cdot l \cdot o
242
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   432
\]
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   433
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   434
\noindent
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   435
but often just write {\it hello}.
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   436
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   437
If you prefer to think in terms of the implementation
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   438
of regular expressions in Scala, the constructors and
245
a5fade10c207 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 244
diff changeset
   439
classes relate as follows\footnote{More about Scala is 
404
245d302791c7 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 403
diff changeset
   440
in the handout about \emph{A Crash-Course on Scala}.}
242
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   441
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   442
\begin{center}
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   443
\begin{tabular}{rcl}
399
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   444
$\ZERO$       & $\mapsto$ & \texttt{ZERO}\\
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   445
$\ONE$        & $\mapsto$ & \texttt{ONE}\\
242
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   446
$c$           & $\mapsto$ & \texttt{CHAR(c)}\\
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   447
$r_1 + r_2$   & $\mapsto$ & \texttt{ALT(r1, r2)}\\
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   448
$r_1 \cdot r_2$ & $\mapsto$ & \texttt{SEQ(r1, r2)}\\
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   449
$r^*$         & $\mapsto$ & \texttt{STAR(r)}
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   450
\end{tabular}
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   451
\end{center}
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   452
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   453
A source of confusion might arise from the fact that we
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   454
use the term \emph{basic regular expression} for the regular
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   455
expressions used in ``theory'' and defined above, and
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   456
\emph{extended regular expression} for the ones used in
243
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   457
``practice'', for example in Scala. If runtime is not an
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   458
issue, then the latter can be seen as syntactic sugar of
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   459
the former. For example we could replace
242
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   460
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   461
\begin{center}
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   462
\begin{tabular}{rcl}
471
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
   463
$r^+$ & $\mapsto$ & $r\cdot r^*$\\
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
   464
$r^?$ & $\mapsto$ & $\ONE + r$\\
242
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   465
$\backslash d$ & $\mapsto$ & $0 + 1 + 2 + \ldots + 9$\\
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   466
$[\text{\it a - z}]$ & $\mapsto$ & $a + b + \ldots + z$\\
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   467
\end{tabular}
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   468
\end{center}
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   469
243
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   470
242
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   471
\subsection*{The Meaning of Regular Expressions}
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   472
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   473
So far we have only considered informally what the
243
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   474
\emph{meaning} of a regular expression is. This is not good
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   475
enough for specifications of what algorithms are supposed to
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   476
do or which problems they are supposed to solve.
242
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   477
243
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   478
To define the meaning of a regular expression we will
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   479
associate with every regular expression a language, or set of
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   480
strings. This language contains all the strings the regular
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   481
expression is supposed to match. To understand what is going
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   482
on here it is crucial that you have read the handout
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   483
about basic mathematical notations.
242
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   484
243
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   485
The \defn{meaning of a regular expression} can be defined
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   486
by a recursive function called $L$ (for language), which
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   487
is defined as follows
242
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   488
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   489
\begin{center}
399
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   490
\begin{tabular}{rcll}
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   491
$L(\ZERO)$         & $\dn$ & $\{\}$\\
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   492
$L(\ONE)$          & $\dn$ & $\{[]\}$\\
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   493
$L(c)$             & $\dn$ & $\{"c"\}$ & or equivalently $\dn \{[c]\}$\\
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   494
$L(r_1+ r_2)$      & $\dn$ & $L(r_1) \cup L(r_2)$\\
243
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   495
$L(r_1 \cdot r_2)$ & $\dn$ & $L(r_1) \,@\, L(r_2)$\\
399
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   496
$L(r^*)$           & $\dn$ & $(L(r))\star$\\
242
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   497
\end{tabular}
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   498
\end{center}
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   499
243
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   500
\noindent As a result we can now precisely state what the
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   501
meaning, for example, of the regular expression $h \cdot
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   502
e \cdot l \cdot l \cdot o$ is, namely
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   503
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   504
\[
248
ce767ca23244 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 245
diff changeset
   505
L(h \cdot e \cdot  l \cdot l \cdot o) = \{"hello"\}
243
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   506
\]
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   507
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   508
\noindent This is expected because this regular expression 
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   509
is only supposed to match the ``$hello$''-string. Similarly if
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   510
we have the choice-regular-expression $a + b$, its meaning is
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   511
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   512
\[
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   513
L(a + b) = \{"a", "b"\}
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   514
\]
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   515
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   516
\noindent You can now also see why we do not make a difference
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   517
between the different regular expressions $(r_1 + r_2) + r_3$
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   518
and $r_1 + (r_2 + r_3)$\ldots they are not the same regular
248
ce767ca23244 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 245
diff changeset
   519
expression, but they have the same meaning. For example
318
7975e4f0d4de updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 306
diff changeset
   520
you can do the following calculation which shows they
7975e4f0d4de updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 306
diff changeset
   521
have the same meaning:
243
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   522
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   523
\begin{eqnarray*}
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   524
L((r_1 + r_2) + r_3) & = & L(r_1 + r_2) \cup L(r_3)\\
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   525
                     & = & L(r_1) \cup L(r_2) \cup L(r_3)\\
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   526
                     & = & L(r_1) \cup L(r_2 + r_3)\\
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   527
                     & = & L(r_1 + (r_2 + r_3))
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   528
\end{eqnarray*}
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   529
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   530
The point of the definition of $L$ is that we can use it to
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   531
precisely specify when a string $s$ is matched by a regular
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   532
expression $r$, namely if and only if $s \in L(r)$. In fact we
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   533
will write a program \pcode{match} that takes any string $s$
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   534
and any regular expression $r$ as argument and returns
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   535
\emph{yes}, if $s \in L(r)$ and \emph{no}, if $s \not\in
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   536
L(r)$. We leave this for the next lecture.
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   537
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   538
There is one more feature of regular expressions that is worth
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   539
mentioning. Given some strings, there are in general many
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   540
different regular expressions that can recognise these
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   541
strings. This is obvious with the regular expression $a + b$
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   542
which can match the strings $a$ and $b$. But also the regular
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   543
expression $b + a$ would match the same strings. However,
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   544
sometimes it is not so obvious whether two regular expressions
399
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   545
match the same strings: for example do $r^*$ and $\ONE + r
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   546
\cdot r^*$ match the same strings? What about $\ZERO^*$
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   547
and $\ONE^*$? This suggests the following relation between
243
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   548
\defn{equivalent regular expressions}: 
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   549
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   550
\[
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   551
r_1 \equiv r_2 \;\dn\; L(r_1) = L(r_2)
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   552
\]
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   553
248
ce767ca23244 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 245
diff changeset
   554
\noindent That means two regular expressions are said to be
ce767ca23244 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 245
diff changeset
   555
equivalent if they match the same set of strings. Therefore we
ce767ca23244 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 245
diff changeset
   556
do not really distinguish between the different regular
ce767ca23244 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 245
diff changeset
   557
expression $(r_1 + r_2) + r_3$ and $r_1 + (r_2 + r_3)$,
ce767ca23244 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 245
diff changeset
   558
because they are equivalent. I leave you to the question
ce767ca23244 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 245
diff changeset
   559
whether
243
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   560
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   561
\[
399
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   562
\ZERO^* \equiv \ONE^*
243
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   563
\]
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   564
399
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   565
\noindent holds or not? Such equivalences will be important
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   566
for our matching algorithm, because we can use them to
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   567
simplify regular expressions, which will mean we can speed
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   568
up the calculations. 
243
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   569
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   570
\subsection*{My Fascination for Regular Expressions}
242
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   571
471
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
   572
Up until a few years ago I was not really interested in regular
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
   573
expressions. They have been studied for the last 60 years (by smarter
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
   574
people than me)---surely nothing new can be found out about them. I
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
   575
even have the vague recollection that I did not quite understand them
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
   576
during my undergraduate study. If I remember correctly,\footnote{That
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
   577
  was really a long time ago.} I got utterly confused about $\ONE$
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
   578
(which my lecturer wrote as $\epsilon$) and the empty string (which he
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
   579
also wrote as $\epsilon$).\footnote{Obviously the lecturer must have
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
   580
  been bad ;o)} Since my then, I have used regular expressions for
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
   581
implementing lexers and parsers as I have always been interested in
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
   582
all kinds of programming languages and compilers, which invariably
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
   583
need regular expressions in some form or shape.
243
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   584
399
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   585
To understand my fascination \emph{nowadays} with regular
243
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   586
expressions, you need to know that my main scientific interest
471
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
   587
for the last 17 years has been with theorem provers. I am a
243
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   588
core developer of one of
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   589
them.\footnote{\url{http://isabelle.in.tum.de}} Theorem
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   590
provers are systems in which you can formally reason about
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   591
mathematical concepts, but also about programs. In this way
471
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
   592
theorem provers can help with the manacing problem of writing bug-free code. Theorem provers have
416
357c395ae838 updated
Christian Urban <urbanc@in.tum.de>
parents: 415
diff changeset
   593
proved already their value in a number of cases (even in
243
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   594
terms of hard cash), but they are still clunky and difficult
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   595
to use by average programmers.
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   596
471
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
   597
Anyway, in about 2011 I came across the notion of \defn{derivatives of
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
   598
  regular expressions}. This notion allows one to do almost all
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
   599
calculations with regular expressions on the level of regular
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
   600
expressions, not needing any automata (you will see we only touch
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
   601
briefly on automata in lecture 3). Automata are usually the main
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
   602
object of study in formal language courses.  The avoidance of automata
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
   603
is crucial because automata are graphs and it is rather difficult to
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
   604
reason about graphs in theorem provers. In contrast, reasoning about
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
   605
regular expressions is easy-peasy in theorem provers. Is this
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
   606
important? I think yes, because according to Kuklewicz nearly all
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
   607
POSIX-based regular expression matchers are
243
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   608
buggy.\footnote{\url{http://www.haskell.org/haskellwiki/Regex_Posix}}
471
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
   609
With my PhD student Fahad Ausaf I proved the correctness for one such
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
   610
matcher that was proposed by Sulzmann and Lu in
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
   611
2014.\footnote{\url{http://goo.gl/bz0eHp}} Hopefully we can prove that
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
   612
the machine code(!)  that implements this code efficiently is correct
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
   613
also. Writing programs in this way does not leave any room for
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
   614
potential errors or bugs. How nice!
243
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   615
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   616
What also helped with my fascination with regular expressions
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   617
is that we could indeed find out new things about them that
416
357c395ae838 updated
Christian Urban <urbanc@in.tum.de>
parents: 415
diff changeset
   618
have surprised some experts. Together with two colleagues from China, I was
243
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   619
able to prove the Myhill-Nerode theorem by only using regular
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   620
expressions and the notion of derivatives. Earlier versions of
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   621
this theorem used always automata in the proof. Using this
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   622
theorem we can show that regular languages are closed under
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   623
complementation, something which Gasarch in his
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   624
blog\footnote{\url{http://goo.gl/2R11Fw}} assumed can only be
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   625
shown via automata. Even sombody who has written a 700+-page
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   626
book\footnote{\url{http://goo.gl/fD0eHx}} on regular
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   627
exprssions did not know better. Well, we showed it can also be
248
ce767ca23244 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 245
diff changeset
   628
done with regular expressions only.\footnote{\url{http://www.inf.kcl.ac.uk/staff/urbanc/Publications/rexp.pdf}} 
471
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
   629
What a feeling when you are an outsider to the subject!
243
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   630
471
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
   631
To conclude: Despite my early ignorance about regular expressions, I
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
   632
find them now very interesting. They have a beautiful mathematical
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
   633
theory behind them, which can be sometimes quite deep and which
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
   634
sometimes contains hidden snares. They have practical importance
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
   635
(remember the shocking runtime of the regular expression matchers in
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
   636
Python, Ruby and Java in some instances and the problems in Stack
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
   637
Exchange and the Atom editor).  People who are not very familiar with
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
   638
the mathematical background of regular expressions get them
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
   639
consistently wrong (surprising given they are a supposed to be core
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
   640
skill for computer scientists). The hope is that we can do better in
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
   641
the future---for example by proving that the algorithms actually
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
   642
satisfy their specification and that the corresponding implementations
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
   643
do not contain any bugs. We are close, but not yet quite there.
242
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   644
332
4755ad4b457b updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 327
diff changeset
   645
Notwithstanding my fascination, I am also happy to admit that regular
244
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   646
expressions have their shortcomings. There are some well-known
471
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
   647
``theoretical'' shortcomings, for example recognising strings of the
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
   648
form $a^{n}b^{n}$ is not possible with regular expressions. This means
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
   649
for example if we try to regognise whether parentheses are well-nested
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
   650
is impossible with (basic) regular expressions.  I am not so bothered
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
   651
by these shortcomings. What I am bothered about is when regular
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
   652
expressions are in the way of practical programming. For example, it
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
   653
turns out that the regular expression for email addresses shown in
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
   654
\eqref{email} is hopelessly inadequate for recognising all of them
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
   655
(despite being touted as something every computer scientist should
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
   656
know about). The W3 Consortium (which standardises the Web) proposes
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
   657
to use the following, already more complicated regular expressions for
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
   658
email addresses:
244
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   659
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   660
{\small\begin{lstlisting}[language={},keywordstyle=\color{black},numbers=none]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   661
[a-zA-Z0-9.!#$%&'*+/=?^_`{|}~-]+@[a-zA-Z0-9-]+(?:\.[a-zA-Z0-9-]+)*
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   662
\end{lstlisting}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   663
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   664
\noindent But they admit that by using this regular expression
471
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
   665
they wilfully violate the RFC 5322 standard, which specifies
244
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   666
the syntax of email addresses. With their proposed regular
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   667
expression they are too strict in some cases and too lax in
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   668
others. Not a good situation to be in. A regular expression
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   669
that is claimed to be closer to the standard is shown in
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   670
Figure~\ref{monster}. Whether this claim is true or not, I
416
357c395ae838 updated
Christian Urban <urbanc@in.tum.de>
parents: 415
diff changeset
   671
would not know---the only thing I can say about this regular
248
ce767ca23244 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 245
diff changeset
   672
expression is it is a monstrosity. However, this might
ce767ca23244 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 245
diff changeset
   673
actually be an argument against the RFC standard, rather than
399
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   674
against regular expressions. A similar argument is made in
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   675
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   676
\begin{center}
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   677
\url{https://elliot.land/validating-an-email-address}
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   678
\end{center}
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   679
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   680
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   681
\noindent which explains some of the crazier parts of email
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   682
addresses. Still it is good to know that some tasks in text
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   683
processing just cannot be achieved by using regular
471
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
   684
expressions. But for what we want to use them (lexing) they are
9476086849ad updated
Christian Urban <urbanc@in.tum.de>
parents: 452
diff changeset
   685
pretty good.
244
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   686
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   687
242
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   688
\begin{figure}[p]
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   689
\lstinputlisting{../progs/crawler1.scala}
399
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   690
242
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   691
\caption{The Scala code for a simple web-crawler that checks
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   692
for broken links in a web-page. It uses the regular expression
399
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   693
\texttt{http\_pattern} in Line~\ref{httpline} for recognising
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   694
URL-addresses. It finds all links using the library function
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   695
\texttt{findAllIn} in Line~\ref{findallline}.\label{crawler1}}
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   696
242
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   697
\end{figure}
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   698
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   699
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   700
\begin{figure}[p]
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   701
\lstinputlisting{../progs/crawler2.scala}
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   702
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   703
\caption{A version of the web-crawler that only follows links
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   704
in ``my'' domain---since these are the ones I am interested in
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   705
to fix. It uses the regular expression \texttt{my\_urls} in
399
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   706
Line~\ref{myurlline} to check for my name in the links. The
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   707
main change is in
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   708
Lines~\ref{changestartline}--\ref{changeendline} where there
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   709
is a test whether URL is in ``my'' domain or
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   710
not.\label{crawler2}}
242
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   711
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   712
\end{figure}
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   713
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   714
\begin{figure}[p]
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   715
\lstinputlisting{../progs/crawler3.scala}
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   716
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   717
\caption{A small email harvester---whenever we download a
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   718
web-page, we also check whether it contains any email
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   719
addresses. For this we use the regular expression
399
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   720
\texttt{email\_pattern} in Line~\ref{emailline}. The main
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   721
change is in Line~\ref{mainline} where all email addresses
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   722
that can be found in a page are printed.\label{crawler3}}
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   723
242
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   724
\end{figure}
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   725
244
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   726
\begin{figure}[p]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   727
\tiny
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   728
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   729
\begin{minipage}{0.8\textwidth}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   730
\lstinputlisting[language={},keywordstyle=\color{black},numbers=none]{../progs/email-rexp}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   731
\end{minipage}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   732
\end{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   733
404
245d302791c7 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 403
diff changeset
   734
\caption{Nothing that can be said about this regular
416
357c395ae838 updated
Christian Urban <urbanc@in.tum.de>
parents: 415
diff changeset
   735
expression\ldots{}except it is a monstrosity.\label{monster}}
244
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   736
\end{figure}
108
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 107
diff changeset
   737
112
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 111
diff changeset
   738
105
397ecdafefd8 added handouts
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   739
\end{document}
397ecdafefd8 added handouts
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   740
397ecdafefd8 added handouts
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   741
%%% Local Variables: 
397ecdafefd8 added handouts
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   742
%%% mode: latex
397ecdafefd8 added handouts
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   743
%%% TeX-master: t
397ecdafefd8 added handouts
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   744
%%% End: