handouts/ho01.tex
author Christian Urban <urbanc@in.tum.de>
Tue, 23 Aug 2016 15:38:20 +0200
changeset 416 357c395ae838
parent 415 4ae59fd3b174
child 417 e74c696821a2
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
105
397ecdafefd8 added handouts
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    30
\begin{document}
399
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
    31
\fnote{\copyright{} Christian Urban, King's College London, 2014, 2015, 2016}
105
397ecdafefd8 added handouts
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    32
397ecdafefd8 added handouts
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    33
\section*{Handout 1}
397ecdafefd8 added handouts
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    34
242
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
    35
This module is about text processing, be it for web-crawlers,
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
    36
compilers, dictionaries, DNA-data and so on. When looking for
404
245d302791c7 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 403
diff changeset
    37
a particular string, like $abc$ in a large text we can use the
242
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
    38
Knuth-Morris-Pratt algorithm, which is currently the most
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
    39
efficient general string search algorithm. But often we do
243
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
    40
\emph{not} just look for a particular string, but for string
395
e57d3d92b856 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 363
diff changeset
    41
patterns. For example in program code we need to identify what
e57d3d92b856 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 363
diff changeset
    42
are the keywords, what are the identifiers etc. A pattern for
e57d3d92b856 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 363
diff changeset
    43
identifiers could be stated as: they start with a letter,
291
201c2c6d8696 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
    44
followed by zero or more letters, numbers and underscores.
243
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
    45
Also often we face the problem that we are given a string (for
242
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
    46
example some user input) and want to know whether it matches a
399
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
    47
particular pattern---be it an email address, for example. In
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
    48
this way we can exclude user input that would otherwise have
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
    49
nasty effects on our program (crashing it or making it go into
416
357c395ae838 updated
Christian Urban <urbanc@in.tum.de>
parents: 415
diff changeset
    50
an infinite loop, if not worse).\smallskip
291
201c2c6d8696 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
    51
201c2c6d8696 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
    52
\defn{Regular expressions} help with conveniently specifying
201c2c6d8696 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
    53
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
    54
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
    55
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
    56
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
    57
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
    58
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
    59
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
    60
``8 Regular Expressions You Should Know''
291
201c2c6d8696 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
    61
\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
    62
expression
242
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
    63
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
    64
\begin{equation}\label{email}
416
357c395ae838 updated
Christian Urban <urbanc@in.tum.de>
parents: 415
diff changeset
    65
\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
    66
\end{equation}
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
    67
416
357c395ae838 updated
Christian Urban <urbanc@in.tum.de>
parents: 415
diff changeset
    68
\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
    69
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
    70
and hyphens. The \pcode{+} at the end of the brackets ensures
245d302791c7 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 403
diff changeset
    71
the ``one or more''. Then comes the \pcode{@}-sign, followed
245d302791c7 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 403
diff changeset
    72
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
    73
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
    74
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
    75
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
    76
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
    77
strings which follow this pattern are:
242
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
    78
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
    79
\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
    80
niceandsimple@example.org
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
    81
very.common@example.co.uk
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
    82
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
    83
other.email-with-dash@example.edu
242
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
    84
\end{lstlisting}
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
    85
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
    86
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
    87
\noindent
399
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
    88
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
    89
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
    90
\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
    91
user@localserver
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
    92
disposable.style.email.with+symbol@example.com
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
    93
\end{lstlisting}
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
    94
399
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
    95
\noindent according to the regular expression we specified in
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
    96
\eqref{email}. Whether this is intended or not is a different
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
    97
question (the second email above is actually an acceptable
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
    98
email address acording to the RFC 5322 standard for email
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
    99
addresses).
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   100
 
327
9470cd124667 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 318
diff changeset
   101
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
   102
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
   103
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
   104
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
   105
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
   106
regular expression
242
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   107
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   108
\begin{center}
243
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   109
\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
   110
\end{center}
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   111
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   112
\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
   113
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
   114
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
   115
404
245d302791c7 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 403
diff changeset
   116
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
   117
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
   118
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
   119
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
   120
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
   121
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   122
\begin{center}
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   123
\begin{tabular}{lp{9cm}}
242
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   124
\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
   125
expression\\
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   126
\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
   127
expression\\
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   128
\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
   129
expression\\
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   130
\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
   131
occurrences of preceding  expression\\
242
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   132
\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
   133
occurences of the preceding expression\\
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   134
\pcode{[...]} & matches any single character inside the 
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   135
brackets\\
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   136
\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
   137
brackets\\
250
b79e704acb72 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 248
diff changeset
   138
\pcode{...-...} & character ranges\\
b79e704acb72 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 248
diff changeset
   139
\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
   140
\pcode{.} & matches every character except newline\\
b79e704acb72 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 248
diff changeset
   141
\pcode{(re)}	& groups regular expressions and remembers 
b79e704acb72 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 248
diff changeset
   142
matched text
243
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   143
\end{tabular}
242
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   144
\end{center}
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   145
243
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   146
\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
   147
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
   148
\ref{crawler1}, \ref{crawler2} and
416
357c395ae838 updated
Christian Urban <urbanc@in.tum.de>
parents: 415
diff changeset
   149
\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
   150
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
   151
is intended to be
242
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   152
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   153
\[
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   154
\pcode{"https?://[^"]*"}
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   155
\]
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
\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
   158
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
   159
\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
   160
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
   161
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
   162
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
   163
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
   164
can just write:
242
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   165
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   166
\[
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   167
\pcode{""""https?://[^"]*"""".r}
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   168
\]
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   169
243
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   170
\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
   171
\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
   172
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
   173
really captures all possible web-addresses.
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   174
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   175
\subsection*{Why Study Regular Expressions?}
242
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   176
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   177
Regular expressions were introduced by Kleene in the 1950ies
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   178
and they have been object of intense study since then. They
404
245d302791c7 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 403
diff changeset
   179
are nowadays pretty much ubiquitous in computer science. There
245d302791c7 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 403
diff changeset
   180
are many libraries implementing regular expressions. I am sure
245d302791c7 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 403
diff changeset
   181
you have come across them before (remember PRA?). Why on earth
245d302791c7 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 403
diff changeset
   182
then is there any interest in studying them again in depth in
415
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   183
this module? Well, one answer is in the following two graphs about
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   184
regular expression matching in Python, Ruby and Java.
242
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   185
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   186
\begin{center}
416
357c395ae838 updated
Christian Urban <urbanc@in.tum.de>
parents: 415
diff changeset
   187
\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
   188
\begin{tikzpicture}
399
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   189
\begin{axis}[
415
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   190
    title={Graph: $\texttt{a?\{n\}\,a{\{n\}}}$ and strings 
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   191
           $\underbrace{\texttt{a}\ldots \texttt{a}}_{n}$},
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   192
    xlabel={$n$},
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   193
    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
   194
    ylabel={time in secs},
291
201c2c6d8696 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   195
    enlargelimits=false,
201c2c6d8696 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   196
    xtick={0,5,...,30},
201c2c6d8696 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   197
    xmax=33,
201c2c6d8696 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   198
    ymax=35,
201c2c6d8696 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   199
    ytick={0,5,...,30},
201c2c6d8696 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   200
    scaled ticks=false,
201c2c6d8696 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   201
    axis lines=left,
415
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   202
    width=5.5cm,
318
7975e4f0d4de updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 306
diff changeset
   203
    height=4.5cm, 
291
201c2c6d8696 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   204
    legend entries={Python,Ruby},  
201c2c6d8696 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   205
    legend pos=north west,
201c2c6d8696 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   206
    legend cell align=left]
201c2c6d8696 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   207
\addplot[blue,mark=*, mark options={fill=white}] 
201c2c6d8696 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   208
  table {re-python.data};
201c2c6d8696 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   209
\addplot[brown,mark=triangle*, mark options={fill=white}] 
201c2c6d8696 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   210
  table {re-ruby.data};  
201c2c6d8696 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   211
\end{axis}
242
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   212
\end{tikzpicture}
415
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   213
&
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   214
\begin{tikzpicture}
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   215
\begin{axis}[
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   216
    title={Graph: $\texttt{(a*)*\,b}$ and strings 
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   217
           $\underbrace{\texttt{a}\ldots \texttt{a}}_{n}$},
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   218
    xlabel={$n$},
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   219
    x label style={at={(1.05,0.0)}},
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   220
    ylabel={time in secs},
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   221
    enlargelimits=false,
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   222
    xtick={0,5,...,30},
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   223
    xmax=33,
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   224
    ymax=35,
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   225
    ytick={0,5,...,30},
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   226
    scaled ticks=false,
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   227
    axis lines=left,
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   228
    width=5.5cm,
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   229
    height=4.5cm, 
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   230
    legend entries={Java},  
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   231
    legend pos=north west,
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   232
    legend cell align=left]
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   233
\addplot[cyan,mark=*, mark options={fill=white}] table {re-java.data};
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   234
\end{axis}
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   235
\end{tikzpicture}
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   236
\end{tabular}
242
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   237
\end{center}
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   238
415
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   239
\noindent This first graph shows that Python needs approximately 29
243
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   240
seconds for finding out whether a string of 28 \texttt{a}s
415
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   241
matches the regular expression \texttt{a?\{28\}\,a\{28\}}.
242
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   242
Ruby is even slightly worse.\footnote{In this example Ruby
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   243
uses the slightly different regular expression
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   244
\texttt{a?a?a?...a?a?aaa...aa}, where the \texttt{a?} and
404
245d302791c7 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 403
diff changeset
   245
\texttt{a} each occur $n$ times. More such test cases can be
415
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   246
found at \url{http://www.computerbytesman.com/redos/}.} Simlarly, Java needs approximately
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   247
30 seconds to find out that the regular expression $\texttt{(a*)*\,b}$
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   248
does not match strings of 28 \texttt{a}s.
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   249
Admittedly, these regular expressions are carefully chosen to
252
e8ef8f38ca84 added style files
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 250
diff changeset
   250
exhibit this exponential behaviour, but similar ones occur
407
4b454a6d1814 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 404
diff changeset
   251
more often than one wants in ``real life''. For example, on 20
4b454a6d1814 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 404
diff changeset
   252
July 2016 a similar regular expression brought the webpage
4b454a6d1814 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 404
diff changeset
   253
\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
   254
4b454a6d1814 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 404
diff changeset
   255
\begin{center}
4b454a6d1814 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 404
diff changeset
   256
\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
   257
\end{center}
4b454a6d1814 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 404
diff changeset
   258
4b454a6d1814 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 404
diff changeset
   259
\noindent
416
357c395ae838 updated
Christian Urban <urbanc@in.tum.de>
parents: 415
diff changeset
   260
It was also a problem in the Atom editor
357c395ae838 updated
Christian Urban <urbanc@in.tum.de>
parents: 415
diff changeset
   261
357c395ae838 updated
Christian Urban <urbanc@in.tum.de>
parents: 415
diff changeset
   262
\begin{center}
357c395ae838 updated
Christian Urban <urbanc@in.tum.de>
parents: 415
diff changeset
   263
\url{http://davidvgalbraith.com/how-i-fixed-atom/}
357c395ae838 updated
Christian Urban <urbanc@in.tum.de>
parents: 415
diff changeset
   264
\end{center}
357c395ae838 updated
Christian Urban <urbanc@in.tum.de>
parents: 415
diff changeset
   265
357c395ae838 updated
Christian Urban <urbanc@in.tum.de>
parents: 415
diff changeset
   266
\noindent
415
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   267
Such troublesome regular expressions are sometimes called \emph{evil
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   268
  regular expressions} because they have the potential to make regular
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   269
expression matching engines to topple over, like in Python, Ruby and
416
357c395ae838 updated
Christian Urban <urbanc@in.tum.de>
parents: 415
diff changeset
   270
Java. This ``toppling over'' is also sometimes called \emph{catastrophic
415
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   271
  backtracking}.  The problem with evil regular expressions is that
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   272
they can have some serious consequences, for example, if you use them
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   273
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
   274
instances where the matching engine behaves badly and then mount a
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   275
nice DoS-attack against your application. These attacks are already
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   276
have their own name: \emph{Regular Expression Denial of Service
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   277
  Attacks (ReDoS)}.
242
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   278
243
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   279
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
   280
out why Python and Ruby (and others) behave so badly when
416
357c395ae838 updated
Christian Urban <urbanc@in.tum.de>
parents: 415
diff changeset
   281
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
   282
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
   283
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
   284
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
   285
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
   286
seconds, while the second version will even be able to process
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   287
up to 12,000 in less than 10(!) seconds, see the graph below:
242
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   288
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   289
\begin{center}
291
201c2c6d8696 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   290
\begin{tikzpicture}
399
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   291
  \begin{axis}[
415
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   292
    title={Graph: $\texttt{a?\{n\}\,a{\{n\}}}$ and strings 
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   293
           $\underbrace{\texttt{a}\ldots \texttt{a}}_{n}$},
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   294
    xlabel={$n$},
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   295
    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
   296
    ylabel={time in secs},
291
201c2c6d8696 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   297
    enlargelimits=false,
201c2c6d8696 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   298
    xtick={0,3000,...,12000},
415
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   299
    xmax=13000,
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   300
    ymax=12,
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   301
    ytick={0,5,10},
291
201c2c6d8696 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   302
    scaled ticks=false,
201c2c6d8696 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 268
diff changeset
   303
    axis lines=left,
415
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   304
    width=7cm,
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   305
    height=4.5cm,
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   306
    legend entries={Our Algorithm V1, Our Algorithm V2},
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   307
    legend pos=outer north east]
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   308
\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
   309
\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
   310
\end{axis}
242
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   311
\end{tikzpicture}
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   312
\end{center}
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   313
415
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   314
\noindent And in the case of the regular expression $\texttt{(a*)*\,b}$
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   315
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
   316
approximately 1,000,000 (note the scale on the $x$-axis). 
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   317
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   318
\begin{center}
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   319
\begin{tikzpicture}
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   320
  \begin{axis}[
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   321
    title={Graph: $\texttt{(a*)*\,b}$ and strings 
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   322
           $\underbrace{\texttt{a}\ldots \texttt{a}}_{n}$},
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   323
    xlabel={$n$},
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   324
    x label style={at={(1.05,0.0)}},
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   325
    ylabel={time in secs},
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   326
    enlargelimits=false,
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   327
    ymax=12,
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   328
    ytick={0,5,10},
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   329
    axis lines=left,
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   330
    width=7cm,
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   331
    height=4.5cm,
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   332
    legend entries={Our Algorithm V2},
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   333
    legend pos=outer north east]
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   334
\addplot[black,mark=square*,mark options={fill=white}] table {re3a.data};
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   335
\end{axis}
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   336
\end{tikzpicture}
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   337
\end{center}
4ae59fd3b174 updated
Christian Urban <urbanc@in.tum.de>
parents: 407
diff changeset
   338
242
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   339
\subsection*{Basic Regular Expressions}
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   340
399
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   341
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
   342
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
   343
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
   344
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
   345
\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
   346
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
   347
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
   348
(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
   349
grammar:
242
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   350
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   351
\begin{center}
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   352
\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
   353
  $r$ & $::=$ &    $\ZERO$          & null language\\
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   354
        & $\mid$ & $\ONE$           & empty string / \texttt{""} / []\\
242
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   355
        & $\mid$ & $c$                  & single character\\
243
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   356
        & $\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
   357
        & $\mid$ & $r_1 \cdot r_2$      & sequence\\
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   358
        & $\mid$ & $r^*$                & star (zero or more)\\
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   359
  \end{tabular}
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   360
\end{center}
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   361
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   362
\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
   363
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
   364
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
   365
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
   366
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
   367
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
   368
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
   369
$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
   370
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
   371
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
   372
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
   373
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
   374
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
   375
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
   376
$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
   377
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
   378
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   379
\[
399
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   380
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
   381
\]
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   382
334
fd89a63e9db3 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 332
diff changeset
   383
242
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   384
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
   385
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
   386
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
   387
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
   388
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
   389
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
   390
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
   391
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
   392
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
   393
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
   394
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
   395
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
   396
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
   397
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
   398
\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
   399
clear shortly. 
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   400
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   401
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
   402
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
   403
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
   404
$\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
   405
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
   406
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
   407
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
   408
in \eqref{email} would look like
242
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   409
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   410
\[
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   411
\texttt{[...]+} \;\cdot\;  \texttt{@} \;\cdot\; 
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   412
\texttt{[...]+} \;\cdot\; \texttt{.} \;\cdot\; 
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   413
\texttt{[...]\{2,6\}}
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   414
\]
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   415
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   416
\noindent
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   417
which is much less readable than \eqref{email}. Similarly for
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   418
the regular expression that matches the string $hello$ we 
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   419
should write
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   420
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   421
\[
248
ce767ca23244 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 245
diff changeset
   422
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
   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
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   426
but often just write {\it hello}.
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   427
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   428
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
   429
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
   430
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
   431
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
   432
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   433
\begin{center}
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   434
\begin{tabular}{rcl}
399
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   435
$\ZERO$       & $\mapsto$ & \texttt{ZERO}\\
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   436
$\ONE$        & $\mapsto$ & \texttt{ONE}\\
242
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   437
$c$           & $\mapsto$ & \texttt{CHAR(c)}\\
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   438
$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
   439
$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
   440
$r^*$         & $\mapsto$ & \texttt{STAR(r)}
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   441
\end{tabular}
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   442
\end{center}
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   443
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   444
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
   445
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
   446
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
   447
\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
   448
``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
   449
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
   450
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
   451
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   452
\begin{center}
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   453
\begin{tabular}{rcl}
243
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   454
$r+$ & $\mapsto$ & $r\cdot r^*$\\
399
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   455
$r?$ & $\mapsto$ & $\ONE + r$\\
242
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   456
$\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
   457
$[\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
   458
\end{tabular}
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   459
\end{center}
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   460
243
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   461
242
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   462
\subsection*{The Meaning of Regular Expressions}
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   463
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   464
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
   465
\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
   466
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
   467
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
   468
243
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   469
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
   470
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
   471
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
   472
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
   473
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
   474
about basic mathematical notations.
242
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   475
243
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   476
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
   477
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
   478
is defined as follows
242
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   479
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   480
\begin{center}
399
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   481
\begin{tabular}{rcll}
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   482
$L(\ZERO)$         & $\dn$ & $\{\}$\\
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   483
$L(\ONE)$          & $\dn$ & $\{[]\}$\\
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   484
$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
   485
$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
   486
$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
   487
$L(r^*)$           & $\dn$ & $(L(r))\star$\\
242
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   488
\end{tabular}
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   489
\end{center}
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   490
243
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   491
\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
   492
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
   493
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
   494
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   495
\[
248
ce767ca23244 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 245
diff changeset
   496
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
   497
\]
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   498
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   499
\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
   500
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
   501
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
   502
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
L(a + b) = \{"a", "b"\}
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   505
\]
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
\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
   508
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
   509
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
   510
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
   511
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
   512
have the same meaning:
243
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   513
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   514
\begin{eqnarray*}
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   515
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
   516
                     & = & 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
   517
                     & = & 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
   518
                     & = & L(r_1 + (r_2 + r_3))
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   519
\end{eqnarray*}
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   520
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   521
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
   522
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
   523
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
   524
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
   525
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
   526
\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
   527
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
   528
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   529
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
   530
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
   531
different regular expressions that can recognise these
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   532
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
   533
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
   534
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
   535
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
   536
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
   537
\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
   538
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
   539
\defn{equivalent regular expressions}: 
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   540
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   541
\[
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   542
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
   543
\]
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   544
248
ce767ca23244 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 245
diff changeset
   545
\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
   546
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
   547
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
   548
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
   549
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
   550
whether
243
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   551
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   552
\[
399
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   553
\ZERO^* \equiv \ONE^*
243
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   554
\]
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   555
399
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   556
\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
   557
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
   558
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
   559
up the calculations. 
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
\subsection*{My Fascination for Regular Expressions}
242
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   562
243
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   563
Up until a few years ago I was not really interested in
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   564
regular expressions. They have been studied for the last 60
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   565
years (by smarter people than me)---surely nothing new can be
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   566
found out about them. I even have the vague recollection that
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   567
I did not quite understand them during my study. If I remember
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   568
correctly,\footnote{That was really a long time ago.} I got
399
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   569
utterly confused about $\ONE$ (which my lecturer wrote as
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   570
$\epsilon$) and the empty string.\footnote{Obviously the
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   571
lecturer must have been bad.} Since my study, I have used
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   572
regular expressions for implementing lexers and parsers as I
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   573
have always been interested in all kinds of programming
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   574
languages and compilers, which invariably need regular
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   575
expression in some form or shape. 
243
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   576
399
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   577
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
   578
expressions, you need to know that my main scientific interest
248
ce767ca23244 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 245
diff changeset
   579
for the last 14 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
   580
core developer of one of
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   581
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
   582
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
   583
mathematical concepts, but also about programs. In this way
416
357c395ae838 updated
Christian Urban <urbanc@in.tum.de>
parents: 415
diff changeset
   584
theorem prover can help with the manacing problem of writing bug-free code. Theorem provers have
357c395ae838 updated
Christian Urban <urbanc@in.tum.de>
parents: 415
diff changeset
   585
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
   586
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
   587
to use by average programmers.
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   588
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   589
Anyway, in about 2011 I came across the notion of
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   590
\defn{derivatives of regular expressions}. This notion allows
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   591
one to do almost all calculations in regular language theory
416
357c395ae838 updated
Christian Urban <urbanc@in.tum.de>
parents: 415
diff changeset
   592
on the level of regular expressions, not needing any automata (you will
357c395ae838 updated
Christian Urban <urbanc@in.tum.de>
parents: 415
diff changeset
   593
see we only touch briefly on automata in lecture 3).
357c395ae838 updated
Christian Urban <urbanc@in.tum.de>
parents: 415
diff changeset
   594
This is crucial because automata are graphs and it is rather
243
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   595
difficult to reason about graphs in theorem provers. In
416
357c395ae838 updated
Christian Urban <urbanc@in.tum.de>
parents: 415
diff changeset
   596
contrast, reasoning about regular expressions is easy-peasy in
243
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   597
theorem provers. Is this important? I think yes, because
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   598
according to Kuklewicz nearly all POSIX-based regular
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   599
expression matchers are
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   600
buggy.\footnote{\url{http://www.haskell.org/haskellwiki/Regex_Posix}}
416
357c395ae838 updated
Christian Urban <urbanc@in.tum.de>
parents: 415
diff changeset
   601
With my PhD student Fahad Ausaf I proved
357c395ae838 updated
Christian Urban <urbanc@in.tum.de>
parents: 415
diff changeset
   602
the correctness for one such matcher that was
243
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   603
proposed by Sulzmann and Lu in
416
357c395ae838 updated
Christian Urban <urbanc@in.tum.de>
parents: 415
diff changeset
   604
2014.\footnote{\url{http://goo.gl/bz0eHp}} Hopefully we can
357c395ae838 updated
Christian Urban <urbanc@in.tum.de>
parents: 415
diff changeset
   605
prove that the machine code(!)
243
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   606
that implements this code efficiently is correct. Writing
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   607
programs in this way does not leave any room for potential
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   608
errors or bugs. How nice!
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   609
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   610
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
   611
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
   612
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
   613
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
   614
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
   615
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
   616
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
   617
complementation, something which Gasarch in his
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   618
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
   619
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
   620
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
   621
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
   622
done with regular expressions only.\footnote{\url{http://www.inf.kcl.ac.uk/staff/urbanc/Publications/rexp.pdf}} 
ce767ca23244 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 245
diff changeset
   623
What a feeling if 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
   624
8d5aaf5b0031 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 242
diff changeset
   625
To conclude: Despite my early ignorance about regular
399
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   626
expressions, I find them now very interesting. They have a
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   627
beautiful mathematical theory behind them, which can be
416
357c395ae838 updated
Christian Urban <urbanc@in.tum.de>
parents: 415
diff changeset
   628
sometimes quite deep and which contains hidden snares. They have
399
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   629
practical importance (remember the shocking runtime of the
416
357c395ae838 updated
Christian Urban <urbanc@in.tum.de>
parents: 415
diff changeset
   630
regular expression matchers in Python, Ruby and Java in some
357c395ae838 updated
Christian Urban <urbanc@in.tum.de>
parents: 415
diff changeset
   631
instances) and the problems in Stack Exchange and the Atom editor. 
357c395ae838 updated
Christian Urban <urbanc@in.tum.de>
parents: 415
diff changeset
   632
People who are not very familiar with the
399
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   633
mathematical background of regular expressions get them
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   634
consistently wrong. The hope is that we can do better in the
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   635
future---for example by proving that the algorithms actually
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   636
satisfy their specification and that the corresponding
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   637
implementations do not contain any bugs. We are close, but not
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   638
yet quite there.
242
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   639
332
4755ad4b457b updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 327
diff changeset
   640
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
   641
expressions have their shortcomings. There are some well-known
248
ce767ca23244 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 245
diff changeset
   642
``theoretical'' shortcomings, for example recognising strings
244
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   643
of the form $a^{n}b^{n}$. I am not so bothered by them. What I
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   644
am bothered about is when regular expressions are in the way
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   645
of practical programming. For example, it turns out that the
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   646
regular expression for email addresses shown in \eqref{email}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   647
is hopelessly inadequate for recognising all of them (despite
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   648
being touted as something every computer scientist should know
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   649
about). The W3 Consortium (which standardises the Web)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   650
proposes to use the following, already more complicated
248
ce767ca23244 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 245
diff changeset
   651
regular expressions for email addresses:
244
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   652
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   653
{\small\begin{lstlisting}[language={},keywordstyle=\color{black},numbers=none]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   654
[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
   655
\end{lstlisting}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   656
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   657
\noindent But they admit that by using this regular expression
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   658
they wilfully violate the RFC 5322 standard which specifies
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   659
the syntax of email addresses. With their proposed regular
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   660
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
   661
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
   662
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
   663
Figure~\ref{monster}. Whether this claim is true or not, I
416
357c395ae838 updated
Christian Urban <urbanc@in.tum.de>
parents: 415
diff changeset
   664
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
   665
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
   666
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
   667
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
   668
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   669
\begin{center}
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   670
\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
   671
\end{center}
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   672
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   673
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   674
\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
   675
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
   676
processing just cannot be achieved by using regular
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   677
expressions.
244
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   678
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   679
242
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   680
\begin{figure}[p]
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   681
\lstinputlisting{../progs/crawler1.scala}
399
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   682
242
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   683
\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
   684
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
   685
\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
   686
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
   687
\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
   688
242
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   689
\end{figure}
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   690
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   691
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   692
\begin{figure}[p]
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   693
\lstinputlisting{../progs/crawler2.scala}
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   694
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   695
\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
   696
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
   697
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
   698
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
   699
main change is in
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   700
Lines~\ref{changestartline}--\ref{changeendline} where there
5c1fbb39c93e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 398
diff changeset
   701
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
   702
not.\label{crawler2}}
242
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   703
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   704
\end{figure}
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   705
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   706
\begin{figure}[p]
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   707
\lstinputlisting{../progs/crawler3.scala}
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   708
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   709
\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
   710
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
   711
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
   712
\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
   713
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
   714
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
   715
242
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   716
\end{figure}
35104ee14f87 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 237
diff changeset
   717
244
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   718
\begin{figure}[p]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   719
\tiny
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   720
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   721
\begin{minipage}{0.8\textwidth}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   722
\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
   723
\end{minipage}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   724
\end{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 243
diff changeset
   725
404
245d302791c7 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 403
diff changeset
   726
\caption{Nothing that can be said about this regular
416
357c395ae838 updated
Christian Urban <urbanc@in.tum.de>
parents: 415
diff changeset
   727
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
   728
\end{figure}
108
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 107
diff changeset
   729
112
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 111
diff changeset
   730
105
397ecdafefd8 added handouts
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   731
\end{document}
397ecdafefd8 added handouts
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   732
397ecdafefd8 added handouts
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   733
%%% Local Variables: 
397ecdafefd8 added handouts
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   734
%%% mode: latex
397ecdafefd8 added handouts
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   735
%%% TeX-master: t
397ecdafefd8 added handouts
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   736
%%% End: