\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

  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}  

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

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

beginning nor at the end. As a result, the regular expression matching

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

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

\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

\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

\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

operation, written $|v|$, which we can use to extract the underlying

(\textit{Char y})|$ is the string $xy$. We omit the straightforward

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 is 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

the characters $c_0$, $c_1$,\ldots  until we exhaust the string and

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

$\textit{mkeps}$, which builds the parse tree for how the empty string

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 = c_i \ldots c_n$ ) from the previous parse tree $v_{i+1}$. After injecting back $n$ characters, we

get the parse tree for how $r_0$ matches $s$, exactly as we wanted.

 A correctness proof using induction can be routinely established.

\[ 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 $\textit{front}$ and $r_2 \backslash c$ at the $\textit{back}$. This allows $mkeps$ to always pick up among two matches the one with a longer prefix. The value \\