% Chapter Template

% Main chapter title

\chapter{Bit-coded Algorithm of Sulzmann and Lu}

\label{Bitcoded1} % Change X to a consecutive number; for referencing this chapter elsewhere, use \ref{ChapterX}

%Then we illustrate how the algorithm without bitcodes falls short for such aggressive 

%simplifications and therefore introduce our version of the bitcoded algorithm and 

%its correctness proof in 

%Chapter 3\ref{Chapter3}. 

In this chapter, we are going to describe the bit-coded algorithm

introduced by Sulzmann and Lu \parencite{Sulzmann2014} to address the growth problem of 

regular expressions. 

\section{Bit-coded Algorithm}

The lexer algorithm in Chapter \ref{Inj}, as shown in \ref{InjFigure},

stores information of previous lexing steps

on a stack, in the form of regular expressions

and characters: $r_0$, $c_0$, $r_1$, $c_1$, etc.

\begin{ceqn}

\begin{equation}%\label{graph:injLexer}

	\begin{tikzcd}[ampersand replacement=\&, execute at end picture={

			\begin{scope}[on background layer]

				\node[rectangle, fill={red!30},

					pattern=north east lines, pattern color=red,

					fit={(-3,-1) (-3, 1) (1, -1) 

						(1, 1)}

				     ] 

				     {}; ,

				\node[rectangle, fill={blue!20},

					pattern=north east lines, pattern color=blue,

					fit= {(1, -1) (1, 1) (3, -1) (3, 1)}

					]

					{};

				\end{scope}}

					]

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

The red part represents what we already know during the first

derivative phase,

and the blue part represents the unknown part of input.

The red area expands as we move towards $r_n$, 

indicating an increasing stack size during lexing.

Despite having some partial lexing information during

the forward derivative phase, we choose to store them

temporarily, only to convert the information to lexical

values at a later stage. In essence we are repeating work we

have already done.

This is both inefficient and prone to stack overflow.

A natural question arises as to whether we can store lexing

information on the fly, while still using regular expression 

derivatives.

If we remove the details of the individual 

lexing steps, and use red and blue areas as before

to indicate consumed (seen) input and constructed

partial value (before recovering the rest of the stack),

one could see that the seen part's lexical information

is stored in the form of a regular expression.

Consider the regular expression $(aa)^* \cdot bc$ matching the string $aabc$

and assume we have just read the two characters $aa$:

\begin{center}

\begin{tikzpicture}[every node/.append style={draw, rounded corners, inner sep=10pt}]

    \node [rectangle split, rectangle split horizontal, rectangle split parts=2, rectangle split part fill={red!30,blue!20},]

	    {Partial lexing info: $\ONE \cdot a \cdot (aa)^* \cdot bc$ etc.

         \nodepart{two} $\Seq(\ldots, \Seq(\Char(b), \Char(c)))$};

\end{tikzpicture}

\end{center}

\noindent

In the injection-based lexing algorithm, we ``neglect" the red area

by putting all the characters we have consumed and

intermediate regular expressions on the stack when 

we go from left to right in the derivative phase.

The red area grows till the string is exhausted.

During the injection phase, the value in the blue area

is built up incrementally, while the red area shrinks.

Before we have recovered all characters and intermediate

derivative regular expressions from the stack,

what values these characters and regular expressions correspond 

to are unknown: 

\begin{center}

\begin{tikzpicture}[every node/.append style={draw, rounded corners, inner sep=10pt}]

    \node [rectangle split, rectangle split horizontal, rectangle split parts=2, rectangle split part fill={white!30,blue!20},]

	    {$(\ONE \cdot \ONE) \cdot (aa)^* \cdot bc $ correspond to:$???$

         \nodepart{two}  $b c$ corresponds to  $\Seq(\ldots, \Seq(\Char(b), \Char(c)))$};

