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

Now we introduce the simplifications, which is why we introduce the 

bitcodes in the first place.

\section{Simplification for Annotated Regular Expressions}

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

\begin{center}

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

\end{center}

\noindent

Despite that we have already implemented the simple-minded simplifications 

such as throwing away useless $\ONE$s and $\ZERO$s.

The simplification rule $r + r \rightarrow $ cannot make a difference either

since it only removes duplicates on the same level, not something like 

$(r+a)+r \rightarrow r+a$.

This requires us to break up nested alternatives into lists, for example 

using the flatten operation similar to the one defined for any function language's

list datatype:

 \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

There is a minor difference though, in that our $\flts$ operation defined by us

also throws away $\ZERO$s.

For a flattened list of regular expressions, a de-duplication can be done efficiently:

\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 the same syntactically,

but having different bit-codes (more on the reason why we can do this later).

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

operation.

A recursive definition of our  simplification function 

that looks somewhat similar to our Scala code is given below:

\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)) \; \erase \; \phi) $ \\

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

\end{tabular}    

\end{center}    

\noindent

The simplification (named $\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 $\erase \; r_1 = \erase\; 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 notation of  natural

extension from derivative w.r.t.~character to derivative

w.r.t.~string, we define the derivative that nests simplifications with derivatives:%\comment{simp in  the [] case?}

\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

Extracting bit-codes from the derivatives that had been simplified repeatedly after 

each derivative run, the simplified $\blexer$, called $\blexersimp$,

is defined as 

 \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, for example,

with this simplification our previous $(a + aa)^*$ example's fast growth (over

$10^5$ nodes at around $20$ input length)

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

input string is.

We show some graphs to better demonstrate this imrpovement.

\section{$(a+aa)^*$ and $(a^*\cdot a^*)^*$  against $\protect\underbrace{aa\ldots a}_\text{n \textit{a}s}$ After Simplification}

For $(a+aa)^*$, it used to grow to over $9000$ nodes with simple-minded simplification

at only around $15$ input characters:

\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 {a_aa_star_bsimp.data};

\end{axis}

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

&

\begin{tikzpicture}

\begin{axis}[

    xlabel={$n$},

    ylabel={derivative size},

    width = 7cm,

    height = 4cm,

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

    legend pos=  north west,

    legend cell align=left]

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

\end{axis}

\end{tikzpicture} 

\end{tabular}

\end{center}

And for $(a^*\cdot a^*)^*$, unlike in \ref{fig:BetterWaterloo}, the size with simplification now stay nicely constant with current

simplification rules (we put the graphs together to show the contrast)

\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 without $\textit{bsimp}$},  

    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}

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

%	SECTION rewrite relation

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

\section{The Rewriting Relation $\rrewrite$($\rightsquigarrow$)}

In the $\blexer$'s correctness proof, we

did not directly derive the fact that $\blexer$ gives out the POSIX value,

but first prove that $\blexer$ is linked with $\lexer$.

Then we re-use

the correctness of $\lexer$.

Here we follow suit by first proving that

$\blexersimp \; r \; s $ 

produces the same output as $\blexer \; r\; s$,

and then putting it together with 

$\blexer$'s correctness result

($(r, s) \rightarrow v \implies \blexer \; r \;s = v$)

to obtain half of the correctness property (the other half

being when $s$ is not $L \; r$ which is routine to establish)

\begin{center}

	$(r, s) \rightarrow v \implies \blexersimp \; r \; s = v$

\end{center}

\noindent

because it makes the proof simpler

The overall idea for the correctness of our simplified bitcoded lexer

\noindent

is that the $\textit{bsimp}$ will not change the regular expressions so much that

it becomes impossible to extract the $\POSIX$ values.

To capture this "similarity" between unsimplified regular expressions and simplified ones,

we devise the rewriting relation $\rrewrite$, written infix as $\rightsquigarrow$:

\begin{center}

