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

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

\end{center}

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

	\item

		We have a set of equalities for this new datatype that enables one to

		rewrite $\rderssimp{r_1 \cdot r_2}{s}$ 

		and $\rderssimp{r^*}{s}$ (the most involved

		inductive cases)

		by a combinatioin of derivatives of their 

		children regular expressions ($r_1$, $r_2$, and $r$, respectively),

		which we call the \emph{Closed Forms}

		of the derivatives.

	\item

		The Closed Forms of the regular expressions

		are controlled by terms that

		are easier to deal with.

		Using inductive hypothesis, these terms

		are in turn bounded loosely

		by a large yet constant number.

\end{itemize}

We give details of these steps in the next sections.

The first step is to use 

$\textit{rrexp}$s,

something simpler than

annotated regular expressions. 

\section{the $\textit{rrexp}$ Datatype and Its Size Functions}

We first recap a bit about the new datatype

we defined in \ref{rrexpDef},

called $\textit{rrexp}$s.

We chose $\rrexp$ over 

the basic regular expressions

because it is more straightforward to tweak 

into the shape we want 

compared with an annotated regular expression.

We want to prove the size property about annotated regular expressions.

The size is 

written $\llbracket r\rrbracket$, whose intuitive definition is as below

\noindent

We first note that $\llbracket \_ \rrbracket$

is unaware of bitcodes, since 

it only counts the number of nodes

if we regard $r$ as a tree.

This suggests that if we define a new datatype that is similar to plain $\rexp$s,

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

			 \mid  \RCHAR{c}  

			 \mid  \RSEQ{r_1}{r_2}

			 \mid  \RALTS{rs}

			 \mid \RSTAR{r}        

\]

and define 

\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

we could calculate the size of annotated regular expressions in terms of

its un-annotated counterpart: 

\begin{lemma}

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

\end{lemma}

\begin{proof}

	By routine induction on the structure of $a$.

\end{proof}

\noindent

We call them \emph{r}-regular expressions:

we use

$\rrexp$ as its type name, so as to make a distinction  

with plain regular expressions.

In $\rrexp$ we throw away the bitcodes on the annotated regular expressions, 

but keep everything else intact.

To transform an annotated regular expression into an r-regular expression,

we use the function \emph{rerase}, written $\downarrow_r$. 

The $r$ in the subscript of $\downarrow$ is to 

differentiate with the $\downarrow$ for the $\erase$ operation.

Before we introduce more functions related to r-regular expressions,

we first give out the reason why we take all the trouble 

defining a new datatype in the first place.

\subsection{Motivation Behind a New Datatype}

The main difference between a plain regular expression

and an r-regular expression is that it can take

non-binary arguments for its alternative constructor.

This turned out to be necessary if we want our proofs to be

simple.

We initially started by using 

plain regular expressions and tried to prove

equalities like 

\begin{center}

	$\llbracket a \rrbracket = \llbracket a\downarrow \rrbracket_p$

\end{center}

and 

\[

	\llbracket a \backslash_{bsimps} s \rrbracket = 

	\llbracket a \downarrow \backslash_s s

\]

One might be able to prove that 

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

$\rrexp$ give the exact correspondence between an annotated regular expression

and its (r-)erased version:

This does not hold for plain $\rexp$s. 

		These operations are 

		almost identical to those of the annotated regular expressions,

		except that no bitcodes are attached.

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 at the current stage 

we can safely ignore them.

Similarly there is a size function for plain regular expressions:

\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

The idea of obatining a bound for $\llbracket \bderssimp{a}{s} \rrbracket$

is to get an equivalent form

of something like $\llbracket \bderssimp{a}{s}\rrbracket = f(a, s)$, where $f(a, s)$ 

is easier to estimate than $\llbracket \bderssimp{a}{s}\rrbracket$.

We notice that while it is not so clear how to obtain

a metamorphic representation of $\bderssimp{a}{s}$ (as we argued in chapter \ref{Bitcoded2},

not interleaving the application of the functions $\backslash$ and $\bsimp{\_}$ 

in the order as our lexer will result in the bit-codes dispensed differently),

it is possible to get an slightly different representation of the unlifted versions:

$ (\bderssimp{a}{s})_\downarrow = (\erase \; \bsimp{a \backslash s})_\downarrow$.

This suggest setting the bounding function $f(a, s)$ as 

$\llbracket  (a \backslash s)_\downarrow \rrbracket_p$, the plain size

of the erased annotated regular expression.

This requires the the regular expression accompanied by bitcodes

to have the same size as its plain counterpart after erasure:

\begin{center}

	$\asize{a} \stackrel{?}{=} \llbracket \erase(a)\rrbracket_p$. 

\end{center}

\noindent

But there is a minor nuisance: 

the erase function unavoidbly messes with the structure of the regular expression,

due to the discrepancy between annotated regular expression's $\sum$ constructor

and plain regular expression's $+$ constructor having different arity.

\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 list of children

 is turned into a $\ZERO$ during the

$\erase$ function, thereby changing the size and structure of the regex.

Therefore the equality in question does not hold.

These will likely be fixable if we really want to use plain $\rexp$s for dealing

with size, but we choose a more straightforward (or stupid) method by 

Similarly we could define the derivative  and simplification on 

