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