% Chapter Template

\chapter{Finiteness Bound} % Main chapter title

\label{Finite} 

%  In Chapter 4 \ref{Chapter4} we give the second guarantee

%of our bitcoded algorithm, that is a finite bound on the size of any 

%regex's derivatives. 

%(this is cahpter 5 now)

In this chapter we give a bound in terms of the size of 

the calculated derivatives: 

given an annotated regular expression $a$, for any string $s$

our algorithm $\blexersimp$'s derivatives

are finitely bounded

by a constant that only depends on $a$.

Formally we show that there exists a constant integer $N_a$ such that

\begin{center}

	$\llbracket \bderssimp{a}{s} \rrbracket \leq N_a$

\end{center}

\noindent

where the size ($\llbracket \_ \rrbracket$) of 

an annotated regular expression is defined

in terms of the number of nodes in its 

tree structure (its recursive definition is given in the next page).

We believe this size bound

is important in the context of POSIX lexing because 

\marginpar{Addressing Gerog comment: "how does this relate to backtracking?"}

\begin{itemize}

	\item

		It is a stepping stone towards the goal 

		of eliminating ``catastrophic backtracking''. 

		The derivative-based lexing algorithm avoids backtracking

		by a trade-off between space and time.

		Backtracking algorithms

		save other possibilities on a stack when exploring one possible

		path of matching. Catastrophic backtracking typically occurs

		when the number of steps increase exponentially with respect

		to input. In other words, the runtime is $O((c_r)^n)$ of the input

		string length $n$, where the base of the exponent is determined by the

		regular expression $r$.

		%so that they

		%can be traversed in the future in a DFS manner,

		%different matchings are stored as sub-expressions 

		%in a regular expression derivative.

		Derivatives saves these possibilities as sub-expressions

		and traverse those during future derivatives. If we denote the size

		of intermediate derivatives as $S_{r,n}$ (where the subscripts

		$r,n$ indicate that $S$ depends on them), then the runtime of 

		derivative-based approaches would be $O(S_{r,n} * n)$.

		We observe that if $S_{r,n}$ continously grows with $n$ (for example

		growing exponentially fast), then this

		is equally bad as catastrophic backtracking.

		Our finiteness bound seeks to find a constant integer

		upper bound $C$ (which in our case is $N_a$ where $a = r^\uparrow$) of $\S_{r,n}$,

		so that the complexity of the algorithm can be seen as linear ($O(C * n)$).

		Even if $C$ is still large in our current work, it is still a constant

		rather than ever-increasing number with respect to input length $n$.

		More importantly this $C$ constant can potentially

		be shrunken as we optimize our simplification procedure. 

		%and showing the potential

		%improvements can be by the notion of partial derivatives.

		%If the internal data structures used by our algorithm

		%grows beyond a finite bound, then clearly 

		%the algorithm (which traverses these structures) will

		%be slow.

		%The next step is to refine the bound $N_a$ so that it

		%is not just finite but polynomial in $\llbracket a\rrbracket$.

	\item

		Having the finite bound formalised 

		gives us higher confidence that

		our simplification algorithm $\simp$ does not ``misbehave''

		like $\textit{simpSL}$ does.

		The bound is universal for a given regular expression, 

		which is an advantage over work which 

		only gives empirical evidence on 

		some test cases (see for example Verbatim work \cite{Verbatimpp}).

\end{itemize}

\noindent

We then extend our $\blexersimp$

to support bounded repetitions ($r^{\{n\}}$).

We update our formalisation of 

the correctness and finiteness properties to

include this new construct. 

We show that we can out-compete other verified lexers such as

Verbatim++ on bounded regular expressions.

In the next section we describe in more detail

what the finite bound means in our algorithm

and why the size of the internal data structures of

a typical derivative-based lexer such as

Sulzmann and Lu's needs formal treatment.

\section{Formalising Size Bound of Derivatives}

\noindent

In our lexer ($\blexersimp$),

we take an annotated regular expression as input,

and repeately take derivative of and simplify it.

