% Chapter Template

% Main chapter title

\chapter{Correctness of Bit-coded Algorithm with Simplification}

\label{Bitcoded2} % 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 introduce the simplifications

on annotated regular expressions that can be applied to 

each intermediate derivative result. This allows

us to make $\blexer$ much more efficient.

We contrast this simplification function 

with Sulzmann and Lu's original

simplifications, indicating the simplicity of our algorithm and

improvements we made, demostrating

the usefulness and reliability of formal proofs on algorithms.

These ``aggressive'' simplifications would not be possible in the injection-based 

lexing we introduced in chapter \ref{Inj}.

We then go on to prove the correctness with the improved version of 

$\blexer$, called $\blexersimp$, by establishing 

$\blexer \; r \; s= \blexersimp \; r \; s$ using a term rewriting system.

\section{Simplifications by Sulzmann and Lu}

The first thing we notice in the fast growth of examples such as $(a^*a^*)^*$'s

and $(a^* + (aa)^*)^*$'s derivatives is that a lot of duplicated sub-patterns

are scattered around different levels, and therefore requires 

de-duplication at different levels:

\begin{center}

	$(a^*a^*)^* \stackrel{\backslash a}{\longrightarrow} (a^*a^* + a^*)\cdot(a^*a^*)^* \stackrel{\backslash a}{\longrightarrow} $\\

	$((a^*a^* + a^*) + a^*)\cdot(a^*a^*)^* + (a^*a^* + a^*)\cdot(a^*a^*)^* \stackrel{\backslash a}{\longrightarrow} \ldots$

\end{center}

\noindent

As we have already mentioned in \ref{eqn:growth2},

a simple-minded simplification function cannot simplify

the third regular expression in the above chain of derivative

regular expressions:

\begin{center}

$((a^*a^* + a^*) + a^*)\cdot(a^*a^*)^* + (a^*a^* + a^*)\cdot(a^*a^*)^*$

\end{center}

one would expect a better simplification function to work in the 

following way:

\begin{gather*}

	((a^*a^* + \underbrace{a^*}_\text{A})+\underbrace{a^*}_\text{duplicate of A})\cdot(a^*a^*)^* + 

	\underbrace{(a^*a^* + a^*)\cdot(a^*a^*)^*}_\text{further simp removes this}.\\

	\bigg\downarrow \\

	(a^*a^* + a^* 

	\color{gray} + a^* \color{black})\cdot(a^*a^*)^* + 

	\underbrace{(a^*a^* + a^*)\cdot(a^*a^*)^*}_\text{further simp removes this} \\

	\bigg\downarrow \\

	(a^*a^* + a^* 

	)\cdot(a^*a^*)^*  

	\color{gray} + (a^*a^* + a^*) \cdot(a^*a^*)^*\\

	\bigg\downarrow \\

	(a^*a^* + a^* 

	)\cdot(a^*a^*)^*  

\end{gather*}

\noindent

This motivating example came from testing Sulzmann and Lu's 

algorithm: their simplification does 

not work!

We quote their $\textit{simp}$ function verbatim here:

