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