%	SECTION 2

\section{Finiteness Property}

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

derivatives with the aggressive simplification function can be finitely bounded.

For convenience, we use a new datatype which we call $\textit{rrexp}$ to denote

the difference between it and annotated regular expressions. 

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

everything else intact.

It is similar to annotated regular expression being $\erase$ed, but with all its structure being intact

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

$\AALTS$.

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

into an $\rrexp$ as $\rerase$.

%TODO: definition of rerase

That we can bound the size of annotated regular expressions by 

$\rrexp$ is that the bitcodes grow linearly w.r.t the input string, and don't contribute to the structural size of 

an annotated regular expression:

$\rsize (\rerase a) = \asize a$

 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

(we omit the precise definition; ditto for lists $\llbracket r\!s\rrbracket$). For this we show that for every $r$

there exists a bound $N$

such that 

\begin{center}

$\forall s. \; \llbracket{\bderssimp r s}\rrbracket \leq N$

\end{center}

\noindent

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 \textit{bs} r_1 r_2$. In this case our induction

hypotheses state $\exists N_1. \forall s. \; \llbracket \bderssimp(r_1, 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\, \textit{bs} \, r_1 \,r_2),  s) \rrbracket$\\

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

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

& $\leq$ &

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

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

& $\leq$ & $\llbracket\ASEQ [] (\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}

% tell Chengsong about Indian paper of closed forms of derivatives

\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) since it we know that you 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 [] (\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

\noindent

Clearly we give in this finiteness argument (Step (5)) a very loose bound that is

far from the actual bound we can expect. We can do better than this, but this does not improve

the finiteness property we are proving. If we are interested in a polynomial bound,

one would hope to obtain a similar tight bound as for partial

derivatives introduced by Antimirov \cite{Antimirov95}. After all the idea with

 $\distinctWith$ is to maintain a ``set'' of alternatives (like the sets in

partial derivatives). Unfortunately to obtain the exact same bound would mean

we need to introduce simplifications, such as

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

which exist for partial derivatives. However, if we introduce them in our

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

bounds for future work.\\[-6.5mm]

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

There is a nice property about the compound regular expression 

$r_1 \cdot r_2$ in general,

that the derivatives of it against a string $s$ can be described by

the derivatives w.r.t $r_1$ and $r_2$ over substrings of $s$:

\begin{lemma}

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

\end{lemma}

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

%	SECTION 3

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

\section{interaction between $\distinctWith$ and $\flts$}

Note that it is not immediately obvious that 

$\llbracket \distinctWith (\flts \textit{rs}) = \phi \rrbracket   \leq \llbracket \distinctWith \textit{rs} = \phi \rrbracket  $