\begin{figure}

	\begin{center}

		\begin{tabular}{lcl}

			$\llbracket _{bs}\ONE \rrbracket$ & $\dn$ & $1$\\

			$\llbracket \ZERO \rrbracket$ & $\dn$ & $1$ \\

			$\llbracket _{bs} r_1 \cdot r_2 \rrbracket$ & $\dn$ & $\llbracket r_1 \rrbracket + \llbracket r_2 \rrbracket + 1$\\

			$\llbracket _{bs}\mathbf{c} \rrbracket $ & $\dn$ & $1$\\

			$\llbracket _{bs}\sum as \rrbracket $ & $\dn$ & $\map \; (\llbracket \_ \rrbracket)\; as   + 1$\\

			$\llbracket _{bs} a^* \rrbracket $ & $\dn$ & $\llbracket a \rrbracket + 1$.

		\end{tabular}

	\end{center}

	\caption{The size function of bitcoded regular expressions}\label{brexpSize}

\end{figure}

\begin{figure}

	\begin{tikzpicture}[scale=2,

		every node/.style={minimum size=11mm},

		->,>=stealth',shorten >=1pt,auto,thick

		]

		\node (r0) [rectangle, draw=black, thick, minimum size = 5mm, draw=blue] {$a$};

		\node (r1) [rectangle, draw=black, thick, right=of r0, minimum size = 7mm]{$a_1$};

		\draw[->,line width=0.2mm](r0)--(r1) node[above,midway] {$\backslash c_1$};

		\node (r1s) [rectangle, draw=blue, thick, right=of r1, minimum size=6mm]{$a_{1s}$};

		\draw[->, line width=0.2mm](r1)--(r1s) node[above, midway] {$\simp$};

		\node (r2) [rectangle, draw=black, thick,  right=of r1s, minimum size = 12mm]{$a_2$};

		\draw[->,line width=0.2mm](r1s)--(r2) node[above,midway] {$\backslash c_2$};

		\node (r2s) [rectangle, draw = blue, thick, right=of r2,minimum size=6mm]{$a_{2s}$};

		\draw[->,line width=0.2mm](r2)--(r2s) node[above,midway] {$\simp$};

		\node (rns) [rectangle, draw = blue, thick, right=of r2s,minimum size=6mm]{$a_{ns}$};

		\draw[->,line width=0.2mm, dashed](r2s)--(rns) node[above,midway] {$\backslash \ldots$};

		\node (v) [circle, thick, draw, right=of rns, minimum size=6mm, right=1.7cm]{$v$};

		\draw[->, line width=0.2mm](rns)--(v) node[above, midway] {\bmkeps} node [below, midway] {\decode};

	\end{tikzpicture}

	\caption{Regular expression size change during our $\blexersimp$ algorithm}\label{simpShrinks}

\end{figure}

\noindent

Each time

a derivative is taken, the regular expression might grow.

However, the simplification that is immediately afterwards will often shrink it so that 

the overall size of the derivatives stays relatively small.

This intuition is depicted by the relative size

change between the black and blue nodes:

After $\simp$ the node shrinks.

Our proof states that all the blue nodes

stay below a size bound $N_a$ determined by the input $a$.

\noindent

Sulzmann and Lu's assumed a similar picture of their algorithm,

though in fact their algorithm's size might be better depicted by the following graph:

