\documentclass[a4paper,UKenglish]{lipics}

\usepackage{graphic}

\usepackage{data}

\usepackage{tikz-cd}

\usepackage{tikz}

\usetikzlibrary{graphs}

\usetikzlibrary{graphdrawing}

\usegdlibrary{trees}

%\usepackage{algorithm}

\usepackage{amsmath}

\usepackage{xcolor}

\usepackage[noend]{algpseudocode}

\usepackage{enumitem}

\usepackage{nccmath}

\usepackage{soul}

\definecolor{darkblue}{rgb}{0,0,0.6}

\hypersetup{colorlinks=true,allcolors=darkblue}

\newcommand{\comment}[1]%

{{\color{red}$\Rightarrow$}\marginpar{\raggedright\small{\bf\color{red}#1}}}

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

\def\bders{\textit{bders}}

\def\lexer{\mathit{lexer}}

\def\blexer{\textit{blexer}}

\def\fuse{\textit{fuse}}

\def\flatten{\textit{flatten}}

\def\map{\textit{map}}

\def\blexers{\mathit{blexer\_simp}}

\def\simp{\mathit{simp}}

\def\mkeps{\mathit{mkeps}}

\def\bmkeps{\textit{bmkeps}}

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

\def\rup{r^\uparrow}

\def\retrieve{\textit{retrieve}}

\def\AALTS{\textit{AALTS}}

\def\AONE{\textit{AONE}}

%\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 does also

  answers with \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. Being fast depends on a complete set of 

  simplification rules, some of which 

  have been put forward by Sulzmann and Lu. We have extended their

  rules in order to obtain a tight bound on the size of regular expressions.

  We have tested these extended rules, but have not 

  formally established their correctness. We have also not yet looked 

  at extended regular expressions, such as bounded repetitions,

  negation and back-references.

\end{abstract}

\section{Introduction}

%Regular expressions' derivatives, which have received 

%renewed interest in the new millenium, is a beautiful....

While we believe derivatives of regular expressions, written

$r\backslash s$, are a beautiful concept (in terms of ease of

implementing them in functional programming languages and in terms of

reasoning about them formally), they have one major drawback: every

derivative step can make regular expressions grow drastically in

size. This in turn has negative effect on the runtime of the

corresponding lexing algorithms. Consider for example the regular

expression $(a+aa)^*$ and the short string $aaaaaaaaaaaa$. The

corresponding derivative contains already 8668 nodes where we assume

the derivative is given as a tree. The reason for the poor runtime of

the derivative-based lexing algorithms is that they need to traverse

such trees over and over again. The solution is to find a complete set

of simplification rules that keep the sizes of derivatives uniformly

small.

This has been partially addressed by the function $\blexer_{simp}$,

which after  the simplification the $(a+aa)^*$ example's 8000 nodes will be

reduced to just 6 and stays constant in each derivative step.

The part that still needs more work is the correctness proof of this 

function, namely,

\begin{equation}\label{mainthm}

\blexers \; r \; s = \blexer \;r\;s

\end{equation}

\noindent

and this is what this report is mainly about. A condensed 

version of the last report will be provided in the next section

to help the reader understand the report, and the attempts 

on the problem will follow.

\section{Recapitulation of Concepts From the Last Report}

\subsection*{Regular Expressions and Derivatives}

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 ingenious contribution of Brzozowski is the notion of \emph{derivatives} of

regular expressions, written~$\_ \backslash \_$. It uses the auxiliary notion of

$\nullable$ defined below.

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

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

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

We can generalise the derivative operation shown above for single characters

to strings as follows:

\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 Brzozowski's  regular-expression matching algorithm as:

\[

match\;s\;r \;\dn\; nullable(r\backslash s)

\]

\noindent

this algorithm presented graphically is 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

an $s = c_0...c_{n-1}$ and an $r_0$, it generates YES if and only if $s \in L(r_0)$).

\subsection*{Values and the Lexing Algorithm by Sulzmann and Lu}

One limitation 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} or

sometimes also \emph{lexical value}.  These 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 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 in case the regular expression matches  the string. 

Pictorially, the Sulzmann and Lu algorithm is as follows:

\begin{ceqn}

\begin{equation}\label{graph:2}

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

\end{ceqn}

\noindent

For convenience, we shall employ the following notations: the regular

expression we start with is $r_0$, and the given string $s$ is composed

of characters $c_0 c_1 \ldots c_{n-1}$. In  the first phase from the

left to right, we build the derivatives $r_1$, $r_2$, \ldots  according

to the characters $c_0$, $c_1$  until we exhaust the string and obtain

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

values incrementally by \emph{injecting} back the characters into the

earlier values $v_n, \ldots, v_0$. This is the second phase of the

algorithm from the right to left. For the first value $v_n$, we call the

function $\textit{mkeps}$, which builds the lexical value

for how the empty string has been matched by the (nullable) 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}

\noindent 

After the $\mkeps$-call, we inject back the characters one by one in order to build

the lexical value $v_i$ for how the regex $r_i$ matches the string $s_i$

($s_i = c_i \ldots c_{n-1}$ ) from the previous lexical value $v_{i+1}$.

After injecting back $n$ characters, we get the lexical value for how $r_0$

matches $s$. For this Sulzmann and Lu defined a function that reverses

the ``chopping off'' of characters during the derivative phase. The

