10 %----------------------------------------------------------------------------------------

    10 

    11 %	SECTION 1

    12 %----------------------------------------------------------------------------------------

    13 

    14 \section{Properties of $\backslash c$}

    15 

    16 To have a clear idea of what we can and 

    17 need to prove about the algorithms involving

    18 Brzozowski's derivatives, there are a few 

    19 properties we need to be clear about .

    20 \subsection{function $\backslash c$ is not 1-to-1}

    21 \begin{center}

    22 The derivative $w.r.t$ character $c$ is not one-to-one.

    23 Formally,

    24 	$\exists r_1 \;r_2. r_1 \neq r_2 \mathit{and} r_1 \backslash c = r_2 \backslash c$

    25 \end{center}

    26 This property is trivially true for the

    27 character regex example:

    28 \begin{center}

    29 	$r_1 = e; \; r_2 = d;\; r_1 \backslash c = \ZERO = r_2 \backslash c$

    30 \end{center}

    31 But apart from the cases where the derivative

    32 output is $\ZERO$, are there non-trivial results

    33 of derivatives which contain strings?

    34 The answer is yes.

    35 For example,

    36 \begin{center}

    37 	Let $r_1 = a^*b\;\quad r_2 = (a\cdot a^*)\cdot b + b$.\\

    38 	where $a$ is not nullable.\\

    39 	$r_1 \backslash c = ((a \backslash c)\cdot a^*)\cdot c + b \backslash c$\\

    40 	$r_2 \backslash c = ((a \backslash c)\cdot a^*)\cdot c + b \backslash c$

    41 \end{center}

    42 We start with two syntactically different regexes,

    43 and end up with the same derivative result, which is

    44 a "meaningful" regex because it contains strings.

    45 We have rediscovered Arden's lemma:\\

    46 \begin{center}

    47 	$A^*B = A\cdot A^* \cdot B + B$

    48 \end{center}

    49 

    50 	

    54 \subsection{Subsection 1}

    14 \section{Specifications of Certain Functions to be Used}

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

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

    69 derivatives with the aggressive simplification function can be finitely bounded.

    77 derivatives with the aggressive simplification function is finitely bounded.

    70 

    78  Suppose

    71 For convenience, we use a new datatype which we call $\rrexp$ to denote

    79 we have a size function for bitcoded regular expressions, written

    72 the difference between it and annotated regular expressions. 

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

    81 

    82 \begin{center}

    83 \begin{tabular}{ccc}

    84 $\llbracket \ACHAR{bs}{c} \rrbracket $ & $\dn$ & $1$\\

    85 \end{tabular}

    86 \end{center}

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

    88 

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

    90 not the bitcodes.

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

    92 in their un-annotated form:

    93 \begin{center}

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

    95 \end{center}

    96 (TODO: turn equals to roughly equals)

    97 

    98 But there is a minor nuisance here:

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

   100 \begin{center}

   101 \begin{tabular}{ccc}

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

   103 \end{tabular}

   104 \end{center}

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

   106 

   107 An alternative regular expression with an empty list of children

   108  is turned into an $\ZERO$ during the

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

   110 These will likely be fixable if we really want to use plain $\rexp$s for dealing

   111 with size, but we choose a more straightforward (or stupid) method by 

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

   113 non-binary arguments for its alternative constructor,

   114  which we call $\rrexp$ to denote

   115 the difference between it and plain regular expressions. 

    87 \begin{tabular}{lcr}

   130 \begin{tabular}{lcl}

   122 A similar equation holds for annotated regular expressions' simplification

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

   123 and the plain regular expressions' simplification:

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

   138  Suppose

   181 

   139 we have a size function for bitcoded regular expressions, written

   182 \begin{theorem}

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

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

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

   184 \end{theorem}

   142 there exists a bound $N$

   143 such that 

   144 

   145 \begin{center}

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

   147 \end{center}

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

   344 far from the actual bound we can expect. 

   345 In our proof for the inductive case $r_1 \cdot r_2$, the dominant term in the bound

   346 is $l_{N_2} * N_2$, where $N_2$ is the bound we have for $\llbracket \bderssimp{r_2}{s} \rrbracket$.

   347 Given that $l_{N_2}$ is roughly the size $4^{N_2}$, the size bound $\llbracket \bderssimp{r_1 \cdot r_2}{s} \rrbracket$

   348 inflates the size bound of $\llbracket \bderssimp{r_2}{s} \rrbracket$ with the function

   349 $f(x) = x * 2^x$.

   350 This means the bound we have will surge up at least

   351 tower-exponentially with a linear increase of the depth.

   352 For a regex of depth $n$, the bound

   353 would be approximately $4^n$.

   354 %TODO: change this to tower exponential!

   355 

   356 We can do better than this, but this does not improve

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

   361 partial derivatives). 

   362 To obtain the exact same bound would mean

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

   365 which exist for partial derivatives. 

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

   366 

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

   367 However, if we introduce them in our

   201 

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

   202 

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

   203 

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

   204 %-----------------------------------

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

   205 %	SECTION ?

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

   206 %-----------------------------------

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

   207 \section{preparatory properties for getting a finiteness bound}

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

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

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

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

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

   210 we shall first develop a few preparatory properties and definitions to 

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

   211 make the process of proving that a breeze.

   378 We will discuss better

   212 

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

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

   380 

   214 same trick as we did for the correctness proof,

   381 

   215 but this time we will have stronger equalities established.

   382 

   216 \subsection{"hrewrite" relation}

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

   218 \begin{center}

   219 \begin{tabular}{lcl}

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

   221 \end{tabular}

   222 \end{center}

   223 

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

   225 \begin{center}

   226 \begin{tabular}{lcl}

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

   228 \end{tabular}

   229 \end{center}

   230 

   231 

   232 

   233 With these relations we prove

   234 \begin{lemma}

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

   236 \end{lemma}

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

   238 \begin{lemma}

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

   240 \end{lemma}

   241 

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

   243 \begin{lemma}

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

   245 \end{lemma}

   246 which is needed in proving things like 

   247 \begin{lemma}

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

   249 \end{lemma}

   250 .

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

   375 \section{a bound for the star regular expression}

   558 \section{A Bound for the Star Regular Expression}

   413 \end{center}

   596 \end{center}s

   455  $\rsimp{(r_1 + r_2)} = \rsimp{\RALTS{\hflataux{r_1} @ \hflataux{r_2}}}$

   638  $\rsimp{r_1 + r_2} = \rsimp{\RALTS{\hflataux{r_1} @ \hflataux{r_2}}}$

   483 for the convenience of a easier proof.

   666 for the convenience of an easier proof.

   484 How much can the regex $r^* \backslash s$ grow? As hinted earlier,

   667 How much can the regex $r^* \backslash s$ grow? 

   668 As  earlier graphs have shown,

   669 %TODO: reference that graph where size grows quickly

   487 but will eventually level off when the string $s$ is long enough,

   672 but will eventually level off when the string $s$ is long enough.

   488 as suggested by the finiteness bound proof.

   673 If they grow to a size exponential $w.r.t$ the original regex, our algorithm

   489 And unfortunately we have concrete examples

   674 would still be slow.

   675 And unfortunately, we have concrete examples

   493 size that is  exponential on the number $n$.

   679  size that is  exponential on the number $n$ 

   494 %TODO: give out a graph showing how the size of the regex grows and levels off at a size exponential to the original regex

   680 under our current simplification rules:

   495 

   681 %TODO: graph of a regex whose size increases exponentially.

   496 

   682 \begin{center}

   497 While the tight upper bound will definitely be a lot lower than 

   683 \begin{tikzpicture}

   498 the one we gave for the finiteness proof, 

   684     \begin{axis}[

   499 it will still be at least expoential, under our current simplification rules.

   685         height=0.5\textwidth,

   500 

   686         width=\textwidth,

   501 This suggests stronger simplifications that keep the tight bound polynomial.

   687         xlabel=number of a's,

   688         xtick={0,...,9},

   689         ylabel=maximum size,

   690         ymode=log,

   691        log basis y={2}

   692 ]

   693         \addplot[mark=*,blue] table {re-chengsong.data};

   694     \end{axis}

   695 \end{tikzpicture}

   696 \end{center}

   697 

   698 For convenience we use $(\oplus_{i=1}^{n} (\underbrace{a \ldots a}_{\text{i a's}})^*)^*$

   699 to express $(a ^ * + (aa) ^ * + (aaa) ^ * + \ldots + 

   700 (\underbrace{a \ldots a}_{\text{n a's}})^*$ in the below discussion.

   701 The exponential size is triggered by that the regex

   702 $\oplus_{i=1}^{n} (\underbrace{a \ldots a}_{\text{i a's}})^*$

   703 inside the $(\ldots) ^*$ having exponentially many

   704 different derivatives, despite those difference being minor.

   705 $(\oplus_{i=1}^{n} (\underbrace{a \ldots a}_{\text{i a's}})^*)^*\backslash \underbrace{a \ldots a}_{\text{m a's}}$

   706 will therefore contain the following terms (after flattening out all nested 

   707 alternatives):

   708 \begin{center}

   709 $(\oplus_{i = 1]{n}  (\underbrace{a \ldots a}_{\text{((i - (m' \% i))\%i) a's}})\cdot  (\underbrace{a \ldots a}_{\text{i a's}})^* })\cdot (\oplus_{i=1}^{n} (\underbrace{a \ldots a}_{\text{i a's}})^*)$\\

   710 $(1 \leq m' \leq m )$

   711 \end{center}

   712 These terms are distinct for $m' \leq L.C.M.(1, \ldots, n)$ (will be explained in appendix).

   713  With each new input character taking the derivative against the intermediate result, more and more such distinct

   714  terms will accumulate, 

   715 until the length reaches $L.C.M.(1, \ldots, n)$.

   716 $\textit{distinctBy}$ will not be able to de-duplicate any two of these terms 

   717 $(\oplus_{i = 1}^{n}  (\underbrace{a \ldots a}_{\text{((i - (m' \% i))\%i) a's}})\cdot  (\underbrace{a \ldots a}_{\text{i a's}})^* )\cdot (\oplus_{i=1}^{n} (\underbrace{a \ldots a}_{\text{i a's}})^*)^*$\\

   718 

   719 $(\oplus_{i = 1}^{n}  (\underbrace{a \ldots a}_{\text{((i - (m'' \% i))\%i) a's}})\cdot  (\underbrace{a \ldots a}_{\text{i a's}})^* )\cdot (\oplus_{i=1}^{n} (\underbrace{a \ldots a}_{\text{i a's}})^*)^*$\\

   720  where $m' \neq m''$ \\

   721  as they are slightly different.

   722  This means that with our current simplification methods,

   723  we will not be able to control the derivative so that

   724  $\llbracket \bderssimp{r}{s} \rrbracket$ stays polynomial %\leq O((\llbracket r\rrbacket)^c)$

   725  as there are already exponentially many terms.

   726  These terms are similar in the sense that the head of those terms

   727  are all consisted of sub-terms of the form: 

   728  $(\underbrace{a \ldots a}_{\text{j a's}})\cdot  (\underbrace{a \ldots a}_{\text{i a's}})^* $.

   729  For  $\oplus_{i=1}^{n} (\underbrace{a \ldots a}_{\text{i a's}})^*$, there will be at most

   730  $n * (n + 1) / 2$ such terms. 

   731  For example, $(a^* + (aa)^* + (aaa)^*) ^*$'s derivatives

   732  can be described by 6 terms:

   733  $a^*$, $a\cdot (aa)^*$, $ (aa)^*$, 

   734  $aa \cdot (aaa)^*$, $a \cdot (aaa)^*$, and $(aaa)^*$.

   735 The total number of different "head terms",  $n * (n + 1) / 2$,

   736  is proportional to the number of characters in the regex 

   737 $(\oplus_{i=1}^{n} (\underbrace{a \ldots a}_{\text{i a's}})^*)^*$.

   738 This suggests a slightly different notion of size, which we call the 

   739 alphabetic width:

   740 %TODO:

   741 (TODO: Alphabetic width def.)

   742 

   743  

   744 Antimirov\parencite{Antimirov95} has proven that 

   745 $\textit{PDER}_{UNIV}(r) \leq \textit{awidth}(r)$.

   746 where $\textit{PDER}_{UNIV}(r)$ is a set of all possible subterms

   747 created by doing derivatives of $r$ against all possible strings.

   748 If we can make sure that at any moment in our lexing algorithm our 

   749 intermediate result hold at most one copy of each of the 

   750 subterms then we can get the same bound as Antimirov's.

   751 This leads to the algorithm in the next section.

   506 \section{A Stronger Version of Simplification}

   756 \section{A Stronger Version of Simplification Inspired by Antimirov}