author | Christian Urban <urbanc@in.tum.de> |
Tue, 23 Aug 2016 12:26:13 +0200 | |
changeset 415 | 4ae59fd3b174 |
parent 407 | 4b454a6d1814 |
child 416 | 357c395ae838 |
permissions | -rw-r--r-- |
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
52ee218151f9
added
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
95ee5cc5c05d
added
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 | 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 |
5c1fbb39c93e
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
398
diff
changeset
|
50 |
an infinite loop, if not worse). |
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} |
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
65 |
\texttt{[a-z0-9\_.-]+ @ [a-z0-9.-]+ . [a-z.]\{2,6\}} |
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 |
|
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
68 |
\noindent where the first part matches one or more lowercase |
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 |
b79e704acb72
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
248
diff
changeset
|
149 |
\ref{crawler3}.\footnote{There is an interesting twist in the |
291
201c2c6d8696
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
268
diff
changeset
|
150 |
web-scraper where \pcode{re*?} is used instead of |
201c2c6d8696
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
268
diff
changeset
|
151 |
\pcode{re*}.} Note, however, the regular expression for |
332
4755ad4b457b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
327
diff
changeset
|
152 |
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
|
153 |
is intended to be |
242
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
154 |
|
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 |
\pcode{"https?://[^"]*"} |
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
157 |
\] |
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
158 |
|
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
159 |
\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
|
160 |
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
|
161 |
\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
|
162 |
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
|
163 |
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
|
164 |
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
|
165 |
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
|
166 |
can just write: |
242
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
167 |
|
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 |
\pcode{""""https?://[^"]*"""".r} |
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
170 |
\] |
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
171 |
|
243
8d5aaf5b0031
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
242
diff
changeset
|
172 |
\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
|
173 |
\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
|
174 |
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
|
175 |
really captures all possible web-addresses. |
8d5aaf5b0031
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
242
diff
changeset
|
176 |
|
8d5aaf5b0031
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
242
diff
changeset
|
177 |
\subsection*{Why Study Regular Expressions?} |
242
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
178 |
|
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
179 |
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
|
180 |
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
|
181 |
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
|
182 |
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
|
183 |
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
|
184 |
then is there any interest in studying them again in depth in |
415 | 185 |
this module? Well, one answer is in the following two graphs about |
186 |
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
|
187 |
|
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
188 |
\begin{center} |
415 | 189 |
\begin{tabular}{@{}cc@{}} |
291
201c2c6d8696
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
268
diff
changeset
|
190 |
\begin{tikzpicture} |
399
5c1fbb39c93e
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
398
diff
changeset
|
191 |
\begin{axis}[ |
415 | 192 |
title={Graph: $\texttt{a?\{n\}\,a{\{n\}}}$ and strings |
193 |
$\underbrace{\texttt{a}\ldots \texttt{a}}_{n}$}, |
|
194 |
xlabel={$n$}, |
|
195 |
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
|
196 |
ylabel={time in secs}, |
291
201c2c6d8696
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
268
diff
changeset
|
197 |
enlargelimits=false, |
201c2c6d8696
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
268
diff
changeset
|
198 |
xtick={0,5,...,30}, |
201c2c6d8696
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
268
diff
changeset
|
199 |
xmax=33, |
201c2c6d8696
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
268
diff
changeset
|
200 |
ymax=35, |
201c2c6d8696
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
268
diff
changeset
|
201 |
ytick={0,5,...,30}, |
201c2c6d8696
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
268
diff
changeset
|
202 |
scaled ticks=false, |
201c2c6d8696
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
268
diff
changeset
|
203 |
axis lines=left, |
415 | 204 |
width=5.5cm, |
318
7975e4f0d4de
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
306
diff
changeset
|
205 |
height=4.5cm, |
291
201c2c6d8696
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
268
diff
changeset
|
206 |
legend entries={Python,Ruby}, |
201c2c6d8696
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
268
diff
changeset
|
207 |
legend pos=north west, |
201c2c6d8696
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
268
diff
changeset
|
208 |
legend cell align=left] |
201c2c6d8696
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
268
diff
changeset
|
209 |
\addplot[blue,mark=*, mark options={fill=white}] |
201c2c6d8696
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
268
diff
changeset
|
210 |
table {re-python.data}; |
201c2c6d8696
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
268
diff
changeset
|
211 |
\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
|
212 |
table {re-ruby.data}; |
201c2c6d8696
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
268
diff
changeset
|
213 |
\end{axis} |
242
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
214 |
\end{tikzpicture} |
415 | 215 |
& |
216 |
\begin{tikzpicture} |
|
217 |
\begin{axis}[ |
|
218 |
title={Graph: $\texttt{(a*)*\,b}$ and strings |
|
219 |
$\underbrace{\texttt{a}\ldots \texttt{a}}_{n}$}, |
|
220 |
xlabel={$n$}, |
|
221 |
x label style={at={(1.05,0.0)}}, |
|
222 |
ylabel={time in secs}, |
|
223 |
enlargelimits=false, |
|
224 |
xtick={0,5,...,30}, |
|
225 |
xmax=33, |
|
226 |
ymax=35, |
|
227 |
ytick={0,5,...,30}, |
|
228 |
scaled ticks=false, |
|
229 |
axis lines=left, |
|
230 |
width=5.5cm, |
|
231 |
height=4.5cm, |
|
232 |
legend entries={Java}, |
|
233 |
legend pos=north west, |
|
234 |
legend cell align=left] |
|
235 |
\addplot[cyan,mark=*, mark options={fill=white}] table {re-java.data}; |
|
236 |
\end{axis} |
|
237 |
\end{tikzpicture} |
|
238 |
\end{tabular} |
|
242
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
239 |
\end{center} |
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
240 |
|
415 | 241 |
\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
|
242 |
seconds for finding out whether a string of 28 \texttt{a}s |
415 | 243 |
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
|
244 |
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
|
245 |
uses the slightly different regular expression |
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
246 |
\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
|
247 |
\texttt{a} each occur $n$ times. More such test cases can be |
415 | 248 |
found at \url{http://www.computerbytesman.com/redos/}.} Simlarly, Java needs approximately |
249 |
30 seconds to find out that the regular expression $\texttt{(a*)*\,b}$ |
|
250 |
does not match strings of 28 \texttt{a}s. |
|
251 |
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
|
252 |
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
|
253 |
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
|
254 |
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
|
255 |
\href{http://stackexchange.com}{Stack Exchange} to its knees: |
4b454a6d1814
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
404
diff
changeset
|
256 |
|
4b454a6d1814
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
404
diff
changeset
|
257 |
\begin{center} |
4b454a6d1814
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
404
diff
changeset
|
258 |
\url{http://stackstatus.net/post/147710624694/outage-postmortem-july-20-2016} |
4b454a6d1814
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
404
diff
changeset
|
259 |
\end{center} |
4b454a6d1814
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
404
diff
changeset
|
260 |
|
4b454a6d1814
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
404
diff
changeset
|
261 |
\noindent |
415 | 262 |
Such troublesome regular expressions are sometimes called \emph{evil |
263 |
regular expressions} because they have the potential to make regular |
|
264 |
expression matching engines to topple over, like in Python, Ruby and |
|
265 |
Java. This `toopling over' is also sometimes called \emph{catastrophic |
|
266 |
backtracking}. The problem with evil regular expressions is that |
|
267 |
they can have some serious consequences, for example, if you use them |
|
268 |
in your web-application. The reason is that hackers can look for these |
|
269 |
instances where the matching engine behaves badly and then mount a |
|
270 |
nice DoS-attack against your application. These attacks are already |
|
271 |
have their own name: \emph{Regular Expression Denial of Service |
|
272 |
Attacks (ReDoS)}. |
|
242
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
273 |
|
243
8d5aaf5b0031
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
242
diff
changeset
|
274 |
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
|
275 |
out why Python and Ruby (and others) behave so badly when |
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
276 |
matching with evil regular expressions. But we will also look |
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
277 |
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
|
278 |
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
|
279 |
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
|
280 |
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
|
281 |
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
|
282 |
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
|
283 |
|
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
284 |
\begin{center} |
291
201c2c6d8696
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
268
diff
changeset
|
285 |
\begin{tikzpicture} |
399
5c1fbb39c93e
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
398
diff
changeset
|
286 |
\begin{axis}[ |
415 | 287 |
title={Graph: $\texttt{a?\{n\}\,a{\{n\}}}$ and strings |
288 |
$\underbrace{\texttt{a}\ldots \texttt{a}}_{n}$}, |
|
289 |
xlabel={$n$}, |
|
290 |
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
|
291 |
ylabel={time in secs}, |
291
201c2c6d8696
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
268
diff
changeset
|
292 |
enlargelimits=false, |
201c2c6d8696
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
268
diff
changeset
|
293 |
xtick={0,3000,...,12000}, |
415 | 294 |
xmax=13000, |
295 |
ymax=12, |
|
296 |
ytick={0,5,10}, |
|
291
201c2c6d8696
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
268
diff
changeset
|
297 |
scaled ticks=false, |
201c2c6d8696
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
268
diff
changeset
|
298 |
axis lines=left, |
415 | 299 |
width=7cm, |
300 |
height=4.5cm, |
|
301 |
legend entries={Our Algorithm V1, Our Algorithm V2}, |
|
302 |
legend pos=outer north east] |
|
303 |
\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
|
304 |
\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
|
305 |
\end{axis} |
242
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
306 |
\end{tikzpicture} |
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
307 |
\end{center} |
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
308 |
|
415 | 309 |
\noindent And in the case of the regular expression $\texttt{(a*)*\,b}$ |
310 |
and strings of \texttt{a}s we will beat Java by factor of |
|
311 |
approximately 1,000,000 (note the scale on the $x$-axis). |
|
312 |
||
313 |
\begin{center} |
|
314 |
\begin{tikzpicture} |
|
315 |
\begin{axis}[ |
|
316 |
title={Graph: $\texttt{(a*)*\,b}$ and strings |
|
317 |
$\underbrace{\texttt{a}\ldots \texttt{a}}_{n}$}, |
|
318 |
xlabel={$n$}, |
|
319 |
x label style={at={(1.05,0.0)}}, |
|
320 |
ylabel={time in secs}, |
|
321 |
enlargelimits=false, |
|
322 |
ymax=12, |
|
323 |
ytick={0,5,10}, |
|
324 |
axis lines=left, |
|
325 |
width=7cm, |
|
326 |
height=4.5cm, |
|
327 |
legend entries={Our Algorithm V2}, |
|
328 |
legend pos=outer north east] |
|
329 |
\addplot[black,mark=square*,mark options={fill=white}] table {re3a.data}; |
|
330 |
\end{axis} |
|
331 |
\end{tikzpicture} |
|
332 |
\end{center} |
|
333 |
||
242
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
334 |
\subsection*{Basic Regular Expressions} |
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
335 |
|
399
5c1fbb39c93e
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
398
diff
changeset
|
336 |
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
|
337 |
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
|
338 |
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
|
339 |
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
|
340 |
\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
|
341 |
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
|
342 |
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
|
343 |
(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
|
344 |
grammar: |
242
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
345 |
|
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
346 |
\begin{center} |
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
347 |
\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
|
348 |
$r$ & $::=$ & $\ZERO$ & null language\\ |
5c1fbb39c93e
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
398
diff
changeset
|
349 |
& $\mid$ & $\ONE$ & empty string / \texttt{""} / []\\ |
242
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
350 |
& $\mid$ & $c$ & single character\\ |
243
8d5aaf5b0031
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
242
diff
changeset
|
351 |
& $\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
|
352 |
& $\mid$ & $r_1 \cdot r_2$ & sequence\\ |
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
353 |
& $\mid$ & $r^*$ & star (zero or more)\\ |
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
354 |
\end{tabular} |
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
355 |
\end{center} |
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
356 |
|
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
357 |
\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
|
358 |
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
|
359 |
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
|
360 |
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
|
361 |
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
|
362 |
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
|
363 |
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
|
364 |
$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
|
365 |
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
|
366 |
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
|
367 |
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
|
368 |
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
|
369 |
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
|
370 |
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
|
371 |
$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
|
372 |
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
|
373 |
|
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
374 |
\[ |
399
5c1fbb39c93e
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
398
diff
changeset
|
375 |
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
|
376 |
\] |
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
377 |
|
334
fd89a63e9db3
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
332
diff
changeset
|
378 |
\noindent |
fd89a63e9db3
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
332
diff
changeset
|
379 |
Note that this expands to |
fd89a63e9db3
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
332
diff
changeset
|
380 |
|
fd89a63e9db3
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
332
diff
changeset
|
381 |
\[ |
399
5c1fbb39c93e
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
398
diff
changeset
|
382 |
A\star \dn A^0 \cup A^1 \cup A^2 \cup A^3 \cup A^4 \cup \ldots |
334
fd89a63e9db3
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
332
diff
changeset
|
383 |
\] |
fd89a63e9db3
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
332
diff
changeset
|
384 |
|
fd89a63e9db3
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
332
diff
changeset
|
385 |
\noindent which is equivalent to |
fd89a63e9db3
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
332
diff
changeset
|
386 |
|
fd89a63e9db3
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
332
diff
changeset
|
387 |
\[ |
399
5c1fbb39c93e
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
398
diff
changeset
|
388 |
A\star \dn \{[]\} \cup A \cup A@A \cup A@A@A \cup A@A@A@A \cup \ldots |
334
fd89a63e9db3
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
332
diff
changeset
|
389 |
\] |
fd89a63e9db3
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
332
diff
changeset
|
390 |
|
fd89a63e9db3
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
332
diff
changeset
|
391 |
\noindent |
fd89a63e9db3
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
332
diff
changeset
|
392 |
Remember that $A^0$ is always the set containing the empty |
fd89a63e9db3
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
332
diff
changeset
|
393 |
string. |
fd89a63e9db3
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
332
diff
changeset
|
394 |
|
242
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
395 |
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
|
396 |
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
|
397 |
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
|
398 |
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
|
399 |
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
|
400 |
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
|
401 |
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
|
402 |
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
|
403 |
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
|
404 |
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
|
405 |
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
|
406 |
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
|
407 |
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
|
408 |
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
|
409 |
\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
|
410 |
clear shortly. |
5c1fbb39c93e
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
398
diff
changeset
|
411 |
|
5c1fbb39c93e
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
398
diff
changeset
|
412 |
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
|
413 |
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
|
414 |
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
|
415 |
$\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
|
416 |
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
|
417 |
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
|
418 |
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
|
419 |
in \eqref{email} would look like |
242
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
420 |
|
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
421 |
\[ |
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
422 |
\texttt{[...]+} \;\cdot\; \texttt{@} \;\cdot\; |
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
423 |
\texttt{[...]+} \;\cdot\; \texttt{.} \;\cdot\; |
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
424 |
\texttt{[...]\{2,6\}} |
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
425 |
\] |
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
426 |
|
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
427 |
\noindent |
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
428 |
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
|
429 |
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
|
430 |
should write |
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 |
\[ |
248
ce767ca23244
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
245
diff
changeset
|
433 |
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
|
434 |
\] |
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
435 |
|
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
436 |
\noindent |
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
437 |
but often just write {\it hello}. |
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
438 |
|
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
439 |
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
|
440 |
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
|
441 |
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
|
442 |
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
|
443 |
|
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
444 |
\begin{center} |
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
445 |
\begin{tabular}{rcl} |
399
5c1fbb39c93e
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
398
diff
changeset
|
446 |
$\ZERO$ & $\mapsto$ & \texttt{ZERO}\\ |
5c1fbb39c93e
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
398
diff
changeset
|
447 |
$\ONE$ & $\mapsto$ & \texttt{ONE}\\ |
242
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
448 |
$c$ & $\mapsto$ & \texttt{CHAR(c)}\\ |
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
449 |
$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
|
450 |
$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
|
451 |
$r^*$ & $\mapsto$ & \texttt{STAR(r)} |
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
452 |
\end{tabular} |
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
453 |
\end{center} |
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
454 |
|
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
455 |
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
|
456 |
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
|
457 |
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
|
458 |
\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
|
459 |
``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
|
460 |
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
|
461 |
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
|
462 |
|
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
463 |
\begin{center} |
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
464 |
\begin{tabular}{rcl} |
243
8d5aaf5b0031
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
242
diff
changeset
|
465 |
$r+$ & $\mapsto$ & $r\cdot r^*$\\ |
399
5c1fbb39c93e
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
398
diff
changeset
|
466 |
$r?$ & $\mapsto$ & $\ONE + r$\\ |
242
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
467 |
$\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
|
468 |
$[\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
|
469 |
\end{tabular} |
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
470 |
\end{center} |
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
471 |
|
243
8d5aaf5b0031
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
242
diff
changeset
|
472 |
|
242
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
473 |
\subsection*{The Meaning of Regular Expressions} |
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
474 |
|
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
475 |
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
|
476 |
\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
|
477 |
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
|
478 |
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
|
479 |
|
243
8d5aaf5b0031
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
242
diff
changeset
|
480 |
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
|
481 |
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
|
482 |
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
|
483 |
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
|
484 |
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
|
485 |
about basic mathematical notations. |
242
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
486 |
|
243
8d5aaf5b0031
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
242
diff
changeset
|
487 |
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
|
488 |
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
|
489 |
is defined as follows |
242
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
490 |
|
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
491 |
\begin{center} |
399
5c1fbb39c93e
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
398
diff
changeset
|
492 |
\begin{tabular}{rcll} |
5c1fbb39c93e
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
398
diff
changeset
|
493 |
$L(\ZERO)$ & $\dn$ & $\{\}$\\ |
5c1fbb39c93e
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
398
diff
changeset
|
494 |
$L(\ONE)$ & $\dn$ & $\{[]\}$\\ |
5c1fbb39c93e
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
398
diff
changeset
|
495 |
$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
|
496 |
$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
|
497 |
$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
|
498 |
$L(r^*)$ & $\dn$ & $(L(r))\star$\\ |
242
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
499 |
\end{tabular} |
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
500 |
\end{center} |
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
501 |
|
243
8d5aaf5b0031
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
242
diff
changeset
|
502 |
\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
|
503 |
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
|
504 |
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
|
505 |
|
8d5aaf5b0031
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
242
diff
changeset
|
506 |
\[ |
248
ce767ca23244
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
245
diff
changeset
|
507 |
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
|
508 |
\] |
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 |
\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
|
511 |
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
|
512 |
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
|
513 |
|
8d5aaf5b0031
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
242
diff
changeset
|
514 |
\[ |
8d5aaf5b0031
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
242
diff
changeset
|
515 |
L(a + b) = \{"a", "b"\} |
8d5aaf5b0031
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
242
diff
changeset
|
516 |
\] |
8d5aaf5b0031
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
242
diff
changeset
|
517 |
|
8d5aaf5b0031
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
242
diff
changeset
|
518 |
\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
|
519 |
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
|
520 |
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
|
521 |
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
|
522 |
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
|
523 |
have the same meaning: |
243
8d5aaf5b0031
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
242
diff
changeset
|
524 |
|
8d5aaf5b0031
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
242
diff
changeset
|
525 |
\begin{eqnarray*} |
8d5aaf5b0031
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
242
diff
changeset
|
526 |
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
|
527 |
& = & 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
|
528 |
& = & 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
|
529 |
& = & L(r_1 + (r_2 + r_3)) |
8d5aaf5b0031
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
242
diff
changeset
|
530 |
\end{eqnarray*} |
8d5aaf5b0031
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
242
diff
changeset
|
531 |
|
8d5aaf5b0031
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
242
diff
changeset
|
532 |
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
|
533 |
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
|
534 |
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
|
535 |
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
|
536 |
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
|
537 |
\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
|
538 |
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
|
539 |
|
8d5aaf5b0031
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
242
diff
changeset
|
540 |
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
|
541 |
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
|
542 |
different regular expressions that can recognise these |
8d5aaf5b0031
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
242
diff
changeset
|
543 |
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
|
544 |
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
|
545 |
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
|
546 |
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
|
547 |
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
|
548 |
\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
|
549 |
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
|
550 |
\defn{equivalent regular expressions}: |
8d5aaf5b0031
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
242
diff
changeset
|
551 |
|
8d5aaf5b0031
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
242
diff
changeset
|
552 |
\[ |
8d5aaf5b0031
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
242
diff
changeset
|
553 |
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
|
554 |
\] |
8d5aaf5b0031
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
242
diff
changeset
|
555 |
|
248
ce767ca23244
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
245
diff
changeset
|
556 |
\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
|
557 |
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
|
558 |
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
|
559 |
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
|
560 |
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
|
561 |
whether |
243
8d5aaf5b0031
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
242
diff
changeset
|
562 |
|
8d5aaf5b0031
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
242
diff
changeset
|
563 |
\[ |
399
5c1fbb39c93e
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
398
diff
changeset
|
564 |
\ZERO^* \equiv \ONE^* |
243
8d5aaf5b0031
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
242
diff
changeset
|
565 |
\] |
8d5aaf5b0031
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
242
diff
changeset
|
566 |
|
399
5c1fbb39c93e
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
398
diff
changeset
|
567 |
\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
|
568 |
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
|
569 |
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
|
570 |
up the calculations. |
243
8d5aaf5b0031
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
242
diff
changeset
|
571 |
|
8d5aaf5b0031
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
242
diff
changeset
|
572 |
\subsection*{My Fascination for Regular Expressions} |
242
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
573 |
|
243
8d5aaf5b0031
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
242
diff
changeset
|
574 |
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
|
575 |
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
|
576 |
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
|
577 |
found out about them. I even have the vague recollection that |
8d5aaf5b0031
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
242
diff
changeset
|
578 |
I did not quite understand them during my study. If I remember |
8d5aaf5b0031
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
242
diff
changeset
|
579 |
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
|
580 |
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
|
581 |
$\epsilon$) and the empty string.\footnote{Obviously the |
5c1fbb39c93e
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
398
diff
changeset
|
582 |
lecturer must have been bad.} Since my study, I have used |
5c1fbb39c93e
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
398
diff
changeset
|
583 |
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
|
584 |
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
|
585 |
languages and compilers, which invariably need regular |
5c1fbb39c93e
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
398
diff
changeset
|
586 |
expression in some form or shape. |
243
8d5aaf5b0031
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
242
diff
changeset
|
587 |
|
399
5c1fbb39c93e
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
398
diff
changeset
|
588 |
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
|
589 |
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
|
590 |
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
|
591 |
core developer of one of |
8d5aaf5b0031
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
242
diff
changeset
|
592 |
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
|
593 |
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
|
594 |
mathematical concepts, but also about programs. In this way |
8d5aaf5b0031
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
242
diff
changeset
|
595 |
they can help with writing bug-free code. Theorem provers have |
8d5aaf5b0031
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
242
diff
changeset
|
596 |
proved already their value in a number of systems (even in |
8d5aaf5b0031
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
242
diff
changeset
|
597 |
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
|
598 |
to use by average programmers. |
8d5aaf5b0031
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
242
diff
changeset
|
599 |
|
8d5aaf5b0031
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
242
diff
changeset
|
600 |
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
|
601 |
\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
|
602 |
one to do almost all calculations in regular language theory |
8d5aaf5b0031
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
242
diff
changeset
|
603 |
on the level of regular expressions, not needing any automata. |
8d5aaf5b0031
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
242
diff
changeset
|
604 |
This is important because automata are graphs and it is rather |
8d5aaf5b0031
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
242
diff
changeset
|
605 |
difficult to reason about graphs in theorem provers. In |
8d5aaf5b0031
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
242
diff
changeset
|
606 |
contrast, to reason about regular expressions is easy-peasy in |
8d5aaf5b0031
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
242
diff
changeset
|
607 |
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
|
608 |
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
|
609 |
expression matchers are |
8d5aaf5b0031
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
242
diff
changeset
|
610 |
buggy.\footnote{\url{http://www.haskell.org/haskellwiki/Regex_Posix}} |
8d5aaf5b0031
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
242
diff
changeset
|
611 |
With my PhD student Fahad Ausaf I am currently working on |
248
ce767ca23244
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
245
diff
changeset
|
612 |
proving 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
|
613 |
proposed by Sulzmann and Lu in |
8d5aaf5b0031
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
242
diff
changeset
|
614 |
2014.\footnote{\url{http://goo.gl/bz0eHp}} This would be an |
8d5aaf5b0031
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
242
diff
changeset
|
615 |
attractive results since we will be able to prove that the |
8d5aaf5b0031
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
242
diff
changeset
|
616 |
algorithm is really correct, but also that the machine code(!) |
8d5aaf5b0031
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
242
diff
changeset
|
617 |
that implements this code efficiently is correct. Writing |
8d5aaf5b0031
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
242
diff
changeset
|
618 |
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
|
619 |
errors or bugs. How nice! |
8d5aaf5b0031
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
242
diff
changeset
|
620 |
|
8d5aaf5b0031
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
242
diff
changeset
|
621 |
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
|
622 |
is that we could indeed find out new things about them that |
8d5aaf5b0031
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
242
diff
changeset
|
623 |
have surprised some experts in the field of regular |
8d5aaf5b0031
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
242
diff
changeset
|
624 |
expressions. Together with two colleagues from China, I was |
8d5aaf5b0031
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
242
diff
changeset
|
625 |
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
|
626 |
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
|
627 |
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
|
628 |
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
|
629 |
complementation, something which Gasarch in his |
8d5aaf5b0031
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
242
diff
changeset
|
630 |
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
|
631 |
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
|
632 |
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
|
633 |
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
|
634 |
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
|
635 |
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
|
636 |
|
8d5aaf5b0031
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
242
diff
changeset
|
637 |
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
|
638 |
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
|
639 |
beautiful mathematical theory behind them, which can be |
5c1fbb39c93e
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
398
diff
changeset
|
640 |
sometimes quite deep and contain hidden snares. They have |
5c1fbb39c93e
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
398
diff
changeset
|
641 |
practical importance (remember the shocking runtime of the |
5c1fbb39c93e
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
398
diff
changeset
|
642 |
regular expression matchers in Python and Ruby in some |
5c1fbb39c93e
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
398
diff
changeset
|
643 |
instances). People who are not very familiar with the |
5c1fbb39c93e
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
398
diff
changeset
|
644 |
mathematical background of regular expressions get them |
5c1fbb39c93e
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
398
diff
changeset
|
645 |
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
|
646 |
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
|
647 |
satisfy their specification and that the corresponding |
5c1fbb39c93e
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
398
diff
changeset
|
648 |
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
|
649 |
yet quite there. |
242
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
650 |
|
332
4755ad4b457b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
327
diff
changeset
|
651 |
Notwithstanding my fascination, I am also happy to admit that regular |
244
771042ac7c3f
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
243
diff
changeset
|
652 |
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
|
653 |
``theoretical'' shortcomings, for example recognising strings |
244
771042ac7c3f
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
243
diff
changeset
|
654 |
of the form $a^{n}b^{n}$. I am not so bothered by them. What I |
771042ac7c3f
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
243
diff
changeset
|
655 |
am bothered about is when regular expressions are in the way |
771042ac7c3f
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
243
diff
changeset
|
656 |
of practical programming. For example, it turns out that the |
771042ac7c3f
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
243
diff
changeset
|
657 |
regular expression for email addresses shown in \eqref{email} |
771042ac7c3f
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
243
diff
changeset
|
658 |
is hopelessly inadequate for recognising all of them (despite |
771042ac7c3f
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
243
diff
changeset
|
659 |
being touted as something every computer scientist should know |
771042ac7c3f
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
243
diff
changeset
|
660 |
about). The W3 Consortium (which standardises the Web) |
771042ac7c3f
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
243
diff
changeset
|
661 |
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
|
662 |
regular expressions for email addresses: |
244
771042ac7c3f
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
243
diff
changeset
|
663 |
|
771042ac7c3f
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
243
diff
changeset
|
664 |
{\small\begin{lstlisting}[language={},keywordstyle=\color{black},numbers=none] |
771042ac7c3f
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
243
diff
changeset
|
665 |
[a-zA-Z0-9.!#$%&'*+/=?^_`{|}~-]+@[a-zA-Z0-9-]+(?:\.[a-zA-Z0-9-]+)* |
771042ac7c3f
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
243
diff
changeset
|
666 |
\end{lstlisting}} |
771042ac7c3f
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
243
diff
changeset
|
667 |
|
771042ac7c3f
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
243
diff
changeset
|
668 |
\noindent But they admit that by using this regular expression |
771042ac7c3f
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
243
diff
changeset
|
669 |
they wilfully violate the RFC 5322 standard which specifies |
771042ac7c3f
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
243
diff
changeset
|
670 |
the syntax of email addresses. With their proposed regular |
771042ac7c3f
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
243
diff
changeset
|
671 |
expression they are too strict in some cases and too lax in |
771042ac7c3f
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
243
diff
changeset
|
672 |
others. Not a good situation to be in. A regular expression |
771042ac7c3f
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
243
diff
changeset
|
673 |
that is claimed to be closer to the standard is shown in |
771042ac7c3f
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
243
diff
changeset
|
674 |
Figure~\ref{monster}. Whether this claim is true or not, I |
248
ce767ca23244
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
245
diff
changeset
|
675 |
would not know---the only thing I can say to this regular |
ce767ca23244
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
245
diff
changeset
|
676 |
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
|
677 |
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
|
678 |
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
|
679 |
|
5c1fbb39c93e
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
398
diff
changeset
|
680 |
\begin{center} |
5c1fbb39c93e
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
398
diff
changeset
|
681 |
\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
|
682 |
\end{center} |
5c1fbb39c93e
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
398
diff
changeset
|
683 |
|
5c1fbb39c93e
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
398
diff
changeset
|
684 |
|
5c1fbb39c93e
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
398
diff
changeset
|
685 |
\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
|
686 |
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
|
687 |
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
|
688 |
expressions. |
244
771042ac7c3f
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
243
diff
changeset
|
689 |
|
771042ac7c3f
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
243
diff
changeset
|
690 |
|
242
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
691 |
\begin{figure}[p] |
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
692 |
\lstinputlisting{../progs/crawler1.scala} |
399
5c1fbb39c93e
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
398
diff
changeset
|
693 |
|
242
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
694 |
\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
|
695 |
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
|
696 |
\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
|
697 |
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
|
698 |
\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
|
699 |
|
242
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
700 |
\end{figure} |
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 |
|
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
703 |
\begin{figure}[p] |
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
704 |
\lstinputlisting{../progs/crawler2.scala} |
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
705 |
|
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
706 |
\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
|
707 |
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
|
708 |
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
|
709 |
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
|
710 |
main change is in |
5c1fbb39c93e
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
398
diff
changeset
|
711 |
Lines~\ref{changestartline}--\ref{changeendline} where there |
5c1fbb39c93e
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
398
diff
changeset
|
712 |
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
|
713 |
not.\label{crawler2}} |
242
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
714 |
|
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
715 |
\end{figure} |
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
716 |
|
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
717 |
\begin{figure}[p] |
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
718 |
\lstinputlisting{../progs/crawler3.scala} |
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
719 |
|
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
720 |
\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
|
721 |
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
|
722 |
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
|
723 |
\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
|
724 |
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
|
725 |
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
|
726 |
|
242
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
727 |
\end{figure} |
35104ee14f87
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
237
diff
changeset
|
728 |
|
244
771042ac7c3f
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
243
diff
changeset
|
729 |
\begin{figure}[p] |
771042ac7c3f
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
243
diff
changeset
|
730 |
\tiny |
771042ac7c3f
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
243
diff
changeset
|
731 |
\begin{center} |
771042ac7c3f
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
243
diff
changeset
|
732 |
\begin{minipage}{0.8\textwidth} |
771042ac7c3f
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
243
diff
changeset
|
733 |
\lstinputlisting[language={},keywordstyle=\color{black},numbers=none]{../progs/email-rexp} |
771042ac7c3f
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
243
diff
changeset
|
734 |
\end{minipage} |
771042ac7c3f
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
243
diff
changeset
|
735 |
\end{center} |
771042ac7c3f
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
243
diff
changeset
|
736 |
|
404
245d302791c7
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
403
diff
changeset
|
737 |
\caption{Nothing that can be said about this regular |
245d302791c7
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
403
diff
changeset
|
738 |
expression\ldots\label{monster}} |
244
771042ac7c3f
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
243
diff
changeset
|
739 |
\end{figure} |
108
52ee218151f9
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
107
diff
changeset
|
740 |
|
112
95ee5cc5c05d
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
111
diff
changeset
|
741 |
|
105
397ecdafefd8
added handouts
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
742 |
\end{document} |
397ecdafefd8
added handouts
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
743 |
|
397ecdafefd8
added handouts
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
744 |
%%% Local Variables: |
397ecdafefd8
added handouts
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
745 |
%%% mode: latex |
397ecdafefd8
added handouts
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
746 |
%%% TeX-master: t |
397ecdafefd8
added handouts
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
747 |
%%% End: |