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

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$.

%material for setting the scene of the formal proof we

%are about to describe.

The fundamental reason is we cannot extend the correctness proof of theorem 4

because lemma 13 does not hold anymore when simplifications are involved.

%The proof details are necessary materials for this thesis

%because it provides necessary context to explain why we need a

%new framework for the proof of $\blexersimp$, which involves

%simplifications that cause structural changes to the regular expression.

%A new formal proof of the correctness of $\blexersimp$, where the 

%proof of $\blexer$

%is not applicatble in the sense that we cannot straightforwardly extend the

%proof of theorem \ref{blexerCorrect} because lemma \ref{retrieveStepwise} does

%not hold anymore.

%This is because the structural induction on the stepwise correctness

%of $\inj$ breaks due to each pair of $r_i$ and $v_i$ described

%in chapter \ref{Inj} and \ref{Bitcoded1} no longer correspond to

%each other.

%In this chapter we introduce simplifications

%for annotated regular expressions that can be applied to 

%each intermediate derivative result. This allows

%us to make $\blexer$ much more efficient.

%Sulzmann and Lu already introduced some simplifications for bitcoded regular expressions,

%but their simplification functions could have been more efficient and in some cases needed fixing.

In particular, the correctness theorem 

of the un-optimised bit-coded lexer $\blexer$ in 

chapter \ref{Bitcoded1} formalised by Ausaf et al.

relies crucially on lemma \ref{retrieveStepwise} that says

any value can be retrieved in a stepwise manner, namely:

\begin{equation}\label{eq:stepwise}%eqref: this proposition needs to be referred	

	\vdash v : (r\backslash c) \implies \retrieve \; (r \backslash c)  \;  v= \retrieve \; r \; (\inj \; r\; c\; v)

\end{equation}

%This no longer holds once we introduce simplifications.

Simplifications are necessary to control the size of derivatives,

but they also destroy the structures of the regular expressions

such that \ref{eq:stepwise} does not hold.

We want to prove the correctness of $\blexersimp$ which integrates

$\textit{bsimp}$ by applying it after each call to the derivative:

\begin{center}

\begin{tabular}{lcl}

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

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

\end{tabular}

\begin{tabular}{lcl}

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

      $\textit{let}\;a = (r^\uparrow)\backslash_{bsimp}\, 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

Previously without $\textit{bsimp}$ the exact structure of each intermediate 

regular expression is preserved, allowing pairs of inhabitation relations in the form $\vdash v : r_{c} $ and

$\vdash v^{c} : r $ to hold in lemma \ref{retrieveStepwise}(if 

we use the convenient notation $r_{c} \dn r\backslash c$

and $v_{r}^{c} \dn \inj \;r \; c \; v$),

but $\blexersimp$ introduces simplification after the derivative,

making it difficult to align the pairs:

\begin{center}

	$\vdash v: \textit{bsimp} \; r_{c} \implies \retrieve \; (\textit{bsimp} \; r_c) \; v =\retrieve \; r  \;(\mathord{?} v_{r}^{c}) $

\end{center}

\noindent

It is clear that once we made 

$v$ to align with $\textit{bsimp} \; r_{c}$

in the inhabitation relation, something different than $v_{r}^{c}$ needs to be plugged

in for the above statement to hold.

Ausaf et al. \cite{AusafUrbanDyckhoff2016}

made some initial attempts with this idea, see \cite{FahadThesis}

for details.

They added

and then rectify it to

this works fine, however that limits the kind of simplifications you can introduce.

We cannot use their idea for our very strong simplification rules.

Therefore we take our route

a wea

The other route is to dispose of lemma \ref{retrieveStepwise},

and prove a weakened inductive invariant instead.

We adopt this approach in this thesis.

Let us first explain why the requirement in $\blexer$'s proof

is too strong, and suggest a few possible fixes, which leads to

our proof which we believe was the most natural and effective method.