\begin{mathpar}

	\inferrule{}{_{bs} \ZERO \cdot r_2 \rightsquigarrow \ZERO\\}

	\inferrule{}{_{bs} r_1 \cdot \ZERO \rightsquigarrow \ZERO\\}

	\inferrule{}{_{bs1} ((_{bs2} \ONE) \cdot r) \rightsquigarrow \fuse \; (bs_1 @ bs_2) \; r\\}\\

	\inferrule{\\ r_1 \rightsquigarrow r_2}{_{bs} r_1 \cdot r_3 \rightsquigarrow _{bs} r_2 \cdot r_3\\}

	\inferrule{\\ r_3 \rightsquigarrow r_4}{_{bs} r_1 \cdot r_3 \rightsquigarrow _{bs} r_1 \cdot r_4\\}\\

	\inferrule{}{ _{bs}\sum [] \rightsquigarrow \ZERO\\}

	\inferrule{}{ _{bs}\sum [a] \rightsquigarrow \fuse \; bs \; a\\}

	\inferrule{\\ rs_1 \stackrel{s}{\rightsquigarrow} rs_2}{_{bs}\sum rs_1 \rightsquigarrow rs_2\\}

	\inferrule{}{\\ [] \stackrel{s}{\rightsquigarrow} []}

	\inferrule{rs_1 \stackrel{s}{\rightsquigarrow} rs_2}{\\ r :: rs_1 \rightsquigarrow r :: rs_2 \rightsquigarrow}

	\inferrule{r_1 \rightsquigarrow r_2}{ r_1 :: rs \stackrel{s}{\rightsquigarrow} r_2 :: rs\\}

	\inferrule{}{\ZERO :: rs \stackrel{s}{\rightsquigarrow} rs}

	\inferrule{}{_{bs} \sum (rs_1 :: rs_b) \stackrel{s}{\rightsquigarrow} ((\map \; (\fuse \; bs_1) \; rs_1) @ rsb) }

	\inferrule{\\ \rerase{a_1} = \rerase{a_2}}{rs_a @ [a_1] @ rs_b @ [a_2] @ rsc \stackrel{s}{\rightsquigarrow} rs_a @ [a_1] @ rs_b @ rs_c}

\end{mathpar}

\end{center}

These "rewrite" steps define the atomic simplifications we could impose on regular expressions

under our simplification algorithm.

For convenience, we define a relation $\stackrel{s}{\rightsquigarrow}$ for rewriting

a list of regular exression to another list.

The $\rerase{}$ function is used instead of $_\downarrow$ for the finiteness bound proof of next chapter,

which we will discuss later. For the moment the reader can assume they basically do the same thing as $\erase$.

Usually more than one steps are taking place during the simplification of a regular expression,

therefore we define the reflexive transitive closure of the $\rightsquigarrow$ and $\stackrel{s}{\rightsquigarrow}$

relations:

\begin{center}

\begin{mathpar}

	\inferrule{}{ r \stackrel{*}{\rightsquigarrow} r \\}

	\inferrule{}{\\ rs \stackrel{s*}{\rightsquigarrow} rs \\}

	\inferrule{\\r_1 \stackrel{*}{\rightsquigarrow}  r_2 \land \; r_2 \stackrel{*}{\rightsquigarrow} r_3}{r_1 \stackrel{*}{\rightsquigarrow} r_3\\}

	\inferrule{\\rs_1 \stackrel{*}{\rightsquigarrow}  rs_2 \land \; rs_2 \stackrel{*}{\rightsquigarrow} rs_3}{rs_1 \stackrel{*}{\rightsquigarrow} rs_3}

\end{mathpar}

\end{center}

Now that we have modelled the rewriting behaviour of our simplifier $\bsimp$, we prove mainly 

three properties about how these relations connect to $\blexersimp$:

