% 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 guarantee in terms of size: 

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

our algorithm $\blexersimp$'s internal annotated regular expression 

size  is finitely bounded

by a constant $N_a$ that only depends on $a$:

\begin{center}

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

\end{center}

\noindent

where the size of an annotated regular expression is defined

in terms of the number of nodes in its tree structure:

\begin{center}

	\begin{tabular}{ccc}

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

We believe this size formalisation 

of the algorithm is important in our context, because 

\begin{itemize}

	\item

		It is a stepping stone towards an ``absence of catastrophic-backtracking''

		guarantee. The next step would be to refine the bound $N_a$ so that it

		is polynomial on $\llbracket a\rrbracket$.

	\item

		The size bound proof gives us a higher confidence that

		our simplification algorithm $\simp$ does not ``mis-behave''

		like $\simpsulz$ does.

		The bound is universal, which is an advantage over work which 

		only gives empirical evidence on some test cases.

\end{itemize}

\section{Formalising About Size}

\noindent

In our lexer $\blexersimp$,

The regular expression is repeatedly being taken derivative of

and then simplified.

\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=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, a regular expression might grow a bit,

but simplification always takes care that 

it stays small.

This intuition is depicted by the relative size

change between the black and blue nodes:

After $\simp$ the node always shrinks.

Our proof says that all the blue nodes

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

\noindent

Sulzmann and Lu's assumed something similar about 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

That is, on certain cases their lexer 

will have an indefinite size explosion, causing the running time 

of each derivative step to grow arbitrarily large (for example 

in \ref{SulzmannLuLexerTime}).

The reason they made this mistake was that

they tested out the run time of their

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

and generalised to all cases, which

cannot happen with our mecahnised proof.\\

We give details of the proof in the next sections.

\subsection{Overview of the Proof}

Here is a bird's eye view of how the proof of finiteness works,

which involves three steps:

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

		a very brief introduction to in chapter \ref{Bitcoded2}.

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

		annotated regular expressions except that they are unaware

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

		annotated regular expressions.

	\item

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

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

		written in the derivatives of their children regular 

		expressions.

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

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

	\item

		We estimate $\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 and Its Lexing-Related Functions}

The first step is to define 

$\textit{rrexp}$s.

They are without bitcodes,

allowing a much simpler 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 account when we wish to tackle the runtime comlexity.

But for the sake of the structural size 

we can safely ignore them.\\

To recapitulate, 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.

\[			\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}{ccc}

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

Adding $r$ as subscript will be used in 

other operations as well.\\

The transformation from an annotated regular expression

to an r-regular expression is straightforward.

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

\noindent

$\textit{Rerase}$ throws away the bitcodes 

on the annotated regular expressions, 

but keeps everything else intact.

Therefore it does not change the size

of an annotated regular expression:

\begin{lemma}\label{rsizeAsize}

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

\end{lemma}

\begin{proof}

	By routine structural induction on $a$.

\end{proof}

\noindent

\subsection{Motivation Behind a New Datatype}

The reason we take all the trouble 

defining a new datatype is that $\erase$ makes things harder.

We initially started by using 

plain regular expressions and tried to prove

the lemma \ref{rsizeAsize},

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

annotated regular expression.

The $+$ constructor

of basic regular expressions is binary whereas $\sum$ 

takes a list, and one has to convert between them:

\begin{center}

	\begin{tabular}{ccc}

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

An alternative regular expression with an empty argument list

will be turned into a $\ZERO$.

The singleton alternative $\sum [r]$ would have $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 expressions, adding unnecessary 

complexities to the size bound proof.\\

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

in the usual way,

\begin{center}

	\begin{tabular}{ccc}

		$\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 = \llbracket a_\downarrow \rrbracket_p$

\end{center}

does not hold.

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{Lexing Related Functions for $\rrexp$ such as $\backslash_r$, $\rdistincts$, and $\rsimp$}

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 becomes simpler:\\

\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

Similarly, $\distinctBy$ does not need 

a function checking equivalence because

there are no bit annotations causing superficial differences

between syntactically equal terms.

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

and the flatten function for $\rrexp$s:

 \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

one can chain together all the other modules

such as $\rsimpalts$:

\begin{center}

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

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

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

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

\end{tabular}    

\end{center}  

\noindent

and $\rsimpseq$:

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