\section{Why Lemma \ref{retrieveStepwise}'s Requirement is too Strong}

%From this chapter we start with the main contribution of this thesis, which

The $\blexer$ proof relies on a lockstep POSIX

correspondence between the lexical value and the

regular expression in each derivative and injection.

If we zoom into the diagram \ref{graph:inj} and look specifically at

the pairs $v_i, r_i$ and $v_{i+1},\, r_{i+1}$, we get the diagram demonstrating

the invariant that the same bitcodes can be extracted from the pairs:

\tikzset{three sided/.style={

        draw=none,

        append after command={

            [-,shorten <= -0.5\pgflinewidth]

            ([shift={(-1.5\pgflinewidth,-0.5\pgflinewidth)}]\tikzlastnode.north east)

        edge([shift={( 0.5\pgflinewidth,-0.5\pgflinewidth)}]\tikzlastnode.north west) 

            ([shift={( 0.5\pgflinewidth,-0.5\pgflinewidth)}]\tikzlastnode.north west)

        edge([shift={( 0.5\pgflinewidth,+0.5\pgflinewidth)}]\tikzlastnode.south west)            

            ([shift={( 0.5\pgflinewidth,+0.5\pgflinewidth)}]\tikzlastnode.south west)

        edge([shift={(-1.0\pgflinewidth,+0.5\pgflinewidth)}]\tikzlastnode.south east)

        }

    }

}

\tikzset{three sided1/.style={

        draw=none,

        append after command={

            [-,shorten <= -0.5\pgflinewidth]

            ([shift={(1.5\pgflinewidth,-0.5\pgflinewidth)}]\tikzlastnode.north west)

        edge([shift={(-0.5\pgflinewidth,-0.5\pgflinewidth)}]\tikzlastnode.north east) 

            ([shift={(-0.5\pgflinewidth,-0.5\pgflinewidth)}]\tikzlastnode.north east)

        edge([shift={(-0.5\pgflinewidth,+0.5\pgflinewidth)}]\tikzlastnode.south east)            

            ([shift={(-0.5\pgflinewidth,+0.5\pgflinewidth)}]\tikzlastnode.south east)

        edge([shift={(1.0\pgflinewidth,+0.5\pgflinewidth)}]\tikzlastnode.south west)

        }

    }

}

	\begin{tikzpicture}[->, >=stealth', shorten >= 1pt, auto, thick]

		\path (1) edge [] node {} (2);

		\path (2) edge [] node {$\backslash a$} (3);

%		\node [rectangle, draw] (r) at (-6, -1) {$(aa)^*(b+c)$};

%		\node [rectangle, draw] (a) at (-6, 4)	  {$(aa)^*(_{Z}b + _{S}c)$};

%		\path	(r)

%			edge [] node {$\internalise$} (a);

%		\node [rectangle, draw] (a1) at (-3, 1) {$(_{Z}(\ONE \cdot a) \cdot (aa)^*) (_{Z}b + _Sc)$};

%		\path	(a)

%			edge [] node {$\backslash a$} (a1);

%

%		\node [rectangle, draw, three sided] (a21) at (-2.5, 4) {$(_{Z}\ONE \cdot (aa)^*)$};

%		\node [rectangle, draw, three sided1] (a22) at (-0.8, 4) {$(_{Z}b + _{S}c)$};

%		\path	(a1)

%			edge [] node {$\backslash a$} (a21);

%		\node [rectangle, draw] (a3) at (0.5, 2) {$_{ZS}(_{Z}\ONE + \ZERO)$};

%		\path	(a22)

%			edge [] node {$\backslash b$} (a3);

%		\path	(a21)

%			edge [dashed, bend right] node {} (a3);

%		\node [rectangle, draw] (bs) at (2, 4) {$ZSZ$};

%		\path	(a3)

%			edge [below] node {$\bmkeps$} (bs);

%		\node [rectangle, draw] (v) at (3, 0) {$\Seq \; (\Stars\; [\Seq \; a \; a]) \; (\Left \; b)$};

%		\path 	(bs)

%			edge [] node {$\decode$} (v);

	\end{tikzpicture}

When simplifications are added, the inhabitation relation no longer holds,

causing the above diagram to break.

Ausaf addressed this with an augmented lexer he called $\textit{slexer}$.

we note that the invariant

$\vdash v_{i+1}: r_{i+1} \implies \retrieve \; r_{i+1} \; v_{i+1} $ is too strong

to maintain because the precondition $\vdash v_i : r_i$ is too weak.

It does not require $v_i$ to be a POSIX value 

{\color{red} \rule{\linewidth}{0.5mm}}

New content ends

{\color{red} \rule{\linewidth}{0.5mm}}

%

%

%which is essential for getting an understanding this thesis

%in chapter \ref{Bitcoded1}, which is necessary for understanding why

%the proof 

%

%In this chapter,

%We contrast our simplification function 

%with Sulzmann and Lu's, indicating the simplicity of our algorithm.

%This is another case for 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 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 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

As can be seen, there are several duplications.

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}