author | Chengsong |
Tue, 16 Jul 2019 22:20:11 +0100 | |
changeset 76 | f575cf219377 |
parent 75 | 24d9d64c2a95 |
parent 74 | 9e791ef6022f |
child 77 | 058133a9ffe0 |
permissions | -rw-r--r-- |
45 | 1 |
\documentclass[a4paper,UKenglish]{lipics} |
30 | 2 |
\usepackage{graphic} |
3 |
\usepackage{data} |
|
4 |
\usepackage{tikz-cd} |
|
63 | 5 |
%\usepackage{algorithm} |
35 | 6 |
\usepackage{amsmath} |
7 |
\usepackage[noend]{algpseudocode} |
|
42 | 8 |
\usepackage{enumitem} |
70 | 9 |
\usepackage{nccmath} |
63 | 10 |
|
11 |
\definecolor{darkblue}{rgb}{0,0,0.6} |
|
12 |
\hypersetup{colorlinks=true,allcolors=darkblue} |
|
70 | 13 |
\newcommand{\comment}[1]% |
14 |
{{\color{red}$\Rightarrow$}\marginpar{\raggedright\small{\bf\color{red}#1}}} |
|
15 |
||
30 | 16 |
% \documentclass{article} |
17 |
%\usepackage[utf8]{inputenc} |
|
18 |
%\usepackage[english]{babel} |
|
19 |
%\usepackage{listings} |
|
20 |
% \usepackage{amsthm} |
|
63 | 21 |
%\usepackage{hyperref} |
30 | 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}} |
|
36 |
\def\lexer{\mathit{lexer}} |
|
37 |
\def\mkeps{\mathit{mkeps}} |
|
38 |
\def\inj{\mathit{inj}} |
|
39 |
\def\Empty{\mathit{Empty}} |
|
40 |
\def\Left{\mathit{Left}} |
|
41 |
\def\Right{\mathit{Right}} |
|
42 |
\def\Stars{\mathit{Stars}} |
|
43 |
\def\Char{\mathit{Char}} |
|
44 |
\def\Seq{\mathit{Seq}} |
|
45 |
\def\Der{\mathit{Der}} |
|
46 |
\def\nullable{\mathit{nullable}} |
|
47 |
\def\Z{\mathit{Z}} |
|
48 |
\def\S{\mathit{S}} |
|
49 |
||
50 |
%\theoremstyle{theorem} |
|
51 |
%\newtheorem{theorem}{Theorem} |
|
52 |
%\theoremstyle{lemma} |
|
53 |
%\newtheorem{lemma}{Lemma} |
|
54 |
%\newcommand{\lemmaautorefname}{Lemma} |
|
55 |
%\theoremstyle{definition} |
|
56 |
%\newtheorem{definition}{Definition} |
|
35 | 57 |
\algnewcommand\algorithmicswitch{\textbf{switch}} |
58 |
\algnewcommand\algorithmiccase{\textbf{case}} |
|
59 |
\algnewcommand\algorithmicassert{\texttt{assert}} |
|
60 |
\algnewcommand\Assert[1]{\State \algorithmicassert(#1)}% |
|
61 |
% New "environments" |
|
62 |
\algdef{SE}[SWITCH]{Switch}{EndSwitch}[1]{\algorithmicswitch\ #1\ \algorithmicdo}{\algorithmicend\ \algorithmicswitch}% |
|
63 |
\algdef{SE}[CASE]{Case}{EndCase}[1]{\algorithmiccase\ #1}{\algorithmicend\ \algorithmiccase}% |
|
64 |
\algtext*{EndSwitch}% |
|
65 |
\algtext*{EndCase}% |
|
30 | 66 |
|
67 |
||
68 |
\begin{document} |
|
69 |
||
70 |
\maketitle |
|
71 |
||
72 |
\begin{abstract} |
|
73 |
Brzozowski introduced in 1964 a beautifully simple algorithm for |
|
74 |
regular expression matching based on the notion of derivatives of |
|
75 |
regular expressions. In 2014, Sulzmann and Lu extended this |
|
40 | 76 |
algorithm to not just give a YES/NO answer for whether or not a |
64 | 77 |
regular expression matches a string, but in case it does also |
58 | 78 |
answers with \emph{how} it matches the string. This is important for |
40 | 79 |
applications such as lexing (tokenising a string). The problem is to |
80 |
make the algorithm by Sulzmann and Lu fast on all inputs without |
|
81 |
breaking its correctness. We have already developed some |
|
59 | 82 |
simplification rules for this, but have not yet proved that they |
40 | 83 |
preserve the correctness of the algorithm. We also have not yet |
84 |
looked at extended regular expressions, such as bounded repetitions, |
|
85 |
negation and back-references. |
|
30 | 86 |
\end{abstract} |
87 |
||
88 |
\section{Introduction} |
|
89 |
||
70 | 90 |
|
30 | 91 |
This PhD-project is about regular expression matching and |
92 |
lexing. Given the maturity of this topic, the reader might wonder: |
|
93 |
Surely, regular expressions must have already been studied to death? |
|
94 |
What could possibly be \emph{not} known in this area? And surely all |
|
95 |
implemented algorithms for regular expression matching are blindingly |
|
96 |
fast? |
|
97 |
||
98 |
Unfortunately these preconceptions are not supported by evidence: Take |
|
99 |
for example the regular expression $(a^*)^*\,b$ and ask whether |
|
100 |
strings of the form $aa..a$ match this regular |
|
64 | 101 |
expression. Obviously not---the expected $b$ in the last |
30 | 102 |
position is missing. One would expect that modern regular expression |
103 |
matching engines can find this out very quickly. Alas, if one tries |
|
104 |
this example in JavaScript, Python or Java 8 with strings like 28 |
|
105 |
$a$'s, one discovers that this decision takes around 30 seconds and |
|
106 |
takes considerably longer when adding a few more $a$'s, as the graphs |
|
107 |
below show: |
|
108 |
||
109 |
\begin{center} |
|
110 |
\begin{tabular}{@{}c@{\hspace{0mm}}c@{\hspace{0mm}}c@{}} |
|
111 |
\begin{tikzpicture} |
|
112 |
\begin{axis}[ |
|
113 |
xlabel={$n$}, |
|
114 |
x label style={at={(1.05,-0.05)}}, |
|
115 |
ylabel={time in secs}, |
|
116 |
enlargelimits=false, |
|
117 |
xtick={0,5,...,30}, |
|
118 |
xmax=33, |
|
119 |
ymax=35, |
|
120 |
ytick={0,5,...,30}, |
|
121 |
scaled ticks=false, |
|
122 |
axis lines=left, |
|
123 |
width=5cm, |
|
124 |
height=4cm, |
|
125 |
legend entries={JavaScript}, |
|
126 |
legend pos=north west, |
|
127 |
legend cell align=left] |
|
128 |
\addplot[red,mark=*, mark options={fill=white}] table {re-js.data}; |
|
129 |
\end{axis} |
|
130 |
\end{tikzpicture} |
|
131 |
& |
|
132 |
\begin{tikzpicture} |
|
133 |
\begin{axis}[ |
|
134 |
xlabel={$n$}, |
|
135 |
x label style={at={(1.05,-0.05)}}, |
|
136 |
%ylabel={time in secs}, |
|
137 |
enlargelimits=false, |
|
138 |
xtick={0,5,...,30}, |
|
139 |
xmax=33, |
|
140 |
ymax=35, |
|
141 |
ytick={0,5,...,30}, |
|
142 |
scaled ticks=false, |
|
143 |
axis lines=left, |
|
144 |
width=5cm, |
|
145 |
height=4cm, |
|
146 |
legend entries={Python}, |
|
147 |
legend pos=north west, |
|
148 |
legend cell align=left] |
|
149 |
\addplot[blue,mark=*, mark options={fill=white}] table {re-python2.data}; |
|
150 |
\end{axis} |
|
151 |
\end{tikzpicture} |
|
152 |
& |
|
153 |
\begin{tikzpicture} |
|
154 |
\begin{axis}[ |
|
155 |
xlabel={$n$}, |
|
156 |
x label style={at={(1.05,-0.05)}}, |
|
157 |
%ylabel={time in secs}, |
|
158 |
enlargelimits=false, |
|
159 |
xtick={0,5,...,30}, |
|
160 |
xmax=33, |
|
161 |
ymax=35, |
|
162 |
ytick={0,5,...,30}, |
|
163 |
scaled ticks=false, |
|
164 |
axis lines=left, |
|
165 |
width=5cm, |
|
166 |
height=4cm, |
|
167 |
legend entries={Java 8}, |
|
168 |
legend pos=north west, |
|
169 |
legend cell align=left] |
|
170 |
\addplot[cyan,mark=*, mark options={fill=white}] table {re-java.data}; |
|
171 |
\end{axis} |
|
172 |
\end{tikzpicture}\\ |
|
173 |
\multicolumn{3}{c}{Graphs: Runtime for matching $(a^*)^*\,b$ with strings |
|
174 |
of the form $\underbrace{aa..a}_{n}$.} |
|
175 |
\end{tabular} |
|
176 |
\end{center} |
|
177 |
||
58 | 178 |
\noindent These are clearly abysmal and possibly surprising results. One |
64 | 179 |
would expect these systems to do much better than that---after all, |
58 | 180 |
given a DFA and a string, deciding whether a string is matched by this |
181 |
DFA should be linear. |
|
30 | 182 |
|
183 |
Admittedly, the regular expression $(a^*)^*\,b$ is carefully chosen to |
|
64 | 184 |
exhibit this exponential behaviour. Unfortunately, such regular |
185 |
expressions are not just a few outliers. They are actually |
|
186 |
frequent enough to have a separate name created for |
|
30 | 187 |
them---\emph{evil regular expressions}. In empiric work, Davis et al |
188 |
report that they have found thousands of such evil regular expressions |
|
189 |
in the JavaScript and Python ecosystems \cite{Davis18}. |
|
190 |
||
58 | 191 |
This exponential blowup in matching algorithms sometimes causes |
63 | 192 |
considerable grief in real life: for example on 20 July 2016 one evil |
58 | 193 |
regular expression brought the webpage |
194 |
\href{http://stackexchange.com}{Stack Exchange} to its |
|
63 | 195 |
knees.\footnote{\url{https://stackstatus.net/post/147710624694/outage-postmortem-july-20-2016}} |
30 | 196 |
In this instance, a regular expression intended to just trim white |
197 |
spaces from the beginning and the end of a line actually consumed |
|
64 | 198 |
massive amounts of CPU-resources---causing web servers to |
199 |
grind to a halt. This happened when a post with 20,000 white spaces was |
|
58 | 200 |
submitted, but importantly the white spaces were neither at the |
75 | 201 |
beginning nor at the end. |
202 |
As a result, the regular expression matching |
|
203 |
engine needed to backtrack over many choices. |
|
204 |
In this example, the time needed to process the string is not |
|
205 |
exactly the classical exponential case, but rather $O(n^2)$ |
|
206 |
with respect to the string length. But this is enough for the |
|
207 |
home page of stackexchnge to respond not fast enough to |
|
208 |
the load balancer, which thought that there must be some |
|
209 |
attack and therefore stopped the servers from responding to |
|
210 |
requests. This makes the whole site become unavailable. |
|
211 |
Another fresh example that just came out of the oven |
|
212 |
is the cloudfare outage incident. A poorly written |
|
213 |
regular expression exhibited exponential behaviour |
|
214 |
and exhausted CPUs that serve HTTP traffic on 2 July 2019, |
|
215 |
resulting in a 27-minute outage. The regular expression contained |
|
216 |
adjacent Kleene stars, which is the source of the exponential number |
|
217 |
of backtracking possibilities. Although this outage has a series of |
|
218 |
causes that came from different vulnerabilities within the system |
|
219 |
of cloudfare, the heart of the problem lies within regular expression. |
|
220 |
Such outages could be excluded from happening if the matching |
|
221 |
algorithm is guaranteed to be fast.\footnote{\url{https://blog.cloudflare.com/details-of-the-cloudflare-outage-on-july-2-2019/}} |
|
222 |
The underlying problem is |
|
58 | 223 |
that many ``real life'' regular expression matching engines do not use |
75 | 224 |
DFAs for matching. |
225 |
This is because they support regular expressions that |
|
58 | 226 |
are not covered by the classical automata theory, and in this more |
227 |
general setting there are quite a few research questions still |
|
228 |
unanswered and fast algorithms still need to be developed (for example |
|
63 | 229 |
how to treat bounded repetitions, negation and back-references |
230 |
efficiently). |
|
64 | 231 |
%question: dfa can have exponential states. isn't this the actual reason why they do not use dfas? |
232 |
%how do they avoid dfas exponential states if they use them for fast matching? |
|
30 | 233 |
There is also another under-researched problem to do with regular |
234 |
expressions and lexing, i.e.~the process of breaking up strings into |
|
235 |
sequences of tokens according to some regular expressions. In this |
|
236 |
setting one is not just interested in whether or not a regular |
|
64 | 237 |
expression matches a string, but also in \emph{how}. Consider for example a regular expression |
30 | 238 |
$r_{key}$ for recognising keywords such as \textit{if}, \textit{then} |
239 |
and so on; and a regular expression $r_{id}$ for recognising |
|
240 |
identifiers (say, a single character followed by characters or |
|
241 |
numbers). One can then form the compound regular expression |
|
242 |
$(r_{key} + r_{id})^*$ and use it to tokenise strings. But then how |
|
243 |
should the string \textit{iffoo} be tokenised? It could be tokenised |
|
244 |
as a keyword followed by an identifier, or the entire string as a |
|
245 |
single identifier. Similarly, how should the string \textit{if} be |
|
246 |
tokenised? Both regular expressions, $r_{key}$ and $r_{id}$, would |
|
247 |
``fire''---so is it an identifier or a keyword? While in applications |
|
248 |
there is a well-known strategy to decide these questions, called POSIX |
|
249 |
matching, only relatively recently precise definitions of what POSIX |
|
64 | 250 |
matching actually means has been formalised |
46 | 251 |
\cite{AusafDyckhoffUrban2016,OkuiSuzuki2010,Vansummeren2006}. |
252 |
Such a definition has also been given by Sulzmann and Lu \cite{Sulzmann2014}, but the |
|
253 |
corresponding correctness proof turned out to be faulty \cite{AusafDyckhoffUrban2016}. |
|
254 |
Roughly, POSIX matching means matching the longest initial substring. |
|
64 | 255 |
In the case of a tie, the initial sub-match is chosen according to some priorities attached to the |
30 | 256 |
regular expressions (e.g.~keywords have a higher priority than |
257 |
identifiers). This sounds rather simple, but according to Grathwohl et |
|
258 |
al \cite[Page 36]{CrashCourse2014} this is not the case. They wrote: |
|
259 |
||
260 |
\begin{quote} |
|
261 |
\it{}``The POSIX strategy is more complicated than the greedy because of |
|
262 |
the dependence on information about the length of matched strings in the |
|
263 |
various subexpressions.'' |
|
264 |
\end{quote} |
|
265 |
||
266 |
\noindent |
|
267 |
This is also supported by evidence collected by Kuklewicz |
|
268 |
\cite{Kuklewicz} who noticed that a number of POSIX regular expression |
|
269 |
matchers calculate incorrect results. |
|
270 |
||
271 |
Our focus is on an algorithm introduced by Sulzmann and Lu in 2014 for |
|
272 |
regular expression matching according to the POSIX strategy |
|
273 |
\cite{Sulzmann2014}. Their algorithm is based on an older algorithm by |
|
274 |
Brzozowski from 1964 where he introduced the notion of derivatives of |
|
72 | 275 |
regular expressions~\cite{Brzozowski1964}. We shall briefly explain |
58 | 276 |
this algorithm next. |
30 | 277 |
|
46 | 278 |
\section{The Algorithm by Brzozowski based on Derivatives of Regular |
279 |
Expressions} |
|
30 | 280 |
|
40 | 281 |
Suppose (basic) regular expressions are given by the following grammar: |
38 | 282 |
\[ r ::= \ZERO \mid \ONE |
283 |
\mid c |
|
284 |
\mid r_1 \cdot r_2 |
|
285 |
\mid r_1 + r_2 |
|
286 |
\mid r^* |
|
287 |
\] |
|
30 | 288 |
|
289 |
\noindent |
|
46 | 290 |
The intended meaning of the constructors is as follows: $\ZERO$ |
30 | 291 |
cannot match any string, $\ONE$ can match the empty string, the |
292 |
character regular expression $c$ can match the character $c$, and so |
|
40 | 293 |
on. |
294 |
||
58 | 295 |
The ingenious contribution by Brzozowski is the notion of |
30 | 296 |
\emph{derivatives} of regular expressions. The idea behind this |
297 |
notion is as follows: suppose a regular expression $r$ can match a |
|
298 |
string of the form $c\!::\! s$ (that is a list of characters starting |
|
299 |
with $c$), what does the regular expression look like that can match |
|
40 | 300 |
just $s$? Brzozowski gave a neat answer to this question. He started |
301 |
with the definition of $nullable$: |
|
36 | 302 |
\begin{center} |
303 |
\begin{tabular}{lcl} |
|
304 |
$\nullable(\ZERO)$ & $\dn$ & $\mathit{false}$ \\ |
|
305 |
$\nullable(\ONE)$ & $\dn$ & $\mathit{true}$ \\ |
|
306 |
$\nullable(c)$ & $\dn$ & $\mathit{false}$ \\ |
|
307 |
$\nullable(r_1 + r_2)$ & $\dn$ & $\nullable(r_1) \vee \nullable(r_2)$ \\ |
|
308 |
$\nullable(r_1\cdot r_2)$ & $\dn$ & $\nullable(r_1) \wedge \nullable(r_2)$ \\ |
|
309 |
$\nullable(r^*)$ & $\dn$ & $\mathit{true}$ \\ |
|
310 |
\end{tabular} |
|
311 |
\end{center} |
|
38 | 312 |
This function simply tests whether the empty string is in $L(r)$. |
36 | 313 |
He then defined |
30 | 314 |
the following operation on regular expressions, written |
315 |
$r\backslash c$ (the derivative of $r$ w.r.t.~the character $c$): |
|
316 |
||
317 |
\begin{center} |
|
318 |
\begin{tabular}{lcl} |
|
319 |
$\ZERO \backslash c$ & $\dn$ & $\ZERO$\\ |
|
320 |
$\ONE \backslash c$ & $\dn$ & $\ZERO$\\ |
|
321 |
$d \backslash c$ & $\dn$ & |
|
322 |
$\mathit{if} \;c = d\;\mathit{then}\;\ONE\;\mathit{else}\;\ZERO$\\ |
|
323 |
$(r_1 + r_2)\backslash c$ & $\dn$ & $r_1 \backslash c \,+\, r_2 \backslash c$\\ |
|
36 | 324 |
$(r_1 \cdot r_2)\backslash c$ & $\dn$ & $\mathit{if} \, nullable(r_1)$\\ |
30 | 325 |
& & $\mathit{then}\;(r_1\backslash c) \cdot r_2 \,+\, r_2\backslash c$\\ |
326 |
& & $\mathit{else}\;(r_1\backslash c) \cdot r_2$\\ |
|
327 |
$(r^*)\backslash c$ & $\dn$ & $(r\backslash c) \cdot r^*$\\ |
|
328 |
\end{tabular} |
|
329 |
\end{center} |
|
330 |
||
46 | 331 |
%Assuming the classic notion of a |
332 |
%\emph{language} of a regular expression, written $L(\_)$, t |
|
30 | 333 |
|
40 | 334 |
\noindent |
335 |
The main property of the derivative operation is that |
|
30 | 336 |
|
337 |
\begin{center} |
|
338 |
$c\!::\!s \in L(r)$ holds |
|
339 |
if and only if $s \in L(r\backslash c)$. |
|
340 |
\end{center} |
|
341 |
||
342 |
\noindent |
|
46 | 343 |
For us the main advantage is that derivatives can be |
38 | 344 |
straightforwardly implemented in any functional programming language, |
345 |
and are easily definable and reasoned about in theorem provers---the |
|
346 |
definitions just consist of inductive datatypes and simple recursive |
|
347 |
functions. Moreover, the notion of derivatives can be easily |
|
348 |
generalised to cover extended regular expression constructors such as |
|
349 |
the not-regular expression, written $\neg\,r$, or bounded repetitions |
|
350 |
(for example $r^{\{n\}}$ and $r^{\{n..m\}}$), which cannot be so |
|
351 |
straightforwardly realised within the classic automata approach. |
|
352 |
For the moment however, we focus only on the usual basic regular expressions. |
|
353 |
||
354 |
||
40 | 355 |
Now if we want to find out whether a string $s$ matches with a regular |
356 |
expression $r$, build the derivatives of $r$ w.r.t.\ (in succession) |
|
357 |
all the characters of the string $s$. Finally, test whether the |
|
358 |
resulting regular expression can match the empty string. If yes, then |
|
359 |
$r$ matches $s$, and no in the negative case. To implement this idea |
|
360 |
we can generalise the derivative operation to strings like this: |
|
46 | 361 |
|
30 | 362 |
\begin{center} |
363 |
\begin{tabular}{lcl} |
|
364 |
$r \backslash (c\!::\!s) $ & $\dn$ & $(r \backslash c) \backslash s$ \\ |
|
40 | 365 |
$r \backslash [\,] $ & $\dn$ & $r$ |
30 | 366 |
\end{tabular} |
367 |
\end{center} |
|
40 | 368 |
|
37 | 369 |
\noindent |
46 | 370 |
and then define as regular-expression matching algorithm: |
30 | 371 |
\[ |
372 |
match\;s\;r \;\dn\; nullable(r\backslash s) |
|
373 |
\] |
|
40 | 374 |
|
375 |
\noindent |
|
64 | 376 |
This algorithm looks graphically as follows: |
46 | 377 |
\begin{equation}\label{graph:*} |
378 |
\begin{tikzcd} |
|
379 |
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} |
|
38 | 380 |
\end{tikzcd} |
46 | 381 |
\end{equation} |
40 | 382 |
|
383 |
\noindent |
|
46 | 384 |
where we start with a regular expression $r_0$, build successive |
385 |
derivatives until we exhaust the string and then use \textit{nullable} |
|
386 |
to test whether the result can match the empty string. It can be |
|
387 |
relatively easily shown that this matcher is correct (that is given |
|
64 | 388 |
an $s = c_0...c_{n-1}$ and an $r_0$, it generates YES if and only if $s \in L(r_0)$). |
46 | 389 |
|
390 |
||
391 |
\section{Values and the Algorithm by Sulzmann and Lu} |
|
38 | 392 |
|
30 | 393 |
One limitation, however, of Brzozowski's algorithm is that it only |
394 |
produces a YES/NO answer for whether a string is being matched by a |
|
395 |
regular expression. Sulzmann and Lu~\cite{Sulzmann2014} extended this |
|
396 |
algorithm to allow generation of an actual matching, called a |
|
72 | 397 |
\emph{value} or sometimes lexical values. These values and regular expressions correspond to each |
46 | 398 |
other as illustrated in the following table: |
399 |
||
30 | 400 |
|
401 |
\begin{center} |
|
402 |
\begin{tabular}{c@{\hspace{20mm}}c} |
|
403 |
\begin{tabular}{@{}rrl@{}} |
|
404 |
\multicolumn{3}{@{}l}{\textbf{Regular Expressions}}\medskip\\ |
|
405 |
$r$ & $::=$ & $\ZERO$\\ |
|
406 |
& $\mid$ & $\ONE$ \\ |
|
407 |
& $\mid$ & $c$ \\ |
|
408 |
& $\mid$ & $r_1 \cdot r_2$\\ |
|
409 |
& $\mid$ & $r_1 + r_2$ \\ |
|
410 |
\\ |
|
411 |
& $\mid$ & $r^*$ \\ |
|
412 |
\end{tabular} |
|
413 |
& |
|
414 |
\begin{tabular}{@{\hspace{0mm}}rrl@{}} |
|
415 |
\multicolumn{3}{@{}l}{\textbf{Values}}\medskip\\ |
|
416 |
$v$ & $::=$ & \\ |
|
417 |
& & $\Empty$ \\ |
|
418 |
& $\mid$ & $\Char(c)$ \\ |
|
419 |
& $\mid$ & $\Seq\,v_1\, v_2$\\ |
|
420 |
& $\mid$ & $\Left(v)$ \\ |
|
421 |
& $\mid$ & $\Right(v)$ \\ |
|
422 |
& $\mid$ & $\Stars\,[v_1,\ldots\,v_n]$ \\ |
|
423 |
\end{tabular} |
|
424 |
\end{tabular} |
|
425 |
\end{center} |
|
426 |
||
427 |
\noindent |
|
64 | 428 |
No value corresponds to $\ZERO$; $\Empty$ corresponds to |
63 | 429 |
$\ONE$; $\Char$ to the character regular expression; $\Seq$ to the |
430 |
sequence regular expression and so on. The idea of values is to encode |
|
72 | 431 |
a kind of lexical value for how the sub-parts of a regular expression match |
64 | 432 |
the sub-parts of a string. To see this, suppose a \emph{flatten} operation, written |
72 | 433 |
$|v|$ for values. We can use this function to extract the underlying string of a value |
63 | 434 |
$v$. For example, $|\mathit{Seq} \, (\textit{Char x}) \, (\textit{Char |
435 |
y})|$ is the string $xy$. Using flatten, we can describe how values |
|
64 | 436 |
encode parse trees: $\Seq\,v_1\, v_2$ encodes a tree with 2 children nodes |
437 |
that tells how the string $|v_1| @ |
|
63 | 438 |
|v_2|$ matches the regex $r_1 \cdot r_2$ whereby $r_1$ matches the |
439 |
substring $|v_1|$ and, respectively, $r_2$ matches the substring |
|
440 |
$|v_2|$. Exactly how these two are matched is contained in the |
|
64 | 441 |
children nodes $v_1$ and $v_2$ of parent $\textit{Seq}$ . |
30 | 442 |
|
72 | 443 |
To give a concrete example of how values work, consider the string $xy$ |
46 | 444 |
and the regular expression $(x + (y + xy))^*$. We can view this regular |
30 | 445 |
expression as a tree and if the string $xy$ is matched by two Star |
46 | 446 |
``iterations'', then the $x$ is matched by the left-most alternative in |
447 |
this tree and the $y$ by the right-left alternative. This suggests to |
|
448 |
record this matching as |
|
30 | 449 |
|
450 |
\begin{center} |
|
451 |
$\Stars\,[\Left\,(\Char\,x), \Right(\Left(\Char\,y))]$ |
|
452 |
\end{center} |
|
453 |
||
454 |
\noindent |
|
72 | 455 |
where $\Stars \; [\ldots]$ records all the |
64 | 456 |
iterations; and $\Left$, respectively $\Right$, which |
30 | 457 |
alternative is used. The value for |
458 |
matching $xy$ in a single ``iteration'', i.e.~the POSIX value, |
|
459 |
would look as follows |
|
460 |
||
461 |
\begin{center} |
|
462 |
$\Stars\,[\Seq\,(\Char\,x)\,(\Char\,y)]$ |
|
463 |
\end{center} |
|
464 |
||
465 |
\noindent |
|
466 |
where $\Stars$ has only a single-element list for the single iteration |
|
467 |
and $\Seq$ indicates that $xy$ is matched by a sequence regular |
|
468 |
expression. |
|
469 |
||
470 |
The contribution of Sulzmann and Lu is an extension of Brzozowski's |
|
471 |
algorithm by a second phase (the first phase being building successive |
|
46 | 472 |
derivatives---see \eqref{graph:*}). In this second phase, a POSIX value |
72 | 473 |
is generated in case the regular expression matches the string. |
474 |
Pictorially, the Sulzmann and Lu algorithm is as follows: |
|
46 | 475 |
|
70 | 476 |
\begin{ceqn} |
59 | 477 |
\begin{equation}\label{graph:2} |
30 | 478 |
\begin{tikzcd} |
36 | 479 |
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] \\ |
30 | 480 |
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] |
481 |
\end{tikzcd} |
|
59 | 482 |
\end{equation} |
70 | 483 |
\end{ceqn} |
37 | 484 |
|
46 | 485 |
\noindent |
59 | 486 |
For convenience, we shall employ the following notations: the regular expression we |
58 | 487 |
start with is $r_0$, and the given string $s$ is composed of characters $c_0 c_1 |
64 | 488 |
\ldots c_{n-1}$. In the first phase, we build the derivatives $r_1$, $r_2$, \ldots according to |
72 | 489 |
the characters $c_0$, $c_1$ until we exhaust the string and |
490 |
obtain the derivative $r_n$. We test whether this derivative is |
|
46 | 491 |
$\textit{nullable}$ or not. If not, we know the string does not match |
492 |
$r$ and no value needs to be generated. If yes, we start building the |
|
72 | 493 |
values incrementally by \emph{injecting} back the characters into |
494 |
the earlier values $v_n, \ldots, v_0$. For the first value $v_0$, we call the function |
|
46 | 495 |
$\textit{mkeps}$, which builds the parse tree for how the empty string |
72 | 496 |
has been matched by the (nullable) regular expression $r_n$. This function is defined |
46 | 497 |
as |
30 | 498 |
|
51
5df7faf69238
added mkeps and pder, still have not proof read it
Chengsong
parents:
50
diff
changeset
|
499 |
\begin{center} |
5df7faf69238
added mkeps and pder, still have not proof read it
Chengsong
parents:
50
diff
changeset
|
500 |
\begin{tabular}{lcl} |
5df7faf69238
added mkeps and pder, still have not proof read it
Chengsong
parents:
50
diff
changeset
|
501 |
$\mkeps(\ONE)$ & $\dn$ & $\Empty$ \\ |
5df7faf69238
added mkeps and pder, still have not proof read it
Chengsong
parents:
50
diff
changeset
|
502 |
$\mkeps(r_{1}+r_{2})$ & $\dn$ |
5df7faf69238
added mkeps and pder, still have not proof read it
Chengsong
parents:
50
diff
changeset
|
503 |
& \textit{if} $\nullable(r_{1})$\\ |
5df7faf69238
added mkeps and pder, still have not proof read it
Chengsong
parents:
50
diff
changeset
|
504 |
& & \textit{then} $\Left(\mkeps(r_{1}))$\\ |
5df7faf69238
added mkeps and pder, still have not proof read it
Chengsong
parents:
50
diff
changeset
|
505 |
& & \textit{else} $\Right(\mkeps(r_{2}))$\\ |
5df7faf69238
added mkeps and pder, still have not proof read it
Chengsong
parents:
50
diff
changeset
|
506 |
$\mkeps(r_1\cdot r_2)$ & $\dn$ & $\Seq\,(\mkeps\,r_1)\,(\mkeps\,r_2)$\\ |
5df7faf69238
added mkeps and pder, still have not proof read it
Chengsong
parents:
50
diff
changeset
|
507 |
$mkeps(r^*)$ & $\dn$ & $\Stars\,[]$ |
5df7faf69238
added mkeps and pder, still have not proof read it
Chengsong
parents:
50
diff
changeset
|
508 |
\end{tabular} |
5df7faf69238
added mkeps and pder, still have not proof read it
Chengsong
parents:
50
diff
changeset
|
509 |
\end{center} |
41 | 510 |
|
59 | 511 |
|
512 |
\noindent There are no cases for $\ZERO$ and $c$, since |
|
513 |
these regular expression cannot match the empty string. Note |
|
514 |
also that in case of alternatives we give preference to the |
|
515 |
regular expression on the left-hand side. This will become |
|
516 |
important later on. |
|
517 |
||
518 |
After this, we inject back the characters one by one in order to build |
|
63 | 519 |
the parse tree $v_i$ for how the regex $r_i$ matches the string $s_i$ |
64 | 520 |
($s_i = c_i \ldots c_{n-1}$ ) from the previous parse tree $v_{i+1}$. After |
63 | 521 |
injecting back $n$ characters, we get the parse tree for how $r_0$ |
522 |
matches $s$. For this Sulzmann and Lu defined a function that reverses |
|
523 |
the ``chopping off'' of characters during the derivative phase. The |
|
524 |
corresponding function is called $\textit{inj}$; it takes three |
|
525 |
arguments: the first one is a regular expression ${r_{i-1}}$, before the |
|
526 |
character is chopped off, the second is a character ${c_{i-1}}$, the |
|
527 |
character we want to inject and the third argument is the value |
|
64 | 528 |
${v_i}$, into which one wants to inject the character (it |
63 | 529 |
corresponds to the regular expression after the character has been |
530 |
chopped off). The result of this function is a new value. The definition |
|
531 |
of $\textit{inj}$ is as follows: |
|
59 | 532 |
|
533 |
\begin{center} |
|
534 |
\begin{tabular}{l@{\hspace{1mm}}c@{\hspace{1mm}}l} |
|
535 |
$\textit{inj}\,(c)\,c\,Empty$ & $\dn$ & $Char\,c$\\ |
|
536 |
$\textit{inj}\,(r_1 + r_2)\,c\,\Left(v)$ & $\dn$ & $\Left(\textit{inj}\,r_1\,c\,v)$\\ |
|
537 |
$\textit{inj}\,(r_1 + r_2)\,c\,Right(v)$ & $\dn$ & $Right(\textit{inj}\,r_2\,c\,v)$\\ |
|
538 |
$\textit{inj}\,(r_1 \cdot r_2)\,c\,Seq(v_1,v_2)$ & $\dn$ & $Seq(\textit{inj}\,r_1\,c\,v_1,v_2)$\\ |
|
539 |
$\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)$\\ |
|
540 |
$\textit{inj}\,(r_1 \cdot r_2)\,c\,Right(v)$ & $\dn$ & $Seq(\textit{mkeps}(r_1),\textit{inj}\,r_2\,c\,v)$\\ |
|
541 |
$\textit{inj}\,(r^*)\,c\,Seq(v,Stars\,vs)$ & $\dn$ & $Stars((\textit{inj}\,r\,c\,v)\,::\,vs)$\\ |
|
542 |
\end{tabular} |
|
543 |
\end{center} |
|
544 |
||
63 | 545 |
\noindent This definition is by recursion on the ``shape'' of regular |
546 |
expressions and values. To understands this definition better consider |
|
547 |
the situation when we build the derivative on regular expression $r_{i-1}$. |
|
548 |
For this we chop off a character from $r_{i-1}$ to form $r_i$. This leaves a |
|
72 | 549 |
``hole'' in $r_i$ and its corresponding value $v_i$. |
550 |
To calculate $v_{i-1}$, we need to |
|
64 | 551 |
locate where that hole is and fill it. |
552 |
We can find this location by |
|
63 | 553 |
comparing $r_{i-1}$ and $v_i$. For instance, if $r_{i-1}$ is of shape |
64 | 554 |
$r_a \cdot r_b$, and $v_i$ is of shape $\Left(Seq(v_1,v_2))$, we know immediately that |
63 | 555 |
% |
556 |
\[ (r_a \cdot r_b)\backslash c = (r_a\backslash c) \cdot r_b \,+\, r_b\backslash c,\] |
|
557 |
||
558 |
\noindent |
|
59 | 559 |
otherwise if $r_a$ is not nullable, |
63 | 560 |
\[ (r_a \cdot r_b)\backslash c = (r_a\backslash c) \cdot r_b,\] |
561 |
||
562 |
\noindent |
|
64 | 563 |
the value $v_i$ should be $\Seq(\ldots)$, contradicting the fact that |
564 |
$v_i$ is actually of shape $\Left(\ldots)$. Furthermore, since $v_i$ is of shape |
|
63 | 565 |
$\Left(\ldots)$ instead of $\Right(\ldots)$, we know that the left |
64 | 566 |
branch of \[ (r_a \cdot r_b)\backslash c = |
567 |
\bold{\underline{ (r_a\backslash c) \cdot r_b} }\,+\, r_b\backslash c,\](underlined) |
|
568 |
is taken instead of the right one. This means $c$ is chopped off |
|
569 |
from $r_a$ rather than $r_b$. |
|
570 |
We have therefore found out |
|
63 | 571 |
that the hole will be on $r_a$. So we recursively call $\inj\, |
64 | 572 |
r_a\,c\,v_a$ to fill that hole in $v_a$. After injection, the value |
63 | 573 |
$v_i$ for $r_i = r_a \cdot r_b$ should be $\Seq\,(\inj\,r_a\,c\,v_a)\,v_b$. |
60
c737a0259194
sorry not all done, need a few more mins for last few changes
Chengsong
parents:
59
diff
changeset
|
574 |
Other clauses can be understood in a similar way. |
59 | 575 |
|
71 | 576 |
%\comment{Other word: insight?} |
577 |
The following example gives an insight of $\textit{inj}$'s effect |
|
65 | 578 |
and how Sulzmann and Lu's algorithm works as a whole. |
579 |
Suppose we have a |
|
580 |
regular expression $((((a+b)+ab)+c)+abc)^*$, and want to match it against |
|
63 | 581 |
the string $abc$ (when $abc$ is written as a regular expression, the most |
582 |
standard way of expressing it should be $a \cdot (b \cdot c)$. We omit |
|
65 | 583 |
the parentheses and dots here for readability). |
584 |
This algorithm returns a POSIX value, which means it |
|
585 |
will go for the longest matching, i.e.~it should match the string |
|
586 |
$abc$ in one star iteration, using the longest alternative $abc$ in the |
|
587 |
sub-expression $((((a+b)+ab)+c)+abc)$ (we use $r$ to denote this sub-expression |
|
64 | 588 |
for conciseness). |
65 | 589 |
Before $\textit{inj}$ comes into play, |
590 |
our lexer first builds derivative using string $abc$ (we simplified some regular expressions like |
|
591 |
$0 \cdot b$ to $0$ for conciseness; we also omit parentheses if |
|
63 | 592 |
they are clear from the context): |
60
c737a0259194
sorry not all done, need a few more mins for last few changes
Chengsong
parents:
59
diff
changeset
|
593 |
%Similarly, we allow |
c737a0259194
sorry not all done, need a few more mins for last few changes
Chengsong
parents:
59
diff
changeset
|
594 |
%$\textit{ALT}$ to take a list of regular expressions as an argument |
c737a0259194
sorry not all done, need a few more mins for last few changes
Chengsong
parents:
59
diff
changeset
|
595 |
%instead of just 2 operands to reduce the nested depth of |
c737a0259194
sorry not all done, need a few more mins for last few changes
Chengsong
parents:
59
diff
changeset
|
596 |
%$\textit{ALT}$ |
c737a0259194
sorry not all done, need a few more mins for last few changes
Chengsong
parents:
59
diff
changeset
|
597 |
\begin{center} |
63 | 598 |
\begin{tabular}{lcl} |
72 | 599 |
$r^*$ & $\xrightarrow{\backslash a}$ & $r_1 = (\ONE+\ZERO+\ONE \cdot b + \ZERO + \ONE \cdot b \cdot c) \cdot r^*$\\ |
600 |
& $\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^*$\\ |
|
601 |
& $\xrightarrow{\backslash c}$ & $r_3 = ((\ZERO+\ZERO+\ZERO + \ZERO + \ONE \cdot \ONE \cdot \ONE) \cdot r^* + (\ZERO+\ZERO+\ZERO + \ONE + \ZERO) \cdot r^*) + $\\ |
|
602 |
& & $\phantom{r_3 = (} ((\ZERO+\ONE+\ZERO + \ZERO + \ZERO) \cdot r^* + (\ZERO+\ZERO+\ZERO + \ONE + \ZERO) \cdot r^* )$ |
|
63 | 603 |
\end{tabular} |
60
c737a0259194
sorry not all done, need a few more mins for last few changes
Chengsong
parents:
59
diff
changeset
|
604 |
\end{center} |
63 | 605 |
|
606 |
\noindent |
|
72 | 607 |
In case $r_3$ is nullable, we can call $\textit{mkeps}$ |
60
c737a0259194
sorry not all done, need a few more mins for last few changes
Chengsong
parents:
59
diff
changeset
|
608 |
to construct a parse tree for how $r_3$ matched the string $abc$. |
72 | 609 |
$\textit{mkeps}$ gives the following value $v_3$: |
65 | 610 |
\begin{center} |
611 |
$\Left(\Left(\Seq(\Right(\Seq(\Empty, \Seq(\Empty,\Empty))), \Stars [])))$ |
|
612 |
\end{center} |
|
613 |
The outer $\Left(\Left(\ldots))$ tells us the leftmost nullable part of $r_3$(underlined): |
|
70 | 614 |
|
65 | 615 |
\begin{center} |
72 | 616 |
$( \underline{(\ZERO+\ZERO+\ZERO+ \ZERO+ \ONE \cdot \ONE \cdot \ONE) \cdot r^*} + (\ZERO+\ZERO+\ZERO + \ONE + \ZERO) |
617 |
\cdot r^*) +((\ZERO+\ONE+\ZERO + \ZERO + \ZERO) \cdot r^*+(\ZERO+\ZERO+\ZERO + \ONE + \ZERO) \cdot r^* ).$ |
|
65 | 618 |
\end{center} |
70 | 619 |
|
620 |
\noindent |
|
72 | 621 |
Note that the leftmost location of term $((\ZERO+\ZERO+\ZERO + \ZERO + \ONE \cdot \ONE \cdot |
622 |
\ONE) \cdot r^*$ (which corresponds to the initial sub-match $abc$) allows |
|
623 |
$\textit{mkeps}$ to pick it up because $\textit{mkeps}$ is defined to always choose the |
|
70 | 624 |
left one when it is nullable. In the case of this example, $abc$ is |
625 |
preferred over $a$ or $ab$. This $\Left(\Left(\ldots))$ location is |
|
626 |
naturally generated by two applications of the splitting clause |
|
627 |
||
628 |
\begin{center} |
|
65 | 629 |
$(r_1 \cdot r_2)\backslash c (when \; r_1 \; nullable) \, = (r_1\backslash c) \cdot r_2 \,+\, r_2\backslash c.$ |
70 | 630 |
\end{center} |
631 |
||
632 |
\noindent |
|
633 |
By this clause, we put $r_1 \backslash c \cdot r_2 $ at the |
|
634 |
$\textit{front}$ and $r_2 \backslash c$ at the $\textit{back}$. This |
|
72 | 635 |
allows $\textit{mkeps}$ to always pick up among two matches the one with a longer |
70 | 636 |
initial sub-match. Removing the outside $\Left(\Left(...))$, the inside |
637 |
sub-value |
|
638 |
||
639 |
\begin{center} |
|
65 | 640 |
$\Seq(\Right(\Seq(\Empty, \Seq(\Empty, \Empty))), \Stars [])$ |
70 | 641 |
\end{center} |
642 |
||
643 |
\noindent |
|
72 | 644 |
tells us how the empty string $[]$ is matched with $(\ZERO+\ZERO+\ZERO + \ZERO + \ONE \cdot |
645 |
\ONE \cdot \ONE) \cdot r^*$. We match $[]$ by a sequence of 2 nullable regular |
|
70 | 646 |
expressions. The first one is an alternative, we take the rightmost |
647 |
alternative---whose language contains the empty string. The second |
|
648 |
nullable regular expression is a Kleene star. $\Stars$ tells us how it |
|
649 |
generates the nullable regular expression: by 0 iterations to form |
|
72 | 650 |
$\ONE$. Now $\textit{inj}$ injects characters back and incrementally |
70 | 651 |
builds a parse tree based on $v_3$. Using the value $v_3$, the character |
652 |
c, and the regular expression $r_2$, we can recover how $r_2$ matched |
|
653 |
the string $[c]$ : $\textit{inj} \; r_2 \; c \; v_3$ gives us |
|
65 | 654 |
\begin{center} |
655 |
$v_2 = \Left(\Seq(\Right(\Seq(\Empty, \Seq(\Empty, c))), \Stars [])),$ |
|
656 |
\end{center} |
|
657 |
which tells us how $r_2$ matched $[c]$. After this we inject back the character $b$, and get |
|
658 |
\begin{center} |
|
659 |
$v_1 = \Seq(\Right(\Seq(\Empty, \Seq(b, c))), \Stars [])$ |
|
660 |
\end{center} |
|
61 | 661 |
for how |
65 | 662 |
\begin{center} |
72 | 663 |
$r_1= (\ONE+\ZERO+\ONE \cdot b + \ZERO + \ONE \cdot b \cdot c) \cdot r*$ |
65 | 664 |
\end{center} |
61 | 665 |
matched the string $bc$ before it split into 2 pieces. |
666 |
Finally, after injecting character $a$ back to $v_1$, |
|
65 | 667 |
we get the parse tree |
668 |
\begin{center} |
|
669 |
$v_0= \Stars [\Right(\Seq(a, \Seq(b, c)))]$ |
|
670 |
\end{center} |
|
671 |
for how $r$ matched $abc$. This completes the algorithm. |
|
672 |
||
61 | 673 |
%We omit the details of injection function, which is provided by Sulzmann and Lu's paper \cite{Sulzmann2014}. |
674 |
Readers might have noticed that the parse tree information |
|
675 |
is actually already available when doing derivatives. |
|
676 |
For example, immediately after the operation $\backslash a$ we know that if we want to match a string that starts with $a$, |
|
677 |
we can either take the initial match to be |
|
65 | 678 |
\begin{center} |
42 | 679 |
\begin{enumerate} |
680 |
\item[1)] just $a$ or |
|
681 |
\item[2)] string $ab$ or |
|
682 |
\item[3)] string $abc$. |
|
683 |
\end{enumerate} |
|
65 | 684 |
\end{center} |
70 | 685 |
|
686 |
\noindent |
|
687 |
In order to differentiate between these choices, we just need to |
|
688 |
remember their positions--$a$ is on the left, $ab$ is in the middle , |
|
689 |
and $abc$ is on the right. Which one of these alternatives is chosen |
|
690 |
later does not affect their relative position because our algorithm does |
|
691 |
not change this order. If this parsing information can be determined and |
|
692 |
does not change because of later derivatives, there is no point in |
|
693 |
traversing this information twice. This leads to an optimisation---if we |
|
694 |
store the information for parse trees inside the regular expression, |
|
695 |
update it when we do derivative on them, and collect the information |
|
72 | 696 |
when finished with derivatives and call $\textit{mkeps}$ for deciding which |
70 | 697 |
branch is POSIX, we can generate the parse tree in one pass, instead of |
698 |
doing the rest $n$ injections. This leads to Sulzmann and Lu's novel |
|
71 | 699 |
idea of using bitcodes in derivatives. |
42 | 700 |
|
72 | 701 |
In the next section, we shall focus on the bitcoded algorithm and the |
63 | 702 |
process of simplification of regular expressions. This is needed in |
30 | 703 |
order to obtain \emph{fast} versions of the Brzozowski's, and Sulzmann |
63 | 704 |
and Lu's algorithms. This is where the PhD-project aims to advance the |
705 |
state-of-the-art. |
|
30 | 706 |
|
707 |
||
708 |
\section{Simplification of Regular Expressions} |
|
63 | 709 |
|
70 | 710 |
Using bitcodes to guide parsing is not a novel idea. It was applied to |
63 | 711 |
context free grammars and then adapted by Henglein and Nielson for |
70 | 712 |
efficient regular expression parsing using DFAs~\cite{nielson11bcre}. |
713 |
Sulzmann and Lu took this idea of bitcodes a step further by integrating |
|
714 |
bitcodes into derivatives. The reason why we want to use bitcodes in |
|
715 |
this project is that we want to introduce more aggressive |
|
716 |
simplifications in order to keep the size of derivatives small |
|
717 |
throughout. This is because the main drawback of building successive |
|
718 |
derivatives according to Brzozowski's definition is that they can grow |
|
719 |
very quickly in size. This is mainly due to the fact that the derivative |
|
720 |
operation generates often ``useless'' $\ZERO$s and $\ONE$s in |
|
63 | 721 |
derivatives. As a result, if implemented naively both algorithms by |
70 | 722 |
Brzozowski and by Sulzmann and Lu are excruciatingly slow. For example |
723 |
when starting with the regular expression $(a + aa)^*$ and building 12 |
|
63 | 724 |
successive derivatives w.r.t.~the character $a$, one obtains a |
725 |
derivative regular expression with more than 8000 nodes (when viewed as |
|
726 |
a tree). Operations like derivative and $\nullable$ need to traverse |
|
727 |
such trees and consequently the bigger the size of the derivative the |
|
66 | 728 |
slower the algorithm. |
35 | 729 |
|
70 | 730 |
Fortunately, one can simplify regular expressions after each derivative |
731 |
step. Various simplifications of regular expressions are possible, such |
|
732 |
as the simplifications of $\ZERO + r$, $r + \ZERO$, $\ONE\cdot r$, $r |
|
733 |
\cdot \ONE$, and $r + r$ to just $r$. These simplifications do not |
|
734 |
affect the answer for whether a regular expression matches a string or |
|
735 |
not, but fortunately also do not affect the POSIX strategy of how |
|
736 |
regular expressions match strings---although the latter is much harder |
|
71 | 737 |
to establish. Some initial results in this regard have been |
70 | 738 |
obtained in \cite{AusafDyckhoffUrban2016}. |
739 |
||
740 |
Unfortunately, the simplification rules outlined above are not |
|
741 |
sufficient to prevent an explosion for all regular expression. We |
|
742 |
believe a tighter bound can be achieved that prevents an explosion in |
|
743 |
all cases. Such a tighter bound is suggested by work of Antimirov who |
|
744 |
proved that (partial) derivatives can be bound by the number of |
|
745 |
characters contained in the initial regular expression |
|
746 |
\cite{Antimirov95}. He defined the \emph{partial derivatives} of regular |
|
747 |
expressions as follows: |
|
748 |
||
52
25bbbb8b0e90
just in case of some accidents from erasing my work
Chengsong
parents:
51
diff
changeset
|
749 |
\begin{center} |
25bbbb8b0e90
just in case of some accidents from erasing my work
Chengsong
parents:
51
diff
changeset
|
750 |
\begin{tabular}{lcl} |
25bbbb8b0e90
just in case of some accidents from erasing my work
Chengsong
parents:
51
diff
changeset
|
751 |
$\textit{pder} \; c \; 0$ & $\dn$ & $\emptyset$\\ |
25bbbb8b0e90
just in case of some accidents from erasing my work
Chengsong
parents:
51
diff
changeset
|
752 |
$\textit{pder} \; c \; 1$ & $\dn$ & $\emptyset$ \\ |
25bbbb8b0e90
just in case of some accidents from erasing my work
Chengsong
parents:
51
diff
changeset
|
753 |
$\textit{pder} \; c \; d$ & $\dn$ & $\textit{if} \; c \,=\, d \; \{ 1 \} \; \textit{else} \; \emptyset$ \\ |
25bbbb8b0e90
just in case of some accidents from erasing my work
Chengsong
parents:
51
diff
changeset
|
754 |
$\textit{pder} \; c \; r_1+r_2$ & $\dn$ & $pder \; c \; r_1 \cup pder \; c \; r_2$ \\ |
70 | 755 |
$\textit{pder} \; c \; r_1 \cdot r_2$ & $\dn$ & $\textit{if} \; nullable \; r_1 $\\ |
756 |
& & $\textit{then} \; \{ r \cdot r_2 \mid r \in pder \; c \; r_1 \} \cup pder \; c \; r_2 \;$\\ |
|
757 |
& & $\textit{else} \; \{ r \cdot r_2 \mid r \in pder \; c \; r_1 \} $ \\ |
|
52
25bbbb8b0e90
just in case of some accidents from erasing my work
Chengsong
parents:
51
diff
changeset
|
758 |
$\textit{pder} \; c \; r^*$ & $\dn$ & $ \{ r' \cdot r^* \mid r' \in pder \; c \; r \} $ \\ |
25bbbb8b0e90
just in case of some accidents from erasing my work
Chengsong
parents:
51
diff
changeset
|
759 |
\end{tabular} |
25bbbb8b0e90
just in case of some accidents from erasing my work
Chengsong
parents:
51
diff
changeset
|
760 |
\end{center} |
70 | 761 |
|
762 |
\noindent |
|
763 |
A partial derivative of a regular expression $r$ is essentially a set of |
|
764 |
regular expressions that are either $r$'s children expressions or a |
|
765 |
concatenation of them. Antimirov has proved a tight bound of the size of |
|
71 | 766 |
partial derivatives. Roughly |
72 | 767 |
speaking the size will be quadruple in the size of the regular expression. |
768 |
If we want the size of derivatives |
|
71 | 769 |
to stay below this bound, we would need more aggressive simplifications |
770 |
such as opening up alternatives to achieve the maximum level of duplicates |
|
771 |
cancellation. |
|
772 |
For example, the parentheses in $(a+b) \cdot c + bc$ can be opened up to |
|
773 |
get $a\cdot c +b \cdot c |
|
774 |
+ b \cdot c$, and then simplified to $a \cdot c+b \cdot c$. Another example is from |
|
72 | 775 |
$(a^*+a) + (a^*+ \ONE) + (a +\ONE)$ to $a^*+a+\ONE$. |
71 | 776 |
Adding these more aggressive simplification rules |
777 |
helped us to achieve the same size bound as that of the partial derivatives. |
|
778 |
To introduce these "spilling out alternatives" simplifications |
|
779 |
and make the correctness proof easier, |
|
780 |
we used bitcodes. |
|
72 | 781 |
Bitcodes look like this: |
71 | 782 |
%This allows us to prove a tight |
783 |
%bound on the size of regular expression during the running time of the |
|
784 |
%algorithm if we can establish the connection between our simplification |
|
785 |
%rules and partial derivatives. |
|
35 | 786 |
|
787 |
%We believe, and have generated test |
|
788 |
%data, that a similar bound can be obtained for the derivatives in |
|
789 |
%Sulzmann and Lu's algorithm. Let us give some details about this next. |
|
30 | 790 |
|
72 | 791 |
|
67 | 792 |
\begin{center} |
793 |
$b ::= S \mid Z \; \;\; |
|
43 | 794 |
bs ::= [] \mid b:bs |
67 | 795 |
$ |
796 |
\end{center} |
|
71 | 797 |
They are just a string of bits, |
798 |
the names $S$ and $Z$ here are quite arbitrary, we can use 0 and 1 |
|
799 |
or any other set of binary symbols to substitute them. |
|
800 |
Bitcodes(or bit-sequences) are a compact form of parse trees. |
|
43 | 801 |
Bitcodes are essentially incomplete values. |
30 | 802 |
This can be straightforwardly seen in the following transformation: |
803 |
\begin{center} |
|
804 |
\begin{tabular}{lcl} |
|
805 |
$\textit{code}(\Empty)$ & $\dn$ & $[]$\\ |
|
806 |
$\textit{code}(\Char\,c)$ & $\dn$ & $[]$\\ |
|
807 |
$\textit{code}(\Left\,v)$ & $\dn$ & $\Z :: code(v)$\\ |
|
808 |
$\textit{code}(\Right\,v)$ & $\dn$ & $\S :: code(v)$\\ |
|
809 |
$\textit{code}(\Seq\,v_1\,v_2)$ & $\dn$ & $code(v_1) \,@\, code(v_2)$\\ |
|
68 | 810 |
$\textit{code}(\Stars\,[])$ & $\dn$ & $[\Z]$\\ |
811 |
$\textit{code}(\Stars\,(v\!::\!vs))$ & $\dn$ & $\S :: code(v) \;@\; |
|
30 | 812 |
code(\Stars\,vs)$ |
813 |
\end{tabular} |
|
814 |
\end{center} |
|
70 | 815 |
|
816 |
Here code encodes a value into a bit-sequence by converting Left into |
|
817 |
$\Z$, Right into $\S$, the start point of a non-empty star iteration |
|
818 |
into $\S$, and the border where a local star terminates into $\Z$. This |
|
819 |
conversion is apparently lossy, as it throws away the character |
|
820 |
information, and does not decode the boundary between the two operands |
|
821 |
of the sequence constructor. Moreover, with only the bitcode we cannot |
|
822 |
even tell whether the $\S$s and $\Z$s are for $\Left/\Right$ or |
|
823 |
$\Stars$. The reason for choosing this compact way of storing |
|
824 |
information is that the relatively small size of bits can be easily |
|
825 |
moved around. In order to recover the bitcode back into values, we will |
|
826 |
need the regular expression as the extra information and decode it back |
|
827 |
into value:\\ |
|
828 |
||
829 |
||
37 | 830 |
%\begin{definition}[Bitdecoding of Values]\mbox{} |
36 | 831 |
\begin{center} |
832 |
\begin{tabular}{@{}l@{\hspace{1mm}}c@{\hspace{1mm}}l@{}} |
|
833 |
$\textit{decode}'\,bs\,(\ONE)$ & $\dn$ & $(\Empty, bs)$\\ |
|
834 |
$\textit{decode}'\,bs\,(c)$ & $\dn$ & $(\Char\,c, bs)$\\ |
|
835 |
$\textit{decode}'\,(\Z\!::\!bs)\;(r_1 + r_2)$ & $\dn$ & |
|
836 |
$\textit{let}\,(v, bs_1) = \textit{decode}'\,bs\,r_1\;\textit{in}\; |
|
837 |
(\Left\,v, bs_1)$\\ |
|
838 |
$\textit{decode}'\,(\S\!::\!bs)\;(r_1 + r_2)$ & $\dn$ & |
|
839 |
$\textit{let}\,(v, bs_1) = \textit{decode}'\,bs\,r_2\;\textit{in}\; |
|
840 |
(\Right\,v, bs_1)$\\ |
|
841 |
$\textit{decode}'\,bs\;(r_1\cdot r_2)$ & $\dn$ & |
|
842 |
$\textit{let}\,(v_1, bs_1) = \textit{decode}'\,bs\,r_1\;\textit{in}$\\ |
|
843 |
& & $\textit{let}\,(v_2, bs_2) = \textit{decode}'\,bs_1\,r_2$\\ |
|
844 |
& & \hspace{35mm}$\textit{in}\;(\Seq\,v_1\,v_2, bs_2)$\\ |
|
845 |
$\textit{decode}'\,(\Z\!::\!bs)\,(r^*)$ & $\dn$ & $(\Stars\,[], bs)$\\ |
|
846 |
$\textit{decode}'\,(\S\!::\!bs)\,(r^*)$ & $\dn$ & |
|
847 |
$\textit{let}\,(v, bs_1) = \textit{decode}'\,bs\,r\;\textit{in}$\\ |
|
848 |
& & $\textit{let}\,(\Stars\,vs, bs_2) = \textit{decode}'\,bs_1\,r^*$\\ |
|
849 |
& & \hspace{35mm}$\textit{in}\;(\Stars\,v\!::\!vs, bs_2)$\bigskip\\ |
|
850 |
||
851 |
$\textit{decode}\,bs\,r$ & $\dn$ & |
|
852 |
$\textit{let}\,(v, bs') = \textit{decode}'\,bs\,r\;\textit{in}$\\ |
|
853 |
& & $\textit{if}\;bs' = []\;\textit{then}\;\textit{Some}\,v\; |
|
854 |
\textit{else}\;\textit{None}$ |
|
855 |
\end{tabular} |
|
856 |
\end{center} |
|
37 | 857 |
%\end{definition} |
30 | 858 |
|
71 | 859 |
Sulzmann and Lu's integrated the bitcodes into regular |
860 |
expressions to create annotated regular expressions. |
|
861 |
It is by attaching them to the head of every substructure of a |
|
862 |
regular expression\cite{Sulzmann2014}. Annotated regular expressions |
|
863 |
are defined by the following |
|
70 | 864 |
grammar: |
43 | 865 |
|
866 |
\begin{center} |
|
867 |
\begin{tabular}{lcl} |
|
868 |
$\textit{a}$ & $::=$ & $\textit{ZERO}$\\ |
|
869 |
& $\mid$ & $\textit{ONE}\;\;bs$\\ |
|
870 |
& $\mid$ & $\textit{CHAR}\;\;bs\,c$\\ |
|
72 | 871 |
& $\mid$ & $\textit{ALT}\;\;bs\,a_1 \, a_2$\\ |
43 | 872 |
& $\mid$ & $\textit{SEQ}\;\;bs\,a_1\,a_2$\\ |
873 |
& $\mid$ & $\textit{STAR}\;\;bs\,a$ |
|
874 |
\end{tabular} |
|
875 |
\end{center} |
|
72 | 876 |
%(in \textit{ALT}) |
43 | 877 |
\noindent |
72 | 878 |
where $bs$ stands for bit-sequences, and $a$ for $\bold{a}$nnotated regular expressions. These bit-sequences encode |
43 | 879 |
information about the (POSIX) value that should be generated by the |
880 |
Sulzmann and Lu algorithm. |
|
881 |
||
70 | 882 |
To do lexing using annotated regular expressions, we shall first |
883 |
transform the usual (un-annotated) regular expressions into annotated |
|
884 |
regular expressions. This operation is called \emph{internalisation} and |
|
885 |
defined as follows: |
|
886 |
||
37 | 887 |
%\begin{definition} |
36 | 888 |
\begin{center} |
889 |
\begin{tabular}{lcl} |
|
890 |
$(\ZERO)^\uparrow$ & $\dn$ & $\textit{ZERO}$\\ |
|
891 |
$(\ONE)^\uparrow$ & $\dn$ & $\textit{ONE}\,[]$\\ |
|
892 |
$(c)^\uparrow$ & $\dn$ & $\textit{CHAR}\,[]\,c$\\ |
|
893 |
$(r_1 + r_2)^\uparrow$ & $\dn$ & |
|
894 |
$\textit{ALT}\;[]\,(\textit{fuse}\,[\Z]\,r_1^\uparrow)\, |
|
895 |
(\textit{fuse}\,[\S]\,r_2^\uparrow)$\\ |
|
896 |
$(r_1\cdot r_2)^\uparrow$ & $\dn$ & |
|
897 |
$\textit{SEQ}\;[]\,r_1^\uparrow\,r_2^\uparrow$\\ |
|
898 |
$(r^*)^\uparrow$ & $\dn$ & |
|
899 |
$\textit{STAR}\;[]\,r^\uparrow$\\ |
|
900 |
\end{tabular} |
|
901 |
\end{center} |
|
37 | 902 |
%\end{definition} |
44
4d674a971852
another changes. have written more. but havent typed them. tomorrow will continue.
Chengsong
parents:
43
diff
changeset
|
903 |
|
70 | 904 |
\noindent |
72 | 905 |
We use up arrows here to imply that the basic un-annotated regular expressions |
906 |
are "lifted up" into something slightly more complex. |
|
907 |
In the fourth clause, $\textit{fuse}$ is an auxiliary function that helps to attach bits to the |
|
70 | 908 |
front of an annotated regular expression. Its definition is as follows: |
909 |
||
44
4d674a971852
another changes. have written more. but havent typed them. tomorrow will continue.
Chengsong
parents:
43
diff
changeset
|
910 |
\begin{center} |
4d674a971852
another changes. have written more. but havent typed them. tomorrow will continue.
Chengsong
parents:
43
diff
changeset
|
911 |
\begin{tabular}{lcl} |
4d674a971852
another changes. have written more. but havent typed them. tomorrow will continue.
Chengsong
parents:
43
diff
changeset
|
912 |
$\textit{fuse}\,bs\,(\textit{ZERO})$ & $\dn$ & $\textit{ZERO}$\\ |
4d674a971852
another changes. have written more. but havent typed them. tomorrow will continue.
Chengsong
parents:
43
diff
changeset
|
913 |
$\textit{fuse}\,bs\,(\textit{ONE}\,bs')$ & $\dn$ & |
4d674a971852
another changes. have written more. but havent typed them. tomorrow will continue.
Chengsong
parents:
43
diff
changeset
|
914 |
$\textit{ONE}\,(bs\,@\,bs')$\\ |
4d674a971852
another changes. have written more. but havent typed them. tomorrow will continue.
Chengsong
parents:
43
diff
changeset
|
915 |
$\textit{fuse}\,bs\,(\textit{CHAR}\,bs'\,c)$ & $\dn$ & |
4d674a971852
another changes. have written more. but havent typed them. tomorrow will continue.
Chengsong
parents:
43
diff
changeset
|
916 |
$\textit{CHAR}\,(bs\,@\,bs')\,c$\\ |
4d674a971852
another changes. have written more. but havent typed them. tomorrow will continue.
Chengsong
parents:
43
diff
changeset
|
917 |
$\textit{fuse}\,bs\,(\textit{ALT}\,bs'\,a_1\,a_2)$ & $\dn$ & |
4d674a971852
another changes. have written more. but havent typed them. tomorrow will continue.
Chengsong
parents:
43
diff
changeset
|
918 |
$\textit{ALT}\,(bs\,@\,bs')\,a_1\,a_2$\\ |
4d674a971852
another changes. have written more. but havent typed them. tomorrow will continue.
Chengsong
parents:
43
diff
changeset
|
919 |
$\textit{fuse}\,bs\,(\textit{SEQ}\,bs'\,a_1\,a_2)$ & $\dn$ & |
4d674a971852
another changes. have written more. but havent typed them. tomorrow will continue.
Chengsong
parents:
43
diff
changeset
|
920 |
$\textit{SEQ}\,(bs\,@\,bs')\,a_1\,a_2$\\ |
4d674a971852
another changes. have written more. but havent typed them. tomorrow will continue.
Chengsong
parents:
43
diff
changeset
|
921 |
$\textit{fuse}\,bs\,(\textit{STAR}\,bs'\,a)$ & $\dn$ & |
4d674a971852
another changes. have written more. but havent typed them. tomorrow will continue.
Chengsong
parents:
43
diff
changeset
|
922 |
$\textit{STAR}\,(bs\,@\,bs')\,a$ |
4d674a971852
another changes. have written more. but havent typed them. tomorrow will continue.
Chengsong
parents:
43
diff
changeset
|
923 |
\end{tabular} |
4d674a971852
another changes. have written more. but havent typed them. tomorrow will continue.
Chengsong
parents:
43
diff
changeset
|
924 |
\end{center} |
4d674a971852
another changes. have written more. but havent typed them. tomorrow will continue.
Chengsong
parents:
43
diff
changeset
|
925 |
|
70 | 926 |
\noindent |
927 |
After internalise we do successive derivative operations on the |
|
928 |
annotated regular expression. This derivative operation is the same as |
|
929 |
what we previously have for the simple regular expressions, except that |
|
930 |
we take special care of the bits :\\ |
|
931 |
||
932 |
%\begin{definition}{bder} |
|
36 | 933 |
\begin{center} |
934 |
\begin{tabular}{@{}lcl@{}} |
|
935 |
$(\textit{ZERO})\backslash c$ & $\dn$ & $\textit{ZERO}$\\ |
|
936 |
$(\textit{ONE}\;bs)\backslash c$ & $\dn$ & $\textit{ZERO}$\\ |
|
937 |
$(\textit{CHAR}\;bs\,d)\backslash c$ & $\dn$ & |
|
938 |
$\textit{if}\;c=d\; \;\textit{then}\; |
|
939 |
\textit{ONE}\;bs\;\textit{else}\;\textit{ZERO}$\\ |
|
940 |
$(\textit{ALT}\;bs\,a_1\,a_2)\backslash c$ & $\dn$ & |
|
941 |
$\textit{ALT}\,bs\,(a_1\backslash c)\,(a_2\backslash c)$\\ |
|
942 |
$(\textit{SEQ}\;bs\,a_1\,a_2)\backslash c$ & $\dn$ & |
|
943 |
$\textit{if}\;\textit{bnullable}\,a_1$\\ |
|
944 |
& &$\textit{then}\;\textit{ALT}\,bs\,(\textit{SEQ}\,[]\,(a_1\backslash c)\,a_2)$\\ |
|
945 |
& &$\phantom{\textit{then}\;\textit{ALT}\,bs\,}(\textit{fuse}\,(\textit{bmkeps}\,a_1)\,(a_2\backslash c))$\\ |
|
946 |
& &$\textit{else}\;\textit{SEQ}\,bs\,(a_1\backslash c)\,a_2$\\ |
|
947 |
$(\textit{STAR}\,bs\,a)\backslash c$ & $\dn$ & |
|
948 |
$\textit{SEQ}\;bs\,(\textit{fuse}\, [\Z] (r\backslash c))\, |
|
949 |
(\textit{STAR}\,[]\,r)$ |
|
950 |
\end{tabular} |
|
951 |
\end{center} |
|
37 | 952 |
%\end{definition} |
74
9e791ef6022f
just a merge - no changes
Christian Urban <urbanc@in.tum.de>
parents:
72
diff
changeset
|
953 |
|
9e791ef6022f
just a merge - no changes
Christian Urban <urbanc@in.tum.de>
parents:
72
diff
changeset
|
954 |
For instance, when we unfold $STAR \; bs \; a$ into a sequence, we |
9e791ef6022f
just a merge - no changes
Christian Urban <urbanc@in.tum.de>
parents:
72
diff
changeset
|
955 |
attach an additional bit Z to the front of $r \backslash c$ to indicate |
9e791ef6022f
just a merge - no changes
Christian Urban <urbanc@in.tum.de>
parents:
72
diff
changeset
|
956 |
that there is one more star iteration. The other example, the $SEQ$ |
9e791ef6022f
just a merge - no changes
Christian Urban <urbanc@in.tum.de>
parents:
72
diff
changeset
|
957 |
clause is more subtle-- when $a_1$ is $bnullable$(here bnullable is |
9e791ef6022f
just a merge - no changes
Christian Urban <urbanc@in.tum.de>
parents:
72
diff
changeset
|
958 |
exactly the same as nullable, except that it is for annotated regular |
9e791ef6022f
just a merge - no changes
Christian Urban <urbanc@in.tum.de>
parents:
72
diff
changeset
|
959 |
expressions, therefore we omit the definition). Assume that $bmkeps$ |
9e791ef6022f
just a merge - no changes
Christian Urban <urbanc@in.tum.de>
parents:
72
diff
changeset
|
960 |
correctly extracts the bitcode for how $a_1$ matches the string prior to |
9e791ef6022f
just a merge - no changes
Christian Urban <urbanc@in.tum.de>
parents:
72
diff
changeset
|
961 |
character c(more on this later), then the right branch of $ALTS$, which |
9e791ef6022f
just a merge - no changes
Christian Urban <urbanc@in.tum.de>
parents:
72
diff
changeset
|
962 |
is $fuse \; bmkeps \; a_1 (a_2 \backslash c)$ will collapse the regular |
9e791ef6022f
just a merge - no changes
Christian Urban <urbanc@in.tum.de>
parents:
72
diff
changeset
|
963 |
expression $a_1$(as it has already been fully matched) and store the |
9e791ef6022f
just a merge - no changes
Christian Urban <urbanc@in.tum.de>
parents:
72
diff
changeset
|
964 |
parsing information at the head of the regular expression $a_2 |
9e791ef6022f
just a merge - no changes
Christian Urban <urbanc@in.tum.de>
parents:
72
diff
changeset
|
965 |
\backslash c$ by fusing to it. The bitsequence $bs$, which was initially |
9e791ef6022f
just a merge - no changes
Christian Urban <urbanc@in.tum.de>
parents:
72
diff
changeset
|
966 |
attached to the head of $SEQ$, has now been elevated to the top-level of |
9e791ef6022f
just a merge - no changes
Christian Urban <urbanc@in.tum.de>
parents:
72
diff
changeset
|
967 |
ALT, as this information will be needed whichever way the $SEQ$ is |
9e791ef6022f
just a merge - no changes
Christian Urban <urbanc@in.tum.de>
parents:
72
diff
changeset
|
968 |
matched--no matter whether c belongs to $a_1$ or $ a_2$. After carefully |
9e791ef6022f
just a merge - no changes
Christian Urban <urbanc@in.tum.de>
parents:
72
diff
changeset
|
969 |
doing these derivatives and maintaining all the parsing information, we |
9e791ef6022f
just a merge - no changes
Christian Urban <urbanc@in.tum.de>
parents:
72
diff
changeset
|
970 |
complete the parsing by collecting the bits using a special $mkeps$ |
9e791ef6022f
just a merge - no changes
Christian Urban <urbanc@in.tum.de>
parents:
72
diff
changeset
|
971 |
function for annotated regular expressions--$bmkeps$: |
44
4d674a971852
another changes. have written more. but havent typed them. tomorrow will continue.
Chengsong
parents:
43
diff
changeset
|
972 |
|
4d674a971852
another changes. have written more. but havent typed them. tomorrow will continue.
Chengsong
parents:
43
diff
changeset
|
973 |
|
37 | 974 |
%\begin{definition}[\textit{bmkeps}]\mbox{} |
36 | 975 |
\begin{center} |
976 |
\begin{tabular}{lcl} |
|
977 |
$\textit{bmkeps}\,(\textit{ONE}\,bs)$ & $\dn$ & $bs$\\ |
|
978 |
$\textit{bmkeps}\,(\textit{ALT}\,bs\,a_1\,a_2)$ & $\dn$ & |
|
979 |
$\textit{if}\;\textit{bnullable}\,a_1$\\ |
|
980 |
& &$\textit{then}\;bs\,@\,\textit{bmkeps}\,a_1$\\ |
|
981 |
& &$\textit{else}\;bs\,@\,\textit{bmkeps}\,a_2$\\ |
|
982 |
$\textit{bmkeps}\,(\textit{SEQ}\,bs\,a_1\,a_2)$ & $\dn$ & |
|
983 |
$bs \,@\,\textit{bmkeps}\,a_1\,@\, \textit{bmkeps}\,a_2$\\ |
|
984 |
$\textit{bmkeps}\,(\textit{STAR}\,bs\,a)$ & $\dn$ & |
|
985 |
$bs \,@\, [\S]$ |
|
986 |
\end{tabular} |
|
987 |
\end{center} |
|
37 | 988 |
%\end{definition} |
70 | 989 |
|
990 |
\noindent |
|
44
4d674a971852
another changes. have written more. but havent typed them. tomorrow will continue.
Chengsong
parents:
43
diff
changeset
|
991 |
This function completes the parse tree information by |
45 | 992 |
travelling along the path on the regular expression that corresponds to a POSIX value snd collect all the bits, and |
72 | 993 |
using S to indicate the end of star iterations. If we take the bits produced by $bmkeps$ and decode it, |
44
4d674a971852
another changes. have written more. but havent typed them. tomorrow will continue.
Chengsong
parents:
43
diff
changeset
|
994 |
we get the parse tree we need, the working flow looks like this:\\ |
37 | 995 |
\begin{center} |
996 |
\begin{tabular}{lcl} |
|
997 |
$\textit{blexer}\;r\,s$ & $\dn$ & |
|
998 |
$\textit{let}\;a = (r^\uparrow)\backslash s\;\textit{in}$\\ |
|
999 |
& & $\;\;\textit{if}\; \textit{bnullable}(a)$\\ |
|
1000 |
& & $\;\;\textit{then}\;\textit{decode}\,(\textit{bmkeps}\,a)\,r$\\ |
|
1001 |
& & $\;\;\textit{else}\;\textit{None}$ |
|
1002 |
\end{tabular} |
|
1003 |
\end{center} |
|
53 | 1004 |
Here $(r^\uparrow)\backslash s$ is similar to what we have previously defined for |
1005 |
$r\backslash s$. |
|
30 | 1006 |
|
71 | 1007 |
The main point of the bit-sequences and annotated regular expressions |
30 | 1008 |
is that we can apply rather aggressive (in terms of size) |
1009 |
simplification rules in order to keep derivatives small. |
|
1010 |
||
1011 |
We have |
|
1012 |
developed such ``aggressive'' simplification rules and generated test |
|
1013 |
data that show that the expected bound can be achieved. Obviously we |
|
1014 |
could only partially cover the search space as there are infinitely |
|
1015 |
many regular expressions and strings. One modification we introduced |
|
1016 |
is to allow a list of annotated regular expressions in the |
|
1017 |
\textit{ALTS} constructor. This allows us to not just delete |
|
1018 |
unnecessary $\ZERO$s and $\ONE$s from regular expressions, but also |
|
1019 |
unnecessary ``copies'' of regular expressions (very similar to |
|
1020 |
simplifying $r + r$ to just $r$, but in a more general |
|
35 | 1021 |
setting). |
49 | 1022 |
Another modification is that we use simplification rules |
1023 |
inspired by Antimirov's work on partial derivatives. They maintain the |
|
1024 |
idea that only the first ``copy'' of a regular expression in an |
|
1025 |
alternative contributes to the calculation of a POSIX value. All |
|
1026 |
subsequent copies can be pruned from the regular expression. |
|
1027 |
||
52
25bbbb8b0e90
just in case of some accidents from erasing my work
Chengsong
parents:
51
diff
changeset
|
1028 |
A recursive definition of simplification function that looks similar to scala code is given below:\\ |
25bbbb8b0e90
just in case of some accidents from erasing my work
Chengsong
parents:
51
diff
changeset
|
1029 |
\begin{center} |
25bbbb8b0e90
just in case of some accidents from erasing my work
Chengsong
parents:
51
diff
changeset
|
1030 |
\begin{tabular}{@{}lcl@{}} |
25bbbb8b0e90
just in case of some accidents from erasing my work
Chengsong
parents:
51
diff
changeset
|
1031 |
$\textit{simp} \; a$ & $\dn$ & $\textit{a} \; \textit{if} \; a = (\textit{ONE} \; bs) \; or\; (\textit{CHAR} \, bs \; c) \; or\; (\textit{STAR}\; bs\; a_1)$\\ |
25bbbb8b0e90
just in case of some accidents from erasing my work
Chengsong
parents:
51
diff
changeset
|
1032 |
|
25bbbb8b0e90
just in case of some accidents from erasing my work
Chengsong
parents:
51
diff
changeset
|
1033 |
$\textit{simp} \; \textit{SEQ}\;bs\,a_1\,a_2$ & $\dn$ & $ (\textit{simp} \; a_1, \textit{simp} \; a_2) \; \textit{match} $ \\ |
25bbbb8b0e90
just in case of some accidents from erasing my work
Chengsong
parents:
51
diff
changeset
|
1034 |
&&$\textit{case} \; (0, \_) \Rightarrow 0$ \\ |
25bbbb8b0e90
just in case of some accidents from erasing my work
Chengsong
parents:
51
diff
changeset
|
1035 |
&&$ \textit{case} \; (\_, 0) \Rightarrow 0$ \\ |
25bbbb8b0e90
just in case of some accidents from erasing my work
Chengsong
parents:
51
diff
changeset
|
1036 |
&&$ \textit{case} \; (1, a_2') \Rightarrow \textit{fuse} \; bs \; a_2'$ \\ |
25bbbb8b0e90
just in case of some accidents from erasing my work
Chengsong
parents:
51
diff
changeset
|
1037 |
&&$ \textit{case} \; (a_1', 1) \Rightarrow \textit{fuse} \; bs \; a_1'$ \\ |
25bbbb8b0e90
just in case of some accidents from erasing my work
Chengsong
parents:
51
diff
changeset
|
1038 |
&&$ \textit{case} \; (a_1', a_2') \Rightarrow \textit{SEQ} \; bs \; a_1' \; a_2'$ \\ |
25bbbb8b0e90
just in case of some accidents from erasing my work
Chengsong
parents:
51
diff
changeset
|
1039 |
|
72 | 1040 |
$\textit{simp} \; \textit{ALTS}\;bs\,as$ & $\dn$ & $\textit{ distinct}( \textit{flatten} ( \textit{map simp as})) \; \textit{match} $ \\ |
52
25bbbb8b0e90
just in case of some accidents from erasing my work
Chengsong
parents:
51
diff
changeset
|
1041 |
&&$\textit{case} \; [] \Rightarrow 0$ \\ |
25bbbb8b0e90
just in case of some accidents from erasing my work
Chengsong
parents:
51
diff
changeset
|
1042 |
&&$ \textit{case} \; a :: [] \Rightarrow \textit{fuse bs a}$ \\ |
25bbbb8b0e90
just in case of some accidents from erasing my work
Chengsong
parents:
51
diff
changeset
|
1043 |
&&$ \textit{case} \; as' \Rightarrow \textit{ALT bs as'}$ |
25bbbb8b0e90
just in case of some accidents from erasing my work
Chengsong
parents:
51
diff
changeset
|
1044 |
\end{tabular} |
25bbbb8b0e90
just in case of some accidents from erasing my work
Chengsong
parents:
51
diff
changeset
|
1045 |
\end{center} |
47 | 1046 |
|
1047 |
The simplification does a pattern matching on the regular expression. When it detected that |
|
72 | 1048 |
the regular expression is an alternative or sequence, |
1049 |
it will try to simplify its children regular expressions |
|
1050 |
recursively and then see if one of the children turn |
|
1051 |
into $\ZERO$ or $\ONE$, which might trigger further simplification |
|
1052 |
at the current level. The most involved part is the $\textit{ALTS}$ |
|
1053 |
clause, where we use two auxiliary functions |
|
1054 |
flatten and distinct to open up nested $\textit{ALTS}$ and |
|
1055 |
reduce as many duplicates as possible. |
|
1056 |
Function distinct keeps the first occurring copy only and |
|
1057 |
remove all later ones when detected duplicates. |
|
1058 |
Function flatten opens up nested \textit{ALT}. Its recursive |
|
1059 |
definition is given below: |
|
53 | 1060 |
\begin{center} |
1061 |
\begin{tabular}{@{}lcl@{}} |
|
70 | 1062 |
$\textit{flatten} \; (\textit{ALT}\;bs\,as) :: as'$ & $\dn$ & $(\textit{map} \; |
1063 |
(\textit{fuse}\;bs)\; \textit{as}) \; @ \; \textit{flatten} \; as' $ \\ |
|
53 | 1064 |
$\textit{flatten} \; \textit{ZERO} :: as'$ & $\dn$ & $ \textit{flatten} \; as' $ \\ |
70 | 1065 |
$\textit{flatten} \; a :: as'$ & $\dn$ & $a :: \textit{flatten} \; as'$ \quad(otherwise) |
53 | 1066 |
\end{tabular} |
1067 |
\end{center} |
|
1068 |
||
70 | 1069 |
\noindent |
71 | 1070 |
Here flatten behaves like the traditional functional programming flatten function, except that it also removes $\ZERO$s. |
1071 |
What it does is basically removing parentheses like changing $a+(b+c)$ into $a+b+c$. |
|
47 | 1072 |
|
53 | 1073 |
Suppose we apply simplification after each derivative step, |
1074 |
and view these two operations as an atomic one: $a \backslash_{simp} c \dn \textit{simp}(a \backslash c)$. |
|
1075 |
Then we can use the previous natural extension from derivative w.r.t character to derivative w.r.t string: |
|
1076 |
||
1077 |
\begin{center} |
|
1078 |
\begin{tabular}{lcl} |
|
1079 |
$r \backslash_{simp} (c\!::\!s) $ & $\dn$ & $(r \backslash_{simp} c) \backslash_{simp} s$ \\ |
|
1080 |
$r \backslash [\,] $ & $\dn$ & $r$ |
|
1081 |
\end{tabular} |
|
1082 |
\end{center} |
|
1083 |
||
1084 |
we get an optimized version of the algorithm: |
|
1085 |
\begin{center} |
|
1086 |
\begin{tabular}{lcl} |
|
1087 |
$\textit{blexer\_simp}\;r\,s$ & $\dn$ & |
|
1088 |
$\textit{let}\;a = (r^\uparrow)\backslash_{simp} s\;\textit{in}$\\ |
|
1089 |
& & $\;\;\textit{if}\; \textit{bnullable}(a)$\\ |
|
1090 |
& & $\;\;\textit{then}\;\textit{decode}\,(\textit{bmkeps}\,a)\,r$\\ |
|
1091 |
& & $\;\;\textit{else}\;\textit{None}$ |
|
1092 |
\end{tabular} |
|
1093 |
\end{center} |
|
48 | 1094 |
|
1095 |
This algorithm effectively keeps the regular expression size small, for example, |
|
1096 |
with this simplification our previous $(a + aa)^*$ example's 8000 nodes will be reduced to only 6 and stay constant, however long the input string is. |
|
35 | 1097 |
|
30 | 1098 |
|
35 | 1099 |
|
70 | 1100 |
\section{Current Work} |
1101 |
||
1102 |
We are currently engaged in two tasks related to this algorithm. |
|
1103 |
||
72 | 1104 |
|
49 | 1105 |
The first one is proving that our simplification rules |
30 | 1106 |
actually do not affect the POSIX value that should be generated by the |
49 | 1107 |
algorithm according to the specification of a POSIX value |
1108 |
and furthermore obtain a much |
|
1109 |
tighter bound on the sizes of derivatives. The result is that our |
|
1110 |
algorithm should be correct and faster on all inputs. The original |
|
1111 |
blow-up, as observed in JavaScript, Python and Java, would be excluded |
|
1112 |
from happening in our algorithm.For |
|
30 | 1113 |
this proof we use the theorem prover Isabelle. Once completed, this |
1114 |
result will advance the state-of-the-art: Sulzmann and Lu wrote in |
|
1115 |
their paper \cite{Sulzmann2014} about the bitcoded ``incremental |
|
1116 |
parsing method'' (that is the matching algorithm outlined in this |
|
1117 |
section): |
|
1118 |
||
1119 |
\begin{quote}\it |
|
1120 |
``Correctness Claim: We further claim that the incremental parsing |
|
1121 |
method in Figure~5 in combination with the simplification steps in |
|
1122 |
Figure 6 yields POSIX parse trees. We have tested this claim |
|
1123 |
extensively by using the method in Figure~3 as a reference but yet |
|
1124 |
have to work out all proof details.'' |
|
1125 |
\end{quote} |
|
1126 |
||
1127 |
\noindent |
|
74
9e791ef6022f
just a merge - no changes
Christian Urban <urbanc@in.tum.de>
parents:
72
diff
changeset
|
1128 |
We would settle the correctness claim. It is relatively straightforward |
9e791ef6022f
just a merge - no changes
Christian Urban <urbanc@in.tum.de>
parents:
72
diff
changeset
|
1129 |
to establish that after one simplification step, the part of a nullable |
9e791ef6022f
just a merge - no changes
Christian Urban <urbanc@in.tum.de>
parents:
72
diff
changeset
|
1130 |
derivative that corresponds to a POSIX value remains intact and can |
9e791ef6022f
just a merge - no changes
Christian Urban <urbanc@in.tum.de>
parents:
72
diff
changeset
|
1131 |
still be collected, in other words, |
9e791ef6022f
just a merge - no changes
Christian Urban <urbanc@in.tum.de>
parents:
72
diff
changeset
|
1132 |
|
71 | 1133 |
\begin{center} |
1134 |
$\textit{bmkeps} \; r = \textit{bmkeps} \; \textit{simp} \; r\;( r\; \textit{nullable})$ |
|
1135 |
\end{center} |
|
74
9e791ef6022f
just a merge - no changes
Christian Urban <urbanc@in.tum.de>
parents:
72
diff
changeset
|
1136 |
|
9e791ef6022f
just a merge - no changes
Christian Urban <urbanc@in.tum.de>
parents:
72
diff
changeset
|
1137 |
\noindent |
9e791ef6022f
just a merge - no changes
Christian Urban <urbanc@in.tum.de>
parents:
72
diff
changeset
|
1138 |
as this basically comes down to proving actions like removing the |
9e791ef6022f
just a merge - no changes
Christian Urban <urbanc@in.tum.de>
parents:
72
diff
changeset
|
1139 |
additional $r$ in $r+r$ does not delete important POSIX information in |
9e791ef6022f
just a merge - no changes
Christian Urban <urbanc@in.tum.de>
parents:
72
diff
changeset
|
1140 |
a regular expression. The hardcore of this problem is to prove that |
9e791ef6022f
just a merge - no changes
Christian Urban <urbanc@in.tum.de>
parents:
72
diff
changeset
|
1141 |
|
71 | 1142 |
\begin{center} |
1143 |
$\textit{bmkeps} \; \textit{blexer}\_{simp} \; r = \textit{bmkeps} \; \textit{blexer} \; \textit{simp} \; r$ |
|
1144 |
\end{center} |
|
74
9e791ef6022f
just a merge - no changes
Christian Urban <urbanc@in.tum.de>
parents:
72
diff
changeset
|
1145 |
|
9e791ef6022f
just a merge - no changes
Christian Urban <urbanc@in.tum.de>
parents:
72
diff
changeset
|
1146 |
\noindent |
71 | 1147 |
That is, if we do derivative on regular expression r and the simplified version, |
1148 |
they can still provide the same POSIX value if there is one . |
|
1149 |
This is not as straightforward as the previous proposition, as the two regular expressions $r$ and $\textit{simp}\; r$ |
|
1150 |
might become very different regular expressions after repeated application of $\textit{simp}$ and derivative. |
|
1151 |
The crucial point is to find the indispensable information of |
|
1152 |
a regular expression and how it is kept intact during simplification so that it performs |
|
1153 |
as good as a regular expression that has not been simplified in the subsequent derivative operations. |
|
1154 |
To aid this, we use the helping function retrieve described by Sulzmann and Lu: |
|
49 | 1155 |
\\definition of retrieve\\ |
72 | 1156 |
This function assembled the bitcode that corresponds to a parse tree for how the current |
71 | 1157 |
derivative matches the suffix of the string(the characters that have not yet appeared, but is stored in the value). |
72 | 1158 |
Sulzmann and Lu used this to connect the bitcoded algorithm to the older algorithm by the following equation: |
1159 |
\begin{center} |
|
1160 |
$inj \;a\; c \; v = \textit{decode} \; (\textit{retrieve}\; ((\textit{internalise}\; r)\backslash_{simp} c) v)$ |
|
1161 |
\end{center} |
|
1162 |
A little fact that needs to be stated to help comprehension: |
|
1163 |
\begin{center} |
|
1164 |
$r^\uparrow = a$($a$ stands for $\textit{annotated}).$ |
|
1165 |
\end{center} |
|
1166 |
Ausaf and Urban also used this fact to prove the correctness of bitcoded algorithm without simplification. |
|
50 | 1167 |
Our purpose of using this, however, is try to establish \\ |
53 | 1168 |
$ \textit{retrieve} \; a \; v \;=\; \textit{retrieve} \; \textit{simp}(a) \; v'.$\\ |
1169 |
The idea is that using $v'$, |
|
71 | 1170 |
a simplified version of $v$ that possibly had gone through the same simplification step as $\textit{simp}(a)$ we are still able to extract the bit-sequence that gives the same parsing information as the unsimplified one. |
53 | 1171 |
After establishing this, we might be able to finally bridge the gap of proving\\ |
1172 |
$\textit{retrieve} \; r \backslash s \; v = \;\textit{retrieve} \; \textit{simp}(r) \backslash s \; v'$\\ |
|
1173 |
and subsequently\\ |
|
1174 |
$\textit{retrieve} \; r \backslash s \; v\; = \; \textit{retrieve} \; r \backslash_{simp} s \; v'$.\\ |
|
58 | 1175 |
This proves that our simplified version of regular expression still contains all the bitcodes needed. |
49 | 1176 |
|
72 | 1177 |
|
70 | 1178 |
The second task is to speed up the more aggressive simplification. |
1179 |
Currently it is slower than a naive simplification(the naive version as |
|
1180 |
implemented in ADU of course can explode in some cases). So it needs to |
|
1181 |
be explored how to make it faster. Our possibility would be to explore |
|
1182 |
again the connection to DFAs. This is very much work in progress. |
|
30 | 1183 |
|
1184 |
\section{Conclusion} |
|
1185 |
||
1186 |
In this PhD-project we are interested in fast algorithms for regular |
|
1187 |
expression matching. While this seems to be a ``settled'' area, in |
|
1188 |
fact interesting research questions are popping up as soon as one steps |
|
1189 |
outside the classic automata theory (for example in terms of what kind |
|
1190 |
of regular expressions are supported). The reason why it is |
|
1191 |
interesting for us to look at the derivative approach introduced by |
|
1192 |
Brzozowski for regular expression matching, and then much further |
|
1193 |
developed by Sulzmann and Lu, is that derivatives can elegantly deal |
|
1194 |
with some of the regular expressions that are of interest in ``real |
|
1195 |
life''. This includes the not-regular expression, written $\neg\,r$ |
|
1196 |
(that is all strings that are not recognised by $r$), but also bounded |
|
1197 |
regular expressions such as $r^{\{n\}}$ and $r^{\{n..m\}}$). There is |
|
1198 |
also hope that the derivatives can provide another angle for how to |
|
1199 |
deal more efficiently with back-references, which are one of the |
|
1200 |
reasons why regular expression engines in JavaScript, Python and Java |
|
1201 |
choose to not implement the classic automata approach of transforming |
|
1202 |
regular expressions into NFAs and then DFAs---because we simply do not |
|
1203 |
know how such back-references can be represented by DFAs. |
|
1204 |
||
1205 |
||
1206 |
\bibliographystyle{plain} |
|
1207 |
\bibliography{root} |
|
1208 |
||
1209 |
||
1210 |
\end{document} |