% 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 time complexity:

given a regular expression $r$, for any string $s$ 

our algorithm's internal data structure is finitely bounded.

Note that it is not immediately obvious that $\llbracket \bderssimp{r}{s} \rrbracket$ (the internal

data structure used in our $\blexer$)

is bounded by a constant $N_r$, where $N$ only depends on the regular expression

$r$, not the string $s$.

When doing a time complexity analysis of any 

lexer/parser based on Brzozowski derivatives, one needs to take into account that

not only the "derivative steps".

%TODO: get a grpah for internal data structure growing arbitrary large

To obtain such a proof, we need to 

\begin{itemize}

\item

Define an new datatype for regular expressions that makes it easy

to reason about the size of an annotated regular expression.

\item

A set of equalities for this new datatype that enables one to

rewrite $\bderssimp{r_1 \cdot r_2}{s}$ and $\bderssimp{r^*}{s}$ etc.

by their children regexes $r_1$, $r_2$, and $r$.

\item

Using those equalities to actually get those rewriting equations, which we call

"closed forms".

\item

Bound the closed forms, thereby bounding the original

$\blexersimp$'s internal data structures.

\end{itemize}

\section{the $\mathbf{r}$-rexp datatype and the size functions}

We have a size function for bitcoded regular expressions, written

$\llbracket r\rrbracket$, which counts the number of nodes if we regard $r$ as a tree

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

\noindent

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 

defining a new datatype that is similar to plain $\rexp$s but can take

non-binary arguments for its alternative constructor,

 which we call $\rrexp$ to denote

the difference between it and plain regular expressions. 

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

			 \mid  \RCHAR{c}  

			 \mid  \RSEQ{r_1}{r_2}

			 \mid  \RALTS{rs}

			 \mid \RSTAR{r}        

\]

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

but keep everything else intact.

It is similar to annotated regular expressions being $\erase$-ed, but with all its structure preserved

We denote the operation of erasing the bits and turning an annotated regular expression 

into an $\rrexp{}$ as $\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}

\noindent

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

and its (r-)erased version:

\begin{lemma}

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

\end{lemma}

\noindent

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

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}

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

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

		\item

		If $r \notin rs$, then $\rdistinct{rs}{acc} = \rdistinct{rs}{\{r\} \cup acc}$.

		\item

			Particularly, when $acc = \varnothing$ and $rs$ de-duplicated, we have\\

			\[ \rdistinct{rs}{\varnothing} = rs \]

	\end{itemize}

\end{lemma}

\begin{proof}

	The first half is by induction on $rs$. The second half is a corollary of the first.

\end{proof}

\noindent

The next property gives the condition for

when $\rdistinct{\_}{\_}$ becomes an identical mapping

for any prefix of an input list, in other words, when can 

we ``push out" the arguments of $\rdistinct{\_}{\_}$:

\begin{lemma}\label{distinctRdistinctAppend}

	If $\textit{isDistinct} \; rs_1$, and $rs_1 \cap acc = \varnothing$,

	then 

	\[\textit{rdistinct}\;  (rs_1 @ rsa)\;\, acc

	= rs_1@(\textit{rdistinct} rsa \; (acc \cup rs_1))\]

\end{lemma}

\noindent

In other words, it can be taken out and left untouched in the output.

\begin{proof}

By an induction on $rs_1$, where $rsa$ and $acc$ are allowed to be arbitrary.

\end{proof}

\noindent

$\rdistinct{}{}$ removes any element in anywhere of a list, if it

had appeared previously:

\begin{lemma}\label{distinctRemovesMiddle}

	The two properties hold if $r \in rs$:

	\begin{itemize}

		\item

			$\rdistinct{rs}{rset} = \rdistinct{(rs @ [r])}{rset}$\\

			and\\

			$\rdistinct{(ab :: rs @ [ab])}{rset'} = \rdistinct{(ab :: rs)}{rset'}$

		\item

			$\rdistinct{ (rs @ rs') }{rset} = \rdistinct{rs @ [r] @ rs'}{rset}$\\

			and\\

			$\rdistinct{(ab :: rs @ [ab] @ rs'')}{rset'} = 

			 \rdistinct{(ab :: rs @ rs'')}{rset'}$

	\end{itemize}

\end{lemma}

\noindent

\begin{proof}

By induction on $rs$. All other variables are allowed to be arbitrary.

The second half of the lemma requires the first half.

Note that for each half's two sub-propositions need to be proven concurrently,

so that the induction goes through.

\end{proof}

\noindent

This allows us to prove ``Idempotency" of $\rdistinct{}{}$ of some kind:

\begin{lemma}\label{rdistinctConcatGeneral}

	The following equalities involving multiple applications  of $\rdistinct{}{}$ hold:

	\begin{itemize}

		\item

			$\rdistinct{(rs @ rs')}{\varnothing} = \rdistinct{((\rdistinct{rs}{\varnothing})@ rs')}{\varnothing}$

		\item

			$\rdistinct{(rs @ rs')}{\varnothing} = \rdistinct{(\rdistinct{rs}{\varnothing} @ rs')}{\varnothing}$

		\item

			If $rset' \subseteq rset$, then $\rdistinct{rs}{rset} = 

			\rdistinct{(\rdistinct{rs}{rset'})}{rset}$. As a corollary

			of this,

		\item