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

\begin{center}

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

\end{center}

\noindent

is finitely bounded

\section{Formalising About Size}

In our lexer $\blexersimp$,

The regular expression is repeatedly being taken derivative of

and then simplified.

\begin{center}

\begin{tikzpicture}[scale=2,node distance=1.4cm,

                    every node/.style={minimum size=9mm}]

\node (r0)  {$r$};

\node (r1) [rectangle, draw=black, thick, right=of r0]{$r_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]{$r_{1s}$};

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

\node (r2) [rectangle, draw=black, thick,  right=of r1s]{$r_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=7mm]{$r_{2s}$};

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

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

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

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

\end{tikzpicture}

\end{center}

\noindent

As illustrated in the picture, 

We give a mechanised proof that after simplification 

the regular expression's size (the blue ones)

$\bderssimp{a}{s}$ will never exceed a constant $N_a$ for

a fixed $a$. 

it is polynomial on $\llbracket a \rrbracket$.

For example, Sulzmann and Lu's made claimed that their algorithm

with bitcodes and simplifications can lex in linear time with respect

to the input string. This assumes that each

derivative operation takes constant time. 

However, it turns out that on certain cases their lexer 

will have an indefinite size explosion, causing the running time 

of each derivative step to grow arbitrarily large.

Here in our proof we state that such explosions cannot happen 

with our simplification function.

\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

\begin{itemize}

\item

almost identical to those of the annotated regular expressions,

except that no bitcodes are attached.

\item

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

by a combinatioin of derivatives of their 

of the derivatives.

\item

by a large yet constant number.

\end{itemize}

We give details of these steps in the next sections.

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. 

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

			then $\textit{isDistinct} \; rs'$.

		\item

			$\rdistinct{rs}{acc} = rs - acc$

	\end{itemize}

\end{lemma}

\noindent

The predicate $\textit{isDistinct}$ is for testing

whether a list's elements are all unique. It is defined

recursively on the structure of a regular expression,

and we omit the precise definition here.

\begin{proof}

	The first part is by an induction on $rs$.

	The second and third part can be proven by using the 

	induction rules of $\rdistinct{\_}{\_}$.

\end{proof}

\noindent

$\rdistinct{\_}{\_}$ will cancel out all regular expression terms

that are in the accumulator, therefore prepending a list $rs_a$ with an arbitrary

list $rs$ whose elements are all from the accumulator, and then call $\rdistinct{\_}{\_}$

on the resulting list, the output will be as if we had called $\rdistinct{\_}{\_}$

without the prepending of $rs$:

\begin{lemma}

	The elements appearing in the accumulator will always be removed.

	More precisely,

	\begin{itemize}

		\item

			If $rs \subseteq rset$, then 

			$\rdistinct{rs@rsa }{acc} = \rdistinct{rsa }{acc}$.

		\item

			Furthermore, if $a \in rset$ and $\rdistinct{rs}{\{a\}} = []$,

			then $\rdistinct{(rs @ rs')}{rset} = \rdistinct{rs'}{rset}$

	\end{itemize}

\end{lemma}

\begin{proof}

	By induction on $rs$.

\end{proof}

\noindent

On the other hand, if an element $r$ does not appear in the input list waiting to be deduplicated,

then expanding the accumulator to include that element will not cause the output list to change:

\begin{lemma}

	The accumulator can be augmented to include elements not appearing in the input list,

	and the output will not change.	

	\begin{itemize}