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

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

\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 

\begin{itemize}

	\item

		It is a stepping stone towards the goal 

		of eliminating ``catastrophic backtracking''. 

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

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

%Everything about the structure remains intact.

%Therefore it does not change the size

%of an annotated regular expression and we have:

\noindent

One might be able to prove an inequality such as

$\llbracket a \rrbracket  \leq \llbracket  a_\downarrow \rrbracket_p $

and then estimate $\llbracket  a_\downarrow \rrbracket_p$,

but we found our approach more straightforward.\\

\subsection{Functions for R-regular Expressions}

The downside of our approach is that we need to redefine

several functions for $\rrexp$.

In this section we shall define the r-regular expression version

of $\bder$, and $\textit{bsimp}$ related functions.

We use $r$ as the prefix or subscript to differentiate

with the bitcoded version.

%For example,$\backslash_r$, $\rdistincts$, and $\rsimp$

%as opposed to $\backslash$, $\distinctBy$, and $\bsimp$.

%As promised, they are much simpler than their bitcoded counterparts.

%The operations on r-regular expressions are 

%almost identical to those of the annotated regular expressions,

%except that no bitcodes are used. For example,

The derivative operation for an r-regular expression is\\

\begin{center}

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

		$(\ZERO)\,\backslash_r c$ & $\dn$ & $\ZERO$\\  

		$(\ONE)\,\backslash_r c$ & $\dn$ &

		$\textit{if}\;c=d\; \;\textit{then}\;

		\ONE\;\textit{else}\;\ZERO$\\  

		$(\sum \;\textit{rs})\,\backslash_r c$ & $\dn$ &

		$\sum\;(\textit{map} \; (\_\backslash_r c) \; rs )$\\

		$(r_1\cdot r_2)\,\backslash_r c$ & $\dn$ &

		$\textit{if}\;(\textit{rnullable}\,r_1)$\\

						 & &$\textit{then}\;\sum\,[(r_1\,\backslash_r c)\cdot\,r_2,$\\

						 & &$\phantom{\textit{then},\;\sum\,}((r_2\,\backslash_r c))]$\\

						 & &$\textit{else}\;\,(r_1\,\backslash_r c)\cdot r_2$\\

		$(r^*)\,\backslash_r c$ & $\dn$ &

		$( r\,\backslash_r c)\cdot

		(_{[]}r^*))$

	\end{tabular}    

\end{center}  

\noindent

where we omit the definition of $\textit{rnullable}$.

The generalisation from the derivatives w.r.t a character to

derivatives w.r.t strings is given as

\begin{center}

	\begin{tabular}{lcl}

		$r \backslash_{rs} []$ & $\dn$ & $r$\\

		$r \backslash_{rs} c::s$ & $\dn$ & $(r\backslash_r c) \backslash_{rs} s$

	\end{tabular}

\end{center}

The function $\distinctBy$ for r-regular expressions does not need 

a function checking equivalence because

there are no bit annotations.

Therefore we have

\begin{center}

	\begin{tabular}{lcl}

		$\rdistinct{[]}{rset} $ & $\dn$ & $[]$\\

		$\rdistinct{r :: rs}{rset}$ & $\dn$ & 

		$\textit{if}(r \in \textit{rset}) \; \textit{then} \; \rdistinct{rs}{rset}$\\

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

					    r::\rdistinct{rs}{(rset \cup \{r\})}$

	\end{tabular}

\end{center}

%TODO: definition of rsimp (maybe only the alternative clause)

\noindent

%We would like to make clear

%a difference between our $\rdistincts$ and

%the Isabelle $\textit {distinct}$ predicate.

%In Isabelle $\textit{distinct}$ is a function that returns a boolean

%rather than a list.