94
+ − 1
\documentclass[a4paper,UKenglish]{lipics}
+ − 2
\usepackage{graphic}
+ − 3
\usepackage{data}
+ − 4
\usepackage{tikz-cd}
+ − 5
%\usepackage{algorithm}
+ − 6
\usepackage{amsmath}
+ − 7
\usepackage[noend]{algpseudocode}
+ − 8
\usepackage{enumitem}
+ − 9
\usepackage{nccmath}
+ − 10
+ − 11
\definecolor{darkblue}{rgb}{0,0,0.6}
+ − 12
\hypersetup{colorlinks=true,allcolors=darkblue}
+ − 13
\newcommand{\comment}[1]%
+ − 14
{{\color{red}$\Rightarrow$}\marginpar{\raggedright\small{\bf\color{red}#1}}}
+ − 15
+ − 16
% \documentclass{article}
+ − 17
%\usepackage[utf8]{inputenc}
+ − 18
%\usepackage[english]{babel}
+ − 19
%\usepackage{listings}
+ − 20
% \usepackage{amsthm}
+ − 21
%\usepackage{hyperref}
+ − 22
% \usepackage[margin=0.5in]{geometry}
+ − 23
%\usepackage{pmboxdraw}
+ − 24
+ − 25
\title{POSIX Regular Expression Matching and Lexing}
+ − 26
\author{Chengsong Tan}
+ − 27
\affil{King's College London\\
+ − 28
London, UK\\
+ − 29
\texttt{chengsong.tan@kcl.ac.uk}}
+ − 30
\authorrunning{Chengsong Tan}
+ − 31
\Copyright{Chengsong Tan}
+ − 32
+ − 33
\newcommand{\dn}{\stackrel{\mbox{\scriptsize def}}{=}}%
+ − 34
\newcommand{\ZERO}{\mbox{\bf 0}}
+ − 35
\newcommand{\ONE}{\mbox{\bf 1}}
101
+ − 36
\def\erase{\textit{erase}}
94
+ − 37
\def\bders{\textit{bders}}
+ − 38
\def\lexer{\mathit{lexer}}
+ − 39
\def\blexer{\textit{blexer}}
+ − 40
\def\blexers{\mathit{blexer\_simp}}
95
+ − 41
\def\simp{\mathit{simp}}
94
+ − 42
\def\mkeps{\mathit{mkeps}}
+ − 43
\def\bmkeps{\textit{bmkeps}}
+ − 44
\def\inj{\mathit{inj}}
+ − 45
\def\Empty{\mathit{Empty}}
+ − 46
\def\Left{\mathit{Left}}
+ − 47
\def\Right{\mathit{Right}}
+ − 48
\def\Stars{\mathit{Stars}}
+ − 49
\def\Char{\mathit{Char}}
+ − 50
\def\Seq{\mathit{Seq}}
+ − 51
\def\Der{\mathit{Der}}
+ − 52
\def\nullable{\mathit{nullable}}
+ − 53
\def\Z{\mathit{Z}}
+ − 54
\def\S{\mathit{S}}
+ − 55
\def\flex{\textit{flex}}
+ − 56
\def\rup{r^\uparrow}
+ − 57
\def\retrieve{\textit{retrieve}}
+ − 58
\def\AALTS{\textit{AALTS}}
+ − 59
\def\AONE{\textit{AONE}}
+ − 60
%\theoremstyle{theorem}
+ − 61
%\newtheorem{theorem}{Theorem}
+ − 62
%\theoremstyle{lemma}
+ − 63
%\newtheorem{lemma}{Lemma}
+ − 64
%\newcommand{\lemmaautorefname}{Lemma}
+ − 65
%\theoremstyle{definition}
+ − 66
%\newtheorem{definition}{Definition}
+ − 67
\algnewcommand\algorithmicswitch{\textbf{switch}}
+ − 68
\algnewcommand\algorithmiccase{\textbf{case}}
+ − 69
\algnewcommand\algorithmicassert{\texttt{assert}}
+ − 70
\algnewcommand\Assert[1]{\State \algorithmicassert(#1)}%
+ − 71
% New "environments"
+ − 72
\algdef{SE}[SWITCH]{Switch}{EndSwitch}[1]{\algorithmicswitch\ #1\ \algorithmicdo}{\algorithmicend\ \algorithmicswitch}%
+ − 73
\algdef{SE}[CASE]{Case}{EndCase}[1]{\algorithmiccase\ #1}{\algorithmicend\ \algorithmiccase}%
+ − 74
\algtext*{EndSwitch}%
+ − 75
\algtext*{EndCase}%
+ − 76
+ − 77
+ − 78
\begin{document}
+ − 79
+ − 80
\maketitle
+ − 81
+ − 82
\begin{abstract}
+ − 83
Brzozowski introduced in 1964 a beautifully simple algorithm for
+ − 84
regular expression matching based on the notion of derivatives of
+ − 85
regular expressions. In 2014, Sulzmann and Lu extended this
+ − 86
algorithm to not just give a YES/NO answer for whether or not a
+ − 87
regular expression matches a string, but in case it does also
+ − 88
answers with \emph{how} it matches the string. This is important for
+ − 89
applications such as lexing (tokenising a string). The problem is to
+ − 90
make the algorithm by Sulzmann and Lu fast on all inputs without
100
+ − 91
breaking its correctness. Being fast depends on a complete set of
+ − 92
simplification rules, some of which
+ − 93
have been put forward by Sulzmann and Lu. We have extended their
105
+ − 94
rules in order to obtain a tight bound on the size of regular expressions.
+ − 95
We have tested these extended rules, but have not
+ − 96
formally established their correctness. We have also not yet looked
100
+ − 97
at extended regular expressions, such as bounded repetitions,
94
+ − 98
negation and back-references.
+ − 99
\end{abstract}
+ − 100
+ − 101
\section{Introduction}
+ − 102
105
+ − 103
While we believe derivatives of regular expressions is a beautiful
+ − 104
concept (in terms of ease of implementing them in functional
+ − 105
programming languages and in terms of reasoning about them formally),
+ − 106
they have one major drawback: every derivative step can make regular
+ − 107
expressions grow drastically in size. This in turn has negative effect
+ − 108
on the runtime of the corresponding lexing algorithms. Consider for
+ − 109
example the regular expression $(a+aa)^*$ and the short string
+ − 110
$aaaaaaaaaaaa$. The corresponding derivative is already 8668 nodes
+ − 111
assuming the derivative is seen as a tree. The reason for the poor
+ − 112
runtime of the lexing algorithms is that they need to traverse such
+ − 113
trees over and over again. The solution is to find a complete set of
+ − 114
simplification rules that keep the sizes of derivatives uniformly
+ − 115
small.
94
+ − 116
105
+ − 117
For reasons beyond this report, it turns out that a complete set of
+ − 118
simplification rules depends on values being encoded as
+ − 119
bitsequences.\footnote{Values are the results the lexing algorithms
+ − 120
generate; they encode how a regular expression matched a string.} We
+ − 121
already know that the lexing algorithm using bitsequences but
+ − 122
\emph{without} simplification is correct, albeilt horribly
+ − 123
slow. Therefore in the past 6 months we were trying to prove that the
+ − 124
algorithm using bitsequences plus our simplification rules is
+ − 125
correct. Formally this amounts to show that
100
+ − 126
+ − 127
\begin{equation}\label{mainthm}
+ − 128
\blexers \; r \; s = \blexer \;r\;s
+ − 129
\end{equation}
+ − 130
94
+ − 131
\noindent
105
+ − 132
whereby $\blexers$ simplifies (makes derivatives smaller) in each
+ − 133
step, whereas with $\blexer$ the size can grow exponentially. This
+ − 134
would be an important milestone for the thesis, because we already
+ − 135
have a very good idea how to establish that our set our simplification
+ − 136
rules keeps the size of derivativs below a relatively tight bound.
100
+ − 137
105
+ − 138
In order to prove the main theorem in \eqref{mainthm}, we need to prove the
100
+ − 139
two functions produce the same output. The definition of these functions
+ − 140
is shown below.
+ − 141
94
+ − 142
\begin{center}
+ − 143
\begin{tabular}{lcl}
+ − 144
$\textit{blexer}\;r\,s$ & $\dn$ &
+ − 145
$\textit{let}\;a = (r^\uparrow)\backslash s\;\textit{in}$\\
+ − 146
& & $\;\;\textit{if}\; \textit{bnullable}(a)$\\
+ − 147
& & $\;\;\textit{then}\;\textit{decode}\,(\textit{bmkeps}\,a)\,r$\\
+ − 148
& & $\;\;\textit{else}\;\textit{None}$
+ − 149
\end{tabular}
+ − 150
\end{center}
+ − 151
100
+ − 152
\begin{center}
94
+ − 153
\begin{tabular}{lcl}
100
+ − 154
$\blexers \; r \, s$ &$\dn$ &
+ − 155
$\textit{let} \; a = (r^\uparrow)\backslash_{simp}\, s\; \textit{in}$\\
+ − 156
& & $\; \; \textit{if} \; \textit{bnullable}(a)$\\
+ − 157
& & $\; \; \textit{then} \; \textit{decode}\,(\textit{bmkeps}\,a)\,r$\\
+ − 158
& & $\;\; \textit{else}\;\textit{None}$
94
+ − 159
\end{tabular}
+ − 160
\end{center}
+ − 161
\noindent
105
+ − 162
In these definitions $(r^\uparrow)$ is a kind of coding function that
+ − 163
is the same in each case, similarly the decode and the \textit{bmkeps}
+ − 164
are functions that are the same in each case. Our main theorem
+ − 165
\eqref{mainthm} therefore boils down to proving the following two
+ − 166
propositions (depending on which branch the if-else clause takes). It
+ − 167
establishes how the derivatives \emph{with} simplification do not
+ − 168
change the computed result:
94
+ − 169
+ − 170
\begin{itemize}
105
+ − 171
\item{(a)} If a string $s$ is in the language of $L(r)$, then \\
100
+ − 172
$\textit{bmkeps} (r^\uparrow)\backslash_{simp}\,s = \textit{bmkeps} (r^\uparrow)\backslash s$,\\
105
+ − 173
\item{(b)} If a string $s$ is in the language $L(r)$, then
100
+ − 174
$\rup \backslash_{simp} \,s$ is not nullable.
94
+ − 175
\end{itemize}
100
+ − 176
94
+ − 177
\noindent
105
+ − 178
We have already proved in Isabelle the second part. This is actually
+ − 179
not too difficult because we can show that simplification does not
+ − 180
change the language of simplified regular expressions.
100
+ − 181
105
+ − 182
If we can prove the first part, that is the bitsequence algorithm with
+ − 183
simplification produces the same result as the one without
+ − 184
simplification, then we are done. Unfortunately that part requires
+ − 185
more effort, because simplification does not only need to \emph{not}
+ − 186
change the language, but also not change the value (that is the
+ − 187
computed result).
+ − 188
+ − 189
%\bigskip\noindent\rule[1.5ex]{\linewidth}{5pt}
+ − 190
%Do you want to keep this? You essentially want to say that the old
+ − 191
%method used retrieve, which unfortunately cannot be adopted to
+ − 192
%the simplification rules. You could just say that and give an example.
+ − 193
%However you have to think about how you give the example....nobody knows
+ − 194
%about AZERO etc yet. Maybe it might be better to use normal regexes
+ − 195
%like $a + aa$, but annotate bitsequences as subscript like $_1(_0a + _1aa)$.
100
+ − 196
105
+ − 197
%\bigskip\noindent\rule[1.5ex]{\linewidth}{5pt}
+ − 198
%REPLY:\\
+ − 199
%Yes, I am essentially saying that the old method
+ − 200
%cannot be adopted without adjustments.
+ − 201
%But this does not mean we should skip
+ − 202
%the proof of the bit-coded algorithm
+ − 203
%as it is still the main direction we are looking into
+ − 204
%to prove things. We are trying to modify
+ − 205
%the old proof to suit our needs, but not give
+ − 206
%up it totally, that is why i believe the old
+ − 207
%proof is fundamental in understanding
+ − 208
%what we are doing in the past 6 months.
+ − 209
%\bigskip\noindent\rule[1.5ex]{\linewidth}{5pt}
100
+ − 210
105
+ − 211
For this we have started with looking at the original proof that
+ − 212
established that the bitsequence algorrithm produces the same result
+ − 213
as the algorithm not using bitsequences. Formally this proof
+ − 214
established
+ − 215
+ − 216
\begin{equation}\label{lexer}
+ − 217
\blexer \; (r^\uparrow) s = \lexer \;r \;s
+ − 218
\end{equation}
+ − 219
+ − 220
%\noindent
+ − 221
%might provide us insight into proving
+ − 222
%\begin{center}
+ − 223
%$\blexer \; r^\uparrow \;s = \blexers \; r^\uparrow \;s$
+ − 224
%\end{center}
+ − 225
94
+ − 226
\noindent
105
+ − 227
This proof used two ``tricks''. One is that it defined a \flex-function
+ − 228
94
+ − 229
\begin{center}
+ − 230
\begin{tabular}{lcl}
+ − 231
$\textit{flex} \;r\; f\; (c\!::\!s) $ & $\dn$ & $\textit{flex} \; (r\backslash c) \;(\lambda v. f (inj \; r \; c \; v)) \;s$ \\
+ − 232
$\textit{flex} \;r\; f\; [\,] $ & $\dn$ & $f$
+ − 233
\end{tabular}
+ − 234
\end{center}
105
+ − 235
94
+ − 236
\noindent
105
+ − 237
and then proved for the right-hand side in \eqref{lexer}
+ − 238
+ − 239
\begin{center}
+ − 240
$\lexer \;r\; s = \flex \;\textit{id} \; r\;s \;(\mkeps \; r\backslash s)$
+ − 241
\end{center}.
+ − 242
+ − 243
+ − 244
\noindent\rule[1.5ex]{\linewidth}{1pt}
+ − 245
+ − 246
\noindent
+ − 247
The $\flex$-function essentially does lexing by
+ − 248
stacking up injection functions while doing derivatives.
+ − 249
94
+ − 250
explicitly showing the order of characters being
+ − 251
injected back in each step.
+ − 252
With $\flex$ we can write $\lexer$ this way:
+ − 253
\begin{center}
+ − 254
$\lexer \;r\; s = \flex \;id \; r\;s \;(\mkeps r\backslash s)$
+ − 255
\end{center}
+ − 256
\noindent
+ − 257
$\flex$ focuses on
+ − 258
the injections instead
+ − 259
of the derivatives ,
+ − 260
compared
+ − 261
to the original definition of $\lexer$,
+ − 262
which puts equal amount of emphasis on
+ − 263
injection and derivative with respect to each character:
+ − 264
\begin{center}
+ − 265
\begin{tabular}{lcl}
+ − 266
$\textit{lexer} \; r\; (c\!::\!s) $ & $\dn$ & $\textit{case} \; \lexer \; (r\backslash c) \;s \; \textit{of}$ \\
+ − 267
& & $\textit{None} \; \Longrightarrow \; \textit{None}$\\
+ − 268
& & $\textbar \; v \; \Longrightarrow \; \inj \; r\;c\;v$\\
+ − 269
$\textit{lexer} \; r\; [\,] $ & $\dn$ & $\textit{if} \; \nullable (r) \; \textit{then} \; \mkeps (r) \; \textit{else} \;None$
+ − 270
\end{tabular}
+ − 271
\end{center}
+ − 272
\noindent
+ − 273
Using this feature of $\flex$ we can rewrite the lexing
+ − 274
$w.r.t \; s @ [c]$ in term of lexing
+ − 275
$w.r.t \; s$:
+ − 276
\begin{center}
+ − 277
$\flex \; r \; id \; (s@[c]) \; v = \flex \; r \; id \; s \; (inj \; (r\backslash s) \; c\; v)$.
+ − 278
\end{center}
+ − 279
\noindent
+ − 280
this allows us to use
+ − 281
the inductive hypothesis to get
+ − 282
\begin{center}
+ − 283
$ \flex \; r\; id\; (s@[c])\; v = \textit{decode} \;( \textit{retrieve}\; (\rup \backslash s) \; (\inj \; (r\backslash s) \;c\;v)\;) r$
+ − 284
\end{center}
+ − 285
\noindent
+ − 286
By using a property of retrieve we have the $\textit{RHS}$ of the above equality is
+ − 287
$decode (retrieve (r^\uparrow \backslash(s @ [c])) v) r$, and this gives the
+ − 288
main lemma result:
+ − 289
\begin{center}
+ − 290
$ \flex \;r\; id \; (s@[c]) \; v =\textit{decode}(\textit{retrieve} (\rup \backslash (s@[c])) \;v) r$
+ − 291
\end{center}
+ − 292
\noindent
+ − 293
To use this lemma result for our
+ − 294
correctness proof, simply replace the $v$ in the
+ − 295
$\textit{RHS}$ of the above equality with
+ − 296
$\mkeps\;(r\backslash (s@[c]))$, and apply the lemma that
+ − 297
+ − 298
\begin{center}
+ − 299
$\textit{decode} \; \bmkeps \; \rup \; r = \textit{decode} \; (\textit{retrieve} \; \rup \; \mkeps(r)) \;r$
+ − 300
\end{center}
+ − 301
\noindent
+ − 302
We get the correctness of our bit-coded algorithm:
+ − 303
\begin{center}
+ − 304
$\flex \;r\; id \; s \; (\mkeps \; r\backslash s) = \textit{decode} \; \bmkeps \; \rup\backslash s \; r$
+ − 305
\end{center}
+ − 306
\noindent
+ − 307
The bridge between the above chain of equalities
+ − 308
is the use of $\retrieve$,
+ − 309
if we want to use a similar technique for the
+ − 310
simplified version of algorithm,
+ − 311
we face the problem that in the above
+ − 312
equalities,
+ − 313
$\retrieve \; a \; v$ is not always defined.
+ − 314
for example,
100
+ − 315
$\retrieve \; _0(_1a+_0a) \; \Left(\Empty)$
101
+ − 316
is defined, but not $\retrieve \; (_{01}a) \;\Left(\Empty)$,
94
+ − 317
though we can extract the same POSIX
+ − 318
bits from the two annotated regular expressions.
95
+ − 319
The latter might occur when we try to retrieve from
+ − 320
a simplified regular expression using the same value
+ − 321
as the unsimplified one.
+ − 322
This is because $\Left(\Empty)$ corresponds to
101
+ − 323
the regular expression structure $\ONE+r_2$ instead of
+ − 324
$\ONE$.
94
+ − 325
That means, if we
+ − 326
want to prove that
+ − 327
\begin{center}
+ − 328
$\textit{decode} \; \bmkeps \; \rup\backslash s \; r = \textit{decode} \; \bmkeps \; \rup\backslash_{simp} s \; r$
+ − 329
\end{center}
+ − 330
\noindent
+ − 331
holds by using $\retrieve$,
+ − 332
we probably need to prove an equality like below:
+ − 333
\begin{center}
+ − 334
%$\retrieve \; \rup\backslash_{simp} s \; \mkeps(r\backslash_{simp} s)=\textit{retrieve} \; \rup\backslash s \; \mkeps(r\backslash s)$
101
+ − 335
$\retrieve \; \rup\backslash_{simp} s \; \mkeps(f(r\backslash s))=\textit{retrieve} \; \rup\backslash s \; \mkeps(r\backslash s)$
94
+ − 336
\end{center}
+ − 337
\noindent
101
+ − 338
$f$ rectifies $r\backslash s$ so the value $\mkeps(f(r\backslash s))$ becomes
+ − 339
something simpler
94
+ − 340
to make the retrieve function defined.\\
95
+ − 341
One way to do this is to prove the following:
+ − 342
\begin{center}
+ − 343
$\retrieve \; \rup\backslash_{simp} s \; \mkeps(\simp(r\backslash s))=\textit{retrieve} \; \rup\backslash s \; \mkeps(r\backslash s)$
+ − 344
\end{center}
+ − 345
\noindent
101
+ − 346
The reason why we choose $\simp$ as $f$ is because
+ − 347
$\rup\backslash_{simp} \, s$ and $\simp(\rup\backslash \, s)$
+ − 348
have the same shape:
+ − 349
\begin{center}
+ − 350
$\erase (\rup\backslash_{simp} \, s) = \erase(\simp(\rup\backslash s))$
+ − 351
\end{center}
+ − 352
+ − 353
\noindent
+ − 354
$\erase$ in the above equality means to remove the bit-codes
+ − 355
in an annotated regular expression and only keep the original
+ − 356
regular expression(just like "erasing" the bits). Its definition is omitted.
+ − 357
$\rup\backslash_{simp} \, s$ and $\simp(\rup\backslash s)$
+ − 358
are very closely related, but not identical.
+ − 359
For example, let $r$ be the regular expression
+ − 360
$(a+b)(a+a*)$ and $s$ be the string $aa$, then
103
+ − 361
both $\erase (\rup\backslash_{simp} \, s)$ and $\erase (\simp (\rup\backslash s))$
+ − 362
are $\ONE + a^*$. However, without $\erase$
101
+ − 363
\begin{center}
+ − 364
$\rup\backslash_{simp} \, s$ is equal to $_0(_0\ONE +_{11}a^*)$
+ − 365
\end{center}
+ − 366
\noindent
+ − 367
whereas
+ − 368
\begin{center}
103
+ − 369
$\simp(\rup\backslash s)$ is equal to $(_{00}\ONE +_{011}a^*)$
101
+ − 370
\end{center}
+ − 371
\noindent
103
+ − 372
For the sake of visual simplicity, we use numbers to denote the bits
+ − 373
in bitcodes as we have previously defined for annotated
+ − 374
regular expressions. $\S$ is replaced by
+ − 375
subscript $_1$ and $\Z$ by $_0$.
+ − 376
101
+ − 377
Two "rules" might be inferred from the above example.
103
+ − 378
101
+ − 379
First, after erasing the bits the two regular expressions
+ − 380
are exactly the same: both become $1+a^*$. Here the
103
+ − 381
function $\simp$ exhibits the "one in the end equals many times
+ − 382
at the front"
101
+ − 383
property: one simplification in the end causes the
+ − 384
same regular expression structure as
103
+ − 385
successive simplifications done alongside derivatives.
+ − 386
$\rup\backslash_{simp} \, s$ unfolds to
+ − 387
$\simp((\simp(r\backslash a))\backslash a)$
+ − 388
and $\simp(\rup\backslash s)$ unfolds to
+ − 389
$\simp((r\backslash a)\backslash a)$. The one simplification
+ − 390
in the latter causes the resulting regular expression to
+ − 391
become $1+a^*$, exactly the same as the former with
+ − 392
two simplifications.
+ − 393
101
+ − 394
Second, the bit-codes are different, but they are essentially
+ − 395
the same: if we push the outmost bits ${\bf_0}(_0\ONE +_{11}a^*)$ of $\rup\backslash_{simp} \, s$
+ − 396
inside then we get $(_{00}\ONE +_{011}a^*)$, exactly the
+ − 397
same as that of $\rup\backslash \, s$. And this difference
+ − 398
does not matter when we try to apply $\bmkeps$ or $\retrieve$
103
+ − 399
to it. This seems a good news if we want to use $\retrieve$
+ − 400
to prove things.
+ − 401
+ − 402
If we look into the difference above, we could see that the
+ − 403
difference is not fundamental: the bits are just being moved
+ − 404
around in a way that does not hurt the correctness.
+ − 405
During the first derivative operation,
+ − 406
$\rup\backslash a=(_0\ONE + \ZERO)(_0a + _1a^*)$ is
+ − 407
in the form of a sequence regular expression with the first
+ − 408
part being nullable.
+ − 409
Recall the simplification function definition:
+ − 410
\begin{center}
+ − 411
\begin{tabular}{@{}lcl@{}}
+ − 412
+ − 413
$\textit{simp} \; (\textit{SEQ}\;bs\,a_1\,a_2)$ & $\dn$ & $ (\textit{simp} \; a_1, \textit{simp} \; a_2) \; \textit{match} $ \\
+ − 414
&&$\quad\textit{case} \; (\ZERO, \_) \Rightarrow \ZERO$ \\
+ − 415
&&$\quad\textit{case} \; (\_, \ZERO) \Rightarrow \ZERO$ \\
+ − 416
&&$\quad\textit{case} \; (\ONE, a_2') \Rightarrow \textit{fuse} \; bs \; a_2'$ \\
+ − 417
&&$\quad\textit{case} \; (a_1', \ONE) \Rightarrow \textit{fuse} \; bs \; a_1'$ \\
+ − 418
&&$\quad\textit{case} \; (a_1', a_2') \Rightarrow \textit{SEQ} \; bs \; a_1' \; a_2'$ \\
+ − 419
+ − 420
$\textit{simp} \; (\textit{ALTS}\;bs\,as)$ & $\dn$ & $\textit{distinct}( \textit{flatten} ( \textit{map simp as})) \; \textit{match} $ \\
+ − 421
&&$\quad\textit{case} \; [] \Rightarrow \ZERO$ \\
+ − 422
&&$\quad\textit{case} \; a :: [] \Rightarrow \textit{fuse bs a}$ \\
+ − 423
&&$\quad\textit{case} \; as' \Rightarrow \textit{ALTS}\;bs\;as'$\\
+ − 424
+ − 425
$\textit{simp} \; a$ & $\dn$ & $\textit{a} \qquad \textit{otherwise}$
+ − 426
\end{tabular}
+ − 427
\end{center}
+ − 428
+ − 429
\noindent
+ − 430
If we call $\simp$ on $\rup$, just as $\backslash_{simp}$
+ − 431
requires, then we would go throught the third clause of
+ − 432
the sequence case:$\quad\textit{case} \; (\ONE, a_2') \Rightarrow \textit{fuse} \; bs \; a_2'$.
+ − 433
The $\ZERO$ of $(_0\ONE + \ZERO)$ is simplified away and
+ − 434
$_0\ONE$ merged into $_0a + _1a^*$ by simply
+ − 435
putting its bits($_0$) to the front of the second component:
+ − 436
${\bf_0}(_0a + _1a^*)$.
+ − 437
After a second derivative operation,
+ − 438
namely, $(_0(_0a + _1a^*))\backslash a$, we get
+ − 439
$
+ − 440
_0(_0 \ONE + _1(_1\ONE \cdot a^*))
+ − 441
$, and this simplifies to $_0(_0 \ONE + _{11} a^*)$
+ − 442
by the third clause of the alternative case:
+ − 443
$\quad\textit{case} \; as' \Rightarrow \textit{ALTS}\;bs\;as'$.
+ − 444
The outmost bit $_0$ remains unchanged and stays with
+ − 445
the outmost regular expression. However, things are a bit
+ − 446
different when it comes to $\simp(\rup\backslash \, s)$, because
+ − 447
without simplification, first term of the sequence
+ − 448
$\rup\backslash a=(_0\ONE + \ZERO)(_0a + _1a^*)$
+ − 449
is not merged into the second component
+ − 450
and is nullable.
+ − 451
Therefore $((_0\ONE + \ZERO)(_0a + _1a^*))\backslash a$ splits into
+ − 452
$([(\ZERO + \ZERO)\cdot(_0a + _1a^*)] + _0( _0\ONE + _1[_1\ONE \cdot a^*]))$.
+ − 453
After these two successive derivatives without simplification,
+ − 454
we apply $\simp$ to this regular expression, which goes through
+ − 455
the alternative clause, and each component of $([(\ZERO + \ZERO)\cdot(_0a + _1a^*)] + _0( _0\ONE + _1[_1\ONE \cdot a^*]))$ will be simplified, giving us the list:$[\ZERO, _0(_0\ONE + _{11}a^*]$,this
+ − 456
list is then flattened--for
+ − 457
$([(\ZERO + \ZERO)\cdot(_0a + _1a^*)]$ it will be simplified into $\ZERO$
+ − 458
and then thrown away by $\textit{flatten}$; $ _0( _0\ONE + _1[_1\ONE \cdot a^*]))$
+ − 459
becomes $ _{00}\ONE + _{011}a^*]))$ because flatten opens up the alternative
+ − 460
$\ONE + a^*$ and fuses the front bit(s) $_0$ to the front of $_0\ONE $ and $_{11}a^*$
+ − 461
and get $_{00}$ and $_{011}$.
+ − 462
%CONSTRUCTION SITE
102
+ − 463
and we can use this to construct a set of examples based
103
+ − 464
on this type of behaviour of two operations:
+ − 465
$r_1$
101
+ − 466
that is to say, despite the bits are being moved around on the regular expression
+ − 467
(difference in bits), the structure of the (unannotated)regular expression
+ − 468
after one simplification is exactly the same after the
+ − 469
same sequence of derivative operations
+ − 470
regardless of whether we did simplification
+ − 471
along the way.
+ − 472
However, without erase the above equality does not hold:
+ − 473
for the regular expression
+ − 474
$(a+b)(a+a*)$,
+ − 475
if we do derivative with respect to string $aa$,
+ − 476
we get
103
+ − 477
101
+ − 478
sdddddr does not equal sdsdsdsr sometimes.\\
+ − 479
For example,
+ − 480
+ − 481
This equicalence class method might still have the potential of proving this,
+ − 482
but not yet
+ − 483
i parallelly tried another method of using retrieve\\
+ − 484
+ − 485
+ − 486
94
+ − 487
%HERE CONSTRUCTION SITE
+ − 488
The vsimp function, defined as follows
+ − 489
tries to simplify the value in lockstep with
+ − 490
regular expression:\\
+ − 491
+ − 492
+ − 493
The problem here is that
+ − 494
+ − 495
we used retrieve for the key induction:
+ − 496
$decode (retrieve (r\backslash (s @ [c])) v) r $
+ − 497
$decode (retrieve (r\backslash s) (inj (r\backslash s) c v)) r$
+ − 498
Here, decode recovers a value that corresponds to a match(possibly partial)
+ − 499
from bits, and the bits are extracted by retrieve,
+ − 500
and the key value $v$ that guides retrieve is
+ − 501
$mkeps r\backslash s$, $inj r c (mkeps r\backslash s)$, $inj (inj (v))$, ......
+ − 502
if we can
+ − 503
the problem is that
+ − 504
need vsiimp to make a value that is suitable for decoding
+ − 505
$Some(flex rid(s@[c])v) = Some(flex rids(inj (r\backslash s)cv))$
+ − 506
another way that christian came up with that might circumvent the
+ − 507
prblem of finding suitable value is by not stating the visimp
+ − 508
function but include all possible value in a set that a regex is able to produce,
+ − 509
and proving that both r and sr are able to produce the bits that correspond the POSIX value
+ − 510
+ − 511
produced by feeding the same initial regular expression $r$ and string $s$ to the
+ − 512
two functions $ders$ and $ders\_simp$.
+ − 513
The reason why
+ − 514
Namely, if $bmkeps( r_1) = bmkeps(r_2)$, then we
+ − 515
+ − 516
+ − 517
If we define the equivalence relation $\sim_{m\epsilon}$ between two regular expressions
+ − 518
$r_1$ and $r_2$as follows:
+ − 519
$r_1 \sim_{m\epsilon} r_2 \iff bmkeps(r_1)= bmkeps(r_2)$
+ − 520
(in other words, they $r1$ and $r2$ produce the same output under the function $bmkeps$.)
+ − 521
Then the first goal
+ − 522
might be restated as
+ − 523
$(r^\uparrow)\backslash_{simp}\, s \sim_{m\epsilon} (r^\uparrow)\backslash s$.
+ − 524
I tried to establish an equivalence relation between the regular experssions
+ − 525
like dddr dddsr,.....
+ − 526
but right now i am only able to establish dsr and dr, using structural induction on r.
+ − 527
Those involve multiple derivative operations are harder to prove.
+ − 528
Two attempts have been made:
+ − 529
(1)induction on the number of der operations(or in other words, the length of the string s),
+ − 530
the inductive hypothesis was initially specified as
+ − 531
"For an arbitrary regular expression r,
+ − 532
For all string s in the language of r whose length do not exceed
+ − 533
the number n, ders s r me derssimp s r"
+ − 534
and the proof goal may be stated as
+ − 535
"For an arbitrary regular expression r,
+ − 536
For all string s in the language of r whose length do not exceed
+ − 537
the number n+1, ders s r me derssimp s r"
+ − 538
the problem here is that although we can easily break down
+ − 539
a string s of length n+1 into s1@list(c), it is not that easy
+ − 540
to use the i.h. as a stepping stone to prove anything because s1 may well be not
+ − 541
in the language L(r). This inhibits us from obtaining the fact that
+ − 542
ders s1 r me derssimps s1 r.
+ − 543
Further exploration is needed to amend this hypothesis so it includes the
+ − 544
situation when s1 is not nullable.
+ − 545
For example, what information(bits?
+ − 546
values?) can be extracted
+ − 547
from the regular expression ders(s1,r) so that we can compute or predict the possible
+ − 548
result of bmkeps after another derivative operation. What function f can used to
+ − 549
carry out the task? The possible way of exploration can be
+ − 550
more directly perceived throught the graph below:
+ − 551
find a function
+ − 552
f
+ − 553
such that
+ − 554
f(bders s1 r)
+ − 555
= re1
+ − 556
f(bderss s1 r)
+ − 557
= re2
+ − 558
bmkeps(bders s r) = g(re1,c)
+ − 559
bmkeps(bderssimp s r) = g(re2,c)
+ − 560
and g(re1,c) = g(re2,c)
+ − 561
The inductive hypothesis would be
+ − 562
"For all strings s1 of length <= n,
+ − 563
f(bders s1 r)
+ − 564
= re1
+ − 565
f(bderss s1 r)
+ − 566
= re2"
+ − 567
proving this would be a lemma for the main proof:
+ − 568
the main proof would be
+ − 569
"
+ − 570
bmkeps(bders s r) = g(re1,c)
+ − 571
bmkeps(bderssimp s r) = g(re2,c)
+ − 572
for s = s1@c
+ − 573
"
+ − 574
and f need to be a recursive property for the lemma to be proved:
+ − 575
it needs to store not only the "after one char nullable info",
+ − 576
but also the "after two char nullable info",
+ − 577
and so on so that it is able to predict what f will compute after a derivative operation,
+ − 578
in other words, it needs to be "infinitely recursive"\\
+ − 579
To prove the lemma, in other words, to get
+ − 580
"For all strings s1 of length <= n+1,
+ − 581
f(bders s1 r)
+ − 582
= re3
+ − 583
f(bderss s1 r)
+ − 584
= re4"\\
+ − 585
from\\
+ − 586
"For all strings s1 of length <= n,
+ − 587
f(bders s1 r)
+ − 588
= re1
+ − 589
f(bderss s1 r)
+ − 590
= re2"\\
+ − 591
it might be best to construct an auxiliary function h such that\\
+ − 592
h(re1, c) = re3\\
+ − 593
h(re2, c) = re4\\
+ − 594
and re3 = f(bder c (bders s1 r))\\
+ − 595
re4 = f(simp(bder c (bderss s1 r)))
+ − 596
The key point here is that we are not satisfied with what bders s r will produce under
+ − 597
bmkeps, but also how it will perform after a derivative operation and then bmkeps, and two
+ − 598
derivative operations and so on. In essence, we are preserving the regular expression
+ − 599
itself under the function f, in a less compact way than the regluar expression: we are
+ − 600
not just recording but also interpreting what the regular expression matches.
+ − 601
In other words, we need to prove the properties of bderss s r beyond the bmkeps result,
+ − 602
i.e., not just the nullable ones, but also those containing remaining characters.\\
+ − 603
(2)we observed the fact that
+ − 604
erase sdddddr= erase sdsdsdsr
+ − 605
that is to say, despite the bits are being moved around on the regular expression
+ − 606
(difference in bits), the structure of the (unannotated)regular expression
+ − 607
after one simplification is exactly the same after the
+ − 608
same sequence of derivative operations
+ − 609
regardless of whether we did simplification
+ − 610
along the way.
+ − 611
However, without erase the above equality does not hold:
+ − 612
for the regular expression
+ − 613
$(a+b)(a+a*)$,
+ − 614
if we do derivative with respect to string $aa$,
+ − 615
we get
+ − 616
%TODO
+ − 617
sdddddr does not equal sdsdsdsr sometimes.\\
+ − 618
For example,
+ − 619
+ − 620
This equicalence class method might still have the potential of proving this,
+ − 621
but not yet
+ − 622
i parallelly tried another method of using retrieve\\
+ − 623
+ − 624
+ − 625
+ − 626
\noindent\rule[0.5ex]{\linewidth}{1pt}
+ − 627
+ − 628
This PhD-project is about regular expression matching and
+ − 629
lexing. Given the maturity of this topic, the reader might wonder:
+ − 630
Surely, regular expressions must have already been studied to death?
+ − 631
What could possibly be \emph{not} known in this area? And surely all
+ − 632
implemented algorithms for regular expression matching are blindingly
+ − 633
fast?
+ − 634
+ − 635
Unfortunately these preconceptions are not supported by evidence: Take
+ − 636
for example the regular expression $(a^*)^*\,b$ and ask whether
+ − 637
strings of the form $aa..a$ match this regular
+ − 638
expression. Obviously this is not the case---the expected $b$ in the last
+ − 639
position is missing. One would expect that modern regular expression
+ − 640
matching engines can find this out very quickly. Alas, if one tries
+ − 641
this example in JavaScript, Python or Java 8 with strings like 28
+ − 642
$a$'s, one discovers that this decision takes around 30 seconds and
+ − 643
takes considerably longer when adding a few more $a$'s, as the graphs
+ − 644
below show:
+ − 645
+ − 646
\begin{center}
+ − 647
\begin{tabular}{@{}c@{\hspace{0mm}}c@{\hspace{0mm}}c@{}}
+ − 648
\begin{tikzpicture}
+ − 649
\begin{axis}[
+ − 650
xlabel={$n$},
+ − 651
x label style={at={(1.05,-0.05)}},
+ − 652
ylabel={time in secs},
+ − 653
enlargelimits=false,
+ − 654
xtick={0,5,...,30},
+ − 655
xmax=33,
+ − 656
ymax=35,
+ − 657
ytick={0,5,...,30},
+ − 658
scaled ticks=false,
+ − 659
axis lines=left,
+ − 660
width=5cm,
+ − 661
height=4cm,
+ − 662
legend entries={JavaScript},
+ − 663
legend pos=north west,
+ − 664
legend cell align=left]
+ − 665
\addplot[red,mark=*, mark options={fill=white}] table {re-js.data};
+ − 666
\end{axis}
+ − 667
\end{tikzpicture}
+ − 668
&
+ − 669
\begin{tikzpicture}
+ − 670
\begin{axis}[
+ − 671
xlabel={$n$},
+ − 672
x label style={at={(1.05,-0.05)}},
+ − 673
%ylabel={time in secs},
+ − 674
enlargelimits=false,
+ − 675
xtick={0,5,...,30},
+ − 676
xmax=33,
+ − 677
ymax=35,
+ − 678
ytick={0,5,...,30},
+ − 679
scaled ticks=false,
+ − 680
axis lines=left,
+ − 681
width=5cm,
+ − 682
height=4cm,
+ − 683
legend entries={Python},
+ − 684
legend pos=north west,
+ − 685
legend cell align=left]
+ − 686
\addplot[blue,mark=*, mark options={fill=white}] table {re-python2.data};
+ − 687
\end{axis}
+ − 688
\end{tikzpicture}
+ − 689
&
+ − 690
\begin{tikzpicture}
+ − 691
\begin{axis}[
+ − 692
xlabel={$n$},
+ − 693
x label style={at={(1.05,-0.05)}},
+ − 694
%ylabel={time in secs},
+ − 695
enlargelimits=false,
+ − 696
xtick={0,5,...,30},
+ − 697
xmax=33,
+ − 698
ymax=35,
+ − 699
ytick={0,5,...,30},
+ − 700
scaled ticks=false,
+ − 701
axis lines=left,
+ − 702
width=5cm,
+ − 703
height=4cm,
+ − 704
legend entries={Java 8},
+ − 705
legend pos=north west,
+ − 706
legend cell align=left]
+ − 707
\addplot[cyan,mark=*, mark options={fill=white}] table {re-java.data};
+ − 708
\end{axis}
+ − 709
\end{tikzpicture}\\
+ − 710
\multicolumn{3}{c}{Graphs: Runtime for matching $(a^*)^*\,b$ with strings
+ − 711
of the form $\underbrace{aa..a}_{n}$.}
+ − 712
\end{tabular}
+ − 713
\end{center}
+ − 714
+ − 715
\noindent These are clearly abysmal and possibly surprising results. One
+ − 716
would expect these systems to do much better than that---after all,
+ − 717
given a DFA and a string, deciding whether a string is matched by this
+ − 718
DFA should be linear in terms of the size of the regular expression and
+ − 719
the string?
+ − 720
+ − 721
Admittedly, the regular expression $(a^*)^*\,b$ is carefully chosen to
+ − 722
exhibit this super-linear behaviour. But unfortunately, such regular
+ − 723
expressions are not just a few outliers. They are actually
+ − 724
frequent enough to have a separate name created for
+ − 725
them---\emph{evil regular expressions}. In empiric work, Davis et al
+ − 726
report that they have found thousands of such evil regular expressions
+ − 727
in the JavaScript and Python ecosystems \cite{Davis18}. Static analysis
+ − 728
approach that is both sound and complete exists\cite{17Bir}, but the running
+ − 729
time on certain examples in the RegExLib and Snort regular expressions
+ − 730
libraries is unacceptable. Therefore the problem of efficiency still remains.
+ − 731
+ − 732
This superlinear blowup in matching algorithms sometimes causes
+ − 733
considerable grief in real life: for example on 20 July 2016 one evil
+ − 734
regular expression brought the webpage
+ − 735
\href{http://stackexchange.com}{Stack Exchange} to its
+ − 736
knees.\footnote{\url{https://stackstatus.net/post/147710624694/outage-postmortem-july-20-2016}}
+ − 737
In this instance, a regular expression intended to just trim white
+ − 738
spaces from the beginning and the end of a line actually consumed
+ − 739
massive amounts of CPU-resources---causing web servers to grind to a
+ − 740
halt. This happened when a post with 20,000 white spaces was submitted,
+ − 741
but importantly the white spaces were neither at the beginning nor at
+ − 742
the end. As a result, the regular expression matching engine needed to
+ − 743
backtrack over many choices. In this example, the time needed to process
+ − 744
the string was $O(n^2)$ with respect to the string length. This
+ − 745
quadratic overhead was enough for the homepage of Stack Exchange to
+ − 746
respond so slowly that the load balancer assumed there must be some
+ − 747
attack and therefore stopped the servers from responding to any
+ − 748
requests. This made the whole site become unavailable. Another very
+ − 749
recent example is a global outage of all Cloudflare servers on 2 July
+ − 750
2019. A poorly written regular expression exhibited exponential
+ − 751
behaviour and exhausted CPUs that serve HTTP traffic. Although the
+ − 752
outage had several causes, at the heart was a regular expression that
+ − 753
was used to monitor network
+ − 754
traffic.\footnote{\url{https://blog.cloudflare.com/details-of-the-cloudflare-outage-on-july-2-2019/}}
+ − 755
+ − 756
The underlying problem is that many ``real life'' regular expression
+ − 757
matching engines do not use DFAs for matching. This is because they
+ − 758
support regular expressions that are not covered by the classical
+ − 759
automata theory, and in this more general setting there are quite a few
+ − 760
research questions still unanswered and fast algorithms still need to be
+ − 761
developed (for example how to treat efficiently bounded repetitions, negation and
+ − 762
back-references).
+ − 763
%question: dfa can have exponential states. isn't this the actual reason why they do not use dfas?
+ − 764
%how do they avoid dfas exponential states if they use them for fast matching?
+ − 765
+ − 766
There is also another under-researched problem to do with regular
+ − 767
expressions and lexing, i.e.~the process of breaking up strings into
+ − 768
sequences of tokens according to some regular expressions. In this
+ − 769
setting one is not just interested in whether or not a regular
+ − 770
expression matches a string, but also in \emph{how}. Consider for
+ − 771
example a regular expression $r_{key}$ for recognising keywords such as
+ − 772
\textit{if}, \textit{then} and so on; and a regular expression $r_{id}$
+ − 773
for recognising identifiers (say, a single character followed by
+ − 774
characters or numbers). One can then form the compound regular
+ − 775
expression $(r_{key} + r_{id})^*$ and use it to tokenise strings. But
+ − 776
then how should the string \textit{iffoo} be tokenised? It could be
+ − 777
tokenised as a keyword followed by an identifier, or the entire string
+ − 778
as a single identifier. Similarly, how should the string \textit{if} be
+ − 779
tokenised? Both regular expressions, $r_{key}$ and $r_{id}$, would
+ − 780
``fire''---so is it an identifier or a keyword? While in applications
+ − 781
there is a well-known strategy to decide these questions, called POSIX
+ − 782
matching, only relatively recently precise definitions of what POSIX
+ − 783
matching actually means have been formalised
+ − 784
\cite{AusafDyckhoffUrban2016,OkuiSuzuki2010,Vansummeren2006}. Such a
+ − 785
definition has also been given by Sulzmann and Lu \cite{Sulzmann2014},
+ − 786
but the corresponding correctness proof turned out to be faulty
+ − 787
\cite{AusafDyckhoffUrban2016}. Roughly, POSIX matching means matching
+ − 788
the longest initial substring. In the case of a tie, the initial
+ − 789
sub-match is chosen according to some priorities attached to the regular
+ − 790
expressions (e.g.~keywords have a higher priority than identifiers).
+ − 791
This sounds rather simple, but according to Grathwohl et al \cite[Page
+ − 792
36]{CrashCourse2014} this is not the case. They wrote:
+ − 793
+ − 794
\begin{quote}
+ − 795
\it{}``The POSIX strategy is more complicated than the greedy because of
+ − 796
the dependence on information about the length of matched strings in the
+ − 797
various subexpressions.''
+ − 798
\end{quote}
+ − 799
+ − 800
\noindent
+ − 801
This is also supported by evidence collected by Kuklewicz
+ − 802
\cite{Kuklewicz} who noticed that a number of POSIX regular expression
+ − 803
matchers calculate incorrect results.
+ − 804
+ − 805
Our focus in this project is on an algorithm introduced by Sulzmann and
+ − 806
Lu in 2014 for regular expression matching according to the POSIX
+ − 807
strategy \cite{Sulzmann2014}. Their algorithm is based on an older
+ − 808
algorithm by Brzozowski from 1964 where he introduced the notion of
+ − 809
derivatives of regular expressions~\cite{Brzozowski1964}. We shall
+ − 810
briefly explain this algorithm next.
+ − 811
+ − 812
\section{The Algorithm by Brzozowski based on Derivatives of Regular
+ − 813
Expressions}
+ − 814
+ − 815
Suppose (basic) regular expressions are given by the following grammar:
+ − 816
\[ r ::= \ZERO \mid \ONE
+ − 817
\mid c
+ − 818
\mid r_1 \cdot r_2
+ − 819
\mid r_1 + r_2
+ − 820
\mid r^*
+ − 821
\]
+ − 822
+ − 823
\noindent
+ − 824
The intended meaning of the constructors is as follows: $\ZERO$
+ − 825
cannot match any string, $\ONE$ can match the empty string, the
+ − 826
character regular expression $c$ can match the character $c$, and so
+ − 827
on.
+ − 828
+ − 829
The ingenious contribution by Brzozowski is the notion of
+ − 830
\emph{derivatives} of regular expressions. The idea behind this
+ − 831
notion is as follows: suppose a regular expression $r$ can match a
+ − 832
string of the form $c\!::\! s$ (that is a list of characters starting
+ − 833
with $c$), what does the regular expression look like that can match
+ − 834
just $s$? Brzozowski gave a neat answer to this question. He started
+ − 835
with the definition of $nullable$:
+ − 836
\begin{center}
+ − 837
\begin{tabular}{lcl}
+ − 838
$\nullable(\ZERO)$ & $\dn$ & $\mathit{false}$ \\
+ − 839
$\nullable(\ONE)$ & $\dn$ & $\mathit{true}$ \\
+ − 840
$\nullable(c)$ & $\dn$ & $\mathit{false}$ \\
+ − 841
$\nullable(r_1 + r_2)$ & $\dn$ & $\nullable(r_1) \vee \nullable(r_2)$ \\
+ − 842
$\nullable(r_1\cdot r_2)$ & $\dn$ & $\nullable(r_1) \wedge \nullable(r_2)$ \\
+ − 843
$\nullable(r^*)$ & $\dn$ & $\mathit{true}$ \\
+ − 844
\end{tabular}
+ − 845
\end{center}
+ − 846
This function simply tests whether the empty string is in $L(r)$.
+ − 847
He then defined
+ − 848
the following operation on regular expressions, written
+ − 849
$r\backslash c$ (the derivative of $r$ w.r.t.~the character $c$):
+ − 850
+ − 851
\begin{center}
+ − 852
\begin{tabular}{lcl}
+ − 853
$\ZERO \backslash c$ & $\dn$ & $\ZERO$\\
+ − 854
$\ONE \backslash c$ & $\dn$ & $\ZERO$\\
+ − 855
$d \backslash c$ & $\dn$ &
+ − 856
$\mathit{if} \;c = d\;\mathit{then}\;\ONE\;\mathit{else}\;\ZERO$\\
+ − 857
$(r_1 + r_2)\backslash c$ & $\dn$ & $r_1 \backslash c \,+\, r_2 \backslash c$\\
+ − 858
$(r_1 \cdot r_2)\backslash c$ & $\dn$ & $\mathit{if} \, nullable(r_1)$\\
+ − 859
& & $\mathit{then}\;(r_1\backslash c) \cdot r_2 \,+\, r_2\backslash c$\\
+ − 860
& & $\mathit{else}\;(r_1\backslash c) \cdot r_2$\\
+ − 861
$(r^*)\backslash c$ & $\dn$ & $(r\backslash c) \cdot r^*$\\
+ − 862
\end{tabular}
+ − 863
\end{center}
+ − 864
+ − 865
%Assuming the classic notion of a
+ − 866
%\emph{language} of a regular expression, written $L(\_)$, t
+ − 867
+ − 868
\noindent
+ − 869
The main property of the derivative operation is that
+ − 870
+ − 871
\begin{center}
+ − 872
$c\!::\!s \in L(r)$ holds
+ − 873
if and only if $s \in L(r\backslash c)$.
+ − 874
\end{center}
+ − 875
+ − 876
\noindent
+ − 877
For us the main advantage is that derivatives can be
+ − 878
straightforwardly implemented in any functional programming language,
+ − 879
and are easily definable and reasoned about in theorem provers---the
+ − 880
definitions just consist of inductive datatypes and simple recursive
+ − 881
functions. Moreover, the notion of derivatives can be easily
+ − 882
generalised to cover extended regular expression constructors such as
+ − 883
the not-regular expression, written $\neg\,r$, or bounded repetitions
+ − 884
(for example $r^{\{n\}}$ and $r^{\{n..m\}}$), which cannot be so
+ − 885
straightforwardly realised within the classic automata approach.
+ − 886
For the moment however, we focus only on the usual basic regular expressions.
+ − 887
+ − 888
+ − 889
Now if we want to find out whether a string $s$ matches with a regular
+ − 890
expression $r$, we can build the derivatives of $r$ w.r.t.\ (in succession)
+ − 891
all the characters of the string $s$. Finally, test whether the
+ − 892
resulting regular expression can match the empty string. If yes, then
+ − 893
$r$ matches $s$, and no in the negative case. To implement this idea
+ − 894
we can generalise the derivative operation to strings like this:
+ − 895
+ − 896
\begin{center}
+ − 897
\begin{tabular}{lcl}
+ − 898
$r \backslash (c\!::\!s) $ & $\dn$ & $(r \backslash c) \backslash s$ \\
+ − 899
$r \backslash [\,] $ & $\dn$ & $r$
+ − 900
\end{tabular}
+ − 901
\end{center}
+ − 902
+ − 903
\noindent
+ − 904
and then define as regular-expression matching algorithm:
+ − 905
\[
+ − 906
match\;s\;r \;\dn\; nullable(r\backslash s)
+ − 907
\]
+ − 908
+ − 909
\noindent
+ − 910
This algorithm looks graphically as follows:
+ − 911
\begin{equation}\label{graph:*}
+ − 912
\begin{tikzcd}
+ − 913
r_0 \arrow[r, "\backslash c_0"] & r_1 \arrow[r, "\backslash c_1"] & r_2 \arrow[r, dashed] & r_n \arrow[r,"\textit{nullable}?"] & \;\textrm{YES}/\textrm{NO}
+ − 914
\end{tikzcd}
+ − 915
\end{equation}
+ − 916
+ − 917
\noindent
+ − 918
where we start with a regular expression $r_0$, build successive
+ − 919
derivatives until we exhaust the string and then use \textit{nullable}
+ − 920
to test whether the result can match the empty string. It can be
+ − 921
relatively easily shown that this matcher is correct (that is given
+ − 922
an $s = c_0...c_{n-1}$ and an $r_0$, it generates YES if and only if $s \in L(r_0)$).
+ − 923
+ − 924
+ − 925
\section{Values and the Algorithm by Sulzmann and Lu}
+ − 926
+ − 927
One limitation of Brzozowski's algorithm is that it only produces a
+ − 928
YES/NO answer for whether a string is being matched by a regular
+ − 929
expression. Sulzmann and Lu~\cite{Sulzmann2014} extended this algorithm
+ − 930
to allow generation of an actual matching, called a \emph{value} or
+ − 931
sometimes also \emph{lexical value}. These values and regular
+ − 932
expressions correspond to each other as illustrated in the following
+ − 933
table:
+ − 934
+ − 935
+ − 936
\begin{center}
+ − 937
\begin{tabular}{c@{\hspace{20mm}}c}
+ − 938
\begin{tabular}{@{}rrl@{}}
+ − 939
\multicolumn{3}{@{}l}{\textbf{Regular Expressions}}\medskip\\
+ − 940
$r$ & $::=$ & $\ZERO$\\
+ − 941
& $\mid$ & $\ONE$ \\
+ − 942
& $\mid$ & $c$ \\
+ − 943
& $\mid$ & $r_1 \cdot r_2$\\
+ − 944
& $\mid$ & $r_1 + r_2$ \\
+ − 945
\\
+ − 946
& $\mid$ & $r^*$ \\
+ − 947
\end{tabular}
+ − 948
&
+ − 949
\begin{tabular}{@{\hspace{0mm}}rrl@{}}
+ − 950
\multicolumn{3}{@{}l}{\textbf{Values}}\medskip\\
+ − 951
$v$ & $::=$ & \\
+ − 952
& & $\Empty$ \\
+ − 953
& $\mid$ & $\Char(c)$ \\
+ − 954
& $\mid$ & $\Seq\,v_1\, v_2$\\
+ − 955
& $\mid$ & $\Left(v)$ \\
+ − 956
& $\mid$ & $\Right(v)$ \\
+ − 957
& $\mid$ & $\Stars\,[v_1,\ldots\,v_n]$ \\
+ − 958
\end{tabular}
+ − 959
\end{tabular}
+ − 960
\end{center}
+ − 961
+ − 962
\noindent
+ − 963
No value corresponds to $\ZERO$; $\Empty$ corresponds to $\ONE$;
+ − 964
$\Char$ to the character regular expression; $\Seq$ to the sequence
+ − 965
regular expression and so on. The idea of values is to encode a kind of
+ − 966
lexical value for how the sub-parts of a regular expression match the
+ − 967
sub-parts of a string. To see this, suppose a \emph{flatten} operation,
+ − 968
written $|v|$ for values. We can use this function to extract the
+ − 969
underlying string of a value $v$. For example, $|\mathit{Seq} \,
+ − 970
(\textit{Char x}) \, (\textit{Char y})|$ is the string $xy$. Using
+ − 971
flatten, we can describe how values encode lexical values: $\Seq\,v_1\,
+ − 972
v_2$ encodes a tree with two children nodes that tells how the string
+ − 973
$|v_1| @ |v_2|$ matches the regex $r_1 \cdot r_2$ whereby $r_1$ matches
+ − 974
the substring $|v_1|$ and, respectively, $r_2$ matches the substring
+ − 975
$|v_2|$. Exactly how these two are matched is contained in the children
+ − 976
nodes $v_1$ and $v_2$ of parent $\textit{Seq}$.
+ − 977
+ − 978
To give a concrete example of how values work, consider the string $xy$
+ − 979
and the regular expression $(x + (y + xy))^*$. We can view this regular
+ − 980
expression as a tree and if the string $xy$ is matched by two Star
+ − 981
``iterations'', then the $x$ is matched by the left-most alternative in
+ − 982
this tree and the $y$ by the right-left alternative. This suggests to
+ − 983
record this matching as
+ − 984
+ − 985
\begin{center}
+ − 986
$\Stars\,[\Left\,(\Char\,x), \Right(\Left(\Char\,y))]$
+ − 987
\end{center}
+ − 988
+ − 989
\noindent
+ − 990
where $\Stars \; [\ldots]$ records all the
+ − 991
iterations; and $\Left$, respectively $\Right$, which
+ − 992
alternative is used. The value for
+ − 993
matching $xy$ in a single ``iteration'', i.e.~the POSIX value,
+ − 994
would look as follows
+ − 995
+ − 996
\begin{center}
+ − 997
$\Stars\,[\Seq\,(\Char\,x)\,(\Char\,y)]$
+ − 998
\end{center}
+ − 999
+ − 1000
\noindent
+ − 1001
where $\Stars$ has only a single-element list for the single iteration
+ − 1002
and $\Seq$ indicates that $xy$ is matched by a sequence regular
+ − 1003
expression.
+ − 1004
+ − 1005
The contribution of Sulzmann and Lu is an extension of Brzozowski's
+ − 1006
algorithm by a second phase (the first phase being building successive
+ − 1007
derivatives---see \eqref{graph:*}). In this second phase, a POSIX value
+ − 1008
is generated in case the regular expression matches the string.
+ − 1009
Pictorially, the Sulzmann and Lu algorithm is as follows:
+ − 1010
+ − 1011
\begin{ceqn}
+ − 1012
\begin{equation}\label{graph:2}
+ − 1013
\begin{tikzcd}
+ − 1014
r_0 \arrow[r, "\backslash c_0"] \arrow[d] & r_1 \arrow[r, "\backslash c_1"] \arrow[d] & r_2 \arrow[r, dashed] \arrow[d] & r_n \arrow[d, "mkeps" description] \\
+ − 1015
v_0 & v_1 \arrow[l,"inj_{r_0} c_0"] & v_2 \arrow[l, "inj_{r_1} c_1"] & v_n \arrow[l, dashed]
+ − 1016
\end{tikzcd}
+ − 1017
\end{equation}
+ − 1018
\end{ceqn}
+ − 1019
+ − 1020
\noindent
+ − 1021
For convenience, we shall employ the following notations: the regular
+ − 1022
expression we start with is $r_0$, and the given string $s$ is composed
+ − 1023
of characters $c_0 c_1 \ldots c_{n-1}$. In the first phase from the
+ − 1024
left to right, we build the derivatives $r_1$, $r_2$, \ldots according
+ − 1025
to the characters $c_0$, $c_1$ until we exhaust the string and obtain
+ − 1026
the derivative $r_n$. We test whether this derivative is
+ − 1027
$\textit{nullable}$ or not. If not, we know the string does not match
+ − 1028
$r$ and no value needs to be generated. If yes, we start building the
+ − 1029
values incrementally by \emph{injecting} back the characters into the
+ − 1030
earlier values $v_n, \ldots, v_0$. This is the second phase of the
+ − 1031
algorithm from the right to left. For the first value $v_n$, we call the
+ − 1032
function $\textit{mkeps}$, which builds the lexical value
+ − 1033
for how the empty string has been matched by the (nullable) regular
+ − 1034
expression $r_n$. This function is defined as
+ − 1035
+ − 1036
\begin{center}
+ − 1037
\begin{tabular}{lcl}
+ − 1038
$\mkeps(\ONE)$ & $\dn$ & $\Empty$ \\
+ − 1039
$\mkeps(r_{1}+r_{2})$ & $\dn$
+ − 1040
& \textit{if} $\nullable(r_{1})$\\
+ − 1041
& & \textit{then} $\Left(\mkeps(r_{1}))$\\
+ − 1042
& & \textit{else} $\Right(\mkeps(r_{2}))$\\
+ − 1043
$\mkeps(r_1\cdot r_2)$ & $\dn$ & $\Seq\,(\mkeps\,r_1)\,(\mkeps\,r_2)$\\
+ − 1044
$mkeps(r^*)$ & $\dn$ & $\Stars\,[]$
+ − 1045
\end{tabular}
+ − 1046
\end{center}
+ − 1047
+ − 1048
+ − 1049
\noindent There are no cases for $\ZERO$ and $c$, since
+ − 1050
these regular expression cannot match the empty string. Note
+ − 1051
also that in case of alternatives we give preference to the
+ − 1052
regular expression on the left-hand side. This will become
+ − 1053
important later on about what value is calculated.
+ − 1054
+ − 1055
After the $\mkeps$-call, we inject back the characters one by one in order to build
+ − 1056
the lexical value $v_i$ for how the regex $r_i$ matches the string $s_i$
+ − 1057
($s_i = c_i \ldots c_{n-1}$ ) from the previous lexical value $v_{i+1}$.
+ − 1058
After injecting back $n$ characters, we get the lexical value for how $r_0$
+ − 1059
matches $s$. For this Sulzmann and Lu defined a function that reverses
+ − 1060
the ``chopping off'' of characters during the derivative phase. The
+ − 1061
corresponding function is called \emph{injection}, written
+ − 1062
$\textit{inj}$; it takes three arguments: the first one is a regular
+ − 1063
expression ${r_{i-1}}$, before the character is chopped off, the second
+ − 1064
is a character ${c_{i-1}}$, the character we want to inject and the
+ − 1065
third argument is the value ${v_i}$, into which one wants to inject the
+ − 1066
character (it corresponds to the regular expression after the character
+ − 1067
has been chopped off). The result of this function is a new value. The
+ − 1068
definition of $\textit{inj}$ is as follows:
+ − 1069
+ − 1070
\begin{center}
+ − 1071
\begin{tabular}{l@{\hspace{1mm}}c@{\hspace{1mm}}l}
+ − 1072
$\textit{inj}\,(c)\,c\,Empty$ & $\dn$ & $Char\,c$\\
+ − 1073
$\textit{inj}\,(r_1 + r_2)\,c\,\Left(v)$ & $\dn$ & $\Left(\textit{inj}\,r_1\,c\,v)$\\
+ − 1074
$\textit{inj}\,(r_1 + r_2)\,c\,Right(v)$ & $\dn$ & $Right(\textit{inj}\,r_2\,c\,v)$\\
+ − 1075
$\textit{inj}\,(r_1 \cdot r_2)\,c\,Seq(v_1,v_2)$ & $\dn$ & $Seq(\textit{inj}\,r_1\,c\,v_1,v_2)$\\
+ − 1076
$\textit{inj}\,(r_1 \cdot r_2)\,c\,\Left(Seq(v_1,v_2))$ & $\dn$ & $Seq(\textit{inj}\,r_1\,c\,v_1,v_2)$\\
+ − 1077
$\textit{inj}\,(r_1 \cdot r_2)\,c\,Right(v)$ & $\dn$ & $Seq(\textit{mkeps}(r_1),\textit{inj}\,r_2\,c\,v)$\\
+ − 1078
$\textit{inj}\,(r^*)\,c\,Seq(v,Stars\,vs)$ & $\dn$ & $Stars((\textit{inj}\,r\,c\,v)\,::\,vs)$\\
+ − 1079
\end{tabular}
+ − 1080
\end{center}
+ − 1081
+ − 1082
\noindent This definition is by recursion on the ``shape'' of regular
+ − 1083
expressions and values. To understands this definition better consider
+ − 1084
the situation when we build the derivative on regular expression $r_{i-1}$.
+ − 1085
For this we chop off a character from $r_{i-1}$ to form $r_i$. This leaves a
+ − 1086
``hole'' in $r_i$ and its corresponding value $v_i$.
+ − 1087
To calculate $v_{i-1}$, we need to
+ − 1088
locate where that hole is and fill it.
+ − 1089
We can find this location by
+ − 1090
comparing $r_{i-1}$ and $v_i$. For instance, if $r_{i-1}$ is of shape
+ − 1091
$r_a \cdot r_b$, and $v_i$ is of shape $\Left(Seq(v_1,v_2))$, we know immediately that
+ − 1092
%
+ − 1093
\[ (r_a \cdot r_b)\backslash c = (r_a\backslash c) \cdot r_b \,+\, r_b\backslash c,\]
+ − 1094
+ − 1095
\noindent
+ − 1096
otherwise if $r_a$ is not nullable,
+ − 1097
\[ (r_a \cdot r_b)\backslash c = (r_a\backslash c) \cdot r_b,\]
+ − 1098
+ − 1099
\noindent
+ − 1100
the value $v_i$ should be $\Seq(\ldots)$, contradicting the fact that
+ − 1101
$v_i$ is actually of shape $\Left(\ldots)$. Furthermore, since $v_i$ is of shape
+ − 1102
$\Left(\ldots)$ instead of $\Right(\ldots)$, we know that the left
+ − 1103
branch of \[ (r_a \cdot r_b)\backslash c =
+ − 1104
\bold{\underline{ (r_a\backslash c) \cdot r_b} }\,+\, r_b\backslash c,\](underlined)
+ − 1105
is taken instead of the right one. This means $c$ is chopped off
+ − 1106
from $r_a$ rather than $r_b$.
+ − 1107
We have therefore found out
+ − 1108
that the hole will be on $r_a$. So we recursively call $\inj\,
+ − 1109
r_a\,c\,v_a$ to fill that hole in $v_a$. After injection, the value
+ − 1110
$v_i$ for $r_i = r_a \cdot r_b$ should be $\Seq\,(\inj\,r_a\,c\,v_a)\,v_b$.
+ − 1111
Other clauses can be understood in a similar way.
+ − 1112
+ − 1113
%\comment{Other word: insight?}
+ − 1114
The following example gives an insight of $\textit{inj}$'s effect and
+ − 1115
how Sulzmann and Lu's algorithm works as a whole. Suppose we have a
+ − 1116
regular expression $((((a+b)+ab)+c)+abc)^*$, and want to match it
+ − 1117
against the string $abc$ (when $abc$ is written as a regular expression,
+ − 1118
the standard way of expressing it is $a \cdot (b \cdot c)$. But we
+ − 1119
usually omit the parentheses and dots here for better readability. This
+ − 1120
algorithm returns a POSIX value, which means it will produce the longest
+ − 1121
matching. Consequently, it matches the string $abc$ in one star
+ − 1122
iteration, using the longest alternative $abc$ in the sub-expression (we shall use $r$ to denote this
+ − 1123
sub-expression for conciseness):
+ − 1124
+ − 1125
\[((((a+b)+ab)+c)+\underbrace{abc}_r)\]
+ − 1126
+ − 1127
\noindent
+ − 1128
Before $\textit{inj}$ is called, our lexer first builds derivative using
+ − 1129
string $abc$ (we simplified some regular expressions like $\ZERO \cdot
+ − 1130
b$ to $\ZERO$ for conciseness; we also omit parentheses if they are
+ − 1131
clear from the context):
+ − 1132
+ − 1133
%Similarly, we allow
+ − 1134
%$\textit{ALT}$ to take a list of regular expressions as an argument
+ − 1135
%instead of just 2 operands to reduce the nested depth of
+ − 1136
%$\textit{ALT}$
+ − 1137
+ − 1138
\begin{center}
+ − 1139
\begin{tabular}{lcl}
+ − 1140
$r^*$ & $\xrightarrow{\backslash a}$ & $r_1 = (\ONE+\ZERO+\ONE \cdot b + \ZERO + \ONE \cdot b \cdot c) \cdot r^*$\\
+ − 1141
& $\xrightarrow{\backslash b}$ & $r_2 = (\ZERO+\ZERO+\ONE \cdot \ONE + \ZERO + \ONE \cdot \ONE \cdot c) \cdot r^* +(\ZERO+\ONE+\ZERO + \ZERO + \ZERO) \cdot r^*$\\
+ − 1142
& $\xrightarrow{\backslash c}$ & $r_3 = ((\ZERO+\ZERO+\ZERO + \ZERO + \ONE \cdot \ONE \cdot \ONE) \cdot r^* + (\ZERO+\ZERO+\ZERO + \ONE + \ZERO) \cdot r^*) + $\\
+ − 1143
& & $\phantom{r_3 = (} ((\ZERO+\ONE+\ZERO + \ZERO + \ZERO) \cdot r^* + (\ZERO+\ZERO+\ZERO + \ONE + \ZERO) \cdot r^* )$
+ − 1144
\end{tabular}
+ − 1145
\end{center}
+ − 1146
+ − 1147
\noindent
+ − 1148
In case $r_3$ is nullable, we can call $\textit{mkeps}$
+ − 1149
to construct a lexical value for how $r_3$ matched the string $abc$.
+ − 1150
This function gives the following value $v_3$:
+ − 1151
+ − 1152
+ − 1153
\begin{center}
+ − 1154
$\Left(\Left(\Seq(\Right(\Seq(\Empty, \Seq(\Empty,\Empty))), \Stars [])))$
+ − 1155
\end{center}
+ − 1156
The outer $\Left(\Left(\ldots))$ tells us the leftmost nullable part of $r_3$(underlined):
+ − 1157
+ − 1158
\begin{center}
+ − 1159
\begin{tabular}{l@{\hspace{2mm}}l}
+ − 1160
& $\big(\underline{(\ZERO+\ZERO+\ZERO+ \ZERO+ \ONE \cdot \ONE \cdot \ONE) \cdot r^*}
+ − 1161
\;+\; (\ZERO+\ZERO+\ZERO + \ONE + \ZERO) \cdot r^*\big)$ \smallskip\\
+ − 1162
$+$ & $\big((\ZERO+\ONE+\ZERO + \ZERO + \ZERO) \cdot r^*
+ − 1163
\;+\; (\ZERO+\ZERO+\ZERO + \ONE + \ZERO) \cdot r^* \big)$
+ − 1164
\end{tabular}
+ − 1165
\end{center}
+ − 1166
+ − 1167
\noindent
+ − 1168
Note that the leftmost location of term $(\ZERO+\ZERO+\ZERO + \ZERO + \ONE \cdot \ONE \cdot
+ − 1169
\ONE) \cdot r^*$ (which corresponds to the initial sub-match $abc$) allows
+ − 1170
$\textit{mkeps}$ to pick it up because $\textit{mkeps}$ is defined to always choose the
+ − 1171
left one when it is nullable. In the case of this example, $abc$ is
+ − 1172
preferred over $a$ or $ab$. This $\Left(\Left(\ldots))$ location is
+ − 1173
generated by two applications of the splitting clause
+ − 1174
+ − 1175
\begin{center}
+ − 1176
$(r_1 \cdot r_2)\backslash c \;\;(when \; r_1 \; nullable) \, = (r_1\backslash c) \cdot r_2 \,+\, r_2\backslash c.$
+ − 1177
\end{center}
+ − 1178
+ − 1179
\noindent
+ − 1180
By this clause, we put $r_1 \backslash c \cdot r_2 $ at the
+ − 1181
$\textit{front}$ and $r_2 \backslash c$ at the $\textit{back}$. This
+ − 1182
allows $\textit{mkeps}$ to always pick up among two matches the one with a longer
+ − 1183
initial sub-match. Removing the outside $\Left(\Left(...))$, the inside
+ − 1184
sub-value
+ − 1185
+ − 1186
\begin{center}
+ − 1187
$\Seq(\Right(\Seq(\Empty, \Seq(\Empty, \Empty))), \Stars [])$
+ − 1188
\end{center}
+ − 1189
+ − 1190
\noindent
+ − 1191
tells us how the empty string $[]$ is matched with $(\ZERO+\ZERO+\ZERO + \ZERO + \ONE \cdot
+ − 1192
\ONE \cdot \ONE) \cdot r^*$. We match $[]$ by a sequence of two nullable regular
+ − 1193
expressions. The first one is an alternative, we take the rightmost
+ − 1194
alternative---whose language contains the empty string. The second
+ − 1195
nullable regular expression is a Kleene star. $\Stars$ tells us how it
+ − 1196
generates the nullable regular expression: by 0 iterations to form
+ − 1197
$\ONE$. Now $\textit{inj}$ injects characters back and incrementally
+ − 1198
builds a lexical value based on $v_3$. Using the value $v_3$, the character
+ − 1199
c, and the regular expression $r_2$, we can recover how $r_2$ matched
+ − 1200
the string $[c]$ : $\textit{inj} \; r_2 \; c \; v_3$ gives us
+ − 1201
\begin{center}
+ − 1202
$v_2 = \Left(\Seq(\Right(\Seq(\Empty, \Seq(\Empty, c))), \Stars [])),$
+ − 1203
\end{center}
+ − 1204
which tells us how $r_2$ matched $[c]$. After this we inject back the character $b$, and get
+ − 1205
\begin{center}
+ − 1206
$v_1 = \Seq(\Right(\Seq(\Empty, \Seq(b, c))), \Stars [])$
+ − 1207
\end{center}
+ − 1208
for how
+ − 1209
\begin{center}
+ − 1210
$r_1= (\ONE+\ZERO+\ONE \cdot b + \ZERO + \ONE \cdot b \cdot c) \cdot r*$
+ − 1211
\end{center}
+ − 1212
matched the string $bc$ before it split into two substrings.
+ − 1213
Finally, after injecting character $a$ back to $v_1$,
+ − 1214
we get the lexical value tree
+ − 1215
\begin{center}
+ − 1216
$v_0= \Stars [\Right(\Seq(a, \Seq(b, c)))]$
+ − 1217
\end{center}
+ − 1218
for how $r$ matched $abc$. This completes the algorithm.
+ − 1219
+ − 1220
%We omit the details of injection function, which is provided by Sulzmann and Lu's paper \cite{Sulzmann2014}.
+ − 1221
Readers might have noticed that the lexical value information is actually
+ − 1222
already available when doing derivatives. For example, immediately after
+ − 1223
the operation $\backslash a$ we know that if we want to match a string
+ − 1224
that starts with $a$, we can either take the initial match to be
+ − 1225
+ − 1226
\begin{center}
+ − 1227
\begin{enumerate}
+ − 1228
\item[1)] just $a$ or
+ − 1229
\item[2)] string $ab$ or
+ − 1230
\item[3)] string $abc$.
+ − 1231
\end{enumerate}
+ − 1232
\end{center}
+ − 1233
+ − 1234
\noindent
+ − 1235
In order to differentiate between these choices, we just need to
+ − 1236
remember their positions---$a$ is on the left, $ab$ is in the middle ,
+ − 1237
and $abc$ is on the right. Which of these alternatives is chosen
+ − 1238
later does not affect their relative position because the algorithm does
+ − 1239
not change this order. If this parsing information can be determined and
+ − 1240
does not change because of later derivatives, there is no point in
+ − 1241
traversing this information twice. This leads to an optimisation---if we
+ − 1242
store the information for lexical values inside the regular expression,
+ − 1243
update it when we do derivative on them, and collect the information
+ − 1244
when finished with derivatives and call $\textit{mkeps}$ for deciding which
+ − 1245
branch is POSIX, we can generate the lexical value in one pass, instead of
+ − 1246
doing the rest $n$ injections. This leads to Sulzmann and Lu's novel
+ − 1247
idea of using bitcodes in derivatives.
+ − 1248
+ − 1249
In the next section, we shall focus on the bitcoded algorithm and the
+ − 1250
process of simplification of regular expressions. This is needed in
+ − 1251
order to obtain \emph{fast} versions of the Brzozowski's, and Sulzmann
+ − 1252
and Lu's algorithms. This is where the PhD-project aims to advance the
+ − 1253
state-of-the-art.
+ − 1254
+ − 1255
+ − 1256
\section{Simplification of Regular Expressions}
+ − 1257
+ − 1258
Using bitcodes to guide parsing is not a novel idea. It was applied to
+ − 1259
context free grammars and then adapted by Henglein and Nielson for
+ − 1260
efficient regular expression lexing using DFAs~\cite{nielson11bcre}.
+ − 1261
Sulzmann and Lu took this idea of bitcodes a step further by integrating
+ − 1262
bitcodes into derivatives. The reason why we want to use bitcodes in
+ − 1263
this project is that we want to introduce more aggressive simplification
+ − 1264
rules in order to keep the size of derivatives small throughout. This is
+ − 1265
because the main drawback of building successive derivatives according
+ − 1266
to Brzozowski's definition is that they can grow very quickly in size.
+ − 1267
This is mainly due to the fact that the derivative operation generates
+ − 1268
often ``useless'' $\ZERO$s and $\ONE$s in derivatives. As a result, if
+ − 1269
implemented naively both algorithms by Brzozowski and by Sulzmann and Lu
+ − 1270
are excruciatingly slow. For example when starting with the regular
+ − 1271
expression $(a + aa)^*$ and building 12 successive derivatives
+ − 1272
w.r.t.~the character $a$, one obtains a derivative regular expression
+ − 1273
with more than 8000 nodes (when viewed as a tree). Operations like
+ − 1274
$\textit{der}$ and $\nullable$ need to traverse such trees and
+ − 1275
consequently the bigger the size of the derivative the slower the
+ − 1276
algorithm.
+ − 1277
+ − 1278
Fortunately, one can simplify regular expressions after each derivative
+ − 1279
step. Various simplifications of regular expressions are possible, such
+ − 1280
as the simplification of $\ZERO + r$, $r + \ZERO$, $\ONE\cdot r$, $r
+ − 1281
\cdot \ONE$, and $r + r$ to just $r$. These simplifications do not
+ − 1282
affect the answer for whether a regular expression matches a string or
+ − 1283
not, but fortunately also do not affect the POSIX strategy of how
+ − 1284
regular expressions match strings---although the latter is much harder
+ − 1285
to establish. Some initial results in this regard have been
+ − 1286
obtained in \cite{AusafDyckhoffUrban2016}.
+ − 1287
+ − 1288
Unfortunately, the simplification rules outlined above are not
+ − 1289
sufficient to prevent a size explosion in all cases. We
+ − 1290
believe a tighter bound can be achieved that prevents an explosion in
+ − 1291
\emph{all} cases. Such a tighter bound is suggested by work of Antimirov who
+ − 1292
proved that (partial) derivatives can be bound by the number of
+ − 1293
characters contained in the initial regular expression
+ − 1294
\cite{Antimirov95}. He defined the \emph{partial derivatives} of regular
+ − 1295
expressions as follows:
+ − 1296
+ − 1297
\begin{center}
+ − 1298
\begin{tabular}{lcl}
+ − 1299
$\textit{pder} \; c \; \ZERO$ & $\dn$ & $\emptyset$\\
+ − 1300
$\textit{pder} \; c \; \ONE$ & $\dn$ & $\emptyset$ \\
+ − 1301
$\textit{pder} \; c \; d$ & $\dn$ & $\textit{if} \; c \,=\, d \; \{ \ONE \} \; \textit{else} \; \emptyset$ \\
+ − 1302
$\textit{pder} \; c \; r_1+r_2$ & $\dn$ & $pder \; c \; r_1 \cup pder \; c \; r_2$ \\
+ − 1303
$\textit{pder} \; c \; r_1 \cdot r_2$ & $\dn$ & $\textit{if} \; nullable \; r_1 $\\
+ − 1304
& & $\textit{then} \; \{ r \cdot r_2 \mid r \in pder \; c \; r_1 \} \cup pder \; c \; r_2 \;$\\
+ − 1305
& & $\textit{else} \; \{ r \cdot r_2 \mid r \in pder \; c \; r_1 \} $ \\
+ − 1306
$\textit{pder} \; c \; r^*$ & $\dn$ & $ \{ r' \cdot r^* \mid r' \in pder \; c \; r \} $ \\
+ − 1307
\end{tabular}
+ − 1308
\end{center}
+ − 1309
+ − 1310
\noindent
+ − 1311
A partial derivative of a regular expression $r$ is essentially a set of
+ − 1312
regular expressions that are either $r$'s children expressions or a
+ − 1313
concatenation of them. Antimirov has proved a tight bound of the sum of
+ − 1314
the size of \emph{all} partial derivatives no matter what the string
+ − 1315
looks like. Roughly speaking the size sum will be at most cubic in the
+ − 1316
size of the regular expression.
+ − 1317
+ − 1318
If we want the size of derivatives in Sulzmann and Lu's algorithm to
+ − 1319
stay below this bound, we would need more aggressive simplifications.
+ − 1320
Essentially we need to delete useless $\ZERO$s and $\ONE$s, as well as
+ − 1321
deleting duplicates whenever possible. For example, the parentheses in
+ − 1322
$(a+b) \cdot c + bc$ can be opened up to get $a\cdot c + b \cdot c + b
+ − 1323
\cdot c$, and then simplified to just $a \cdot c + b \cdot c$. Another
+ − 1324
example is simplifying $(a^*+a) + (a^*+ \ONE) + (a +\ONE)$ to just
+ − 1325
$a^*+a+\ONE$. Adding these more aggressive simplification rules helps us
+ − 1326
to achieve the same size bound as that of the partial derivatives.
+ − 1327
+ − 1328
In order to implement the idea of ``spilling out alternatives'' and to
+ − 1329
make them compatible with the $\text{inj}$-mechanism, we use
+ − 1330
\emph{bitcodes}. Bits and bitcodes (lists of bits) are just:
+ − 1331
+ − 1332
%This allows us to prove a tight
+ − 1333
%bound on the size of regular expression during the running time of the
+ − 1334
%algorithm if we can establish the connection between our simplification
+ − 1335
%rules and partial derivatives.
+ − 1336
+ − 1337
%We believe, and have generated test
+ − 1338
%data, that a similar bound can be obtained for the derivatives in
+ − 1339
%Sulzmann and Lu's algorithm. Let us give some details about this next.
+ − 1340
+ − 1341
+ − 1342
\begin{center}
+ − 1343
$b ::= S \mid Z \qquad
+ − 1344
bs ::= [] \mid b:bs
+ − 1345
$
+ − 1346
\end{center}
+ − 1347
+ − 1348
\noindent
+ − 1349
The $S$ and $Z$ are arbitrary names for the bits in order to avoid
+ − 1350
confusion with the regular expressions $\ZERO$ and $\ONE$. Bitcodes (or
+ − 1351
bit-lists) can be used to encode values (or incomplete values) in a
+ − 1352
compact form. This can be straightforwardly seen in the following
+ − 1353
coding function from values to bitcodes:
+ − 1354
+ − 1355
\begin{center}
+ − 1356
\begin{tabular}{lcl}
+ − 1357
$\textit{code}(\Empty)$ & $\dn$ & $[]$\\
+ − 1358
$\textit{code}(\Char\,c)$ & $\dn$ & $[]$\\
+ − 1359
$\textit{code}(\Left\,v)$ & $\dn$ & $\Z :: code(v)$\\
+ − 1360
$\textit{code}(\Right\,v)$ & $\dn$ & $\S :: code(v)$\\
+ − 1361
$\textit{code}(\Seq\,v_1\,v_2)$ & $\dn$ & $code(v_1) \,@\, code(v_2)$\\
+ − 1362
$\textit{code}(\Stars\,[])$ & $\dn$ & $[\Z]$\\
+ − 1363
$\textit{code}(\Stars\,(v\!::\!vs))$ & $\dn$ & $\S :: code(v) \;@\;
+ − 1364
code(\Stars\,vs)$
+ − 1365
\end{tabular}
+ − 1366
\end{center}
+ − 1367
+ − 1368
\noindent
+ − 1369
Here $\textit{code}$ encodes a value into a bitcodes by converting
+ − 1370
$\Left$ into $\Z$, $\Right$ into $\S$, the start point of a non-empty
+ − 1371
star iteration into $\S$, and the border where a local star terminates
+ − 1372
into $\Z$. This coding is lossy, as it throws away the information about
+ − 1373
characters, and also does not encode the ``boundary'' between two
+ − 1374
sequence values. Moreover, with only the bitcode we cannot even tell
+ − 1375
whether the $\S$s and $\Z$s are for $\Left/\Right$ or $\Stars$. The
+ − 1376
reason for choosing this compact way of storing information is that the
+ − 1377
relatively small size of bits can be easily manipulated and ``moved
+ − 1378
around'' in a regular expression. In order to recover values, we will
+ − 1379
need the corresponding regular expression as an extra information. This
+ − 1380
means the decoding function is defined as:
+ − 1381
+ − 1382
+ − 1383
%\begin{definition}[Bitdecoding of Values]\mbox{}
+ − 1384
\begin{center}
+ − 1385
\begin{tabular}{@{}l@{\hspace{1mm}}c@{\hspace{1mm}}l@{}}
+ − 1386
$\textit{decode}'\,bs\,(\ONE)$ & $\dn$ & $(\Empty, bs)$\\
+ − 1387
$\textit{decode}'\,bs\,(c)$ & $\dn$ & $(\Char\,c, bs)$\\
+ − 1388
$\textit{decode}'\,(\Z\!::\!bs)\;(r_1 + r_2)$ & $\dn$ &
+ − 1389
$\textit{let}\,(v, bs_1) = \textit{decode}'\,bs\,r_1\;\textit{in}\;
+ − 1390
(\Left\,v, bs_1)$\\
+ − 1391
$\textit{decode}'\,(\S\!::\!bs)\;(r_1 + r_2)$ & $\dn$ &
+ − 1392
$\textit{let}\,(v, bs_1) = \textit{decode}'\,bs\,r_2\;\textit{in}\;
+ − 1393
(\Right\,v, bs_1)$\\
+ − 1394
$\textit{decode}'\,bs\;(r_1\cdot r_2)$ & $\dn$ &
+ − 1395
$\textit{let}\,(v_1, bs_1) = \textit{decode}'\,bs\,r_1\;\textit{in}$\\
+ − 1396
& & $\textit{let}\,(v_2, bs_2) = \textit{decode}'\,bs_1\,r_2$\\
+ − 1397
& & \hspace{35mm}$\textit{in}\;(\Seq\,v_1\,v_2, bs_2)$\\
+ − 1398
$\textit{decode}'\,(\Z\!::\!bs)\,(r^*)$ & $\dn$ & $(\Stars\,[], bs)$\\
+ − 1399
$\textit{decode}'\,(\S\!::\!bs)\,(r^*)$ & $\dn$ &
+ − 1400
$\textit{let}\,(v, bs_1) = \textit{decode}'\,bs\,r\;\textit{in}$\\
+ − 1401
& & $\textit{let}\,(\Stars\,vs, bs_2) = \textit{decode}'\,bs_1\,r^*$\\
+ − 1402
& & \hspace{35mm}$\textit{in}\;(\Stars\,v\!::\!vs, bs_2)$\bigskip\\
+ − 1403
+ − 1404
$\textit{decode}\,bs\,r$ & $\dn$ &
+ − 1405
$\textit{let}\,(v, bs') = \textit{decode}'\,bs\,r\;\textit{in}$\\
+ − 1406
& & $\textit{if}\;bs' = []\;\textit{then}\;\textit{Some}\,v\;
+ − 1407
\textit{else}\;\textit{None}$
+ − 1408
\end{tabular}
+ − 1409
\end{center}
+ − 1410
%\end{definition}
+ − 1411
+ − 1412
Sulzmann and Lu's integrated the bitcodes into regular expressions to
+ − 1413
create annotated regular expressions \cite{Sulzmann2014}.
+ − 1414
\emph{Annotated regular expressions} are defined by the following
+ − 1415
grammar:%\comment{ALTS should have an $as$ in the definitions, not just $a_1$ and $a_2$}
+ − 1416
+ − 1417
\begin{center}
+ − 1418
\begin{tabular}{lcl}
+ − 1419
$\textit{a}$ & $::=$ & $\textit{ZERO}$\\
+ − 1420
& $\mid$ & $\textit{ONE}\;\;bs$\\
+ − 1421
& $\mid$ & $\textit{CHAR}\;\;bs\,c$\\
+ − 1422
& $\mid$ & $\textit{ALTS}\;\;bs\,as$\\
+ − 1423
& $\mid$ & $\textit{SEQ}\;\;bs\,a_1\,a_2$\\
+ − 1424
& $\mid$ & $\textit{STAR}\;\;bs\,a$
+ − 1425
\end{tabular}
+ − 1426
\end{center}
+ − 1427
%(in \textit{ALTS})
+ − 1428
+ − 1429
\noindent
+ − 1430
where $bs$ stands for bitcodes, $a$ for $\bold{a}$nnotated regular
+ − 1431
expressions and $as$ for a list of annotated regular expressions.
+ − 1432
The alternative constructor($\textit{ALTS}$) has been generalized to
+ − 1433
accept a list of annotated regular expressions rather than just 2.
+ − 1434
We will show that these bitcodes encode information about
+ − 1435
the (POSIX) value that should be generated by the Sulzmann and Lu
+ − 1436
algorithm.
+ − 1437
+ − 1438
+ − 1439
To do lexing using annotated regular expressions, we shall first
+ − 1440
transform the usual (un-annotated) regular expressions into annotated
+ − 1441
regular expressions. This operation is called \emph{internalisation} and
+ − 1442
defined as follows:
+ − 1443
+ − 1444
%\begin{definition}
+ − 1445
\begin{center}
+ − 1446
\begin{tabular}{lcl}
+ − 1447
$(\ZERO)^\uparrow$ & $\dn$ & $\textit{ZERO}$\\
+ − 1448
$(\ONE)^\uparrow$ & $\dn$ & $\textit{ONE}\,[]$\\
+ − 1449
$(c)^\uparrow$ & $\dn$ & $\textit{CHAR}\,[]\,c$\\
+ − 1450
$(r_1 + r_2)^\uparrow$ & $\dn$ &
+ − 1451
$\textit{ALTS}\;[]\,List((\textit{fuse}\,[\Z]\,r_1^\uparrow),\,
+ − 1452
(\textit{fuse}\,[\S]\,r_2^\uparrow))$\\
+ − 1453
$(r_1\cdot r_2)^\uparrow$ & $\dn$ &
+ − 1454
$\textit{SEQ}\;[]\,r_1^\uparrow\,r_2^\uparrow$\\
+ − 1455
$(r^*)^\uparrow$ & $\dn$ &
+ − 1456
$\textit{STAR}\;[]\,r^\uparrow$\\
+ − 1457
\end{tabular}
+ − 1458
\end{center}
+ − 1459
%\end{definition}
+ − 1460
+ − 1461
\noindent
+ − 1462
We use up arrows here to indicate that the basic un-annotated regular
+ − 1463
expressions are ``lifted up'' into something slightly more complex. In the
+ − 1464
fourth clause, $\textit{fuse}$ is an auxiliary function that helps to
+ − 1465
attach bits to the front of an annotated regular expression. Its
+ − 1466
definition is as follows:
+ − 1467
+ − 1468
\begin{center}
+ − 1469
\begin{tabular}{lcl}
+ − 1470
$\textit{fuse}\;bs\,(\textit{ZERO})$ & $\dn$ & $\textit{ZERO}$\\
+ − 1471
$\textit{fuse}\;bs\,(\textit{ONE}\,bs')$ & $\dn$ &
+ − 1472
$\textit{ONE}\,(bs\,@\,bs')$\\
+ − 1473
$\textit{fuse}\;bs\,(\textit{CHAR}\,bs'\,c)$ & $\dn$ &
+ − 1474
$\textit{CHAR}\,(bs\,@\,bs')\,c$\\
+ − 1475
$\textit{fuse}\;bs\,(\textit{ALTS}\,bs'\,as)$ & $\dn$ &
+ − 1476
$\textit{ALTS}\,(bs\,@\,bs')\,as$\\
+ − 1477
$\textit{fuse}\;bs\,(\textit{SEQ}\,bs'\,a_1\,a_2)$ & $\dn$ &
+ − 1478
$\textit{SEQ}\,(bs\,@\,bs')\,a_1\,a_2$\\
+ − 1479
$\textit{fuse}\;bs\,(\textit{STAR}\,bs'\,a)$ & $\dn$ &
+ − 1480
$\textit{STAR}\,(bs\,@\,bs')\,a$
+ − 1481
\end{tabular}
+ − 1482
\end{center}
+ − 1483
+ − 1484
\noindent
+ − 1485
After internalising the regular expression, we perform successive
+ − 1486
derivative operations on the annotated regular expressions. This
+ − 1487
derivative operation is the same as what we had previously for the
+ − 1488
basic regular expressions, except that we beed to take care of
+ − 1489
the bitcodes:
+ − 1490
+ − 1491
%\begin{definition}{bder}
+ − 1492
\begin{center}
+ − 1493
\begin{tabular}{@{}lcl@{}}
+ − 1494
$(\textit{ZERO})\,\backslash c$ & $\dn$ & $\textit{ZERO}$\\
+ − 1495
$(\textit{ONE}\;bs)\,\backslash c$ & $\dn$ & $\textit{ZERO}$\\
+ − 1496
$(\textit{CHAR}\;bs\,d)\,\backslash c$ & $\dn$ &
+ − 1497
$\textit{if}\;c=d\; \;\textit{then}\;
+ − 1498
\textit{ONE}\;bs\;\textit{else}\;\textit{ZERO}$\\
+ − 1499
$(\textit{ALTS}\;bs\,as)\,\backslash c$ & $\dn$ &
+ − 1500
$\textit{ALTS}\;bs\,(as.map(\backslash c))$\\
+ − 1501
$(\textit{SEQ}\;bs\,a_1\,a_2)\,\backslash c$ & $\dn$ &
+ − 1502
$\textit{if}\;\textit{bnullable}\,a_1$\\
+ − 1503
& &$\textit{then}\;\textit{ALTS}\,bs\,List((\textit{SEQ}\,[]\,(a_1\,\backslash c)\,a_2),$\\
+ − 1504
& &$\phantom{\textit{then}\;\textit{ALTS}\,bs\,}(\textit{fuse}\,(\textit{bmkeps}\,a_1)\,(a_2\,\backslash c)))$\\
+ − 1505
& &$\textit{else}\;\textit{SEQ}\,bs\,(a_1\,\backslash c)\,a_2$\\
+ − 1506
$(\textit{STAR}\,bs\,a)\,\backslash c$ & $\dn$ &
+ − 1507
$\textit{SEQ}\;bs\,(\textit{fuse}\, [\Z] (r\,\backslash c))\,
+ − 1508
(\textit{STAR}\,[]\,r)$
+ − 1509
\end{tabular}
+ − 1510
\end{center}
+ − 1511
%\end{definition}
+ − 1512
+ − 1513
\noindent
+ − 1514
For instance, when we unfold $\textit{STAR} \; bs \; a$ into a sequence,
+ − 1515
we need to attach an additional bit $Z$ to the front of $r \backslash c$
+ − 1516
to indicate that there is one more star iteration. Also the $SEQ$ clause
+ − 1517
is more subtle---when $a_1$ is $\textit{bnullable}$ (here
+ − 1518
\textit{bnullable} is exactly the same as $\textit{nullable}$, except
+ − 1519
that it is for annotated regular expressions, therefore we omit the
+ − 1520
definition). Assume that $bmkeps$ correctly extracts the bitcode for how
+ − 1521
$a_1$ matches the string prior to character $c$ (more on this later),
+ − 1522
then the right branch of $ALTS$, which is $fuse \; bmkeps \; a_1 (a_2
+ − 1523
\backslash c)$ will collapse the regular expression $a_1$(as it has
+ − 1524
already been fully matched) and store the parsing information at the
+ − 1525
head of the regular expression $a_2 \backslash c$ by fusing to it. The
+ − 1526
bitsequence $bs$, which was initially attached to the head of $SEQ$, has
+ − 1527
now been elevated to the top-level of $ALTS$, as this information will be
+ − 1528
needed whichever way the $SEQ$ is matched---no matter whether $c$ belongs
+ − 1529
to $a_1$ or $ a_2$. After building these derivatives and maintaining all
+ − 1530
the lexing information, we complete the lexing by collecting the
+ − 1531
bitcodes using a generalised version of the $\textit{mkeps}$ function
+ − 1532
for annotated regular expressions, called $\textit{bmkeps}$:
+ − 1533
+ − 1534
+ − 1535
%\begin{definition}[\textit{bmkeps}]\mbox{}
+ − 1536
\begin{center}
+ − 1537
\begin{tabular}{lcl}
+ − 1538
$\textit{bmkeps}\,(\textit{ONE}\;bs)$ & $\dn$ & $bs$\\
+ − 1539
$\textit{bmkeps}\,(\textit{ALTS}\;bs\,a::as)$ & $\dn$ &
+ − 1540
$\textit{if}\;\textit{bnullable}\,a$\\
+ − 1541
& &$\textit{then}\;bs\,@\,\textit{bmkeps}\,a$\\
+ − 1542
& &$\textit{else}\;bs\,@\,\textit{bmkeps}\,(\textit{ALTS}\;bs\,as)$\\
+ − 1543
$\textit{bmkeps}\,(\textit{SEQ}\;bs\,a_1\,a_2)$ & $\dn$ &
+ − 1544
$bs \,@\,\textit{bmkeps}\,a_1\,@\, \textit{bmkeps}\,a_2$\\
+ − 1545
$\textit{bmkeps}\,(\textit{STAR}\;bs\,a)$ & $\dn$ &
+ − 1546
$bs \,@\, [\S]$
+ − 1547
\end{tabular}
+ − 1548
\end{center}
+ − 1549
%\end{definition}
+ − 1550
+ − 1551
\noindent
+ − 1552
This function completes the value information by travelling along the
+ − 1553
path of the regular expression that corresponds to a POSIX value and
+ − 1554
collecting all the bitcodes, and using $S$ to indicate the end of star
+ − 1555
iterations. If we take the bitcodes produced by $\textit{bmkeps}$ and
+ − 1556
decode them, we get the value we expect. The corresponding lexing
+ − 1557
algorithm looks as follows:
+ − 1558
+ − 1559
\begin{center}
+ − 1560
\begin{tabular}{lcl}
+ − 1561
$\textit{blexer}\;r\,s$ & $\dn$ &
+ − 1562
$\textit{let}\;a = (r^\uparrow)\backslash s\;\textit{in}$\\
+ − 1563
& & $\;\;\textit{if}\; \textit{bnullable}(a)$\\
+ − 1564
& & $\;\;\textit{then}\;\textit{decode}\,(\textit{bmkeps}\,a)\,r$\\
+ − 1565
& & $\;\;\textit{else}\;\textit{None}$
+ − 1566
\end{tabular}
+ − 1567
\end{center}
+ − 1568
+ − 1569
\noindent
+ − 1570
In this definition $\_\backslash s$ is the generalisation of the derivative
+ − 1571
operation from characters to strings (just like the derivatives for un-annotated
+ − 1572
regular expressions).
+ − 1573
+ − 1574
The main point of the bitcodes and annotated regular expressions is that
+ − 1575
we can apply rather aggressive (in terms of size) simplification rules
+ − 1576
in order to keep derivatives small. We have developed such
+ − 1577
``aggressive'' simplification rules and generated test data that show
+ − 1578
that the expected bound can be achieved. Obviously we could only
+ − 1579
partially cover the search space as there are infinitely many regular
+ − 1580
expressions and strings.
+ − 1581
+ − 1582
One modification we introduced is to allow a list of annotated regular
+ − 1583
expressions in the \textit{ALTS} constructor. This allows us to not just
+ − 1584
delete unnecessary $\ZERO$s and $\ONE$s from regular expressions, but
+ − 1585
also unnecessary ``copies'' of regular expressions (very similar to
+ − 1586
simplifying $r + r$ to just $r$, but in a more general setting). Another
+ − 1587
modification is that we use simplification rules inspired by Antimirov's
+ − 1588
work on partial derivatives. They maintain the idea that only the first
+ − 1589
``copy'' of a regular expression in an alternative contributes to the
+ − 1590
calculation of a POSIX value. All subsequent copies can be pruned away from
+ − 1591
the regular expression. A recursive definition of our simplification function
+ − 1592
that looks somewhat similar to our Scala code is given below:
+ − 1593
%\comment{Use $\ZERO$, $\ONE$ and so on.
+ − 1594
%Is it $ALTS$ or $ALTS$?}\\
+ − 1595
+ − 1596
\begin{center}
+ − 1597
\begin{tabular}{@{}lcl@{}}
+ − 1598
+ − 1599
$\textit{simp} \; (\textit{SEQ}\;bs\,a_1\,a_2)$ & $\dn$ & $ (\textit{simp} \; a_1, \textit{simp} \; a_2) \; \textit{match} $ \\
+ − 1600
&&$\quad\textit{case} \; (\ZERO, \_) \Rightarrow \ZERO$ \\
+ − 1601
&&$\quad\textit{case} \; (\_, \ZERO) \Rightarrow \ZERO$ \\
+ − 1602
&&$\quad\textit{case} \; (\ONE, a_2') \Rightarrow \textit{fuse} \; bs \; a_2'$ \\
+ − 1603
&&$\quad\textit{case} \; (a_1', \ONE) \Rightarrow \textit{fuse} \; bs \; a_1'$ \\
+ − 1604
&&$\quad\textit{case} \; (a_1', a_2') \Rightarrow \textit{SEQ} \; bs \; a_1' \; a_2'$ \\
+ − 1605
+ − 1606
$\textit{simp} \; (\textit{ALTS}\;bs\,as)$ & $\dn$ & $\textit{distinct}( \textit{flatten} ( \textit{map simp as})) \; \textit{match} $ \\
+ − 1607
&&$\quad\textit{case} \; [] \Rightarrow \ZERO$ \\
+ − 1608
&&$\quad\textit{case} \; a :: [] \Rightarrow \textit{fuse bs a}$ \\
+ − 1609
&&$\quad\textit{case} \; as' \Rightarrow \textit{ALTS}\;bs\;as'$\\
+ − 1610
+ − 1611
$\textit{simp} \; a$ & $\dn$ & $\textit{a} \qquad \textit{otherwise}$
+ − 1612
\end{tabular}
+ − 1613
\end{center}
+ − 1614
+ − 1615
\noindent
+ − 1616
The simplification does a pattern matching on the regular expression.
+ − 1617
When it detected that the regular expression is an alternative or
+ − 1618
sequence, it will try to simplify its children regular expressions
+ − 1619
recursively and then see if one of the children turn into $\ZERO$ or
+ − 1620
$\ONE$, which might trigger further simplification at the current level.
+ − 1621
The most involved part is the $\textit{ALTS}$ clause, where we use two
+ − 1622
auxiliary functions $\textit{flatten}$ and $\textit{distinct}$ to open up nested
+ − 1623
$\textit{ALTS}$ and reduce as many duplicates as possible. Function
+ − 1624
$\textit{distinct}$ keeps the first occurring copy only and remove all later ones
+ − 1625
when detected duplicates. Function $\textit{flatten}$ opens up nested \textit{ALTS}.
+ − 1626
Its recursive definition is given below:
+ − 1627
+ − 1628
\begin{center}
+ − 1629
\begin{tabular}{@{}lcl@{}}
+ − 1630
$\textit{flatten} \; (\textit{ALTS}\;bs\,as) :: as'$ & $\dn$ & $(\textit{map} \;
+ − 1631
(\textit{fuse}\;bs)\; \textit{as}) \; @ \; \textit{flatten} \; as' $ \\
+ − 1632
$\textit{flatten} \; \textit{ZERO} :: as'$ & $\dn$ & $ \textit{flatten} \; as' $ \\
+ − 1633
$\textit{flatten} \; a :: as'$ & $\dn$ & $a :: \textit{flatten} \; as'$ \quad(otherwise)
+ − 1634
\end{tabular}
+ − 1635
\end{center}
+ − 1636
+ − 1637
\noindent
+ − 1638
Here $\textit{flatten}$ behaves like the traditional functional programming flatten
+ − 1639
function, except that it also removes $\ZERO$s. Or in terms of regular expressions, it
+ − 1640
removes parentheses, for example changing $a+(b+c)$ into $a+b+c$.
+ − 1641
+ − 1642
Suppose we apply simplification after each derivative step, and view
+ − 1643
these two operations as an atomic one: $a \backslash_{simp}\,c \dn
+ − 1644
\textit{simp}(a \backslash c)$. Then we can use the previous natural
+ − 1645
extension from derivative w.r.t.~character to derivative
+ − 1646
w.r.t.~string:%\comment{simp in the [] case?}
+ − 1647
+ − 1648
\begin{center}
+ − 1649
\begin{tabular}{lcl}
+ − 1650
$r \backslash_{simp} (c\!::\!s) $ & $\dn$ & $(r \backslash_{simp}\, c) \backslash_{simp}\, s$ \\
+ − 1651
$r \backslash_{simp} [\,] $ & $\dn$ & $r$
+ − 1652
\end{tabular}
+ − 1653
\end{center}
+ − 1654
+ − 1655
\noindent
+ − 1656
we obtain an optimised version of the algorithm:
+ − 1657
+ − 1658
\begin{center}
+ − 1659
\begin{tabular}{lcl}
+ − 1660
$\textit{blexer\_simp}\;r\,s$ & $\dn$ &
+ − 1661
$\textit{let}\;a = (r^\uparrow)\backslash_{simp}\, s\;\textit{in}$\\
+ − 1662
& & $\;\;\textit{if}\; \textit{bnullable}(a)$\\
+ − 1663
& & $\;\;\textit{then}\;\textit{decode}\,(\textit{bmkeps}\,a)\,r$\\
+ − 1664
& & $\;\;\textit{else}\;\textit{None}$
+ − 1665
\end{tabular}
+ − 1666
\end{center}
+ − 1667
+ − 1668
\noindent
+ − 1669
This algorithm keeps the regular expression size small, for example,
+ − 1670
with this simplification our previous $(a + aa)^*$ example's 8000 nodes
+ − 1671
will be reduced to just 6 and stays constant, no matter how long the
+ − 1672
input string is.
+ − 1673
+ − 1674
+ − 1675
+ − 1676
\section{Current Work}
+ − 1677
+ − 1678
We are currently engaged in two tasks related to this algorithm. The
+ − 1679
first task is proving that our simplification rules actually do not
+ − 1680
affect the POSIX value that should be generated by the algorithm
+ − 1681
according to the specification of a POSIX value and furthermore obtain a
+ − 1682
much tighter bound on the sizes of derivatives. The result is that our
+ − 1683
algorithm should be correct and faster on all inputs. The original
+ − 1684
blow-up, as observed in JavaScript, Python and Java, would be excluded
+ − 1685
from happening in our algorithm. For this proof we use the theorem prover
+ − 1686
Isabelle. Once completed, this result will advance the state-of-the-art:
+ − 1687
Sulzmann and Lu wrote in their paper~\cite{Sulzmann2014} about the
+ − 1688
bitcoded ``incremental parsing method'' (that is the lexing algorithm
+ − 1689
outlined in this section):
+ − 1690
+ − 1691
\begin{quote}\it
+ − 1692
``Correctness Claim: We further claim that the incremental parsing
+ − 1693
method in Figure~5 in combination with the simplification steps in
+ − 1694
Figure 6 yields POSIX parse tree [our lexical values]. We have tested this claim
+ − 1695
extensively by using the method in Figure~3 as a reference but yet
+ − 1696
have to work out all proof details.''
+ − 1697
\end{quote}
+ − 1698
+ − 1699
\noindent
+ − 1700
We like to settle this correctness claim. It is relatively
+ − 1701
straightforward to establish that after one simplification step, the part of a
+ − 1702
nullable derivative that corresponds to a POSIX value remains intact and can
+ − 1703
still be collected, in other words, we can show that
+ − 1704
%\comment{Double-check....I
+ − 1705
%think this is not the case}
+ − 1706
%\comment{If i remember correctly, you have proved this lemma.
+ − 1707
%I feel this is indeed not true because you might place arbitrary
+ − 1708
%bits on the regex r, however if this is the case, did i remember wrongly that
+ − 1709
%you proved something like simplification does not affect $\textit{bmkeps}$ results?
+ − 1710
%Anyway, i have amended this a little bit so it does not allow arbitrary bits attached
+ − 1711
%to a regex. Maybe it works now.}
+ − 1712
+ − 1713
\begin{center}
+ − 1714
$\textit{bmkeps} \; a = \textit{bmkeps} \; \textit{bsimp} \; a\;($\textit{provided}$ \; a\; is \; \textit{bnullable} )$
+ − 1715
\end{center}
+ − 1716
+ − 1717
\noindent
+ − 1718
as this basically comes down to proving actions like removing the
+ − 1719
additional $r$ in $r+r$ does not delete important POSIX information in
+ − 1720
a regular expression. The hard part of this proof is to establish that
+ − 1721
+ − 1722
\begin{center}
+ − 1723
$ \textit{blexer}\_{simp}(r, \; s) = \textit{blexer}(r, \; s)$
+ − 1724
\end{center}
+ − 1725
%comment{This is not true either...look at the definion blexer/blexer-simp}
+ − 1726
+ − 1727
\noindent That is, if we do derivative on regular expression $r$ and then
+ − 1728
simplify it, and repeat this process until we exhaust the string, we get a
+ − 1729
regular expression $r''$($\textit{LHS}$) that provides the POSIX matching
+ − 1730
information, which is exactly the same as the result $r'$($\textit{RHS}$ of the
+ − 1731
normal derivative algorithm that only does derivative repeatedly and has no
+ − 1732
simplification at all. This might seem at first glance very unintuitive, as
+ − 1733
the $r'$ could be exponentially larger than $r''$, but can be explained in the
+ − 1734
following way: we are pruning away the possible matches that are not POSIX.
+ − 1735
Since there could be exponentially many
+ − 1736
non-POSIX matchings and only 1 POSIX matching, it
+ − 1737
is understandable that our $r''$ can be a lot smaller. we can still provide
+ − 1738
the same POSIX value if there is one. This is not as straightforward as the
+ − 1739
previous proposition, as the two regular expressions $r'$ and $r''$ might have
+ − 1740
become very different. The crucial point is to find the
+ − 1741
$\textit{POSIX}$ information of a regular expression and how it is modified,
+ − 1742
augmented and propagated
+ − 1743
during simplification in parallel with the regular expression that
+ − 1744
has not been simplified in the subsequent derivative operations. To aid this,
+ − 1745
we use the helper function retrieve described by Sulzmann and Lu:
+ − 1746
\begin{center}
+ − 1747
\begin{tabular}{@{}l@{\hspace{2mm}}c@{\hspace{2mm}}l@{}}
+ − 1748
$\textit{retrieve}\,(\textit{ONE}\,bs)\,\Empty$ & $\dn$ & $bs$\\
+ − 1749
$\textit{retrieve}\,(\textit{CHAR}\,bs\,c)\,(\Char\,d)$ & $\dn$ & $bs$\\
+ − 1750
$\textit{retrieve}\,(\textit{ALTS}\,bs\,a::as)\,(\Left\,v)$ & $\dn$ &
+ − 1751
$bs \,@\, \textit{retrieve}\,a\,v$\\
+ − 1752
$\textit{retrieve}\,(\textit{ALTS}\,bs\,a::as)\,(\Right\,v)$ & $\dn$ &
+ − 1753
$bs \,@\, \textit{retrieve}\,(\textit{ALTS}\,bs\,as)\,v$\\
+ − 1754
$\textit{retrieve}\,(\textit{SEQ}\,bs\,a_1\,a_2)\,(\Seq\,v_1\,v_2)$ & $\dn$ &
+ − 1755
$bs \,@\,\textit{retrieve}\,a_1\,v_1\,@\, \textit{retrieve}\,a_2\,v_2$\\
+ − 1756
$\textit{retrieve}\,(\textit{STAR}\,bs\,a)\,(\Stars\,[])$ & $\dn$ &
+ − 1757
$bs \,@\, [\S]$\\
+ − 1758
$\textit{retrieve}\,(\textit{STAR}\,bs\,a)\,(\Stars\,(v\!::\!vs))$ & $\dn$ &\\
+ − 1759
\multicolumn{3}{l}{
+ − 1760
\hspace{3cm}$bs \,@\, [\Z] \,@\, \textit{retrieve}\,a\,v\,@\,
+ − 1761
\textit{retrieve}\,(\textit{STAR}\,[]\,a)\,(\Stars\,vs)$}\\
+ − 1762
\end{tabular}
+ − 1763
\end{center}
+ − 1764
%\comment{Did not read further}\\
+ − 1765
This function assembles the bitcode
+ − 1766
%that corresponds to a lexical value for how
+ − 1767
%the current derivative matches the suffix of the string(the characters that
+ − 1768
%have not yet appeared, but will appear as the successive derivatives go on.
+ − 1769
%How do we get this "future" information? By the value $v$, which is
+ − 1770
%computed by a pass of the algorithm that uses
+ − 1771
%$inj$ as described in the previous section).
+ − 1772
using information from both the derivative regular expression and the
+ − 1773
value. Sulzmann and Lu poroposed this function, but did not prove
+ − 1774
anything about it. Ausaf and Urban used it to connect the bitcoded
+ − 1775
algorithm to the older algorithm by the following equation:
+ − 1776
+ − 1777
\begin{center} $inj \;a\; c \; v = \textit{decode} \; (\textit{retrieve}\;
+ − 1778
(r^\uparrow)\backslash_{simp} \,c)\,v)$
+ − 1779
\end{center}
+ − 1780
+ − 1781
\noindent
+ − 1782
whereby $r^\uparrow$ stands for the internalised version of $r$. Ausaf
+ − 1783
and Urban also used this fact to prove the correctness of bitcoded
+ − 1784
algorithm without simplification. Our purpose of using this, however,
+ − 1785
is to establish
+ − 1786
+ − 1787
\begin{center}
+ − 1788
$ \textit{retrieve} \;
+ − 1789
a \; v \;=\; \textit{retrieve} \; (\textit{simp}\,a) \; v'.$
+ − 1790
\end{center}
+ − 1791
The idea is that using $v'$, a simplified version of $v$ that had gone
+ − 1792
through the same simplification step as $\textit{simp}(a)$, we are able
+ − 1793
to extract the bitcode that gives the same parsing information as the
+ − 1794
unsimplified one. However, we noticed that constructing such a $v'$
+ − 1795
from $v$ is not so straightforward. The point of this is that we might
+ − 1796
be able to finally bridge the gap by proving
+ − 1797
+ − 1798
\begin{center}
+ − 1799
$\textit{retrieve} \; (r^\uparrow \backslash s) \; v = \;\textit{retrieve} \;
+ − 1800
(\textit{simp}(r^\uparrow) \backslash s) \; v'$
+ − 1801
\end{center}
+ − 1802
+ − 1803
\noindent
+ − 1804
and subsequently
+ − 1805
+ − 1806
\begin{center}
+ − 1807
$\textit{retrieve} \; (r^\uparrow \backslash s) \; v\; = \; \textit{retrieve} \;
+ − 1808
(r^\uparrow \backslash_{simp} \, s) \; v'$.
+ − 1809
\end{center}
+ − 1810
+ − 1811
\noindent
+ − 1812
The $\textit{LHS}$ of the above equation is the bitcode we want. This
+ − 1813
would prove that our simplified version of regular expression still
+ − 1814
contains all the bitcodes needed. The task here is to find a way to
+ − 1815
compute the correct $v'$.
+ − 1816
+ − 1817
The second task is to speed up the more aggressive simplification. Currently
+ − 1818
it is slower than the original naive simplification by Ausaf and Urban (the
+ − 1819
naive version as implemented by Ausaf and Urban of course can ``explode'' in
+ − 1820
some cases). It is therefore not surprising that the speed is also much slower
+ − 1821
than regular expression engines in popular programming languages such as Java
+ − 1822
and Python on most inputs that are linear. For example, just by rewriting the
+ − 1823
example regular expression in the beginning of this report $(a^*)^*\,b$ into
+ − 1824
$a^*\,b$ would eliminate the ambiguity in the matching and make the time
+ − 1825
for matching linear with respect to the input string size. This allows the
+ − 1826
DFA approach to become blindingly fast, and dwarf the speed of our current
+ − 1827
implementation. For example, here is a comparison of Java regex engine
+ − 1828
and our implementation on this example.
+ − 1829
+ − 1830
\begin{center}
+ − 1831
\begin{tabular}{@{}c@{\hspace{0mm}}c@{\hspace{0mm}}c@{}}
+ − 1832
\begin{tikzpicture}
+ − 1833
\begin{axis}[
+ − 1834
xlabel={$n*1000$},
+ − 1835
x label style={at={(1.05,-0.05)}},
+ − 1836
ylabel={time in secs},
+ − 1837
enlargelimits=false,
+ − 1838
xtick={0,5,...,30},
+ − 1839
xmax=33,
+ − 1840
ymax=9,
+ − 1841
scaled ticks=true,
+ − 1842
axis lines=left,
+ − 1843
width=5cm,
+ − 1844
height=4cm,
+ − 1845
legend entries={Bitcoded Algorithm},
+ − 1846
legend pos=north west,
+ − 1847
legend cell align=left]
+ − 1848
\addplot[red,mark=*, mark options={fill=white}] table {bad-scala.data};
+ − 1849
\end{axis}
+ − 1850
\end{tikzpicture}
+ − 1851
&
+ − 1852
\begin{tikzpicture}
+ − 1853
\begin{axis}[
+ − 1854
xlabel={$n*1000$},
+ − 1855
x label style={at={(1.05,-0.05)}},
+ − 1856
%ylabel={time in secs},
+ − 1857
enlargelimits=false,
+ − 1858
xtick={0,5,...,30},
+ − 1859
xmax=33,
+ − 1860
ymax=9,
+ − 1861
scaled ticks=false,
+ − 1862
axis lines=left,
+ − 1863
width=5cm,
+ − 1864
height=4cm,
+ − 1865
legend entries={Java},
+ − 1866
legend pos=north west,
+ − 1867
legend cell align=left]
+ − 1868
\addplot[cyan,mark=*, mark options={fill=white}] table {good-java.data};
+ − 1869
\end{axis}
+ − 1870
\end{tikzpicture}\\
+ − 1871
\multicolumn{3}{c}{Graphs: Runtime for matching $a^*\,b$ with strings
+ − 1872
of the form $\underbrace{aa..a}_{n}$.}
+ − 1873
\end{tabular}
+ − 1874
\end{center}
+ − 1875
+ − 1876
+ − 1877
Java regex engine can match string of thousands of characters in a few milliseconds,
+ − 1878
whereas our current algorithm gets excruciatingly slow on input of this size.
+ − 1879
The running time in theory is linear, however it does not appear to be the
+ − 1880
case in an actual implementation. So it needs to be explored how to
+ − 1881
make our algorithm faster on all inputs. It could be the recursive calls that are
+ − 1882
needed to manipulate bits that are causing the slow down. A possible solution
+ − 1883
is to write recursive functions into tail-recusive form.
+ − 1884
Another possibility would be to explore
+ − 1885
again the connection to DFAs to speed up the algorithm on
+ − 1886
subcalls that are small enough. This is very much work in progress.
+ − 1887
+ − 1888
\section{Conclusion}
+ − 1889
+ − 1890
In this PhD-project we are interested in fast algorithms for regular
+ − 1891
expression matching. While this seems to be a ``settled'' area, in
+ − 1892
fact interesting research questions are popping up as soon as one steps
+ − 1893
outside the classic automata theory (for example in terms of what kind
+ − 1894
of regular expressions are supported). The reason why it is
+ − 1895
interesting for us to look at the derivative approach introduced by
+ − 1896
Brzozowski for regular expression matching, and then much further
+ − 1897
developed by Sulzmann and Lu, is that derivatives can elegantly deal
+ − 1898
with some of the regular expressions that are of interest in ``real
+ − 1899
life''. This includes the not-regular expression, written $\neg\,r$
+ − 1900
(that is all strings that are not recognised by $r$), but also bounded
+ − 1901
regular expressions such as $r^{\{n\}}$ and $r^{\{n..m\}}$). There is
+ − 1902
also hope that the derivatives can provide another angle for how to
+ − 1903
deal more efficiently with back-references, which are one of the
+ − 1904
reasons why regular expression engines in JavaScript, Python and Java
+ − 1905
choose to not implement the classic automata approach of transforming
+ − 1906
regular expressions into NFAs and then DFAs---because we simply do not
+ − 1907
know how such back-references can be represented by DFAs.
+ − 1908
We also plan to implement the bitcoded algorithm
+ − 1909
in some imperative language like C to see if the inefficiency of the
+ − 1910
Scala implementation
+ − 1911
is language specific. To make this research more comprehensive we also plan
+ − 1912
to contrast our (faster) version of bitcoded algorithm with the
+ − 1913
Symbolic Regex Matcher, the RE2, the Rust Regex Engine, and the static
+ − 1914
analysis approach by implementing them in the same language and then compare
+ − 1915
their performance.
+ − 1916
+ − 1917
\bibliographystyle{plain}
+ − 1918
\bibliography{root}
+ − 1919
+ − 1920
+ − 1921
\end{document}