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

%\section{Overview}

\marginpar{\em Added a completely new \\overview section, \\highlighting\\ contributions.}

This chapter

is the point from which novel contributions of this PhD project are introduced

in detail. 

The material in the

previous

chapters is necessary for this thesis,

because it provides the context for why we need a new framework for

the proof of $\blexersimp$.

We will first introduce why aggressive simplifications are needed, after which we

provide our algorithm, contrasting with Sulzmann and Lu's simplifications.

We then explain how our simplifications make

reusing $\blexer$'s correctness proof impossible.

%with some minor modifications

We discuss possible fixes such as rectification functions and then introduce our proof, 

which involves a weaker inductive

invariant than that used in the correctness proof of $\blexer$.

\marginpar{Shortened overview.}

%material for setting the scene of the formal proof we

%are about to describe.

\section{Simplifications by Sulzmann and Lu}

\marginpar{moved \\simplification \\section to front \\to make coherent\\ sense.}

The algorithms $\lexer$ and $\blexer$ work beautifully as functional 

programs, but not as practical code. One main reason for the slowness is due

to the size of intermediate representations--the derivative regular expressions

tend to grow unbounded if the matching involved a large number of possible matches.

Consider the derivatives of the following example $(a^*a^*)^*$:

%and $(a^* + (aa)^*)^*$:

