532
+ − 1 % Chapter Template
+ − 2
+ − 3 \chapter{Finiteness Bound} % Main chapter title
+ − 4
+ − 5 \label{Finite}
+ − 6 % In Chapter 4 \ref{Chapter4} we give the second guarantee
+ − 7 %of our bitcoded algorithm, that is a finite bound on the size of any
+ − 8 %regex's derivatives.
+ − 9
576
+ − 10 In this chapter we give a guarantee in terms of size:
590
+ − 11 given an annotated regular expression $a$, for any string $s$
+ − 12 our algorithm $\blexersimp$'s internal annotated regular expression
+ − 13 size is finitely bounded
+ − 14 by a constant $N_a$ that only depends on $a$:
576
+ − 15 \begin{center}
593
+ − 16 $\llbracket \bderssimp{a}{s} \rrbracket \leq N_a$
576
+ − 17 \end{center}
+ − 18 \noindent
577
+ − 19 where the size of an annotated regular expression is defined
+ − 20 in terms of the number of nodes in its tree structure:
+ − 21 \begin{center}
593
+ − 22 \begin{tabular}{ccc}
+ − 23 $\llbracket _{bs}\ONE \rrbracket$ & $\dn$ & $1$\\
+ − 24 $\llbracket \ZERO \rrbracket$ & $\dn$ & $1$ \\
+ − 25 $\llbracket _{bs} r_1 \cdot r_2 \rrbracket$ & $\dn$ & $\llbracket r_1 \rrbracket + \llbracket r_2 \rrbracket + 1$\\
+ − 26 $\llbracket _{bs}\mathbf{c} \rrbracket $ & $\dn$ & $1$\\
+ − 27 $\llbracket _{bs}\sum as \rrbracket $ & $\dn$ & $\map \; (\llbracket \_ \rrbracket)\; as + 1$\\
+ − 28 $\llbracket _{bs} a^* \rrbracket $ & $\dn$ & $\llbracket a \rrbracket + 1$.
+ − 29 \end{tabular}
577
+ − 30 \end{center}
590
+ − 31 We believe this size formalisation
+ − 32 of the algorithm is important in our context, because
+ − 33 \begin{itemize}
+ − 34 \item
+ − 35 It is a stepping stone towards an ``absence of catastrophic-backtracking''
+ − 36 guarantee. The next step would be to refine the bound $N_a$ so that it
+ − 37 is polynomial on $\llbracket a\rrbracket$.
+ − 38 \item
+ − 39 The size bound proof gives us a higher confidence that
+ − 40 our simplification algorithm $\simp$ does not ``mis-behave''
+ − 41 like $\simpsulz$ does.
+ − 42 The bound is universal, which is an advantage over work which
+ − 43 only gives empirical evidence on some test cases.
+ − 44 \end{itemize}
576
+ − 45 \section{Formalising About Size}
577
+ − 46 \noindent
576
+ − 47 In our lexer $\blexersimp$,
+ − 48 The regular expression is repeatedly being taken derivative of
+ − 49 and then simplified.
590
+ − 50 \begin{figure}[H]
593
+ − 51 \begin{tikzpicture}[scale=2,
+ − 52 every node/.style={minimum size=11mm},
+ − 53 ->,>=stealth',shorten >=1pt,auto,thick
+ − 54 ]
+ − 55 \node (r0) [rectangle, draw=black, thick, minimum size = 5mm, draw=blue] {$a$};
+ − 56 \node (r1) [rectangle, draw=black, thick, right=of r0, minimum size = 7mm]{$a_1$};
+ − 57 \draw[->,line width=0.2mm](r0)--(r1) node[above,midway] {$\backslash c_1$};
590
+ − 58
593
+ − 59 \node (r1s) [rectangle, draw=blue, thick, right=of r1, minimum size=6mm]{$a_{1s}$};
+ − 60 \draw[->, line width=0.2mm](r1)--(r1s) node[above, midway] {$\simp$};
590
+ − 61
593
+ − 62 \node (r2) [rectangle, draw=black, thick, right=of r1s, minimum size = 12mm]{$a_2$};
+ − 63 \draw[->,line width=0.2mm](r1s)--(r2) node[above,midway] {$\backslash c_2$};
590
+ − 64
593
+ − 65 \node (r2s) [rectangle, draw = blue, thick, right=of r2,minimum size=6mm]{$a_{2s}$};
+ − 66 \draw[->,line width=0.2mm](r2)--(r2s) node[above,midway] {$\simp$};
590
+ − 67
593
+ − 68 \node (rns) [rectangle, draw = blue, thick, right=of r2s,minimum size=6mm]{$a_{ns}$};
+ − 69 \draw[->,line width=0.2mm, dashed](r2s)--(rns) node[above,midway] {$\backslash \ldots$};
590
+ − 70
593
+ − 71 \node (v) [circle, thick, draw, right=of rns, minimum size=6mm, right=1.7cm]{$v$};
+ − 72 \draw[->, line width=0.2mm](rns)--(v) node[above, midway] {\bmkeps} node [below, midway] {\decode};
+ − 73 \end{tikzpicture}
+ − 74 \caption{Regular expression size change during our $\blexersimp$ algorithm}\label{simpShrinks}
590
+ − 75 \end{figure}
576
+ − 76 \noindent
590
+ − 77 Each time
+ − 78 a derivative is taken, a regular expression might grow a bit,
+ − 79 but simplification always takes care that
+ − 80 it stays small.
577
+ − 81 This intuition is depicted by the relative size
590
+ − 82 change between the black and blue nodes:
+ − 83 After $\simp$ the node always shrinks.
+ − 84 Our proof says that all the blue nodes
+ − 85 stay below a size bound $N_a$ determined by $a$.
576
+ − 86
590
+ − 87 \noindent
+ − 88 Sulzmann and Lu's assumed something similar about their algorithm,
+ − 89 though in fact their algorithm's size might be better depicted by the following graph:
+ − 90 \begin{figure}[H]
593
+ − 91 \begin{tikzpicture}[scale=2,
+ − 92 every node/.style={minimum size=11mm},
+ − 93 ->,>=stealth',shorten >=1pt,auto,thick
+ − 94 ]
+ − 95 \node (r0) [rectangle, draw=black, thick, minimum size = 5mm, draw=blue] {$a$};
+ − 96 \node (r1) [rectangle, draw=black, thick, right=of r0, minimum size = 7mm]{$a_1$};
+ − 97 \draw[->,line width=0.2mm](r0)--(r1) node[above,midway] {$\backslash c_1$};
590
+ − 98
593
+ − 99 \node (r1s) [rectangle, draw=blue, thick, right=of r1, minimum size=7mm]{$a_{1s}$};
+ − 100 \draw[->, line width=0.2mm](r1)--(r1s) node[above, midway] {$\simp'$};
590
+ − 101
593
+ − 102 \node (r2) [rectangle, draw=black, thick, right=of r1s, minimum size = 17mm]{$a_2$};
+ − 103 \draw[->,line width=0.2mm](r1s)--(r2) node[above,midway] {$\backslash c_2$};
590
+ − 104
593
+ − 105 \node (r2s) [rectangle, draw = blue, thick, right=of r2,minimum size=14mm]{$a_{2s}$};
+ − 106 \draw[->,line width=0.2mm](r2)--(r2s) node[above,midway] {$\simp'$};
590
+ − 107
593
+ − 108 \node (r3) [rectangle, draw = black, thick, right= of r2s, minimum size = 22mm]{$a_3$};
+ − 109 \draw[->,line width=0.2mm](r2s)--(r3) node[above,midway] {$\backslash c_3$};
590
+ − 110
593
+ − 111 \node (rns) [right = of r3, draw=blue, minimum size = 20mm]{$a_{3s}$};
+ − 112 \draw[->,line width=0.2mm] (r3)--(rns) node [above, midway] {$\simp'$};
590
+ − 113
593
+ − 114 \node (rnn) [right = of rns, minimum size = 1mm]{};
+ − 115 \draw[->, dashed] (rns)--(rnn) node [above, midway] {$\ldots$};
590
+ − 116
593
+ − 117 \end{tikzpicture}
+ − 118 \caption{Regular expression size change during our $\blexersimp$ algorithm}\label{sulzShrinks}
590
+ − 119 \end{figure}
+ − 120 \noindent
+ − 121 That is, on certain cases their lexer
576
+ − 122 will have an indefinite size explosion, causing the running time
590
+ − 123 of each derivative step to grow arbitrarily large (for example
+ − 124 in \ref{SulzmannLuLexerTime}).
+ − 125 The reason they made this mistake was that
+ − 126 they tested out the run time of their
+ − 127 lexer on particular examples such as $(a+b+ab)^*$
+ − 128 and generalised to all cases, which
+ − 129 cannot happen with our mecahnised proof.\\
+ − 130 We give details of the proof in the next sections.
+ − 131
577
+ − 132 \subsection{Overview of the Proof}
+ − 133 Here is a bird's eye view of how the proof of finiteness works,
+ − 134 which involves three steps:
593
+ − 135 \begin{figure}[H]
+ − 136 \begin{tikzpicture}[scale=1,font=\bf,
+ − 137 node/.style={
+ − 138 rectangle,rounded corners=3mm,
+ − 139 ultra thick,draw=black!50,minimum height=18mm,
+ − 140 minimum width=20mm,
+ − 141 top color=white,bottom color=black!20}]
543
+ − 142
+ − 143
593
+ − 144 \node (0) at (-5,0)
+ − 145 [node, text width=1.8cm, text centered]
+ − 146 {$\llbracket \bderssimp{a}{s} \rrbracket$};
+ − 147 \node (A) at (0,0)
+ − 148 [node,text width=1.6cm, text centered]
+ − 149 {$\llbracket \rderssimp{r}{s} \rrbracket_r$};
+ − 150 \node (B) at (3,0)
+ − 151 [node,text width=3.0cm, anchor=west, minimum width = 40mm]
+ − 152 {$\llbracket \textit{ClosedForm}(r, s)\rrbracket_r$};
+ − 153 \node (C) at (9.5,0) [node, minimum width=10mm] {$N_r$};
+ − 154
+ − 155 \draw [->,line width=0.5mm] (0) --
+ − 156 node [above,pos=0.45] {=} (A) node [below, pos = 0.45] {$(r = a \downarrow_r)$} (A);
+ − 157 \draw [->,line width=0.5mm] (A) --
+ − 158 node [above,pos=0.35] {$\quad =\ldots=$} (B);
+ − 159 \draw [->,line width=0.5mm] (B) --
+ − 160 node [above,pos=0.35] {$\quad \leq \ldots \leq$} (C);
+ − 161 \end{tikzpicture}
+ − 162 %\caption{
+ − 163 \end{figure}
576
+ − 164 \noindent
577
+ − 165 We explain the steps one by one:
532
+ − 166 \begin{itemize}
590
+ − 167 \item
+ − 168 We first introduce the operations such as
+ − 169 derivatives, simplification, size calculation, etc.
+ − 170 associated with $\rrexp$s, which we have given
+ − 171 a very brief introduction to in chapter \ref{Bitcoded2}.
593
+ − 172 The operations on $\rrexp$s are identical to those on
+ − 173 annotated regular expressions except that they are unaware
+ − 174 of bitcodes. This means that all proofs about size of $\rrexp$s will apply to
+ − 175 annotated regular expressions.
590
+ − 176 \item
593
+ − 177 We prove that $\rderssimp{r}{s} = \textit{ClosedForm}(r, s)$,
+ − 178 where $\textit{ClosedForm}(r, s)$ is entirely
+ − 179 written in the derivatives of their children regular
+ − 180 expressions.
+ − 181 We call the right-hand-side the \emph{Closed Form}
+ − 182 of the derivative $\rderssimp{r}{s}$.
590
+ − 183 \item
593
+ − 184 We estimate $\llbracket \textit{ClosedForm}(r, s) \rrbracket_r$.
+ − 185 The key observation is that $\distinctBy$'s output is
+ − 186 a list with a constant length bound.
532
+ − 187 \end{itemize}
594
+ − 188 We will expand on these steps in the next sections.\\
532
+ − 189
593
+ − 190 \section{The $\textit{Rrexp}$ Datatype and Its Lexing-Related Functions}
594
+ − 191 The first step is to define
+ − 192 $\textit{rrexp}$s.
+ − 193 They are without bitcodes,
+ − 194 allowing a much simpler size bound proof.
+ − 195 Of course, the bits which encode the lexing information
+ − 196 would grow linearly with respect
+ − 197 to the input, which should be taken into account when we wish to tackle the runtime comlexity.
+ − 198 But for the sake of the structural size
+ − 199 we can safely ignore them.\\
+ − 200 To recapitulate, the datatype
+ − 201 definition of the $\rrexp$, called
593
+ − 202 \emph{r-regular expressions},
594
+ − 203 was initially defined in \ref{rrexpDef}.
+ − 204 The reason for the prefix $r$ is
593
+ − 205 to make a distinction
594
+ − 206 with basic regular expressions.
576
+ − 207 \[ \rrexp ::= \RZERO \mid \RONE
593
+ − 208 \mid \RCHAR{c}
+ − 209 \mid \RSEQ{r_1}{r_2}
+ − 210 \mid \RALTS{rs}
+ − 211 \mid \RSTAR{r}
576
+ − 212 \]
593
+ − 213 The size of an r-regular expression is
+ − 214 written $\llbracket r\rrbracket_r$,
+ − 215 whose definition mirrors that of an annotated regular expression.
576
+ − 216 \begin{center}
593
+ − 217 \begin{tabular}{ccc}
+ − 218 $\llbracket _{bs}\ONE \rrbracket_r$ & $\dn$ & $1$\\
+ − 219 $\llbracket \ZERO \rrbracket_r$ & $\dn$ & $1$ \\
+ − 220 $\llbracket _{bs} r_1 \cdot r_2 \rrbracket_r$ & $\dn$ & $\llbracket r_1 \rrbracket_r + \llbracket r_2 \rrbracket_r + 1$\\
+ − 221 $\llbracket _{bs}\mathbf{c} \rrbracket_r $ & $\dn$ & $1$\\
+ − 222 $\llbracket _{bs}\sum as \rrbracket_r $ & $\dn$ & $\map \; (\llbracket \_ \rrbracket_r)\; as + 1$\\
+ − 223 $\llbracket _{bs} a^* \rrbracket_r $ & $\dn$ & $\llbracket a \rrbracket_r + 1$.
+ − 224 \end{tabular}
576
+ − 225 \end{center}
+ − 226 \noindent
593
+ − 227 The $r$ in the subscript of $\llbracket \rrbracket_r$ is to
+ − 228 differentiate with the same operation for annotated regular expressions.
+ − 229 Adding $r$ as subscript will be used in
594
+ − 230 other operations as well.\\
593
+ − 231 The transformation from an annotated regular expression
+ − 232 to an r-regular expression is straightforward.
+ − 233 \begin{center}
+ − 234 \begin{tabular}{lcl}
+ − 235 $\rerase{\ZERO}$ & $\dn$ & $\RZERO$\\
+ − 236 $\rerase{_{bs}\ONE}$ & $\dn$ & $\RONE$\\
+ − 237 $\rerase{_{bs}\mathbf{c}}$ & $\dn$ & $\RCHAR{c}$\\
+ − 238 $\rerase{_{bs}r_1\cdot r_2}$ & $\dn$ & $\RSEQ{\rerase{r_1}}{\rerase{r_2}}$\\
+ − 239 $\rerase{_{bs}\sum as}$ & $\dn$ & $\RALTS{\map \; \rerase{\_} \; as}$\\
+ − 240 $\rerase{_{bs} a ^*}$ & $\dn$ & $\rerase{a} ^*$
+ − 241 \end{tabular}
+ − 242 \end{center}
576
+ − 243 \noindent
594
+ − 244 $\textit{Rerase}$ throws away the bitcodes
+ − 245 on the annotated regular expressions,
593
+ − 246 but keeps everything else intact.
594
+ − 247 Therefore it does not change the size
+ − 248 of an annotated regular expression:
+ − 249 \begin{lemma}\label{rsizeAsize}
593
+ − 250 $\rsize{\rerase a} = \asize a$
+ − 251 \end{lemma}
+ − 252 \begin{proof}
+ − 253 By routine structural induction on $a$.
+ − 254 \end{proof}
+ − 255 \noindent
594
+ − 256
576
+ − 257 \subsection{Motivation Behind a New Datatype}
594
+ − 258 The reason we take all the trouble
+ − 259 defining a new datatype is that $\erase$ makes things harder.
576
+ − 260 We initially started by using
+ − 261 plain regular expressions and tried to prove
594
+ − 262 the lemma \ref{rsizeAsize},
+ − 263 however the $\erase$ function unavoidbly messes with the structure of the
+ − 264 annotated regular expression.
+ − 265 The $+$ constructor
+ − 266 of basic regular expressions is binary whereas $\sum$
+ − 267 takes a list, and one has to convert between them:
576
+ − 268 \begin{center}
594
+ − 269 \begin{tabular}{ccc}
+ − 270 $\erase \; _{bs}\sum [] $ & $\dn$ & $\ZERO$\\
+ − 271 $\erase \; _{bs}\sum [a]$ & $\dn$ & $a$\\
+ − 272 $\erase \; _{bs}\sum a :: as$ & $\dn$ & $a + (\erase \; _{[]} \sum as)\quad \text{if $as$ length over 1}$
+ − 273 \end{tabular}
576
+ − 274 \end{center}
594
+ − 275 \noindent
+ − 276 An alternative regular expression with an empty argument list
+ − 277 will be turned into a $\ZERO$.
+ − 278 The singleton alternative $\sum [r]$ would have $r$ during the
+ − 279 $\erase$ function.
+ − 280 The annotated regular expression $\sum[a, b, c]$ would turn into
+ − 281 $(a+(b+c))$.
+ − 282 All these operations change the size and structure of
+ − 283 an annotated regular expressions, adding unnecessary
+ − 284 complexities to the size bound proof.\\
+ − 285 For example, if we define the size of a basic regular expression
+ − 286 in the usual way,
543
+ − 287 \begin{center}
593
+ − 288 \begin{tabular}{ccc}
+ − 289 $\llbracket \ONE \rrbracket_p$ & $\dn$ & $1$\\
+ − 290 $\llbracket \ZERO \rrbracket_p$ & $\dn$ & $1$ \\
+ − 291 $\llbracket r_1 \cdot r_2 \rrbracket_p$ & $\dn$ & $\llbracket r_1 \rrbracket_p + \llbracket r_2 \rrbracket_p + 1$\\
+ − 292 $\llbracket \mathbf{c} \rrbracket_p $ & $\dn$ & $1$\\
+ − 293 $\llbracket r_1 \cdot r_2 \rrbracket_p $ & $\dn$ & $\llbracket r_1 \rrbracket_p \; + \llbracket r_2 \rrbracket_p + 1$\\
+ − 294 $\llbracket a^* \rrbracket_p $ & $\dn$ & $\llbracket a \rrbracket_p + 1$
+ − 295 \end{tabular}
532
+ − 296 \end{center}
543
+ − 297 \noindent
594
+ − 298 Then the property
532
+ − 299 \begin{center}
594
+ − 300 $\llbracket a \rrbracket = \llbracket a_\downarrow \rrbracket_p$
532
+ − 301 \end{center}
594
+ − 302 does not hold.
+ − 303 One might be able to prove an inequality such as
+ − 304 $\llbracket a \rrbracket \leq \llbracket a_\downarrow \rrbracket_p $
+ − 305 and then estimate $\llbracket a_\downarrow \rrbracket_p$,
+ − 306 but we found our approach more straightforward.\\
532
+ − 307
594
+ − 308 \subsection{Lexing Related Functions for $\rrexp$ such as $\backslash_r$, $\rdistincts$, and $\rsimp$}
+ − 309 The operations on r-regular expressions are
+ − 310 almost identical to those of the annotated regular expressions,
+ − 311 except that no bitcodes are used. For example,
+ − 312 the derivative operation becomes simpler:\\
543
+ − 313 \begin{center}
593
+ − 314 \begin{tabular}{@{}lcl@{}}
+ − 315 $(\ZERO)\,\backslash_r c$ & $\dn$ & $\ZERO$\\
+ − 316 $(\ONE)\,\backslash_r c$ & $\dn$ &
+ − 317 $\textit{if}\;c=d\; \;\textit{then}\;
+ − 318 \ONE\;\textit{else}\;\ZERO$\\
+ − 319 $(\sum \;\textit{rs})\,\backslash_r c$ & $\dn$ &
+ − 320 $\sum\;(\textit{map} \; (\_\backslash_r c) \; rs )$\\
+ − 321 $(r_1\cdot r_2)\,\backslash_r c$ & $\dn$ &
594
+ − 322 $\textit{if}\;(\textit{rnullable}\,r_1)$\\
593
+ − 323 & &$\textit{then}\;\sum\,[(r_1\,\backslash_r c)\cdot\,r_2,$\\
+ − 324 & &$\phantom{\textit{then},\;\sum\,}((r_2\,\backslash_r c))]$\\
+ − 325 & &$\textit{else}\;\,(r_1\,\backslash_r c)\cdot r_2$\\
+ − 326 $(r^*)\,\backslash_r c$ & $\dn$ &
+ − 327 $( r\,\backslash_r c)\cdot
+ − 328 (_{[]}r^*))$
+ − 329 \end{tabular}
543
+ − 330 \end{center}
+ − 331 \noindent
594
+ − 332 Similarly, $\distinctBy$ does not need
+ − 333 a function checking equivalence because
+ − 334 there are no bit annotations causing superficial differences
+ − 335 between syntactically equal terms.
532
+ − 336 \begin{center}
593
+ − 337 \begin{tabular}{lcl}
+ − 338 $\rdistinct{[]}{rset} $ & $\dn$ & $[]$\\
594
+ − 339 $\rdistinct{r :: rs}{rset}$ & $\dn$ &
+ − 340 $\textit{if}(r \in \textit{rset}) \; \textit{then} \; \rdistinct{rs}{rset}$\\
+ − 341 & & $\textit{else}\; \;
+ − 342 r::\rdistinct{rs}{(rset \cup \{r\})}$
593
+ − 343 \end{tabular}
532
+ − 344 \end{center}
+ − 345 %TODO: definition of rsimp (maybe only the alternative clause)
543
+ − 346 \noindent
595
+ − 347 We would like to make clear
+ − 348 a difference between our $\rdistincts$ and
+ − 349 the Isabelle $\textit {distinct}$ predicate.
+ − 350 In Isabelle $\textit{distinct}$ is a function that returns a boolean
+ − 351 rather than a list.
+ − 352 It tests if all the elements of a list are unique.\\
+ − 353 With $\textit{rdistinct}$,
+ − 354 and the flatten function for $\rrexp$s:
+ − 355 \begin{center}
+ − 356 \begin{tabular}{@{}lcl@{}}
596
+ − 357 $\textit{rflts} \; (\sum \textit{as}) :: \textit{as'}$ & $\dn$ & $as \; @ \; \textit{rflts} \; as' $ \\
595
+ − 358 $\textit{rflts} \; \ZERO :: as'$ & $\dn$ & $ \textit{rflts} \; \textit{as'} $ \\
+ − 359 $\textit{rflts} \; a :: as'$ & $\dn$ & $a :: \textit{rflts} \; \textit{as'}$ \quad(otherwise)
+ − 360 \end{tabular}
+ − 361 \end{center}
+ − 362 \noindent
+ − 363 one can chain together all the other modules
596
+ − 364 such as $\rsimpalts$:
+ − 365 \begin{center}
+ − 366 \begin{tabular}{@{}lcl@{}}
+ − 367 $\rsimpalts \;\; nil$ & $\dn$ & $\RZERO$\\
+ − 368 $\rsimpalts \;\; r::nil$ & $\dn$ & $r$\\
+ − 369 $\rsimpalts \;\; rs$ & $\dn$ & $\sum rs$\\
+ − 370 \end{tabular}
+ − 371 \end{center}
+ − 372 \noindent
+ − 373 and $\rsimpseq$:
+ − 374 \begin{center}
+ − 375 \begin{tabular}{@{}lcl@{}}
+ − 376 $\rsimpseq \;\; \RZERO \; \_ $ & $=$ & $\RZERO$\\
+ − 377 $\rsimpseq \;\; \_ \; \RZERO $ & $=$ & $\RZERO$\\
+ − 378 $\rsimpseq \;\; \RONE \cdot r_2$ & $\dn$ & $r_2$\\
+ − 379 $\rsimpseq \;\; r_1 r_2$ & $\dn$ & $r_1 \cdot r_2$\\
+ − 380 \end{tabular}
+ − 381 \end{center}
+ − 382 and get $\textit{rsimp}$ and $\rderssimp{\_}{\_}$:
595
+ − 383 \begin{center}
+ − 384 \begin{tabular}{@{}lcl@{}}
+ − 385
596
+ − 386 $\textit{rsimp} \; (r_1\cdot r_2)$ & $\dn$ & $ \textit{rsimp}_{SEQ} \; bs \;(\textit{rsimp} \; r_1) \; (\textit{rsimp} \; r_2) $ \\
+ − 387 $\textit{rsimp} \; (_{bs}\sum \textit{rs})$ & $\dn$ & $\textit{rsimp}_{ALTS} \; \textit{bs} \; (\textit{rdistinct} \; ( \textit{rflts} ( \textit{map} \; rsimp \; rs)) \; \rerases \; \varnothing) $ \\
+ − 388 $\textit{rsimp} \; r$ & $\dn$ & $\textit{r} \qquad \textit{otherwise}$
595
+ − 389 \end{tabular}
+ − 390 \end{center}
596
+ − 391 \begin{center}
+ − 392 \begin{tabular}{@{}lcl@{}}
+ − 393 $r\backslash_{rsimp} \, c$ & $\dn$ & $\rsimp \; (r\backslash_r \, c)$
+ − 394 \end{tabular}
+ − 395 \end{center}
+ − 396
+ − 397 \begin{center}
+ − 398 \begin{tabular}{@{}lcl@{}}
+ − 399 $r \backslash_{rsimps} (c\!::\!s) $ & $\dn$ & $(r \backslash_{rsimp}\, c) \backslash_{rsimps}\, s$ \\
+ − 400 $r \backslash_{rsimps} [\,] $ & $\dn$ & $r$
+ − 401 \end{tabular}
+ − 402 \end{center}
+ − 403 \noindent
543
+ − 404 With $\rrexp$ the size caclulation of annotated regular expressions'
+ − 405 simplification and derivatives can be done by the size of their unlifted
+ − 406 counterpart with the unlifted version of simplification and derivatives applied.
564
+ − 407 \begin{lemma}\label{sizeRelations}
553
+ − 408 The following equalities hold:
543
+ − 409 \begin{itemize}
+ − 410 \item
554
+ − 411 $\asize{\bsimp{a}} = \rsize{\rsimp{\rerase{a}}}$
+ − 412 \item
596
+ − 413 $\asize{\bderssimp{a}{s}} = \rsize{\rderssimp{\rerase{a}}{s}}$
554
+ − 414 \end{itemize}
532
+ − 415 \end{lemma}
543
+ − 416 \noindent
596
+ − 417 With lemma \ref{sizeRelations},
+ − 418 a bound on $\rsize{\rderssimp{\rerase{a}}{s}}$
+ − 419 \[
+ − 420 \llbracket \rderssimp{a}{s} \rrbracket_r \leq N_r
+ − 421 \]
+ − 422 \noindent
+ − 423 would apply to $\asize{\bderssimp{a}{s}}$ as well.
+ − 424 \[
+ − 425 \llbracket a \backslash_{bsimps} s \rrbracket \leq N_r.
+ − 426 \]
543
+ − 427 In the following content, we will focus on $\rrexp$'s size bound.
596
+ − 428 Whatever bounds we proved for $ \rsize{\rderssimp{\rerase{r}}{s}}$
+ − 429 will automatically apply to $\asize{\bderssimp{r}{s}}$.\\
+ − 430 Unless stated otherwise in this chapter all regular expressions without
593
+ − 431 bitcodes are seen as $\rrexp$s.
+ − 432 We also use $r_1 + r_2$ and $\RALTS{[r_1, r_2]}$ interchageably
+ − 433 as the former suits people's intuitive way of stating a binary alternative
+ − 434 regular expression.
532
+ − 435
+ − 436
+ − 437
+ − 438 %-----------------------------------
596
+ − 439 % SUB SECTION ROADMAP RREXP BOUND
532
+ − 440 %-----------------------------------
553
+ − 441
596
+ − 442 %\subsection{Roadmap to a Bound for $\textit{Rrexp}$}
553
+ − 443
596
+ − 444 %The way we obtain the bound for $\rrexp$s is by two steps:
+ − 445 %\begin{itemize}
+ − 446 % \item
+ − 447 % First, we rewrite $r\backslash s$ into something else that is easier
+ − 448 % to bound. This step is especially important for the inductive case
+ − 449 % $r_1 \cdot r_2$ and $r^*$, where the derivative can grow and bloat in a wild way,
+ − 450 % but after simplification they will always be equal or smaller to a form consisting of an alternative
+ − 451 % list of regular expressions $f \; (g\; (\sum rs))$ with some functions applied to it, where each element will be distinct after the function application.
+ − 452 % \item
+ − 453 % Then, for such a sum list of regular expressions $f\; (g\; (\sum rs))$, we can control its size
+ − 454 % by estimation, since $\distinctBy$ and $\flts$ are well-behaved and working together would only
+ − 455 % reduce the size of a regular expression, not adding to it.
+ − 456 %\end{itemize}
+ − 457 %
+ − 458 %\section{Step One: Closed Forms}
+ − 459 %We transform the function application $\rderssimp{r}{s}$
+ − 460 %into an equivalent
+ − 461 %form $f\; (g \; (\sum rs))$.
+ − 462 %The functions $f$ and $g$ can be anything from $\flts$, $\distinctBy$ and other helper functions from $\bsimp{\_}$.
+ − 463 %This way we get a different but equivalent way of expressing : $r\backslash s = f \; (g\; (\sum rs))$, we call the
+ − 464 %right hand side the "closed form" of $r\backslash s$.
+ − 465 %
+ − 466 %\begin{quote}\it
+ − 467 % Claim: For regular expressions $r_1 \cdot r_2$, we claim that
+ − 468 % \begin{center}
+ − 469 % $ \rderssimp{r_1 \cdot r_2}{s} =
+ − 470 % \rsimp{(\sum (r_1 \backslash s \cdot r_2 ) \; :: \;(\map \; \rderssimp{r2}{\_} \;(\vsuf{s}{r_1})))}$
+ − 471 % \end{center}
+ − 472 %\end{quote}
+ − 473 %\noindent
+ − 474 %We explain in detail how we reached those claims.
543
+ − 475 \subsection{Basic Properties needed for Closed Forms}
596
+ − 476 The next steps involves getting a closed form for
+ − 477 $\rderssimp{r}{s}$ and then obtaining
+ − 478 an estimate for the closed form.
543
+ − 479 \subsubsection{$\textit{rdistinct}$'s Deduplicates Successfully}
+ − 480 The $\textit{rdistinct}$ function, as its name suggests, will
553
+ − 481 remove duplicates in an \emph{r}$\textit{rexp}$ list,
+ − 482 according to the accumulator
543
+ − 483 and leave only one of each different element in a list:
555
+ − 484 \begin{lemma}\label{rdistinctDoesTheJob}
543
+ − 485 The function $\textit{rdistinct}$ satisfies the following
+ − 486 properties:
+ − 487 \begin{itemize}
+ − 488 \item
+ − 489 If $a \in acc$ then $a \notin (\rdistinct{rs}{acc})$.
+ − 490 \item
+ − 491 If list $rs'$ is the result of $\rdistinct{rs}{acc}$,
555
+ − 492 then $\textit{isDistinct} \; rs'$.
+ − 493 \item
+ − 494 $\rdistinct{rs}{acc} = rs - acc$
543
+ − 495 \end{itemize}
+ − 496 \end{lemma}
555
+ − 497 \noindent
+ − 498 The predicate $\textit{isDistinct}$ is for testing
+ − 499 whether a list's elements are all unique. It is defined
+ − 500 recursively on the structure of a regular expression,
+ − 501 and we omit the precise definition here.
543
+ − 502 \begin{proof}
+ − 503 The first part is by an induction on $rs$.
555
+ − 504 The second and third part can be proven by using the
543
+ − 505 induction rules of $\rdistinct{\_}{\_}$.
593
+ − 506
543
+ − 507 \end{proof}
+ − 508
+ − 509 \noindent
+ − 510 $\rdistinct{\_}{\_}$ will cancel out all regular expression terms
+ − 511 that are in the accumulator, therefore prepending a list $rs_a$ with an arbitrary
+ − 512 list $rs$ whose elements are all from the accumulator, and then call $\rdistinct{\_}{\_}$
+ − 513 on the resulting list, the output will be as if we had called $\rdistinct{\_}{\_}$
+ − 514 without the prepending of $rs$:
+ − 515 \begin{lemma}
554
+ − 516 The elements appearing in the accumulator will always be removed.
+ − 517 More precisely,
+ − 518 \begin{itemize}
+ − 519 \item
+ − 520 If $rs \subseteq rset$, then
+ − 521 $\rdistinct{rs@rsa }{acc} = \rdistinct{rsa }{acc}$.
+ − 522 \item
+ − 523 Furthermore, if $a \in rset$ and $\rdistinct{rs}{\{a\}} = []$,
+ − 524 then $\rdistinct{(rs @ rs')}{rset} = \rdistinct{rs'}{rset}$
+ − 525 \end{itemize}
543
+ − 526 \end{lemma}
554
+ − 527
543
+ − 528 \begin{proof}
+ − 529 By induction on $rs$.
+ − 530 \end{proof}
+ − 531 \noindent
+ − 532 On the other hand, if an element $r$ does not appear in the input list waiting to be deduplicated,
+ − 533 then expanding the accumulator to include that element will not cause the output list to change:
+ − 534 \begin{lemma}
+ − 535 The accumulator can be augmented to include elements not appearing in the input list,
+ − 536 and the output will not change.
+ − 537 \begin{itemize}
+ − 538 \item
593
+ − 539 If $r \notin rs$, then $\rdistinct{rs}{acc} = \rdistinct{rs}{\{r\} \cup acc}$.
543
+ − 540 \item
+ − 541 Particularly, when $acc = \varnothing$ and $rs$ de-duplicated, we have\\
+ − 542 \[ \rdistinct{rs}{\varnothing} = rs \]
+ − 543 \end{itemize}
+ − 544 \end{lemma}
+ − 545 \begin{proof}
+ − 546 The first half is by induction on $rs$. The second half is a corollary of the first.
+ − 547 \end{proof}
+ − 548 \noindent
+ − 549 The next property gives the condition for
+ − 550 when $\rdistinct{\_}{\_}$ becomes an identical mapping
+ − 551 for any prefix of an input list, in other words, when can
+ − 552 we ``push out" the arguments of $\rdistinct{\_}{\_}$:
555
+ − 553 \begin{lemma}\label{distinctRdistinctAppend}
554
+ − 554 If $\textit{isDistinct} \; rs_1$, and $rs_1 \cap acc = \varnothing$,
555
+ − 555 then
553
+ − 556 \[\textit{rdistinct}\; (rs_1 @ rsa)\;\, acc
+ − 557 = rs_1@(\textit{rdistinct} rsa \; (acc \cup rs_1))\]
543
+ − 558 \end{lemma}
554
+ − 559 \noindent
555
+ − 560 In other words, it can be taken out and left untouched in the output.
543
+ − 561 \begin{proof}
593
+ − 562 By an induction on $rs_1$, where $rsa$ and $acc$ are allowed to be arbitrary.
543
+ − 563 \end{proof}
554
+ − 564 \noindent
+ − 565 $\rdistinct{}{}$ removes any element in anywhere of a list, if it
+ − 566 had appeared previously:
+ − 567 \begin{lemma}\label{distinctRemovesMiddle}
+ − 568 The two properties hold if $r \in rs$:
+ − 569 \begin{itemize}
+ − 570 \item
555
+ − 571 $\rdistinct{rs}{rset} = \rdistinct{(rs @ [r])}{rset}$\\
+ − 572 and\\
554
+ − 573 $\rdistinct{(ab :: rs @ [ab])}{rset'} = \rdistinct{(ab :: rs)}{rset'}$
+ − 574 \item
555
+ − 575 $\rdistinct{ (rs @ rs') }{rset} = \rdistinct{rs @ [r] @ rs'}{rset}$\\
+ − 576 and\\
554
+ − 577 $\rdistinct{(ab :: rs @ [ab] @ rs'')}{rset'} =
593
+ − 578 \rdistinct{(ab :: rs @ rs'')}{rset'}$
554
+ − 579 \end{itemize}
+ − 580 \end{lemma}
+ − 581 \noindent
+ − 582 \begin{proof}
593
+ − 583 By induction on $rs$. All other variables are allowed to be arbitrary.
+ − 584 The second half of the lemma requires the first half.
+ − 585 Note that for each half's two sub-propositions need to be proven concurrently,
+ − 586 so that the induction goes through.
554
+ − 587 \end{proof}
+ − 588
555
+ − 589 \noindent
+ − 590 This allows us to prove ``Idempotency" of $\rdistinct{}{}$ of some kind:
+ − 591 \begin{lemma}\label{rdistinctConcatGeneral}
+ − 592 The following equalities involving multiple applications of $\rdistinct{}{}$ hold:
+ − 593 \begin{itemize}
+ − 594 \item
+ − 595 $\rdistinct{(rs @ rs')}{\varnothing} = \rdistinct{((\rdistinct{rs}{\varnothing})@ rs')}{\varnothing}$
+ − 596 \item
+ − 597 $\rdistinct{(rs @ rs')}{\varnothing} = \rdistinct{(\rdistinct{rs}{\varnothing} @ rs')}{\varnothing}$
+ − 598 \item
+ − 599 If $rset' \subseteq rset$, then $\rdistinct{rs}{rset} =
+ − 600 \rdistinct{(\rdistinct{rs}{rset'})}{rset}$. As a corollary
+ − 601 of this,
+ − 602 \item
+ − 603 $\rdistinct{(rs @ rs')}{rset} = \rdistinct{
+ − 604 (\rdistinct{rs}{\varnothing}) @ rs')}{rset}$. This
+ − 605 gives another corollary use later:
+ − 606 \item
+ − 607 If $a \in rset$, then $\rdistinct{(rs @ rs')}{rset} = \rdistinct{
+ − 608 (\rdistinct{(a :: rs)}{\varnothing} @ rs')}{rset} $,
+ − 609
+ − 610 \end{itemize}
+ − 611 \end{lemma}
+ − 612 \begin{proof}
+ − 613 By \ref{rdistinctDoesTheJob} and \ref{distinctRemovesMiddle}.
+ − 614 \end{proof}
+ − 615
553
+ − 616 \subsubsection{The Properties of $\backslash_r$, $\backslash_{rsimp}$, $\textit{Rflts}$ and $\textit{Rsimp}_{ALTS}$}
+ − 617 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.
543
+ − 618 These will be helpful in later closed form proofs, when
+ − 619 we want to transform the ways in which multiple functions involving
+ − 620 those are composed together
+ − 621 in interleaving derivative and simplification steps.
+ − 622
+ − 623 When the function $\textit{Rflts}$
+ − 624 is applied to the concatenation of two lists, the output can be calculated by first applying the
+ − 625 functions on two lists separately, and then concatenating them together.
554
+ − 626 \begin{lemma}\label{rfltsProps}
543
+ − 627 The function $\rflts$ has the below properties:\\
+ − 628 \begin{itemize}
+ − 629 \item
554
+ − 630 $\rflts \; (rs_1 @ rs_2) = \rflts \; rs_1 @ \rflts \; rs_2$
+ − 631 \item
+ − 632 If $r \neq \RZERO$ and $\nexists rs_1. r = \RALTS{rs}_1$, then $\rflts \; (r::rs) = r :: \rflts \; rs$
+ − 633 \item
+ − 634 $\rflts \; (rs @ [\RZERO]) = \rflts \; rs$
+ − 635 \item
+ − 636 $\rflts \; (rs' @ [\RALTS{rs}]) = \rflts \; rs'@rs$
+ − 637 \item
+ − 638 $\rflts \; (rs @ [\RONE]) = \rflts \; rs @ [\RONE]$
+ − 639 \item
+ − 640 If $r \neq \RZERO$ and $\nexists rs'. r = \RALTS{rs'}$ then $\rflts \; (rs @ [r])
+ − 641 = (\rflts \; rs) @ [r]$
555
+ − 642 \item
+ − 643 If $r = \RALTS{rs}$ and $r \in rs'$ then for all $r_1 \in rs.
+ − 644 r_1 \in \rflts \; rs'$.
+ − 645 \item
+ − 646 $\rflts \; (rs_a @ \RZERO :: rs_b) = \rflts \; (rs_a @ rs_b)$
543
+ − 647 \end{itemize}
+ − 648 \end{lemma}
+ − 649 \noindent
+ − 650 \begin{proof}
555
+ − 651 By induction on $rs_1$ in the first sub-lemma, and induction on $r$ in the second part,
+ − 652 and induction on $rs$, $rs'$, $rs$, $rs'$, $rs_a$ in the third, fourth, fifth, sixth and
+ − 653 last sub-lemma.
543
+ − 654 \end{proof}
555
+ − 655
554
+ − 656 \subsubsection{The $RL$ Function: Language Interpretation of $\textit{Rrexp}$s}
+ − 657 Much like the definition of $L$ on plain regular expressions, one could also
+ − 658 define the language interpretation of $\rrexp$s.
+ − 659 \begin{center}
593
+ − 660 \begin{tabular}{lcl}
+ − 661 $RL \; (\ZERO)$ & $\dn$ & $\phi$\\
+ − 662 $RL \; (\ONE)$ & $\dn$ & $\{[]\}$\\
+ − 663 $RL \; (c)$ & $\dn$ & $\{[c]\}$\\
+ − 664 $RL \; \sum rs$ & $\dn$ & $ \bigcup_{r \in rs} (RL \; r)$\\
+ − 665 $RL \; (r_1 \cdot r_2)$ & $\dn$ & $ RL \; (r_1) @ RL \; (r_2)$\\
+ − 666 $RL \; (r^*)$ & $\dn$ & $ (RL(r))^*$
+ − 667 \end{tabular}
554
+ − 668 \end{center}
+ − 669 \noindent
+ − 670 The main use of $RL$ is to establish some connections between $\rsimp{}$
+ − 671 and $\rnullable{}$:
+ − 672 \begin{lemma}
+ − 673 The following properties hold:
+ − 674 \begin{itemize}
+ − 675 \item
+ − 676 If $\rnullable{r}$, then $\rsimp{r} \neq \RZERO$.
+ − 677 \item
+ − 678 $\rnullable{r \backslash s} \quad $ if and only if $\quad \rnullable{\rderssimp{r}{s}}$.
+ − 679 \end{itemize}
+ − 680 \end{lemma}
+ − 681 \begin{proof}
+ − 682 The first part is by induction on $r$.
+ − 683 The second part is true because property
+ − 684 \[ RL \; r = RL \; (\rsimp{r})\] holds.
+ − 685 \end{proof}
593
+ − 686
554
+ − 687 \subsubsection{$\rsimp{}$ is Non-Increasing}
+ − 688 In this subsection, we prove that the function $\rsimp{}$ does not
+ − 689 make the $\llbracket \rrbracket_r$ size increase.
543
+ − 690
+ − 691
554
+ − 692 \begin{lemma}\label{rsimpSize}
+ − 693 $\llbracket \rsimp{r} \rrbracket_r \leq \llbracket r \rrbracket_r$
+ − 694 \end{lemma}
+ − 695 \subsubsection{Simplified $\textit{Rrexp}$s are Good}
+ − 696 We formalise the notion of ``good" regular expressions,
+ − 697 which means regular expressions that
+ − 698 are not fully simplified. For alternative regular expressions that means they
+ − 699 do not contain any nested alternatives like
+ − 700 \[ r_1 + (r_2 + r_3) \], un-removed $\RZERO$s like \[\RZERO + r\]
+ − 701 or duplicate elements in a children regular expression list like \[ \sum [r, r, \ldots]\]:
+ − 702 \begin{center}
+ − 703 \begin{tabular}{@{}lcl@{}}
+ − 704 $\good\; \RZERO$ & $\dn$ & $\textit{false}$\\
+ − 705 $\good\; \RONE$ & $\dn$ & $\textit{true}$\\
+ − 706 $\good\; \RCHAR{c}$ & $\dn$ & $\btrue$\\
+ − 707 $\good\; \RALTS{[]}$ & $\dn$ & $\bfalse$\\
+ − 708 $\good\; \RALTS{[r]}$ & $\dn$ & $\bfalse$\\
+ − 709 $\good\; \RALTS{r_1 :: r_2 :: rs}$ & $\dn$ &
+ − 710 $\textit{isDistinct} \; (r_1 :: r_2 :: rs) \;$\\
593
+ − 711 & & $\textit{and}\; (\forall r' \in (r_1 :: r_2 :: rs).\; \good \; r'\; \, \textit{and}\; \, \textit{nonAlt}\; r')$\\
554
+ − 712 $\good \; \RSEQ{\RZERO}{r}$ & $\dn$ & $\bfalse$\\
+ − 713 $\good \; \RSEQ{\RONE}{r}$ & $\dn$ & $\bfalse$\\
+ − 714 $\good \; \RSEQ{r}{\RZERO}$ & $\dn$ & $\bfalse$\\
+ − 715 $\good \; \RSEQ{r_1}{r_2}$ & $\dn$ & $\good \; r_1 \;\, \textit{and} \;\, \good \; r_2$\\
+ − 716 $\good \; \RSTAR{r}$ & $\dn$ & $\btrue$\\
+ − 717 \end{tabular}
+ − 718 \end{center}
+ − 719 \noindent
+ − 720 The predicate $\textit{nonAlt}$ evaluates to true when the regular expression is not an
+ − 721 alternative, and false otherwise.
+ − 722 The $\good$ property is preserved under $\rsimp_{ALTS}$, provided that
+ − 723 its non-empty argument list of expressions are all good themsleves, and $\textit{nonAlt}$,
+ − 724 and unique:
+ − 725 \begin{lemma}\label{rsimpaltsGood}
+ − 726 If $rs \neq []$ and forall $r \in rs. \textit{nonAlt} \; r$ and $\textit{isDistinct} \; rs$,
+ − 727 then $\good \; (\rsimpalts \; rs)$ if and only if forall $r \in rs. \; \good \; r$.
+ − 728 \end{lemma}
+ − 729 \noindent
+ − 730 We also note that
+ − 731 if a regular expression $r$ is good, then $\rflts$ on the singleton
+ − 732 list $[r]$ will not break goodness:
+ − 733 \begin{lemma}\label{flts2}
+ − 734 If $\good \; r$, then forall $r' \in \rflts \; [r]. \; \good \; r'$ and $\textit{nonAlt} \; r'$.
+ − 735 \end{lemma}
+ − 736 \begin{proof}
+ − 737 By an induction on $r$.
+ − 738 \end{proof}
543
+ − 739 \noindent
554
+ − 740 The other observation we make about $\rsimp{r}$ is that it never
+ − 741 comes with nested alternatives, which we describe as the $\nonnested$
+ − 742 property:
+ − 743 \begin{center}
+ − 744 \begin{tabular}{lcl}
+ − 745 $\nonnested \; \, \sum []$ & $\dn$ & $\btrue$\\
+ − 746 $\nonnested \; \, \sum ((\sum rs_1) :: rs_2)$ & $\dn$ & $\bfalse$\\
+ − 747 $\nonnested \; \, \sum (r :: rs)$ & $\dn$ & $\nonnested (\sum rs)$\\
+ − 748 $\nonnested \; \, r $ & $\dn$ & $\btrue$
+ − 749 \end{tabular}
+ − 750 \end{center}
+ − 751 \noindent
+ − 752 The $\rflts$ function
+ − 753 always opens up nested alternatives,
+ − 754 which enables $\rsimp$ to be non-nested:
+ − 755
+ − 756 \begin{lemma}\label{nonnestedRsimp}
+ − 757 $\nonnested \; (\rsimp{r})$
+ − 758 \end{lemma}
+ − 759 \begin{proof}
+ − 760 By an induction on $r$.
+ − 761 \end{proof}
+ − 762 \noindent
+ − 763 With this we could prove that a regular expressions
+ − 764 after simplification and flattening and de-duplication,
+ − 765 will not contain any alternative regular expression directly:
+ − 766 \begin{lemma}\label{nonaltFltsRd}
+ − 767 If $x \in \rdistinct{\rflts\; (\map \; \rsimp{} \; rs)}{\varnothing}$
+ − 768 then $\textit{nonAlt} \; x$.
+ − 769 \end{lemma}
+ − 770 \begin{proof}
+ − 771 By \ref{nonnestedRsimp}.
+ − 772 \end{proof}
+ − 773 \noindent
+ − 774 The other thing we know is that once $\rsimp{}$ had finished
+ − 775 processing an alternative regular expression, it will not
+ − 776 contain any $\RZERO$s, this is because all the recursive
+ − 777 calls to the simplification on the children regular expressions
+ − 778 make the children good, and $\rflts$ will not take out
+ − 779 any $\RZERO$s out of a good regular expression list,
+ − 780 and $\rdistinct{}$ will not mess with the result.
+ − 781 \begin{lemma}\label{flts3Obv}
+ − 782 The following are true:
+ − 783 \begin{itemize}
+ − 784 \item
+ − 785 If for all $r \in rs. \, \good \; r $ or $r = \RZERO$,
+ − 786 then for all $r \in \rflts\; rs. \, \good \; r$.
+ − 787 \item
+ − 788 If $x \in \rdistinct{\rflts\; (\map \; rsimp{}\; rs)}{\varnothing}$
+ − 789 and for all $y$ such that $\llbracket y \rrbracket_r$ less than
+ − 790 $\llbracket rs \rrbracket_r + 1$, either
+ − 791 $\good \; (\rsimp{y})$ or $\rsimp{y} = \RZERO$,
+ − 792 then $\good \; x$.
+ − 793 \end{itemize}
+ − 794 \end{lemma}
+ − 795 \begin{proof}
+ − 796 The first part is by induction on $rs$, where the induction
+ − 797 rule is the inductive cases for $\rflts$.
+ − 798 The second part is a corollary from the first part.
+ − 799 \end{proof}
543
+ − 800
554
+ − 801 And this leads to good structural property of $\rsimp{}$,
+ − 802 that after simplification, a regular expression is
+ − 803 either good or $\RZERO$:
+ − 804 \begin{lemma}\label{good1}
+ − 805 For any r-regular expression $r$, $\good \; \rsimp{r}$ or $\rsimp{r} = \RZERO$.
+ − 806 \end{lemma}
+ − 807 \begin{proof}
+ − 808 By an induction on $r$. The inductive measure is the size $\llbracket \rrbracket_r$.
+ − 809 Lemma \ref{rsimpSize} says that
+ − 810 $\llbracket \rsimp{r}\rrbracket_r$ is smaller than or equal to
+ − 811 $\llbracket r \rrbracket_r$.
+ − 812 Therefore, in the $r_1 \cdot r_2$ and $\sum rs$ case,
+ − 813 Inductive hypothesis applies to the children regular expressions
+ − 814 $r_1$, $r_2$, etc. The lemma \ref{flts3Obv}'s precondition is satisfied
+ − 815 by that as well.
+ − 816 The lemmas \ref{nonnestedRsimp} and \ref{nonaltFltsRd} are used
+ − 817 to ensure that goodness is preserved at the topmost level.
+ − 818 \end{proof}
+ − 819 We shall prove that any good regular expression is
+ − 820 a fixed-point for $\rsimp{}$.
+ − 821 First we prove an auxiliary lemma:
+ − 822 \begin{lemma}\label{goodaltsNonalt}
+ − 823 If $\good \; \sum rs$, then $\rflts\; rs = rs$.
+ − 824 \end{lemma}
+ − 825 \begin{proof}
+ − 826 By an induction on $\sum rs$. The inductive rules are the cases
+ − 827 for $\good$.
+ − 828 \end{proof}
+ − 829 \noindent
+ − 830 Now we are ready to prove that good regular expressions are invariant
+ − 831 of $\rsimp{}$ application:
+ − 832 \begin{lemma}\label{test}
+ − 833 If $\good \;r$ then $\rsimp{r} = r$.
+ − 834 \end{lemma}
+ − 835 \begin{proof}
+ − 836 By an induction on the inductive cases of $\good$.
+ − 837 The lemma \ref{goodaltsNonalt} is used in the alternative
+ − 838 case where 2 or more elements are present in the list.
+ − 839 \end{proof}
555
+ − 840 \noindent
+ − 841 Given below is a property involving $\rflts$, $\rdistinct{}{}$, $\rsimp{}$ and $\rsimp_{ALTS}$,
+ − 842 which requires $\ref{good1}$ to go through smoothly.
+ − 843 It says that an application of $\rsimp_{ALTS}$ can be "absorbed",
+ − 844 if it its output is concatenated with a list and then applied to $\rflts$.
+ − 845 \begin{lemma}\label{flattenRsimpalts}
+ − 846 $\rflts \; ( (\rsimp_{ALTS} \;
+ − 847 (\rdistinct{(\rflts \; (\map \; \rsimp{}\; rs))}{\varnothing})) ::
+ − 848 \map \; \rsimp{} \; rs' ) =
+ − 849 \rflts \; ( (\rdistinct{(\rflts \; (\map \; \rsimp{}\; rs))}{\varnothing}) @ (
+ − 850 \map \; \rsimp{rs'}))$
554
+ − 851
593
+ − 852
555
+ − 853 \end{lemma}
+ − 854 \begin{proof}
+ − 855 By \ref{good1}.
+ − 856 \end{proof}
+ − 857 \noindent
+ − 858
+ − 859
+ − 860
+ − 861
+ − 862
+ − 863 We are also
554
+ − 864 \subsubsection{$\rsimp$ is Idempotent}
+ − 865 The idempotency of $\rsimp$ is very useful in
+ − 866 manipulating regular expression terms into desired
+ − 867 forms so that key steps allowing further rewriting to closed forms
+ − 868 are possible.
+ − 869 \begin{lemma}\label{rsimpIdem}
593
+ − 870 $\rsimp{r} = \rsimp{\rsimp{r}}$
554
+ − 871 \end{lemma}
+ − 872
+ − 873 \begin{proof}
+ − 874 By \ref{test} and \ref{good1}.
+ − 875 \end{proof}
+ − 876 \noindent
+ − 877 This property means we do not have to repeatedly
+ − 878 apply simplification in each step, which justifies
+ − 879 our definition of $\blexersimp$.
+ − 880
532
+ − 881
554
+ − 882 On the other hand, we could repeat the same $\rsimp{}$ applications
+ − 883 on regular expressions as many times as we want, if we have at least
+ − 884 one simplification applied to it, and apply it wherever we would like to:
+ − 885 \begin{corollary}\label{headOneMoreSimp}
555
+ − 886 The following properties hold, directly from \ref{rsimpIdem}:
+ − 887
+ − 888 \begin{itemize}
+ − 889 \item
+ − 890 $\map \; \rsimp{(r :: rs)} = \map \; \rsimp{} \; (\rsimp{r} :: rs)$
+ − 891 \item
+ − 892 $\rsimp{(\RALTS{rs})} = \rsimp{(\RALTS{\map \; \rsimp{} \; rs})}$
+ − 893 \end{itemize}
554
+ − 894 \end{corollary}
+ − 895 \noindent
+ − 896 This will be useful in later closed form proof's rewriting steps.
+ − 897 Similarly, we point out the following useful facts below:
+ − 898 \begin{lemma}
+ − 899 The following equalities hold if $r = \rsimp{r'}$ for some $r'$:
+ − 900 \begin{itemize}
+ − 901 \item
+ − 902 If $r = \sum rs$ then $\rsimpalts \; rs = \sum rs$.
+ − 903 \item
+ − 904 If $r = \sum rs$ then $\rdistinct{rs}{\varnothing} = rs$.
+ − 905 \item
+ − 906 $\rsimpalts \; (\rdistinct{\rflts \; [r]}{\varnothing}) = r$.
+ − 907 \end{itemize}
+ − 908 \end{lemma}
+ − 909 \begin{proof}
+ − 910 By application of \ref{rsimpIdem} and \ref{good1}.
+ − 911 \end{proof}
+ − 912
+ − 913 \noindent
+ − 914 With the idempotency of $\rsimp{}$ and its corollaries,
+ − 915 we can start proving some key equalities leading to the
+ − 916 closed forms.
+ − 917 Now presented are a few equivalent terms under $\rsimp{}$.
+ − 918 We use $r_1 \sequal r_2 $ here to denote $\rsimp{r_1} = \rsimp{r_2}$.
+ − 919 \begin{lemma}
593
+ − 920 \begin{itemize}
+ − 921 The following equivalence hold:
554
+ − 922 \item
+ − 923 $\rsimpalts \; (\RZERO :: rs) \sequal \rsimpalts\; rs$
+ − 924 \item
+ − 925 $\rsimpalts \; rs \sequal \rsimpalts (\map \; \rsimp{} \; rs)$
+ − 926 \item
+ − 927 $\RALTS{\RALTS{rs}} \sequal \RALTS{rs}$
555
+ − 928 \item
+ − 929 $\sum ((\sum rs_a) :: rs_b) \sequal \sum rs_a @ rs_b$
+ − 930 \item
+ − 931 $\RALTS{rs} = \RALTS{\map \; \rsimp{} \; rs}$
554
+ − 932 \end{itemize}
+ − 933 \end{lemma}
555
+ − 934 \begin{proof}
+ − 935 By induction on the lists involved.
+ − 936 \end{proof}
+ − 937 \noindent
+ − 938 Similarly,
+ − 939 we introduce the equality for $\sum$ when certain child regular expressions
+ − 940 are $\sum$ themselves:
+ − 941 \begin{lemma}\label{simpFlatten3}
+ − 942 One can flatten the inside $\sum$ of a $\sum$ if it is being
+ − 943 simplified. Concretely,
+ − 944 \begin{itemize}
+ − 945 \item
+ − 946 If for all $r \in rs, rs', rs''$, we have $\good \; r $
+ − 947 or $r = \RZERO$, then $\sum (rs' @ rs @ rs'') \sequal
+ − 948 \sum (rs' @ [\sum rs] @ rs'')$ holds. As a corollary,
+ − 949 \item
+ − 950 $\sum (rs' @ [\sum rs] @ rs'') \sequal \sum (rs' @ rs @ rs'')$
+ − 951 \end{itemize}
+ − 952 \end{lemma}
+ − 953 \begin{proof}
+ − 954 By rewriting steps involving the use of \ref{test} and \ref{rdistinctConcatGeneral}.
+ − 955 The second sub-lemma is a corollary of the previous.
+ − 956 \end{proof}
+ − 957 %Rewriting steps not put in--too long and complicated-------------------------------
+ − 958 \begin{comment}
+ − 959 \begin{center}
+ − 960 $\rsimp{\sum (rs' @ rs @ rs'')} \stackrel{def of bsimp}{=}$ \\
+ − 961 $\rsimpalts \; (\rdistinct{\rflts \; ((\map \; \rsimp{}\; rs') @ (\map \; \rsimp{} \; rs ) @ (\map \; \rsimp{} \; rs''))}{\varnothing})$ \\
+ − 962 $\stackrel{by \ref{test}}{=}
+ − 963 \rsimpalts \; (\rdistinct{(\rflts \; rs' @ \rflts \; rs @ \rflts \; rs'')}{
+ − 964 \varnothing})$\\
+ − 965 $\stackrel{by \ref{rdistinctConcatGeneral}}{=}
+ − 966 \rsimpalts \; (\rdistinct{\rflts \; rs'}{\varnothing} @ \rdistinct{(
+ − 967 \rflts\; rs @ \rflts \; rs'')}{\rflts \; rs'})$\\
593
+ − 968
555
+ − 969 \end{center}
+ − 970 \end{comment}
+ − 971 %Rewriting steps not put in--too long and complicated-------------------------------
554
+ − 972 \noindent
+ − 973 We need more equalities like the above to enable a closed form,
+ − 974 but to proceed we need to introduce two rewrite relations,
+ − 975 to make things smoother.
557
+ − 976 \subsubsection{The rewrite relation $\hrewrite$ , $\scfrewrites$ , $\frewrite$ and $\grewrite$}
554
+ − 977 Insired by the success we had in the correctness proof
+ − 978 in \ref{Bitcoded2}, where we invented
555
+ − 979 a term rewriting system to capture the similarity between terms,
+ − 980 we follow suit here defining simplification
+ − 981 steps as rewriting steps. This allows capturing
+ − 982 similarities between terms that would be otherwise
+ − 983 hard to express.
+ − 984
557
+ − 985 We use $\hrewrite$ for one-step atomic rewrite of
+ − 986 regular expression simplification,
555
+ − 987 $\frewrite$ for rewrite of list of regular expressions that
+ − 988 include all operations carried out in $\rflts$, and $\grewrite$ for
+ − 989 rewriting a list of regular expressions possible in both $\rflts$ and $\rdistinct{}{}$.
+ − 990 Their reflexive transitive closures are used to denote zero or many steps,
+ − 991 as was the case in the previous chapter.
554
+ − 992 The presentation will be more concise than that in \ref{Bitcoded2}.
+ − 993 To differentiate between the rewriting steps for annotated regular expressions
+ − 994 and $\rrexp$s, we add characters $h$ and $g$ below the squig arrow symbol
+ − 995 to mean atomic simplification transitions
+ − 996 of $\rrexp$s and $\rrexp$ lists, respectively.
+ − 997
555
+ − 998
+ − 999
593
+ − 1000 List of one-step rewrite rules for $\rrexp$ ($\hrewrite$):
555
+ − 1001
+ − 1002
554
+ − 1003 \begin{center}
593
+ − 1004 \begin{mathpar}
+ − 1005 \inferrule[RSEQ0L]{}{\RZERO \cdot r_2 \hrewrite \RZERO\\}
555
+ − 1006
593
+ − 1007 \inferrule[RSEQ0R]{}{r_1 \cdot \RZERO \hrewrite \RZERO\\}
555
+ − 1008
593
+ − 1009 \inferrule[RSEQ1]{}{(\RONE \cdot r) \hrewrite r\\}\\
555
+ − 1010
593
+ − 1011 \inferrule[RSEQL]{ r_1 \hrewrite r_2}{r_1 \cdot r_3 \hrewrite r_2 \cdot r_3\\}
+ − 1012
+ − 1013 \inferrule[RSEQR]{ r_3 \hrewrite r_4}{r_1 \cdot r_3 \hrewrite r_1 \cdot r_4\\}\\
555
+ − 1014
593
+ − 1015 \inferrule[RALTSChild]{r \hrewrite r'}{\sum (rs_1 @ [r] @ rs_2) \hrewrite \sum (rs_1 @ [r'] @ rs_2)\\}
555
+ − 1016
593
+ − 1017 \inferrule[RALTS0]{}{\sum (rs_a @ [\RZERO] @ rs_b) \hrewrite \sum (rs_a @ rs_b)}
555
+ − 1018
593
+ − 1019 \inferrule[RALTSNested]{}{\sum (rs_a @ [\sum rs_1] @ rs_b) \hrewrite \sum (rs_a @ rs_1 @ rs_b)}
555
+ − 1020
593
+ − 1021 \inferrule[RALTSNil]{}{ \sum [] \hrewrite \RZERO\\}
555
+ − 1022
593
+ − 1023 \inferrule[RALTSSingle]{}{ \sum [r] \hrewrite r\\}
555
+ − 1024
593
+ − 1025 \inferrule[RALTSDelete]{\\ r_1 = r_2}{\sum rs_a @ [r_1] @ rs_b @ [r_2] @ rsc \hrewrite \sum rs_a @ [r_1] @ rs_b @ rs_c}
555
+ − 1026
593
+ − 1027 \end{mathpar}
555
+ − 1028 \end{center}
554
+ − 1029
557
+ − 1030
593
+ − 1031 List of rewrite rules for a list of regular expressions,
+ − 1032 where each element can rewrite in many steps to the other (scf stands for
+ − 1033 li\emph{s}t \emph{c}losed \emph{f}orm). This relation is similar to the
+ − 1034 $\stackrel{s*}{\rightsquigarrow}$ for annotated regular expressions.
557
+ − 1035
+ − 1036 \begin{center}
593
+ − 1037 \begin{mathpar}
+ − 1038 \inferrule{}{[] \scfrewrites [] }
+ − 1039 \inferrule{r \hrewrites r' \\ rs \scfrewrites rs'}{r :: rs \scfrewrites r' :: rs'}
+ − 1040 \end{mathpar}
557
+ − 1041 \end{center}
555
+ − 1042 %frewrite
593
+ − 1043 List of one-step rewrite rules for flattening
+ − 1044 a list of regular expressions($\frewrite$):
555
+ − 1045 \begin{center}
593
+ − 1046 \begin{mathpar}
+ − 1047 \inferrule{}{\RZERO :: rs \frewrite rs \\}
555
+ − 1048
593
+ − 1049 \inferrule{}{(\sum rs) :: rs_a \frewrite rs @ rs_a \\}
555
+ − 1050
593
+ − 1051 \inferrule{rs_1 \frewrite rs_2}{r :: rs_1 \frewrite r :: rs_2}
+ − 1052 \end{mathpar}
555
+ − 1053 \end{center}
+ − 1054
593
+ − 1055 Lists of one-step rewrite rules for flattening and de-duplicating
+ − 1056 a list of regular expressions ($\grewrite$):
555
+ − 1057 \begin{center}
593
+ − 1058 \begin{mathpar}
+ − 1059 \inferrule{}{\RZERO :: rs \grewrite rs \\}
532
+ − 1060
593
+ − 1061 \inferrule{}{(\sum rs) :: rs_a \grewrite rs @ rs_a \\}
555
+ − 1062
593
+ − 1063 \inferrule{rs_1 \grewrite rs_2}{r :: rs_1 \grewrite r :: rs_2}
555
+ − 1064
593
+ − 1065 \inferrule[dB]{}{rs_a @ [a] @ rs_b @[a] @ rs_c \grewrite rs_a @ [a] @ rsb @ rsc}
+ − 1066 \end{mathpar}
555
+ − 1067 \end{center}
+ − 1068
+ − 1069 \noindent
+ − 1070 The reason why we take the trouble of defining
+ − 1071 two separate list rewriting definitions $\frewrite$ and $\grewrite$
557
+ − 1072 is to separate the two stages of simplification: flattening and de-duplicating.
+ − 1073 Sometimes $\grewrites$ is slightly too powerful
+ − 1074 so we would rather use $\frewrites$ which makes certain rewriting steps
+ − 1075 more straightforward to prove.
556
+ − 1076 For example, when proving the closed-form for the alternative regular expression,
+ − 1077 one of the rewriting steps would be:
+ − 1078 \begin{lemma}
557
+ − 1079 $\sum (\rDistinct \;\; (\map \; (\_ \backslash x) \; (\rflts \; rs)) \;\; \varnothing) \sequal
593
+ − 1080 \sum (\rDistinct \;\; (\rflts \; (\map \; (\_ \backslash x) \; rs)) \;\; \varnothing)
+ − 1081 $
556
+ − 1082 \end{lemma}
+ − 1083 \noindent
+ − 1084 Proving this is by first showing
557
+ − 1085 \begin{lemma}\label{earlyLaterDerFrewrites}
556
+ − 1086 $\map \; (\_ \backslash x) \; (\rflts \; rs) \frewrites
557
+ − 1087 \rflts \; (\map \; (\_ \backslash x) \; rs)$
556
+ − 1088 \end{lemma}
+ − 1089 \noindent
+ − 1090 and then using lemma
+ − 1091 \begin{lemma}\label{frewritesSimpeq}
+ − 1092 If $rs_1 \frewrites rs_2 $, then $\sum (\rDistinct \; rs_1 \; \varnothing) \sequal
557
+ − 1093 \sum (\rDistinct \; rs_2 \; \varnothing)$.
556
+ − 1094 \end{lemma}
557
+ − 1095 \noindent
+ − 1096 is a piece of cake.
+ − 1097 But this trick will not work for $\grewrites$.
+ − 1098 For example, a rewriting step in proving
+ − 1099 closed forms is:
+ − 1100 \begin{center}
593
+ − 1101 $\rsimp{(\rsimpalts \; (\map \; (\_ \backslash x) \; (\rdistinct{(\rflts \; (\map \; (\rsimp{} \; \circ \; (\lambda r. \rderssimp{r}{xs}))))}{\varnothing})))}$\\
+ − 1102 $=$ \\
+ − 1103 $\rsimp{(\rsimpalts \; (\rdistinct{(\map \; (\_ \backslash x) \; (\rflts \; (\map \; (\rsimp{} \; \circ \; (\lambda r. \rderssimp{r}{xs})))) ) }{\varnothing}))} $
+ − 1104 \noindent
557
+ − 1105 \end{center}
+ − 1106 For this one would hope to have a rewriting relation between the two lists involved,
+ − 1107 similar to \ref{earlyLaterDerFrewrites}. However, it turns out that
556
+ − 1108 \begin{center}
593
+ − 1109 $\map \; (\_ \backslash x) \; (\rDistinct \; rs \; rset) \grewrites \rDistinct \; (\map \;
+ − 1110 (\_ \backslash x) \; rs) \; ( rset \backslash x)$
556
+ − 1111 \end{center}
+ − 1112 \noindent
557
+ − 1113 does $\mathbf{not}$ hold in general.
+ − 1114 For this rewriting step we will introduce some slightly more cumbersome
+ − 1115 proof technique in later sections.
+ − 1116 The point is that $\frewrite$
+ − 1117 allows us to prove equivalence in a straightforward two-step method that is
+ − 1118 not possible for $\grewrite$, thereby reducing the complexity of the entire proof.
555
+ − 1119
556
+ − 1120
557
+ − 1121 \subsubsection{Terms That Can Be Rewritten Using $\hrewrites$, $\grewrites$, and $\frewrites$}
+ − 1122 We present in the below lemma a few pairs of terms that are rewritable via
+ − 1123 $\grewrites$:
+ − 1124 \begin{lemma}\label{gstarRdistinctGeneral}
+ − 1125 \begin{itemize}
+ − 1126 \item
+ − 1127 $rs_1 @ rs \grewrites rs_1 @ (\rDistinct \; rs \; rs_1)$
+ − 1128 \item
+ − 1129 $rs \grewrites \rDistinct \; rs \; \varnothing$
+ − 1130 \item
+ − 1131 $rs_a @ (\rDistinct \; rs \; rs_a) \grewrites rs_a @ (\rDistinct \;
+ − 1132 rs \; (\{\RZERO\} \cup rs_a))$
+ − 1133 \item
+ − 1134 $rs \;\; @ \;\; \rDistinct \; rs_a \; rset \grewrites rs @ \rDistinct \; rs_a \;
+ − 1135 (rest \cup rs)$
+ − 1136
+ − 1137 \end{itemize}
+ − 1138 \end{lemma}
+ − 1139 \noindent
+ − 1140 If a pair of terms $rs_1, rs_2$ are rewritable via $\grewrites$ to each other,
+ − 1141 then they are equivalent under $\rsimp{}$:
+ − 1142 \begin{lemma}\label{grewritesSimpalts}
+ − 1143 If $rs_1 \grewrites rs_2$, then
+ − 1144 we have the following equivalence hold:
+ − 1145 \begin{itemize}
+ − 1146 \item
+ − 1147 $\sum rs_1 \sequal \sum rs_2$
+ − 1148 \item
+ − 1149 $\rsimpalts \; rs_1 \sequal \rsimpalts \; rs_2$
+ − 1150 \end{itemize}
+ − 1151 \end{lemma}
+ − 1152 \noindent
+ − 1153 Here are a few connecting lemmas showing that
+ − 1154 if a list of regular expressions can be rewritten using $\grewrites$ or $\frewrites $ or
+ − 1155 $\scfrewrites$,
+ − 1156 then an alternative constructor taking the list can also be rewritten using $\hrewrites$:
+ − 1157 \begin{lemma}
+ − 1158 \begin{itemize}
+ − 1159 \item
+ − 1160 If $rs \grewrites rs'$ then $\sum rs \hrewrites \sum rs'$.
+ − 1161 \item
+ − 1162 If $rs \grewrites rs'$ then $\sum rs \hrewrites \rsimpalts \; rs'$
+ − 1163 \item
+ − 1164 If $rs_1 \scfrewrites rs_2$ then $\sum (rs @ rs_1) \hrewrites \sum (rs @ rs_2)$
+ − 1165 \item
+ − 1166 If $rs_1 \scfrewrites rs_2$ then $\sum rs_1 \hrewrites \sum rs_2$
+ − 1167
+ − 1168 \end{itemize}
+ − 1169 \end{lemma}
+ − 1170 \noindent
+ − 1171 Here comes the meat of the proof,
+ − 1172 which says that once two lists are rewritable to each other,
+ − 1173 then they are equivalent under $\rsimp{}$:
+ − 1174 \begin{lemma}
+ − 1175 If $r_1 \hrewrites r_2$ then $r_1 \sequal r_2$.
+ − 1176 \end{lemma}
+ − 1177
+ − 1178 \noindent
+ − 1179 And similar to \ref{Bitcoded2} one can preserve rewritability after taking derivative
+ − 1180 of two regular expressions on both sides:
+ − 1181 \begin{lemma}\label{interleave}
+ − 1182 If $r \hrewrites r' $ then $\rder{c}{r} \hrewrites \rder{c}{r'}$
+ − 1183 \end{lemma}
+ − 1184 \noindent
+ − 1185 This allows proving more $\mathbf{rsimp}$-equivalent terms, involving $\backslash_r$ now.
+ − 1186 \begin{lemma}\label{insideSimpRemoval}
+ − 1187 $\rsimp{\rder{c}{\rsimp{r}}} = \rsimp{\rder{c}{r}} $
+ − 1188 \end{lemma}
+ − 1189 \noindent
+ − 1190 \begin{proof}
+ − 1191 By \ref{interleave} and \ref{rsimpIdem}.
+ − 1192 \end{proof}
+ − 1193 \noindent
+ − 1194 And this unlocks more equivalent terms:
+ − 1195 \begin{lemma}\label{Simpders}
+ − 1196 As corollaries of \ref{insideSimpRemoval}, we have
+ − 1197 \begin{itemize}
+ − 1198 \item
+ − 1199 If $s \neq []$ then $\rderssimp{r}{s} = \rsimp{(\rders \; r \; s)}$.
+ − 1200 \item
+ − 1201 $\rsimpalts \; (\map \; (\_ \backslash_r x) \;
593
+ − 1202 (\rdistinct{rs}{\varnothing})) \sequal
+ − 1203 \rsimpalts \; (\rDistinct \;
+ − 1204 (\map \; (\_ \backslash_r x) rs) \;\varnothing )$
+ − 1205 \end{itemize}
+ − 1206 \end{lemma}
557
+ − 1207 \noindent
+ − 1208
+ − 1209 Finally,
+ − 1210 together with
+ − 1211 \begin{lemma}\label{rderRsimpAltsCommute}
+ − 1212 $\rder{x}{(\rsimpalts \; rs)} = \rsimpalts \; (\map \; (\rder{x}{\_}) \; rs)$
+ − 1213 \end{lemma}
+ − 1214 \noindent
+ − 1215 this leads to the first closed form--
+ − 1216 \begin{lemma}\label{altsClosedForm}
593
+ − 1217 \begin{center}
+ − 1218 $\rderssimp{(\sum rs)}{s} \sequal
+ − 1219 \sum \; (\map \; (\rderssimp{\_}{s}) \; rs)$
+ − 1220 \end{center}
557
+ − 1221 \end{lemma}
593
+ − 1222
556
+ − 1223 \noindent
557
+ − 1224 \begin{proof}
+ − 1225 By a reverse induction on the string $s$.
+ − 1226 One rewriting step, as we mentioned earlier,
+ − 1227 involves
+ − 1228 \begin{center}
+ − 1229 $\rsimpalts \; (\map \; (\_ \backslash x) \;
+ − 1230 (\rdistinct{(\rflts \; (\map \; (\rsimp{} \; \circ \;
+ − 1231 (\lambda r. \rderssimp{r}{xs}))))}{\varnothing}))
+ − 1232 \sequal
+ − 1233 \rsimpalts \; (\rdistinct{(\map \; (\_ \backslash x) \;
593
+ − 1234 (\rflts \; (\map \; (\rsimp{} \; \circ \;
557
+ − 1235 (\lambda r. \rderssimp{r}{xs})))) ) }{\varnothing}) $.
+ − 1236 \end{center}
+ − 1237 This can be proven by a combination of
+ − 1238 \ref{grewritesSimpalts}, \ref{gstarRdistinctGeneral}, \ref{rderRsimpAltsCommute}, and
+ − 1239 \ref{insideSimpRemoval}.
+ − 1240 \end{proof}
+ − 1241 \noindent
+ − 1242 This closed form has a variant which can be more convenient in later proofs:
559
+ − 1243 \begin{corollary}{altsClosedForm1}
557
+ − 1244 If $s \neq []$ then
+ − 1245 $\rderssimp \; (\sum \; rs) \; s =
+ − 1246 \rsimp{(\sum \; (\map \; \rderssimp{\_}{s} \; rs))}$.
+ − 1247 \end{corollary}
+ − 1248 \noindent
+ − 1249 The harder closed forms are the sequence and star ones.
+ − 1250 Before we go on to obtain them, some preliminary definitions
+ − 1251 are needed to make proof statements concise.
556
+ − 1252
558
+ − 1253 \section{"Closed Forms" of Sequence Regular Expressions}
+ − 1254 The problem of obataining a closed-form for sequence regular expression
+ − 1255 is constructing $(r_1 \cdot r_2) \backslash_r s$
+ − 1256 if we are only allowed to use a combination of $r_1 \backslash s''$
+ − 1257 and $r_2 \backslash s''$ , where $s''$ is from $s$.
+ − 1258 First let's look at a series of derivatives steps on a sequence
+ − 1259 regular expression, assuming that each time the first
+ − 1260 component of the sequence is always nullable):
557
+ − 1261 \begin{center}
558
+ − 1262
593
+ − 1263 $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$\\
+ − 1264 $((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
+ − 1265 \ldots$
558
+ − 1266
557
+ − 1267 \end{center}
558
+ − 1268 Roughly speaking $r_1 \cdot r_2 \backslash s$ can be expresssed as
+ − 1269 a giant alternative taking a list of terms
+ − 1270 $[r_1 \backslash_r s \cdot r_2, r_2 \backslash_r s'', r_2 \backslash_r s_1'', \ldots]$,
+ − 1271 where the head of the list is always the term
+ − 1272 representing a match involving only $r_1$, and the tail of the list consisting of
+ − 1273 terms of the shape $r_2 \backslash_r s''$, $s''$ being a suffix of $s$.
557
+ − 1274 This intuition is also echoed by IndianPaper, where they gave
+ − 1275 a pencil-and-paper derivation of $(r_1 \cdot r_2)\backslash s$:
532
+ − 1276 \begin{center}
558
+ − 1277 \begin{tabular}{c}
593
+ − 1278 $(r_1 \cdot r_2) \backslash_r (c_1 :: c_2 :: \ldots c_n) \myequiv$\\
+ − 1279 \rule{0pt}{3ex} $((r_1 \backslash_r c_1) \cdot r_2 + (\delta\; (\rnullable \; r_1) \; r_2 \backslash_r c_1)) \backslash_r (c_2 :: \ldots c_n)
+ − 1280 \myequiv$\\
+ − 1281 \rule{0pt}{3ex} $((r_1 \backslash_r c_1c_2 \cdot r_2 + (\delta \; (\rnullable \; r_1) \; r_2 \backslash_r c_1c_2))
+ − 1282 + (\delta \ (\rnullable \; r_1 \backslash_r c)\; r_2 \backslash_r c_2)) \backslash_r (c_3 \ldots c_n)
+ − 1283 $
558
+ − 1284 \end{tabular}
557
+ − 1285 \end{center}
+ − 1286 \noindent
558
+ − 1287 The equality in above should be interpretated
+ − 1288 as language equivalence.
+ − 1289 The $\delta$ function works similarly to that of
+ − 1290 a Kronecker delta function:
+ − 1291 \[ \delta \; b\; r\]
+ − 1292 will produce $r$
+ − 1293 if $b$ evaluates to true,
+ − 1294 and $\RZERO$ otherwise.
+ − 1295 Note that their formulation
+ − 1296 \[
+ − 1297 ((r_1 \backslash_r \, c_1c_2 \cdot r_2 + (\delta \; (\rnullable) \; r_1, r_2 \backslash_r c_1c_2)
+ − 1298 + (\delta \; (\rnullable \; r_1 \backslash_r c)\; r_2 \backslash_r c_2)
+ − 1299 \]
+ − 1300 does not faithfully
+ − 1301 represent what the intermediate derivatives would actually look like
+ − 1302 when one or more intermediate results $r_1 \backslash s' \cdot r_2$ are not
+ − 1303 nullable in the head of the sequence.
+ − 1304 For example, when $r_1$ and $r_1 \backslash_r c_1$ are not nullable,
+ − 1305 the regular expression would not look like
+ − 1306 \[
+ − 1307 (r_1 \backslash_r c_1c_2 + \RZERO ) + \RZERO,
+ − 1308 \]
+ − 1309 but actually $r_1 \backslash_r c_1c_2$, the redundant $\RZERO$s will not be created in the
+ − 1310 first place.
+ − 1311 In a closed-form one would want to take into account this
+ − 1312 and generate the list of
+ − 1313 regular expressions $r_2 \backslash_r s''$ with
+ − 1314 string pairs $(s', s'')$ where $s'@s'' = s$ and
+ − 1315 $r_1 \backslash s'$ nullable.
+ − 1316 We denote the list consisting of such
+ − 1317 strings $s''$ as $\vsuf{s}{r_1}$.
+ − 1318
+ − 1319 The function $\vsuf{\_}{\_}$ is defined recursively on the structure of the string:
+ − 1320 \begin{center}
593
+ − 1321 \begin{tabular}{lcl}
+ − 1322 $\vsuf{[]}{\_} $ & $=$ & $[]$\\
+ − 1323 $\vsuf{c::cs}{r_1}$ & $ =$ & $ \textit{if} (\rnullable{r_1}) \textit{then} \; (\vsuf{cs}{(\rder{c}{r_1})}) @ [c :: cs]$\\
+ − 1324 && $\textit{else} \; (\vsuf{cs}{(\rder{c}{r_1}) }) $
+ − 1325 \end{tabular}
558
+ − 1326 \end{center}
+ − 1327 \noindent
+ − 1328 The list is sorted in the order $r_2\backslash s''$
+ − 1329 appears in $(r_1\cdot r_2)\backslash s$.
+ − 1330 In essence, $\vsuf{\_}{\_}$ is doing a
+ − 1331 "virtual derivative" of $r_1 \cdot r_2$, but instead of producing
+ − 1332 the entire result $(r_1 \cdot r_2) \backslash s$,
+ − 1333 it only stores all the strings $s''$ such that $r_2 \backslash s''$
+ − 1334 are occurring terms in $(r_1\cdot r_2)\backslash s$.
+ − 1335
+ − 1336 To make the closed form representation
+ − 1337 more straightforward,
+ − 1338 the flattetning function $\sflat{\_}$ is used to enable the transformation from
557
+ − 1339 a left-associative nested sequence of alternatives into
+ − 1340 a flattened list:
558
+ − 1341 \[
593
+ − 1342 \sum [r_1, r_2, r_3, \ldots] \stackrel{\sflat{\_}}{\rightarrow}
+ − 1343 (\ldots ((r_1 + r_2) + r_3) + \ldots)
558
+ − 1344 \]
+ − 1345 \noindent
+ − 1346 The definitions $\sflat{\_}$, $\sflataux{\_}$ are given below.
593
+ − 1347 \begin{center}
+ − 1348 \begin{tabular}{ccc}
+ − 1349 $\sflataux{\AALTS{ }{r :: rs}}$ & $=$ & $\sflataux{r} @ rs$\\
+ − 1350 $\sflataux{\AALTS{ }{[]}}$ & $ = $ & $ []$\\
+ − 1351 $\sflataux r$ & $=$ & $ [r]$
+ − 1352 \end{tabular}
532
+ − 1353 \end{center}
+ − 1354
593
+ − 1355 \begin{center}
+ − 1356 \begin{tabular}{ccc}
+ − 1357 $\sflat{(\sum r :: rs)}$ & $=$ & $\sum (\sflataux{r} @ rs)$\\
+ − 1358 $\sflat{\sum []}$ & $ = $ & $ \sum []$\\
+ − 1359 $\sflat r$ & $=$ & $ r$
+ − 1360 \end{tabular}
557
+ − 1361 \end{center}
558
+ − 1362 \noindent
576
+ − 1363 $\sflataux{\_}$ breaks up nested alternative regular expressions
557
+ − 1364 of the $(\ldots((r_1 + r_2) + r_3) + \ldots )$(left-associated) shape
558
+ − 1365 into a "balanced" list: $\AALTS{\_}{[r_1,\, r_2 ,\, r_3, \ldots]}$.
557
+ − 1366 It will return the singleton list $[r]$ otherwise.
+ − 1367 $\sflat{\_}$ works the same as $\sflataux{\_}$, except that it keeps
+ − 1368 the output type a regular expression, not a list.
558
+ − 1369 $\sflataux{\_}$ and $\sflat{\_}$ are only recursive on the
+ − 1370 first element of the list.
+ − 1371
+ − 1372 With $\sflataux{}$ a preliminary to the closed form can be stated,
+ − 1373 where the derivative of $r_1 \cdot r_2 \backslash s$ can be
+ − 1374 flattened into a list whose head and tail meet the description
+ − 1375 we gave earlier.
+ − 1376 \begin{lemma}\label{seqSfau0}
+ − 1377 $\sflataux{\rders{(r_1 \cdot r_2) \backslash s }} = (r_1 \backslash_r s) \cdot r_2
+ − 1378 :: (\map \; (r_2 \backslash_r \_) \; (\textit{Suffix} \; s \; r1))$
+ − 1379 \end{lemma}
+ − 1380 \begin{proof}
+ − 1381 By an induction on the string $s$, where the inductive cases
+ − 1382 are split as $[]$ and $xs @ [x]$.
+ − 1383 Note the key identify holds:
+ − 1384 \[
+ − 1385 \map \; (r_2 \backslash_r \_) \; (\vsuf{[x]}{(r_1 \backslash_r xs)}) \;\; @ \;\;
+ − 1386 \map \; (\_ \backslash_r x) \; (\map \; (r_2 \backslash \_) \; (\vsuf{xs}{r_1}))
+ − 1387 \]
593
+ − 1388 =
558
+ − 1389 \[
+ − 1390 \map \; (r_2 \backslash_r \_) \; (\vsuf{xs @ [x]}{r_1})
+ − 1391 \]
+ − 1392 This enables the inductive case to go through.
+ − 1393 \end{proof}
+ − 1394 \noindent
+ − 1395 Note that this lemma does $\mathbf{not}$ depend on any
+ − 1396 specific definitions we used,
+ − 1397 allowing people investigating derivatives to get an alternative
+ − 1398 view of what $r_1 \cdot r_2$ is.
532
+ − 1399
558
+ − 1400 Now we are able to use this for the intuition that
+ − 1401 the different ways in which regular expressions are
+ − 1402 nested do not matter under $\rsimp{}$:
557
+ − 1403 \begin{center}
558
+ − 1404 $\rsimp{r} \stackrel{?}{\sequal} \rsimp{r'}$ if $r = \sum [r_1, r_2, r_3, \ldots]$
593
+ − 1405 and $r' =(\ldots ((r_1 + r_2) + r_3) + \ldots)$
557
+ − 1406 \end{center}
558
+ − 1407 Simply wrap with $\sum$ constructor and add
+ − 1408 simplifications to both sides of \ref{seqSfau0}
+ − 1409 and one gets
+ − 1410 \begin{corollary}\label{seqClosedFormGeneral}
+ − 1411 $\rsimp{\sflat{(r_1 \cdot r_2) \backslash s} }
+ − 1412 =\rsimp{(\sum ( (r_1 \backslash s) \cdot r_2 ::
593
+ − 1413 \map\; (r_2 \backslash \_) \; (\vsuf{s}{r_1})))}$
558
+ − 1414 \end{corollary}
+ − 1415 Together with the idempotency property of $\rsimp{}$ (lemma \ref{rsimpIdem}),
+ − 1416 it is possible to convert the above lemma to obtain a "closed form"
+ − 1417 for derivatives nested with simplification:
+ − 1418 \begin{lemma}\label{seqClosedForm}
+ − 1419 $\rderssimp{(r_1 \cdot r_2)}{s} = \rsimp{(\sum ((r_1 \backslash s) \cdot r_2 )
+ − 1420 :: (\map \; (r_2 \backslash \_) (\vsuf{s}{r_1})))}$
+ − 1421 \end{lemma}
+ − 1422 \begin{proof}
+ − 1423 By a case analysis of string $s$.
+ − 1424 When $s$ is empty list, the rewrite is straightforward.
+ − 1425 When $s$ is a list, one could use the corollary \ref{seqSfau0},
+ − 1426 and lemma \ref{Simpders} to rewrite the left-hand-side.
+ − 1427 \end{proof}
+ − 1428 As a corollary for this closed form, one can estimate the size
+ − 1429 of the sequence derivative $r_1 \cdot r_2 \backslash_r s$ using
+ − 1430 an easier-to-handle expression:
+ − 1431 \begin{corollary}\label{seqEstimate1}
+ − 1432 \begin{center}
557
+ − 1433
593
+ − 1434 $\llbracket \rderssimp{(r_1 \cdot r_2)}{s} \rrbracket_r = \llbracket \rsimp{(\sum ((r_1 \backslash s) \cdot r_2 )
+ − 1435 :: (\map \; (r_2 \backslash \_) (\vsuf{s}{r_1})))} \rrbracket_r$
+ − 1436
558
+ − 1437 \end{center}
+ − 1438 \end{corollary}
+ − 1439 \noindent
+ − 1440 \subsection{Closed Forms for Star Regular Expressions}
564
+ − 1441 We have shown how to control the size of the sequence regular expression $r_1\cdot r_2$ using
+ − 1442 the "closed form" of $(r_1 \cdot r_2) \backslash s$ and then
+ − 1443 the property of the $\distinct$ function.
+ − 1444 Now we try to get a bound on $r^* \backslash s$ as well.
+ − 1445 Again, we first look at how a star's derivatives evolve, if they grow maximally:
+ − 1446 \begin{center}
+ − 1447
593
+ − 1448 $r^* \quad \longrightarrow_{\backslash c} \quad (r\backslash c) \cdot r^* \quad \longrightarrow_{\backslash c'} \quad
+ − 1449 r \backslash cc' \cdot r^* + r \backslash c' \cdot r^* \quad \longrightarrow_{\backslash c''} \quad
+ − 1450 (r_1 \backslash cc'c'' \cdot r^* + r \backslash c'') + (r \backslash c'c'' \cdot r^* + r \backslash c'' \cdot r^*) \quad \longrightarrow_{\backslash c'''}
+ − 1451 \quad \ldots$
564
+ − 1452
+ − 1453 \end{center}
+ − 1454 When we have a string $s = c :: c' :: c'' \ldots$ such that $r \backslash c$, $r \backslash cc'$, $r \backslash c'$,
+ − 1455 $r \backslash cc'c''$, $r \backslash c'c''$, $r\backslash c''$ etc. are all nullable,
+ − 1456 the number of terms in $r^* \backslash s$ will grow exponentially, causing the size
+ − 1457 of the derivatives $r^* \backslash s$ to grow exponentially, even if we do not
+ − 1458 count the possible size explosions of $r \backslash c$ themselves.
+ − 1459
576
+ − 1460 Thanks to $\rflts$ and $\rDistinct$, we are able to open up regular expressions like
564
+ − 1461 $(r_1 \backslash cc'c'' \cdot r^* + r \backslash c'') +
+ − 1462 (r \backslash c'c'' \cdot r^* + r \backslash c'' \cdot r^*) $
+ − 1463 into $\RALTS{[r_1 \backslash cc'c'' \cdot r^*, r \backslash c'',
+ − 1464 r \backslash c'c'' \cdot r^*, r \backslash c'' \cdot r^*]}$
+ − 1465 and then de-duplicate terms of the form $r\backslash s' \cdot r^*$ ($s'$ being a substring of $s$).
+ − 1466 This allows us to use a similar technique as $r_1 \cdot r_2$ case,
+ − 1467 where the crux is to get an equivalent form of
+ − 1468 $\rderssimp{r^*}{s}$ with shape $\rsimp{\sum rs}$.
+ − 1469 This requires generating
558
+ − 1470 all possible sub-strings $s'$ of $s$
+ − 1471 such that $r\backslash s' \cdot r^*$ will appear
+ − 1472 as a term in $(r^*) \backslash s$.
+ − 1473 The first function we define is a single-step
+ − 1474 updating function $\starupdate$, which takes three arguments as input:
+ − 1475 the new character $c$ to take derivative with,
+ − 1476 the regular expression
+ − 1477 $r$ directly under the star $r^*$, and the
+ − 1478 list of strings $sSet$ for the derivative $r^* \backslash s$
+ − 1479 up til this point
+ − 1480 such that $(r^*) \backslash s = \sum_{s' \in sSet} (r\backslash s') \cdot r^*$
+ − 1481 (the equality is not exact, more on this later).
+ − 1482 \begin{center}
+ − 1483 \begin{tabular}{lcl}
+ − 1484 $\starupdate \; c \; r \; [] $ & $\dn$ & $[]$\\
+ − 1485 $\starupdate \; c \; r \; (s :: Ss)$ & $\dn$ & \\
+ − 1486 & & $\textit{if} \;
+ − 1487 (\rnullable \; (\rders \; r \; s))$ \\
+ − 1488 & & $\textit{then} \;\; (s @ [c]) :: [c] :: (
+ − 1489 \starupdate \; c \; r \; Ss)$ \\
+ − 1490 & & $\textit{else} \;\; (s @ [c]) :: (
+ − 1491 \starupdate \; c \; r \; Ss)$
+ − 1492 \end{tabular}
+ − 1493 \end{center}
+ − 1494 \noindent
+ − 1495 As a generalisation from characters to strings,
+ − 1496 $\starupdates$ takes a string instead of a character
+ − 1497 as the first input argument, and is otherwise the same
+ − 1498 as $\starupdate$.
+ − 1499 \begin{center}
+ − 1500 \begin{tabular}{lcl}
+ − 1501 $\starupdates \; [] \; r \; Ss$ & $=$ & $Ss$\\
+ − 1502 $\starupdates \; (c :: cs) \; r \; Ss$ & $=$ & $\starupdates \; cs \; r \; (
+ − 1503 \starupdate \; c \; r \; Ss)$
+ − 1504 \end{tabular}
+ − 1505 \end{center}
+ − 1506 \noindent
+ − 1507 For the star regular expression,
+ − 1508 its derivatives can be seen as a nested gigantic
+ − 1509 alternative similar to that of sequence regular expression's derivatives,
+ − 1510 and therefore need
+ − 1511 to be ``straightened out" as well.
+ − 1512 The function for this would be $\hflat{}$ and $\hflataux{}$.
+ − 1513 \begin{center}
+ − 1514 \begin{tabular}{lcl}
+ − 1515 $\hflataux{r_1 + r_2}$ & $\dn$ & $\hflataux{r_1} @ \hflataux{r_2}$\\
+ − 1516 $\hflataux{r}$ & $\dn$ & $[r]$
+ − 1517 \end{tabular}
+ − 1518 \end{center}
557
+ − 1519
+ − 1520 \begin{center}
558
+ − 1521 \begin{tabular}{lcl}
+ − 1522 $\hflat{r_1 + r_2}$ & $\dn$ & $\sum (\hflataux {r_1} @ \hflataux {r_2}) $\\
+ − 1523 $\hflat{r}$ & $\dn$ & $r$
+ − 1524 \end{tabular}
+ − 1525 \end{center}
+ − 1526 \noindent
+ − 1527 %MAYBE TODO: introduce createdByStar
564
+ − 1528 Again these definitions are tailor-made for dealing with alternatives that have
+ − 1529 originated from a star's derivatives, so we do not attempt to open up all possible
576
+ − 1530 regular expressions of the form $\RALTS{rs}$, where $\textit{rs}$ might not contain precisely 2
564
+ − 1531 elements.
+ − 1532 We give a predicate for such "star-created" regular expressions:
+ − 1533 \begin{center}
593
+ − 1534 \begin{tabular}{lcr}
+ − 1535 & & $\createdByStar{(\RSEQ{ra}{\RSTAR{rb}}) }$\\
+ − 1536 $\createdByStar{r_1} \land \createdByStar{r_2} $ & $ \Longrightarrow$ & $\createdByStar{(r_1 + r_2)}$
+ − 1537 \end{tabular}
+ − 1538 \end{center}
+ − 1539
+ − 1540 These definitions allows us the flexibility to talk about
+ − 1541 regular expressions in their most convenient format,
+ − 1542 for example, flattened out $\RALTS{[r_1, r_2, \ldots, r_n]} $
+ − 1543 instead of binary-nested: $((r_1 + r_2) + (r_3 + r_4)) + \ldots$.
+ − 1544 These definitions help express that certain classes of syntatically
+ − 1545 distinct regular expressions are actually the same under simplification.
+ − 1546 This is not entirely true for annotated regular expressions:
+ − 1547 %TODO: bsimp bders \neq bderssimp
+ − 1548 \begin{center}
+ − 1549 $(1+ (c\cdot \ASEQ{bs}{c^*}{c} ))$
+ − 1550 \end{center}
+ − 1551 For bit-codes, the order in which simplification is applied
+ − 1552 might cause a difference in the location they are placed.
+ − 1553 If we want something like
+ − 1554 \begin{center}
+ − 1555 $\bderssimp{r}{s} \myequiv \bsimp{\bders{r}{s}}$
+ − 1556 \end{center}
+ − 1557 Some "canonicalization" procedure is required,
+ − 1558 which either pushes all the common bitcodes to nodes
+ − 1559 as senior as possible:
+ − 1560 \begin{center}
+ − 1561 $_{bs}(_{bs_1 @ bs'}r_1 + _{bs_1 @ bs''}r_2) \rightarrow _{bs @ bs_1}(_{bs'}r_1 + _{bs''}r_2) $
+ − 1562 \end{center}
+ − 1563 or does the reverse. However bitcodes are not of interest if we are talking about
+ − 1564 the $\llbracket r \rrbracket$ size of a regex.
+ − 1565 Therefore for the ease and simplicity of producing a
+ − 1566 proof for a size bound, we are happy to restrict ourselves to
+ − 1567 unannotated regular expressions, and obtain such equalities as
+ − 1568 \begin{lemma}
+ − 1569 $\rsimp{r_1 + r_2} = \rsimp{\RALTS{\hflataux{r_1} @ \hflataux{r_2}}}$
+ − 1570 \end{lemma}
+ − 1571
+ − 1572 \begin{proof}
+ − 1573 By using the rewriting relation $\rightsquigarrow$
+ − 1574 \end{proof}
+ − 1575 %TODO: rsimp sflat
564
+ − 1576 And from this we obtain a proof that a star's derivative will be the same
+ − 1577 as if it had all its nested alternatives created during deriving being flattened out:
593
+ − 1578 For example,
+ − 1579 \begin{lemma}
+ − 1580 $\createdByStar{r} \implies \rsimp{r} = \rsimp{\RALTS{\hflataux{r}}}$
+ − 1581 \end{lemma}
+ − 1582 \begin{proof}
+ − 1583 By structural induction on $r$, where the induction rules are these of $\createdByStar{_}$.
+ − 1584 \end{proof}
564
+ − 1585 % The simplification of a flattened out regular expression, provided it comes
+ − 1586 %from the derivative of a star, is the same as the one nested.
593
+ − 1587
564
+ − 1588
+ − 1589
558
+ − 1590 We first introduce an inductive property
+ − 1591 for $\starupdate$ and $\hflataux{\_}$,
+ − 1592 it says if we do derivatives of $r^*$
+ − 1593 with a string that starts with $c$,
+ − 1594 then flatten it out,
+ − 1595 we obtain a list
+ − 1596 of the shape $\sum_{s' \in sSet} (r\backslash_r s') \cdot r^*$,
+ − 1597 where $sSet = \starupdates \; s \; r \; [[c]]$.
+ − 1598 \begin{lemma}\label{starHfauInduct}
+ − 1599 $\hflataux{(\rders{( (\rder{c}{r_0})\cdot(r_0^*))}{s})} =
+ − 1600 \map \; (\lambda s_1. (r_0 \backslash_r s_1) \cdot (r_0^*)) \;
+ − 1601 (\starupdates \; s \; r_0 \; [[c]])$
+ − 1602 \end{lemma}
+ − 1603 \begin{proof}
+ − 1604 By an induction on $s$, the inductive cases
+ − 1605 being $[]$ and $s@[c]$.
+ − 1606 \end{proof}
+ − 1607 \noindent
+ − 1608 Here is a corollary that states the lemma in
+ − 1609 a more intuitive way:
+ − 1610 \begin{corollary}
+ − 1611 $\hflataux{r^* \backslash_r (c::xs)} = \map \; (\lambda s. (r \backslash_r s) \cdot
+ − 1612 (r^*))\; (\starupdates \; c\; r\; [[c]])$
+ − 1613 \end{corollary}
+ − 1614 \noindent
+ − 1615 Note that this is also agnostic of the simplification
+ − 1616 function we defined, and is therefore of more general interest.
+ − 1617
+ − 1618 Now adding the $\rsimp{}$ bit for closed forms,
+ − 1619 we have
+ − 1620 \begin{lemma}
+ − 1621 $a :: rs \grewrites \hflataux{a} @ rs$
+ − 1622 \end{lemma}
+ − 1623 \noindent
+ − 1624 giving us
+ − 1625 \begin{lemma}\label{cbsHfauRsimpeq1}
+ − 1626 $\rsimp{a+b} = \rsimp{(\sum \hflataux{a} @ \hflataux{b})}$.
+ − 1627 \end{lemma}
+ − 1628 \noindent
+ − 1629 This yields
+ − 1630 \begin{lemma}\label{hfauRsimpeq2}
593
+ − 1631 $\rsimp{r} = \rsimp{(\sum \hflataux{r})}$
558
+ − 1632 \end{lemma}
+ − 1633 \noindent
+ − 1634 Together with the rewriting relation
+ − 1635 \begin{lemma}\label{starClosedForm6Hrewrites}
+ − 1636 $\map \; (\lambda s. (\rsimp{r \backslash_r s}) \cdot (r^*)) \; Ss
+ − 1637 \scfrewrites
593
+ − 1638 \map \; (\lambda s. (\rsimp{r \backslash_r s}) \cdot (r^*)) \; Ss$
558
+ − 1639 \end{lemma}
+ − 1640 \noindent
+ − 1641 We obtain the closed form for star regular expression:
+ − 1642 \begin{lemma}\label{starClosedForm}
+ − 1643 $\rderssimp{r^*}{c::s} =
+ − 1644 \rsimp{
+ − 1645 (\sum (\map \; (\lambda s. (\rderssimp{r}{s})\cdot r^*) \;
593
+ − 1646 (\starupdates \; s\; r \; [[c]])
558
+ − 1647 )
593
+ − 1648 )
+ − 1649 }
558
+ − 1650 $
+ − 1651 \end{lemma}
+ − 1652 \begin{proof}
+ − 1653 By an induction on $s$.
+ − 1654 The lemmas \ref{rsimpIdem}, \ref{starHfauInduct}, and \ref{hfauRsimpeq2}
+ − 1655 are used.
+ − 1656 \end{proof}
+ − 1657 \section{Estimating the Closed Forms' sizes}
+ − 1658 We now summarize the closed forms below:
+ − 1659 \begin{itemize}
+ − 1660 \item
593
+ − 1661 $\rderssimp{(\sum rs)}{s} \sequal
+ − 1662 \sum \; (\map \; (\rderssimp{\_}{s}) \; rs)$
558
+ − 1663 \item
593
+ − 1664 $\rderssimp{(r_1 \cdot r_2)}{s} \sequal \sum ((r_1 \backslash s) \cdot r_2 )
+ − 1665 :: (\map \; (r_2 \backslash \_) (\vsuf{s}{r_1}))$
558
+ − 1666 \item
+ − 1667
593
+ − 1668 $\rderssimp{r^*}{c::s} =
+ − 1669 \rsimp{
+ − 1670 (\sum (\map \; (\lambda s. (\rderssimp{r}{s})\cdot r^*) \;
558
+ − 1671 (\starupdates \; s\; r \; [[c]])
593
+ − 1672 )
+ − 1673 )
+ − 1674 }
+ − 1675 $
558
+ − 1676 \end{itemize}
+ − 1677 \noindent
+ − 1678 The closed forms on the left-hand-side
+ − 1679 are all of the same shape: $\rsimp{ (\sum rs)} $.
+ − 1680 Such regular expression will be bounded by the size of $\sum rs'$,
+ − 1681 where every element in $rs'$ is distinct, and each element
+ − 1682 can be described by some inductive sub-structures
+ − 1683 (for example when $r = r_1 \cdot r_2$ then $rs'$
+ − 1684 will be solely comprised of $r_1 \backslash s'$
+ − 1685 and $r_2 \backslash s''$, $s'$ and $s''$ being
+ − 1686 sub-strings of $s$).
+ − 1687 which will each have a size uppder bound
+ − 1688 according to inductive hypothesis, which controls $r \backslash s$.
557
+ − 1689
558
+ − 1690 We elaborate the above reasoning by a series of lemmas
+ − 1691 below, where straightforward proofs are omitted.
532
+ − 1692 \begin{lemma}
558
+ − 1693 If $\forall r \in rs. \rsize{r} $ is less than or equal to $N$,
+ − 1694 and $\textit{length} \; rs$ is less than or equal to $l$,
+ − 1695 then $\rsize{\sum rs}$ is less than or equal to $l*N + 1$.
+ − 1696 \end{lemma}
+ − 1697 \noindent
+ − 1698 If we define all regular expressions with size no
+ − 1699 more than $N$ as $\sizeNregex \; N$:
+ − 1700 \[
+ − 1701 \sizeNregex \; N \dn \{r \mid \rsize{r} \leq N \}
+ − 1702 \]
+ − 1703 Then such set is finite:
+ − 1704 \begin{lemma}\label{finiteSizeN}
+ − 1705 $\textit{isFinite}\; (\sizeNregex \; N)$
+ − 1706 \end{lemma}
+ − 1707 \begin{proof}
+ − 1708 By overestimating the set $\sizeNregex \; N + 1$
+ − 1709 using union of sets like
+ − 1710 $\{r_1 \cdot r_2 \mid r_1 \in A
+ − 1711 \text{and}
593
+ − 1712 r_2 \in A\}
558
+ − 1713 $ where $A = \sizeNregex \; N$.
+ − 1714 \end{proof}
+ − 1715 \noindent
+ − 1716 From this we get a corollary that
+ − 1717 if forall $r \in rs$, $\rsize{r} \leq N$, then the output of
+ − 1718 $\rdistinct{rs}{\varnothing}$ is a list of regular
+ − 1719 expressions of finite size depending on $N$ only.
561
+ − 1720 \begin{corollary}\label{finiteSizeNCorollary}
558
+ − 1721 Assumes that for all $r \in rs. \rsize{r} \leq N$,
+ − 1722 and the cardinality of $\sizeNregex \; N$ is $c_N$
+ − 1723 then$\rsize{\rdistinct{rs}{\varnothing}} \leq c*N$.
+ − 1724 \end{corollary}
+ − 1725 \noindent
+ − 1726 We have proven that the output of $\rdistinct{rs'}{\varnothing}$
+ − 1727 is bounded by a constant $c_N$ depending only on $N$,
+ − 1728 provided that each of $rs'$'s element
+ − 1729 is bounded by $N$.
+ − 1730 We want to apply it to our setting $\rsize{\rsimp{\sum rs}}$.
+ − 1731
+ − 1732 We show how $\rdistinct$ and $\rflts$
+ − 1733 in the simplification function together is at least as
+ − 1734 good as $\rdistinct{}{}$ alone.
+ − 1735 \begin{lemma}\label{interactionFltsDB}
+ − 1736 $\llbracket \rdistinct{(\rflts \; \textit{rs})}{\varnothing} \rrbracket_r
+ − 1737 \leq
+ − 1738 \llbracket \rdistinct{rs}{\varnothing} \rrbracket_r $.
532
+ − 1739 \end{lemma}
558
+ − 1740 \noindent
+ − 1741 The intuition is that if we remove duplicates from the $\textit{LHS}$, at least the same amount of
+ − 1742 duplicates will be removed from the list $\textit{rs}$ in the $\textit{RHS}$.
+ − 1743
+ − 1744 Now this $\rsimp{\sum rs}$ can be estimated using $\rdistinct{rs}{\varnothing}$:
+ − 1745 \begin{lemma}\label{altsSimpControl}
+ − 1746 $\rsize{\rsimp{\sum rs}} \leq \rsize{\rdistinct{rs}{\varnothing}}+ 1$
532
+ − 1747 \end{lemma}
558
+ − 1748 \begin{proof}
+ − 1749 By using \ref{interactionFltsDB}.
+ − 1750 \end{proof}
+ − 1751 \noindent
+ − 1752 which says that the size of regular expression
+ − 1753 is always smaller if we apply the full simplification
+ − 1754 rather than just one component ($\rdistinct{}{}$).
+ − 1755
+ − 1756
+ − 1757 Now we are ready to control the sizes of
+ − 1758 $r_1 \cdot r_2 \backslash s$, $r^* \backslash s$.
+ − 1759 \begin{theorem}
593
+ − 1760 For any regex $r$, $\exists N_r. \forall s. \; \rsize{\rderssimp{r}{s}} \leq N_r$
558
+ − 1761 \end{theorem}
+ − 1762 \noindent
+ − 1763 \begin{proof}
593
+ − 1764 We prove this by induction on $r$. The base cases for $\RZERO$,
+ − 1765 $\RONE $ and $\RCHAR{c}$ are straightforward.
+ − 1766 In the sequence $r_1 \cdot r_2$ case,
+ − 1767 the inductive hypotheses state
+ − 1768 $\exists N_1. \forall s. \; \llbracket \rderssimp{r}{s} \rrbracket \leq N_1$ and
+ − 1769 $\exists N_2. \forall s. \; \llbracket \rderssimp{r_2}{s} \rrbracket \leq N_2$.
562
+ − 1770
593
+ − 1771 When the string $s$ is not empty, we can reason as follows
+ − 1772 %
+ − 1773 \begin{center}
+ − 1774 \begin{tabular}{lcll}
558
+ − 1775 & & $ \llbracket \rderssimp{r_1\cdot r_2 }{s} \rrbracket_r $\\
561
+ − 1776 & $ = $ & $\llbracket \rsimp{(\sum(r_1 \backslash_{rsimp} s \cdot r_2 \; \; :: \; \;
593
+ − 1777 \map \; (r_2\backslash_{rsimp} \_)\; (\vsuf{s}{r})))} \rrbracket_r $ & (1) \\
+ − 1778 & $\leq$ & $\llbracket \rdistinct{(r_1 \backslash_{rsimp} s \cdot r_2 \; \; :: \; \;
+ − 1779 \map \; (r_2\backslash_{rsimp} \_)\; (\vsuf{s}{r}))}{\varnothing} \rrbracket_r + 1$ & (2) \\
+ − 1780 & $\leq$ & $2 + N_1 + \rsize{r_2} + (N_2 * (card\;(\sizeNregex \; N_2)))$ & (3)\\
558
+ − 1781 \end{tabular}
+ − 1782 \end{center}
561
+ − 1783 \noindent
+ − 1784 (1) is by the corollary \ref{seqEstimate1}.
+ − 1785 (2) is by \ref{altsSimpControl}.
+ − 1786 (3) is by \ref{finiteSizeNCorollary}.
562
+ − 1787
+ − 1788
+ − 1789 Combining the cases when $s = []$ and $s \neq []$, we get (4):
+ − 1790 \begin{center}
+ − 1791 \begin{tabular}{lcll}
+ − 1792 $\rsize{(r_1 \cdot r_2) \backslash_r s}$ & $\leq$ &
+ − 1793 $max \; (2 + N_1 +
+ − 1794 \llbracket r_2 \rrbracket_r +
+ − 1795 N_2 * (card\; (\sizeNregex \; N_2))) \; \rsize{r_1\cdot r_2}$ & (4)
+ − 1796 \end{tabular}
+ − 1797 \end{center}
558
+ − 1798
562
+ − 1799 We reason similarly for $\STAR$.
+ − 1800 The inductive hypothesis is
+ − 1801 $\exists N. \forall s. \; \llbracket \rderssimp{r}{s} \rrbracket \leq N$.
564
+ − 1802 Let $n_r = \llbracket r^* \rrbracket_r$.
562
+ − 1803 When $s = c :: cs$ is not empty,
+ − 1804 \begin{center}
593
+ − 1805 \begin{tabular}{lcll}
562
+ − 1806 & & $ \llbracket \rderssimp{r^* }{c::cs} \rrbracket_r $\\
+ − 1807 & $ = $ & $\llbracket \rsimp{(\sum (\map \; (\lambda s. (r \backslash_{rsimp} s) \cdot r^*) \; (\starupdates\;
593
+ − 1808 cs \; r \; [[c]] )) )} \rrbracket_r $ & (5) \\
+ − 1809 & $\leq$ & $\llbracket
+ − 1810 \rdistinct{
+ − 1811 (\map \;
+ − 1812 (\lambda s. (r \backslash_{rsimp} s) \cdot r^*) \;
+ − 1813 (\starupdates\; cs \; r \; [[c]] )
+ − 1814 )}
562
+ − 1815 {\varnothing} \rrbracket_r + 1$ & (6) \\
+ − 1816 & $\leq$ & $1 + (\textit{card} (\sizeNregex \; (N + n_r)))
+ − 1817 * (1 + (N + n_r)) $ & (7)\\
+ − 1818 \end{tabular}
+ − 1819 \end{center}
+ − 1820 \noindent
+ − 1821 (5) is by the lemma \ref{starClosedForm}.
+ − 1822 (6) is by \ref{altsSimpControl}.
+ − 1823 (7) is by \ref{finiteSizeNCorollary}.
+ − 1824 Combining with the case when $s = []$, one gets
+ − 1825 \begin{center}
593
+ − 1826 \begin{tabular}{lcll}
+ − 1827 $\rsize{r^* \backslash_r s}$ & $\leq$ & $max \; n_r \; 1 + (\textit{card} (\sizeNregex \; (N + n_r)))
+ − 1828 * (1 + (N + n_r)) $ & (8)\\
+ − 1829 \end{tabular}
562
+ − 1830 \end{center}
+ − 1831 \noindent
+ − 1832
+ − 1833 The alternative case is slightly less involved.
+ − 1834 The inductive hypothesis
+ − 1835 is equivalent to $\exists N. \forall r \in (\map \; (\_ \backslash_r s) \; rs). \rsize{r} \leq N$.
+ − 1836 In the case when $s = c::cs$, we have
+ − 1837 \begin{center}
593
+ − 1838 \begin{tabular}{lcll}
562
+ − 1839 & & $ \llbracket \rderssimp{\sum rs }{c::cs} \rrbracket_r $\\
+ − 1840 & $ = $ & $\llbracket \rsimp{(\sum (\map \; (\_ \backslash_{rsimp} s) \; rs) )} \rrbracket_r $ & (9) \\
+ − 1841 & $\leq$ & $\llbracket (\sum (\map \; (\_ \backslash_{rsimp} s) \; rs) ) \rrbracket_r $ & (10) \\
+ − 1842 & $\leq$ & $1 + N * (length \; rs) $ & (11)\\
593
+ − 1843 \end{tabular}
562
+ − 1844 \end{center}
+ − 1845 \noindent
+ − 1846 (9) is by \ref{altsClosedForm}, (10) by \ref{rsimpSize} and (11) by inductive hypothesis.
+ − 1847
+ − 1848 Combining with the case when $s = []$, one gets
+ − 1849 \begin{center}
593
+ − 1850 \begin{tabular}{lcll}
+ − 1851 $\rsize{\sum rs \backslash_r s}$ & $\leq$ & $max \; \rsize{\sum rs} \; 1+N*(length \; rs)$
+ − 1852 & (12)\\
+ − 1853 \end{tabular}
562
+ − 1854 \end{center}
+ − 1855 (4), (8), and (12) are all the inductive cases proven.
558
+ − 1856 \end{proof}
+ − 1857
564
+ − 1858
+ − 1859 \begin{corollary}
593
+ − 1860 For any regex $a$, $\exists N_r. \forall s. \; \rsize{\bderssimp{a}{s}} \leq N_r$
564
+ − 1861 \end{corollary}
+ − 1862 \begin{proof}
+ − 1863 By \ref{sizeRelations}.
+ − 1864 \end{proof}
558
+ − 1865 \noindent
+ − 1866
+ − 1867 %-----------------------------------
+ − 1868 % SECTION 2
+ − 1869 %-----------------------------------
+ − 1870
532
+ − 1871
557
+ − 1872 %----------------------------------------------------------------------------------------
+ − 1873 % SECTION 3
+ − 1874 %----------------------------------------------------------------------------------------
+ − 1875
532
+ − 1876
554
+ − 1877 \subsection{A Closed Form for the Sequence Regular Expression}
+ − 1878 \noindent
+ − 1879
+ − 1880 Before we get to the proof that says the intermediate result of our lexer will
+ − 1881 remain finitely bounded, which is an important efficiency/liveness guarantee,
+ − 1882 we shall first develop a few preparatory properties and definitions to
+ − 1883 make the process of proving that a breeze.
+ − 1884
+ − 1885 We define rewriting relations for $\rrexp$s, which allows us to do the
+ − 1886 same trick as we did for the correctness proof,
+ − 1887 but this time we will have stronger equalities established.
+ − 1888
532
+ − 1889
+ − 1890
+ − 1891 What guarantee does this bound give us?
+ − 1892
+ − 1893 Whatever the regex is, it will not grow indefinitely.
+ − 1894 Take our previous example $(a + aa)^*$ as an example:
+ − 1895 \begin{center}
593
+ − 1896 \begin{tabular}{@{}c@{\hspace{0mm}}c@{\hspace{0mm}}c@{}}
+ − 1897 \begin{tikzpicture}
+ − 1898 \begin{axis}[
+ − 1899 xlabel={number of $a$'s},
+ − 1900 x label style={at={(1.05,-0.05)}},
+ − 1901 ylabel={regex size},
+ − 1902 enlargelimits=false,
+ − 1903 xtick={0,5,...,30},
+ − 1904 xmax=33,
+ − 1905 ymax= 40,
+ − 1906 ytick={0,10,...,40},
+ − 1907 scaled ticks=false,
+ − 1908 axis lines=left,
+ − 1909 width=5cm,
+ − 1910 height=4cm,
+ − 1911 legend entries={$(a + aa)^*$},
+ − 1912 legend pos=north west,
+ − 1913 legend cell align=left]
+ − 1914 \addplot[red,mark=*, mark options={fill=white}] table {a_aa_star.data};
+ − 1915 \end{axis}
+ − 1916 \end{tikzpicture}
+ − 1917 \end{tabular}
532
+ − 1918 \end{center}
+ − 1919 We are able to limit the size of the regex $(a + aa)^*$'s derivatives
593
+ − 1920 with our simplification
532
+ − 1921 rules very effectively.
+ − 1922
+ − 1923
+ − 1924 In our proof for the inductive case $r_1 \cdot r_2$, the dominant term in the bound
+ − 1925 is $l_{N_2} * N_2$, where $N_2$ is the bound we have for $\llbracket \bderssimp{r_2}{s} \rrbracket$.
+ − 1926 Given that $l_{N_2}$ is roughly the size $4^{N_2}$, the size bound $\llbracket \bderssimp{r_1 \cdot r_2}{s} \rrbracket$
+ − 1927 inflates the size bound of $\llbracket \bderssimp{r_2}{s} \rrbracket$ with the function
+ − 1928 $f(x) = x * 2^x$.
+ − 1929 This means the bound we have will surge up at least
+ − 1930 tower-exponentially with a linear increase of the depth.
+ − 1931 For a regex of depth $n$, the bound
+ − 1932 would be approximately $4^n$.
+ − 1933
+ − 1934 Test data in the graphs from randomly generated regular expressions
+ − 1935 shows that the giant bounds are far from being hit.
+ − 1936 %a few sample regular experessions' derivatives
+ − 1937 %size change
576
+ − 1938 %TODO: giving regex1_size_change.data showing a few regular expressions' size changes
532
+ − 1939 %w;r;t the input characters number, where the size is usually cubic in terms of original size
+ − 1940 %a*, aa*, aaa*, .....
576
+ − 1941 %randomly generated regular expressions
532
+ − 1942 \begin{center}
593
+ − 1943 \begin{tabular}{@{}c@{\hspace{0mm}}c@{\hspace{0mm}}c@{}}
+ − 1944 \begin{tikzpicture}
+ − 1945 \begin{axis}[
+ − 1946 xlabel={number of $a$'s},
+ − 1947 x label style={at={(1.05,-0.05)}},
+ − 1948 ylabel={regex size},
+ − 1949 enlargelimits=false,
+ − 1950 xtick={0,5,...,30},
+ − 1951 xmax=33,
+ − 1952 ymax=1000,
+ − 1953 ytick={0,100,...,1000},
+ − 1954 scaled ticks=false,
+ − 1955 axis lines=left,
+ − 1956 width=5cm,
+ − 1957 height=4cm,
+ − 1958 legend entries={regex1},
+ − 1959 legend pos=north west,
+ − 1960 legend cell align=left]
+ − 1961 \addplot[red,mark=*, mark options={fill=white}] table {regex1_size_change.data};
+ − 1962 \end{axis}
+ − 1963 \end{tikzpicture}
532
+ − 1964 &
593
+ − 1965 \begin{tikzpicture}
+ − 1966 \begin{axis}[
+ − 1967 xlabel={$n$},
+ − 1968 x label style={at={(1.05,-0.05)}},
+ − 1969 %ylabel={time in secs},
+ − 1970 enlargelimits=false,
+ − 1971 xtick={0,5,...,30},
+ − 1972 xmax=33,
+ − 1973 ymax=1000,
+ − 1974 ytick={0,100,...,1000},
+ − 1975 scaled ticks=false,
+ − 1976 axis lines=left,
+ − 1977 width=5cm,
+ − 1978 height=4cm,
+ − 1979 legend entries={regex2},
+ − 1980 legend pos=north west,
+ − 1981 legend cell align=left]
+ − 1982 \addplot[blue,mark=*, mark options={fill=white}] table {regex2_size_change.data};
+ − 1983 \end{axis}
+ − 1984 \end{tikzpicture}
532
+ − 1985 &
593
+ − 1986 \begin{tikzpicture}
+ − 1987 \begin{axis}[
+ − 1988 xlabel={$n$},
+ − 1989 x label style={at={(1.05,-0.05)}},
+ − 1990 %ylabel={time in secs},
+ − 1991 enlargelimits=false,
+ − 1992 xtick={0,5,...,30},
+ − 1993 xmax=33,
+ − 1994 ymax=1000,
+ − 1995 ytick={0,100,...,1000},
+ − 1996 scaled ticks=false,
+ − 1997 axis lines=left,
+ − 1998 width=5cm,
+ − 1999 height=4cm,
+ − 2000 legend entries={regex3},
+ − 2001 legend pos=north west,
+ − 2002 legend cell align=left]
+ − 2003 \addplot[cyan,mark=*, mark options={fill=white}] table {regex3_size_change.data};
+ − 2004 \end{axis}
+ − 2005 \end{tikzpicture}\\
+ − 2006 \multicolumn{3}{c}{Graphs: size change of 3 randomly generated regular expressions $w.r.t.$ input string length.}
+ − 2007 \end{tabular}
532
+ − 2008 \end{center}
+ − 2009 \noindent
+ − 2010 Most of the regex's sizes seem to stay within a polynomial bound $w.r.t$ the
+ − 2011 original size.
591
+ − 2012 We will discuss improvements to this bound in the next chapter.
532
+ − 2013
+ − 2014
+ − 2015
+ − 2016 %----------------------------------------------------------------------------------------
+ − 2017 % SECTION ??
+ − 2018 %----------------------------------------------------------------------------------------
+ − 2019
+ − 2020 %-----------------------------------
+ − 2021 % SECTION syntactic equivalence under simp
+ − 2022 %-----------------------------------
+ − 2023 \section{Syntactic Equivalence Under $\simp$}
+ − 2024 We prove that minor differences can be annhilated
+ − 2025 by $\simp$.
+ − 2026 For example,
+ − 2027 \begin{center}
593
+ − 2028 $\simp \;(\simpALTs\; (\map \;(\_\backslash \; x)\; (\distinct \; \mathit{rs}\; \phi))) =
+ − 2029 \simp \;(\simpALTs \;(\distinct \;(\map \;(\_ \backslash\; x) \; \mathit{rs}) \; \phi))$
532
+ − 2030 \end{center}
+ − 2031
+ − 2032
+ − 2033 %----------------------------------------------------------------------------------------
+ − 2034 % SECTION ALTS CLOSED FORM
+ − 2035 %----------------------------------------------------------------------------------------
+ − 2036 \section{A Closed Form for \textit{ALTS}}
+ − 2037 Now we prove that $rsimp (rders\_simp (RALTS rs) s) = rsimp (RALTS (map (\lambda r. rders\_simp r s) rs))$.
+ − 2038
+ − 2039
+ − 2040 There are a few key steps, one of these steps is
556
+ − 2041
532
+ − 2042
+ − 2043
+ − 2044 One might want to prove this by something a simple statement like:
+ − 2045
+ − 2046 For this to hold we want the $\textit{distinct}$ function to pick up
+ − 2047 the elements before and after derivatives correctly:
+ − 2048 $r \in rset \equiv (rder x r) \in (rder x rset)$.
+ − 2049 which essentially requires that the function $\backslash$ is an injective mapping.
+ − 2050
+ − 2051 Unfortunately the function $\backslash c$ is not an injective mapping.
+ − 2052
+ − 2053 \subsection{function $\backslash c$ is not injective (1-to-1)}
+ − 2054 \begin{center}
593
+ − 2055 The derivative $w.r.t$ character $c$ is not one-to-one.
+ − 2056 Formally,
532
+ − 2057 $\exists r_1 \;r_2. r_1 \neq r_2 \mathit{and} r_1 \backslash c = r_2 \backslash c$
+ − 2058 \end{center}
+ − 2059 This property is trivially true for the
+ − 2060 character regex example:
+ − 2061 \begin{center}
+ − 2062 $r_1 = e; \; r_2 = d;\; r_1 \backslash c = \ZERO = r_2 \backslash c$
+ − 2063 \end{center}
+ − 2064 But apart from the cases where the derivative
+ − 2065 output is $\ZERO$, are there non-trivial results
+ − 2066 of derivatives which contain strings?
+ − 2067 The answer is yes.
+ − 2068 For example,
+ − 2069 \begin{center}
+ − 2070 Let $r_1 = a^*b\;\quad r_2 = (a\cdot a^*)\cdot b + b$.\\
+ − 2071 where $a$ is not nullable.\\
+ − 2072 $r_1 \backslash c = ((a \backslash c)\cdot a^*)\cdot c + b \backslash c$\\
+ − 2073 $r_2 \backslash c = ((a \backslash c)\cdot a^*)\cdot c + b \backslash c$
+ − 2074 \end{center}
576
+ − 2075 We start with two syntactically different regular expressions,
532
+ − 2076 and end up with the same derivative result.
+ − 2077 This is not surprising as we have such
+ − 2078 equality as below in the style of Arden's lemma:\\
+ − 2079 \begin{center}
+ − 2080 $L(A^*B) = L(A\cdot A^* \cdot B + B)$
+ − 2081 \end{center}
+ − 2082
590
+ − 2083 There are two problems with this finiteness result, though.
+ − 2084 \begin{itemize}
+ − 2085 \item
593
+ − 2086 First, It is not yet a direct formalisation of our lexer's complexity,
+ − 2087 as a complexity proof would require looking into
+ − 2088 the time it takes to execute {\bf all} the operations
+ − 2089 involved in the lexer (simp, collect, decode), not just the derivative.
+ − 2090 \item
+ − 2091 Second, the bound is not yet tight, and we seek to improve $N_a$ so that
+ − 2092 it is polynomial on $\llbracket a \rrbracket$.
590
+ − 2093 \end{itemize}
+ − 2094 Still, we believe this contribution is fruitful,
+ − 2095 because
+ − 2096 \begin{itemize}
+ − 2097 \item
+ − 2098
+ − 2099 The size proof can serve as a cornerstone for a complexity
+ − 2100 formalisation.
+ − 2101 Derivatives are the most important phases of our lexer algorithm.
+ − 2102 Size properties about derivatives covers the majority of the algorithm
+ − 2103 and is therefore a good indication of complexity of the entire program.
+ − 2104 \item
+ − 2105 The bound is already a strong indication that catastrophic
+ − 2106 backtracking is much less likely to occur in our $\blexersimp$
+ − 2107 algorithm.
+ − 2108 We refine $\blexersimp$ with $\blexerStrong$ in the next chapter
+ − 2109 so that the bound becomes polynomial.
+ − 2110 \end{itemize}
593
+ − 2111
532
+ − 2112 %----------------------------------------------------------------------------------------
+ − 2113 % SECTION 4
+ − 2114 %----------------------------------------------------------------------------------------
593
+ − 2115
+ − 2116
+ − 2117
+ − 2118
+ − 2119
+ − 2120
+ − 2121
+ − 2122
532
+ − 2123 One might wonder the actual bound rather than the loose bound we gave
+ − 2124 for the convenience of an easier proof.
+ − 2125 How much can the regex $r^* \backslash s$ grow?
+ − 2126 As earlier graphs have shown,
+ − 2127 %TODO: reference that graph where size grows quickly
593
+ − 2128 they can grow at a maximum speed
+ − 2129 exponential $w.r.t$ the number of characters,
532
+ − 2130 but will eventually level off when the string $s$ is long enough.
+ − 2131 If they grow to a size exponential $w.r.t$ the original regex, our algorithm
+ − 2132 would still be slow.
+ − 2133 And unfortunately, we have concrete examples
576
+ − 2134 where such regular expressions grew exponentially large before levelling off:
532
+ − 2135 $(a ^ * + (aa) ^ * + (aaa) ^ * + \ldots +
+ − 2136 (\underbrace{a \ldots a}_{\text{n a's}})^*$ will already have a maximum
593
+ − 2137 size that is exponential on the number $n$
532
+ − 2138 under our current simplification rules:
+ − 2139 %TODO: graph of a regex whose size increases exponentially.
+ − 2140 \begin{center}
593
+ − 2141 \begin{tikzpicture}
+ − 2142 \begin{axis}[
+ − 2143 height=0.5\textwidth,
+ − 2144 width=\textwidth,
+ − 2145 xlabel=number of a's,
+ − 2146 xtick={0,...,9},
+ − 2147 ylabel=maximum size,
+ − 2148 ymode=log,
+ − 2149 log basis y={2}
+ − 2150 ]
+ − 2151 \addplot[mark=*,blue] table {re-chengsong.data};
+ − 2152 \end{axis}
+ − 2153 \end{tikzpicture}
532
+ − 2154 \end{center}
+ − 2155
+ − 2156 For convenience we use $(\oplus_{i=1}^{n} (\underbrace{a \ldots a}_{\text{i a's}})^*)^*$
+ − 2157 to express $(a ^ * + (aa) ^ * + (aaa) ^ * + \ldots +
+ − 2158 (\underbrace{a \ldots a}_{\text{n a's}})^*$ in the below discussion.
+ − 2159 The exponential size is triggered by that the regex
+ − 2160 $\oplus_{i=1}^{n} (\underbrace{a \ldots a}_{\text{i a's}})^*$
+ − 2161 inside the $(\ldots) ^*$ having exponentially many
+ − 2162 different derivatives, despite those difference being minor.
+ − 2163 $(\oplus_{i=1}^{n} (\underbrace{a \ldots a}_{\text{i a's}})^*)^*\backslash \underbrace{a \ldots a}_{\text{m a's}}$
+ − 2164 will therefore contain the following terms (after flattening out all nested
+ − 2165 alternatives):
+ − 2166 \begin{center}
593
+ − 2167 $(\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}})^*)$\\
+ − 2168 $(1 \leq m' \leq m )$
532
+ − 2169 \end{center}
+ − 2170 These terms are distinct for $m' \leq L.C.M.(1, \ldots, n)$ (will be explained in appendix).
593
+ − 2171 With each new input character taking the derivative against the intermediate result, more and more such distinct
+ − 2172 terms will accumulate,
532
+ − 2173 until the length reaches $L.C.M.(1, \ldots, n)$.
+ − 2174 $\textit{distinctBy}$ will not be able to de-duplicate any two of these terms
+ − 2175 $(\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}})^*)^*$\\
+ − 2176
+ − 2177 $(\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}})^*)^*$\\
593
+ − 2178 where $m' \neq m''$ \\
+ − 2179 as they are slightly different.
+ − 2180 This means that with our current simplification methods,
+ − 2181 we will not be able to control the derivative so that
+ − 2182 $\llbracket \bderssimp{r}{s} \rrbracket$ stays polynomial %\leq O((\llbracket r\rrbacket)^c)$
+ − 2183 as there are already exponentially many terms.
+ − 2184 These terms are similar in the sense that the head of those terms
+ − 2185 are all consisted of sub-terms of the form:
+ − 2186 $(\underbrace{a \ldots a}_{\text{j a's}})\cdot (\underbrace{a \ldots a}_{\text{i a's}})^* $.
+ − 2187 For $\oplus_{i=1}^{n} (\underbrace{a \ldots a}_{\text{i a's}})^*$, there will be at most
+ − 2188 $n * (n + 1) / 2$ such terms.
+ − 2189 For example, $(a^* + (aa)^* + (aaa)^*) ^*$'s derivatives
+ − 2190 can be described by 6 terms:
+ − 2191 $a^*$, $a\cdot (aa)^*$, $ (aa)^*$,
+ − 2192 $aa \cdot (aaa)^*$, $a \cdot (aaa)^*$, and $(aaa)^*$.
532
+ − 2193 The total number of different "head terms", $n * (n + 1) / 2$,
593
+ − 2194 is proportional to the number of characters in the regex
532
+ − 2195 $(\oplus_{i=1}^{n} (\underbrace{a \ldots a}_{\text{i a's}})^*)^*$.
+ − 2196 This suggests a slightly different notion of size, which we call the
+ − 2197 alphabetic width:
+ − 2198 %TODO:
+ − 2199 (TODO: Alphabetic width def.)
+ − 2200
593
+ − 2201
532
+ − 2202 Antimirov\parencite{Antimirov95} has proven that
+ − 2203 $\textit{PDER}_{UNIV}(r) \leq \textit{awidth}(r)$.
+ − 2204 where $\textit{PDER}_{UNIV}(r)$ is a set of all possible subterms
+ − 2205 created by doing derivatives of $r$ against all possible strings.
+ − 2206 If we can make sure that at any moment in our lexing algorithm our
+ − 2207 intermediate result hold at most one copy of each of the
+ − 2208 subterms then we can get the same bound as Antimirov's.
+ − 2209 This leads to the algorithm in the next chapter.
+ − 2210
+ − 2211
+ − 2212
+ − 2213
+ − 2214
+ − 2215 %----------------------------------------------------------------------------------------
+ − 2216 % SECTION 1
+ − 2217 %----------------------------------------------------------------------------------------
+ − 2218
+ − 2219
+ − 2220 %-----------------------------------
+ − 2221 % SUBSECTION 1
+ − 2222 %-----------------------------------
+ − 2223 \subsection{Syntactic Equivalence Under $\simp$}
+ − 2224 We prove that minor differences can be annhilated
+ − 2225 by $\simp$.
+ − 2226 For example,
+ − 2227 \begin{center}
593
+ − 2228 $\simp \;(\simpALTs\; (\map \;(\_\backslash \; x)\; (\distinct \; \mathit{rs}\; \phi))) =
+ − 2229 \simp \;(\simpALTs \;(\distinct \;(\map \;(\_ \backslash\; x) \; \mathit{rs}) \; \phi))$
532
+ − 2230 \end{center}
+ − 2231