% Chapter 1

\chapter{Introduction} % Main chapter title

\label{Chapter1} % For referencing the chapter elsewhere, use \ref{Chapter1} 

%----------------------------------------------------------------------------------------

% Define some commands to keep the formatting separated from the content 

\newcommand{\keyword}[1]{\textbf{#1}}

\newcommand{\tabhead}[1]{\textbf{#1}}

\newcommand{\code}[1]{\texttt{#1}}

\newcommand{\file}[1]{\texttt{\bfseries#1}}

\newcommand{\option}[1]{\texttt{\itshape#1}}

\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\DFA{\textit{DFA}}

\def\bmkeps{\textit{bmkeps}}

\def\retrieve{\textit{retrieve}}

\def\blexer{\textit{blexer}}

\def\flex{\textit{flex}}

\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}}

\def\rup{r^\uparrow}

\def\simp{\mathit{simp}}

\def\simpALTs{\mathit{simp}\_\mathit{ALTs}}

\def\map{\mathit{map}}

\def\distinct{\mathit{distinct}}

\def\blexersimp{\mathit{blexer}\_\mathit{simp}}

%----------------------------------------------------------------------------------------

If you go to a popular programming language's

regex engine,

you can supply it with regex and strings of your own,

and get matching/lexing  information such as how a 

sub-part of the regex matches a sub-part of the string.

These lexing libraries are on average quite fast.

For example, the regex engines some network intrusion detection

systems use are able to process

 megabytes or even gigabytes of network traffic per second.

Why do we need to have our version, if the algorithms work well on 

average?

Take $(a^*)^*\,b$ and ask whether

strings of the form $aa..a$ match this regular

expression. Obviously this is not the case---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}  

This is clearly exponential behaviour, and 

is triggered by some relatively simple regex patterns.

The opens up the possibility of

 a ReDoS (regular expression denial-of-service ) attack.

Theoretical results say that regular expression matching

should be linear with respect to the input. You could construct

an NFA via Thompson construction, and simulate  running it.

This would be linear.

Or you could determinize the NFA into a DFA, and minimize that

DFA. Once you have the DFA, the running time is also linear, requiring just 

one scanning pass of the input.

But modern  regex libraries in popular language engines

 often want to support richer constructs

than  the most basic regular expressions such as bounded repetitions

and back references. 

%put in illustrations

%a{1}{3}

These make a DFA construction impossible because

of an exponential states explosion.

 They also want to support lexing rather than just matching

 for tasks that involves text processing.

 Existing regex libraries either pose restrictions on the user input, or does 

 not give linear running time guarantee.

 %TODO: give examples such as RE2 GOLANG 1000 restriction, rust no repetitions 

 For example, the Rust regex engine claims to be linear, 

 but does not support lookarounds and back-references.

 The GoLang regex library does not support over 1000 repetitions.  

 Java and Python both support back-references, but shows

catastrophic backtracking behaviours on inputs without back-references(

when the language is still regular).

 %TODO: test performance of Rust on (((((a*a*)b*)b){20})*)c  baabaabababaabaaaaaaaaababaaaababababaaaabaaabaaaaaabaabaabababaababaaaaaaaaababaaaababababaaaaaaaaaaaaac

 %TODO: verify the fact Rust does not allow 1000+ reps

 %TODO: Java 17 updated graphs? Is it ok to still use Java 8 graphs?

 Another thing about the these libraries is that there

 is no correctness guarantee.

 In some cases they either fails to generate a lexing result when there is a match,

 or gives the wrong way of matching.

This superlinear blowup in matching algorithms sometimes causes

considerable grief 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{\url{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---causing web servers to grind 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. In this example, the time needed to process

the string was $O(n^2)$ with respect to the string length. This

quadratic overhead was enough for the homepage of Stack Exchange to

respond so slowly that the load balancer assumed there must be some

attack and therefore stopped the servers from responding to any

requests. This made the whole site become unavailable. Another very

recent example is a global outage of all Cloudflare servers on 2 July

2019. A poorly written regular expression exhibited exponential

behaviour and exhausted CPUs that serve HTTP traffic. Although the

outage had several causes, at the heart was a regular expression that

was used to monitor network

%traffic.\footnote{\url{https://blog.cloudflare.com/details-of-the-cloudflare-outage-on-july-2-2019/}}

 Is it possible to have a regex lexing algorithm with proven correctness and 

 time complexity, which allows easy extensions to

  constructs like 

 bounded repetitions, negation,  lookarounds, and even back-references? 

 We propose Brzozowski's derivatives as a solution to this problem.

 In the last fifteen or so years, Brzozowski's derivatives of regular

expressions have sparked quite a bit of interest in the functional

programming and theorem prover communities.  

The beauty of

Brzozowski's derivatives \parencite{Brzozowski1964} is that they are neatly

expressible in any functional language, and easily definable and

reasoned about in theorem provers---the definitions just consist of

inductive datatypes and simple recursive functions. 

Suppose we have an alphabet $\Sigma$, the strings  whose characters

are from $\Sigma$

can be expressed as $\Sigma^*$.

We use patterns to define a set of strings concisely. Regular expressions

are one of such patterns systems:

The basic regular expressions  are defined inductively

 by the following grammar:

\[			r ::=   \ZERO \mid  \ONE

			 \mid  c  

			 \mid  r_1 \cdot r_2

			 \mid  r_1 + r_2   

			 \mid r^*         

\]

The language or set of strings defined by regular expressions are defined as

%TODO: FILL in the other defs

\begin{center}

\begin{tabular}{lcl}

$L \; r_1 + r_2$ & $\dn$ & $ L \; r_1 \cup L \; r_2$\\

$L \; r_1 \cdot r_2$ & $\dn$ & $ L \; r_1 \cap L \; r_2$\\

\end{tabular}

\end{center}

Which are also called the "language interpretation".

The Brzozowski derivative w.r.t character $c$ is an operation on the regex,

where the operation transforms the regex to a new one containing

strings without the head character $c$.

Formally, we define first such a transformation on any string set, which

we call semantic derivative:

\begin{center}

$\Der \; c\; \textit{StringSet} = \{s \mid c :: s \in StringSet\}$

\end{center}

Mathematically, it can be expressed as the 

If the $\textit{StringSet}$ happen to have some structure, for example,

if it is regular, then we have that it

The the derivative of regular expression, denoted as

$r \backslash c$, is a function that takes parameters

$r$ and $c$, and returns another regular expression $r'$,

which is computed by the following recursive function:

\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}

\noindent

\noindent

The $\nullable$ function tests whether the empty string $""$ 

is in the language of $r$:

\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}

\noindent

The empty set does not contain any string and

therefore not the empty string, the empty string 

regular expression contains the empty string

by definition, the character regular expression

is the singleton that contains character only,

and therefore does not contain the empty string,

the alternative regular expression(or "or" expression)

might have one of its children regular expressions

being nullable and any one of its children being nullable

would suffice. The sequence regular expression

would require both children to have the empty string

to compose an empty string and the Kleene star

operation naturally introduced the empty string.

We can give the meaning of regular expressions derivatives

by language interpretation: