% Chapter Template

\chapter{Finiteness Bound} % Main chapter title

\label{ChapterFinite} 

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

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

%	SECTION ?

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

\section{preparatory properties for getting a finiteness bound}

Before we get to the proof that says the intermediate result of our lexer will

remain finitely bounded, which is an important efficiency/liveness guarantee,

we shall first develop a few preparatory properties and definitions to 

make the process of proving that a breeze.

We define rewriting relations for $\rrexp$s, which allows us to do the 

same trick as we did for the correctness proof,

but this time we will have stronger equalities established.

\subsection{"hrewrite" relation}

List of 1-step rewrite rules for regular expressions simplification without bitcodes:

\begin{center}

\begin{tabular}{lcl}

$r_1 \cdot \ZERO$ & $\rightarrow$ & $\ZERO$

\end{tabular}

\end{center}

And we define an "grewrite" relation that works on lists:

\begin{center}

\begin{tabular}{lcl}

$ \ZERO :: rs$ & $\rightarrow_g$ & $rs$

\end{tabular}

\end{center}

With these relations we prove

\begin{lemma}

$rs \rightarrow rs'  \implies \RALTS{rs} \rightarrow \RALTS{rs'}$

\end{lemma}

which enables us to prove "closed forms" equalities such as

\begin{lemma}

$\sflat{(r_1 \cdot r_2) \backslash s} = \RALTS{ (r_1 \backslash s) \cdot r_2 :: (\map (r_2 \backslash \_) (\vsuf{s}{r_1}))}$

\end{lemma}

But the most involved part of the above lemma is proving the following:

\begin{lemma}

$\bsimp{\RALTS{rs @ \RALTS{rs_1} @ rs'}} = \bsimp{\RALTS{rs @rs_1 @ rs'}} $ 

\end{lemma}

which is needed in proving things like 

\begin{lemma}

$r \rightarrow_f r'  \implies \rsimp{r} \rightarrow \rsimp{r'}$

\end{lemma}

Fortunately this is provable by induction on the list $rs$

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

%	SECTION 2

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

\section{Finiteness Property}

In this section let us describe our argument for why the size of the simplified

derivatives with the aggressive simplification function is finitely bounded.

 Suppose

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 \ACHAR{bs}{c} \rrbracket $ & $\dn$ & $1$\\

\end{tabular}

\end{center}

(TODO: COMPLETE this defn and for $rs$)

The size is based on a recursive function on the structure of the regex,

not the bitcodes.

Therefore we may as well talk about size of an annotated regular expression 

in their un-annotated form:

\begin{center}

$\asize(a) = \size(\erase(a))$. 

\end{center}

(TODO: turn equals to roughly equals)

But there is a minor nuisance here:

the erase function actually messes with the structure of the regular expression:

\begin{center}

\begin{tabular}{ccc}

$\erase(\AALTS{bs}{[]} )$ & $\dn$ & $\ZERO$\\

\end{tabular}

\end{center}

(TODO: complete this definition with singleton r in alts)

An alternative regular expression with an empty list of children

 is turned into an $\ZERO$ during the

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

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

(the $\erase$ function unfortunately does not preserve structure in the case of empty and singleton

$\ALTS$).

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{\AZERO}$ & $=$ & $\RZERO$\\

$\rerase{\ASEQ{bs}{r_1}{r_2}}$ & $=$ & $\RSEQ{\rerase{r_1}}{\rerase{r_2}}$\\

$\rerase{\AALTS{bs}{rs}}$ & $ =$ & $ \RALTS{rs}$

\end{tabular}

\end{center}

%TODO: FINISH definition of rerase

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$ & $=$ &  $\RALTS{map\; (\_ \backslash c) \;rs}$\\

(other clauses omitted)

\end{tabular}

\end{center}

Now that $\rrexp$s do not have bitcodes on them, we can do the 

duplicate removal without  an equivalence relation:

\begin{center}

\begin{tabular}{lcl}

$\rdistinct{r :: rs}{rset}$ & $=$ & $\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)

The reason why these definitions  mirror precisely the corresponding operations

on annotated regualar expressions is that we can calculate sizes more easily:

\begin{lemma}

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

\end{lemma}

This lemma says that the size of an r-erased regex is the same as the annotated regex.

this does not hold for plain $\rexp$s due to their ways of how alternatives are represented.

\begin{lemma}

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

\end{lemma}

Putting these two together we get a property that allows us to estimate the 

size of an annotated regular expression derivative using its un-annotated counterpart:

\begin{lemma}

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

\end{lemma}

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.

\begin{theorem}

For any regex $r$, $\exists N_r. \forall s. \; \llbracket{\bderssimp{r}{s}}\rrbracket \leq N_r$

\end{theorem}

\noindent

\begin{proof}

We prove this by induction on $r$. The base cases for $\AZERO$,

$\AONE \textit{bs}$ and $\ACHAR \textit{bs} c$ are straightforward. The interesting case is

for sequences of the form $\ASEQ{bs}{r_1}{r_2}$. In this case our induction

hypotheses state $\exists N_1. \forall s. \; \llbracket \bderssimp{r}{s} \rrbracket \leq N_1$ and

$\exists N_2. \forall s. \; \llbracket \bderssimp{r_2}{s} \rrbracket \leq N_2$. We can reason as follows

%

\begin{center}

\begin{tabular}{lcll}

& & $ \llbracket   \bderssimp{\ASEQ{bs}{r_1}{r_2} }{s} \rrbracket$\\

& $ = $ & $\llbracket bsimp\,(\textit{ALTs}\;bs\;(\ASEQ{nil}{\bderssimp{ r_1}{s}}{ r_2} ::

    [\bderssimp{ r_2}{s'} \;|\; s' \in \textit{Suffix}( r_1, s)]))\rrbracket $ & (1) \\

& $\leq$ &

    $\llbracket\textit{\distinctWith}\,((\ASEQ{nil}{\bderssimp{r_1}{s}}{r_2}$) ::

    [$\bderssimp{ r_2}{s'} \;|\; s' \in \textit{Suffix}( r_1, s)])\,\approx\;{}\rrbracket + 1 $ & (2) \\

& $\leq$ & $\llbracket\ASEQ{bs}{\bderssimp{ r_1}{s}}{r_2}\rrbracket +

             \llbracket\textit{distinctWith}\,[\bderssimp{r_2}{s'} \;|\; s' \in \textit{Suffix}( r_1, s)]\,\approx\;{}\rrbracket + 1 $ & (3) \\

& $\leq$ & $N_1 + \llbracket r_2\rrbracket + 2 +

      \llbracket \distinctWith\,[ \bderssimp{r_2}{s'} \;|\; s' \in \textit{Suffix}( r_1, s)] \,\approx\;\rrbracket$ & (4)\\

& $\leq$ & $N_1 + \llbracket r_2\rrbracket + 2 + l_{N_{2}} * N_{2}$ & (5)

\end{tabular}

\end{center}

\noindent

where in (1) the $\textit{Suffix}( r_1, s)$ are the all the suffixes of $s$ where $\bderssimp{ r_1}{s'}$ is nullable ($s'$ being a suffix of $s$).

The reason why we could write the derivatives of a sequence this way is described in section 2.

The term (2) is used to control (1). 

That is because one can obtain an overall

smaller regex list

by flattening it and removing $\ZERO$s first before applying $\distinctWith$ on it.

Section 3 is dedicated to its proof.

In (3) we know that  $\llbracket \ASEQ{bs}{(\bderssimp{ r_1}{s}}{r_2}\rrbracket$ is 

bounded by $N_1 + \llbracket{}r_2\rrbracket + 1$. In (5) we know the list comprehension contains only regular expressions of size smaller

than $N_2$. The list length after  $\distinctWith$ is bounded by a number, which we call $l_{N_2}$. It stands

for the number of distinct regular expressions smaller than $N_2$ (there can only be finitely many of them).

We reason similarly for  $\STAR$.\medskip

\end{proof}

What guarantee does this bound give us?

Whatever the regex is, it will not grow indefinitely.

Take our previous example $(a + aa)^*$ as an example:

\begin{center}

\begin{tabular}{@{}c@{\hspace{0mm}}c@{\hspace{0mm}}c@{}}

\begin{tikzpicture}

\begin{axis}[

    xlabel={number of $a$'s},

    x label style={at={(1.05,-0.05)}},

    ylabel={regex size},

    enlargelimits=false,

    xtick={0,5,...,30},

    xmax=33,

    ymax= 40,

    ytick={0,10,...,40},

    scaled ticks=false,

    axis lines=left,

    width=5cm,

    height=4cm, 

    legend entries={$(a + aa)^*$},  

    legend pos=north west,

    legend cell align=left]

\addplot[red,mark=*, mark options={fill=white}] table {a_aa_star.data};

\end{axis}

\end{tikzpicture}

\end{tabular}

\end{center}

We are able to limit the size of the regex $(a + aa)^*$'s derivatives

 with our simplification

rules very effectively.

%a few sample regular experessions' derivatives

%size change

%a*, aa*, aaa*, .....

%randomly generated regexes

\begin{center}

\begin{tabular}{@{}c@{\hspace{0mm}}c@{\hspace{0mm}}c@{}}

\begin{tikzpicture}

\begin{axis}[

    xlabel={number of $a$'s},

    x label style={at={(1.05,-0.05)}},

    ylabel={regex size},

    enlargelimits=false,

    xtick={0,5,...,30},

    xmax=33,

    ymax=1000,

    ytick={0,100,...,1000},

    scaled ticks=false,

    axis lines=left,

    width=5cm,

    height=4cm, 

    legend entries={regex1},  

    legend pos=north west,

    legend cell align=left]

\addplot[red,mark=*, mark options={fill=white}] table {regex1_size_change.data};

\end{axis}

\end{tikzpicture}

  &

\begin{tikzpicture}

\begin{axis}[

    xlabel={$n$},

    x label style={at={(1.05,-0.05)}},

    %ylabel={time in secs},

    enlargelimits=false,

    xtick={0,5,...,30},

    xmax=33,

    ymax=1000,

    ytick={0,100,...,1000},

    scaled ticks=false,

    axis lines=left,

    width=5cm,

    height=4cm, 

    legend entries={regex2},  

    legend pos=north west,

    legend cell align=left]

\addplot[blue,mark=*, mark options={fill=white}] table {regex2_size_change.data};

\end{axis}

\end{tikzpicture}

  &

\begin{tikzpicture}

\begin{axis}[

    xlabel={$n$},

    x label style={at={(1.05,-0.05)}},

    %ylabel={time in secs},

    enlargelimits=false,

    xtick={0,5,...,30},

    xmax=33,

    ymax=1000,

    ytick={0,100,...,1000},

    scaled ticks=false,

    axis lines=left,

    width=5cm,

    height=4cm, 

    legend entries={regex3},  

    legend pos=north west,

    legend cell align=left]

\addplot[cyan,mark=*, mark options={fill=white}] table {regex3_size_change.data};

\end{axis}

\end{tikzpicture}\\

\multicolumn{3}{c}{Graphs: size change of 3 randomly generated regexes $w.r.t.$ input string length.}

\end{tabular}    

\end{center}  

\noindent

 $(r_1 + r_2) \cdot r_3 \longrightarrow (r_1 \cdot r_3) + (r_2 \cdot r_3)$,

However, if we introduce them in our

setting we would lose the POSIX property of our calculated values. 

A simple example for this would be the regex $(a + a\cdot b)\cdot(b\cdot c + c)$.

If we split this regex up into $a\cdot(b\cdot c + c) + a\cdot b \cdot (b\cdot c + c)$, the lexer 

would give back $\Left(\Seq(\Char(a), \Left(\Char(b \cdot c))))$ instead of

what we want: $\Seq(\Right(ab), \Right(c))$. Unless we can store the structural information

in all the places where a transformation of the form $(r_1 + r_2)\cdot r \rightarrow r_1 \cdot r + r_2 \cdot r$

occurs, and apply them in the right order once we get 

a result of the "aggressively simplified" regex, it would be impossible to still get a $\POSIX$ value.

This is unlike the simplification we had before, where the rewriting rules 

such  as $\ONE \cdot r \rightsquigarrow r$, under which our lexer will give the same value.

We will discuss better

bounds in the last section of this chapter.\\[-6.5mm]

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

%	SECTION ??

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

\section{"Closed Forms" of regular expressions' derivatives w.r.t strings}

To embark on getting the "closed forms" of regexes, we first

define a few auxiliary definitions to make expressing them smoothly.

 \begin{center}  

 \begin{tabular}{ccc}

 $\sflataux{\AALTS{ }{r :: rs}}$ & $=$ & $\sflataux{r} @ rs$\\

$\sflataux{\AALTS{ }{[]}}$ & $ = $ & $ []$\\

$\sflataux r$ & $=$ & $ [r]$

\end{tabular}

\end{center}

The intuition behind $\sflataux{\_}$ is to break up nested regexes 

of the $(\ldots((r_1 + r_2) + r_3) + \ldots )$(left-associated) shape

into a more "balanced" list: $\AALTS{\_}{[r_1,\, r_2 ,\, r_3, \ldots]}$.

It will return the singleton list $[r]$ otherwise.

$\sflat{\_}$ works the same  as $\sflataux{\_}$, except that it keeps

the output type a regular expression, not a list:

 \begin{center} 

 \begin{tabular}{ccc}

 $\sflat{\AALTS{ }{r :: rs}}$ & $=$ & $\sflataux{r} @ rs$\\

$\sflat{\AALTS{ }{[]}}$ & $ = $ & $ \AALTS{ }{[]}$\\

$\sflat r$ & $=$ & $ [r]$

\end{tabular}

\end{center}

$\sflataux{\_}$  and $\sflat{\_}$ is only recursive in terms of the

 first element of the list of children of

an alternative regex ($\AALTS{ }{rs}$), and is purposefully built for  dealing with the regular expression

$r_1 \cdot r_2 \backslash s$.

With $\sflat{\_}$ and $\sflataux{\_}$ we make 

precise what  "closed forms" we have for the sequence derivatives and their simplifications,

in other words, how can we construct $(r_1 \cdot r_2) \backslash s$

and $\bderssimp{(r_1\cdot r_2)}{s}$,

if we are only allowed to use a combination of $r_1 \backslash s'$ ($\bderssimp{r_1}{s'}$)

and  $r_2 \backslash s'$ ($\bderssimp{r_2}{s'}$), where $s'$  ranges over 

the substring of $s$?

First let's look at a series of derivatives steps on a sequence 

regular expression,  (assuming) that each time the first

component of the sequence is always nullable):

\begin{center}

$r_1 \cdot r_2 \quad \longrightarrow_{\backslash c}  \quad   r_1  \backslash c \cdot r_2 + r_2 \backslash c \quad \longrightarrow_{\backslash c'} \quad (r_1 \backslash cc' \cdot r_2 + r_2 \backslash c') + r_2 \backslash cc' \longrightarrow_{\backslash c''} \quad$\\

$((r_1 \backslash cc'c'' \cdot r_2 + r_2 \backslash c'') + r_2 \backslash c'c'') + r_2 \backslash cc'c''   \longrightarrow_{\backslash c''} \quad

 \ldots$

\end{center}

%TODO: cite indian paper

Indianpaper have  come up with a slightly more formal way of putting the above process:

\begin{center}

$r_1 \cdot r_2 \backslash (c_1 :: c_2 ::\ldots c_n) \myequiv r_1 \backslash (c_1 :: c_2:: \ldots c_n) +

\delta(\nullable(r_1 \backslash (c_1 :: c_2 \ldots c_{n-1}) ), r_2 \backslash (c_n)) + \ldots

+ \delta (\nullable(r_1), r_2\backslash (c_1 :: c_2 ::\ldots c_n))$

\end{center}

where  $\delta(b, r)$ will produce $r$

if $b$ evaluates to true, 

and $\ZERO$ otherwise.

 But the $\myequiv$ sign in the above equation means language equivalence instead of syntactical

 equivalence. To make this intuition useful 

 for a formal proof, we need something

stronger than language equivalence.

With the help of $\sflat{\_}$ we can state the equation in Indianpaper

more rigorously:

\begin{lemma}

$\sflat{(r_1 \cdot r_2) \backslash s} = \RALTS{ (r_1 \backslash s) \cdot r_2 :: (\map (r_2 \backslash \_) (\vsuf{s}{r_1}))}$

\end{lemma}

The function $\vsuf{\_}{\_}$ is defined recursively on the structure of the string:

\begin{center}

\begin{tabular}{lcl}

$\vsuf{[]}{\_} $ & $=$ &  $[]$\\

$\vsuf{c::cs}{r_1}$ & $ =$ & $ \textit{if} (\rnullable{r_1}) \textit{then} \; (\vsuf{cs}{(\rder{c}{r_1})}) @ [c :: cs]$\\

                                     && $\textit{else} \; (\vsuf{cs}{(\rder{c}{r_1}) })  $

\end{tabular}

\end{center}                   

It takes into account which prefixes $s'$ of $s$ would make $r \backslash s'$ nullable,