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