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