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

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

		\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

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

			(\rdistinct{rs}{\varnothing}) @ rs')}{rset}$. This

			gives another corollary use later:

		\item

			If $a \in rset$, then $\rdistinct{(rs @ rs')}{rset} = \rdistinct{

			(\rdistinct{(a :: rs)}{\varnothing} @ rs')}{rset} $,

	\end{itemize}

\end{lemma}

\begin{proof}

	By \ref{rdistinctDoesTheJob} and \ref{distinctRemovesMiddle}.

\end{proof}

\subsubsection{The Properties of $\backslash_r$, $\backslash_{rsimp}$, $\textit{Rflts}$ and $\textit{Rsimp}_{ALTS}$} 

We give in this subsection some properties of how $\backslash_r$, $\backslash_{rsimp}$, $\textit{Rflts}$ and $\textit{Rsimp}_{ALTS} $ interact with each other and with $@$, the concatenation operator.

These will be helpful in later closed form proofs, when

we want to transform the ways in which multiple functions involving

those are composed together

in interleaving derivative and  simplification steps.

When the function $\textit{Rflts}$ 

is applied to the concatenation of two lists, the output can be calculated by first applying the

functions on two lists separately, and then concatenating them together.

\begin{lemma}\label{rfltsProps}

	The function $\rflts$ has the below properties:\\

	\begin{itemize}

		\item

			$\rflts \; (rs_1 @ rs_2) = \rflts \; rs_1 @ \rflts \; rs_2$

		\item

			If $r \neq \RZERO$ and $\nexists rs_1. r = \RALTS{rs}_1$, then $\rflts \; (r::rs) = r :: \rflts \; rs$

		\item

			$\rflts \; (rs @ [\RZERO]) = \rflts \; rs$

		\item

			$\rflts \; (rs' @ [\RALTS{rs}]) = \rflts \; rs'@rs$

		\item

			$\rflts \; (rs @ [\RONE]) = \rflts \; rs @ [\RONE]$

		\item

			If $r \neq \RZERO$ and $\nexists rs'. r = \RALTS{rs'}$ then $\rflts \; (rs @ [r])

			= (\rflts \; rs) @ [r]$

		\item

			If $r = \RALTS{rs}$ and $r \in rs'$ then for all $r_1 \in rs. 

			r_1 \in \rflts \; rs'$.

		\item

			$\rflts \; (rs_a @ \RZERO :: rs_b) = \rflts \; (rs_a @ rs_b)$

	\end{itemize}

\end{lemma}

\noindent

\begin{proof}

	By induction on $rs_1$ in the first sub-lemma, and induction on $r$ in the second part,

	and induction on $rs$, $rs'$, $rs$, $rs'$, $rs_a$ in the third, fourth, fifth, sixth and 

	last sub-lemma.

\end{proof}

\subsubsection{The $RL$ Function: Language Interpretation of $\textit{Rrexp}$s}

Much like the definition of $L$ on plain regular expressions, one could also 

define the language interpretation of $\rrexp$s.

\begin{center}

\begin{tabular}{lcl}

$RL \; (\ZERO)$ & $\dn$ & $\phi$\\

$RL \; (\ONE)$ & $\dn$ & $\{[]\}$\\

$RL \; (c)$ & $\dn$ & $\{[c]\}$\\

$RL \; \sum rs$ & $\dn$ & $ \bigcup_{r \in rs} (RL \; r)$\\

$RL \; (r_1 \cdot r_2)$ & $\dn$ & $ RL \; (r_1) @ RL \; (r_2)$\\

$RL \; (r^*)$ & $\dn$ & $ (RL(r))^*$

\end{tabular}

\end{center}

\noindent

The main use of $RL$ is to establish some connections between $\rsimp{}$ 

and $\rnullable{}$:

\begin{lemma}

	The following properties hold:

	\begin{itemize}

		\item

			If $\rnullable{r}$, then $\rsimp{r} \neq \RZERO$.

		\item

			$\rnullable{r \backslash s} \quad $ if and only if $\quad \rnullable{\rderssimp{r}{s}}$.

	\end{itemize}

\end{lemma}

\begin{proof}

	The first part is by induction on $r$. 

	The second part is true because property 

	\[ RL \; r = RL \; (\rsimp{r})\] holds.

\end{proof}

\subsubsection{$\rsimp{}$ is Non-Increasing}

In this subsection, we prove that the function $\rsimp{}$ does not 

make the $\llbracket \rrbracket_r$ size increase.