corresponding function is called \emph{injection}, written

$\textit{inj}$; it takes three arguments: the first one is a regular

expression ${r_{i-1}}$, before the character is chopped off, the second

is a character ${c_{i-1}}$, the character we want to inject and the

third argument is the value ${v_i}$, into which one wants to inject the

character (it corresponds to the regular expression after the character

has been chopped off). The result of this function is a new value. The

definition of $\textit{inj}$ is as follows: 

\begin{center}

\begin{tabular}{l@{\hspace{1mm}}c@{\hspace{1mm}}l}

  $\textit{inj}\,(c)\,c\,Empty$            & $\dn$ & $Char\,c$\\

  $\textit{inj}\,(r_1 + r_2)\,c\,\Left(v)$ & $\dn$ & $\Left(\textit{inj}\,r_1\,c\,v)$\\

  $\textit{inj}\,(r_1 + r_2)\,c\,Right(v)$ & $\dn$ & $Right(\textit{inj}\,r_2\,c\,v)$\\

  $\textit{inj}\,(r_1 \cdot r_2)\,c\,Seq(v_1,v_2)$ & $\dn$  & $Seq(\textit{inj}\,r_1\,c\,v_1,v_2)$\\

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

  $\textit{inj}\,(r_1 \cdot r_2)\,c\,Right(v)$ & $\dn$  & $Seq(\textit{mkeps}(r_1),\textit{inj}\,r_2\,c\,v)$\\

  $\textit{inj}\,(r^*)\,c\,Seq(v,Stars\,vs)$         & $\dn$  & $Stars((\textit{inj}\,r\,c\,v)\,::\,vs)$\\

\end{tabular}

\end{center}

\noindent This definition is by recursion on the ``shape'' of regular

expressions and values. 

\subsection*{Simplification of Regular Expressions}

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

$\textit{der}$ 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 simplification 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}. 

If we want the size of derivatives in Sulzmann and Lu's algorithm to

stay below this bound, we would need more aggressive simplifications.

Essentially we need to delete useless $\ZERO$s and $\ONE$s, as well as

deleting duplicates whenever possible. For example, the parentheses in

$(a+b) \cdot c + b\cdot c$ can be opened up to get $a\cdot c + b \cdot c + b

\cdot c$, and then simplified to just $a \cdot c + b \cdot c$. Another

example is simplifying $(a^*+a) + (a^*+ \ONE) + (a +\ONE)$ to just

$a^*+a+\ONE$. Adding these more aggressive simplification rules help us

to achieve the same size bound as that of the partial derivatives. 

In order to implement the idea of ``spilling out alternatives'' and to

make them compatible with the $\textit{inj}$-mechanism, we use

\emph{bitcodes}. They were first introduced by Sulzmann and Lu.

Here bits and bitcodes (lists of bits) are defined as:

\begin{center}

		$b ::=   1 \mid  0 \qquad

$

\end{center}

\noindent

The $1$ and $0$ are not in bold in order to avoid 

confusion with the regular expressions $\ZERO$ and $\ONE$. Bitcodes (or

compact form. This can be straightforwardly seen in the following

coding function from values to bitcodes: 

\begin{center}

\begin{tabular}{lcl}

  $\textit{code}(\Empty)$ & $\dn$ & $[]$\\

  $\textit{code}(\Char\,c)$ & $\dn$ & $[]$\\

  $\textit{code}(\Left\,v)$ & $\dn$ & $0 :: code(v)$\\

  $\textit{code}(\Right\,v)$ & $\dn$ & $1 :: code(v)$\\

  $\textit{code}(\Seq\,v_1\,v_2)$ & $\dn$ & $code(v_1) \,@\, code(v_2)$\\

  $\textit{code}(\Stars\,[])$ & $\dn$ & $[0]$\\

  $\textit{code}(\Stars\,(v\!::\!vs))$ & $\dn$ & $1 :: code(v) \;@\;

                                                 code(\Stars\,vs)$

\end{tabular}    

\end{center} 

\noindent

Here $\textit{code}$ encodes a value into a bitcodes by converting

$\Left$ into $0$, $\Right$ into $1$, and marks the start of a non-empty

star iteration by $1$. The border where a local star terminates

is marked by $0$. This coding is lossy, as it throws away the information about

characters, and also does not encode the ``boundary'' between two

sequence values. Moreover, with only the bitcode we cannot even tell

whether the $1$s and $0$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 manipulated and ``moved

around'' in a regular expression. In order to recover values, we will 

need the corresponding regular expression as an extra information. This

means the decoding function is defined as:

%\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}'\,(0\!::\!bs)\;(r_1 + r_2)$ & $\dn$ &

     $\textit{let}\,(v, bs_1) = \textit{decode}'\,bs\,r_1\;\textit{in}\;

       (\Left\,v, bs_1)$\\

  $\textit{decode}'\,(1\!::\!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}'\,(0\!::\!bs)\,(r^*)$ & $\dn$ & $(\Stars\,[], bs)$\\

  $\textit{decode}'\,(1\!::\!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 regular expressions to

create annotated regular expressions \cite{Sulzmann2014}.

\emph{Annotated regular expressions} are defined by the following

grammar:%\comment{ALTS should have  an $as$ in  the definitions, not  just $a_1$ and $a_2$}

\begin{center}