\begin{figure}[H]

	\begin{tikzpicture}[scale=2,

		every node/.style={minimum size=11mm},

		->,>=stealth',shorten >=1pt,auto,thick

		]

		\node (r0) [rectangle, draw=black, thick, minimum size = 5mm, draw=blue] {$a$};

		\node (r1) [rectangle, draw=black, thick, right=of r0, minimum size = 7mm]{$a_1$};

		\draw[->,line width=0.2mm](r0)--(r1) node[above,midway] {$\backslash c_1$};

		\node (r1s) [rectangle, draw=blue, thick, right=of r1, minimum size=7mm]{$a_{1s}$};

		\draw[->, line width=0.2mm](r1)--(r1s) node[above, midway] {$\simp'$};

		\node (r2) [rectangle, draw=black, thick,  right=of r1s, minimum size = 17mm]{$a_2$};

		\draw[->,line width=0.2mm](r1s)--(r2) node[above,midway] {$\backslash c_2$};

		\node (r2s) [rectangle, draw = blue, thick, right=of r2,minimum size=14mm]{$a_{2s}$};

		\draw[->,line width=0.2mm](r2)--(r2s) node[above,midway] {$\simp'$};

		\node (r3) [rectangle, draw = black, thick, right= of r2s, minimum size = 22mm]{$a_3$};

		\draw[->,line width=0.2mm](r2s)--(r3) node[above,midway] {$\backslash c_3$};

		\node (rns) [right = of r3, draw=blue, minimum size = 20mm]{$a_{3s}$};

		\draw[->,line width=0.2mm] (r3)--(rns) node [above, midway] {$\simp'$};

		\node (rnn) [right = of rns, minimum size = 1mm]{};

		\draw[->, dashed] (rns)--(rnn) node [above, midway] {$\ldots$};

	\end{tikzpicture}

	\caption{Regular expression size change during our $\blexersimp$ algorithm}\label{sulzShrinks}

\end{figure}

\noindent

The picture means that in some cases their lexer (where they use $\simpsulz$ 

as the simplification function)

will have a size explosion, causing the running time 

of each derivative step to grow continuously (for example 

in \ref{SulzmannLuLexerTime}).

They tested out the run time of their

lexer on particular examples such as $(a+b+ab)^*$

and claimed that their algorithm is linear w.r.t to the input.

With our mechanised proof, we avoid this type of unintentional

generalisation.

Before delving into the details of the formalisation,

we are going to provide an overview of it in the following subsection.

\subsection{Overview of the Proof}

\marginpar{trying to make it more intuitive

and provide more insights into proof}

regular expression derivatives with respect to strings.

Assume we have a regular expression $r$, be it an alternative,

a sequence or a star, the idea is if we try to take several derivatives

of it on paper, we end up getting a list of subexpressions,

something like

%omitting certain

%nested structures of those expressions:

\[

	r\backslash s = r_1 + r_2 + r_3 + \ldots + r_n,

\]

if we omit the way these regular expressions need to be nested.

where each $r_i$ ($i \in \{1, \ldots, n\}$) is related to some fragments

of $r$ and $s$.

The second important observation is that the list %of regular expressions

$[r_1, \ldots, r_n]$ %is not

cannot grow indefinitely because they all come from $r$, and derivatives

of the same regular expression are finite up to some isomorphisms.

We prove that the simplifications of $\blexersimp$ %make use of 

is powerful enough to counteract the effect of nested structure of alternatives

and eliminate duplicates

such that indeed the list in $a\backslash s$ does not grow unbounded.

A high-level overview of the main components of the finiteness proof

is as follows:

\begin{figure}[H]

	\begin{tikzpicture}[scale=1,font=\bf,

		node/.style={

			rectangle,rounded corners=3mm,

			ultra thick,draw=black!50,minimum height=18mm, 

			minimum width=20mm,

		top color=white,bottom color=black!20}]

		\node (0) at (-5,0) 

			[node, text width=1.8cm, text centered] 

			{$\llbracket \bderssimp{a}{s} \rrbracket$};

		\node (A) at (0,0) 

			[node,text width=1.6cm,  text centered] 

			{$\llbracket \rderssimp{r}{s} \rrbracket_r$};

		\node (B) at (3,0) 

			[node,text width=3.0cm, anchor=west, minimum width = 40mm] 

			{$\llbracket \textit{ClosedForm}(r, s)\rrbracket_r$};

		\node (C) at (9.5,0) [node, minimum width=10mm] {$N_r$};

		\draw [->,line width=0.5mm] (0) -- 

			node [above,pos=0.45] {=} (A) node [below, pos = 0.45] {$(r = a \downarrow_r)$} (A); 

		\draw [->,line width=0.5mm] (A) -- 

			node [above,pos=0.35] {$\quad =\ldots=$} (B); 

		\draw [->,line width=0.5mm] (B) -- 

			node [above,pos=0.35] {$\quad \leq \ldots \leq$} (C); 

	\end{tikzpicture}

	%\caption{

\end{figure}

\noindent

We explain the steps one by one:

\begin{itemize}

	\item

		We first introduce the operations such as 

		derivatives, simplification, size calculation, etc.

		associated with $\rrexp$s, which we have introduced

		in chapter \ref{Bitcoded2}. As promised we will discuss

		why they are needed in \ref{whyRerase}.

		The operations on $\rrexp$s are identical to those on

		annotated regular expressions except that they dispense with

		bitcodes. This means that all proofs about size of $\rrexp$s will apply to

		annotated regular expressions, because the size of a regular

		expression is independent of the bitcodes.

	\item

		We prove that $\rderssimp{r}{s} = \textit{ClosedForm}(r, s)$,

		where $\textit{ClosedForm}(r, s)$ is entirely 

		given as the derivatives of their children regular 

		expressions.

		We call the right-hand-side the \emph{Closed Form}

		of the derivative $\rderssimp{r}{s}$.

	\item

		Formally we give an estimate of 

		$\llbracket \textit{ClosedForm}(r, s) \rrbracket_r$.

		The key observation is that $\distinctBy$'s output is

		a list with a constant length bound.

\end{itemize}

We will expand on these steps in the next sections.\\

\section{The $\textit{Rrexp}$ Datatype}

The first step is to define 

$\textit{rrexp}$s.

They are annotated regular expressions without bitcodes,

allowing a more convenient size bound proof.

%Of course, the bits which encode the lexing information 

%would grow linearly with respect 

%to the input, which should be taken into accounte when we wish to tackle the runtime complexity.

%But for the sake of the structural size 

%we can safely ignore them.\\

The datatype 

definition of the $\rrexp$, called

\emph{r-regular expressions},

was initially defined in \ref{rrexpDef}.

The reason for the prefix $r$ is

to make a distinction  

with basic regular expressions.

We give here again the definition of $\rrexp$.

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

	\mid  \RCHAR{c}  

	\mid  \RSEQ{r_1}{r_2}

	\mid  \RALTS{rs}

	\mid \RSTAR{r}        

\]

The size of an r-regular expression is

written $\llbracket r\rrbracket_r$, 

whose definition mirrors that of an annotated regular expression. 

\begin{center}

	\begin{tabular}{lcl}

		$\llbracket _{bs}\ONE \rrbracket_r$ & $\dn$ & $1$\\

		$\llbracket \ZERO \rrbracket_r$ & $\dn$ & $1$ \\

		$\llbracket _{bs} r_1 \cdot r_2 \rrbracket_r$ & $\dn$ & $\llbracket r_1 \rrbracket_r + \llbracket r_2 \rrbracket_r + 1$\\

		$\llbracket _{bs}\mathbf{c} \rrbracket_r $ & $\dn$ & $1$\\

		$\llbracket _{bs}\sum as \rrbracket_r $ & $\dn$ & $\map \; (\llbracket \_ \rrbracket_r)\; as   + 1$\\

		$\llbracket _{bs} a^* \rrbracket_r $ & $\dn$ & $\llbracket a \rrbracket_r + 1$.

	\end{tabular}

\end{center}

\noindent

The $r$ in the subscript of $\llbracket \rrbracket_r$ is to 

differentiate with the same operation for annotated regular expressions.

Similar subscripts will be added for operations like $\rerase{}$:

\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{Why a New Datatype?}\label{whyRerase}

\marginpar{\em added label so this section can be referenced by other parts of the thesis

so that interested readers can jump to/be reassured that there will explanations.}

Originally the erase operation $(\_)_\downarrow$ was

used by Ausaf et al. in their proofs related to $\blexer$.

This function was not part of the lexing algorithm, and the sole purpose was to

bridge the gap between the $r$

%$\textit{rexp}$ 

(un-annotated) and $\textit{arexp}$ (annotated)

regular expression datatypes so as to leverage the correctness

theorem of $\lexer$.%to establish the correctness of $\blexer$.

For example, lemma \ref{retrieveStepwise} %and \ref{bmkepsRetrieve} 

uses $\erase$ to convert an annotated regular expression $a$ into

a plain one so that it can be used by $\inj$ to create the desired value

$\inj\; (a)_\downarrow \; c \; v$.

Ideally $\erase$ should only remove the auxiliary information not related to the

structure--the 

bitcodes. However there exists a complication

where the alternative constructors have different arity for $\textit{arexp}$

and $\textit{r}$:

\begin{center}

	\begin{tabular}{lcl}

		$\textit{r}$ & $::=$ & $\ldots \;|\; (\_ + \_) \; ::\; "\textit{r} \Rightarrow \textit{r} \Rightarrow \textit{r}" | \ldots$\\

		$\textit{arexp}$ & $::=$ & $\ldots\; |\; (\Sigma \_ ) \; ::\; "\textit{arexp} \; list \Rightarrow \textit{arexp}" | \ldots$

	\end{tabular}

\end{center}

\noindent

To convert between the two

$\erase$ has to recursively disassemble a list into nested binary applications of the 

$(\_ + \_)$ operator,

handling corner cases like empty or

singleton alternative lists:

%becomes $r$ during the

%$\erase$ function.

%The  annotated regular expression $\sum[a, b, c]$ would turn into

%$(a+(b+c))$.

\begin{center}

	\begin{tabular}{lcl}

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

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

		$ (_{bs}\sum a_1 :: a_2)_\downarrow$ & $\dn$ & $(a_1)_\downarrow + (a_2)_\downarrow)$\\

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

	\end{tabular}

\end{center}

\noindent

These operations inevitably change the structure and size of

an annotated regular expression. For example,

$a_1 = \sum _{Z}[x]$ has size 2, but $(a_1)_\downarrow = x$ 

only has size 1.

%adding unnecessary 

%complexities to the size bound proof.

%The reason we

%define a new datatype is that 

%the $\erase$ function 

%does not preserve the structure of annotated

%regular expressions.

%We initially started by using 

%plain regular expressions and tried to prove

%lemma \ref{rsizeAsize},

%however the $\erase$ function messes with the structure of the 

%annotated regular expression.

%The $+$ constructor

%of basic regular expressions is only binary, whereas $\sum$ 

%takes a list. Therefore we need to convert between

%annotated and normal regular expressions as follows:

For example, if we define the size of a basic plain regular expression 

in the usual way,

\begin{center}

	\begin{tabular}{lcl}

		$\llbracket \ONE \rrbracket_p$ & $\dn$ & $1$\\

		$\llbracket \ZERO \rrbracket_p$ & $\dn$ & $1$ \\

		$\llbracket r_1 + r_2 \rrbracket_p$ & $\dn$ & $\llbracket r_1 \rrbracket_p + \llbracket r_2 \rrbracket_p + 1$\\

		$\llbracket \mathbf{c} \rrbracket_p $ & $\dn$ & $1$\\

		$\llbracket r_1 \cdot r_2 \rrbracket_p $ & $\dn$ & $\llbracket r_1 \rrbracket_p \; + \llbracket r_2 \rrbracket_p + 1$\\

		$\llbracket a^* \rrbracket_p $ & $\dn$ & $\llbracket a \rrbracket_p + 1$

	\end{tabular}

\end{center}

\noindent

Then the property

\begin{center}

	$\llbracket a \rrbracket \stackrel{?}{=} \llbracket a_\downarrow \rrbracket_p$

\end{center}

does not hold.

%With $\textit{rerase}$, however, 

%only the bitcodes are thrown away.

That leads to us defining the new regular expression datatype without

bitcodes but with a list alternative constructor, and defining a new erase function

in a strictly structure-preserving manner:

\begin{center}

	\begin{tabular}{lcl}

		$\textit{rrexp}$ & $::=$ & $\ldots\; |\; (\sum \_ ) \; ::\; "\textit{rrexp} \; list \Rightarrow \textit{rrexp}" | \ldots$\\

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

	\end{tabular}

\end{center}

\noindent

%But