\documentclass[a4paper,UKenglish]{lipics}
\usepackage{graphic}
\usepackage{data}
\usepackage{tikz-cd}
\usepackage{algorithm}
\usepackage{amsmath}
\usepackage[noend]{algpseudocode}
\usepackage{enumitem}
% \documentclass{article}
%\usepackage[utf8]{inputenc}
%\usepackage[english]{babel}
%\usepackage{listings}
% \usepackage{amsthm}
% \usepackage{hyperref}
% \usepackage[margin=0.5in]{geometry}
%\usepackage{pmboxdraw}
\title{POSIX Regular Expression Matching and Lexing}
\author{Chengsong Tan}
\affil{King's College London\\
London, UK\\
\texttt{chengsong.tan@kcl.ac.uk}}
\authorrunning{Chengsong Tan}
\Copyright{Chengsong Tan}
\newcommand{\dn}{\stackrel{\mbox{\scriptsize def}}{=}}%
\newcommand{\ZERO}{\mbox{\bf 0}}
\newcommand{\ONE}{\mbox{\bf 1}}
\def\lexer{\mathit{lexer}}
\def\mkeps{\mathit{mkeps}}
\def\inj{\mathit{inj}}
\def\Empty{\mathit{Empty}}
\def\Left{\mathit{Left}}
\def\Right{\mathit{Right}}
\def\Stars{\mathit{Stars}}
\def\Char{\mathit{Char}}
\def\Seq{\mathit{Seq}}
\def\Der{\mathit{Der}}
\def\nullable{\mathit{nullable}}
\def\Z{\mathit{Z}}
\def\S{\mathit{S}}
%\theoremstyle{theorem}
%\newtheorem{theorem}{Theorem}
%\theoremstyle{lemma}
%\newtheorem{lemma}{Lemma}
%\newcommand{\lemmaautorefname}{Lemma}
%\theoremstyle{definition}
%\newtheorem{definition}{Definition}
\algnewcommand\algorithmicswitch{\textbf{switch}}
\algnewcommand\algorithmiccase{\textbf{case}}
\algnewcommand\algorithmicassert{\texttt{assert}}
\algnewcommand\Assert[1]{\State \algorithmicassert(#1)}%
% New "environments"
\algdef{SE}[SWITCH]{Switch}{EndSwitch}[1]{\algorithmicswitch\ #1\ \algorithmicdo}{\algorithmicend\ \algorithmicswitch}%
\algdef{SE}[CASE]{Case}{EndCase}[1]{\algorithmiccase\ #1}{\algorithmicend\ \algorithmiccase}%
\algtext*{EndSwitch}%
\algtext*{EndCase}%
\begin{document}
\maketitle
\begin{abstract}
Brzozowski introduced in 1964 a beautifully simple algorithm for
regular expression matching based on the notion of derivatives of
regular expressions. In 2014, Sulzmann and Lu extended this
algorithm to not just give a YES/NO answer for whether or not a
regular expression matches a string, but in case it matches also
\emph{how} it matches the string. This is important for
applications such as lexing (tokenising a string). The problem is to
make the algorithm by Sulzmann and Lu fast on all inputs without
breaking its correctness. We have already developed some
simplification rules for this, but have not proved yet that they
preserve the correctness of the algorithm. We also have not yet
looked at extended regular expressions, such as bounded repetitions,
negation and back-references.
\end{abstract}
\section{Introduction}
This PhD-project is about regular expression matching and
lexing. Given the maturity of this topic, the reader might wonder:
Surely, regular expressions must have already been studied to death?
What could possibly be \emph{not} known in this area? And surely all
implemented algorithms for regular expression matching are blindingly
fast?
Unfortunately these preconceptions are not supported by evidence: Take
for example the regular expression $(a^*)^*\,b$ and ask whether
strings of the form $aa..a$ match this regular
expression. Obviously they do not match---the expected $b$ in the last
position is missing. One would expect that modern regular expression
matching engines can find this out very quickly. Alas, if one tries
this example in JavaScript, Python or Java 8 with strings like 28
$a$'s, one discovers that this decision takes around 30 seconds and
takes considerably longer when adding a few more $a$'s, as the graphs
below show:
\begin{center}
\begin{tabular}{@{}c@{\hspace{0mm}}c@{\hspace{0mm}}c@{}}
\begin{tikzpicture}
\begin{axis}[
xlabel={$n$},
x label style={at={(1.05,-0.05)}},
ylabel={time in secs},
enlargelimits=false,
xtick={0,5,...,30},
xmax=33,
ymax=35,
ytick={0,5,...,30},
scaled ticks=false,
axis lines=left,
width=5cm,
height=4cm,
legend entries={JavaScript},
legend pos=north west,
legend cell align=left]
\addplot[red,mark=*, mark options={fill=white}] table {re-js.data};
\end{axis}
\end{tikzpicture}
&
\begin{tikzpicture}
\begin{axis}[
xlabel={$n$},
x label style={at={(1.05,-0.05)}},
%ylabel={time in secs},
enlargelimits=false,
xtick={0,5,...,30},
xmax=33,
ymax=35,
ytick={0,5,...,30},
scaled ticks=false,
axis lines=left,
width=5cm,
height=4cm,
legend entries={Python},
legend pos=north west,
legend cell align=left]
\addplot[blue,mark=*, mark options={fill=white}] table {re-python2.data};
\end{axis}
\end{tikzpicture}
&
\begin{tikzpicture}
\begin{axis}[
xlabel={$n$},
x label style={at={(1.05,-0.05)}},
%ylabel={time in secs},
enlargelimits=false,
xtick={0,5,...,30},
xmax=33,
ymax=35,
ytick={0,5,...,30},
scaled ticks=false,
axis lines=left,
width=5cm,
height=4cm,
legend entries={Java 8},
legend pos=north west,
legend cell align=left]
\addplot[cyan,mark=*, mark options={fill=white}] table {re-java.data};
\end{axis}
\end{tikzpicture}\\
\multicolumn{3}{c}{Graphs: Runtime for matching $(a^*)^*\,b$ with strings
of the form $\underbrace{aa..a}_{n}$.}
\end{tabular}
\end{center}
\noindent These are clearly abysmal and possibly surprising results.
One would expect these systems doing much better than that---after
all, given a DFA and a string, whether a string is matched by this DFA
should be linear.
Admittedly, the regular expression $(a^*)^*\,b$ is carefully chosen to
exhibit this ``exponential behaviour''. Unfortunately, such regular
expressions are not just a few ``outliers'', but actually they are
frequent enough that a separate name has been created for
them---\emph{evil regular expressions}. In empiric work, Davis et al
report that they have found thousands of such evil regular expressions
in the JavaScript and Python ecosystems \cite{Davis18}.
This exponential blowup sometimes causes pain in real life:
for example on 20 July 2016 one evil regular expression brought the
webpage \href{http://stackexchange.com}{Stack Exchange} to its
knees.\footnote{https://stackstatus.net/post/147710624694/outage-postmortem-july-20-2016}
In this instance, a regular expression intended to just trim white
spaces from the beginning and the end of a line actually consumed
massive amounts of CPU-resources and because of this the web servers
ground to a halt. This happened when a post with 20,000 white spaces
was submitted, but importantly the white spaces were neither at the
beginning nor at the end. As a result, the regular expression matching
engine needed to backtrack over many choices.
The underlying problem is that many ``real life'' regular expression
matching engines do not use DFAs for matching. This is because they
support regular expressions that are not covered by the classical
automata theory, and in this more general setting there are quite a
few research questions still unanswered and fast algorithms still need
to be developed (for example how to include bounded repetitions, negation
and back-references).
There is also another under-researched problem to do with regular
expressions and lexing, i.e.~the process of breaking up strings into
sequences of tokens according to some regular expressions. In this
setting one is not just interested in whether or not a regular
expression matches a string, but if it matches also in \emph{how} it
matches the string. Consider for example a regular expression
$r_{key}$ for recognising keywords such as \textit{if}, \textit{then}
and so on; and a regular expression $r_{id}$ for recognising
identifiers (say, a single character followed by characters or
numbers). One can then form the compound regular expression
$(r_{key} + r_{id})^*$ and use it to tokenise strings. But then how
should the string \textit{iffoo} be tokenised? It could be tokenised
as a keyword followed by an identifier, or the entire string as a
single identifier. Similarly, how should the string \textit{if} be
tokenised? Both regular expressions, $r_{key}$ and $r_{id}$, would
``fire''---so is it an identifier or a keyword? While in applications
there is a well-known strategy to decide these questions, called POSIX
matching, only relatively recently precise definitions of what POSIX
matching actually means have been formalised
\cite{AusafDyckhoffUrban2016,OkuiSuzuki2010,Vansummeren2006}.
Such a definition has also been given by Sulzmann and Lu \cite{Sulzmann2014}, but the
corresponding correctness proof turned out to be faulty \cite{AusafDyckhoffUrban2016}.
Roughly, POSIX matching means matching the longest initial substring.
In the case of a tie, the initial submatch is chosen according to some priorities attached to the
regular expressions (e.g.~keywords have a higher priority than
identifiers). This sounds rather simple, but according to Grathwohl et
al \cite[Page 36]{CrashCourse2014} this is not the case. They wrote:
\begin{quote}
\it{}``The POSIX strategy is more complicated than the greedy because of
the dependence on information about the length of matched strings in the
various subexpressions.''
\end{quote}
\noindent
This is also supported by evidence collected by Kuklewicz
\cite{Kuklewicz} who noticed that a number of POSIX regular expression
matchers calculate incorrect results.
Our focus is on an algorithm introduced by Sulzmann and Lu in 2014 for
regular expression matching according to the POSIX strategy
\cite{Sulzmann2014}. Their algorithm is based on an older algorithm by
Brzozowski from 1964 where he introduced the notion of derivatives of
regular expressions \cite{Brzozowski1964}. We shall briefly explain
this algorithms next.
\section{The Algorithm by Brzozowski based on Derivatives of Regular
Expressions}
Suppose (basic) regular expressions are given by the following grammar:
\[ r ::= \ZERO \mid \ONE
\mid c
\mid r_1 \cdot r_2
\mid r_1 + r_2
\mid r^*
\]
\noindent
The intended meaning of the constructors is as follows: $\ZERO$
cannot match any string, $\ONE$ can match the empty string, the
character regular expression $c$ can match the character $c$, and so
on.
The brilliant contribution by Brzozowski is the notion of
\emph{derivatives} of regular expressions. The idea behind this
notion is as follows: suppose a regular expression $r$ can match a
string of the form $c\!::\! s$ (that is a list of characters starting
with $c$), what does the regular expression look like that can match
just $s$? Brzozowski gave a neat answer to this question. He started
with the definition of $nullable$:
\begin{center}
\begin{tabular}{lcl}
$\nullable(\ZERO)$ & $\dn$ & $\mathit{false}$ \\
$\nullable(\ONE)$ & $\dn$ & $\mathit{true}$ \\
$\nullable(c)$ & $\dn$ & $\mathit{false}$ \\
$\nullable(r_1 + r_2)$ & $\dn$ & $\nullable(r_1) \vee \nullable(r_2)$ \\
$\nullable(r_1\cdot r_2)$ & $\dn$ & $\nullable(r_1) \wedge \nullable(r_2)$ \\
$\nullable(r^*)$ & $\dn$ & $\mathit{true}$ \\
\end{tabular}
\end{center}
This function simply tests whether the empty string is in $L(r)$.
He then defined
the following operation on regular expressions, written
$r\backslash c$ (the derivative of $r$ w.r.t.~the character $c$):
\begin{center}
\begin{tabular}{lcl}
$\ZERO \backslash c$ & $\dn$ & $\ZERO$\\
$\ONE \backslash c$ & $\dn$ & $\ZERO$\\
$d \backslash c$ & $\dn$ &
$\mathit{if} \;c = d\;\mathit{then}\;\ONE\;\mathit{else}\;\ZERO$\\
$(r_1 + r_2)\backslash c$ & $\dn$ & $r_1 \backslash c \,+\, r_2 \backslash c$\\
$(r_1 \cdot r_2)\backslash c$ & $\dn$ & $\mathit{if} \, nullable(r_1)$\\
& & $\mathit{then}\;(r_1\backslash c) \cdot r_2 \,+\, r_2\backslash c$\\
& & $\mathit{else}\;(r_1\backslash c) \cdot r_2$\\
$(r^*)\backslash c$ & $\dn$ & $(r\backslash c) \cdot r^*$\\
\end{tabular}
\end{center}
%Assuming the classic notion of a
%\emph{language} of a regular expression, written $L(\_)$, t
\noindent
The main property of the derivative operation is that
\begin{center}
$c\!::\!s \in L(r)$ holds
if and only if $s \in L(r\backslash c)$.
\end{center}
\noindent
For us the main advantage is that derivatives can be
straightforwardly implemented in any functional programming language,
and are easily definable and reasoned about in theorem provers---the
definitions just consist of inductive datatypes and simple recursive
functions. Moreover, the notion of derivatives can be easily
generalised to cover extended regular expression constructors such as
the not-regular expression, written $\neg\,r$, or bounded repetitions
(for example $r^{\{n\}}$ and $r^{\{n..m\}}$), which cannot be so
straightforwardly realised within the classic automata approach.
For the moment however, we focus only on the usual basic regular expressions.
Now if we want to find out whether a string $s$ matches with a regular
expression $r$, build the derivatives of $r$ w.r.t.\ (in succession)
all the characters of the string $s$. Finally, test whether the
resulting regular expression can match the empty string. If yes, then
$r$ matches $s$, and no in the negative case. To implement this idea
we can generalise the derivative operation to strings like this:
\begin{center}
\begin{tabular}{lcl}
$r \backslash (c\!::\!s) $ & $\dn$ & $(r \backslash c) \backslash s$ \\
$r \backslash [\,] $ & $\dn$ & $r$
\end{tabular}
\end{center}
\noindent
and then define as regular-expression matching algorithm:
\[
match\;s\;r \;\dn\; nullable(r\backslash s)
\]
\noindent
This algorithm can be illustrated as follows:
\begin{equation}\label{graph:*}
\begin{tikzcd}
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}
\end{tikzcd}
\end{equation}
\noindent
where we start with a regular expression $r_0$, build successive
derivatives until we exhaust the string and then use \textit{nullable}
to test whether the result can match the empty string. It can be
relatively easily shown that this matcher is correct (that is given
$s$ and $r$, it generates YES if and only if $s \in L(r)$).
\section{Values and the Algorithm by Sulzmann and Lu}
One limitation, however, of Brzozowski's algorithm is that it only
produces a YES/NO answer for whether a string is being matched by a
regular expression. Sulzmann and Lu~\cite{Sulzmann2014} extended this
algorithm to allow generation of an actual matching, called a
\emph{value}. Values and regular expressions correspond to each
other as illustrated in the following table:
\begin{center}
\begin{tabular}{c@{\hspace{20mm}}c}
\begin{tabular}{@{}rrl@{}}
\multicolumn{3}{@{}l}{\textbf{Regular Expressions}}\medskip\\
$r$ & $::=$ & $\ZERO$\\
& $\mid$ & $\ONE$ \\
& $\mid$ & $c$ \\
& $\mid$ & $r_1 \cdot r_2$\\
& $\mid$ & $r_1 + r_2$ \\
\\
& $\mid$ & $r^*$ \\
\end{tabular}
&
\begin{tabular}{@{\hspace{0mm}}rrl@{}}
\multicolumn{3}{@{}l}{\textbf{Values}}\medskip\\
$v$ & $::=$ & \\
& & $\Empty$ \\
& $\mid$ & $\Char(c)$ \\
& $\mid$ & $\Seq\,v_1\, v_2$\\
& $\mid$ & $\Left(v)$ \\
& $\mid$ & $\Right(v)$ \\
& $\mid$ & $\Stars\,[v_1,\ldots\,v_n]$ \\
\end{tabular}
\end{tabular}
\end{center}
\noindent
The idea of values is to express parse trees. Suppose a flatten
operation, written $|v|$, which we can use to extract the underlying
string of $v$. For example, $|\mathit{Seq} \, (\textit{Char x}) \,
(\textit{Char y})|$ is the string $xy$. We omit the straightforward
definition of flatten. Using flatten, we can describe how
values encode parse trees: $\Seq\,v_1\, v_2$ tells us how the
string $|v_1| @ |v_2|$ matches the regex $r_1 \cdot r_2$: $r_1$
matches $|v_1|$ and, respectively, $r_2$ matches $|v_2|$. Exactly how
these two are matched is contained in the sub-structure of $v_1$ and
$v_2$.
To give a concrete example of how value works, consider the string $xy$
and the regular expression $(x + (y + xy))^*$. We can view this regular
expression as a tree and if the string $xy$ is matched by two Star
``iterations'', then the $x$ is matched by the left-most alternative in
this tree and the $y$ by the right-left alternative. This suggests to
record this matching as
\begin{center}
$\Stars\,[\Left\,(\Char\,x), \Right(\Left(\Char\,y))]$
\end{center}
\noindent
where $\Stars$ records how many
iterations were used; and $\Left$, respectively $\Right$, which
alternative is used. The value for
matching $xy$ in a single ``iteration'', i.e.~the POSIX value,
would look as follows
\begin{center}
$\Stars\,[\Seq\,(\Char\,x)\,(\Char\,y)]$
\end{center}
\noindent
where $\Stars$ has only a single-element list for the single iteration
and $\Seq$ indicates that $xy$ is matched by a sequence regular
expression.
The contribution of Sulzmann and Lu is an extension of Brzozowski's
algorithm by a second phase (the first phase being building successive
derivatives---see \eqref{graph:*}). In this second phase, a POSIX value
is generated assuming the regular expression matches the string.
Pictorially, the algorithm as follows:
\begin{center}
\begin{tikzcd}
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] \\
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]
\end{tikzcd}
\end{center}
\noindent
We shall briefly explain this algorithm. For the convenience of
explanation, we have the following notations: the regular expression we
start with is $r_0$ and the string $s$ is composed characters $c_0 c_1
\ldots c_n$. First, we build the derivatives $r_1$, $r_2$, \ldots, using
the characters $c_0$, $c_1$,\ldots until we exhaust the string and
arrive at the derivative $r_n$. We test whether this derivative is
$\textit{nullable}$ or not. If not, we know the string does not match
$r$ and no value needs to be generated. If yes, we start building the
parse tree incrementally by \emph{injecting} back the characters into
the values $v_n, \ldots, v_0$. We first call the function
$\textit{mkeps}$, which builds the parse tree for how the empty string
is matched the empty regular expression $r_n$. This function is defined
as
\begin{center}
\begin{tabular}{lcl}
$\mkeps(\ONE)$ & $\dn$ & $\Empty$ \\
$\mkeps(r_{1}+r_{2})$ & $\dn$
& \textit{if} $\nullable(r_{1})$\\
& & \textit{then} $\Left(\mkeps(r_{1}))$\\
& & \textit{else} $\Right(\mkeps(r_{2}))$\\
$\mkeps(r_1\cdot r_2)$ & $\dn$ & $\Seq\,(\mkeps\,r_1)\,(\mkeps\,r_2)$\\
$mkeps(r^*)$ & $\dn$ & $\Stars\,[]$
\end{tabular}
\end{center}
After this, we inject back the characters one by one in order to build
the parse tree $v_i$ for how the regex $r_i$ matches the string
$s_i$ ($s_i$ means the string s with the first $i$ characters being
chopped off) from the previous parse tree. After $n$ transformations, we
get the parse tree for how $r_0$ matches $s$, exactly as we wanted. An
inductive proof can be routinely established.
It is instructive to see how it works by a little example. Suppose we have a regular expression $(a+b+ab+c+abc)*$ and we want to match it against the string $abc$. By POSIX rules the lexer should go for the longest matching, i.e. it should match the string $abc$ in one star iteration, using the longest string $abc$ in the sub-expression $a+b+ab+c+abc$(we use $r$ to denote this sub-expression for conciseness). Here is how the lexer achieves a parse tree for this matching.
First, we build successive derivatives until we exhaust the string, as illustrated here( we omitted some parenthesis for better readability):
\[ r^* \xrightarrow{\backslash a} r_1 = (1+0+1 \cdot b + 0 + 1 \cdot b \cdot c) \cdot r* \xrightarrow{\backslash b}\]
\[r_2 = (0+0+1 \cdot 1 + 0 + 1 \cdot 1 \cdot c) \cdot r^* +(0+1+0 + 0 + 0) \cdot r* \xrightarrow{\backslash c}\]
\[r_3 = ((0+0+0 + 0 + 1 \cdot 1 \cdot 1) \cdot r^* + (0+0+0 + 1 + 0) \cdot r*) +((0+1+0 + 0 + 0) \cdot r*+(0+0+0 + 1 + 0) \cdot r* )
\]
Now instead of using $nullable$ to give a $yes$, we call $mkeps$ to construct a parse tree for how $r_3$ matched the string $abc$. $mkeps$ gives the following value $v_3$: \\$Left(Left(Seq(Right(Right(Right(Seq(Empty, Seq(Empty, Empty)))))), Stars []))$\\
This corresponds to the leftmost term $((0+0+0 + 0 + 1 \cdot 1 \cdot 1) \cdot r^* $ in $r_3$. Note that its leftmost location allows $mkeps$ to choose it as the first candidate that meets the requirement of being $nullable$. This location is naturally generated by the splitting clause\\ $(r_1 \cdot r_2)\backslash c (when \, r_1 \, nullable)) \, = (r_1\backslash c) \cdot r_2 \,+\, r_2\backslash c. \\$. By this clause, we put
$r_1 \backslash c \cdot r_2 $ at the front and $r_2 \backslash c$ at the back. This allows $mkeps$ to always pick up among two matches the one with a longer prefix. The value \\
$Left(Left(Seq(Right(Right(Right(Seq(Empty, Seq(Empty, Empty)))))), Stars []))$\\
tells us how about the empty string matches the final regular expression after doing all the derivatives: among the regular expressions $(0+0+0 + 0 + 1 \cdot 1 \cdot 1) \cdot r^* + (0+0+0 + 1 + 0) \cdot r*) +((0+1+0 + 0 + 0) \cdot r*+(0+0+0 + 1 + 0) \cdot r* )$ we choose the left most nullable one, which is composed of a sequence of a nested alternative and a folded star that iterates 0 times. In that nested alternative we take the rightmost alternative.
Using the value $v_3$, the character c, and the regular expression $r_2$, we can recover how $r_2$ matched the string $[c]$ : we inject $c$ back to $v_3$, and get \\ $v_2 = Left(Seq(Right(Right(Right(Seq(Empty, Seq(Empty, c)))))), Stars [])$, which tells us how $r_2$ matched $c$. After this we inject back the character $b$, and get\\ $v_1 = Seq(Right(Right(Right(Seq(Empty, Seq(b, c)))))), Stars [])$ for how $r_1= (1+0+1 \cdot b + 0 + 1 \cdot b \cdot c) \cdot r*$ matched the string $bc$ before it split into 2 pieces. Finally, after injecting character a back to $v_1$, we get the parse tree $v_0= Stars [Right(Right(Right(Seq(a, Seq(b, c)))))]$ for how r matched $abc$.
We omit the details of injection function, which is provided by Sulzmann and Lu's paper \cite{Sulzmann2014}.
Readers might have noticed that the parse tree information as actually already available when doing derivatives. For example, immediately after the operation $\backslash a$ we know that if we want to match a string that starts with a, we can either take the initial match to be
\begin{enumerate}
\item[1)] just $a$ or
\item[2)] string $ab$ or
\item[3)] string $abc$.
\end{enumerate}
In order to differentiate between these choices, we just need to remember their positions--$a$ is on the left, $ab$ is in the middle , and $abc$ is on the right. Which one of these alternatives is chosen later does not affect their relative position because our algorithm does not change this order. There is no need to traverse this information twice. This leads to a new approach of lexing-- if we store the information for parse trees in the corresponding regular expression pieces, update this information when we do derivative operation on them, and collect the information when finished with derivatives and calling $mkeps$ for deciding which branch is POSIX, we can generate the parse tree in one pass, instead of doing an n-step backward transformation.This leads to Sulzmann and Lu's novel idea of using bit-codes on derivatives.
In the next section, we shall focus on the bit-coded algorithm and the natural
process of simplification of regular expressions using bit-codes, which is needed in
order to obtain \emph{fast} versions of the Brzozowski's, and Sulzmann
and Lu's algorithms. This is where the PhD-project hopes to advance
the state-of-the-art.
\section{Simplification of Regular Expressions}
Using bit-codes to guide parsing is not a new idea.
It was applied to context free grammars and then adapted by Henglein and Nielson for efficient regular expression parsing \cite{nielson11bcre}. Sulzmann and Lu took a step further by integrating bitcodes into derivatives.
The argument for complicating the data structures from basic regular expressions to those with bitcodes
is that we can introduce simplification without making the algorithm crash or impossible to reason about.
The reason why we need simplification is due to the shortcoming of a naive algorithm using Brzozowski's definition only.
The main drawback of building successive derivatives according to
Brzozowski's definition is that they can grow very quickly in size.
This is mainly due to the fact that the derivative operation generates
often ``useless'' $\ZERO$s and $\ONE$s in derivatives. As a result,
if implemented naively both algorithms by Brzozowski and by Sulzmann
and Lu are excruciatingly slow. For example when starting with the
regular expression $(a + aa)^*$ and building 12 successive derivatives
w.r.t.~the character $a$, one obtains a derivative regular expression
with more than 8000 nodes (when viewed as a tree). Operations like
derivative and $\nullable$ need to traverse such trees and
consequently the bigger the size of the derivative the slower the
algorithm. Fortunately, one can simplify regular expressions after
each derivative step. Various simplifications of regular expressions
are possible, such as the simplifications of $\ZERO + r$,
$r + \ZERO$, $\ONE\cdot r$, $r \cdot \ONE$, and $r + r$ to just
$r$. These simplifications do not affect the answer for whether a
regular expression matches a string or not, but fortunately also do
not affect the POSIX strategy of how regular expressions match
strings---although the latter is much harder to establish. Some
initial results in this regard have been obtained in
\cite{AusafDyckhoffUrban2016}. However, what has not been achieved yet
is a very tight bound for the size. Such a tight bound is suggested by
work of Antimirov who proved that (partial) derivatives can be bound
by the number of characters contained in the initial regular
expression \cite{Antimirov95}.
Antimirov defined the "partial derivatives" of regular expressions to be this:
%TODO definition of partial derivatives
\begin{center}
\begin{tabular}{lcl}
$\textit{pder} \; c \; 0$ & $\dn$ & $\emptyset$\\
$\textit{pder} \; c \; 1$ & $\dn$ & $\emptyset$ \\
$\textit{pder} \; c \; d$ & $\dn$ & $\textit{if} \; c \,=\, d \; \{ 1 \} \; \textit{else} \; \emptyset$ \\
$\textit{pder} \; c \; r_1+r_2$ & $\dn$ & $pder \; c \; r_1 \cup pder \; c \; r_2$ \\
$\textit{pder} \; c \; r_1 \cdot r_2$ & $\dn$ & $\textit{if} \; nullable \; r_1 \; \{ r \cdot r_2 \mid r \in pder \; c \; r_1 \} \cup pder \; c \; r_2 \; \textit{else} \; \{ r \cdot r_2 \mid r \in pder \; c \; r_1 \} $ \\
$\textit{pder} \; c \; r^*$ & $\dn$ & $ \{ r' \cdot r^* \mid r' \in pder \; c \; r \} $ \\
\end{tabular}
\end{center}
it is essentially a set of regular expressions that come from the sub-structure of the original regular expression.
Antimirov has proved a nice size bound of the size of partial derivatives. Roughly speaking the size will not exceed the fourth power of the number of nodes in that regular expression. Interestingly, we observed from experiment that after the simplification step, our regular expression has the same size or is smaller than the partial derivatives. This allows us to prove a tight bound on the size of regular expression during the running time of the algorithm if we can establish the connection between our simplification rules and partial derivatives.
%We believe, and have generated test
%data, that a similar bound can be obtained for the derivatives in
%Sulzmann and Lu's algorithm. Let us give some details about this next.
Bit-codes look like this:
\[ b ::= S \mid Z \; \;\;
bs ::= [] \mid b:bs
\]
They are just a string of bits, the names "S" and "Z" here are kind of arbitrary, we can use 0 and 1 or binary symbol to substitute them. They are a compact form of parse trees.
Here is how values and bit-codes are related:
Bitcodes are essentially incomplete values.
This can be straightforwardly seen in the following transformation:
\begin{center}
\begin{tabular}{lcl}
$\textit{code}(\Empty)$ & $\dn$ & $[]$\\
$\textit{code}(\Char\,c)$ & $\dn$ & $[]$\\
$\textit{code}(\Left\,v)$ & $\dn$ & $\Z :: code(v)$\\
$\textit{code}(\Right\,v)$ & $\dn$ & $\S :: code(v)$\\
$\textit{code}(\Seq\,v_1\,v_2)$ & $\dn$ & $code(v_1) \,@\, code(v_2)$\\
$\textit{code}(\Stars\,[])$ & $\dn$ & $[\S]$\\
$\textit{code}(\Stars\,(v\!::\!vs))$ & $\dn$ & $\Z :: code(v) \;@\;
code(\Stars\,vs)$
\end{tabular}
\end{center}
where $\Z$ and $\S$ are arbitrary names for the bits in the
bitsequences.
Here code encodes a value into a bitsequence by converting Left into $\Z$, Right into $\S$, the start point of a non-empty star iteration into $\S$, and the border where a local star terminates into $\Z$. This conversion is apparently lossy, as it throws away the character information, and does not decode the boundary between the two operands of the sequence constructor. Moreover, with only the bitcode we cannot even tell whether the $\S$s and $\Z$s are for $Left/Right$ or $Stars$. The reason for choosing this compact way of storing information is that the relatively small size of bits can be easily moved around during the lexing process. In order to recover the bitcode back into values, we will need the regular expression as the extra information and decode them back into value:\\
%\begin{definition}[Bitdecoding of Values]\mbox{}
\begin{center}
\begin{tabular}{@{}l@{\hspace{1mm}}c@{\hspace{1mm}}l@{}}
$\textit{decode}'\,bs\,(\ONE)$ & $\dn$ & $(\Empty, bs)$\\
$\textit{decode}'\,bs\,(c)$ & $\dn$ & $(\Char\,c, bs)$\\
$\textit{decode}'\,(\Z\!::\!bs)\;(r_1 + r_2)$ & $\dn$ &
$\textit{let}\,(v, bs_1) = \textit{decode}'\,bs\,r_1\;\textit{in}\;
(\Left\,v, bs_1)$\\
$\textit{decode}'\,(\S\!::\!bs)\;(r_1 + r_2)$ & $\dn$ &
$\textit{let}\,(v, bs_1) = \textit{decode}'\,bs\,r_2\;\textit{in}\;
(\Right\,v, bs_1)$\\
$\textit{decode}'\,bs\;(r_1\cdot r_2)$ & $\dn$ &
$\textit{let}\,(v_1, bs_1) = \textit{decode}'\,bs\,r_1\;\textit{in}$\\
& & $\textit{let}\,(v_2, bs_2) = \textit{decode}'\,bs_1\,r_2$\\
& & \hspace{35mm}$\textit{in}\;(\Seq\,v_1\,v_2, bs_2)$\\
$\textit{decode}'\,(\Z\!::\!bs)\,(r^*)$ & $\dn$ & $(\Stars\,[], bs)$\\
$\textit{decode}'\,(\S\!::\!bs)\,(r^*)$ & $\dn$ &
$\textit{let}\,(v, bs_1) = \textit{decode}'\,bs\,r\;\textit{in}$\\
& & $\textit{let}\,(\Stars\,vs, bs_2) = \textit{decode}'\,bs_1\,r^*$\\
& & \hspace{35mm}$\textit{in}\;(\Stars\,v\!::\!vs, bs_2)$\bigskip\\
$\textit{decode}\,bs\,r$ & $\dn$ &
$\textit{let}\,(v, bs') = \textit{decode}'\,bs\,r\;\textit{in}$\\
& & $\textit{if}\;bs' = []\;\textit{then}\;\textit{Some}\,v\;
\textit{else}\;\textit{None}$
\end{tabular}
\end{center}
%\end{definition}
Sulzmann and Lu's integrated the bitcodes into annotated regular expressions by attaching them to the head of every substructure of a regular expression\emph{annotated regular expressions}~\cite{Sulzmann2014}. They are
defined by the following grammar:
\begin{center}
\begin{tabular}{lcl}
$\textit{a}$ & $::=$ & $\textit{ZERO}$\\
& $\mid$ & $\textit{ONE}\;\;bs$\\
& $\mid$ & $\textit{CHAR}\;\;bs\,c$\\
& $\mid$ & $\textit{ALTS}\;\;bs\,as$\\
& $\mid$ & $\textit{SEQ}\;\;bs\,a_1\,a_2$\\
& $\mid$ & $\textit{STAR}\;\;bs\,a$
\end{tabular}
\end{center}
\noindent
where $bs$ stands for bitsequences, and $as$ (in \textit{ALTS}) for a
list of annotated regular expressions. These bitsequences encode
information about the (POSIX) value that should be generated by the
Sulzmann and Lu algorithm.
To do lexing using annotated regular expressions, we shall first transform the
usual (un-annotated) regular expressions into annotated regular
expressions:\\
%\begin{definition}
\begin{center}
\begin{tabular}{lcl}
$(\ZERO)^\uparrow$ & $\dn$ & $\textit{ZERO}$\\
$(\ONE)^\uparrow$ & $\dn$ & $\textit{ONE}\,[]$\\
$(c)^\uparrow$ & $\dn$ & $\textit{CHAR}\,[]\,c$\\
$(r_1 + r_2)^\uparrow$ & $\dn$ &
$\textit{ALT}\;[]\,(\textit{fuse}\,[\Z]\,r_1^\uparrow)\,
(\textit{fuse}\,[\S]\,r_2^\uparrow)$\\
$(r_1\cdot r_2)^\uparrow$ & $\dn$ &
$\textit{SEQ}\;[]\,r_1^\uparrow\,r_2^\uparrow$\\
$(r^*)^\uparrow$ & $\dn$ &
$\textit{STAR}\;[]\,r^\uparrow$\\
\end{tabular}
\end{center}
%\end{definition}
Here $fuse$ is an auxiliary function that helps to attach bits to the front of an annotated regular expression. Its definition goes as follows:
\begin{center}
\begin{tabular}{lcl}
$\textit{fuse}\,bs\,(\textit{ZERO})$ & $\dn$ & $\textit{ZERO}$\\
$\textit{fuse}\,bs\,(\textit{ONE}\,bs')$ & $\dn$ &
$\textit{ONE}\,(bs\,@\,bs')$\\
$\textit{fuse}\,bs\,(\textit{CHAR}\,bs'\,c)$ & $\dn$ &
$\textit{CHAR}\,(bs\,@\,bs')\,c$\\
$\textit{fuse}\,bs\,(\textit{ALT}\,bs'\,a_1\,a_2)$ & $\dn$ &
$\textit{ALT}\,(bs\,@\,bs')\,a_1\,a_2$\\
$\textit{fuse}\,bs\,(\textit{SEQ}\,bs'\,a_1\,a_2)$ & $\dn$ &
$\textit{SEQ}\,(bs\,@\,bs')\,a_1\,a_2$\\
$\textit{fuse}\,bs\,(\textit{STAR}\,bs'\,a)$ & $\dn$ &
$\textit{STAR}\,(bs\,@\,bs')\,a$
\end{tabular}
\end{center}
After internalise we do successive derivative operations on the annotated regular expression.
This derivative operation is the same as what we previously have for the simple regular expressions, except that we take special care of the bits :\\
%\begin{definition}{bder}
\begin{center}
\begin{tabular}{@{}lcl@{}}
$(\textit{ZERO})\backslash c$ & $\dn$ & $\textit{ZERO}$\\
$(\textit{ONE}\;bs)\backslash c$ & $\dn$ & $\textit{ZERO}$\\
$(\textit{CHAR}\;bs\,d)\backslash c$ & $\dn$ &
$\textit{if}\;c=d\; \;\textit{then}\;
\textit{ONE}\;bs\;\textit{else}\;\textit{ZERO}$\\
$(\textit{ALT}\;bs\,a_1\,a_2)\backslash c$ & $\dn$ &
$\textit{ALT}\,bs\,(a_1\backslash c)\,(a_2\backslash c)$\\
$(\textit{SEQ}\;bs\,a_1\,a_2)\backslash c$ & $\dn$ &
$\textit{if}\;\textit{bnullable}\,a_1$\\
& &$\textit{then}\;\textit{ALT}\,bs\,(\textit{SEQ}\,[]\,(a_1\backslash c)\,a_2)$\\
& &$\phantom{\textit{then}\;\textit{ALT}\,bs\,}(\textit{fuse}\,(\textit{bmkeps}\,a_1)\,(a_2\backslash c))$\\
& &$\textit{else}\;\textit{SEQ}\,bs\,(a_1\backslash c)\,a_2$\\
$(\textit{STAR}\,bs\,a)\backslash c$ & $\dn$ &
$\textit{SEQ}\;bs\,(\textit{fuse}\, [\Z] (r\backslash c))\,
(\textit{STAR}\,[]\,r)$
\end{tabular}
\end{center}
%\end{definition}
For instance, when we unfold $STAR \; bs \; a$ into a sequence, we attach an additional bit Z to the front of $r \backslash c$ to indicate that there is one more star iteration.
The other example, the $SEQ$ clause is more subtle-- when $a_1$ is $bnullable$(here bnullable is exactly the same as nullable, except that it is for annotated regular expressions, therefore we omit the definition).
Assume that $bmkeps$ correctly extracts the bitcode for how $a_1$ matches the string prior to character c(more on this later), then the right branch of $ALTS$, which is $fuse \; bmkeps \; a_1 (a_2 \backslash c)$ will collapse the regular expression $a_1$(as it has already been fully matched) and store the parsing information at the head of the regular expression $a_2 \backslash c$ by fusing to it. The bitsequence $bs$, which was initially attached to the head of $SEQ$, has now been elevated to the top-level of ALT,
as this information will be needed whichever way the $SEQ$ is matched--no matter whether c belongs to $a_1$ or $ a_2$.
After carefully doing these derivatives and maintaining all the parsing information, we complete the parsing by collecting the bits using a special $mkeps$ function for annotated regular expressions--$bmkeps$:
%\begin{definition}[\textit{bmkeps}]\mbox{}
\begin{center}
\begin{tabular}{lcl}
$\textit{bmkeps}\,(\textit{ONE}\,bs)$ & $\dn$ & $bs$\\
$\textit{bmkeps}\,(\textit{ALT}\,bs\,a_1\,a_2)$ & $\dn$ &
$\textit{if}\;\textit{bnullable}\,a_1$\\
& &$\textit{then}\;bs\,@\,\textit{bmkeps}\,a_1$\\
& &$\textit{else}\;bs\,@\,\textit{bmkeps}\,a_2$\\
$\textit{bmkeps}\,(\textit{SEQ}\,bs\,a_1\,a_2)$ & $\dn$ &
$bs \,@\,\textit{bmkeps}\,a_1\,@\, \textit{bmkeps}\,a_2$\\
$\textit{bmkeps}\,(\textit{STAR}\,bs\,a)$ & $\dn$ &
$bs \,@\, [\S]$
\end{tabular}
\end{center}
%\end{definition}
This function completes the parse tree information by
travelling along the path on the regular expression that corresponds to a POSIX value snd collect all the bits, and
using S to indicate the end of star iterations. If we take the bitsproduced by $bmkeps$ and decode it,
we get the parse tree we need, the working flow looks like this:\\
\begin{center}
\begin{tabular}{lcl}
$\textit{blexer}\;r\,s$ & $\dn$ &
$\textit{let}\;a = (r^\uparrow)\backslash s\;\textit{in}$\\
& & $\;\;\textit{if}\; \textit{bnullable}(a)$\\
& & $\;\;\textit{then}\;\textit{decode}\,(\textit{bmkeps}\,a)\,r$\\
& & $\;\;\textit{else}\;\textit{None}$
\end{tabular}
\end{center}
The main point of the bitsequences and annotated regular expressions
is that we can apply rather aggressive (in terms of size)
simplification rules in order to keep derivatives small.
We have
developed such ``aggressive'' simplification rules and generated test
data that show that the expected bound can be achieved. Obviously we
could only partially cover the search space as there are infinitely
many regular expressions and strings. One modification we introduced
is to allow a list of annotated regular expressions in the
\textit{ALTS} constructor. This allows us to not just delete
unnecessary $\ZERO$s and $\ONE$s from regular expressions, but also
unnecessary ``copies'' of regular expressions (very similar to
simplifying $r + r$ to just $r$, but in a more general
setting).
Another modification is that we use simplification rules
inspired by Antimirov's work on partial derivatives. They maintain the
idea that only the first ``copy'' of a regular expression in an
alternative contributes to the calculation of a POSIX value. All
subsequent copies can be pruned from the regular expression.
A recursive definition of simplification function that looks similar to scala code is given below:\\
\begin{center}
\begin{tabular}{@{}lcl@{}}
$\textit{simp} \; a$ & $\dn$ & $\textit{a} \; \textit{if} \; a = (\textit{ONE} \; bs) \; or\; (\textit{CHAR} \, bs \; c) \; or\; (\textit{STAR}\; bs\; a_1)$\\
$\textit{simp} \; \textit{SEQ}\;bs\,a_1\,a_2$ & $\dn$ & $ (\textit{simp} \; a_1, \textit{simp} \; a_2) \; \textit{match} $ \\
&&$\textit{case} \; (0, \_) \Rightarrow 0$ \\
&&$ \textit{case} \; (\_, 0) \Rightarrow 0$ \\
&&$ \textit{case} \; (1, a_2') \Rightarrow \textit{fuse} \; bs \; a_2'$ \\
&&$ \textit{case} \; (a_1', 1) \Rightarrow \textit{fuse} \; bs \; a_1'$ \\
&&$ \textit{case} \; (a_1', a_2') \Rightarrow \textit{SEQ} \; bs \; a_1' \; a_2'$ \\
$\textit{simp} \; \textit{ALT}\;bs\,as$ & $\dn$ & $\textit{ distinct}( \textit{flatten} ( \textit{map simp as})) \; \textit{match} $ \\
&&$\textit{case} \; [] \Rightarrow 0$ \\
&&$ \textit{case} \; a :: [] \Rightarrow \textit{fuse bs a}$ \\
&&$ \textit{case} \; as' \Rightarrow \textit{ALT bs as'}$
\end{tabular}
\end{center}
The simplification does a pattern matching on the regular expression. When it detected that
the regular expression is an alternative or sequence, it will try to simplify its children regular expressions
recursively and then see if one of the children turn into 0 or 1, which might trigger further simplification
at the current level. The most involved part is the ALTS clause, where we use two auxiliary functions
flatten and distinct to open up nested ALT and reduce as many duplicates as possible.
Function distinct keeps the first occurring copy only and remove all later ones when detected duplicates.
Function flatten opens up nested ALT. Its recursive definition is given below:
\\
\[flatten ALT bs rs :: rss = (map fuse( bs,_) rs )@ flatten rss
flatten ZERO :: rss = flatten rss
flatten r::rss = r @ flatten rss if r is of any other shape
\]
Here flatten behaves like the traditional functional programming flatten function,
what it does is basically removing parentheses like changing $a+(b+c)$ into $a+b+c$.
If we apply simplification after each derivative step, we get an optimized version of the algorithm:
\\TODO definition of $blexer_simp$
This algorithm effectively keeps the regular expression size small, for example,
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.
We are currently engaged in 2 tasks related to this algorithm.
The first one is proving that our simplification rules
actually do not affect the POSIX value that should be generated by the
algorithm according to the specification of a POSIX value
and furthermore obtain a much
tighter bound on the sizes of derivatives. The result is that our
algorithm should be correct and faster on all inputs. The original
blow-up, as observed in JavaScript, Python and Java, would be excluded
from happening in our algorithm.For
this proof we use the theorem prover Isabelle. Once completed, this
result will advance the state-of-the-art: Sulzmann and Lu wrote in
their paper \cite{Sulzmann2014} about the bitcoded ``incremental
parsing method'' (that is the matching algorithm outlined in this
section):
\begin{quote}\it
``Correctness Claim: We further claim that the incremental parsing
method in Figure~5 in combination with the simplification steps in
Figure 6 yields POSIX parse trees. We have tested this claim
extensively by using the method in Figure~3 as a reference but yet
have to work out all proof details.''
\end{quote}
\noindent
We would settle the correctness claim.
It is relatively straightforward to establish that after 1 simplification step, the part of derivative that corresponds to a POSIX value remains intact and can still be collected, in other words,
bmkeps r = bmkeps simp r
as this basically comes down to proving actions like removing the additional $r$ in $r+r$ does not delete imporatnt POSIX information in a regular expression.
The hardcore of this problem is to prove that
bmkeps bders r = bmkeps bders simp r
That is, if we do derivative on regular expression r and the simplificed version fo r , they can still provie the same POSIZ calue if there is one . This is not as strightforward as the previous proposition, as the two regular expression r and simp r might become very different regular epxressions after repeated application ofd simp and derivative.
The crucial point is to find the "gene" of a regular expression and how it is kept intact during simplification.
To aid this, we are utilizing the helping function retrieve described by Sulzmann and Lu:
\\definition of retrieve\\
This function assembled the bitcode that corresponds to a parse tree for how the current derivative mathces the suffix of the string(the characters that have not yet appeared, but is stored in the value).
Sulzmann and Lu used this to connect the bit-coded algorithm to the older algorithm by the following equation:\\
inj r c v = decode retrieve (bder c (internalise r)) v
Fahad and Christian also used this fact to prove the correctness of bit-coded algorithm without simplificaiton.
Our purpose of using this, however, is try to establish \\
$ retrieve \; r \; v \;=\; retrieve \; simp(r) \; v'.$\\
Although the r and v are different now, we can still extract the bitsequence that gies the same parsing information.
After establishing this, we might be able to finally bridge the gap of proving
$retrieve \; r \; \backslash \;s \; v = \;retrieve \; simp(r) \; \backslash \; s \; v'$
and subsequently
$retrieve \; r \; \backslash \; s \; v\; = \; retrieve \; r \; \backslash{with simplification} \; s \; v'$.
This proves that our simplified version of regular expression still contains all the bitcodes neeeded.
The second task is to speed up the more aggressive simplification. Currently it is slower than a naive simplifiction(the naive version as implemented in ADU of course can explode in some cases).
So it needs to be explored how to make it faster. Our possibility would be to explore again the connection to DFAs. This is very much work in progress.
\section{Conclusion}
In this PhD-project we are interested in fast algorithms for regular
expression matching. While this seems to be a ``settled'' area, in
fact interesting research questions are popping up as soon as one steps
outside the classic automata theory (for example in terms of what kind
of regular expressions are supported). The reason why it is
interesting for us to look at the derivative approach introduced by
Brzozowski for regular expression matching, and then much further
developed by Sulzmann and Lu, is that derivatives can elegantly deal
with some of the regular expressions that are of interest in ``real
life''. This includes the not-regular expression, written $\neg\,r$
(that is all strings that are not recognised by $r$), but also bounded
regular expressions such as $r^{\{n\}}$ and $r^{\{n..m\}}$). There is
also hope that the derivatives can provide another angle for how to
deal more efficiently with back-references, which are one of the
reasons why regular expression engines in JavaScript, Python and Java
choose to not implement the classic automata approach of transforming
regular expressions into NFAs and then DFAs---because we simply do not
know how such back-references can be represented by DFAs.
\bibliographystyle{plain}
\bibliography{root}
\end{document}