\begin{center}

	\begin{tabular}{lcl}

		$\simpsulz \; _{bs}(_{bs'}\ONE \cdot r)$ & $\dn$ & 

		$\textit{if} \; (\textit{zeroable} \; r)\; \textit{then} \;\; \ZERO$\\

						   & &$\textit{else}\;\; \fuse \; (bs@ bs') \; r$\\

		$\simpsulz \;(_{bs}r_1\cdot r_2)$ & $\dn$ & $\textit{if} 

		\; (\textit{zeroable} \; r_1 \; \textit{or} \; \textit{zeroable}\; r_2)\;

		\textit{then} \;\; \ZERO$\\

					     & & $\textit{else}\;\;_{bs}((\simpsulz \;r_1)\cdot

					     (\simpsulz \; r_2))$\\

		$\simpsulz  \; _{bs}\sum []$ & $\dn$ & $\ZERO$\\

		$\simpsulz  \; _{bs}\sum ((_{bs'}\sum rs_1) :: rs_2)$ & $\dn$ &

		$_{bs}\sum ((\map \; (\fuse \; bs')\; rs_1) @ rs_2)$\\

		$\simpsulz  \; _{bs}\sum[r]$ & $\dn$ & $\fuse \; bs \; (\simpsulz  \; r)$\\

		$\simpsulz  \; _{bs}\sum(r::rs)$ & $\dn$ & $_{bs}\sum 

		(\nub \; (\filter \; (\not \circ \zeroable)\;((\simpsulz  \; r) :: \map \; \simpsulz  \; rs)))$\\ 

	\end{tabular}

\end{center}

\noindent

the $\textit{zeroable}$ predicate 

which tests whether the regular expression

is equivalent to $\ZERO$,

is defined as:

\begin{center}

	\begin{tabular}{lcl}

		$\zeroable \; _{bs}\sum (r::rs)$ & $\dn$ & $\zeroable \; r\;\; \land \;\;

		\zeroable \;_{[]}\sum\;rs $\\

		$\zeroable\;_{bs}(r_1 \cdot r_2)$ & $\dn$ & $\zeroable\; r_1 \;\; \lor \;\; \zeroable \; r_2$\\

		$\zeroable\;_{bs}r^*$ & $\dn$ & $\textit{false}$ \\

		$\zeroable\;_{bs}c$ & $\dn$ & $\textit{false}$\\

		$\zeroable\;_{bs}\ONE$ & $\dn$ & $\textit{false}$\\

		$\zeroable\;_{bs}\ZERO$ & $\dn$ & $\textit{true}$

	\end{tabular}

\end{center}

\noindent

They suggested that the $\simpsulz $ function should be

applied repeatedly until a fixpoint is reached.

We call this construction $\textit{sulzSimp}$:

\begin{center}

	\begin{tabular}{lcl}

		$\textit{sulzSimp} \; r$ & $\dn$ & 

		$\textit{while}((\simpsulz  \; r)\; \cancel{=} \; r)$ \\

		& & $\quad r := \simpsulz  \; r$\\

		& & $\textit{return} \; r$

	\end{tabular}

\end{center}

We call the operation of alternatingly 

applying derivatives and simplifications

(until the string is exhausted) Sulz-simp-derivative,

written $\backslash_{sulzSimp}$:

\begin{center}

\begin{tabular}{lcl}

	$r \backslash_{sulzSimp} (c\!::\!s) $ & $\dn$ & $(\textit{sulzSimp} \; (r \backslash c)) \backslash_{sulzSimp}\, s$ \\

$r \backslash_{sulzSimp} [\,] $ & $\dn$ & $r$

\end{tabular}

\end{center}

\noindent

After the derivatives have been taken, the bitcodes

are extracted and decoded in the same manner

as $\blexer$:

\begin{center}

\begin{tabular}{lcl}

  $\textit{blexer\_sulzSimp}\;r\,s$ & $\dn$ &

      $\textit{let}\;a = (r^\uparrow)\backslash_{sulzSimp}\, s\;\textit{in}$\\                

  & & $\;\;\textit{if}\; \textit{bnullable}(a)$\\

  & & $\;\;\textit{then}\;\textit{decode}\,(\textit{bmkeps}\,a)\,r$\\

  & & $\;\;\textit{else}\;\textit{None}$

\end{tabular}

\end{center}

\noindent

We implemented this lexing algorithm in Scala, 

and found that the final derivative regular expression

size grows exponentially fast:

\begin{figure}[H]

	\centering

\begin{tikzpicture}

\begin{axis}[

    xlabel={$n$},

    ylabel={size},

    ymode = log,

    legend entries={Final Derivative Size},  

    legend pos=north west,

    legend cell align=left]

\addplot[red,mark=*, mark options={fill=white}] table {SulzmannLuLexer.data};

\end{axis}

\end{tikzpicture} 

\caption{Lexing the regular expression $(a^*a^*)^*$ against strings of the form

$\protect\underbrace{aa\ldots a}_\text{n \textit{a}s}

$ using Sulzmann and Lu's lexer}\label{SulzmannLuLexer}

\end{figure}

\noindent

At $n= 20$ we already get an out of memory error with Scala's normal 

JVM heap size settings.

In fact their simplification does not improve over

the simple-minded simplifications we have shown in \ref{fig:BetterWaterloo}.

The time required also grows exponentially:

\begin{figure}[H]

	\centering

\begin{tikzpicture}

\begin{axis}[

    xlabel={$n$},

    ylabel={time},

    ymode = log,

    legend entries={time in secs},  

    legend pos=north west,

    legend cell align=left]

\addplot[red,mark=*, mark options={fill=white}] table {SulzmannLuLexerTime.data};

\end{axis}

\end{tikzpicture} 

\caption{Lexing the regular expression $(a^*a^*)^*$ against strings of the form

$\protect\underbrace{aa\ldots a}_\text{n \textit{a}s}

$ using Sulzmann and Lu's lexer}\label{SulzmannLuLexerTime}

\end{figure}

\noindent

which seems like a counterexample for 

their linear complexity claim:

\begin{quote}\it

Linear-Time Complexity Claim \\It is easy to see that each call of one of the functions/operations:

simp, fuse, mkEpsBC and isPhi leads to subcalls whose number is bound by the size of the regular expression involved. We claim that thanks to aggressively applying simp this size remains finite. Hence, we can argue that the above mentioned functions/operations have constant time complexity which implies that we can incrementally compute bit-coded parse trees in linear time in the size of the input. 

\end{quote}

\noindent

The assumption that the size of the regular expressions

in the algorithm

would stay below a finite constant is not ture.

In addition to that, even if the regular expressions size

do stay finite, one has to take into account that

the $\simpsulz$ function is applied many times

in each derivative step, and that number is not necessarily

a constant with respect to the size of the regular expression.

To not get ``caught off guard'' by

these counterexamples,

one needs to be more careful when designing the

simplification function and making claims about them.

\section{Our $\textit{Simp}$ Function}

We will now introduce our simplification function,

by making a contrast with $\simpsulz$.

We describe

the ideas behind components in their algorithm 

and why they fail to achieve the desired effect, followed

by our solution. These solutions come with correctness

statements that are backed up by formal proofs.

\subsection{Flattening Nested Alternatives}

The idea behind the 

\begin{center}

$\simpsulz  \; _{bs}\sum ((_{bs'}\sum rs_1) :: rs_2) \quad \dn \quad

	       _{bs}\sum ((\map \; (\fuse \; bs')\; rs_1) @ rs_2)$

\end{center}

clause is that it allows

duplicate removal of regular expressions at different

levels.

For example, this would help with the

following simplification:

\begin{center}

$(a+r)+r \longrightarrow a+r$

\end{center}

The problem here is that only the head element

is ``spilled out'',

whereas we would want to flatten

an entire list to open up possibilities for further simplifications.\\

Not flattening the rest of the elements also means that

the later de-duplication processs 

does not fully remove apparent duplicates.

For example,

using $\simpsulz$ we could not 

simplify

\begin{center}

$((a^* a^*)+ (a^* + a^*))\cdot (a^*a^*)^*+

((a^*a^*)+a^*)\cdot (a^*a^*)^*$

\end{center}

due to the underlined part not in the first element

of the alternative.\\

We define a flatten operation that flattens not only 

the first regular expression of an alternative,

but the entire list: 

 \begin{center}

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

  $\textit{flts} \; (_{bs}\sum \textit{as}) :: \textit{as'}$ & $\dn$ & $(\textit{map} \;

     (\textit{fuse}\;bs)\; \textit{as}) \; @ \; \textit{flts} \; as' $ \\

  $\textit{flts} \; \ZERO :: as'$ & $\dn$ & $ \textit{flts} \;  \textit{as'} $ \\

    $\textit{flts} \; a :: as'$ & $\dn$ & $a :: \textit{flts} \; \textit{as'}$ \quad(otherwise) 

\end{tabular}    

\end{center}  

\noindent

Our $\flts$ operation 

also throws away $\ZERO$s

as they do not contribute to a lexing result.

\subsection{Duplicate Removal}

After flattening is done, we are ready to deduplicate.

The de-duplicate function is called $\distinctBy$,

and that is where we make our second improvement over

Sulzmann and Lu's.

The process goes as follows:

\begin{center}

$rs \stackrel{\textit{flts}}{\longrightarrow} 

rs_{flat} 

\xrightarrow{\distinctBy \; 

rs_{flat} \; \rerases\; \varnothing} rs_{distinct}$

%\stackrel{\distinctBy \; 

%rs_{flat} \; \erase\; \varnothing}{\longrightarrow} \; rs_{distinct}$

\end{center}

where the $\distinctBy$ function is defined as:

\begin{center}

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

		$\distinctBy \; [] \; f\; acc $ & $ =$ & $ []$\\

		$\distinctBy \; (x :: xs) \; f \; acc$ & $=$ & $\quad \textit{if} (f \; x \in acc)\;\; \textit{then} \;\; \distinctBy \; xs \; f \; acc$\\

						       & & $\quad \textit{else}\;\; x :: (\distinctBy \; xs \; f \; (\{f \; x\} \cup acc))$ 

	\end{tabular}

\end{center}

\noindent

The reason we define a distinct function under a mapping $f$ is because

we want to eliminate regular expressions that are syntactically the same,

but with different bit-codes.

For example, we can remove the second $a^*a^*$ from

$_{ZSZ}a^*a^* + _{SZZ}a^*a^*$, because it

represents a match with shorter initial sub-match 

(and therefore is definitely not POSIX),

and will be discarded by $\bmkeps$ later.

\begin{center}

	$_{ZSZ}\underbrace{a^*}_{ZS:\; match \; 1\; times\quad}\underbrace{a^*}_{Z: \;match\; 1 \;times} + 

	_{SZZ}\underbrace{a^*}_{S: \; match \; 0 \; times\quad}\underbrace{a^*}_{ZZ: \; match \; 2 \; times}

	$

\end{center}

%$_{bs1} r_1 + _{bs2} r_2 \text{where} (r_1)_{\downarrow} = (r_2)_{\downarrow}$

Due to the way our algorithm works,

the matches that conform to the POSIX standard 

will always be placed further to the left. When we 

traverse the list from left to right,

regular expressions we have already seen

will definitely not contribute to a POSIX value,

even if they are attached with different bitcodes.

These duplicates therefore need to be removed.

To achieve this, we call $\rerases$ as the function $f$ during the distinction

operation.\\

$\rerases$ is very similar to $\erase$, except that it preserves the structure

when erasing an alternative regular expression.

The reason why we use $\rerases$ instead of $\erase$ is that

it keeps the structures of alternative 

annotated regular expressions

whereas $\erase$ would turn it back into a binary structure.

Not having to mess with the structure 

greatly simplifies the finiteness proof in chapter \ref{Finite}.

We give the definitions of $\rerases$ here together with

the new datatype used by $\rerases$ (as our plain

regular expression datatype does not allow non-binary alternatives),

and explain in detail

why we want it in the next chapter.

For the moment the reader can just think of 

$\rerases$ as $\erase$ and $\rrexp$ as plain regular expressions.

\[			\rrexp ::=   \RZERO \mid  \RONE

			 \mid  \RCHAR{c}  

			 \mid  \RSEQ{r_1}{r_2}

			 \mid  \RALTS{rs}

			 \mid \RSTAR{r}        

\]

The notation of $\rerases$ also follows that of $\erase$,

which is a postfix operator written as a subscript,

except that it has an \emph{r} attached to it to distinguish against $\erase$:

\begin{center}

\begin{tabular}{lcl}

$\rerase{\ZERO}$ & $\dn$ & $\RZERO$\\

$\rerase{_{bs}\ONE}$ & $\dn$ & $\RONE$\\

	$\rerase{_{bs}\mathbf{c}}$ & $\dn$ & $\RCHAR{c}$\\

$\rerase{_{bs}r_1\cdot r_2}$ & $\dn$ & $\RSEQ{\rerase{r_1}}{\rerase{r_2}}$\\

$\rerase{_{bs}\sum as}$ & $\dn$ & $\RALTS{\map \; \rerase{\_} \; as}$\\

$\rerase{_{bs} a ^*}$ & $\dn$ & $\rerase{a}^*$

\end{tabular}

\end{center}

\subsection{Putting Things Together}

A recursive definition of our  simplification function 

is given below:

%that looks somewhat similar to our Scala code is 

\begin{center}

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

	  $\textit{bsimp} \; (_{bs}a_1\cdot a_2)$ & $\dn$ & $ \textit{bsimp}_{ASEQ} \; bs \;(\textit{bsimp} \; a_1) \; (\textit{bsimp}  \; a_2)  $ \\

	  $\textit{bsimp} \; (_{bs}\sum \textit{as})$ & $\dn$ & $\textit{bsimp}_{ALTS} \; \textit{bs} \; (\textit{distinctBy} \; ( \textit{flatten} ( \textit{map} \; bsimp \; as)) \; \rerases \; \varnothing) $ \\

   $\textit{bsimp} \; a$ & $\dn$ & $\textit{a} \qquad \textit{otherwise}$   

\end{tabular}    

\end{center}    

\noindent

The simplification (named $\textit{bsimp}$ for \emph{b}it-coded) 

does a pattern matching on the regular expression.

When it detected that the regular expression is an alternative or

sequence, it will try to simplify its children regular expressions

recursively and then see if one of the children turns into $\ZERO$ or

$\ONE$, which might trigger further simplification at the current level.

Current level simplifications are handled by the function $\textit{bsimp}_{ASEQ}$,

using rules such as  $\ZERO \cdot r \rightarrow \ZERO$ and $\ONE \cdot r \rightarrow r$.

\begin{center}

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

		$\textit{bsimp}_{ASEQ} \; bs\; a \; b$ & $\dn$ & $ (a,\; b) \textit{match}$\\

   &&$\quad\textit{case} \; (\ZERO, \_) \Rightarrow  \ZERO$ \\

   &&$\quad\textit{case} \; (\_, \ZERO) \Rightarrow  \ZERO$ \\

   &&$\quad\textit{case} \;  (_{bs1}\ONE, a_2') \Rightarrow  \textit{fuse} \; (bs@bs_1) \;  a_2'$ \\

   &&$\quad\textit{case} \; (a_1', a_2') \Rightarrow   _{bs}a_1' \cdot a_2'$ 

	\end{tabular}

\end{center}

\noindent

The most involved part is the $\sum$ clause, where we first call $\flts$ on

the simplified children regular expression list $\textit{map}\; \textit{bsimp}\; \textit{as}$.

and then call $\distinctBy$ on that list, the predicate determining whether two 

elements are the same is $\rerases \; r_1 = \rerases\; r_2$.

Finally, depending on whether the regular expression list $as'$ has turned into a

singleton or empty list after $\flts$ and $\distinctBy$, $\textit{bsimp}_{AALTS}$

decides whether to keep the current level constructor $\sum$ as it is, and 

removes it when there are less than two elements:

\begin{center}

	\begin{tabular}{lcl}

		$\textit{bsimp}_{AALTS} \; bs \; as'$ & $ \dn$ & $ as' \; \textit{match}$\\		

  &&$\quad\textit{case} \; [] \Rightarrow  \ZERO$ \\

   &&$\quad\textit{case} \; a :: [] \Rightarrow  \textit{fuse bs a}$ \\

   &&$\quad\textit{case} \;  as' \Rightarrow _{bs}\sum \textit{as'}$\\ 

	\end{tabular}

\end{center}

Having defined the $\bsimp$ function,

we add it as a phase after a derivative is taken,

so it stays small:

\begin{center}

	\begin{tabular}{lcl}

		$r \backslash_{bsimp} s$ & $\dn$ & $\textit{bsimp}(r \backslash s)$

	\end{tabular}

\end{center}

%Following previous notations

%when extending from derivatives w.r.t.~character to derivative

%w.r.t.~string, we define the derivative that nests simplifications 

%with derivatives:%\comment{simp in  the [] case?}

We extend this from character to string:

\begin{center}

\begin{tabular}{lcl}

$r \backslash_{bsimps} (c\!::\!s) $ & $\dn$ & $(r \backslash_{bsimp}\, c) \backslash_{bsimps}\, s$ \\

$r \backslash_{bsimps} [\,] $ & $\dn$ & $r$

\end{tabular}

\end{center}

\noindent

The lexer that extracts bitcodes from the 

derivatives with simplifications from our $\simp$ function

is called $\blexersimp$:

\begin{center}

\begin{tabular}{lcl}

  $\textit{blexer\_simp}\;r\,s$ & $\dn$ &

      $\textit{let}\;a = (r^\uparrow)\backslash_{simp}\, s\;\textit{in}$\\                

  & & $\;\;\textit{if}\; \textit{bnullable}(a)$\\

  & & $\;\;\textit{then}\;\textit{decode}\,(\textit{bmkeps}\,a)\,r$\\

  & & $\;\;\textit{else}\;\textit{None}$

\end{tabular}

\end{center}

\noindent

This algorithm keeps the regular expression size small.

\subsection{$(a+aa)^*$ and $(a^*\cdot a^*)^*$  against 

$\protect\underbrace{aa\ldots a}_\text{n \textit{a}s}$ After Simplification}

For example,

with our simplification the

previous $(a^*a^*)^*$ example

where $\simpsulz$ could not

stop the fast growth (over

3 million nodes just below $20$ input length)

will be reduced to just 15 and stays constant, no matter how long the

input string is.

This is demonstrated in the graphs below.

\begin{figure}[H]

\begin{center}

\begin{tabular}{ll}

\begin{tikzpicture}

\begin{axis}[

    xlabel={$n$},

    ylabel={derivative size},

        width=7cm,

    height=4cm, 

    legend entries={Lexer with $\textit{bsimp}$},  

    legend pos=  south east,

    legend cell align=left]

\addplot[red,mark=*, mark options={fill=white}] table {BitcodedLexer.data};

\end{axis}

\end{tikzpicture} %\label{fig:BitcodedLexer}

&

\begin{tikzpicture}

\begin{axis}[

    xlabel={$n$},

    ylabel={derivative size},

    width = 7cm,

    height = 4cm,

    legend entries={Lexer with $\simpsulz$},  

    legend pos=  north west,

    legend cell align=left]

\addplot[red,mark=*, mark options={fill=white}] table {BetterWaterloo.data};

\end{axis}

\end{tikzpicture} 

\end{tabular}

\end{center}

\caption{Our Improvement over Sulzmann and Lu's in terms of size}

\end{figure}

\noindent

Given the size difference, it is not

surprising that our $\blexersimp$ significantly outperforms

$\textit{blexer\_sulzSimp}$.

In the next section we are going to establish the

first important property of our lexer--the correctness.

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

%	SECTION rewrite relation

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

\section{Correctness of $\blexersimp$}

In this section we give details

of the correctness proof of $\blexersimp$,

an important contribution of this thesis.\\

We first introduce the rewriting relation \emph{rrewrite}

($\rrewrite$) between two regular expressions,

which expresses an atomic

simplification step from the left-hand-side

to the right-hand-side.

We then prove properties about

this rewriting relation and its reflexive transitive closure.

Finally we leverage these properties to show

an equivalence between the internal data structures of 

$\blexer$ and $\blexersimp$.