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