\def\fuse{\textit{fuse}}

\def\flatten{\textit{flatten}}

\def\map{\textit{map}}

\section{Recapitulation of Concepts From the Last Report}

\subsection{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 ingenious contribution by Brzozowski is the notion of

\emph{derivatives} of regular expressions.  

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

%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

Now 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 looks graphically 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 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 + bc$ 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 helps 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 $\text{inj}$-mechanism, we use

\emph{bitcodes}. Bits and bitcodes (lists of bits) are just:

\begin{center}

		$b ::=   S \mid  Z \qquad

bs ::= [] \mid b:bs    

$

\end{center}

\noindent

The $S$ and $Z$ are arbitrary names for the bits in order to avoid 

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

bit-lists) can be used to encode values (or incomplete values) in a

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$ & $\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$ & $[\Z]$\\

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

                                                 code(\Stars\,vs)$

\end{tabular}    

\end{center} 

\noindent

Here $\textit{code}$ encodes a value into a bitcodes 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 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 $\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 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}'\,(\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 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}

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

%(in \textit{ALTS})

\noindent

where $bs$ stands for bitcodes, $a$  for $\bold{a}$nnotated regular

expressions and $as$ for a list of annotated regular expressions.

The alternative constructor($\textit{ALTS}$) has been generalized to 

accept a list of annotated regular expressions rather than just 2.

We will show that these bitcodes 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. This operation is called \emph{internalisation} and

defined as follows:

%\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{ALTS}\;[]\,List((\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}

\noindent

We use up arrows here to indicate that the basic un-annotated regular

expressions are ``lifted up'' into something slightly more complex. In the

fourth clause, $\textit{fuse}$ is an auxiliary function that helps to

attach bits to the front of an annotated regular expression. Its

definition is 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{ALTS}\,bs'\,as)$ & $\dn$ &

     $\textit{ALTS}\,(bs\,@\,bs')\,as$\\

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

\noindent

After internalising the regular expression, we perform successive

derivative operations on the annotated regular expressions. This

derivative operation is the same as what we had previously for the

basic regular expressions, except that we beed to take care of

the bitcodes:

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