%\caption{term 1 \ref{term:1}'s matching configuration}

\end{tikzpicture}

\end{center}

\noindent

However, they should be calculable,

as characters and regular expression shapes

after taking derivative w.r.t those characters

have already been known, therefore in our example,

we know that the value starts with two $a$s,

and makes up to an iteration in a Kleene star:

(We have put the injection-based lexing's partial 

result in the right part of the split rectangle

to contrast it with the partial valued produced

in a forward manner)

\begin{center}

\begin{tikzpicture}[every node/.append style={draw, rounded corners, inner sep=10pt}]

    \node [rectangle split, rectangle split horizontal, rectangle split parts=2, rectangle split part fill={red!30,blue!20},]

	    {$\stackrel{Bitcoded}{\longrightarrow} \Seq(\Stars[\Char(a), \Char(a)], ???)$

	\nodepart{two} $\Seq(\ldots, \Seq(\Char(b), \Char(c)))$  $\stackrel{Inj}{\longleftarrow}$};

%\caption{term 1 \ref{term:1}'s matching configuration}

\end{tikzpicture}

\end{center}

\noindent

If we do this kind of "attachment"

and each time augment the attached partially

constructed value when taking off a 

character:

\begin{center}

\begin{tikzpicture}[every node/.append style={draw, rounded corners, inner sep=10pt}]

	\node [rectangle split, rectangle split horizontal, rectangle split parts=2, rectangle split part fill={red!30,blue!20},] (spPoint)

        {$\Seq(\Stars[\Char(a), \Char(a)], \ldots)$

         \nodepart{two} Remaining: $b c$};

\end{tikzpicture}\\

$\downarrow$\\

\begin{tikzpicture}[every node/.append style={draw, rounded corners, inner sep=10pt}]

    \node [rectangle split, rectangle split horizontal, rectangle split parts=2, rectangle split part fill={red!30,blue!20},]

        {$\Seq(\Stars[\Char(a), \Char(a)], \Seq(\Char(b), \ldots))$

         \nodepart{two} Remaining: $c$};

\end{tikzpicture}\\

$\downarrow$\\

\begin{tikzpicture}[every node/.append style={draw, rounded corners, inner sep=10pt}]

    \node [rectangle split, rectangle split horizontal, rectangle split parts=2, rectangle split part fill={red!30,blue!20},]

        {$\Seq(\Stars[\Char(a), \Char(a)], \Seq(\Char(b), \Char(c)))$

         \nodepart{two} EOF};

\end{tikzpicture}

\end{center}

\noindent

In the end we could recover the value without a backward phase.

But (partial) values are a bit clumsy to stick together with a regular expression, so 

we instead use bit-codes to encode them.

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

\begin{center}

		$b ::=   S \mid  Z \qquad

bs ::= [] \mid b::bs    

$

\end{center}

\noindent

Using $S$ and $Z$ rather than $1$ and $0$ is to avoid

confusion with the regular expressions $\ZERO$ and $\ONE$.

Bitcodes (or

bit-lists) can be used to encode values (or potentially 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 bit-code by converting

$\Left$ into $Z$, $\Right$ into $S$, and marks the start of any non-empty

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

is marked by $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. 

Because of the lossiness, the process of decoding a bitlist requires additionally 

a regular expression. The function $\decode$ 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}

\noindent

The function $\decode'$ returns a pair consisting of 

a partially decoded value and some leftover bit list that cannot

be decide yet.

The function $\decode'$ succeeds if the left-over 

bit-sequence is empty.

$\decode$ is terminating as $\decode'$ is terminating.

$\decode'$ is terminating 

because at least one of $\decode'$'s parameters will go down in terms

of size.

Assuming we have a value $v$ and regular expression $r$

with $\vdash v:r$,

then we have the property that $\decode$ and $\code$ are

reverse operations of one another:

\begin{lemma}

\[If \vdash v : r \; then \;\decode \; (\code \; v) \; r = \textit{Some}(v) \]

\end{lemma}

\begin{proof}

By proving a more general version of the lemma, on $\decode'$:

\[\vdash v : r \implies \decode' \; ((\code \; v) @ ds) \; r = (v, ds) \]

Then setting $ds$ to be $[]$ and unfolding $\decode$ definition,

we obtain the property.

\end{proof}

With the $\code$ and $\decode$ functions in hand, we know how to 

switch between bit-codes and values. 

The next step is to integrate this information into regular expression.

Attaching bits to the front of regular expressions is the solution Sulzamann and Lu

gave for storing partial values in regular expressions. 

Annotated regular expressions are therefore defined as the Isabelle

datatype:

\begin{center}

\begin{tabular}{lcl}

  $\textit{a}$ & $::=$  & $\ZERO$\\

                  & $\mid$ & $_{bs}\ONE$\\

                  & $\mid$ & $_{bs}{\bf c}$\\

                  & $\mid$ & $_{bs}\sum\,as$\\

                  & $\mid$ & $_{bs}a_1\cdot a_2$\\

                  & $\mid$ & $_{bs}a^*$

\end{tabular}    

\end{center}  

%(in \textit{ALTS})

\noindent

where $bs$ stands for bit-codes, $a$  for $\mathbf{a}$nnotated regular

expressions and $as$ for lists of annotated regular expressions.

The alternative constructor, written, $\sum$, has been generalised to 

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

Why is it generalised? This is because when we open up nested 

alternatives, there could be more than two elements at the same level

after de-duplication, which can no longer be stored in a binary

constructor.

The first operation we define related to bit-coded regular expressions

is how we move bits to the inside of regular expressions.

Called $\fuse$, this operation is attaches bit-codes 

to the front of an annotated regular expression:

\begin{center}

\begin{tabular}{lcl}

  $\textit{fuse}\;bs \; \ZERO$ & $\dn$ & $\ZERO$\\

  $\textit{fuse}\;bs\; _{bs'}\ONE$ & $\dn$ &

     $_{bs @ bs'}\ONE$\\

  $\textit{fuse}\;bs\;_{bs'}{\bf c}$ & $\dn$ &

     $_{bs@bs'}{\bf c}$\\

  $\textit{fuse}\;bs\,_{bs'}\sum\textit{as}$ & $\dn$ &

     $_{bs@bs'}\sum\textit{as}$\\

  $\textit{fuse}\;bs\; _{bs'}a_1\cdot a_2$ & $\dn$ &

     $_{bs@bs'}a_1 \cdot a_2$\\

  $\textit{fuse}\;bs\,_{bs'}a^*$ & $\dn$ &

     $_{bs @ bs'}a^*$

\end{tabular}    

\end{center} 

\noindent

With \emph{fuse} we are able to define the $\internalise$ function

that translates a ``standard'' regular expression into an

annotated regular expression.

This function will be applied before we start

with the derivative phase of the algorithm.

\begin{center}

\begin{tabular}{lcl}

  $(\ZERO)^\uparrow$ & $\dn$ & $\ZERO$\\

  $(\ONE)^\uparrow$ & $\dn$ & $_{[]}\ONE$\\

  $(c)^\uparrow$ & $\dn$ & $_{[]}{\bf c}$\\

  $(r_1 + r_2)^\uparrow$ & $\dn$ &

  $_{[]}\sum[\textit{fuse}\,[Z]\,r_1^\uparrow,\,

  \textit{fuse}\,[S]\,r_2^\uparrow]$\\

  $(r_1\cdot r_2)^\uparrow$ & $\dn$ &

         $_{[]}r_1^\uparrow \cdot r_2^\uparrow$\\

  $(r^*)^\uparrow$ & $\dn$ &

         $_{[]}(r^\uparrow)^*$\\

\end{tabular}    

\end{center}    

%\end{definition}

\noindent

We use an up arrow with postfix notation

to denote this operation.

for convenience. The $\textit{internalise} \; r$

notation is more cumbersome.

The opposite of $\textit{internalise}$ is

$\erase$, where all the bit-codes are removed,

and the alternative operator $\sum$ for annotated

regular expressions is transformed to the binary alternatives

for plain regular expressions.

\begin{center}

	\begin{tabular}{lcl}

		$\ZERO_\downarrow$ & $\dn$ & $\ZERO$\\

		$( _{bs}\ONE )_\downarrow$ & $\dn$ & $\ONE$\\

		$( _{bs}\mathbf{c} )_\downarrow$ & $\dn$ & $\mathbf{c}$\\

		$( _{bs} a_1 \cdot a_2 )_\downarrow$ & $\dn$ & 

		$ (a_1) _\downarrow \cdot  (a_2) _\downarrow$\\

		$( _{bs} [])_\downarrow $ & $\dn$ & $\ZERO $\\

		$( _{bs} [a]  )_\downarrow$ & $\dn$ & $a_\downarrow$\\

		$_{bs} \sum [a_1, \; a_2]$ & $\dn$ & $ (a_1) _\downarrow + ( a_2 ) _\downarrow $\\

		$(_{bs} \sum (a :: as))_\downarrow$ & $\dn$ & $ a_\downarrow + \; (_{[]} \sum as)_\downarrow$\\

		$( _{bs} a^* )_\downarrow$ & $\dn$ & $(a_\downarrow)^*$

	\end{tabular}

\end{center}

\noindent

We also abbreviate the $\erase\; a$ operation

as $a_\downarrow$, for conciseness.

For bit-coded regular expressions, as a different datatype, 

testing whether they contain empty string in their lauguage requires

a dedicated function $\bnullable$

which simply calls $\erase$ first before testing whether it is $\nullable$.

\begin{definition}

		$\bnullable \; a \dn  \nullable \; (a_\downarrow)$

\end{definition}

The function for collecting the

bitcodes at the end of the derivative 

phase from a (b)nullable regular expression

is a generalised version of the $\textit{mkeps}$ function

for annotated regular expressions, called $\textit{bmkeps}$:

%\begin{definition}[\textit{bmkeps}]\mbox{}

\begin{center}

\begin{tabular}{lcl}

  $\textit{bmkeps}\,(_{bs}\ONE)$ & $\dn$ & $bs$\\

  $\textit{bmkeps}\,(_{bs}\sum a::\textit{as})$ & $\dn$ &

     $\textit{if}\;\textit{bnullable}\,a$\\

  & &$\textit{then}\;bs\,@\,\textit{bmkeps}\,a$\\

  & &$\textit{else}\;bs\,@\,\textit{bmkeps}\,(_{[]}\sum \textit{as})$\\

  $\textit{bmkeps}\,(_{bs} a_1 \cdot a_2)$ & $\dn$ &

     $bs \,@\,\textit{bmkeps}\,a_1\,@\, \textit{bmkeps}\,a_2$\\

  $\textit{bmkeps}\,(_{bs}a^*)$ & $\dn$ &

     $bs \,@\, [Z]$

\end{tabular}    

\end{center}    

%\end{definition}

\noindent

$\bmkeps$ completes the value information by travelling along the

path of the regular expression that corresponds to a POSIX value and

collecting all the bitcodes, and attaching $S$ to indicate the end of star

iterations. 

Now we give out the central part of this lexing algorithm,

the $\bder$ function (stands for \emph{b}itcoded-derivative).

For most time we use the infix notation $(\_\backslash\_)$ 

to mean $\bder$ for brevity when

there is no danger of confusion with derivatives on plain regular expressions.

For example, we write $( _{[]}r^* ) \backslash c$ instead of $\bder \;c \; _{[]}r^*$,

as the bitcodes at the front of $r^*$ indicates that it is 

a bit-coded regular expression, not a plain one.

$\bder$ tells us how regular expressions can be recursively traversed,

where the bitcodes are augmented and carried around 

when a derivative is taken.

\begin{center}

  \begin{tabular}{@{}lcl@{}}

  $(\ZERO)\,\backslash c$ & $\dn$ & $\ZERO$\\  

  $(_{bs}\ONE)\,\backslash c$ & $\dn$ & $\ZERO$\\  

  $(_{bs}{\bf d})\,\backslash c$ & $\dn$ &

        $\textit{if}\;c=d\; \;\textit{then}\;

         _{bs}\ONE\;\textit{else}\;\ZERO$\\  

  $(_{bs}\sum \;\textit{as})\,\backslash c$ & $\dn$ &

  $_{bs}\sum\;(\textit{map} \; (\_\backslash c) \; as )$\\

  $(_{bs}\;a_1\cdot a_2)\,\backslash c$ & $\dn$ &

     $\textit{if}\;\textit{bnullable}\,a_1$\\

					       & &$\textit{then}\;_{bs}\sum\,[(_{[]}\,(a_1\,\backslash c)\cdot\,a_2),$\\

					       & &$\phantom{\textit{then},\;_{bs}\sum\,}(\textit{fuse}\,(\textit{bmkeps}\,a_1)\,(a_2\,\backslash c))]$\\

  & &$\textit{else}\;_{bs}\,(a_1\,\backslash c)\cdot a_2$\\

  $(_{bs}a^*)\,\backslash c$ & $\dn$ &

      $_{bs}(\textit{fuse}\, [Z] \; r\,\backslash c)\cdot

       (_{[]}r^*))$

\end{tabular}    

\end{center}    

\noindent

We give the intuition behind some of the more involved cases in 

$\bder$. For example,

in the \emph{star} case,

a derivative on $_{bs}a^*$ means 

that one more star iteratoin needs to be taken.

we need to unfold it into a sequence,

and attach an additional bit $Z$ to the front of $r \backslash c$

as a record to indicate one new star iteration is unfolded.

\noindent

\begin{center}

  \begin{tabular}{@{}lcl@{}}

  $(_{bs}a^*)\,\backslash c$ & $\dn$ &

  $_{bs}(\underbrace{\textit{fuse}\, [Z] \; a\,\backslash c}_{\text{One more iteration}})\cdot

       (_{[]}a^*))$

\end{tabular}    

\end{center}   

\noindent

This information will be recovered later by the $\decode$ function.

The intuition is that the bit $Z$ will be decoded at the right location,

because we accumulate bits from left to right (a rigorous proof will be given

later).

\begin{tikzpicture}[ > = stealth, % arrow head style

        shorten > = 1pt, % don't touch arrow head to node

        semithick % line style

    ]

    \tikzstyle{every state}=[

        draw = black,

        thin,

        fill = cyan!29,

        minimum size = 7mm

    ]

    \begin{scope}[node distance=1cm and 0cm, every node/.style=state]

		\node (k) [rectangle split, rectangle split horizontal, rectangle split parts=2, rectangle split part fill={red!30,blue!20},]

        {$bs$

         \nodepart{two} $a^*$ };

	 \node (l) [below =of k, rectangle split, rectangle split horizontal, rectangle split parts=2, rectangle split part fill={red!30,blue!20},]

        { $bs$ + [Z]

         \nodepart{two}  $(a\backslash c )\cdot a^*$ };

    \end{scope}

    \path[->] 

	      (k) edge (l);

\end{tikzpicture}

Pictorially the process looks like below.

Like before, the red region denotes

previous lexing information (stored as bitcodes in $bs$).

\begin{tikzpicture}[every node/.append style={draw, rounded corners, inner sep=10pt}]

	\begin{scope}[node distance=1cm]   

		\node (a) [rectangle split, rectangle split horizontal, rectangle split parts=2, rectangle split part fill={red!30,blue!20},]

        {$bs$

         \nodepart{two} $a^*$ };

	 \node (b) [rectangle split, rectangle split horizontal, rectangle split parts=2, rectangle split part fill={red!30,blue!20},]

        { $bs$ + [Z]

         \nodepart{two}  $(a\backslash c )\cdot a^*$ };

%\caption{term 1 \ref{term:1}'s matching configuration}

 	\end{scope}

\end{tikzpicture}

\noindent

Another place in the $\bder$ function where it differs

from normal derivatives (on un-annotated regular expressions)

is the sequence case:

\begin{center}

  \begin{tabular}{@{}lcl@{}}

  $(_{bs}\;a_1\cdot a_2)\,\backslash c$ & $\dn$ &

     $\textit{if}\;\textit{bnullable}\,a_1$\\

					       & &$\textit{then}\;_{bs}\sum\,[(_{[]}\,(a_1\,\backslash c)\cdot\,a_2),$\\

					       & &$\phantom{\textit{then},\;_{bs}\sum\,}(\textit{fuse}\,(\textit{bmkeps}\,a_1)\,(a_2\,\backslash c))]$\\

  & &$\textit{else}\;_{bs}\,(a_1\,\backslash c)\cdot a_2$

\end{tabular}    

\end{center}    

The difference is that (when $a_1$ is $\bnullable$)

we use $\bmkeps$ to store the lexing information

in $a_1$ before collapsing it (as it has been fully matched by string prior to $c$, 

and attach the collected bit-codes to the front of $a_2$

before throwing away $a_1$. We assume that $\bmkeps$ correctly extracts the bitcode for how $a_1$

matches the string prior to $c$ (more on this later).

The bitsequence $\textit{bs}$ which was initially attached to the first element of the sequence

$a_1 \cdot a_2$, has now been elevated to the top level of teh $\sum$. 

This is because this piece of information will be needed whichever way the sequence is matched,

regardless of whether $c$ belongs to $a_1$ or $a_2$.

In the injection-based lexing, $r_1$ is immediately thrown away in 

subsequent derivatives on the right branch (when $r_1$ is $\nullable$),

\begin{center}

	$(r_1 \cdot r_2 )\backslash c = (r_1 \backslash c) \cdot r_2 + r_2 \backslash c$