\begin{itemize}

	\item

		$r \stackrel{*}{\rightsquigarrow} \bsimp{r}$

		The algorithm $\bsimp$ only transforms the regex $r$ using steps specified by 

		$\stackrel{*}{\rightsquigarrow}$ and nothing else.

	\item

		$r \rightsquigarrow r' \implies r \backslash c \rightsquigarrow r'\backslash c$.

		The relation $\stackrel{*}{rightsquigarrow}$ is preserved under derivative. 

	\item

		$(r \stackrel{*}{\rightsquigarrow} r'\land \bnullable \; r_1) \implies \bmkeps \; r = \bmkeps \; r'$. If we reach another 

		expression in finitely many atomic simplification steps, then these two regular expressions

		will produce the same bit-codes under the bit collection function $\bmkeps$ used by our $\blexer$.

\end{itemize}

\section{Three Important properties}

These properties would work together towards the correctness theorem.

We start proving each of these lemmas below.

\subsection{$(r \stackrel{*}{\rightsquigarrow} r'\land \bnullable \; r_1) \implies \bmkeps \; r = \bmkeps \; r'$ and $r \stackrel{*}{\rightsquigarrow} \bsimp{r}$}

The first few properties we establish is that the inference rules we gave for $\rightsquigarrow$

and $\stackrel{s}{\rightsquigarrow}$ also hold as implications for $\stackrel{*}{\rightsquigarrow}$ and 

$\stackrel{s*}{\rightsquigarrow}$.

\begin{lemma}

	$rs_1 \stackrel{s*}{\rightsquigarrow} rs_2 \implies _{bs} \sum rs_1 \stackrel{*}{\rightsquigarrow} _{bs} \sum rs_2$

\end{lemma}

\begin{proof}

	By rule induction of $\stackrel{s*}{\rightsquigarrow}$.

\end{proof}

\begin{lemma}

	$r \stackrel{*}{\rightsquigarrow} r' \implies _{bs} \sum r :: rs \stackrel{*}{\rightsquigarrow}  _{bs} \sum r' :: rs$

\end{lemma}

\begin{proof}

	By rule induction of $\stackrel{*}{\rightsquigarrow} $.

\end{proof}

\noindent

Then we establish that the $\stackrel{s}{\rightsquigarrow}$ and $\stackrel{s*}{\rightsquigarrow}$ relation is preserved w.r.t appending and prepending of a  list:

\begin{lemma}

	$rs_1 \stackrel{s}{\rightsquigarrow} rs_2 \implies rs @ rs_1 \stackrel{s}{\rightsquigarrow} rs @ rs_2$

\end{lemma}

\begin{proof}

	By induction on the list $rs$.

\end{proof}

\begin{lemma}

	$rs_1 \stackrel{s*}{\rightsquigarrow} rs_2 \implies rs @ rs_1 \stackrel{s*}{\rightsquigarrow} rs @ rs_2$

\end{lemma}

\begin{proof}

	By rule induction of $\stackrel{s*}{\rightsquigarrow}$.

\end{proof}

\noindent

The $\stackrel{s}{\rightsquigarrow} $ relation after appending a list becomes $\stackrel{s*}{\rightsquigarrow}$:

\begin{lemma}\label{ssgqTossgs}

	$rs_1 \stackrel{s}{\rightsquigarrow} rs_2 \implies rs_1 @ rs \stackrel{s*}{\rightsquigarrow} rs_2 @ rs$

\end{lemma}

\begin{proof}

	By rule induction of $\stackrel{s}{\rightsquigarrow}$.

\end{proof}

\begin{lemma}

	$rs_1 \stackrel{s*}{\rightsquigarrow} rs_2 \implies rs_1 @ rs \stackrel{s*}{\rightsquigarrow} rs_2 @ rs$

\end{lemma}

\begin{proof}

	By rule induction of $\stackrel{s*}{\rightsquigarrow}$ and using \ref{ssgqTossgs}.

\end{proof}

Here are two lemmas relating $\stackrel{*}{\rightsquigarrow}$ and $\stackrel{s*}{\rightsquigarrow}$:

\begin{lemma}\label{singleton}

	$r_1 \stackrel{*}{\rightsquigarrow} r_2 \implies [r_1] \stackrel{s*}{\rightsquigarrow} [r_2]$

\end{lemma}

\begin{proof}

	By rule induction of $ \stackrel{*}{\rightsquigarrow} $.

\end{proof}

\begin{lemma}

	$rs_3 \stackrel{s*}{\rightsquigarrow} rs_4 \land r_1 \stackrel{*}{\rightsquigarrow}  r_2 \implies

	r_2 :: rs_3 \stackrel{s*}{\rightsquigarrow} r_2 :: rs_4$

\end{lemma}

\begin{proof}

	By using \ref{singleton}.

\end{proof}

Now we get to the "meaty" part of the proof, which relates the relations $\stackrel{s*}{\rightsquigarrow}$ and 

$\stackrel{*}{\rightsquigarrow} $ with our simplification components such $\distinctBy$ and $\flts$.

The first lemma below says that for a list made of two parts $rs_1 @ rs_2$, one can throw away the duplicate

elements in $rs_2$, as well as those that have appeared in $rs_1$:

\begin{lemma}

	$rs_1 @ rs_2 \stackrel{s*}{\rightsquigarrow} (rs_1 @ (\distinctBy \; rs_2 \; \; \rerase{\_}\;  \; (\map\;\; \rerase{\_}\; \; rs_1)))$

\end{lemma}

\begin{proof}

	By induction on $rs_2$, where $rs_1$ is allowed to be arbitrary.

\end{proof}

The above h as the corollary that is suitable for the actual way $\distinctBy$ is called in $\bsimp$:

\begin{lemma}\label{dBPreserves}

	$rs_ 1 \rightarrow \distinctBy \; rs_1 \; \phi$

\end{lemma}

The flatten function $\flts$ works within the $\rightsquigarrow$ relation:

\begin{lemma}\label{fltsPreserves}

	$rs \stackrel{s*}{\rightsquigarrow} \flts \; rs$

\end{lemma}

The rewriting in many steps property is composible in terms of regular expression constructors:

\begin{lemma}

	$r_1 \stackrel{*}{\rightsquigarrow} r_2 \implies _{bs} r_1 \cdot r_3 \stackrel{*}{\rightsquigarrow} \;  _{bs} r_2 \cdot r_3 \quad $ and 

$r_3 \stackrel{*}{\rightsquigarrow} r_4 \implies _{bs} r_1 \cdot r_3 \stackrel{*}{\rightsquigarrow} _{bs} \; r_1 \cdot r_4$

\end{lemma}

The rewriting in many steps properties $\stackrel{*}{\rightsquigarrow}$ and $\stackrel{s*}{\rightsquigarrow}$ is preserved under the function $\fuse$:

\begin{lemma}

	$r_1 \stackrel{*}{\rightsquigarrow} r_2 \implies \fuse \; bs \; r_1 \stackrel{*}{\rightsquigarrow} \; \fuse \; bs \; r_2 \quad $ and 

	$rs_1 \stackrel{s}{\rightsquigarrow} rs_2 \implies \map \; (\fuse \; bs) \; rs_1 \stackrel{s*}{\rightsquigarrow} \map \; (\fuse \; bs) \; rs_2$

\end{lemma}

\begin{proof}

	By the properties $r_1 \rightsquigarrow r_2 \implies \fuse \; bs \; r_1 \implies \fuse \; bs \; r_2$ and

	$rs_2 \stackrel{s}{\rightsquigarrow} rs_3 \implies \map \; (\fuse \; bs) rs_2 \stackrel{s*}{\rightsquigarrow} \map \; (\fuse \; bs)\; rs_3$.

\end{proof}

\noindent

If we could rewrite a regular expression in many steps to $\ZERO$, then 

we could also rewrite any sequence containing it to $\ZERO$:

\begin{lemma}

	$r_1 \stackrel{*}{\rightsquigarrow} \ZERO \implies _{bs}r_1\cdot r_2 \stackrel{*}{\rightsquigarrow} \ZERO$

\end{lemma}

\begin{lemma}

	$\bmkeps \; (r \backslash s) = \bmkeps \; \bderssimp{r}{s}$

\end{lemma}