\begin{center}

	\begin{tabular}{lcl}

		$(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{tabular}

\end{center}

\noindent

From the second derivative several duplicate sub-expressions 

already needs to be eliminated (possible

bitcodes are omitted to make the presentation more concise

because they are not the key part of the simplifications).

A simple-minded simplification function cannot simplify

the third regular expression in the above chain of derivative

regular expressions, namely

\begin{center}

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

\end{center}

because the duplicates are

not next to each other, and therefore the rule

$r+ r \rightarrow r$ from $\textit{simp}$ does not fire.

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 (1) \\

	(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 (2) \\

	(a^*a^* + a^* 

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

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

	\bigg\downarrow (3) \\

	(a^*a^* + a^* 

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

\end{gather*}

\noindent

In the first step, the nested alternative regular expression

$(a^*a^* + a^*) + a^*$ is flattened into $a^*a^* + a^* + a^*$.

Now the third term $a^*$ can clearly be identified as a duplicate

and therefore removed in the second step. 

This causes the two

top-level terms to become the same and the second $(a^*a^*+a^*)\cdot(a^*a^*)^*$ 

removed in the final step.

Sulzmann and Lu's simplification function (using our notations) can achieve this

simplification:

\begin{center}

	\begin{tabular}{lcl}

		$\textit{simp}\_{SL} \; _{bs}(_{bs'}\ONE \cdot r)$ & $\dn$ & 

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

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

		$\textit{simp}\_{SL} \;(_{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}((\textit{simp}\_{SL} \;r_1)\cdot

							    (\textit{simp}\_{SL} \; r_2))$\\

		$\textit{simp}\_{SL}  \; _{bs}\sum []$ & $\dn$ & $\ZERO$\\

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

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

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

		$\textit{simp}\_{SL}  \; _{bs}\sum(r::rs)$ & $\dn$ & $_{bs}\sum 

		(\nub \; (\filter \; (\neg\zeroable)\;((\textit{simp}\_{SL}  \; r) :: \map \; \textit{simp}\_{SL}  \; rs)))$\\ 

	\end{tabular}

\end{center}

\noindent

The $\textit{zeroable}$ predicate 

tests whether the regular expression

is equivalent to $\ZERO$, and

can be 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

The 

\begin{center}

	\begin{tabular}{lcl}

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

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

	\end{tabular}

\end{center}

\noindent

clause does flatten the alternative as required in step (1),

but $\textit{simp}\_{SL}$ is insufficient if we want to do steps (2) and (3),

as these ``identical'' terms have different bit-annotations.

They also suggested that the $\textit{simp}\_{SL} $ function should be

applied repeatedly until a fixpoint is reached.

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

\begin{center}

	\begin{tabular}{lcl}

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

		$\textit{while}((\textit{simp}\_{SL}  \; r)\; \cancel{=} \; r)$ \\

					 & & $\quad r := \textit{simp}\_{SL}  \; 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_{SLSimp}$:

\begin{center}

\begin{tabular}{lcl}

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

$r \backslash_{SLSimp} [\,] $ & $\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\_SLSimp}\;r\,s$ & $\dn$ &

      $\textit{let}\;a = (r^\uparrow)\backslash_{SLSimp}\, 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 still grows exponentially (note the logarithmic scale):

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

Sulzmann and Lu's linear complexity claim

in their paper \cite{Sulzmann2014}:

\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 true, at least not in the

examples we considered.

The main reason behind this is that (i) Haskell's $\textit{nub}$

function requires identical annotations between two 

annotated regular expressions to qualify as duplicates,

and therefore cannot simplify cases like $_{SZZ}a^*+_{SZS}a^*$

even if both $a^*$ denote the same language, and

(ii) the ``flattening'' only applies to the head of the list

in the 

\begin{center}

	\begin{tabular}{lcl}

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

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

	\end{tabular}

\end{center}

\noindent

clause, and therefore is not strong enough to simplify all

needed parts of the regular expression. Moreover,

the $\textit{simp}\_{SL}$ function is applied repeatedly

in each derivative step until a fixed point is reached, 

which makes the algorithm even more

unpredictable and inefficient.

%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 own simplification function.

%by making a contrast with $\textit{simp}\_{SL}$.

We also describe

the ideas behind Sulzmann and Lu's $\textit{simp}\_{SL}$

algorithm 

and why it fails to achieve the desired effect of keeping the sizes of derivatives finitely bounded. 

In addition, our simplification function will come with a formal

correctness proof.

\subsection{Flattening Nested Alternatives}

The idea behind the clause

\begin{center}

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

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

\end{center}

is that it allows

duplicate removal of regular expressions at different

``levels'' of alternatives.

For example, this would help with the

following simplification:

\begin{center}

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

\end{center}

The problem is that only the head element

is ``spilled out''.

It is more desirable

to flatten

an entire list to open up possibilities for further simplifications

with later regular expressions.

Not flattening the rest of the elements also means that

the later de-duplication process 

does not fully remove further duplicates.

For example,

using $\textit{simp}\_{SL}$ we cannot

simplify

\begin{center}

	$((a^* a^*)+\underline{(a^* + a^*)})\cdot (a^*a^*)^*+

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

\end{center}

due to the underlined part not being the head 

of the alternative.

We define our flatten operation so that it flattens 

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 can deduplicate.

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

and that is where we make our second improvement over

Sulzmann and Lu's simplification method.

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 have 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. The function

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

For now we can think of 

$\rerases$ as the function erase ($(\_)_\downarrow$) defined in chapter \ref{Bitcoded1}

and $\rrexp$ as plain regular expressions, but having a general list constructor

for alternatives:

\begin{figure}[H]

\begin{center}	

	$\rrexp ::=   \RZERO \mid  \RONE

			 \mid  \RCHAR{c}  

			 \mid  \RSEQ{r_1}{r_2}

			 \mid  \RALTS{rs}

			 \mid \RSTAR{r}        $

\end{center}

\caption{$\rrexp$: plain regular expressions, but with $\sum$ alternative 

constructor}\label{rrexpDef}

\end{figure}

The function $\rerases$ we define as follows:

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

We will provide more details in \ref{whyRerase} for why a new

erase function and new datatype is needed. But briefly speaking

it is for backward-compatibility with $\blexer$'s correctness proof and 

the path we (naturally) took during our proof engineering of the finiteness property.

\subsection{Putting Things Together}

We can now give the definition of our  simplification function:

%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 detects 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 used in $\distinctBy$ for 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}_{ALTS}$

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

removes it when there are fewer than two elements:

\begin{center}

	\begin{tabular}{lcl}

		$\textit{bsimp}_{ALTS} \; 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 $\textit{bsimp}$ function,

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

\begin{center}

	\begin{tabular}{lcl}

		$a \backslash_{bsimp} c$ & $\dn$ & $\textit{bsimp}(a \backslash c)$

	\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 characters to strings:

\begin{center}

\begin{tabular}{lcl}

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

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

\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_{bsimp}\, s\;\textit{in}$\\