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

Formally we show that there exists an $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 

\begin{itemize}

	\item

		It is a stepping stone towards the goal 

		of eliminating ``catastrophic backtracking''. 

		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}

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

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

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:

\begin{center}

	\begin{tabular}{lcl}

		$\erase \; _{bs}\sum [] $ & $\dn$ & $\ZERO$\\

		$\erase \; _{bs}\sum [a]$ & $\dn$ & $a$\\

		$\erase \; _{bs}\sum a :: as$ & $\dn$ & $a + (\erase \; _{[]} \sum as)\quad \text{if $as$ length over 1}$

	\end{tabular}

\end{center}

\noindent

As can be seen, alternative regular expressions with an empty argument list

will be turned into a $\ZERO$.

The singleton alternative $\sum [r]$ becomes $r$ during the

$\erase$ function.

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

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

All these operations change the size and structure of

an annotated regular expression, adding unnecessary 

complexities to the size bound proof.

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 \cdot 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.

Everything about the structure remains intact.

Therefore it does not change the size

of an annotated regular expression and we have:

\begin{lemma}\label{rsizeAsize}

	$\rsize{\rerase a} = \asize a$

\end{lemma}

\begin{proof}

	By routine structural induction on $a$.

\end{proof}

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

%It tests if all the elements of a list are unique.\\

With $\textit{rdistinct}$ in place,

the flatten function for $\rrexp$ is as follows:

 \begin{center}

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

  $\textit{rflts} \; (\sum \textit{as}) :: \textit{as'}$ & $\dn$ & $as \; @ \; \textit{rflts} \; as' $ \\

  $\textit{rflts} \; \ZERO :: as'$ & $\dn$ & $ \textit{rflts} \;  \textit{as'} $ \\

    $\textit{rflts} \; a :: as'$ & $\dn$ & $a :: \textit{rflts} \; \textit{as'}$ \quad(otherwise) 

\end{tabular}    

\end{center}  

\noindent

The function 

$\rsimpalts$ corresponds to $\textit{bsimp}_{ALTS}$:

\begin{center}

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

	  $\rsimpalts \;\; nil$ & $\dn$ & $\RZERO$\\

	  $\rsimpalts \;\; r::nil$ & $\dn$ & $r$\\

	  $\rsimpalts \;\; rs$ & $\dn$ & $\sum rs$\\

\end{tabular}    

\end{center}  

\noindent

Similarly, we have $\rsimpseq$ which corresponds to $\textit{bsimp}_{SEQ}$:

\begin{center}

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

	  $\rsimpseq \;\; \RZERO \; \_ $ &   $=$ &   $\RZERO$\\

	  $\rsimpseq \;\; \_ \; \RZERO $ &   $=$ &   $\RZERO$\\

	  $\rsimpseq \;\; \RONE \cdot r_2$ & $\dn$ & $r_2$\\

	  $\rsimpseq \;\; r_1 r_2$ & $\dn$ & $r_1 \cdot r_2$\\

\end{tabular}    

\end{center}  

and get $\textit{rsimp}$ and $\rderssimp{\_}{\_}$:

\begin{center}

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

	  $\textit{rsimp} \; (r_1\cdot r_2)$ & $\dn$ & $ \textit{rsimp}_{SEQ} \; bs \;(\textit{rsimp} \; r_1) \; (\textit{rsimp}  \; r_2)  $ \\

	  $\textit{rsimp} \; (_{bs}\sum \textit{rs})$ & $\dn$ & $\textit{rsimp}_{ALTS} \; \textit{bs} \; (\textit{rdistinct} \; ( \textit{rflts} ( \textit{map} \; rsimp \; rs)) \; \rerases \; \varnothing) $ \\

   $\textit{rsimp} \; r$ & $\dn$ & $\textit{r} \qquad \textit{otherwise}$   

\end{tabular}    

\end{center} 

\begin{center}

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

		$r\backslash_{rsimp} \, c$ & $\dn$ & $\rsimp \; (r\backslash_r \, c)$

	\end{tabular}

\end{center}

\begin{center}

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

$r \backslash_{rsimps} \; \; c\!::\!s $ & $\dn$ & $(r \backslash_{rsimp}\, c) \backslash_{rsimps}\, s$ \\

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

	\end{tabular}

\end{center}

\noindent

We do not define an r-regular expression version of $\blexersimp$,

as our proof does not depend on it.

Now we are ready to introduce how r-regular expressions allow

us to prove the size bound on bitcoded regular expressions.

\subsection{Using R-regular Expressions to Bound Bit-coded Regular Expressions}

Everything about the size of annotated regular expressions after the application

of function $\bsimp$ and $\backslash_{simps}$

can be calculated via the size of r-regular expressions after the application

of $\rsimp$ and $\backslash_{rsimps}$:

\begin{lemma}\label{sizeRelations}

	The following two equalities hold:

	\begin{itemize}

		\item

			$\asize{\bsimps \; a} = \rsize{\rsimp{ \rerase{a}}}$

		\item

			$\asize{\bderssimp{a}{s}} =  \rsize{\rderssimp{\rerase{a}}{s}}$