$\rrexp$, which would be identical to those we defined for plain $\rexp$s in chapter1, 

except that now they can operate on alternatives taking multiple arguments.

\begin{center}

\begin{tabular}{lcr}

	$(\RALTS{rs})\; \backslash c$ & $\dn$ &  $\RALTS{\map\; (\_ \backslash c) \;rs}$\\

(other clauses omitted)

With the new $\rrexp$ datatype in place, one can define its size function,

which precisely mirrors that of the annotated regular expressions:

\end{tabular}

\end{center}

\noindent

\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

\subsection{Lexing Related Functions for $\rrexp$}

Everything else for $\rrexp$ will be precisely the same for annotated expressions,

except that they do not involve rectifying and augmenting bit-encoded tokenization information.

As expected, most functions are simpler, such as the derivative:

\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

The simplification function is simplified without annotation causing superficial differences.

Duplicate removal without  an equivalence relation:

\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

The prefix $r$ in front of $\rdistinct{}{}$ is used mainly to 

differentiate with $\textit{distinct}$, which is a built-in predicate

in Isabelle that says all the elements of a list are unique.

With $\textit{rdistinct}$ one can chain together all the other modules

of $\bsimp{\_}$ (removing the functionalities related to bit-sequences)

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

We omit these functions, as they are routine. Please refer to the formalisation

(in file BasicIdentities.thy) for the exact definition.

With $\rrexp$ the size caclulation of annotated regular expressions'

simplification and derivatives can be done by the size of their unlifted 

counterpart with the unlifted version of simplification and derivatives applied.

\begin{lemma}\label{sizeRelations}

	The following equalities hold:

	\begin{itemize}

		\item

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

		\item

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

	\end{itemize}

\end{lemma}

\noindent

In the following content, we will focus on $\rrexp$'s size bound.

We will piece together this bound and show the same bound for annotated regular 

expressions in the end.

Unless stated otherwise in this chapter all $\textit{rexp}$s without

 bitcodes are seen as $\rrexp$s.

 We also use $r_1 + r_2$ and $\RALTS{[r_1, r_2]}$ interchageably

 as the former suits people's intuitive way of stating a binary alternative

 regular expression.

%-----------------------------------

%	SECTION ?

%-----------------------------------

 \subsection{Finiteness Proof Using $\rrexp$s}

 Now that we have defined the $\rrexp$ datatype, and proven that its size changes

 w.r.t derivatives and simplifications mirrors precisely those of annotated regular expressions,

 we aim to bound the size of $r \backslash s$ for any $\rrexp$  $r$.

 Once we have a bound like: 

 \[

	 \llbracket r \backslash_{rsimp} s \rrbracket_r \leq N_r

 \]

 \noindent

 we could easily extend that to 

 \[

	 \llbracket a \backslash_{bsimps} s \rrbracket \leq N_r.

 \]

 \subsection{Roadmap to a Bound for $\textit{Rrexp}$}

The way we obtain the bound for $\rrexp$s is by two steps:

\begin{itemize}

	\item

		First, we rewrite $r\backslash s$ into something else that is easier

		to bound. This step is especially important for the inductive case 

		$r_1 \cdot r_2$ and $r^*$, where the derivative can grow and bloat in a wild way,

		but after simplification they will always be equal or smaller to a form consisting of an alternative

		list of regular expressions $f \; (g\; (\sum rs))$ with some functions applied to it, where each element will be distinct after the function application.

	\item

		Then, for such a sum  list of regular expressions $f\; (g\; (\sum rs))$, we can control its size

		by estimation, since $\distinctBy$ and $\flts$ are well-behaved and working together would only 

		reduce the size of a regular expression, not adding to it.

\end{itemize}

\section{Step One: Closed Forms}

		We transform the function application $\rderssimp{r}{s}$

		into an equivalent 

		form $f\; (g \; (\sum rs))$.

		The functions $f$ and $g$ can be anything from $\flts$, $\distinctBy$ and other helper functions from $\bsimp{\_}$.

		This way we get a different but equivalent way of expressing : $r\backslash s = f \; (g\; (\sum rs))$, we call the

		right hand side the "closed form" of $r\backslash s$.

\begin{quote}\it

	Claim: For regular expressions $r_1 \cdot r_2$, we claim that

	\begin{center}

		$ \rderssimp{r_1 \cdot r_2}{s} = 

	\rsimp{(\sum (r_1 \backslash s \cdot r_2 ) \; :: \;(\map \; \rderssimp{r2}{\_} \;(\vsuf{s}{r_1})))}$

	\end{center}

\end{quote}

\noindent

We explain in detail how we reached those claims.

\subsection{Basic Properties needed for Closed Forms}

\subsubsection{$\textit{rdistinct}$'s Deduplicates Successfully}

The $\textit{rdistinct}$ function, as its name suggests, will

remove duplicates in an \emph{r}$\textit{rexp}$ list, 

according to the accumulator

and leave only one of each different element in a list:

\begin{lemma}\label{rdistinctDoesTheJob}

	The function $\textit{rdistinct}$ satisfies the following

	properties:

	\begin{itemize}

		\item

			If $a \in acc$ then $a \notin (\rdistinct{rs}{acc})$.

		\item

			If list $rs'$ is the result of $\rdistinct{rs}{acc}$,