|
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 |
|
|
618
|
10 |
|
|
624
|
11 |
In this chapter we give a bound in terms of size of
|
|
|
12 |
the calculated derivatives:
|
|
590
|
13 |
given an annotated regular expression $a$, for any string $s$
|
|
624
|
14 |
our algorithm $\blexersimp$'s derivatives
|
|
|
15 |
are finitely bounded
|
|
618
|
16 |
by a constant that only depends on $a$.
|
|
|
17 |
Formally we show that there exists an $N_a$ such that
|
|
576
|
18 |
\begin{center}
|
|
593
|
19 |
$\llbracket \bderssimp{a}{s} \rrbracket \leq N_a$
|
|
576
|
20 |
\end{center}
|
|
|
21 |
\noindent
|
|
618
|
22 |
where the size ($\llbracket \_ \rrbracket$) of
|
|
|
23 |
an annotated regular expression is defined
|
|
|
24 |
in terms of the number of nodes in its
|
|
|
25 |
tree structure (its recursive definition given in the next page).
|
|
613
|
26 |
We believe this size bound
|
|
|
27 |
is important in the context of POSIX lexing, because
|
|
590
|
28 |
\begin{itemize}
|
|
|
29 |
\item
|
|
618
|
30 |
It is a stepping stone towards the goal
|
|
|
31 |
of eliminating ``catastrophic backtracking''.
|
|
|
32 |
If the internal data structures used by our algorithm
|
|
|
33 |
grows beyond a finite bound, then clearly
|
|
|
34 |
the algorithm (which traverses these structures) will
|
|
|
35 |
be slow.
|
|
624
|
36 |
The next step is to refine the bound $N_a$ so that it
|
|
|
37 |
is not just finite but polynomial in $\llbracket a\rrbracket$.
|
|
590
|
38 |
\item
|
|
618
|
39 |
Having the finite bound formalised
|
|
|
40 |
gives us a higher confidence that
|
|
590
|
41 |
our simplification algorithm $\simp$ does not ``mis-behave''
|
|
639
|
42 |
like $\textit{simpSL}$ does.
|
|
618
|
43 |
The bound is universal for a given regular expression,
|
|
|
44 |
which is an advantage over work which
|
|
624
|
45 |
only gives empirical evidence on
|
|
639
|
46 |
some test cases (see for example Verbatim work \cite{Verbatimpp}).
|
|
590
|
47 |
\end{itemize}
|
|
625
|
48 |
\noindent
|
|
|
49 |
We then extend our $\blexersimp$
|
|
|
50 |
to support bounded repetitions ($r^{\{n\}}$).
|
|
|
51 |
We update our formalisation of
|
|
|
52 |
the correctness and finiteness properties to
|
|
|
53 |
include this new construct.
|
|
639
|
54 |
We show that we can out-compete other verified lexers such as
|
|
625
|
55 |
Verbatim++ on bounded regular expressions.
|
|
|
56 |
|
|
618
|
57 |
In the next section we describe in more detail
|
|
|
58 |
what the finite bound means in our algorithm
|
|
|
59 |
and why the size of the internal data structures of
|
|
|
60 |
a typical derivative-based lexer such as
|
|
639
|
61 |
Sulzmann and Lu's needs formal treatment.
|
|
618
|
62 |
|
|
625
|
63 |
|
|
|
64 |
|
|
|
65 |
|
|
639
|
66 |
\section{Formalising Size Bound of Derivatives}
|
|
577
|
67 |
\noindent
|
|
613
|
68 |
In our lexer ($\blexersimp$),
|
|
|
69 |
we take an annotated regular expression as input,
|
|
618
|
70 |
and repeately take derivative of and simplify it.
|
|
|
71 |
\begin{figure}
|
|
|
72 |
\begin{center}
|
|
|
73 |
\begin{tabular}{lcl}
|
|
|
74 |
$\llbracket _{bs}\ONE \rrbracket$ & $\dn$ & $1$\\
|
|
|
75 |
$\llbracket \ZERO \rrbracket$ & $\dn$ & $1$ \\
|
|
|
76 |
$\llbracket _{bs} r_1 \cdot r_2 \rrbracket$ & $\dn$ & $\llbracket r_1 \rrbracket + \llbracket r_2 \rrbracket + 1$\\
|
|
|
77 |
$\llbracket _{bs}\mathbf{c} \rrbracket $ & $\dn$ & $1$\\
|
|
|
78 |
$\llbracket _{bs}\sum as \rrbracket $ & $\dn$ & $\map \; (\llbracket \_ \rrbracket)\; as + 1$\\
|
|
|
79 |
$\llbracket _{bs} a^* \rrbracket $ & $\dn$ & $\llbracket a \rrbracket + 1$.
|
|
|
80 |
\end{tabular}
|
|
|
81 |
\end{center}
|
|
|
82 |
\caption{The size function of bitcoded regular expressions}\label{brexpSize}
|
|
|
83 |
\end{figure}
|
|
|
84 |
|
|
|
85 |
\begin{figure}
|
|
593
|
86 |
\begin{tikzpicture}[scale=2,
|
|
|
87 |
every node/.style={minimum size=11mm},
|
|
|
88 |
->,>=stealth',shorten >=1pt,auto,thick
|
|
|
89 |
]
|
|
|
90 |
\node (r0) [rectangle, draw=black, thick, minimum size = 5mm, draw=blue] {$a$};
|
|
|
91 |
\node (r1) [rectangle, draw=black, thick, right=of r0, minimum size = 7mm]{$a_1$};
|
|
|
92 |
\draw[->,line width=0.2mm](r0)--(r1) node[above,midway] {$\backslash c_1$};
|
|
590
|
93 |
|
|
593
|
94 |
\node (r1s) [rectangle, draw=blue, thick, right=of r1, minimum size=6mm]{$a_{1s}$};
|
|
|
95 |
\draw[->, line width=0.2mm](r1)--(r1s) node[above, midway] {$\simp$};
|
|
590
|
96 |
|
|
593
|
97 |
\node (r2) [rectangle, draw=black, thick, right=of r1s, minimum size = 12mm]{$a_2$};
|
|
|
98 |
\draw[->,line width=0.2mm](r1s)--(r2) node[above,midway] {$\backslash c_2$};
|
|
590
|
99 |
|
|
593
|
100 |
\node (r2s) [rectangle, draw = blue, thick, right=of r2,minimum size=6mm]{$a_{2s}$};
|
|
|
101 |
\draw[->,line width=0.2mm](r2)--(r2s) node[above,midway] {$\simp$};
|
|
590
|
102 |
|
|
593
|
103 |
\node (rns) [rectangle, draw = blue, thick, right=of r2s,minimum size=6mm]{$a_{ns}$};
|
|
|
104 |
\draw[->,line width=0.2mm, dashed](r2s)--(rns) node[above,midway] {$\backslash \ldots$};
|
|
590
|
105 |
|
|
593
|
106 |
\node (v) [circle, thick, draw, right=of rns, minimum size=6mm, right=1.7cm]{$v$};
|
|
|
107 |
\draw[->, line width=0.2mm](rns)--(v) node[above, midway] {\bmkeps} node [below, midway] {\decode};
|
|
|
108 |
\end{tikzpicture}
|
|
|
109 |
\caption{Regular expression size change during our $\blexersimp$ algorithm}\label{simpShrinks}
|
|
590
|
110 |
\end{figure}
|
|
618
|
111 |
|
|
576
|
112 |
\noindent
|
|
590
|
113 |
Each time
|
|
613
|
114 |
a derivative is taken, the regular expression might grow.
|
|
639
|
115 |
However, the simplification that is immediately afterwards will often shrink it so that
|
|
|
116 |
the overall size of the derivatives stays relatively small.
|
|
577
|
117 |
This intuition is depicted by the relative size
|
|
590
|
118 |
change between the black and blue nodes:
|
|
639
|
119 |
After $\simp$ the node shrinks.
|
|
618
|
120 |
Our proof states that all the blue nodes
|
|
613
|
121 |
stay below a size bound $N_a$ determined by the input $a$.
|
|
576
|
122 |
|
|
590
|
123 |
\noindent
|
|
613
|
124 |
Sulzmann and Lu's assumed a similar picture about their algorithm,
|
|
590
|
125 |
though in fact their algorithm's size might be better depicted by the following graph:
|
|
|
126 |
\begin{figure}[H]
|
|
593
|
127 |
\begin{tikzpicture}[scale=2,
|
|
|
128 |
every node/.style={minimum size=11mm},
|
|
|
129 |
->,>=stealth',shorten >=1pt,auto,thick
|
|
|
130 |
]
|
|
|
131 |
\node (r0) [rectangle, draw=black, thick, minimum size = 5mm, draw=blue] {$a$};
|
|
|
132 |
\node (r1) [rectangle, draw=black, thick, right=of r0, minimum size = 7mm]{$a_1$};
|
|
|
133 |
\draw[->,line width=0.2mm](r0)--(r1) node[above,midway] {$\backslash c_1$};
|
|
590
|
134 |
|
|
593
|
135 |
\node (r1s) [rectangle, draw=blue, thick, right=of r1, minimum size=7mm]{$a_{1s}$};
|
|
|
136 |
\draw[->, line width=0.2mm](r1)--(r1s) node[above, midway] {$\simp'$};
|
|
590
|
137 |
|
|
593
|
138 |
\node (r2) [rectangle, draw=black, thick, right=of r1s, minimum size = 17mm]{$a_2$};
|
|
|
139 |
\draw[->,line width=0.2mm](r1s)--(r2) node[above,midway] {$\backslash c_2$};
|
|
590
|
140 |
|
|
593
|
141 |
\node (r2s) [rectangle, draw = blue, thick, right=of r2,minimum size=14mm]{$a_{2s}$};
|
|
|
142 |
\draw[->,line width=0.2mm](r2)--(r2s) node[above,midway] {$\simp'$};
|
|
590
|
143 |
|
|
593
|
144 |
\node (r3) [rectangle, draw = black, thick, right= of r2s, minimum size = 22mm]{$a_3$};
|
|
|
145 |
\draw[->,line width=0.2mm](r2s)--(r3) node[above,midway] {$\backslash c_3$};
|
|
590
|
146 |
|
|
593
|
147 |
\node (rns) [right = of r3, draw=blue, minimum size = 20mm]{$a_{3s}$};
|
|
|
148 |
\draw[->,line width=0.2mm] (r3)--(rns) node [above, midway] {$\simp'$};
|
|
590
|
149 |
|
|
593
|
150 |
\node (rnn) [right = of rns, minimum size = 1mm]{};
|
|
|
151 |
\draw[->, dashed] (rns)--(rnn) node [above, midway] {$\ldots$};
|
|
590
|
152 |
|
|
593
|
153 |
\end{tikzpicture}
|
|
|
154 |
\caption{Regular expression size change during our $\blexersimp$ algorithm}\label{sulzShrinks}
|
|
590
|
155 |
\end{figure}
|
|
|
156 |
\noindent
|
|
639
|
157 |
The picture means that in some cases their lexer (where they use $\simpsulz$
|
|
613
|
158 |
as the simplification function)
|
|
618
|
159 |
will have a size explosion, causing the running time
|
|
613
|
160 |
of each derivative step to grow continuously (for example
|
|
590
|
161 |
in \ref{SulzmannLuLexerTime}).
|
|
613
|
162 |
They tested out the run time of their
|
|
590
|
163 |
lexer on particular examples such as $(a+b+ab)^*$
|
|
613
|
164 |
and claimed that their algorithm is linear w.r.t to the input.
|
|
|
165 |
With our mecahnised proof, we avoid this type of unintentional
|
|
639
|
166 |
generalisation.
|
|
613
|
167 |
|
|
|
168 |
Before delving in to the details of the formalisation,
|
|
639
|
169 |
we are going to provide an overview of it in the next subsection.
|
|
613
|
170 |
|
|
590
|
171 |
|
|
577
|
172 |
\subsection{Overview of the Proof}
|
|
618
|
173 |
A high-level overview of the main components of the finiteness proof
|
|
|
174 |
is as follows:
|
|
593
|
175 |
\begin{figure}[H]
|
|
|
176 |
\begin{tikzpicture}[scale=1,font=\bf,
|
|
|
177 |
node/.style={
|
|
|
178 |
rectangle,rounded corners=3mm,
|
|
|
179 |
ultra thick,draw=black!50,minimum height=18mm,
|
|
|
180 |
minimum width=20mm,
|
|
|
181 |
top color=white,bottom color=black!20}]
|
|
543
|
182 |
|
|
|
183 |
|
|
593
|
184 |
\node (0) at (-5,0)
|
|
|
185 |
[node, text width=1.8cm, text centered]
|
|
|
186 |
{$\llbracket \bderssimp{a}{s} \rrbracket$};
|
|
|
187 |
\node (A) at (0,0)
|
|
|
188 |
[node,text width=1.6cm, text centered]
|
|
|
189 |
{$\llbracket \rderssimp{r}{s} \rrbracket_r$};
|
|
|
190 |
\node (B) at (3,0)
|
|
|
191 |
[node,text width=3.0cm, anchor=west, minimum width = 40mm]
|
|
|
192 |
{$\llbracket \textit{ClosedForm}(r, s)\rrbracket_r$};
|
|
|
193 |
\node (C) at (9.5,0) [node, minimum width=10mm] {$N_r$};
|
|
|
194 |
|
|
|
195 |
\draw [->,line width=0.5mm] (0) --
|
|
|
196 |
node [above,pos=0.45] {=} (A) node [below, pos = 0.45] {$(r = a \downarrow_r)$} (A);
|
|
|
197 |
\draw [->,line width=0.5mm] (A) --
|
|
|
198 |
node [above,pos=0.35] {$\quad =\ldots=$} (B);
|
|
|
199 |
\draw [->,line width=0.5mm] (B) --
|
|
|
200 |
node [above,pos=0.35] {$\quad \leq \ldots \leq$} (C);
|
|
|
201 |
\end{tikzpicture}
|
|
|
202 |
%\caption{
|
|
|
203 |
\end{figure}
|
|
576
|
204 |
\noindent
|
|
577
|
205 |
We explain the steps one by one:
|
|
532
|
206 |
\begin{itemize}
|
|
590
|
207 |
\item
|
|
|
208 |
We first introduce the operations such as
|
|
|
209 |
derivatives, simplification, size calculation, etc.
|
|
618
|
210 |
associated with $\rrexp$s, which we have introduced
|
|
|
211 |
in chapter \ref{Bitcoded2}.
|
|
593
|
212 |
The operations on $\rrexp$s are identical to those on
|
|
618
|
213 |
annotated regular expressions except that they dispense with
|
|
|
214 |
bitcodes. This means that all proofs about size of $\rrexp$s will apply to
|
|
|
215 |
annotated regular expressions, because the size of a regular
|
|
|
216 |
expression is independent of the bitcodes.
|
|
590
|
217 |
\item
|
|
593
|
218 |
We prove that $\rderssimp{r}{s} = \textit{ClosedForm}(r, s)$,
|
|
|
219 |
where $\textit{ClosedForm}(r, s)$ is entirely
|
|
618
|
220 |
given as the derivatives of their children regular
|
|
593
|
221 |
expressions.
|
|
|
222 |
We call the right-hand-side the \emph{Closed Form}
|
|
|
223 |
of the derivative $\rderssimp{r}{s}$.
|
|
590
|
224 |
\item
|
|
618
|
225 |
Formally we give an estimate of
|
|
|
226 |
$\llbracket \textit{ClosedForm}(r, s) \rrbracket_r$.
|
|
593
|
227 |
The key observation is that $\distinctBy$'s output is
|
|
|
228 |
a list with a constant length bound.
|
|
532
|
229 |
\end{itemize}
|
|
594
|
230 |
We will expand on these steps in the next sections.\\
|
|
532
|
231 |
|
|
613
|
232 |
\section{The $\textit{Rrexp}$ Datatype}
|
|
594
|
233 |
The first step is to define
|
|
|
234 |
$\textit{rrexp}$s.
|
|
618
|
235 |
They are annotated regular expressions without bitcodes,
|
|
639
|
236 |
allowing a more convenient size bound proof.
|
|
618
|
237 |
%Of course, the bits which encode the lexing information
|
|
|
238 |
%would grow linearly with respect
|
|
|
239 |
%to the input, which should be taken into account when we wish to tackle the runtime comlexity.
|
|
|
240 |
%But for the sake of the structural size
|
|
|
241 |
%we can safely ignore them.\\
|
|
|
242 |
The datatype
|
|
594
|
243 |
definition of the $\rrexp$, called
|
|
593
|
244 |
\emph{r-regular expressions},
|
|
594
|
245 |
was initially defined in \ref{rrexpDef}.
|
|
|
246 |
The reason for the prefix $r$ is
|
|
593
|
247 |
to make a distinction
|
|
594
|
248 |
with basic regular expressions.
|
|
639
|
249 |
We give here again the definition of $\rrexp$.
|
|
576
|
250 |
\[ \rrexp ::= \RZERO \mid \RONE
|
|
593
|
251 |
\mid \RCHAR{c}
|
|
|
252 |
\mid \RSEQ{r_1}{r_2}
|
|
|
253 |
\mid \RALTS{rs}
|
|
|
254 |
\mid \RSTAR{r}
|
|
576
|
255 |
\]
|
|
593
|
256 |
The size of an r-regular expression is
|
|
|
257 |
written $\llbracket r\rrbracket_r$,
|
|
|
258 |
whose definition mirrors that of an annotated regular expression.
|
|
576
|
259 |
\begin{center}
|
|
618
|
260 |
\begin{tabular}{lcl}
|
|
593
|
261 |
$\llbracket _{bs}\ONE \rrbracket_r$ & $\dn$ & $1$\\
|
|
|
262 |
$\llbracket \ZERO \rrbracket_r$ & $\dn$ & $1$ \\
|
|
|
263 |
$\llbracket _{bs} r_1 \cdot r_2 \rrbracket_r$ & $\dn$ & $\llbracket r_1 \rrbracket_r + \llbracket r_2 \rrbracket_r + 1$\\
|
|
|
264 |
$\llbracket _{bs}\mathbf{c} \rrbracket_r $ & $\dn$ & $1$\\
|
|
|
265 |
$\llbracket _{bs}\sum as \rrbracket_r $ & $\dn$ & $\map \; (\llbracket \_ \rrbracket_r)\; as + 1$\\
|
|
|
266 |
$\llbracket _{bs} a^* \rrbracket_r $ & $\dn$ & $\llbracket a \rrbracket_r + 1$.
|
|
|
267 |
\end{tabular}
|
|
576
|
268 |
\end{center}
|
|
|
269 |
\noindent
|
|
593
|
270 |
The $r$ in the subscript of $\llbracket \rrbracket_r$ is to
|
|
|
271 |
differentiate with the same operation for annotated regular expressions.
|
|
|
272 |
Adding $r$ as subscript will be used in
|
|
594
|
273 |
other operations as well.\\
|
|
593
|
274 |
The transformation from an annotated regular expression
|
|
|
275 |
to an r-regular expression is straightforward.
|
|
|
276 |
\begin{center}
|
|
|
277 |
\begin{tabular}{lcl}
|
|
|
278 |
$\rerase{\ZERO}$ & $\dn$ & $\RZERO$\\
|
|
|
279 |
$\rerase{_{bs}\ONE}$ & $\dn$ & $\RONE$\\
|
|
|
280 |
$\rerase{_{bs}\mathbf{c}}$ & $\dn$ & $\RCHAR{c}$\\
|
|
|
281 |
$\rerase{_{bs}r_1\cdot r_2}$ & $\dn$ & $\RSEQ{\rerase{r_1}}{\rerase{r_2}}$\\
|
|
|
282 |
$\rerase{_{bs}\sum as}$ & $\dn$ & $\RALTS{\map \; \rerase{\_} \; as}$\\
|
|
|
283 |
$\rerase{_{bs} a ^*}$ & $\dn$ & $\rerase{a} ^*$
|
|
|
284 |
\end{tabular}
|
|
|
285 |
\end{center}
|
|
594
|
286 |
|
|
613
|
287 |
\subsection{Why a New Datatype?}
|
|
618
|
288 |
The reason we
|
|
|
289 |
define a new datatype is that
|
|
|
290 |
the $\erase$ function
|
|
|
291 |
does not preserve the structure of annotated
|
|
|
292 |
regular expressions.
|
|
576
|
293 |
We initially started by using
|
|
|
294 |
plain regular expressions and tried to prove
|
|
618
|
295 |
lemma \ref{rsizeAsize},
|
|
|
296 |
however the $\erase$ function messes with the structure of the
|
|
594
|
297 |
annotated regular expression.
|
|
|
298 |
The $+$ constructor
|
|
618
|
299 |
of basic regular expressions is only binary, whereas $\sum$
|
|
|
300 |
takes a list. Therefore we need to convert between
|
|
|
301 |
annotated and normal regular expressions as follows:
|
|
576
|
302 |
\begin{center}
|
|
618
|
303 |
\begin{tabular}{lcl}
|
|
594
|
304 |
$\erase \; _{bs}\sum [] $ & $\dn$ & $\ZERO$\\
|
|
|
305 |
$\erase \; _{bs}\sum [a]$ & $\dn$ & $a$\\
|
|
|
306 |
$\erase \; _{bs}\sum a :: as$ & $\dn$ & $a + (\erase \; _{[]} \sum as)\quad \text{if $as$ length over 1}$
|
|
|
307 |
\end{tabular}
|
|
576
|
308 |
\end{center}
|
|
594
|
309 |
\noindent
|
|
639
|
310 |
As can be seen, alternative regular expressions with an empty argument list
|
|
594
|
311 |
will be turned into a $\ZERO$.
|
|
618
|
312 |
The singleton alternative $\sum [r]$ becomes $r$ during the
|
|
594
|
313 |
$\erase$ function.
|
|
|
314 |
The annotated regular expression $\sum[a, b, c]$ would turn into
|
|
|
315 |
$(a+(b+c))$.
|
|
|
316 |
All these operations change the size and structure of
|
|
|
317 |
an annotated regular expressions, adding unnecessary
|
|
639
|
318 |
complexities to the size bound proof.
|
|
|
319 |
|
|
613
|
320 |
For example, if we define the size of a basic plain regular expression
|
|
594
|
321 |
in the usual way,
|
|
543
|
322 |
\begin{center}
|
|
618
|
323 |
\begin{tabular}{lcl}
|
|
593
|
324 |
$\llbracket \ONE \rrbracket_p$ & $\dn$ & $1$\\
|
|
|
325 |
$\llbracket \ZERO \rrbracket_p$ & $\dn$ & $1$ \\
|
|
|
326 |
$\llbracket r_1 \cdot r_2 \rrbracket_p$ & $\dn$ & $\llbracket r_1 \rrbracket_p + \llbracket r_2 \rrbracket_p + 1$\\
|
|
|
327 |
$\llbracket \mathbf{c} \rrbracket_p $ & $\dn$ & $1$\\
|
|
|
328 |
$\llbracket r_1 \cdot r_2 \rrbracket_p $ & $\dn$ & $\llbracket r_1 \rrbracket_p \; + \llbracket r_2 \rrbracket_p + 1$\\
|
|
|
329 |
$\llbracket a^* \rrbracket_p $ & $\dn$ & $\llbracket a \rrbracket_p + 1$
|
|
|
330 |
\end{tabular}
|
|
532
|
331 |
\end{center}
|
|
543
|
332 |
\noindent
|
|
594
|
333 |
Then the property
|
|
532
|
334 |
\begin{center}
|
|
613
|
335 |
$\llbracket a \rrbracket \stackrel{?}{=} \llbracket a_\downarrow \rrbracket_p$
|
|
532
|
336 |
\end{center}
|
|
594
|
337 |
does not hold.
|
|
613
|
338 |
With $\textit{rerase}$, however,
|
|
|
339 |
only the bitcodes are thrown away.
|
|
|
340 |
Everything about the structure remains intact.
|
|
|
341 |
Therefore it does not change the size
|
|
618
|
342 |
of an annotated regular expression and we have:
|
|
613
|
343 |
\begin{lemma}\label{rsizeAsize}
|
|
|
344 |
$\rsize{\rerase a} = \asize a$
|
|
|
345 |
\end{lemma}
|
|
|
346 |
\begin{proof}
|
|
|
347 |
By routine structural induction on $a$.
|
|
|
348 |
\end{proof}
|
|
|
349 |
\noindent
|
|
594
|
350 |
One might be able to prove an inequality such as
|
|
|
351 |
$\llbracket a \rrbracket \leq \llbracket a_\downarrow \rrbracket_p $
|
|
|
352 |
and then estimate $\llbracket a_\downarrow \rrbracket_p$,
|
|
|
353 |
but we found our approach more straightforward.\\
|
|
532
|
354 |
|
|
613
|
355 |
\subsection{Functions for R-regular Expressions}
|
|
639
|
356 |
The downside of our approach is that we need to redefine
|
|
|
357 |
several functions for $\rrexp$.
|
|
618
|
358 |
In this section we shall define the r-regular expression version
|
|
639
|
359 |
of $\bder$, and $\textit{bsimp}$ related functions.
|
|
613
|
360 |
We use $r$ as the prefix or subscript to differentiate
|
|
|
361 |
with the bitcoded version.
|
|
618
|
362 |
%For example,$\backslash_r$, $\rdistincts$, and $\rsimp$
|
|
|
363 |
%as opposed to $\backslash$, $\distinctBy$, and $\bsimp$.
|
|
|
364 |
%As promised, they are much simpler than their bitcoded counterparts.
|
|
613
|
365 |
%The operations on r-regular expressions are
|
|
|
366 |
%almost identical to those of the annotated regular expressions,
|
|
|
367 |
%except that no bitcodes are used. For example,
|
|
618
|
368 |
The derivative operation for an r-regular expression is\\
|
|
543
|
369 |
\begin{center}
|
|
593
|
370 |
\begin{tabular}{@{}lcl@{}}
|
|
|
371 |
$(\ZERO)\,\backslash_r c$ & $\dn$ & $\ZERO$\\
|
|
|
372 |
$(\ONE)\,\backslash_r c$ & $\dn$ &
|
|
|
373 |
$\textit{if}\;c=d\; \;\textit{then}\;
|
|
|
374 |
\ONE\;\textit{else}\;\ZERO$\\
|
|
|
375 |
$(\sum \;\textit{rs})\,\backslash_r c$ & $\dn$ &
|
|
|
376 |
$\sum\;(\textit{map} \; (\_\backslash_r c) \; rs )$\\
|
|
|
377 |
$(r_1\cdot r_2)\,\backslash_r c$ & $\dn$ &
|
|
594
|
378 |
$\textit{if}\;(\textit{rnullable}\,r_1)$\\
|
|
593
|
379 |
& &$\textit{then}\;\sum\,[(r_1\,\backslash_r c)\cdot\,r_2,$\\
|
|
|
380 |
& &$\phantom{\textit{then},\;\sum\,}((r_2\,\backslash_r c))]$\\
|
|
|
381 |
& &$\textit{else}\;\,(r_1\,\backslash_r c)\cdot r_2$\\
|
|
|
382 |
$(r^*)\,\backslash_r c$ & $\dn$ &
|
|
|
383 |
$( r\,\backslash_r c)\cdot
|
|
|
384 |
(_{[]}r^*))$
|
|
|
385 |
\end{tabular}
|
|
543
|
386 |
\end{center}
|
|
|
387 |
\noindent
|
|
618
|
388 |
where we omit the definition of $\textit{rnullable}$.
|
|
639
|
389 |
The generalisation from the derivatives w.r.t a character to
|
|
|
390 |
derivatives w.r.t strings is given as
|
|
620
|
391 |
\begin{center}
|
|
|
392 |
\begin{tabular}{lcl}
|
|
|
393 |
$r \backslash_{rs} []$ & $\dn$ & $r$\\
|
|
|
394 |
$r \backslash_{rs} c::s$ & $\dn$ & $(r\backslash_r c) \backslash_{rs} s$
|
|
|
395 |
\end{tabular}
|
|
|
396 |
\end{center}
|
|
618
|
397 |
|
|
|
398 |
The function $\distinctBy$ for r-regular expressions does not need
|
|
594
|
399 |
a function checking equivalence because
|
|
618
|
400 |
there are no bit annotations.
|
|
|
401 |
Therefore we have
|
|
532
|
402 |
\begin{center}
|
|
593
|
403 |
\begin{tabular}{lcl}
|
|
|
404 |
$\rdistinct{[]}{rset} $ & $\dn$ & $[]$\\
|
|
594
|
405 |
$\rdistinct{r :: rs}{rset}$ & $\dn$ &
|
|
|
406 |
$\textit{if}(r \in \textit{rset}) \; \textit{then} \; \rdistinct{rs}{rset}$\\
|
|
|
407 |
& & $\textit{else}\; \;
|
|
|
408 |
r::\rdistinct{rs}{(rset \cup \{r\})}$
|
|
593
|
409 |
\end{tabular}
|
|
532
|
410 |
\end{center}
|
|
|
411 |
%TODO: definition of rsimp (maybe only the alternative clause)
|
|
543
|
412 |
\noindent
|
|
618
|
413 |
%We would like to make clear
|
|
|
414 |
%a difference between our $\rdistincts$ and
|
|
|
415 |
%the Isabelle $\textit {distinct}$ predicate.
|
|
|
416 |
%In Isabelle $\textit{distinct}$ is a function that returns a boolean
|
|
|
417 |
%rather than a list.
|
|
|
418 |
%It tests if all the elements of a list are unique.\\
|
|
|
419 |
With $\textit{rdistinct}$ in place,
|
|
|
420 |
the flatten function for $\rrexp$ is as follows:
|
|
595
|
421 |
\begin{center}
|
|
|
422 |
\begin{tabular}{@{}lcl@{}}
|
|
596
|
423 |
$\textit{rflts} \; (\sum \textit{as}) :: \textit{as'}$ & $\dn$ & $as \; @ \; \textit{rflts} \; as' $ \\
|
|
595
|
424 |
$\textit{rflts} \; \ZERO :: as'$ & $\dn$ & $ \textit{rflts} \; \textit{as'} $ \\
|
|
|
425 |
$\textit{rflts} \; a :: as'$ & $\dn$ & $a :: \textit{rflts} \; \textit{as'}$ \quad(otherwise)
|
|
|
426 |
\end{tabular}
|
|
|
427 |
\end{center}
|
|
|
428 |
\noindent
|
|
618
|
429 |
The function
|
|
|
430 |
$\rsimpalts$ corresponds to $\textit{bsimp}_{ALTS}$:
|
|
596
|
431 |
\begin{center}
|
|
|
432 |
\begin{tabular}{@{}lcl@{}}
|
|
|
433 |
$\rsimpalts \;\; nil$ & $\dn$ & $\RZERO$\\
|
|
|
434 |
$\rsimpalts \;\; r::nil$ & $\dn$ & $r$\\
|
|
|
435 |
$\rsimpalts \;\; rs$ & $\dn$ & $\sum rs$\\
|
|
|
436 |
\end{tabular}
|
|
|
437 |
\end{center}
|
|
|
438 |
\noindent
|
|
618
|
439 |
Similarly, we have $\rsimpseq$ which corresponds to $\textit{bsimp}_{SEQ}$:
|
|
596
|
440 |
\begin{center}
|
|
|
441 |
\begin{tabular}{@{}lcl@{}}
|
|
|
442 |
$\rsimpseq \;\; \RZERO \; \_ $ & $=$ & $\RZERO$\\
|
|
|
443 |
$\rsimpseq \;\; \_ \; \RZERO $ & $=$ & $\RZERO$\\
|
|
|
444 |
$\rsimpseq \;\; \RONE \cdot r_2$ & $\dn$ & $r_2$\\
|
|
|
445 |
$\rsimpseq \;\; r_1 r_2$ & $\dn$ & $r_1 \cdot r_2$\\
|
|
|
446 |
\end{tabular}
|
|
|
447 |
\end{center}
|
|
|
448 |
and get $\textit{rsimp}$ and $\rderssimp{\_}{\_}$:
|
|
595
|
449 |
\begin{center}
|
|
|
450 |
\begin{tabular}{@{}lcl@{}}
|
|
|
451 |
|
|
596
|
452 |
$\textit{rsimp} \; (r_1\cdot r_2)$ & $\dn$ & $ \textit{rsimp}_{SEQ} \; bs \;(\textit{rsimp} \; r_1) \; (\textit{rsimp} \; r_2) $ \\
|
|
|
453 |
$\textit{rsimp} \; (_{bs}\sum \textit{rs})$ & $\dn$ & $\textit{rsimp}_{ALTS} \; \textit{bs} \; (\textit{rdistinct} \; ( \textit{rflts} ( \textit{map} \; rsimp \; rs)) \; \rerases \; \varnothing) $ \\
|
|
|
454 |
$\textit{rsimp} \; r$ & $\dn$ & $\textit{r} \qquad \textit{otherwise}$
|
|
595
|
455 |
\end{tabular}
|
|
|
456 |
\end{center}
|
|
596
|
457 |
\begin{center}
|
|
|
458 |
\begin{tabular}{@{}lcl@{}}
|
|
|
459 |
$r\backslash_{rsimp} \, c$ & $\dn$ & $\rsimp \; (r\backslash_r \, c)$
|
|
|
460 |
\end{tabular}
|
|
|
461 |
\end{center}
|
|
|
462 |
|
|
|
463 |
\begin{center}
|
|
|
464 |
\begin{tabular}{@{}lcl@{}}
|
|
601
|
465 |
$r \backslash_{rsimps} \; \; c\!::\!s $ & $\dn$ & $(r \backslash_{rsimp}\, c) \backslash_{rsimps}\, s$ \\
|
|
596
|
466 |
$r \backslash_{rsimps} [\,] $ & $\dn$ & $r$
|
|
|
467 |
\end{tabular}
|
|
|
468 |
\end{center}
|
|
|
469 |
\noindent
|
|
601
|
470 |
We do not define an r-regular expression version of $\blexersimp$,
|
|
618
|
471 |
as our proof does not depend on it.
|
|
613
|
472 |
Now we are ready to introduce how r-regular expressions allow
|
|
|
473 |
us to prove the size bound on bitcoded regular expressions.
|
|
|
474 |
|
|
|
475 |
\subsection{Using R-regular Expressions to Bound Bit-coded Regular Expressions}
|
|
|
476 |
Everything about the size of annotated regular expressions after the application
|
|
|
477 |
of function $\bsimp$ and $\backslash_{simps}$
|
|
|
478 |
can be calculated via the size of r-regular expressions after the application
|
|
|
479 |
of $\rsimp$ and $\backslash_{rsimps}$:
|
|
564
|
480 |
\begin{lemma}\label{sizeRelations}
|
|
618
|
481 |
The following two equalities hold:
|
|
543
|
482 |
\begin{itemize}
|
|
|
483 |
\item
|
|
601
|
484 |
$\asize{\bsimps \; a} = \rsize{\rsimp{ \rerase{a}}}$
|
|
554
|
485 |
\item
|
|
596
|
486 |
$\asize{\bderssimp{a}{s}} = \rsize{\rderssimp{\rerase{a}}{s}}$
|
|
554
|
487 |
\end{itemize}
|
|
532
|
488 |
\end{lemma}
|
|
601
|
489 |
\begin{proof}
|
|
|
490 |
The first part is by induction on the inductive cases
|
|
|
491 |
of $\textit{bsimp}$.
|
|
|
492 |
The second part is by induction on the string $s$,
|
|
|
493 |
where the inductive step follows from part one.
|
|
|
494 |
\end{proof}
|
|
543
|
495 |
\noindent
|
|
596
|
496 |
With lemma \ref{sizeRelations},
|
|
601
|
497 |
we will be able to focus on
|
|
|
498 |
estimating only
|
|
|
499 |
$\rsize{\rderssimp{\rerase{a}}{s}}$
|
|
|
500 |
in later parts because
|
|
|
501 |
\begin{center}
|
|
|
502 |
$\rsize{\rderssimp{\rerase{a}}{s}} \leq N_r \quad$
|
|
|
503 |
implies
|
|
|
504 |
$\quad \llbracket a \backslash_{bsimps} s \rrbracket \leq N_r$.
|
|
|
505 |
\end{center}
|
|
618
|
506 |
%From now on we
|
|
|
507 |
%Unless stated otherwise in the rest of this
|
|
|
508 |
%chapter all regular expressions without
|
|
|
509 |
%bitcodes are seen as r-regular expressions ($\rrexp$s).
|
|
|
510 |
%For the binary alternative r-regular expression $\RALTS{[r_1, r_2]}$,
|
|
|
511 |
%we use the notation $r_1 + r_2$
|
|
|
512 |
%for brevity.
|
|
532
|
513 |
|
|
|
514 |
|
|
|
515 |
%-----------------------------------
|
|
596
|
516 |
% SUB SECTION ROADMAP RREXP BOUND
|
|
532
|
517 |
%-----------------------------------
|
|
553
|
518 |
|
|
596
|
519 |
%\subsection{Roadmap to a Bound for $\textit{Rrexp}$}
|
|
553
|
520 |
|
|
596
|
521 |
%The way we obtain the bound for $\rrexp$s is by two steps:
|
|
|
522 |
%\begin{itemize}
|
|
|
523 |
% \item
|
|
|
524 |
% First, we rewrite $r\backslash s$ into something else that is easier
|
|
|
525 |
% to bound. This step is especially important for the inductive case
|
|
|
526 |
% $r_1 \cdot r_2$ and $r^*$, where the derivative can grow and bloat in a wild way,
|
|
|
527 |
% but after simplification they will always be equal or smaller to a form consisting of an alternative
|
|
|
528 |
% list of regular expressions $f \; (g\; (\sum rs))$ with some functions applied to it, where each element will be distinct after the function application.
|
|
|
529 |
% \item
|
|
|
530 |
% Then, for such a sum list of regular expressions $f\; (g\; (\sum rs))$, we can control its size
|
|
|
531 |
% by estimation, since $\distinctBy$ and $\flts$ are well-behaved and working together would only
|
|
|
532 |
% reduce the size of a regular expression, not adding to it.
|
|
|
533 |
%\end{itemize}
|
|
|
534 |
%
|
|
|
535 |
%\section{Step One: Closed Forms}
|
|
|
536 |
%We transform the function application $\rderssimp{r}{s}$
|
|
|
537 |
%into an equivalent
|
|
|
538 |
%form $f\; (g \; (\sum rs))$.
|
|
|
539 |
%The functions $f$ and $g$ can be anything from $\flts$, $\distinctBy$ and other helper functions from $\bsimp{\_}$.
|
|
|
540 |
%This way we get a different but equivalent way of expressing : $r\backslash s = f \; (g\; (\sum rs))$, we call the
|
|
|
541 |
%right hand side the "closed form" of $r\backslash s$.
|
|
|
542 |
%
|
|
|
543 |
%\begin{quote}\it
|
|
|
544 |
% Claim: For regular expressions $r_1 \cdot r_2$, we claim that
|
|
|
545 |
%\end{quote}
|
|
|
546 |
%\noindent
|
|
|
547 |
%We explain in detail how we reached those claims.
|
|
601
|
548 |
If we attempt to prove
|
|
|
549 |
\begin{center}
|
|
609
|
550 |
$\forall r. \; \exists N_r.\;\; s.t. \llbracket r\backslash_{rsimps} s \rrbracket_r \leq N_r$
|
|
601
|
551 |
\end{center}
|
|
|
552 |
using a naive induction on the structure of $r$,
|
|
|
553 |
then we are stuck at the inductive cases such as
|
|
|
554 |
$r_1\cdot r_2$.
|
|
|
555 |
The inductive hypotheses are:
|
|
|
556 |
\begin{center}
|
|
|
557 |
1: $\text{for } r_1, \text{there exists } N_{r_1}.\;\; s.t.
|
|
609
|
558 |
\;\;\forall s. \llbracket r_1 \backslash_{rsimps} s \rrbracket_r \leq N_{r_1}. $\\
|
|
601
|
559 |
2: $\text{for } r_2, \text{there exists } N_{r_2}.\;\; s.t.
|
|
609
|
560 |
\;\; \forall s. \llbracket r_2 \backslash_{rsimps} s \rrbracket_r \leq N_{r_2}. $
|
|
601
|
561 |
\end{center}
|
|
|
562 |
The inductive step to prove would be
|
|
|
563 |
\begin{center}
|
|
|
564 |
$\text{there exists } N_{r_1\cdot r_2}. \;\; s.t. \forall s.
|
|
609
|
565 |
\llbracket (r_1 \cdot r_2) \backslash_{rsimps} s \rrbracket_r \leq N_{r_1\cdot r_2}.$
|
|
601
|
566 |
\end{center}
|
|
|
567 |
The problem is that it is not clear what
|
|
609
|
568 |
$(r_1\cdot r_2) \backslash_{rsimps} s$ looks like,
|
|
601
|
569 |
and therefore $N_{r_1}$ and $N_{r_2}$ in the
|
|
|
570 |
inductive hypotheses cannot be directly used.
|
|
618
|
571 |
%We have already seen that $(r_1 \cdot r_2)\backslash s$
|
|
|
572 |
%and $(r^*)\backslash s$ can grow in a wild way.
|
|
613
|
573 |
|
|
618
|
574 |
The point however, is that they will be equivalent to a list of
|
|
609
|
575 |
terms $\sum rs$, where each term in $rs$ will
|
|
|
576 |
be made of $r_1 \backslash s' $, $r_2\backslash s'$,
|
|
618
|
577 |
and $r \backslash s'$ with $s' \in \textit{SubString} \; s$ (which stands
|
|
|
578 |
for the set of substrings of $s$).
|
|
609
|
579 |
The list $\sum rs$ will then be de-duplicated by $\textit{rdistinct}$
|
|
618
|
580 |
in the simplification, which prevents the $rs$ from growing indefinitely.
|
|
609
|
581 |
|
|
613
|
582 |
Based on this idea, we develop a proof in two steps.
|
|
|
583 |
First, we show the equality (where
|
|
609
|
584 |
$f$ and $g$ are functions that do not increase the size of the input)
|
|
|
585 |
\begin{center}
|
|
613
|
586 |
$r\backslash_{rsimps} s = f\; (\textit{rdistinct} \; (g\; \sum rs))$,
|
|
609
|
587 |
\end{center}
|
|
613
|
588 |
where $r = r_1 \cdot r_2$ or $r = r_0^*$ and so on.
|
|
|
589 |
For example, for $r_1 \cdot r_2$ we have the equality as
|
|
|
590 |
\begin{center}
|
|
|
591 |
$ \rderssimp{r_1 \cdot r_2}{s} =
|
|
639
|
592 |
\rsimp{(\sum (r_1 \backslash s \cdot r_2 ) \; :: \;(\map \; \rderssimp{r_2}{\_} \;(\vsuf{s}{r_1})))}$
|
|
613
|
593 |
\end{center}
|
|
609
|
594 |
We call the right-hand-side the
|
|
|
595 |
\emph{Closed Form} of $(r_1 \cdot r_2)\backslash_{rsimps} s$.
|
|
613
|
596 |
Second, we will bound the closed form of r-regular expressions
|
|
|
597 |
using some estimation techniques
|
|
618
|
598 |
and then apply
|
|
|
599 |
lemma \ref{sizeRelations} to show that the bitcoded regular expressions
|
|
613
|
600 |
in our $\blexersimp$ are finitely bounded.
|
|
609
|
601 |
|
|
618
|
602 |
We will describe in detail the first step of the proof
|
|
|
603 |
in the next section.
|
|
613
|
604 |
|
|
|
605 |
\section{Closed Forms}
|
|
609
|
606 |
In this section we introduce in detail
|
|
618
|
607 |
how we express the string derivatives
|
|
|
608 |
of regular expressions (i.e. $r \backslash_r s$ where $s$ is a string
|
|
|
609 |
rather than a single character) in a different way than
|
|
|
610 |
our previous definition.
|
|
|
611 |
In previous chapters, the derivative of a
|
|
|
612 |
regular expression $r$ w.r.t a string $s$
|
|
|
613 |
was recursively defined on the string:
|
|
|
614 |
\begin{center}
|
|
|
615 |
$r \backslash_s (c::s) \dn (r \backslash c) \backslash_s s$
|
|
|
616 |
\end{center}
|
|
|
617 |
The problem is that
|
|
|
618 |
this definition does not provide much information
|
|
|
619 |
on what $r \backslash_s s$ looks like.
|
|
|
620 |
If we are interested in the size of a derivative like
|
|
|
621 |
$(r_1 \cdot r_2)\backslash s$,
|
|
|
622 |
we have to somehow get a more concrete form to begin.
|
|
|
623 |
We call such more concrete representations the ``closed forms'' of
|
|
|
624 |
string derivatives as opposed to their original definitions.
|
|
|
625 |
The terminology ``closed form'' is borrowed from mathematics,
|
|
|
626 |
which usually describe expressions that are solely comprised of
|
|
|
627 |
well-known and easy-to-compute operations such as
|
|
|
628 |
additions, multiplications, exponential functions.
|
|
|
629 |
|
|
613
|
630 |
We start by proving some basic identities
|
|
609
|
631 |
involving the simplification functions for r-regular expressions.
|
|
613
|
632 |
After that we introduce the rewrite relations
|
|
|
633 |
$\rightsquigarrow_h$, $\rightsquigarrow^*_{scf}$
|
|
|
634 |
$\rightsquigarrow_f$ and $\rightsquigarrow_g$.
|
|
618
|
635 |
These relations involves similar techniques as in chapter \ref{Bitcoded2}
|
|
|
636 |
for annotated regular expressions.
|
|
613
|
637 |
Finally, we use these identities to establish the
|
|
|
638 |
closed forms of the alternative regular expression,
|
|
|
639 |
the sequence regular expression, and the star regular expression.
|
|
609
|
640 |
%$r_1\cdot r_2$, $r^*$ and $\sum rs$.
|
|
601
|
641 |
|
|
|
642 |
|
|
609
|
643 |
|
|
613
|
644 |
\subsection{Some Basic Identities}
|
|
609
|
645 |
|
|
618
|
646 |
In what follows we will often convert between lists
|
|
|
647 |
and sets.
|
|
|
648 |
We use Isabelle's $set$ to refere to the
|
|
611
|
649 |
function that converts a list $rs$ to the set
|
|
|
650 |
containing all the elements in $rs$.
|
|
|
651 |
\subsubsection{$\textit{rdistinct}$'s Does the Job of De-duplication}
|
|
543
|
652 |
The $\textit{rdistinct}$ function, as its name suggests, will
|
|
613
|
653 |
de-duplicate an r-regular expression list.
|
|
|
654 |
It will also remove any elements that
|
|
|
655 |
is already in the accumulator set.
|
|
555
|
656 |
\begin{lemma}\label{rdistinctDoesTheJob}
|
|
609
|
657 |
%The function $\textit{rdistinct}$ satisfies the following
|
|
|
658 |
%properties:
|
|
|
659 |
Assume we have the predicate $\textit{isDistinct}$\footnote{We omit its
|
|
618
|
660 |
recursive definition here. Its Isabelle counterpart would be $\textit{distinct}$.}
|
|
609
|
661 |
for testing
|
|
613
|
662 |
whether a list's elements are unique. Then the following
|
|
609
|
663 |
properties about $\textit{rdistinct}$ hold:
|
|
543
|
664 |
\begin{itemize}
|
|
|
665 |
\item
|
|
|
666 |
If $a \in acc$ then $a \notin (\rdistinct{rs}{acc})$.
|
|
|
667 |
\item
|
|
609
|
668 |
%If list $rs'$ is the result of $\rdistinct{rs}{acc}$,
|
|
|
669 |
$\textit{isDistinct} \;\;\; (\rdistinct{rs}{acc})$.
|
|
555
|
670 |
\item
|
|
609
|
671 |
$\textit{set} \; (\rdistinct{rs}{acc})
|
|
639
|
672 |
= (\textit{set} \; rs) - acc$
|
|
543
|
673 |
\end{itemize}
|
|
|
674 |
\end{lemma}
|
|
555
|
675 |
\noindent
|
|
543
|
676 |
\begin{proof}
|
|
|
677 |
The first part is by an induction on $rs$.
|
|
555
|
678 |
The second and third part can be proven by using the
|
|
609
|
679 |
inductive cases of $\textit{rdistinct}$.
|
|
593
|
680 |
|
|
543
|
681 |
\end{proof}
|
|
|
682 |
|
|
|
683 |
\noindent
|
|
613
|
684 |
%$\textit{rdistinct}$ will out all regular expression terms
|
|
|
685 |
%that are in the accumulator, therefore
|
|
|
686 |
Concatenating a list $rs_a$ at the front of another
|
|
|
687 |
list $rs$ whose elements are all from the accumulator, and then calling $\textit{rdistinct}$
|
|
|
688 |
on the merged list, the output will be as if we had called $\textit{rdistinct}$
|
|
543
|
689 |
without the prepending of $rs$:
|
|
609
|
690 |
\begin{lemma}\label{rdistinctConcat}
|
|
554
|
691 |
The elements appearing in the accumulator will always be removed.
|
|
|
692 |
More precisely,
|
|
|
693 |
\begin{itemize}
|
|
|
694 |
\item
|
|
|
695 |
If $rs \subseteq rset$, then
|
|
|
696 |
$\rdistinct{rs@rsa }{acc} = \rdistinct{rsa }{acc}$.
|
|
|
697 |
\item
|
|
609
|
698 |
More generally, if $a \in rset$ and $\rdistinct{rs}{\{a\}} = []$,
|
|
554
|
699 |
then $\rdistinct{(rs @ rs')}{rset} = \rdistinct{rs'}{rset}$
|
|
|
700 |
\end{itemize}
|
|
543
|
701 |
\end{lemma}
|
|
554
|
702 |
|
|
543
|
703 |
\begin{proof}
|
|
609
|
704 |
By induction on $rs$ and using \ref{rdistinctDoesTheJob}.
|
|
543
|
705 |
\end{proof}
|
|
|
706 |
\noindent
|
|
|
707 |
On the other hand, if an element $r$ does not appear in the input list waiting to be deduplicated,
|
|
|
708 |
then expanding the accumulator to include that element will not cause the output list to change:
|
|
611
|
709 |
\begin{lemma}\label{rdistinctOnDistinct}
|
|
543
|
710 |
The accumulator can be augmented to include elements not appearing in the input list,
|
|
|
711 |
and the output will not change.
|
|
|
712 |
\begin{itemize}
|
|
|
713 |
\item
|
|
611
|
714 |
If $r \notin rs$, then $\rdistinct{rs}{acc} = \rdistinct{rs}{(\{r\} \cup acc)}$.
|
|
543
|
715 |
\item
|
|
611
|
716 |
Particularly, if $\;\;\textit{isDistinct} \; rs$, then we have\\
|
|
543
|
717 |
\[ \rdistinct{rs}{\varnothing} = rs \]
|
|
|
718 |
\end{itemize}
|
|
|
719 |
\end{lemma}
|
|
|
720 |
\begin{proof}
|
|
|
721 |
The first half is by induction on $rs$. The second half is a corollary of the first.
|
|
|
722 |
\end{proof}
|
|
|
723 |
\noindent
|
|
611
|
724 |
The function $\textit{rdistinct}$ removes duplicates from anywhere in a list.
|
|
|
725 |
Despite being seemingly obvious,
|
|
|
726 |
the induction technique is not as straightforward.
|
|
554
|
727 |
\begin{lemma}\label{distinctRemovesMiddle}
|
|
|
728 |
The two properties hold if $r \in rs$:
|
|
|
729 |
\begin{itemize}
|
|
|
730 |
\item
|
|
555
|
731 |
$\rdistinct{rs}{rset} = \rdistinct{(rs @ [r])}{rset}$\\
|
|
|
732 |
and\\
|
|
554
|
733 |
$\rdistinct{(ab :: rs @ [ab])}{rset'} = \rdistinct{(ab :: rs)}{rset'}$
|
|
|
734 |
\item
|
|
555
|
735 |
$\rdistinct{ (rs @ rs') }{rset} = \rdistinct{rs @ [r] @ rs'}{rset}$\\
|
|
|
736 |
and\\
|
|
554
|
737 |
$\rdistinct{(ab :: rs @ [ab] @ rs'')}{rset'} =
|
|
593
|
738 |
\rdistinct{(ab :: rs @ rs'')}{rset'}$
|
|
554
|
739 |
\end{itemize}
|
|
|
740 |
\end{lemma}
|
|
|
741 |
\noindent
|
|
|
742 |
\begin{proof}
|
|
593
|
743 |
By induction on $rs$. All other variables are allowed to be arbitrary.
|
|
611
|
744 |
The second part of the lemma requires the first.
|
|
618
|
745 |
Note that for each part, the two sub-propositions need to be proven
|
|
|
746 |
at the same time,
|
|
593
|
747 |
so that the induction goes through.
|
|
554
|
748 |
\end{proof}
|
|
555
|
749 |
\noindent
|
|
611
|
750 |
This allows us to prove a few more equivalence relations involving
|
|
618
|
751 |
$\textit{rdistinct}$ (they will be useful later):
|
|
555
|
752 |
\begin{lemma}\label{rdistinctConcatGeneral}
|
|
611
|
753 |
\mbox{}
|
|
555
|
754 |
\begin{itemize}
|
|
|
755 |
\item
|
|
|
756 |
$\rdistinct{(rs @ rs')}{\varnothing} = \rdistinct{((\rdistinct{rs}{\varnothing})@ rs')}{\varnothing}$
|
|
|
757 |
\item
|
|
|
758 |
$\rdistinct{(rs @ rs')}{\varnothing} = \rdistinct{(\rdistinct{rs}{\varnothing} @ rs')}{\varnothing}$
|
|
|
759 |
\item
|
|
|
760 |
If $rset' \subseteq rset$, then $\rdistinct{rs}{rset} =
|
|
|
761 |
\rdistinct{(\rdistinct{rs}{rset'})}{rset}$. As a corollary
|
|
|
762 |
of this,
|
|
|
763 |
\item
|
|
|
764 |
$\rdistinct{(rs @ rs')}{rset} = \rdistinct{
|
|
|
765 |
(\rdistinct{rs}{\varnothing}) @ rs')}{rset}$. This
|
|
|
766 |
gives another corollary use later:
|
|
|
767 |
\item
|
|
|
768 |
If $a \in rset$, then $\rdistinct{(rs @ rs')}{rset} = \rdistinct{
|
|
|
769 |
(\rdistinct{(a :: rs)}{\varnothing} @ rs')}{rset} $,
|
|
|
770 |
|
|
|
771 |
\end{itemize}
|
|
|
772 |
\end{lemma}
|
|
|
773 |
\begin{proof}
|
|
|
774 |
By \ref{rdistinctDoesTheJob} and \ref{distinctRemovesMiddle}.
|
|
|
775 |
\end{proof}
|
|
611
|
776 |
\noindent
|
|
639
|
777 |
The next lemma is a more general form of \ref{rdistinctConcat};
|
|
|
778 |
It says that
|
|
611
|
779 |
$\textit{rdistinct}$ is composable w.r.t list concatenation:
|
|
|
780 |
\begin{lemma}\label{distinctRdistinctAppend}
|
|
|
781 |
If $\;\; \textit{isDistinct} \; rs_1$,
|
|
|
782 |
and $(set \; rs_1) \cap acc = \varnothing$,
|
|
|
783 |
then applying $\textit{rdistinct}$ on $rs_1 @ rs_a$ does not
|
|
|
784 |
have an effect on $rs_1$:
|
|
|
785 |
\[\textit{rdistinct}\; (rs_1 @ rsa)\;\, acc
|
|
|
786 |
= rs_1@(\textit{rdistinct} rsa \; (acc \cup rs_1))\]
|
|
|
787 |
\end{lemma}
|
|
|
788 |
\begin{proof}
|
|
|
789 |
By an induction on
|
|
|
790 |
$rs_1$, where $rsa$ and $acc$ are allowed to be arbitrary.
|
|
|
791 |
\end{proof}
|
|
|
792 |
\noindent
|
|
|
793 |
$\textit{rdistinct}$ needs to be applied only once, and
|
|
618
|
794 |
applying it multiple times does not make any difference:
|
|
611
|
795 |
\begin{corollary}\label{distinctOnceEnough}
|
|
639
|
796 |
$\textit{rdistinct} \; (rs @ rsa) {} = \textit{rdistinct} \; ( (rdistinct \;
|
|
|
797 |
rs \; \{ \}) @ (\textit{rdistinct} \; rs_a \; (set \; rs)))$
|
|
611
|
798 |
\end{corollary}
|
|
|
799 |
\begin{proof}
|
|
|
800 |
By lemma \ref{distinctRdistinctAppend}.
|
|
|
801 |
\end{proof}
|
|
555
|
802 |
|
|
611
|
803 |
\subsubsection{The Properties of $\textit{Rflts}$}
|
|
|
804 |
We give in this subsection some properties
|
|
620
|
805 |
involving $\backslash_r$, $\backslash_{rsimps}$, $\textit{rflts}$ and
|
|
611
|
806 |
$\textit{rsimp}_{ALTS} $, together with any non-trivial lemmas that lead to them.
|
|
543
|
807 |
These will be helpful in later closed form proofs, when
|
|
611
|
808 |
we want to transform derivative terms which have
|
|
|
809 |
%the ways in which multiple functions involving
|
|
|
810 |
%those are composed together
|
|
|
811 |
interleaving derivatives and simplifications applied to them.
|
|
543
|
812 |
|
|
611
|
813 |
\noindent
|
|
|
814 |
%When the function $\textit{Rflts}$
|
|
|
815 |
%is applied to the concatenation of two lists, the output can be calculated by first applying the
|
|
|
816 |
%functions on two lists separately, and then concatenating them together.
|
|
|
817 |
$\textit{Rflts}$ is composable in terms of concatenation:
|
|
554
|
818 |
\begin{lemma}\label{rfltsProps}
|
|
618
|
819 |
The function $\rflts$ has the properties below:\\
|
|
543
|
820 |
\begin{itemize}
|
|
|
821 |
\item
|
|
554
|
822 |
$\rflts \; (rs_1 @ rs_2) = \rflts \; rs_1 @ \rflts \; rs_2$
|
|
|
823 |
\item
|
|
|
824 |
If $r \neq \RZERO$ and $\nexists rs_1. r = \RALTS{rs}_1$, then $\rflts \; (r::rs) = r :: \rflts \; rs$
|
|
|
825 |
\item
|
|
|
826 |
$\rflts \; (rs @ [\RZERO]) = \rflts \; rs$
|
|
|
827 |
\item
|
|
|
828 |
$\rflts \; (rs' @ [\RALTS{rs}]) = \rflts \; rs'@rs$
|
|
|
829 |
\item
|
|
|
830 |
$\rflts \; (rs @ [\RONE]) = \rflts \; rs @ [\RONE]$
|
|
|
831 |
\item
|
|
|
832 |
If $r \neq \RZERO$ and $\nexists rs'. r = \RALTS{rs'}$ then $\rflts \; (rs @ [r])
|
|
|
833 |
= (\rflts \; rs) @ [r]$
|
|
555
|
834 |
\item
|
|
|
835 |
If $r = \RALTS{rs}$ and $r \in rs'$ then for all $r_1 \in rs.
|
|
|
836 |
r_1 \in \rflts \; rs'$.
|
|
|
837 |
\item
|
|
|
838 |
$\rflts \; (rs_a @ \RZERO :: rs_b) = \rflts \; (rs_a @ rs_b)$
|
|
543
|
839 |
\end{itemize}
|
|
|
840 |
\end{lemma}
|
|
|
841 |
\noindent
|
|
|
842 |
\begin{proof}
|
|
555
|
843 |
By induction on $rs_1$ in the first sub-lemma, and induction on $r$ in the second part,
|
|
|
844 |
and induction on $rs$, $rs'$, $rs$, $rs'$, $rs_a$ in the third, fourth, fifth, sixth and
|
|
|
845 |
last sub-lemma.
|
|
543
|
846 |
\end{proof}
|
|
611
|
847 |
\noindent
|
|
|
848 |
Now we introduce the property that the operations
|
|
|
849 |
derivative and $\rsimpalts$
|
|
639
|
850 |
commute, this will be used later on when deriving the closed form for
|
|
611
|
851 |
the alternative regular expression:
|
|
|
852 |
\begin{lemma}\label{rderRsimpAltsCommute}
|
|
|
853 |
$\rder{x}{(\rsimpalts \; rs)} = \rsimpalts \; (\map \; (\rder{x}{\_}) \; rs)$
|
|
|
854 |
\end{lemma}
|
|
618
|
855 |
\begin{proof}
|
|
|
856 |
By induction on $rs$.
|
|
|
857 |
\end{proof}
|
|
611
|
858 |
\noindent
|
|
614
|
859 |
|
|
639
|
860 |
\subsubsection{The $RL$ Function: Language Interpretation for $\textit{Rrexp}$s}
|
|
618
|
861 |
Much like the definition of $L$ on plain regular expressions, one can also
|
|
639
|
862 |
define the language interpretation for $\rrexp$s.
|
|
614
|
863 |
\begin{center}
|
|
|
864 |
\begin{tabular}{lcl}
|
|
639
|
865 |
$RL \; (\ZERO_r)$ & $\dn$ & $\phi$\\
|
|
|
866 |
$RL \; (\ONE_r)$ & $\dn$ & $\{[]\}$\\
|
|
614
|
867 |
$RL \; (c)$ & $\dn$ & $\{[c]\}$\\
|
|
|
868 |
$RL \; \sum rs$ & $\dn$ & $ \bigcup_{r \in rs} (RL \; r)$\\
|
|
|
869 |
$RL \; (r_1 \cdot r_2)$ & $\dn$ & $ RL \; (r_1) @ RL \; (r_2)$\\
|
|
|
870 |
$RL \; (r^*)$ & $\dn$ & $ (RL(r))^*$
|
|
|
871 |
\end{tabular}
|
|
|
872 |
\end{center}
|
|
|
873 |
\noindent
|
|
|
874 |
The main use of $RL$ is to establish some connections between $\rsimp{}$
|
|
|
875 |
and $\rnullable{}$:
|
|
|
876 |
\begin{lemma}
|
|
|
877 |
The following properties hold:
|
|
|
878 |
\begin{itemize}
|
|
|
879 |
\item
|
|
|
880 |
If $\rnullable{r}$, then $\rsimp{r} \neq \RZERO$.
|
|
|
881 |
\item
|
|
|
882 |
$\rnullable{r \backslash s} \quad $ if and only if $\quad \rnullable{\rderssimp{r}{s}}$.
|
|
|
883 |
\end{itemize}
|
|
|
884 |
\end{lemma}
|
|
|
885 |
\begin{proof}
|
|
|
886 |
The first part is by induction on $r$.
|
|
|
887 |
The second part is true because property
|
|
|
888 |
\[ RL \; r = RL \; (\rsimp{r})\] holds.
|
|
|
889 |
\end{proof}
|
|
|
890 |
|
|
|
891 |
\subsubsection{Simplified $\textit{Rrexp}$s are Good}
|
|
|
892 |
We formalise the notion of ``good" regular expressions,
|
|
|
893 |
which means regular expressions that
|
|
618
|
894 |
are fully simplified in terms of our $\textit{rsimp}$ function.
|
|
|
895 |
For alternative regular expressions that means they
|
|
|
896 |
do not contain any nested alternatives, un-eliminated $\RZERO$s
|
|
|
897 |
or duplicate elements (for example,
|
|
|
898 |
$r_1 + (r_2 + r_3)$, $\RZERO + r$ and $ \sum [r, r, \ldots]$).
|
|
|
899 |
The clauses for $\good$ are:
|
|
614
|
900 |
\begin{center}
|
|
|
901 |
\begin{tabular}{@{}lcl@{}}
|
|
|
902 |
$\good\; \RZERO$ & $\dn$ & $\textit{false}$\\
|
|
|
903 |
$\good\; \RONE$ & $\dn$ & $\textit{true}$\\
|
|
|
904 |
$\good\; \RCHAR{c}$ & $\dn$ & $\btrue$\\
|
|
|
905 |
$\good\; \RALTS{[]}$ & $\dn$ & $\bfalse$\\
|
|
|
906 |
$\good\; \RALTS{[r]}$ & $\dn$ & $\bfalse$\\
|
|
|
907 |
$\good\; \RALTS{r_1 :: r_2 :: rs}$ & $\dn$ &
|
|
|
908 |
$\textit{isDistinct} \; (r_1 :: r_2 :: rs) \;$\\
|
|
618
|
909 |
& & $\land \; (\forall r' \in (r_1 :: r_2 :: rs).\; \good \; r'\; \, \land \; \, \textit{nonAlt}\; r')$\\
|
|
614
|
910 |
$\good \; \RSEQ{\RZERO}{r}$ & $\dn$ & $\bfalse$\\
|
|
|
911 |
$\good \; \RSEQ{\RONE}{r}$ & $\dn$ & $\bfalse$\\
|
|
|
912 |
$\good \; \RSEQ{r}{\RZERO}$ & $\dn$ & $\bfalse$\\
|
|
|
913 |
$\good \; \RSEQ{r_1}{r_2}$ & $\dn$ & $\good \; r_1 \;\, \textit{and} \;\, \good \; r_2$\\
|
|
|
914 |
$\good \; \RSTAR{r}$ & $\dn$ & $\btrue$\\
|
|
|
915 |
\end{tabular}
|
|
|
916 |
\end{center}
|
|
|
917 |
\noindent
|
|
618
|
918 |
We omit the recursive definition of the predicate $\textit{nonAlt}$,
|
|
|
919 |
which evaluates to true when the regular expression is not an
|
|
614
|
920 |
alternative, and false otherwise.
|
|
|
921 |
The $\good$ property is preserved under $\rsimp_{ALTS}$, provided that
|
|
|
922 |
its non-empty argument list of expressions are all good themsleves, and $\textit{nonAlt}$,
|
|
|
923 |
and unique:
|
|
|
924 |
\begin{lemma}\label{rsimpaltsGood}
|
|
|
925 |
If $rs \neq []$ and forall $r \in rs. \textit{nonAlt} \; r$ and $\textit{isDistinct} \; rs$,
|
|
|
926 |
then $\good \; (\rsimpalts \; rs)$ if and only if forall $r \in rs. \; \good \; r$.
|
|
|
927 |
\end{lemma}
|
|
|
928 |
\noindent
|
|
|
929 |
We also note that
|
|
|
930 |
if a regular expression $r$ is good, then $\rflts$ on the singleton
|
|
|
931 |
list $[r]$ will not break goodness:
|
|
|
932 |
\begin{lemma}\label{flts2}
|
|
|
933 |
If $\good \; r$, then forall $r' \in \rflts \; [r]. \; \good \; r'$ and $\textit{nonAlt} \; r'$.
|
|
|
934 |
\end{lemma}
|
|
|
935 |
\begin{proof}
|
|
|
936 |
By an induction on $r$.
|
|
|
937 |
\end{proof}
|
|
|
938 |
\noindent
|
|
|
939 |
The other observation we make about $\rsimp{r}$ is that it never
|
|
|
940 |
comes with nested alternatives, which we describe as the $\nonnested$
|
|
|
941 |
property:
|
|
|
942 |
\begin{center}
|
|
|
943 |
\begin{tabular}{lcl}
|
|
|
944 |
$\nonnested \; \, \sum []$ & $\dn$ & $\btrue$\\
|
|
|
945 |
$\nonnested \; \, \sum ((\sum rs_1) :: rs_2)$ & $\dn$ & $\bfalse$\\
|
|
|
946 |
$\nonnested \; \, \sum (r :: rs)$ & $\dn$ & $\nonnested (\sum rs)$\\
|
|
|
947 |
$\nonnested \; \, r $ & $\dn$ & $\btrue$
|
|
|
948 |
\end{tabular}
|
|
|
949 |
\end{center}
|
|
|
950 |
\noindent
|
|
|
951 |
The $\rflts$ function
|
|
|
952 |
always opens up nested alternatives,
|
|
|
953 |
which enables $\rsimp$ to be non-nested:
|
|
|
954 |
|
|
|
955 |
\begin{lemma}\label{nonnestedRsimp}
|
|
618
|
956 |
It is always the case that
|
|
|
957 |
\begin{center}
|
|
|
958 |
$\nonnested \; (\rsimp{r})$
|
|
|
959 |
\end{center}
|
|
614
|
960 |
\end{lemma}
|
|
|
961 |
\begin{proof}
|
|
618
|
962 |
By induction on $r$.
|
|
614
|
963 |
\end{proof}
|
|
|
964 |
\noindent
|
|
639
|
965 |
With this we can prove that a regular expressions
|
|
614
|
966 |
after simplification and flattening and de-duplication,
|
|
|
967 |
will not contain any alternative regular expression directly:
|
|
|
968 |
\begin{lemma}\label{nonaltFltsRd}
|
|
|
969 |
If $x \in \rdistinct{\rflts\; (\map \; \rsimp{} \; rs)}{\varnothing}$
|
|
|
970 |
then $\textit{nonAlt} \; x$.
|
|
|
971 |
\end{lemma}
|
|
|
972 |
\begin{proof}
|
|
|
973 |
By \ref{nonnestedRsimp}.
|
|
|
974 |
\end{proof}
|
|
|
975 |
\noindent
|
|
618
|
976 |
The other fact we know is that once $\rsimp{}$ has finished
|
|
614
|
977 |
processing an alternative regular expression, it will not
|
|
618
|
978 |
contain any $\RZERO$s. This is because all the recursive
|
|
614
|
979 |
calls to the simplification on the children regular expressions
|
|
618
|
980 |
make the children good, and $\rflts$ will not delete
|
|
614
|
981 |
any $\RZERO$s out of a good regular expression list,
|
|
618
|
982 |
and $\rdistinct{}$ will not ``mess'' with the result.
|
|
614
|
983 |
\begin{lemma}\label{flts3Obv}
|
|
|
984 |
The following are true:
|
|
|
985 |
\begin{itemize}
|
|
|
986 |
\item
|
|
|
987 |
If for all $r \in rs. \, \good \; r $ or $r = \RZERO$,
|
|
|
988 |
then for all $r \in \rflts\; rs. \, \good \; r$.
|
|
|
989 |
\item
|
|
|
990 |
If $x \in \rdistinct{\rflts\; (\map \; rsimp{}\; rs)}{\varnothing}$
|
|
|
991 |
and for all $y$ such that $\llbracket y \rrbracket_r$ less than
|
|
|
992 |
$\llbracket rs \rrbracket_r + 1$, either
|
|
|
993 |
$\good \; (\rsimp{y})$ or $\rsimp{y} = \RZERO$,
|
|
|
994 |
then $\good \; x$.
|
|
|
995 |
\end{itemize}
|
|
|
996 |
\end{lemma}
|
|
|
997 |
\begin{proof}
|
|
|
998 |
The first part is by induction on $rs$, where the induction
|
|
|
999 |
rule is the inductive cases for $\rflts$.
|
|
|
1000 |
The second part is a corollary from the first part.
|
|
|
1001 |
\end{proof}
|
|
|
1002 |
|
|
639
|
1003 |
This leads to good structural property of $\rsimp{}$,
|
|
614
|
1004 |
that after simplification, a regular expression is
|
|
|
1005 |
either good or $\RZERO$:
|
|
|
1006 |
\begin{lemma}\label{good1}
|
|
|
1007 |
For any r-regular expression $r$, $\good \; \rsimp{r}$ or $\rsimp{r} = \RZERO$.
|
|
|
1008 |
\end{lemma}
|
|
|
1009 |
\begin{proof}
|
|
|
1010 |
By an induction on $r$. The inductive measure is the size $\llbracket \rrbracket_r$.
|
|
618
|
1011 |
Lemma \ref{rsimpMono} says that
|
|
614
|
1012 |
$\llbracket \rsimp{r}\rrbracket_r$ is smaller than or equal to
|
|
|
1013 |
$\llbracket r \rrbracket_r$.
|
|
|
1014 |
Therefore, in the $r_1 \cdot r_2$ and $\sum rs$ case,
|
|
|
1015 |
Inductive hypothesis applies to the children regular expressions
|
|
|
1016 |
$r_1$, $r_2$, etc. The lemma \ref{flts3Obv}'s precondition is satisfied
|
|
|
1017 |
by that as well.
|
|
|
1018 |
The lemmas \ref{nonnestedRsimp} and \ref{nonaltFltsRd} are used
|
|
|
1019 |
to ensure that goodness is preserved at the topmost level.
|
|
|
1020 |
\end{proof}
|
|
|
1021 |
We shall prove that any good regular expression is
|
|
639
|
1022 |
a fixed-point for $\textit{rsimp}$.
|
|
614
|
1023 |
First we prove an auxiliary lemma:
|
|
|
1024 |
\begin{lemma}\label{goodaltsNonalt}
|
|
|
1025 |
If $\good \; \sum rs$, then $\rflts\; rs = rs$.
|
|
|
1026 |
\end{lemma}
|
|
|
1027 |
\begin{proof}
|
|
|
1028 |
By an induction on $\sum rs$. The inductive rules are the cases
|
|
|
1029 |
for $\good$.
|
|
|
1030 |
\end{proof}
|
|
|
1031 |
\noindent
|
|
|
1032 |
Now we are ready to prove that good regular expressions are invariant
|
|
618
|
1033 |
with respect to $\rsimp{}$:
|
|
614
|
1034 |
\begin{lemma}\label{test}
|
|
|
1035 |
If $\good \;r$ then $\rsimp{r} = r$.
|
|
|
1036 |
\end{lemma}
|
|
|
1037 |
\begin{proof}
|
|
|
1038 |
By an induction on the inductive cases of $\good$, using lemmas
|
|
|
1039 |
\ref{goodaltsNonalt} and \ref{rdistinctOnDistinct}.
|
|
|
1040 |
The lemma \ref{goodaltsNonalt} is used in the alternative
|
|
|
1041 |
case where 2 or more elements are present in the list.
|
|
|
1042 |
\end{proof}
|
|
|
1043 |
\noindent
|
|
639
|
1044 |
Below we show a property involving $\rflts$, $\textit{rdistinct}$,
|
|
618
|
1045 |
$\rsimp{}$ and $\rsimp_{ALTS}$,
|
|
|
1046 |
which requires $\ref{good1}$ to go through smoothly:
|
|
614
|
1047 |
\begin{lemma}\label{flattenRsimpalts}
|
|
618
|
1048 |
An application of $\rsimp_{ALTS}$ can be ``absorbed'',
|
|
|
1049 |
if its output is concatenated with a list and then applied to $\rflts$.
|
|
|
1050 |
\begin{center}
|
|
614
|
1051 |
$\rflts \; ( (\rsimp_{ALTS} \;
|
|
|
1052 |
(\rdistinct{(\rflts \; (\map \; \rsimp{}\; rs))}{\varnothing})) ::
|
|
|
1053 |
\map \; \rsimp{} \; rs' ) =
|
|
|
1054 |
\rflts \; ( (\rdistinct{(\rflts \; (\map \; \rsimp{}\; rs))}{\varnothing}) @ (
|
|
|
1055 |
\map \; \rsimp{rs'}))$
|
|
618
|
1056 |
\end{center}
|
|
614
|
1057 |
|
|
|
1058 |
|
|
|
1059 |
\end{lemma}
|
|
|
1060 |
\begin{proof}
|
|
|
1061 |
By \ref{good1}.
|
|
|
1062 |
\end{proof}
|
|
|
1063 |
\noindent
|
|
|
1064 |
|
|
|
1065 |
|
|
|
1066 |
|
|
|
1067 |
|
|
|
1068 |
|
|
|
1069 |
We are also ready to prove that $\textit{rsimp}$ is idempotent.
|
|
|
1070 |
\subsubsection{$\rsimp$ is Idempotent}
|
|
|
1071 |
The idempotency of $\rsimp$ is very useful in
|
|
|
1072 |
manipulating regular expression terms into desired
|
|
|
1073 |
forms so that key steps allowing further rewriting to closed forms
|
|
|
1074 |
are possible.
|
|
|
1075 |
\begin{lemma}\label{rsimpIdem}
|
|
618
|
1076 |
$\rsimp{r} = \rsimp{(\rsimp{r})}$
|
|
614
|
1077 |
\end{lemma}
|
|
|
1078 |
|
|
|
1079 |
\begin{proof}
|
|
|
1080 |
By \ref{test} and \ref{good1}.
|
|
|
1081 |
\end{proof}
|
|
|
1082 |
\noindent
|
|
|
1083 |
This property means we do not have to repeatedly
|
|
|
1084 |
apply simplification in each step, which justifies
|
|
|
1085 |
our definition of $\blexersimp$.
|
|
639
|
1086 |
This is in contrast to the work of Sulzmann and Lu where
|
|
|
1087 |
the simplification is applied in a fixpoint manner.
|
|
614
|
1088 |
|
|
|
1089 |
|
|
618
|
1090 |
On the other hand, we can repeat the same $\rsimp{}$ applications
|
|
614
|
1091 |
on regular expressions as many times as we want, if we have at least
|
|
639
|
1092 |
one simplification applied to it, and apply it wherever we need to:
|
|
614
|
1093 |
\begin{corollary}\label{headOneMoreSimp}
|
|
|
1094 |
The following properties hold, directly from \ref{rsimpIdem}:
|
|
|
1095 |
|
|
|
1096 |
\begin{itemize}
|
|
|
1097 |
\item
|
|
|
1098 |
$\map \; \rsimp{(r :: rs)} = \map \; \rsimp{} \; (\rsimp{r} :: rs)$
|
|
|
1099 |
\item
|
|
|
1100 |
$\rsimp{(\RALTS{rs})} = \rsimp{(\RALTS{\map \; \rsimp{} \; rs})}$
|
|
|
1101 |
\end{itemize}
|
|
|
1102 |
\end{corollary}
|
|
|
1103 |
\noindent
|
|
618
|
1104 |
This will be useful in the later closed form proof's rewriting steps.
|
|
|
1105 |
Similarly, we state the following useful facts below:
|
|
614
|
1106 |
\begin{lemma}
|
|
|
1107 |
The following equalities hold if $r = \rsimp{r'}$ for some $r'$:
|
|
|
1108 |
\begin{itemize}
|
|
|
1109 |
\item
|
|
|
1110 |
If $r = \sum rs$ then $\rsimpalts \; rs = \sum rs$.
|
|
|
1111 |
\item
|
|
|
1112 |
If $r = \sum rs$ then $\rdistinct{rs}{\varnothing} = rs$.
|
|
|
1113 |
\item
|
|
|
1114 |
$\rsimpalts \; (\rdistinct{\rflts \; [r]}{\varnothing}) = r$.
|
|
|
1115 |
\end{itemize}
|
|
|
1116 |
\end{lemma}
|
|
|
1117 |
\begin{proof}
|
|
|
1118 |
By application of lemmas \ref{rsimpIdem} and \ref{good1}.
|
|
|
1119 |
\end{proof}
|
|
|
1120 |
|
|
|
1121 |
\noindent
|
|
639
|
1122 |
With the idempotency of $\textit{rsimp}$ and its corollaries,
|
|
614
|
1123 |
we can start proving some key equalities leading to the
|
|
|
1124 |
closed forms.
|
|
639
|
1125 |
Next we present a few equivalent terms under $\textit{rsimp}$.
|
|
618
|
1126 |
To make the notation more concise
|
|
639
|
1127 |
We use $r_1 \sequal r_2 $ to denote that $\rsimp{r_1} = \rsimp{r_2}$.
|
|
|
1128 |
%\begin{center}
|
|
|
1129 |
%\begin{tabular}{lcl}
|
|
|
1130 |
% $a \sequal b$ & $ \dn$ & $ \textit{rsimp} \; a = \textit{rsimp} \; b$
|
|
|
1131 |
%\end{tabular}
|
|
|
1132 |
%\end{center}
|
|
|
1133 |
%\noindent
|
|
618
|
1134 |
%\vspace{0em}
|
|
614
|
1135 |
\begin{lemma}
|
|
618
|
1136 |
The following equivalence hold:
|
|
614
|
1137 |
\begin{itemize}
|
|
|
1138 |
\item
|
|
|
1139 |
$\rsimpalts \; (\RZERO :: rs) \sequal \rsimpalts\; rs$
|
|
|
1140 |
\item
|
|
|
1141 |
$\rsimpalts \; rs \sequal \rsimpalts (\map \; \rsimp{} \; rs)$
|
|
|
1142 |
\item
|
|
|
1143 |
$\RALTS{\RALTS{rs}} \sequal \RALTS{rs}$
|
|
|
1144 |
\item
|
|
|
1145 |
$\sum ((\sum rs_a) :: rs_b) \sequal \sum rs_a @ rs_b$
|
|
|
1146 |
\item
|
|
639
|
1147 |
$\RALTS{rs} \sequal \RALTS{\map \; \rsimp{} \; rs}$
|
|
614
|
1148 |
\end{itemize}
|
|
|
1149 |
\end{lemma}
|
|
|
1150 |
\begin{proof}
|
|
|
1151 |
By induction on the lists involved.
|
|
|
1152 |
\end{proof}
|
|
|
1153 |
\noindent
|
|
|
1154 |
The above allows us to prove
|
|
|
1155 |
two similar equalities (which are a bit more involved).
|
|
618
|
1156 |
It says that we could flatten the elements
|
|
614
|
1157 |
before simplification and still get the same result.
|
|
|
1158 |
\begin{lemma}\label{simpFlatten3}
|
|
|
1159 |
One can flatten the inside $\sum$ of a $\sum$ if it is being
|
|
|
1160 |
simplified. Concretely,
|
|
|
1161 |
\begin{itemize}
|
|
|
1162 |
\item
|
|
|
1163 |
If for all $r \in rs, rs', rs''$, we have $\good \; r $
|
|
|
1164 |
or $r = \RZERO$, then $\sum (rs' @ rs @ rs'') \sequal
|
|
|
1165 |
\sum (rs' @ [\sum rs] @ rs'')$ holds. As a corollary,
|
|
|
1166 |
\item
|
|
|
1167 |
$\sum (rs' @ [\sum rs] @ rs'') \sequal \sum (rs' @ rs @ rs'')$
|
|
|
1168 |
\end{itemize}
|
|
|
1169 |
\end{lemma}
|
|
|
1170 |
\begin{proof}
|
|
|
1171 |
By rewriting steps involving the use of \ref{test} and \ref{rdistinctConcatGeneral}.
|
|
|
1172 |
The second sub-lemma is a corollary of the previous.
|
|
|
1173 |
\end{proof}
|
|
|
1174 |
%Rewriting steps not put in--too long and complicated-------------------------------
|
|
|
1175 |
\begin{comment}
|
|
|
1176 |
\begin{center}
|
|
|
1177 |
$\rsimp{\sum (rs' @ rs @ rs'')} \stackrel{def of bsimp}{=}$ \\
|
|
|
1178 |
$\rsimpalts \; (\rdistinct{\rflts \; ((\map \; \rsimp{}\; rs') @ (\map \; \rsimp{} \; rs ) @ (\map \; \rsimp{} \; rs''))}{\varnothing})$ \\
|
|
|
1179 |
$\stackrel{by \ref{test}}{=}
|
|
|
1180 |
\rsimpalts \; (\rdistinct{(\rflts \; rs' @ \rflts \; rs @ \rflts \; rs'')}{
|
|
|
1181 |
\varnothing})$\\
|
|
|
1182 |
$\stackrel{by \ref{rdistinctConcatGeneral}}{=}
|
|
|
1183 |
\rsimpalts \; (\rdistinct{\rflts \; rs'}{\varnothing} @ \rdistinct{(
|
|
|
1184 |
\rflts\; rs @ \rflts \; rs'')}{\rflts \; rs'})$\\
|
|
|
1185 |
|
|
|
1186 |
\end{center}
|
|
|
1187 |
\end{comment}
|
|
|
1188 |
%Rewriting steps not put in--too long and complicated-------------------------------
|
|
|
1189 |
\noindent
|
|
|
1190 |
|
|
|
1191 |
|
|
618
|
1192 |
We need more equalities like the above to enable a closed form lemma,
|
|
613
|
1193 |
for which we need to introduce a few rewrite relations
|
|
|
1194 |
to help
|
|
|
1195 |
us obtain them.
|
|
554
|
1196 |
|
|
610
|
1197 |
\subsection{The rewrite relation $\hrewrite$ , $\scfrewrites$ , $\frewrite$ and $\grewrite$}
|
|
613
|
1198 |
Inspired by the success we had in the correctness proof
|
|
|
1199 |
in \ref{Bitcoded2},
|
|
|
1200 |
we follow suit here, defining atomic simplification
|
|
|
1201 |
steps as ``small-step'' rewriting steps. This allows capturing
|
|
555
|
1202 |
similarities between terms that would be otherwise
|
|
|
1203 |
hard to express.
|
|
|
1204 |
|
|
557
|
1205 |
We use $\hrewrite$ for one-step atomic rewrite of
|
|
|
1206 |
regular expression simplification,
|
|
555
|
1207 |
$\frewrite$ for rewrite of list of regular expressions that
|
|
|
1208 |
include all operations carried out in $\rflts$, and $\grewrite$ for
|
|
613
|
1209 |
rewriting a list of regular expressions possible in both $\rflts$ and $\textit{rdistinct}$.
|
|
555
|
1210 |
Their reflexive transitive closures are used to denote zero or many steps,
|
|
|
1211 |
as was the case in the previous chapter.
|
|
613
|
1212 |
As we have already
|
|
|
1213 |
done something similar, the presentation about
|
|
|
1214 |
these rewriting rules will be more concise than that in \ref{Bitcoded2}.
|
|
554
|
1215 |
To differentiate between the rewriting steps for annotated regular expressions
|
|
|
1216 |
and $\rrexp$s, we add characters $h$ and $g$ below the squig arrow symbol
|
|
|
1217 |
to mean atomic simplification transitions
|
|
|
1218 |
of $\rrexp$s and $\rrexp$ lists, respectively.
|
|
|
1219 |
|
|
555
|
1220 |
|
|
|
1221 |
|
|
|
1222 |
|
|
613
|
1223 |
\begin{figure}[H]
|
|
554
|
1224 |
\begin{center}
|
|
593
|
1225 |
\begin{mathpar}
|
|
|
1226 |
\inferrule[RSEQ0L]{}{\RZERO \cdot r_2 \hrewrite \RZERO\\}
|
|
555
|
1227 |
|
|
593
|
1228 |
\inferrule[RSEQ0R]{}{r_1 \cdot \RZERO \hrewrite \RZERO\\}
|
|
555
|
1229 |
|
|
593
|
1230 |
\inferrule[RSEQ1]{}{(\RONE \cdot r) \hrewrite r\\}\\
|
|
555
|
1231 |
|
|
593
|
1232 |
\inferrule[RSEQL]{ r_1 \hrewrite r_2}{r_1 \cdot r_3 \hrewrite r_2 \cdot r_3\\}
|
|
|
1233 |
|
|
|
1234 |
\inferrule[RSEQR]{ r_3 \hrewrite r_4}{r_1 \cdot r_3 \hrewrite r_1 \cdot r_4\\}\\
|
|
555
|
1235 |
|
|
593
|
1236 |
\inferrule[RALTSChild]{r \hrewrite r'}{\sum (rs_1 @ [r] @ rs_2) \hrewrite \sum (rs_1 @ [r'] @ rs_2)\\}
|
|
555
|
1237 |
|
|
593
|
1238 |
\inferrule[RALTS0]{}{\sum (rs_a @ [\RZERO] @ rs_b) \hrewrite \sum (rs_a @ rs_b)}
|
|
555
|
1239 |
|
|
593
|
1240 |
\inferrule[RALTSNested]{}{\sum (rs_a @ [\sum rs_1] @ rs_b) \hrewrite \sum (rs_a @ rs_1 @ rs_b)}
|
|
555
|
1241 |
|
|
593
|
1242 |
\inferrule[RALTSNil]{}{ \sum [] \hrewrite \RZERO\\}
|
|
555
|
1243 |
|
|
593
|
1244 |
\inferrule[RALTSSingle]{}{ \sum [r] \hrewrite r\\}
|
|
555
|
1245 |
|
|
593
|
1246 |
\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
|
1247 |
|
|
593
|
1248 |
\end{mathpar}
|
|
555
|
1249 |
\end{center}
|
|
613
|
1250 |
\caption{List of one-step rewrite rules for r-regular expressions ($\hrewrite$)}\label{hRewrite}
|
|
|
1251 |
\end{figure}
|
|
554
|
1252 |
|
|
557
|
1253 |
|
|
613
|
1254 |
Like $\rightsquigarrow_s$, it is
|
|
|
1255 |
convenient to define rewrite rules for a list of regular expressions,
|
|
593
|
1256 |
where each element can rewrite in many steps to the other (scf stands for
|
|
|
1257 |
li\emph{s}t \emph{c}losed \emph{f}orm). This relation is similar to the
|
|
|
1258 |
$\stackrel{s*}{\rightsquigarrow}$ for annotated regular expressions.
|
|
557
|
1259 |
|
|
613
|
1260 |
\begin{figure}[H]
|
|
557
|
1261 |
\begin{center}
|
|
593
|
1262 |
\begin{mathpar}
|
|
|
1263 |
\inferrule{}{[] \scfrewrites [] }
|
|
613
|
1264 |
|
|
593
|
1265 |
\inferrule{r \hrewrites r' \\ rs \scfrewrites rs'}{r :: rs \scfrewrites r' :: rs'}
|
|
|
1266 |
\end{mathpar}
|
|
557
|
1267 |
\end{center}
|
|
613
|
1268 |
\caption{List of one-step rewrite rules for a list of r-regular expressions}\label{scfRewrite}
|
|
|
1269 |
\end{figure}
|
|
555
|
1270 |
%frewrite
|
|
593
|
1271 |
List of one-step rewrite rules for flattening
|
|
|
1272 |
a list of regular expressions($\frewrite$):
|
|
613
|
1273 |
\begin{figure}[H]
|
|
555
|
1274 |
\begin{center}
|
|
593
|
1275 |
\begin{mathpar}
|
|
|
1276 |
\inferrule{}{\RZERO :: rs \frewrite rs \\}
|
|
555
|
1277 |
|
|
593
|
1278 |
\inferrule{}{(\sum rs) :: rs_a \frewrite rs @ rs_a \\}
|
|
555
|
1279 |
|
|
593
|
1280 |
\inferrule{rs_1 \frewrite rs_2}{r :: rs_1 \frewrite r :: rs_2}
|
|
|
1281 |
\end{mathpar}
|
|
555
|
1282 |
\end{center}
|
|
613
|
1283 |
\caption{List of one-step rewrite rules characterising the $\rflts$ operation on a list}\label{fRewrites}
|
|
|
1284 |
\end{figure}
|
|
555
|
1285 |
|
|
593
|
1286 |
Lists of one-step rewrite rules for flattening and de-duplicating
|
|
|
1287 |
a list of regular expressions ($\grewrite$):
|
|
613
|
1288 |
\begin{figure}[H]
|
|
555
|
1289 |
\begin{center}
|
|
593
|
1290 |
\begin{mathpar}
|
|
|
1291 |
\inferrule{}{\RZERO :: rs \grewrite rs \\}
|
|
532
|
1292 |
|
|
593
|
1293 |
\inferrule{}{(\sum rs) :: rs_a \grewrite rs @ rs_a \\}
|
|
555
|
1294 |
|
|
593
|
1295 |
\inferrule{rs_1 \grewrite rs_2}{r :: rs_1 \grewrite r :: rs_2}
|
|
555
|
1296 |
|
|
593
|
1297 |
\inferrule[dB]{}{rs_a @ [a] @ rs_b @[a] @ rs_c \grewrite rs_a @ [a] @ rsb @ rsc}
|
|
|
1298 |
\end{mathpar}
|
|
555
|
1299 |
\end{center}
|
|
613
|
1300 |
\caption{List of one-step rewrite rules characterising the $\rflts$ and $\textit{rdistinct}$
|
|
|
1301 |
operations}\label{gRewrite}
|
|
|
1302 |
\end{figure}
|
|
555
|
1303 |
\noindent
|
|
618
|
1304 |
We define
|
|
613
|
1305 |
two separate list rewriting relations $\frewrite$ and $\grewrite$.
|
|
611
|
1306 |
The rewriting steps that take place during
|
|
639
|
1307 |
flattening are characterised by $\frewrite$.
|
|
618
|
1308 |
The rewrite relation $\grewrite$ characterises both flattening and de-duplicating.
|
|
557
|
1309 |
Sometimes $\grewrites$ is slightly too powerful
|
|
613
|
1310 |
so we would rather use $\frewrites$ to prove
|
|
|
1311 |
%because we only
|
|
|
1312 |
equalities related to $\rflts$.
|
|
|
1313 |
%certain equivalence under the rewriting steps of $\frewrites$.
|
|
556
|
1314 |
For example, when proving the closed-form for the alternative regular expression,
|
|
613
|
1315 |
one of the equalities needed is:
|
|
|
1316 |
\begin{center}
|
|
557
|
1317 |
$\sum (\rDistinct \;\; (\map \; (\_ \backslash x) \; (\rflts \; rs)) \;\; \varnothing) \sequal
|
|
593
|
1318 |
\sum (\rDistinct \;\; (\rflts \; (\map \; (\_ \backslash x) \; rs)) \;\; \varnothing)
|
|
|
1319 |
$
|
|
613
|
1320 |
\end{center}
|
|
556
|
1321 |
\noindent
|
|
|
1322 |
Proving this is by first showing
|
|
557
|
1323 |
\begin{lemma}\label{earlyLaterDerFrewrites}
|
|
556
|
1324 |
$\map \; (\_ \backslash x) \; (\rflts \; rs) \frewrites
|
|
557
|
1325 |
\rflts \; (\map \; (\_ \backslash x) \; rs)$
|
|
556
|
1326 |
\end{lemma}
|
|
|
1327 |
\noindent
|
|
613
|
1328 |
and then the equivalence between two terms
|
|
618
|
1329 |
that can reduce in many steps to each other:
|
|
556
|
1330 |
\begin{lemma}\label{frewritesSimpeq}
|
|
|
1331 |
If $rs_1 \frewrites rs_2 $, then $\sum (\rDistinct \; rs_1 \; \varnothing) \sequal
|
|
557
|
1332 |
\sum (\rDistinct \; rs_2 \; \varnothing)$.
|
|
556
|
1333 |
\end{lemma}
|
|
557
|
1334 |
\noindent
|
|
618
|
1335 |
These two lemmas can both be proven using a straightforward induction (and
|
|
|
1336 |
the proofs for them are therefore omitted).
|
|
613
|
1337 |
|
|
639
|
1338 |
Now the above equalities can be derived with ease:
|
|
613
|
1339 |
\begin{corollary}
|
|
|
1340 |
$\sum (\rDistinct \;\; (\map \; (\_ \backslash x) \; (\rflts \; rs)) \;\; \varnothing) \sequal
|
|
|
1341 |
\sum (\rDistinct \;\; (\rflts \; (\map \; (\_ \backslash x) \; rs)) \;\; \varnothing)
|
|
|
1342 |
$
|
|
|
1343 |
\end{corollary}
|
|
618
|
1344 |
\begin{proof}
|
|
|
1345 |
By lemmas \ref{earlyLaterDerFrewrites} and \ref{frewritesSimpeq}.
|
|
|
1346 |
\end{proof}
|
|
557
|
1347 |
But this trick will not work for $\grewrites$.
|
|
|
1348 |
For example, a rewriting step in proving
|
|
|
1349 |
closed forms is:
|
|
|
1350 |
\begin{center}
|
|
593
|
1351 |
$\rsimp{(\rsimpalts \; (\map \; (\_ \backslash x) \; (\rdistinct{(\rflts \; (\map \; (\rsimp{} \; \circ \; (\lambda r. \rderssimp{r}{xs}))))}{\varnothing})))}$\\
|
|
|
1352 |
$=$ \\
|
|
|
1353 |
$\rsimp{(\rsimpalts \; (\rdistinct{(\map \; (\_ \backslash x) \; (\rflts \; (\map \; (\rsimp{} \; \circ \; (\lambda r. \rderssimp{r}{xs})))) ) }{\varnothing}))} $
|
|
|
1354 |
\noindent
|
|
557
|
1355 |
\end{center}
|
|
618
|
1356 |
For this, one would hope to have a rewriting relation between the two lists involved,
|
|
557
|
1357 |
similar to \ref{earlyLaterDerFrewrites}. However, it turns out that
|
|
556
|
1358 |
\begin{center}
|
|
593
|
1359 |
$\map \; (\_ \backslash x) \; (\rDistinct \; rs \; rset) \grewrites \rDistinct \; (\map \;
|
|
|
1360 |
(\_ \backslash x) \; rs) \; ( rset \backslash x)$
|
|
556
|
1361 |
\end{center}
|
|
|
1362 |
\noindent
|
|
557
|
1363 |
does $\mathbf{not}$ hold in general.
|
|
|
1364 |
For this rewriting step we will introduce some slightly more cumbersome
|
|
618
|
1365 |
proof technique later.
|
|
557
|
1366 |
The point is that $\frewrite$
|
|
613
|
1367 |
allows us to prove equivalence in a straightforward way that is
|
|
|
1368 |
not possible for $\grewrite$.
|
|
555
|
1369 |
|
|
556
|
1370 |
|
|
557
|
1371 |
\subsubsection{Terms That Can Be Rewritten Using $\hrewrites$, $\grewrites$, and $\frewrites$}
|
|
613
|
1372 |
In this part, we present lemmas stating
|
|
618
|
1373 |
pairs of r-regular expressions and r-regular expression lists
|
|
639
|
1374 |
where one can rewrite from one in many steps to the other.
|
|
613
|
1375 |
Most of the proofs to these lemmas are straightforward, using
|
|
618
|
1376 |
an induction on the corresponding rewriting relations.
|
|
613
|
1377 |
These proofs will therefore be omitted when this is the case.
|
|
618
|
1378 |
We present in the following lemma a few pairs of terms that are rewritable via
|
|
557
|
1379 |
$\grewrites$:
|
|
|
1380 |
\begin{lemma}\label{gstarRdistinctGeneral}
|
|
613
|
1381 |
\mbox{}
|
|
557
|
1382 |
\begin{itemize}
|
|
|
1383 |
\item
|
|
|
1384 |
$rs_1 @ rs \grewrites rs_1 @ (\rDistinct \; rs \; rs_1)$
|
|
|
1385 |
\item
|
|
|
1386 |
$rs \grewrites \rDistinct \; rs \; \varnothing$
|
|
|
1387 |
\item
|
|
|
1388 |
$rs_a @ (\rDistinct \; rs \; rs_a) \grewrites rs_a @ (\rDistinct \;
|
|
|
1389 |
rs \; (\{\RZERO\} \cup rs_a))$
|
|
|
1390 |
\item
|
|
|
1391 |
$rs \;\; @ \;\; \rDistinct \; rs_a \; rset \grewrites rs @ \rDistinct \; rs_a \;
|
|
|
1392 |
(rest \cup rs)$
|
|
|
1393 |
|
|
|
1394 |
\end{itemize}
|
|
|
1395 |
\end{lemma}
|
|
|
1396 |
\noindent
|
|
|
1397 |
If a pair of terms $rs_1, rs_2$ are rewritable via $\grewrites$ to each other,
|
|
|
1398 |
then they are equivalent under $\rsimp{}$:
|
|
|
1399 |
\begin{lemma}\label{grewritesSimpalts}
|
|
618
|
1400 |
\mbox{}
|
|
557
|
1401 |
If $rs_1 \grewrites rs_2$, then
|
|
613
|
1402 |
we have the following equivalence:
|
|
557
|
1403 |
\begin{itemize}
|
|
|
1404 |
\item
|
|
|
1405 |
$\sum rs_1 \sequal \sum rs_2$
|
|
|
1406 |
\item
|
|
|
1407 |
$\rsimpalts \; rs_1 \sequal \rsimpalts \; rs_2$
|
|
|
1408 |
\end{itemize}
|
|
|
1409 |
\end{lemma}
|
|
|
1410 |
\noindent
|
|
|
1411 |
Here are a few connecting lemmas showing that
|
|
|
1412 |
if a list of regular expressions can be rewritten using $\grewrites$ or $\frewrites $ or
|
|
|
1413 |
$\scfrewrites$,
|
|
|
1414 |
then an alternative constructor taking the list can also be rewritten using $\hrewrites$:
|
|
|
1415 |
\begin{lemma}
|
|
|
1416 |
\begin{itemize}
|
|
|
1417 |
\item
|
|
|
1418 |
If $rs \grewrites rs'$ then $\sum rs \hrewrites \sum rs'$.
|
|
|
1419 |
\item
|
|
|
1420 |
If $rs \grewrites rs'$ then $\sum rs \hrewrites \rsimpalts \; rs'$
|
|
|
1421 |
\item
|
|
|
1422 |
If $rs_1 \scfrewrites rs_2$ then $\sum (rs @ rs_1) \hrewrites \sum (rs @ rs_2)$
|
|
|
1423 |
\item
|
|
|
1424 |
If $rs_1 \scfrewrites rs_2$ then $\sum rs_1 \hrewrites \sum rs_2$
|
|
|
1425 |
|
|
|
1426 |
\end{itemize}
|
|
|
1427 |
\end{lemma}
|
|
|
1428 |
\noindent
|
|
618
|
1429 |
Now comes the core of the proof,
|
|
557
|
1430 |
which says that once two lists are rewritable to each other,
|
|
639
|
1431 |
then they are equivalent under $\textit{rsimp}$:
|
|
557
|
1432 |
\begin{lemma}
|
|
|
1433 |
If $r_1 \hrewrites r_2$ then $r_1 \sequal r_2$.
|
|
|
1434 |
\end{lemma}
|
|
|
1435 |
|
|
|
1436 |
\noindent
|
|
639
|
1437 |
Similar to what we did in chapter \ref{Bitcoded2},
|
|
618
|
1438 |
we prove that if one can rewrite from one r-regular expression ($r$)
|
|
639
|
1439 |
to the other ($r'$), after taking derivatives one can still rewrite
|
|
618
|
1440 |
the first ($r\backslash c$) to the other ($r'\backslash c$).
|
|
557
|
1441 |
\begin{lemma}\label{interleave}
|
|
|
1442 |
If $r \hrewrites r' $ then $\rder{c}{r} \hrewrites \rder{c}{r'}$
|
|
|
1443 |
\end{lemma}
|
|
|
1444 |
\noindent
|
|
618
|
1445 |
This allows us proving more $\mathbf{rsimp}$-equivalent terms, involving $\backslash_r$.
|
|
557
|
1446 |
\begin{lemma}\label{insideSimpRemoval}
|
|
618
|
1447 |
$\rsimp{(\rder{c}{(\rsimp{r})})} = \rsimp{(\rder{c}{r})} $
|
|
557
|
1448 |
\end{lemma}
|
|
|
1449 |
\noindent
|
|
|
1450 |
\begin{proof}
|
|
|
1451 |
By \ref{interleave} and \ref{rsimpIdem}.
|
|
|
1452 |
\end{proof}
|
|
|
1453 |
\noindent
|
|
|
1454 |
And this unlocks more equivalent terms:
|
|
|
1455 |
\begin{lemma}\label{Simpders}
|
|
|
1456 |
As corollaries of \ref{insideSimpRemoval}, we have
|
|
|
1457 |
\begin{itemize}
|
|
|
1458 |
\item
|
|
620
|
1459 |
If $s \neq []$ then $\rderssimp{r}{s} = \rsimp{( r \backslash_{rs} s)}$.
|
|
557
|
1460 |
\item
|
|
|
1461 |
$\rsimpalts \; (\map \; (\_ \backslash_r x) \;
|
|
593
|
1462 |
(\rdistinct{rs}{\varnothing})) \sequal
|
|
|
1463 |
\rsimpalts \; (\rDistinct \;
|
|
|
1464 |
(\map \; (\_ \backslash_r x) rs) \;\varnothing )$
|
|
|
1465 |
\end{itemize}
|
|
|
1466 |
\end{lemma}
|
|
611
|
1467 |
\begin{proof}
|
|
|
1468 |
Part 1 is by lemma \ref{insideSimpRemoval},
|
|
613
|
1469 |
part 2 is by lemma \ref{insideSimpRemoval} .%and \ref{distinctDer}.
|
|
611
|
1470 |
\end{proof}
|
|
557
|
1471 |
\noindent
|
|
613
|
1472 |
|
|
|
1473 |
\subsection{Closed Forms for $\sum rs$, $r_1\cdot r_2$ and $r^*$}
|
|
618
|
1474 |
Lemma \ref{Simpders} leads to our first closed form,
|
|
|
1475 |
which is for the alternative regular expression:
|
|
|
1476 |
\begin{theorem}\label{altsClosedForm}
|
|
|
1477 |
\mbox{}
|
|
593
|
1478 |
\begin{center}
|
|
|
1479 |
$\rderssimp{(\sum rs)}{s} \sequal
|
|
|
1480 |
\sum \; (\map \; (\rderssimp{\_}{s}) \; rs)$
|
|
|
1481 |
\end{center}
|
|
618
|
1482 |
\end{theorem}
|
|
556
|
1483 |
\noindent
|
|
557
|
1484 |
\begin{proof}
|
|
|
1485 |
By a reverse induction on the string $s$.
|
|
|
1486 |
One rewriting step, as we mentioned earlier,
|
|
|
1487 |
involves
|
|
|
1488 |
\begin{center}
|
|
|
1489 |
$\rsimpalts \; (\map \; (\_ \backslash x) \;
|
|
|
1490 |
(\rdistinct{(\rflts \; (\map \; (\rsimp{} \; \circ \;
|
|
|
1491 |
(\lambda r. \rderssimp{r}{xs}))))}{\varnothing}))
|
|
|
1492 |
\sequal
|
|
|
1493 |
\rsimpalts \; (\rdistinct{(\map \; (\_ \backslash x) \;
|
|
593
|
1494 |
(\rflts \; (\map \; (\rsimp{} \; \circ \;
|
|
557
|
1495 |
(\lambda r. \rderssimp{r}{xs})))) ) }{\varnothing}) $.
|
|
|
1496 |
\end{center}
|
|
|
1497 |
This can be proven by a combination of
|
|
|
1498 |
\ref{grewritesSimpalts}, \ref{gstarRdistinctGeneral}, \ref{rderRsimpAltsCommute}, and
|
|
|
1499 |
\ref{insideSimpRemoval}.
|
|
|
1500 |
\end{proof}
|
|
|
1501 |
\noindent
|
|
|
1502 |
This closed form has a variant which can be more convenient in later proofs:
|
|
618
|
1503 |
\begin{corollary}\label{altsClosedForm1}
|
|
557
|
1504 |
If $s \neq []$ then
|
|
|
1505 |
$\rderssimp \; (\sum \; rs) \; s =
|
|
|
1506 |
\rsimp{(\sum \; (\map \; \rderssimp{\_}{s} \; rs))}$.
|
|
|
1507 |
\end{corollary}
|
|
|
1508 |
\noindent
|
|
|
1509 |
The harder closed forms are the sequence and star ones.
|
|
613
|
1510 |
Before we obtain them, some preliminary definitions
|
|
557
|
1511 |
are needed to make proof statements concise.
|
|
556
|
1512 |
|
|
609
|
1513 |
|
|
|
1514 |
\subsubsection{Closed Form for Sequence Regular Expressions}
|
|
618
|
1515 |
For the sequence regular expression,
|
|
|
1516 |
let's first look at a series of derivative steps on it
|
|
|
1517 |
(assuming that each time when a derivative is taken,
|
|
|
1518 |
the head of the sequence is always nullable):
|
|
557
|
1519 |
\begin{center}
|
|
618
|
1520 |
\begin{tabular}{llll}
|
|
|
1521 |
$r_1 \cdot r_2$ &
|
|
|
1522 |
$\longrightarrow_{\backslash c}$ &
|
|
|
1523 |
$r_1\backslash c \cdot r_2 + r_2 \backslash c$ &
|
|
|
1524 |
$ \longrightarrow_{\backslash c'} $ \\
|
|
|
1525 |
\\
|
|
|
1526 |
$(r_1 \backslash cc' \cdot r_2 + r_2 \backslash c') + r_2 \backslash cc'$ &
|
|
|
1527 |
$\longrightarrow_{\backslash c''} $ &
|
|
|
1528 |
$((r_1 \backslash cc'c'' \cdot r_2 + r_2 \backslash c'') + r_2 \backslash c'c'')
|
|
|
1529 |
+ r_2 \backslash cc'c''$ &
|
|
|
1530 |
$ \longrightarrow_{\backslash c''} \quad \ldots$\\
|
|
|
1531 |
\end{tabular}
|
|
557
|
1532 |
\end{center}
|
|
558
|
1533 |
Roughly speaking $r_1 \cdot r_2 \backslash s$ can be expresssed as
|
|
|
1534 |
a giant alternative taking a list of terms
|
|
|
1535 |
$[r_1 \backslash_r s \cdot r_2, r_2 \backslash_r s'', r_2 \backslash_r s_1'', \ldots]$,
|
|
|
1536 |
where the head of the list is always the term
|
|
|
1537 |
representing a match involving only $r_1$, and the tail of the list consisting of
|
|
|
1538 |
terms of the shape $r_2 \backslash_r s''$, $s''$ being a suffix of $s$.
|
|
618
|
1539 |
This intuition is also echoed by Murugesan and Sundaram \cite{Murugesan2014},
|
|
|
1540 |
where they gave
|
|
557
|
1541 |
a pencil-and-paper derivation of $(r_1 \cdot r_2)\backslash s$:
|
|
532
|
1542 |
\begin{center}
|
|
618
|
1543 |
\begin{tabular}{lc}
|
|
|
1544 |
$L \; [ (r_1 \cdot r_2) \backslash_r (c_1 :: c_2 :: \ldots c_n) ]$ & $ =$\\
|
|
|
1545 |
\\
|
|
|
1546 |
\rule{0pt}{3ex} $L \; [ ((r_1 \backslash_r c_1) \cdot r_2 +
|
|
|
1547 |
(\delta\; (\nullable \; r_1) \; (r_2 \backslash_r c_1) )) \backslash_r
|
|
|
1548 |
(c_2 :: \ldots c_n) ]$ &
|
|
|
1549 |
$=$\\
|
|
|
1550 |
\\
|
|
|
1551 |
\rule{0pt}{3ex} $L \; [ ((r_1 \backslash_r c_1c_2 \cdot r_2 +
|
|
|
1552 |
(\delta \; (\nullable \; r_1) \; (r_2 \backslash_r c_1c_2)))
|
|
|
1553 |
$ & \\
|
|
|
1554 |
\\
|
|
|
1555 |
$\quad + (\delta \ (\nullable \; r_1 \backslash_r c)\; (r_2 \backslash_r c_2) ))
|
|
|
1556 |
\backslash_r (c_3 \ldots c_n) ]$ & $\ldots$ \\
|
|
558
|
1557 |
\end{tabular}
|
|
557
|
1558 |
\end{center}
|
|
|
1559 |
\noindent
|
|
618
|
1560 |
The $\delta$ function
|
|
|
1561 |
returns $r$ when the boolean condition
|
|
|
1562 |
$b$ evaluates to true and
|
|
639
|
1563 |
$\ZERO_r$ otherwise:
|
|
618
|
1564 |
\begin{center}
|
|
|
1565 |
\begin{tabular}{lcl}
|
|
|
1566 |
$\delta \; b\; r$ & $\dn$ & $r \quad \textit{if} \; b \; is \;\textit{true}$\\
|
|
639
|
1567 |
& $\dn$ & $\ZERO_r \quad otherwise$
|
|
618
|
1568 |
\end{tabular}
|
|
|
1569 |
\end{center}
|
|
|
1570 |
\noindent
|
|
|
1571 |
Note that the term
|
|
|
1572 |
\begin{center}
|
|
|
1573 |
\begin{tabular}{lc}
|
|
|
1574 |
\rule{0pt}{3ex} $((r_1 \backslash_r c_1c_2 \cdot r_2 +
|
|
|
1575 |
(\delta \; (\nullable \; r_1) \; (r_2 \backslash_r c_1c_2)))
|
|
|
1576 |
$ & \\
|
|
|
1577 |
\\
|
|
|
1578 |
$\quad + (\delta \ (\nullable \; r_1 \backslash_r c)\; (r_2 \backslash_r c_2) ))
|
|
|
1579 |
\backslash_r (c_3 \ldots c_n)$ &\\
|
|
|
1580 |
\end{tabular}
|
|
|
1581 |
\end{center}
|
|
|
1582 |
\noindent
|
|
558
|
1583 |
does not faithfully
|
|
|
1584 |
represent what the intermediate derivatives would actually look like
|
|
|
1585 |
when one or more intermediate results $r_1 \backslash s' \cdot r_2$ are not
|
|
|
1586 |
nullable in the head of the sequence.
|
|
|
1587 |
For example, when $r_1$ and $r_1 \backslash_r c_1$ are not nullable,
|
|
|
1588 |
the regular expression would not look like
|
|
|
1589 |
\[
|
|
618
|
1590 |
r_1 \backslash_r c_1c_2
|
|
558
|
1591 |
\]
|
|
618
|
1592 |
instead of
|
|
|
1593 |
\[
|
|
639
|
1594 |
(r_1 \backslash_r c_1c_2 + \ZERO_r ) + \ZERO_r.
|
|
618
|
1595 |
\]
|
|
639
|
1596 |
The redundant $\ZERO_r$s will not be created in the
|
|
558
|
1597 |
first place.
|
|
618
|
1598 |
In a closed-form one needs to take into account this (because
|
|
|
1599 |
closed forms require exact equality rather than language equivalence)
|
|
|
1600 |
and only generate the
|
|
|
1601 |
$r_2 \backslash_r s''$ terms satisfying the property
|
|
|
1602 |
\begin{center}
|
|
|
1603 |
$\exists s'. such \; that \; s'@s'' = s \;\; \land \;\;
|
|
|
1604 |
r_1 \backslash s' \; is \; nullable$.
|
|
|
1605 |
\end{center}
|
|
|
1606 |
Given the arguments $s$ and $r_1$, we denote the list of strings
|
|
|
1607 |
$s''$ satisfying the above property as $\vsuf{s}{r_1}$.
|
|
|
1608 |
The function $\vsuf{\_}{\_}$ is defined recursively on the structure of the string\footnote{
|
|
|
1609 |
Perhaps a better name of it would be ``NullablePrefixSuffix''
|
|
|
1610 |
to differentiate with the list of \emph{all} prefixes of $s$, but
|
|
|
1611 |
that is a bit too long for a function name and we are yet to find
|
|
|
1612 |
a more concise and easy-to-understand name.}
|
|
558
|
1613 |
\begin{center}
|
|
593
|
1614 |
\begin{tabular}{lcl}
|
|
|
1615 |
$\vsuf{[]}{\_} $ & $=$ & $[]$\\
|
|
618
|
1616 |
$\vsuf{c::cs}{r_1}$ & $ =$ & $ \textit{if} \; (\rnullable{r_1}) \; \textit{then} \; (\vsuf{cs}{(\rder{c}{r_1})}) @ [c :: cs]$\\
|
|
593
|
1617 |
&& $\textit{else} \; (\vsuf{cs}{(\rder{c}{r_1}) }) $
|
|
|
1618 |
\end{tabular}
|
|
558
|
1619 |
\end{center}
|
|
|
1620 |
\noindent
|
|
618
|
1621 |
The list starts with shorter suffixes
|
|
|
1622 |
and ends with longer ones (in other words, the string elements $s''$
|
|
|
1623 |
in the list $\vsuf{s}{r_1}$ are sorted
|
|
|
1624 |
in the same order as that of the terms $r_2\backslash s''$
|
|
|
1625 |
appearing in $(r_1\cdot r_2)\backslash s$).
|
|
558
|
1626 |
In essence, $\vsuf{\_}{\_}$ is doing a
|
|
|
1627 |
"virtual derivative" of $r_1 \cdot r_2$, but instead of producing
|
|
|
1628 |
the entire result $(r_1 \cdot r_2) \backslash s$,
|
|
618
|
1629 |
it only stores strings,
|
|
|
1630 |
with each string $s''$ representing a term such that $r_2 \backslash s''$
|
|
|
1631 |
is occurring in $(r_1\cdot r_2)\backslash s$.
|
|
558
|
1632 |
|
|
618
|
1633 |
With $\textit{Suffix}$ we are ready to express the
|
|
|
1634 |
sequence regular expression's closed form,
|
|
|
1635 |
but before doing so
|
|
639
|
1636 |
more definitions are needed.
|
|
618
|
1637 |
The first thing is the flattening function $\sflat{\_}$,
|
|
|
1638 |
which takes an alternative regular expression and produces a flattened version
|
|
|
1639 |
of that alternative regular expression.
|
|
|
1640 |
It is needed to convert
|
|
557
|
1641 |
a left-associative nested sequence of alternatives into
|
|
|
1642 |
a flattened list:
|
|
558
|
1643 |
\[
|
|
618
|
1644 |
\sum(\ldots ((r_1 + r_2) + r_3) + \ldots)
|
|
|
1645 |
\stackrel{\sflat{\_}}{\rightarrow}
|
|
|
1646 |
\sum[r_1, r_2, r_3, \ldots]
|
|
558
|
1647 |
\]
|
|
|
1648 |
\noindent
|
|
618
|
1649 |
The definitions of $\sflat{\_}$ and helper functions
|
|
|
1650 |
$\sflataux{\_}$ and $\llparenthesis \_ \rrparenthesis''$ are given below.
|
|
593
|
1651 |
\begin{center}
|
|
618
|
1652 |
\begin{tabular}{lcl}
|
|
|
1653 |
$\sflataux{\sum r :: rs}$ & $\dn$ & $\sflataux{r} @ rs$\\
|
|
|
1654 |
$\sflataux{\sum []}$ & $ \dn $ & $ []$\\
|
|
|
1655 |
$\sflataux r$ & $\dn$ & $ [r]$
|
|
593
|
1656 |
\end{tabular}
|
|
532
|
1657 |
\end{center}
|
|
|
1658 |
|
|
593
|
1659 |
\begin{center}
|
|
618
|
1660 |
\begin{tabular}{lcl}
|
|
|
1661 |
$\sflat{(\sum r :: rs)}$ & $\dn$ & $\sum (\sflataux{r} @ rs)$\\
|
|
|
1662 |
$\sflat{\sum []}$ & $ \dn $ & $ \sum []$\\
|
|
|
1663 |
$\sflat r$ & $\dn$ & $ r$
|
|
|
1664 |
\end{tabular}
|
|
|
1665 |
\end{center}
|
|
|
1666 |
|
|
|
1667 |
\begin{center}
|
|
|
1668 |
\begin{tabular}{lcl}
|
|
|
1669 |
$\sflataux{[]}'$ & $ \dn $ & $ []$\\
|
|
|
1670 |
$\sflataux{ (r_1 + r_2) :: rs }'$ & $\dn$ & $r_1 :: r_2 :: rs$\\
|
|
639
|
1671 |
$\sflataux{r :: rs}'$ & $\dn$ & $ r::rs$
|
|
593
|
1672 |
\end{tabular}
|
|
557
|
1673 |
\end{center}
|
|
558
|
1674 |
\noindent
|
|
576
|
1675 |
$\sflataux{\_}$ breaks up nested alternative regular expressions
|
|
557
|
1676 |
of the $(\ldots((r_1 + r_2) + r_3) + \ldots )$(left-associated) shape
|
|
558
|
1677 |
into a "balanced" list: $\AALTS{\_}{[r_1,\, r_2 ,\, r_3, \ldots]}$.
|
|
557
|
1678 |
It will return the singleton list $[r]$ otherwise.
|
|
|
1679 |
$\sflat{\_}$ works the same as $\sflataux{\_}$, except that it keeps
|
|
|
1680 |
the output type a regular expression, not a list.
|
|
558
|
1681 |
$\sflataux{\_}$ and $\sflat{\_}$ are only recursive on the
|
|
|
1682 |
first element of the list.
|
|
618
|
1683 |
$\sflataux{\_}'$ takes a list of regular expressions as input, and outputs
|
|
|
1684 |
a list of regular expressions.
|
|
|
1685 |
The use of $\sflataux{\_}$ and $\sflataux{\_}'$ is clear once we have
|
|
|
1686 |
$\textit{createdBySequence}$ defined:
|
|
|
1687 |
\begin{center}
|
|
|
1688 |
\begin{mathpar}
|
|
|
1689 |
\inferrule{\mbox{}}{\textit{createdBySequence}\; (r_1 \cdot r_2)}
|
|
558
|
1690 |
|
|
618
|
1691 |
\inferrule{\textit{createdBySequence} \; r_1}{\textit{createdBySequence} \;
|
|
|
1692 |
(r_1 + r_2)}
|
|
|
1693 |
\end{mathpar}
|
|
|
1694 |
\end{center}
|
|
|
1695 |
\noindent
|
|
|
1696 |
The predicate $\textit{createdBySequence}$ is used to describe the shape of
|
|
|
1697 |
the derivative regular expressions $(r_1\cdot r_2) \backslash s$:
|
|
|
1698 |
\begin{lemma}\label{recursivelyDerseq}
|
|
|
1699 |
It is always the case that
|
|
|
1700 |
\begin{center}
|
|
|
1701 |
$\textit{createdBySequence} \; ( (r_1\cdot r_2) \backslash_r s) $
|
|
|
1702 |
\end{center}
|
|
|
1703 |
holds.
|
|
|
1704 |
\end{lemma}
|
|
|
1705 |
\begin{proof}
|
|
|
1706 |
By a reverse induction on the string $s$, where the inductive cases are $[]$
|
|
|
1707 |
and $xs @ [x]$.
|
|
|
1708 |
\end{proof}
|
|
|
1709 |
\noindent
|
|
639
|
1710 |
If we have a regular expression $r$ whose shape
|
|
618
|
1711 |
fits into those described by $\textit{createdBySequence}$,
|
|
639
|
1712 |
then we can convert between
|
|
618
|
1713 |
$r \backslash_r c$ and $(\sflataux{r}) \backslash_r c$ with
|
|
|
1714 |
$\sflataux{\_}'$:
|
|
|
1715 |
\begin{lemma}\label{sfauIdemDer}
|
|
|
1716 |
If $\textit{createdBySequence} \; r$, then
|
|
|
1717 |
\begin{center}
|
|
|
1718 |
$\sflataux{ r \backslash_r c} =
|
|
|
1719 |
\llparenthesis (\map \; (\_ \backslash_r c) \; (\sflataux{r}) ) \rrparenthesis''$
|
|
|
1720 |
\end{center}
|
|
|
1721 |
holds.
|
|
|
1722 |
\end{lemma}
|
|
|
1723 |
\begin{proof}
|
|
|
1724 |
By a simple induction on the inductive cases of $\textit{createdBySequence}.
|
|
|
1725 |
$
|
|
|
1726 |
\end{proof}
|
|
|
1727 |
|
|
|
1728 |
Now we are ready to express
|
|
|
1729 |
the shape of $r_1 \cdot r_2 \backslash s$
|
|
558
|
1730 |
\begin{lemma}\label{seqSfau0}
|
|
618
|
1731 |
$\sflataux{(r_1 \cdot r_2) \backslash_r s} = (r_1 \backslash_r s) \cdot r_2
|
|
639
|
1732 |
:: (\map \; (r_2 \backslash_r \_) \; (\textit{Suffix} \; s \; r_1))$
|
|
558
|
1733 |
\end{lemma}
|
|
|
1734 |
\begin{proof}
|
|
618
|
1735 |
By a reverse induction on the string $s$, where the inductive cases
|
|
|
1736 |
are $[]$ and $xs @ [x]$.
|
|
|
1737 |
For the inductive case, we know that $\textit{createdBySequence} \; ((r_1 \cdot r_2)
|
|
|
1738 |
\backslash_r xs)$ holds from lemma \ref{recursivelyDerseq},
|
|
|
1739 |
which can be used to prove
|
|
558
|
1740 |
\[
|
|
|
1741 |
\map \; (r_2 \backslash_r \_) \; (\vsuf{[x]}{(r_1 \backslash_r xs)}) \;\; @ \;\;
|
|
|
1742 |
\map \; (\_ \backslash_r x) \; (\map \; (r_2 \backslash \_) \; (\vsuf{xs}{r_1}))
|
|
|
1743 |
\]
|
|
593
|
1744 |
=
|
|
558
|
1745 |
\[
|
|
|
1746 |
\map \; (r_2 \backslash_r \_) \; (\vsuf{xs @ [x]}{r_1})
|
|
|
1747 |
\]
|
|
618
|
1748 |
using lemma \ref{sfauIdemDer}.
|
|
|
1749 |
This equality enables the inductive case to go through.
|
|
558
|
1750 |
\end{proof}
|
|
|
1751 |
\noindent
|
|
618
|
1752 |
This lemma says that $(r_1\cdot r_2)\backslash s$
|
|
|
1753 |
can be flattened into a list whose head and tail meet the description
|
|
|
1754 |
we gave earlier.
|
|
|
1755 |
%Note that this lemma does $\mathbf{not}$ depend on any
|
|
|
1756 |
%specific definitions we used,
|
|
|
1757 |
%allowing people investigating derivatives to get an alternative
|
|
|
1758 |
%view of what $r_1 \cdot r_2$ is.
|
|
532
|
1759 |
|
|
618
|
1760 |
We now use $\textit{createdBySequence}$ and
|
|
|
1761 |
$\sflataux{\_}$ to describe an intuition
|
|
639
|
1762 |
behind the sequence closed form.
|
|
618
|
1763 |
If two regular expressions only differ in the way their
|
|
|
1764 |
alternatives are nested, then we should be able to get the same result
|
|
|
1765 |
once we apply simplification to both of them:
|
|
|
1766 |
\begin{lemma}\label{sflatRsimpeq}
|
|
|
1767 |
If $r$ is created from a sequence through
|
|
|
1768 |
a series of derivatives
|
|
|
1769 |
(i.e. if $\textit{createdBySequence} \; r$ holds),
|
|
|
1770 |
and that $\sflataux{r} = rs$,
|
|
|
1771 |
then we have
|
|
|
1772 |
that
|
|
|
1773 |
\begin{center}
|
|
|
1774 |
$\textit{rsimp} \; r = \textit{rsimp} \; (\sum \; rs)$
|
|
|
1775 |
\end{center}
|
|
|
1776 |
holds.
|
|
|
1777 |
\end{lemma}
|
|
|
1778 |
\begin{proof}
|
|
|
1779 |
By an induction on the inductive cases of $\textit{createdBySequence}$.
|
|
|
1780 |
\end{proof}
|
|
|
1781 |
|
|
|
1782 |
Now we are ready for the closed form
|
|
|
1783 |
for the sequence regular expressions (without the inner applications
|
|
|
1784 |
of simplifications):
|
|
|
1785 |
\begin{lemma}\label{seqClosedFormGeneral}
|
|
558
|
1786 |
$\rsimp{\sflat{(r_1 \cdot r_2) \backslash s} }
|
|
|
1787 |
=\rsimp{(\sum ( (r_1 \backslash s) \cdot r_2 ::
|
|
593
|
1788 |
\map\; (r_2 \backslash \_) \; (\vsuf{s}{r_1})))}$
|
|
558
|
1789 |
\end{lemma}
|
|
|
1790 |
\begin{proof}
|
|
618
|
1791 |
We know that
|
|
|
1792 |
$\sflataux{(r_1 \cdot r_2) \backslash_r s} = (r_1 \backslash_r s) \cdot r_2
|
|
639
|
1793 |
:: (\map \; (r_2 \backslash_r \_) \; (\textit{Suffix} \; s \; r_1))$
|
|
618
|
1794 |
holds
|
|
|
1795 |
by lemma \ref{seqSfau0}.
|
|
|
1796 |
This allows the theorem to go through because of lemma \ref{sflatRsimpeq}.
|
|
558
|
1797 |
\end{proof}
|
|
618
|
1798 |
Together with the idempotency property of $\rsimp{}$ (lemma \ref{rsimpIdem}),
|
|
|
1799 |
it is possible to convert the above lemma to obtain the
|
|
|
1800 |
proper closed form for $\backslash_{rsimps}$ rather than $\backslash_r$:
|
|
|
1801 |
for derivatives nested with simplification:
|
|
|
1802 |
\begin{theorem}\label{seqClosedForm}
|
|
|
1803 |
$\rderssimp{(r_1 \cdot r_2)}{s} = \rsimp{(\sum ((r_1 \backslash s) \cdot r_2 )
|
|
|
1804 |
:: (\map \; (r_2 \backslash \_) (\vsuf{s}{r_1})))}$
|
|
|
1805 |
\end{theorem}
|
|
|
1806 |
\begin{proof}
|
|
|
1807 |
By a case analysis of the string $s$.
|
|
|
1808 |
When $s$ is an empty list, the rewrite is straightforward.
|
|
|
1809 |
When $s$ is a non-empty list, the
|
|
|
1810 |
lemmas \ref{seqClosedFormGeneral} and \ref{Simpders} apply,
|
|
|
1811 |
making the proof go through.
|
|
|
1812 |
\end{proof}
|
|
609
|
1813 |
\subsubsection{Closed Forms for Star Regular Expressions}
|
|
618
|
1814 |
The closed form for the star regular expression involves similar tricks
|
|
|
1815 |
for the sequence regular expression.
|
|
|
1816 |
The $\textit{Suffix}$ function is now replaced by something
|
|
|
1817 |
slightly more complex, because the growth pattern of star
|
|
|
1818 |
regular expressions' derivatives is a bit different:
|
|
564
|
1819 |
\begin{center}
|
|
618
|
1820 |
\begin{tabular}{lclc}
|
|
|
1821 |
$r^* $ & $\longrightarrow_{\backslash c}$ &
|
|
|
1822 |
$(r\backslash c) \cdot r^*$ & $\longrightarrow_{\backslash c'}$\\
|
|
|
1823 |
\\
|
|
|
1824 |
$r \backslash cc' \cdot r^* + r \backslash c' \cdot r^*$ &
|
|
|
1825 |
$\longrightarrow_{\backslash c''}$ &
|
|
|
1826 |
$(r_1 \backslash cc'c'' \cdot r^* + r \backslash c'') +
|
|
|
1827 |
(r \backslash c'c'' \cdot r^* + r \backslash c'' \cdot r^*)$ &
|
|
|
1828 |
$\longrightarrow_{\backslash c'''}$ \\
|
|
|
1829 |
\\
|
|
|
1830 |
$\ldots$\\
|
|
|
1831 |
\end{tabular}
|
|
564
|
1832 |
\end{center}
|
|
|
1833 |
When we have a string $s = c :: c' :: c'' \ldots$ such that $r \backslash c$, $r \backslash cc'$, $r \backslash c'$,
|
|
|
1834 |
$r \backslash cc'c''$, $r \backslash c'c''$, $r\backslash c''$ etc. are all nullable,
|
|
618
|
1835 |
the number of terms in $r^* \backslash s$ will grow exponentially rather than linearly
|
|
|
1836 |
in the sequence case.
|
|
|
1837 |
The good news is that the function $\textit{rsimp}$ will again
|
|
|
1838 |
ignore the difference between differently nesting patterns of alternatives,
|
|
|
1839 |
and the exponentially growing star derivative like
|
|
|
1840 |
\begin{center}
|
|
|
1841 |
$(r_1 \backslash cc'c'' \cdot r^* + r \backslash c'') +
|
|
|
1842 |
(r \backslash c'c'' \cdot r^* + r \backslash c'' \cdot r^*) $
|
|
|
1843 |
\end{center}
|
|
|
1844 |
can be treated as
|
|
|
1845 |
\begin{center}
|
|
|
1846 |
$\RALTS{[r_1 \backslash cc'c'' \cdot r^*, r \backslash c'',
|
|
|
1847 |
r \backslash c'c'' \cdot r^*, r \backslash c'' \cdot r^*]}$
|
|
|
1848 |
\end{center}
|
|
|
1849 |
which can be de-duplicated by $\rDistinct$
|
|
|
1850 |
and therefore bounded finitely.
|
|
564
|
1851 |
|
|
639
|
1852 |
%and then de-duplicate terms of the form ($s'$ being a substring of $s$).
|
|
|
1853 |
%This allows us to use a similar technique as $r_1 \cdot r_2$ case,
|
|
618
|
1854 |
|
|
|
1855 |
Now the crux of this section is finding a suitable description
|
|
|
1856 |
for $rs$ where
|
|
|
1857 |
\begin{center}
|
|
|
1858 |
$\rderssimp{r^*}{s} = \rsimp{\sum rs}$.
|
|
|
1859 |
\end{center}
|
|
|
1860 |
holds.
|
|
|
1861 |
In addition, the list $rs$
|
|
|
1862 |
shall be in the form of
|
|
|
1863 |
$\map \; (\lambda s'. r\backslash s' \cdot r^*) \; Ss$.
|
|
|
1864 |
The $Ss$ is a list of strings, and for example in the sequence
|
|
|
1865 |
closed form it is specified as $\textit{Suffix} \; s \; r_1$.
|
|
|
1866 |
To get $Ss$ for the star regular expression,
|
|
|
1867 |
we need to introduce $\starupdate$ and $\starupdates$:
|
|
558
|
1868 |
\begin{center}
|
|
|
1869 |
\begin{tabular}{lcl}
|
|
|
1870 |
$\starupdate \; c \; r \; [] $ & $\dn$ & $[]$\\
|
|
|
1871 |
$\starupdate \; c \; r \; (s :: Ss)$ & $\dn$ & \\
|
|
|
1872 |
& & $\textit{if} \;
|
|
620
|
1873 |
(\rnullable \; (r \backslash_{rs} s))$ \\
|
|
558
|
1874 |
& & $\textit{then} \;\; (s @ [c]) :: [c] :: (
|
|
|
1875 |
\starupdate \; c \; r \; Ss)$ \\
|
|
|
1876 |
& & $\textit{else} \;\; (s @ [c]) :: (
|
|
|
1877 |
\starupdate \; c \; r \; Ss)$
|
|
|
1878 |
\end{tabular}
|
|
|
1879 |
\end{center}
|
|
|
1880 |
\begin{center}
|
|
|
1881 |
\begin{tabular}{lcl}
|
|
|
1882 |
$\starupdates \; [] \; r \; Ss$ & $=$ & $Ss$\\
|
|
|
1883 |
$\starupdates \; (c :: cs) \; r \; Ss$ & $=$ & $\starupdates \; cs \; r \; (
|
|
|
1884 |
\starupdate \; c \; r \; Ss)$
|
|
|
1885 |
\end{tabular}
|
|
|
1886 |
\end{center}
|
|
|
1887 |
\noindent
|
|
618
|
1888 |
Assuming we have that
|
|
|
1889 |
\begin{center}
|
|
|
1890 |
$\rderssimp{r^*}{s} = \rsimp{(\sum \map \; (\lambda s'. r\backslash s' \cdot r^*) \; Ss)}$.
|
|
|
1891 |
\end{center}
|
|
|
1892 |
holds.
|
|
|
1893 |
The idea of $\starupdate$ and $\starupdates$
|
|
|
1894 |
is to update $Ss$ when another
|
|
|
1895 |
derivative is taken on $\rderssimp{r^*}{s}$
|
|
|
1896 |
w.r.t a character $c$ and a string $s'$
|
|
|
1897 |
respectively.
|
|
|
1898 |
Both $\starupdate$ and $\starupdates$ take three arguments as input:
|
|
|
1899 |
the new character $c$ or string $s$ to take derivative with,
|
|
|
1900 |
the regular expression
|
|
|
1901 |
$r$ under the star $r^*$, and the
|
|
|
1902 |
list of strings $Ss$ for the derivative $r^* \backslash s$
|
|
|
1903 |
up until this point
|
|
|
1904 |
such that
|
|
|
1905 |
\begin{center}
|
|
|
1906 |
$(r^*) \backslash s = \sum_{s' \in sSet} (r\backslash s') \cdot r^*$
|
|
|
1907 |
\end{center}
|
|
|
1908 |
is satisfied.
|
|
|
1909 |
|
|
|
1910 |
Functions $\starupdate$ and $\starupdates$ characterise what the
|
|
|
1911 |
star derivatives will look like once ``straightened out'' into lists.
|
|
|
1912 |
The helper functions for such operations will be similar to
|
|
|
1913 |
$\sflat{\_}$, $\sflataux{\_}$ and $\sflataux{\_}$, which we defined for sequence.
|
|
|
1914 |
We use similar symbols to denote them, with a $*$ subscript to mark the difference.
|
|
558
|
1915 |
\begin{center}
|
|
|
1916 |
\begin{tabular}{lcl}
|
|
|
1917 |
$\hflataux{r_1 + r_2}$ & $\dn$ & $\hflataux{r_1} @ \hflataux{r_2}$\\
|
|
|
1918 |
$\hflataux{r}$ & $\dn$ & $[r]$
|
|
|
1919 |
\end{tabular}
|
|
|
1920 |
\end{center}
|
|
557
|
1921 |
|
|
|
1922 |
\begin{center}
|
|
558
|
1923 |
\begin{tabular}{lcl}
|
|
|
1924 |
$\hflat{r_1 + r_2}$ & $\dn$ & $\sum (\hflataux {r_1} @ \hflataux {r_2}) $\\
|
|
|
1925 |
$\hflat{r}$ & $\dn$ & $r$
|
|
|
1926 |
\end{tabular}
|
|
|
1927 |
\end{center}
|
|
|
1928 |
\noindent
|
|
618
|
1929 |
These definitions are tailor-made for dealing with alternatives that have
|
|
|
1930 |
originated from a star's derivatives.
|
|
|
1931 |
A typical star derivative always has the structure of a balanced binary tree:
|
|
564
|
1932 |
\begin{center}
|
|
618
|
1933 |
$(r_1 \backslash cc'c'' \cdot r^* + r \backslash c'') +
|
|
|
1934 |
(r \backslash c'c'' \cdot r^* + r \backslash c'' \cdot r^*) $
|
|
593
|
1935 |
\end{center}
|
|
618
|
1936 |
All of the nested structures of alternatives
|
|
|
1937 |
generated from derivatives are binary, and therefore
|
|
|
1938 |
$\hflat{\_}$ and $\hflataux{\_}$ only deal with binary alternatives.
|
|
|
1939 |
$\hflat{\_}$ ``untangles'' like the following:
|
|
|
1940 |
\[
|
|
|
1941 |
\sum ((r_1 + r_2) + (r_3 + r_4)) + \ldots \;
|
|
|
1942 |
\stackrel{\hflat{\_}}{\longrightarrow} \;
|
|
|
1943 |
\RALTS{[r_1, r_2, \ldots, r_n]}
|
|
|
1944 |
\]
|
|
|
1945 |
Here is a lemma stating the recursive property of $\starupdate$ and $\starupdates$,
|
|
|
1946 |
with the helpers $\hflat{\_}$ and $\hflataux{\_}$\footnote{The function $\textit{concat}$ takes a list of lists
|
|
|
1947 |
and merges each of the element lists to form a flattened list.}:
|
|
|
1948 |
\begin{lemma}\label{stupdateInduct1}
|
|
|
1949 |
\mbox
|
|
|
1950 |
For a list of strings $Ss$, the following hold.
|
|
|
1951 |
\begin{itemize}
|
|
|
1952 |
\item
|
|
|
1953 |
If we do a derivative on the terms
|
|
|
1954 |
$r\backslash_r s \cdot r^*$ (where $s$ is taken from the list $Ss$),
|
|
|
1955 |
the result will be the same as if we apply $\starupdate$ to $Ss$.
|
|
|
1956 |
\begin{center}
|
|
|
1957 |
\begin{tabular}{c}
|
|
|
1958 |
$\textit{concat} \; (\map \; (\hflataux{\_} \circ ( (\_\backslash_r x)
|
|
|
1959 |
\circ (\lambda s.\;\; (r \backslash_r s) \cdot r^*)))\; Ss )\;
|
|
|
1960 |
$\\
|
|
|
1961 |
\\
|
|
|
1962 |
$=$ \\
|
|
|
1963 |
\\
|
|
|
1964 |
$\map \; (\lambda s. (r \backslash_r s) \cdot (r^*)) \;
|
|
|
1965 |
(\starupdate \; x \; r \; Ss)$
|
|
|
1966 |
\end{tabular}
|
|
|
1967 |
\end{center}
|
|
|
1968 |
\item
|
|
|
1969 |
$\starupdates$ is ``composable'' w.r.t a derivative.
|
|
|
1970 |
It piggybacks the character $x$ to the tail of the string
|
|
|
1971 |
$xs$.
|
|
|
1972 |
\begin{center}
|
|
|
1973 |
\begin{tabular}{c}
|
|
|
1974 |
$\textit{concat} \; (\map \; \hflataux{\_} \;
|
|
|
1975 |
(\map \; (\_\backslash_r x) \;
|
|
|
1976 |
(\map \; (\lambda s.\;\; (r \backslash_r s) \cdot
|
|
|
1977 |
(r^*) ) \; (\starupdates \; xs \; r \; Ss))))$\\
|
|
|
1978 |
\\
|
|
|
1979 |
$=$\\
|
|
|
1980 |
\\
|
|
|
1981 |
$\map \; (\lambda s.\;\; (r\backslash_r s) \cdot (r^*)) \;
|
|
|
1982 |
(\starupdates \; (xs @ [x]) \; r \; Ss)$
|
|
|
1983 |
\end{tabular}
|
|
|
1984 |
\end{center}
|
|
|
1985 |
\end{itemize}
|
|
|
1986 |
\end{lemma}
|
|
|
1987 |
|
|
|
1988 |
\begin{proof}
|
|
|
1989 |
Part 1 is by induction on $Ss$.
|
|
|
1990 |
Part 2 is by induction on $xs$, where $Ss$ is left to take arbitrary values.
|
|
|
1991 |
\end{proof}
|
|
|
1992 |
|
|
593
|
1993 |
|
|
618
|
1994 |
Like $\textit{createdBySequence}$, we need
|
|
|
1995 |
a predicate for ``star-created'' regular expressions:
|
|
593
|
1996 |
\begin{center}
|
|
618
|
1997 |
\begin{mathpar}
|
|
|
1998 |
\inferrule{\mbox{}}{ \textit{createdByStar}\; \RSEQ{ra}{\RSTAR{rb}} }
|
|
|
1999 |
|
|
|
2000 |
\inferrule{ \textit{createdByStar} \; r_1\; \land \; \textit{createdByStar} \; r_2 }{\textit{createdByStar} \; (r_1 + r_2) }
|
|
|
2001 |
\end{mathpar}
|
|
593
|
2002 |
\end{center}
|
|
618
|
2003 |
\noindent
|
|
|
2004 |
All regular expressions created by taking derivatives of
|
|
|
2005 |
$r_1 \cdot (r_2)^*$ satisfy the $\textit{createdByStar}$ predicate:
|
|
|
2006 |
\begin{lemma}\label{starDersCbs}
|
|
|
2007 |
$\textit{createdByStar} \; ((r_1 \cdot r_2^*) \backslash_r s) $ holds.
|
|
|
2008 |
\end{lemma}
|
|
|
2009 |
\begin{proof}
|
|
|
2010 |
By a reverse induction on $s$.
|
|
|
2011 |
\end{proof}
|
|
|
2012 |
If a regular expression conforms to the shape of a star's derivative,
|
|
|
2013 |
then we can push an application of $\hflataux{\_}$ inside a derivative of it:
|
|
|
2014 |
\begin{lemma}\label{hfauPushin}
|
|
|
2015 |
If $\textit{createdByStar} \; r$ holds, then
|
|
|
2016 |
\begin{center}
|
|
|
2017 |
$\hflataux{r \backslash_r c} = \textit{concat} \; (
|
|
|
2018 |
\map \; \hflataux{\_} (\map \; (\_\backslash_r c) \;(\hflataux{r})))$
|
|
|
2019 |
\end{center}
|
|
|
2020 |
holds.
|
|
|
2021 |
\end{lemma}
|
|
|
2022 |
\begin{proof}
|
|
|
2023 |
By an induction on the inductivev cases of $\textit{createdByStar}$.
|
|
|
2024 |
\end{proof}
|
|
|
2025 |
%This is not entirely true for annotated regular expressions:
|
|
|
2026 |
%%TODO: bsimp bders \neq bderssimp
|
|
|
2027 |
%\begin{center}
|
|
|
2028 |
% $(1+ (c\cdot \ASEQ{bs}{c^*}{c} ))$
|
|
|
2029 |
%\end{center}
|
|
|
2030 |
%For bit-codes, the order in which simplification is applied
|
|
|
2031 |
%might cause a difference in the location they are placed.
|
|
|
2032 |
%If we want something like
|
|
|
2033 |
%\begin{center}
|
|
|
2034 |
% $\bderssimp{r}{s} \myequiv \bsimp{\bders{r}{s}}$
|
|
|
2035 |
%\end{center}
|
|
|
2036 |
%Some "canonicalization" procedure is required,
|
|
|
2037 |
%which either pushes all the common bitcodes to nodes
|
|
|
2038 |
%as senior as possible:
|
|
|
2039 |
%\begin{center}
|
|
|
2040 |
% $_{bs}(_{bs_1 @ bs'}r_1 + _{bs_1 @ bs''}r_2) \rightarrow _{bs @ bs_1}(_{bs'}r_1 + _{bs''}r_2) $
|
|
|
2041 |
%\end{center}
|
|
|
2042 |
%or does the reverse. However bitcodes are not of interest if we are talking about
|
|
|
2043 |
%the $\llbracket r \rrbracket$ size of a regex.
|
|
|
2044 |
%Therefore for the ease and simplicity of producing a
|
|
|
2045 |
%proof for a size bound, we are happy to restrict ourselves to
|
|
|
2046 |
%unannotated regular expressions, and obtain such equalities as
|
|
|
2047 |
%TODO: rsimp sflat
|
|
|
2048 |
% The simplification of a flattened out regular expression, provided it comes
|
|
|
2049 |
%from the derivative of a star, is the same as the one nested.
|
|
|
2050 |
|
|
|
2051 |
|
|
|
2052 |
|
|
|
2053 |
Now we introduce an inductive property
|
|
|
2054 |
for $\starupdate$ and $\hflataux{\_}$.
|
|
|
2055 |
\begin{lemma}\label{starHfauInduct}
|
|
|
2056 |
If we do derivatives of $r^*$
|
|
|
2057 |
with a string that starts with $c$,
|
|
|
2058 |
then flatten it out,
|
|
|
2059 |
we obtain a list
|
|
|
2060 |
of the shape $\sum_{s' \in sS} (r\backslash_r s') \cdot r^*$,
|
|
|
2061 |
where $sS = \starupdates \; s \; r \; [[c]]$. Namely,
|
|
|
2062 |
\begin{center}
|
|
620
|
2063 |
$\hflataux{(( (\rder{c}{r_0})\cdot(r_0^*))\backslash_{rs} s)} =
|
|
618
|
2064 |
\map \; (\lambda s_1. (r_0 \backslash_r s_1) \cdot (r_0^*)) \;
|
|
|
2065 |
(\starupdates \; s \; r_0 \; [[c]])$
|
|
|
2066 |
\end{center}
|
|
|
2067 |
holds.
|
|
|
2068 |
\end{lemma}
|
|
|
2069 |
\begin{proof}
|
|
|
2070 |
By an induction on $s$, the inductive cases
|
|
|
2071 |
being $[]$ and $s@[c]$. The lemmas \ref{hfauPushin} and \ref{starDersCbs} are used.
|
|
|
2072 |
\end{proof}
|
|
|
2073 |
\noindent
|
|
|
2074 |
|
|
639
|
2075 |
The function $\hflataux{\_}$ has a similar effect as $\textit{flatten}$:
|
|
618
|
2076 |
\begin{lemma}\label{hflatauxGrewrites}
|
|
|
2077 |
$a :: rs \grewrites \hflataux{a} @ rs$
|
|
|
2078 |
\end{lemma}
|
|
|
2079 |
\begin{proof}
|
|
|
2080 |
By induction on $a$. $rs$ is set to take arbitrary values.
|
|
|
2081 |
\end{proof}
|
|
638
|
2082 |
It is also not surprising that
|
|
|
2083 |
two regular expressions differing only in terms
|
|
|
2084 |
of the
|
|
|
2085 |
nesting of parentheses are equivalent w.r.t. $\textit{rsimp}$:
|
|
618
|
2086 |
\begin{lemma}\label{cbsHfauRsimpeq1}
|
|
|
2087 |
$\rsimp{(r_1 + r_2)} = \rsimp{(\RALTS{\hflataux{r_1} @ \hflataux{r_2}})}$
|
|
593
|
2088 |
\end{lemma}
|
|
|
2089 |
|
|
|
2090 |
\begin{proof}
|
|
|
2091 |
By using the rewriting relation $\rightsquigarrow$
|
|
|
2092 |
\end{proof}
|
|
639
|
2093 |
And from this we obtain that a
|
|
|
2094 |
regular expression created by star
|
|
|
2095 |
is the same as its flattened version, up to equivalence under $\textit{bsimp}$.
|
|
593
|
2096 |
For example,
|
|
618
|
2097 |
\begin{lemma}\label{hfauRsimpeq2}
|
|
639
|
2098 |
$\textit{createdByStar} \; r \implies \rsimp{r} = \rsimp{\RALTS{\hflataux{r}}}$
|
|
593
|
2099 |
\end{lemma}
|
|
|
2100 |
\begin{proof}
|
|
618
|
2101 |
By structural induction on $r$, where the induction rules
|
|
|
2102 |
are these of $\createdByStar{\_}$.
|
|
|
2103 |
Lemma \ref{cbsHfauRsimpeq1} is used in the inductive case.
|
|
593
|
2104 |
\end{proof}
|
|
564
|
2105 |
|
|
|
2106 |
|
|
618
|
2107 |
%Here is a corollary that states the lemma in
|
|
|
2108 |
%a more intuitive way:
|
|
|
2109 |
%\begin{corollary}
|
|
|
2110 |
% $\hflataux{r^* \backslash_r (c::xs)} = \map \; (\lambda s. (r \backslash_r s) \cdot
|
|
|
2111 |
% (r^*))\; (\starupdates \; c\; r\; [[c]])$
|
|
|
2112 |
%\end{corollary}
|
|
|
2113 |
%\noindent
|
|
|
2114 |
%Note that this is also agnostic of the simplification
|
|
|
2115 |
%function we defined, and is therefore of more general interest.
|
|
|
2116 |
|
|
|
2117 |
Together with the rewriting relation
|
|
|
2118 |
\begin{lemma}\label{starClosedForm6Hrewrites}
|
|
|
2119 |
We have the following set of rewriting relations or equalities:
|
|
|
2120 |
\begin{itemize}
|
|
|
2121 |
\item
|
|
|
2122 |
$\textit{rsimp} \; (r^* \backslash_r (c::s))
|
|
|
2123 |
\sequal
|
|
|
2124 |
\sum \; ( ( \sum (\lambda s. (r\backslash_r s) \cdot r^*) \; (
|
|
|
2125 |
\starupdates \; s \; r \; [ c::[]] ) ) )$
|
|
|
2126 |
\item
|
|
620
|
2127 |
$r \backslash_{rsimps} (c::s) = \textit{rsimp} \; ( (
|
|
618
|
2128 |
\sum ( (\map \; (\lambda s_1. (r\backslash s_1) \; r^*) \;
|
|
|
2129 |
(\starupdates \;s \; r \; [ c::[] ])))))$
|
|
|
2130 |
\item
|
|
|
2131 |
$\sum ( (\map \; (\lambda s. (r\backslash s) \; r^*) \; Ss))
|
|
|
2132 |
\sequal
|
|
|
2133 |
\sum ( (\map \; (\lambda s. \textit{rsimp} \; (r\backslash s) \;
|
|
|
2134 |
r^*) \; Ss) )$
|
|
|
2135 |
\item
|
|
|
2136 |
$\map \; (\lambda s. (\rsimp{r \backslash_r s}) \cdot (r^*)) \; Ss
|
|
|
2137 |
\scfrewrites
|
|
|
2138 |
\map \; (\lambda s. (\rsimp{r \backslash_r s}) \cdot (r^*)) \; Ss$
|
|
|
2139 |
\item
|
|
|
2140 |
$( ( \sum ( ( \map \ (\lambda s. \;\;
|
|
|
2141 |
(\textit{rsimp} \; (r \backslash_r s)) \cdot r^*) \; (\starupdates \;
|
|
|
2142 |
s \; r \; [ c::[] ])))))$\\
|
|
|
2143 |
$\sequal$\\
|
|
|
2144 |
$( ( \sum ( ( \map \ (\lambda s. \;\;
|
|
620
|
2145 |
( r \backslash_{rsimps} s)) \cdot r^*) \; (\starupdates \;
|
|
618
|
2146 |
s \; r \; [ c::[] ]))))$\\
|
|
|
2147 |
\end{itemize}
|
|
558
|
2148 |
\end{lemma}
|
|
|
2149 |
\begin{proof}
|
|
618
|
2150 |
Part 1 leads to part 2.
|
|
|
2151 |
The rest of them are routine.
|
|
558
|
2152 |
\end{proof}
|
|
|
2153 |
\noindent
|
|
618
|
2154 |
Next the closed form for star regular expressions can be derived:
|
|
|
2155 |
\begin{theorem}\label{starClosedForm}
|
|
558
|
2156 |
$\rderssimp{r^*}{c::s} =
|
|
|
2157 |
\rsimp{
|
|
|
2158 |
(\sum (\map \; (\lambda s. (\rderssimp{r}{s})\cdot r^*) \;
|
|
593
|
2159 |
(\starupdates \; s\; r \; [[c]])
|
|
558
|
2160 |
)
|
|
593
|
2161 |
)
|
|
|
2162 |
}
|
|
558
|
2163 |
$
|
|
618
|
2164 |
\end{theorem}
|
|
558
|
2165 |
\begin{proof}
|
|
|
2166 |
By an induction on $s$.
|
|
618
|
2167 |
The lemmas \ref{rsimpIdem}, \ref{starHfauInduct}, \ref{starClosedForm6Hrewrites}
|
|
|
2168 |
and \ref{hfauRsimpeq2}
|
|
558
|
2169 |
are used.
|
|
618
|
2170 |
In \ref{starClosedForm6Hrewrites}, the equalities are
|
|
|
2171 |
used to link the LHS and RHS.
|
|
558
|
2172 |
\end{proof}
|
|
609
|
2173 |
|
|
|
2174 |
|
|
|
2175 |
|
|
|
2176 |
|
|
|
2177 |
|
|
|
2178 |
|
|
613
|
2179 |
%----------------------------------------------------------------------------------------
|
|
|
2180 |
% SECTION ??
|
|
|
2181 |
%----------------------------------------------------------------------------------------
|
|
|
2182 |
|
|
|
2183 |
%-----------------------------------
|
|
|
2184 |
% SECTION syntactic equivalence under simp
|
|
|
2185 |
%-----------------------------------
|
|
|
2186 |
|
|
|
2187 |
|
|
|
2188 |
%----------------------------------------------------------------------------------------
|
|
|
2189 |
% SECTION ALTS CLOSED FORM
|
|
|
2190 |
%----------------------------------------------------------------------------------------
|
|
|
2191 |
%\section{A Closed Form for \textit{ALTS}}
|
|
|
2192 |
%Now we prove that $rsimp (rders\_simp (RALTS rs) s) = rsimp (RALTS (map (\lambda r. rders\_simp r s) rs))$.
|
|
|
2193 |
%
|
|
|
2194 |
%
|
|
|
2195 |
%There are a few key steps, one of these steps is
|
|
|
2196 |
%
|
|
|
2197 |
%
|
|
|
2198 |
%
|
|
|
2199 |
%One might want to prove this by something a simple statement like:
|
|
|
2200 |
%
|
|
|
2201 |
%For this to hold we want the $\textit{distinct}$ function to pick up
|
|
|
2202 |
%the elements before and after derivatives correctly:
|
|
|
2203 |
%$r \in rset \equiv (rder x r) \in (rder x rset)$.
|
|
|
2204 |
%which essentially requires that the function $\backslash$ is an injective mapping.
|
|
|
2205 |
%
|
|
|
2206 |
%Unfortunately the function $\backslash c$ is not an injective mapping.
|
|
|
2207 |
%
|
|
|
2208 |
%\subsection{function $\backslash c$ is not injective (1-to-1)}
|
|
|
2209 |
%\begin{center}
|
|
|
2210 |
% The derivative $w.r.t$ character $c$ is not one-to-one.
|
|
|
2211 |
% Formally,
|
|
|
2212 |
% $\exists r_1 \;r_2. r_1 \neq r_2 \mathit{and} r_1 \backslash c = r_2 \backslash c$
|
|
|
2213 |
%\end{center}
|
|
|
2214 |
%This property is trivially true for the
|
|
|
2215 |
%character regex example:
|
|
|
2216 |
%\begin{center}
|
|
|
2217 |
% $r_1 = e; \; r_2 = d;\; r_1 \backslash c = \ZERO = r_2 \backslash c$
|
|
|
2218 |
%\end{center}
|
|
|
2219 |
%But apart from the cases where the derivative
|
|
|
2220 |
%output is $\ZERO$, are there non-trivial results
|
|
|
2221 |
%of derivatives which contain strings?
|
|
|
2222 |
%The answer is yes.
|
|
|
2223 |
%For example,
|
|
|
2224 |
%\begin{center}
|
|
|
2225 |
% Let $r_1 = a^*b\;\quad r_2 = (a\cdot a^*)\cdot b + b$.\\
|
|
|
2226 |
% where $a$ is not nullable.\\
|
|
|
2227 |
% $r_1 \backslash c = ((a \backslash c)\cdot a^*)\cdot c + b \backslash c$\\
|
|
|
2228 |
% $r_2 \backslash c = ((a \backslash c)\cdot a^*)\cdot c + b \backslash c$
|
|
|
2229 |
%\end{center}
|
|
|
2230 |
%We start with two syntactically different regular expressions,
|
|
|
2231 |
%and end up with the same derivative result.
|
|
|
2232 |
%This is not surprising as we have such
|
|
|
2233 |
%equality as below in the style of Arden's lemma:\\
|
|
|
2234 |
%\begin{center}
|
|
|
2235 |
% $L(A^*B) = L(A\cdot A^* \cdot B + B)$
|
|
|
2236 |
%\end{center}
|
|
|
2237 |
\section{Bounding Closed Forms}
|
|
|
2238 |
|
|
|
2239 |
In this section, we introduce how we formalised the bound
|
|
|
2240 |
on closed forms.
|
|
618
|
2241 |
We first show that in general regular expressions up to a certain
|
|
|
2242 |
size are finite.
|
|
|
2243 |
Then we prove that functions such as $\rflts$
|
|
613
|
2244 |
will not cause the size of r-regular expressions to grow.
|
|
|
2245 |
Putting this together with a general bound
|
|
|
2246 |
on the finiteness of distinct regular expressions
|
|
618
|
2247 |
up to a certain size, we obtain a bound on
|
|
613
|
2248 |
the closed forms.
|
|
|
2249 |
|
|
618
|
2250 |
\subsection{Finiteness of Distinct Regular Expressions}
|
|
|
2251 |
We define the set of regular expressions whose size are no more than
|
|
|
2252 |
a certain size $N$ as $\textit{sizeNregex} \; N$:
|
|
|
2253 |
\[
|
|
|
2254 |
\textit{sizeNregex} \; N \dn \{r\; \mid \; \llbracket r \rrbracket_r \leq N \}
|
|
|
2255 |
\]
|
|
|
2256 |
We have that $\textit{sizeNregex} \; N$ is always a finite set:
|
|
|
2257 |
\begin{lemma}\label{finiteSizeN}
|
|
|
2258 |
$\textit{finite} \; (\textit{sizeNregex} \; N)$ holds.
|
|
|
2259 |
\end{lemma}
|
|
|
2260 |
\begin{proof}
|
|
|
2261 |
By splitting the set $\textit{sizeNregex} \; (N + 1)$ into
|
|
|
2262 |
subsets by their categories:
|
|
639
|
2263 |
$\{\ZERO_r, \ONE_r, c\}$, $\{r^* \mid r \in \textit{sizeNregex} \; N\}$,
|
|
618
|
2264 |
and so on. Each of these subsets are finitely bounded.
|
|
|
2265 |
\end{proof}
|
|
|
2266 |
\noindent
|
|
|
2267 |
From this we get a corollary that
|
|
|
2268 |
if forall $r \in rs$, $\rsize{r} \leq N$, then the output of
|
|
|
2269 |
$\rdistinct{rs}{\varnothing}$ is a list of regular
|
|
|
2270 |
expressions of finite size depending on $N$ only.
|
|
|
2271 |
\begin{corollary}\label{finiteSizeNCorollary}
|
|
|
2272 |
$\rsize{\rdistinct{rs}{\varnothing}} \leq c_N * N$ holds,
|
|
|
2273 |
where the constant $c_N$ is equal to $\textit{card} \; (\textit{sizeNregex} \;
|
|
|
2274 |
N)$.
|
|
|
2275 |
\end{corollary}
|
|
|
2276 |
\begin{proof}
|
|
|
2277 |
For all $r$ in
|
|
|
2278 |
$\textit{set} \; (\rdistinct{rs}{\varnothing})$,
|
|
|
2279 |
it is always the case that $\rsize{r} \leq N$.
|
|
|
2280 |
In addition, the list length is bounded by
|
|
|
2281 |
$c_N$, yielding the desired bound.
|
|
|
2282 |
\end{proof}
|
|
|
2283 |
\noindent
|
|
|
2284 |
This fact will be handy in estimating the closed form sizes.
|
|
|
2285 |
%We have proven that the size of the
|
|
|
2286 |
%output of $\textit{rdistinct} \; rs' \; \varnothing$
|
|
|
2287 |
%is bounded by a constant $N * c_N$ depending only on $N$,
|
|
|
2288 |
%provided that each of $rs'$'s element
|
|
|
2289 |
%is bounded by $N$.
|
|
|
2290 |
|
|
639
|
2291 |
\subsection{$\textit{rsimp}$ Does Not Increase the Size}
|
|
613
|
2292 |
Although it seems evident, we need a series
|
|
|
2293 |
of non-trivial lemmas to establish that functions such as $\rflts$
|
|
|
2294 |
do not cause the regular expressions to grow.
|
|
|
2295 |
\begin{lemma}\label{rsimpMonoLemmas}
|
|
|
2296 |
\mbox{}
|
|
|
2297 |
\begin{itemize}
|
|
|
2298 |
\item
|
|
|
2299 |
\[
|
|
|
2300 |
\llbracket \rsimpalts \; rs \rrbracket_r \leq
|
|
|
2301 |
\llbracket \sum \; rs \rrbracket_r
|
|
|
2302 |
\]
|
|
|
2303 |
\item
|
|
|
2304 |
\[
|
|
|
2305 |
\llbracket \rsimpseq \; r_1 \; r_2 \rrbracket_r \leq
|
|
|
2306 |
\llbracket r_1 \cdot r_2 \rrbracket_r
|
|
|
2307 |
\]
|
|
|
2308 |
\item
|
|
|
2309 |
\[
|
|
|
2310 |
\llbracket \rflts \; rs \rrbracket_r \leq
|
|
|
2311 |
\llbracket rs \rrbracket_r
|
|
|
2312 |
\]
|
|
|
2313 |
\item
|
|
|
2314 |
\[
|
|
|
2315 |
\llbracket \rDistinct \; rs \; ss \rrbracket_r \leq
|
|
|
2316 |
\llbracket rs \rrbracket_r
|
|
|
2317 |
\]
|
|
|
2318 |
\item
|
|
|
2319 |
If all elements $a$ in the set $as$ satisfy the property
|
|
|
2320 |
that $\llbracket \textit{rsimp} \; a \rrbracket_r \leq
|
|
|
2321 |
\llbracket a \rrbracket_r$, then we have
|
|
|
2322 |
\[
|
|
|
2323 |
\llbracket \; \rsimpalts \; (\textit{rdistinct} \;
|
|
|
2324 |
(\textit{rflts} \; (\textit{map}\;\textit{rsimp} as)) \{\})
|
|
|
2325 |
\rrbracket \leq
|
|
|
2326 |
\llbracket \; \sum \; (\rDistinct \; (\rflts \;(\map \;
|
|
|
2327 |
\textit{rsimp} \; x))\; \{ \} ) \rrbracket_r
|
|
|
2328 |
\]
|
|
|
2329 |
\end{itemize}
|
|
|
2330 |
\end{lemma}
|
|
|
2331 |
\begin{proof}
|
|
|
2332 |
Point 1, 3, 4 can be proven by an induction on $rs$.
|
|
|
2333 |
Point 2 is by case analysis on $r_1$ and $r_2$.
|
|
|
2334 |
The last part is a corollary of the previous ones.
|
|
|
2335 |
\end{proof}
|
|
|
2336 |
\noindent
|
|
|
2337 |
With the lemmas for each inductive case in place, we are ready to get
|
|
|
2338 |
the non-increasing property as a corollary:
|
|
|
2339 |
\begin{corollary}\label{rsimpMono}
|
|
|
2340 |
$\llbracket \textit{rsimp} \; r \rrbracket_r \leq \llbracket r \rrbracket_r$
|
|
|
2341 |
\end{corollary}
|
|
|
2342 |
\begin{proof}
|
|
|
2343 |
By \ref{rsimpMonoLemmas}.
|
|
|
2344 |
\end{proof}
|
|
|
2345 |
|
|
609
|
2346 |
\subsection{Estimating the Closed Forms' sizes}
|
|
618
|
2347 |
We recap the closed forms we obtained
|
|
639
|
2348 |
earlier:
|
|
558
|
2349 |
\begin{itemize}
|
|
|
2350 |
\item
|
|
593
|
2351 |
$\rderssimp{(\sum rs)}{s} \sequal
|
|
|
2352 |
\sum \; (\map \; (\rderssimp{\_}{s}) \; rs)$
|
|
558
|
2353 |
\item
|
|
593
|
2354 |
$\rderssimp{(r_1 \cdot r_2)}{s} \sequal \sum ((r_1 \backslash s) \cdot r_2 )
|
|
|
2355 |
:: (\map \; (r_2 \backslash \_) (\vsuf{s}{r_1}))$
|
|
558
|
2356 |
\item
|
|
|
2357 |
|
|
593
|
2358 |
$\rderssimp{r^*}{c::s} =
|
|
|
2359 |
\rsimp{
|
|
|
2360 |
(\sum (\map \; (\lambda s. (\rderssimp{r}{s})\cdot r^*) \;
|
|
558
|
2361 |
(\starupdates \; s\; r \; [[c]])
|
|
593
|
2362 |
)
|
|
|
2363 |
)
|
|
|
2364 |
}
|
|
|
2365 |
$
|
|
558
|
2366 |
\end{itemize}
|
|
|
2367 |
\noindent
|
|
|
2368 |
The closed forms on the left-hand-side
|
|
|
2369 |
are all of the same shape: $\rsimp{ (\sum rs)} $.
|
|
|
2370 |
Such regular expression will be bounded by the size of $\sum rs'$,
|
|
|
2371 |
where every element in $rs'$ is distinct, and each element
|
|
|
2372 |
can be described by some inductive sub-structures
|
|
|
2373 |
(for example when $r = r_1 \cdot r_2$ then $rs'$
|
|
|
2374 |
will be solely comprised of $r_1 \backslash s'$
|
|
|
2375 |
and $r_2 \backslash s''$, $s'$ and $s''$ being
|
|
|
2376 |
sub-strings of $s$).
|
|
|
2377 |
which will each have a size uppder bound
|
|
|
2378 |
according to inductive hypothesis, which controls $r \backslash s$.
|
|
557
|
2379 |
|
|
558
|
2380 |
We elaborate the above reasoning by a series of lemmas
|
|
|
2381 |
below, where straightforward proofs are omitted.
|
|
639
|
2382 |
%We want to apply it to our setting $\rsize{\rsimp{\sum rs}}$.
|
|
|
2383 |
We show that $\textit{rdistinct}$ and $\rflts$
|
|
609
|
2384 |
working together is at least as
|
|
639
|
2385 |
good as $\textit{rdistinct}$ alone, which can be written as
|
|
609
|
2386 |
\begin{center}
|
|
|
2387 |
$\llbracket \rdistinct{(\rflts \; \textit{rs})}{\varnothing} \rrbracket_r
|
|
|
2388 |
\leq
|
|
|
2389 |
\llbracket \rdistinct{rs}{\varnothing} \rrbracket_r $.
|
|
|
2390 |
\end{center}
|
|
|
2391 |
We need this so that we know the outcome of our real
|
|
|
2392 |
simplification is better than or equal to a rough estimate,
|
|
|
2393 |
and therefore can be bounded by that estimate.
|
|
|
2394 |
This is a bit harder to establish compared with proving
|
|
|
2395 |
$\textit{flts}$ does not make a list larger (which can
|
|
|
2396 |
be proven using routine induction):
|
|
|
2397 |
\begin{center}
|
|
|
2398 |
$\llbracket \textit{rflts}\; rs \rrbracket_r \leq
|
|
|
2399 |
\llbracket \textit{rs} \rrbracket_r$
|
|
|
2400 |
\end{center}
|
|
|
2401 |
We cannot simply prove how each helper function
|
|
|
2402 |
reduces the size and then put them together:
|
|
|
2403 |
From
|
|
|
2404 |
\begin{center}
|
|
|
2405 |
$\llbracket \textit{rflts}\; rs \rrbracket_r \leq
|
|
618
|
2406 |
\llbracket \textit{rs} \rrbracket_r$
|
|
609
|
2407 |
\end{center}
|
|
|
2408 |
and
|
|
|
2409 |
\begin{center}
|
|
|
2410 |
$\llbracket \textit{rdistinct} \; rs \; \varnothing \leq
|
|
|
2411 |
\llbracket rs \rrbracket_r$
|
|
|
2412 |
\end{center}
|
|
618
|
2413 |
one cannot infer
|
|
609
|
2414 |
\begin{center}
|
|
558
|
2415 |
$\llbracket \rdistinct{(\rflts \; \textit{rs})}{\varnothing} \rrbracket_r
|
|
|
2416 |
\leq
|
|
|
2417 |
\llbracket \rdistinct{rs}{\varnothing} \rrbracket_r $.
|
|
609
|
2418 |
\end{center}
|
|
618
|
2419 |
What we can infer is that
|
|
609
|
2420 |
\begin{center}
|
|
|
2421 |
$\llbracket \rdistinct{(\rflts \; \textit{rs})}{\varnothing} \rrbracket_r
|
|
|
2422 |
\leq
|
|
|
2423 |
\llbracket rs \rrbracket_r$
|
|
|
2424 |
\end{center}
|
|
|
2425 |
but this estimate is too rough and $\llbracket rs \rrbracket_r$ is unbounded.
|
|
|
2426 |
The way we
|
|
618
|
2427 |
get around this is by first proving a more general lemma
|
|
609
|
2428 |
(so that the inductive case goes through):
|
|
|
2429 |
\begin{lemma}\label{fltsSizeReductionAlts}
|
|
|
2430 |
If we have three accumulator sets:
|
|
|
2431 |
$noalts\_set$, $alts\_set$ and $corr\_set$,
|
|
|
2432 |
satisfying:
|
|
|
2433 |
\begin{itemize}
|
|
|
2434 |
\item
|
|
|
2435 |
$\forall r \in noalts\_set. \; \nexists xs.\; r = \sum xs$
|
|
|
2436 |
\item
|
|
|
2437 |
$\forall r \in alts\_set. \; \exists xs. \; r = \sum xs
|
|
|
2438 |
\; \textit{and} \; set \; xs \subseteq corr\_set$
|
|
|
2439 |
\end{itemize}
|
|
|
2440 |
then we have that
|
|
|
2441 |
\begin{center}
|
|
|
2442 |
\begin{tabular}{lcl}
|
|
|
2443 |
$\llbracket (\textit{rdistinct} \; (\textit{rflts} \; as) \;
|
|
|
2444 |
(noalts\_set \cup corr\_set)) \rrbracket_r$ & $\leq$ &\\
|
|
|
2445 |
$\llbracket (\textit{rdistinct} \; as \; (noalts\_set \cup alts\_set \cup
|
|
639
|
2446 |
\{ \ZERO_r \} )) \rrbracket_r$ & & \\
|
|
609
|
2447 |
\end{tabular}
|
|
|
2448 |
\end{center}
|
|
|
2449 |
holds.
|
|
532
|
2450 |
\end{lemma}
|
|
558
|
2451 |
\noindent
|
|
618
|
2452 |
We split the accumulator into two parts: the part
|
|
609
|
2453 |
which contains alternative regular expressions ($alts\_set$), and
|
|
|
2454 |
the part without any of them($noalts\_set$).
|
|
618
|
2455 |
This is because $\rflts$ opens up the alternatives in $as$,
|
|
|
2456 |
causing the accumulators on both sides of the inequality
|
|
|
2457 |
to diverge slightly.
|
|
|
2458 |
If we want to compare the accumulators that are not
|
|
|
2459 |
perfectly in sync, we need to consider the alternatives and non-alternatives
|
|
|
2460 |
separately.
|
|
609
|
2461 |
The set $corr\_set$ is the corresponding set
|
|
618
|
2462 |
of $alts\_set$ with all elements under the alternative constructor
|
|
609
|
2463 |
spilled out.
|
|
|
2464 |
\begin{proof}
|
|
|
2465 |
By induction on the list $as$. We make use of lemma \ref{rdistinctConcat}.
|
|
|
2466 |
\end{proof}
|
|
|
2467 |
By setting all three sets to the empty set, one gets the desired size estimate:
|
|
|
2468 |
\begin{corollary}\label{interactionFltsDB}
|
|
|
2469 |
$\llbracket \rdistinct{(\rflts \; \textit{rs})}{\varnothing} \rrbracket_r
|
|
|
2470 |
\leq
|
|
|
2471 |
\llbracket \rdistinct{rs}{\varnothing} \rrbracket_r $.
|
|
|
2472 |
\end{corollary}
|
|
|
2473 |
\begin{proof}
|
|
|
2474 |
By using the lemma \ref{fltsSizeReductionAlts}.
|
|
|
2475 |
\end{proof}
|
|
|
2476 |
\noindent
|
|
618
|
2477 |
The intuition for why this is true
|
|
|
2478 |
is that if we remove duplicates from the $\textit{LHS}$, at least the same amount of
|
|
558
|
2479 |
duplicates will be removed from the list $\textit{rs}$ in the $\textit{RHS}$.
|
|
|
2480 |
|
|
|
2481 |
Now this $\rsimp{\sum rs}$ can be estimated using $\rdistinct{rs}{\varnothing}$:
|
|
|
2482 |
\begin{lemma}\label{altsSimpControl}
|
|
|
2483 |
$\rsize{\rsimp{\sum rs}} \leq \rsize{\rdistinct{rs}{\varnothing}}+ 1$
|
|
532
|
2484 |
\end{lemma}
|
|
558
|
2485 |
\begin{proof}
|
|
618
|
2486 |
By using corollary \ref{interactionFltsDB}.
|
|
558
|
2487 |
\end{proof}
|
|
|
2488 |
\noindent
|
|
609
|
2489 |
This is a key lemma in establishing the bounds on all the
|
|
|
2490 |
closed forms.
|
|
|
2491 |
With this we are now ready to control the sizes of
|
|
618
|
2492 |
$(r_1 \cdot r_2 )\backslash s$ and $r^* \backslash s$.
|
|
|
2493 |
\begin{theorem}\label{rBound}
|
|
593
|
2494 |
For any regex $r$, $\exists N_r. \forall s. \; \rsize{\rderssimp{r}{s}} \leq N_r$
|
|
558
|
2495 |
\end{theorem}
|
|
|
2496 |
\noindent
|
|
|
2497 |
\begin{proof}
|
|
593
|
2498 |
We prove this by induction on $r$. The base cases for $\RZERO$,
|
|
|
2499 |
$\RONE $ and $\RCHAR{c}$ are straightforward.
|
|
|
2500 |
In the sequence $r_1 \cdot r_2$ case,
|
|
|
2501 |
the inductive hypotheses state
|
|
|
2502 |
$\exists N_1. \forall s. \; \llbracket \rderssimp{r}{s} \rrbracket \leq N_1$ and
|
|
|
2503 |
$\exists N_2. \forall s. \; \llbracket \rderssimp{r_2}{s} \rrbracket \leq N_2$.
|
|
562
|
2504 |
|
|
593
|
2505 |
When the string $s$ is not empty, we can reason as follows
|
|
|
2506 |
%
|
|
|
2507 |
\begin{center}
|
|
|
2508 |
\begin{tabular}{lcll}
|
|
558
|
2509 |
& & $ \llbracket \rderssimp{r_1\cdot r_2 }{s} \rrbracket_r $\\
|
|
620
|
2510 |
& $ = $ & $\llbracket \rsimp{(\sum(r_1 \backslash_{rsimps} s \cdot r_2 \; \; :: \; \;
|
|
|
2511 |
\map \; (r_2\backslash_{rsimps} \_)\; (\vsuf{s}{r})))} \rrbracket_r $ & (1) \\
|
|
|
2512 |
& $\leq$ & $\llbracket \rdistinct{(r_1 \backslash_{rsimps} s \cdot r_2 \; \; :: \; \;
|
|
|
2513 |
\map \; (r_2\backslash_{rsimps} \_)\; (\vsuf{s}{r}))}{\varnothing} \rrbracket_r + 1$ & (2) \\
|
|
593
|
2514 |
& $\leq$ & $2 + N_1 + \rsize{r_2} + (N_2 * (card\;(\sizeNregex \; N_2)))$ & (3)\\
|
|
558
|
2515 |
\end{tabular}
|
|
|
2516 |
\end{center}
|
|
561
|
2517 |
\noindent
|
|
618
|
2518 |
(1) is by theorem \ref{seqClosedForm}.
|
|
561
|
2519 |
(2) is by \ref{altsSimpControl}.
|
|
|
2520 |
(3) is by \ref{finiteSizeNCorollary}.
|
|
562
|
2521 |
|
|
|
2522 |
|
|
|
2523 |
Combining the cases when $s = []$ and $s \neq []$, we get (4):
|
|
|
2524 |
\begin{center}
|
|
|
2525 |
\begin{tabular}{lcll}
|
|
|
2526 |
$\rsize{(r_1 \cdot r_2) \backslash_r s}$ & $\leq$ &
|
|
|
2527 |
$max \; (2 + N_1 +
|
|
|
2528 |
\llbracket r_2 \rrbracket_r +
|
|
|
2529 |
N_2 * (card\; (\sizeNregex \; N_2))) \; \rsize{r_1\cdot r_2}$ & (4)
|
|
|
2530 |
\end{tabular}
|
|
|
2531 |
\end{center}
|
|
558
|
2532 |
|
|
562
|
2533 |
We reason similarly for $\STAR$.
|
|
|
2534 |
The inductive hypothesis is
|
|
|
2535 |
$\exists N. \forall s. \; \llbracket \rderssimp{r}{s} \rrbracket \leq N$.
|
|
564
|
2536 |
Let $n_r = \llbracket r^* \rrbracket_r$.
|
|
562
|
2537 |
When $s = c :: cs$ is not empty,
|
|
|
2538 |
\begin{center}
|
|
593
|
2539 |
\begin{tabular}{lcll}
|
|
562
|
2540 |
& & $ \llbracket \rderssimp{r^* }{c::cs} \rrbracket_r $\\
|
|
620
|
2541 |
& $ = $ & $\llbracket \rsimp{(\sum (\map \; (\lambda s. (r \backslash_{rsimps} s) \cdot r^*) \; (\starupdates\;
|
|
593
|
2542 |
cs \; r \; [[c]] )) )} \rrbracket_r $ & (5) \\
|
|
|
2543 |
& $\leq$ & $\llbracket
|
|
|
2544 |
\rdistinct{
|
|
|
2545 |
(\map \;
|
|
620
|
2546 |
(\lambda s. (r \backslash_{rsimps} s) \cdot r^*) \;
|
|
593
|
2547 |
(\starupdates\; cs \; r \; [[c]] )
|
|
|
2548 |
)}
|
|
562
|
2549 |
{\varnothing} \rrbracket_r + 1$ & (6) \\
|
|
|
2550 |
& $\leq$ & $1 + (\textit{card} (\sizeNregex \; (N + n_r)))
|
|
|
2551 |
* (1 + (N + n_r)) $ & (7)\\
|
|
|
2552 |
\end{tabular}
|
|
|
2553 |
\end{center}
|
|
|
2554 |
\noindent
|
|
618
|
2555 |
(5) is by theorem \ref{starClosedForm}.
|
|
562
|
2556 |
(6) is by \ref{altsSimpControl}.
|
|
618
|
2557 |
(7) is by corollary \ref{finiteSizeNCorollary}.
|
|
639
|
2558 |
Combining with the case when $s = []$, one obtains
|
|
562
|
2559 |
\begin{center}
|
|
593
|
2560 |
\begin{tabular}{lcll}
|
|
|
2561 |
$\rsize{r^* \backslash_r s}$ & $\leq$ & $max \; n_r \; 1 + (\textit{card} (\sizeNregex \; (N + n_r)))
|
|
|
2562 |
* (1 + (N + n_r)) $ & (8)\\
|
|
|
2563 |
\end{tabular}
|
|
562
|
2564 |
\end{center}
|
|
|
2565 |
\noindent
|
|
|
2566 |
|
|
|
2567 |
The alternative case is slightly less involved.
|
|
|
2568 |
The inductive hypothesis
|
|
|
2569 |
is equivalent to $\exists N. \forall r \in (\map \; (\_ \backslash_r s) \; rs). \rsize{r} \leq N$.
|
|
|
2570 |
In the case when $s = c::cs$, we have
|
|
|
2571 |
\begin{center}
|
|
593
|
2572 |
\begin{tabular}{lcll}
|
|
562
|
2573 |
& & $ \llbracket \rderssimp{\sum rs }{c::cs} \rrbracket_r $\\
|
|
620
|
2574 |
& $ = $ & $\llbracket \rsimp{(\sum (\map \; (\_ \backslash_{rsimps} s) \; rs) )} \rrbracket_r $ & (9) \\
|
|
|
2575 |
& $\leq$ & $\llbracket (\sum (\map \; (\_ \backslash_{rsimps} s) \; rs) ) \rrbracket_r $ & (10) \\
|
|
562
|
2576 |
& $\leq$ & $1 + N * (length \; rs) $ & (11)\\
|
|
593
|
2577 |
\end{tabular}
|
|
562
|
2578 |
\end{center}
|
|
|
2579 |
\noindent
|
|
618
|
2580 |
(9) is by theorem \ref{altsClosedForm}, (10) by lemma \ref{rsimpMono} and (11) by inductive hypothesis.
|
|
562
|
2581 |
|
|
639
|
2582 |
Combining with the case when $s = []$, we obtain
|
|
562
|
2583 |
\begin{center}
|
|
593
|
2584 |
\begin{tabular}{lcll}
|
|
|
2585 |
$\rsize{\sum rs \backslash_r s}$ & $\leq$ & $max \; \rsize{\sum rs} \; 1+N*(length \; rs)$
|
|
|
2586 |
& (12)\\
|
|
|
2587 |
\end{tabular}
|
|
562
|
2588 |
\end{center}
|
|
618
|
2589 |
We have all the inductive cases proven.
|
|
558
|
2590 |
\end{proof}
|
|
|
2591 |
|
|
618
|
2592 |
This leads to our main result on the size bound:
|
|
564
|
2593 |
\begin{corollary}
|
|
618
|
2594 |
For any annotated regular expression $a$, $\exists N_r. \forall s. \; \rsize{\bderssimp{a}{s}} \leq N_r$
|
|
564
|
2595 |
\end{corollary}
|
|
|
2596 |
\begin{proof}
|
|
618
|
2597 |
By lemma \ref{sizeRelations} and theorem \ref{rBound}.
|
|
564
|
2598 |
\end{proof}
|
|
558
|
2599 |
\noindent
|
|
|
2600 |
|
|
609
|
2601 |
|
|
|
2602 |
|
|
|
2603 |
|
|
|
2604 |
|
|
558
|
2605 |
%-----------------------------------
|
|
|
2606 |
% SECTION 2
|
|
|
2607 |
%-----------------------------------
|
|
|
2608 |
|
|
625
|
2609 |
\section{Bounded Repetitions}
|
|
|
2610 |
We have promised in chapter \ref{Introduction}
|
|
|
2611 |
that our lexing algorithm can potentially be extended
|
|
|
2612 |
to handle bounded repetitions
|
|
|
2613 |
in natural and elegant ways.
|
|
|
2614 |
Now we fulfill our promise by adding support for
|
|
|
2615 |
the ``exactly-$n$-times'' bounded regular expression $r^{\{n\}}$.
|
|
|
2616 |
We add clauses in our derivatives-based lexing algorithms (with simplifications)
|
|
|
2617 |
introduced in chapter \ref{Bitcoded2}.
|
|
|
2618 |
|
|
|
2619 |
\subsection{Augmented Definitions}
|
|
|
2620 |
There are a number of definitions that need to be augmented.
|
|
|
2621 |
The most notable one would be the POSIX rules for $r^{\{n\}}$:
|
|
|
2622 |
\begin{center}
|
|
|
2623 |
\begin{mathpar}
|
|
|
2624 |
\inferrule{\forall v \in vs_1. \vdash v:r \land
|
|
|
2625 |
|v| \neq []\\ \forall v \in vs_2. \vdash v:r \land |v| = []\\
|
|
|
2626 |
\textit{length} \; (vs_1 @ vs_2) = n}{\textit{Stars} \;
|
|
|
2627 |
(vs_1 @ vs_2) : r^{\{n\}} }
|
|
|
2628 |
\end{mathpar}
|
|
|
2629 |
\end{center}
|
|
|
2630 |
As Ausaf had pointed out \cite{Ausaf},
|
|
|
2631 |
sometimes empty iterations have to be taken to get
|
|
|
2632 |
a match with exactly $n$ repetitions,
|
|
|
2633 |
and hence the $vs_2$ part.
|
|
|
2634 |
|
|
|
2635 |
Another important definition would be the size:
|
|
|
2636 |
\begin{center}
|
|
|
2637 |
\begin{tabular}{lcl}
|
|
|
2638 |
$\llbracket r^{\{n\}} \rrbracket_r$ & $\dn$ &
|
|
|
2639 |
$\llbracket r \rrbracket_r + n$\\
|
|
|
2640 |
\end{tabular}
|
|
|
2641 |
\end{center}
|
|
|
2642 |
\noindent
|
|
|
2643 |
Arguably we should use $\log \; n$ for the size because
|
|
|
2644 |
the number of digits increase logarithmically w.r.t $n$.
|
|
|
2645 |
For simplicity we choose to add the counter directly to the size.
|
|
|
2646 |
|
|
|
2647 |
The derivative w.r.t a bounded regular expression
|
|
|
2648 |
is given as
|
|
|
2649 |
\begin{center}
|
|
|
2650 |
\begin{tabular}{lcl}
|
|
|
2651 |
$r^{\{n\}} \backslash_r c$ & $\dn$ &
|
|
|
2652 |
$r\backslash_r c \cdot r^{\{n-1\}} \;\; \textit{if} \; n \geq 1$\\
|
|
|
2653 |
& & $\RZERO \;\quad \quad\quad \quad
|
|
|
2654 |
\textit{otherwise}$\\
|
|
|
2655 |
\end{tabular}
|
|
|
2656 |
\end{center}
|
|
|
2657 |
\noindent
|
|
|
2658 |
For brevity, we sometimes use NTIMES to refer to bounded
|
|
|
2659 |
regular expressions.
|
|
|
2660 |
The $\mkeps$ function clause for NTIMES would be
|
|
|
2661 |
\begin{center}
|
|
|
2662 |
\begin{tabular}{lcl}
|
|
|
2663 |
$\mkeps \; r^{\{n\}} $ & $\dn$ & $\Stars \;
|
|
|
2664 |
(\textit{replicate} \; n\; (\mkeps \; r))$
|
|
|
2665 |
\end{tabular}
|
|
|
2666 |
\end{center}
|
|
|
2667 |
\noindent
|
|
|
2668 |
The injection looks like
|
|
|
2669 |
\begin{center}
|
|
|
2670 |
\begin{tabular}{lcl}
|
|
|
2671 |
$\inj \; r^{\{n\}} \; c\; (\Seq \;v \; (\Stars \; vs)) $ &
|
|
|
2672 |
$\dn$ & $\Stars \;
|
|
|
2673 |
((\inj \; r \;c \;v ) :: vs)$
|
|
|
2674 |
\end{tabular}
|
|
|
2675 |
\end{center}
|
|
|
2676 |
\noindent
|
|
|
2677 |
|
|
|
2678 |
|
|
|
2679 |
\subsection{Proofs for the Augmented Lexing Algorithm}
|
|
|
2680 |
We need to maintain two proofs with the additional $r^{\{n\}}$
|
|
|
2681 |
construct: the
|
|
|
2682 |
correctness proof in chapter \ref{Bitcoded2},
|
|
|
2683 |
and the finiteness proof in chapter \ref{Finite}.
|
|
|
2684 |
|
|
|
2685 |
\subsubsection{Correctness Proof Augmentation}
|
|
|
2686 |
The correctness of $\textit{lexer}$ and $\textit{blexer}$ with bounded repetitions
|
|
|
2687 |
have been proven by Ausaf and Urban\cite{AusafDyckhoffUrban2016}.
|
|
|
2688 |
As they have commented, once the definitions are in place,
|
|
|
2689 |
the proofs given for the basic regular expressions will extend to
|
|
|
2690 |
bounded regular expressions, and there are no ``surprises''.
|
|
|
2691 |
We confirm this point because the correctness theorem would also
|
|
|
2692 |
extend without surprise to $\blexersimp$.
|
|
|
2693 |
The rewrite rules such as $\rightsquigarrow$, $\stackrel{s}{\rightsquigarrow}$ and so on
|
|
|
2694 |
do not need to be changed,
|
|
|
2695 |
and only a few lemmas such as lemma \ref{fltsPreserves} need to be adjusted to
|
|
|
2696 |
add one more line which can be solved by sledgehammer
|
|
|
2697 |
to solve the $r^{\{n\}}$ inductive case.
|
|
|
2698 |
|
|
|
2699 |
|
|
|
2700 |
\subsubsection{Finiteness Proof Augmentation}
|
|
|
2701 |
The bounded repetitions are
|
|
|
2702 |
very similar to stars, and therefore the treatment
|
|
|
2703 |
is similar, with minor changes to handle some slight complications
|
|
|
2704 |
when the counter reaches 0.
|
|
|
2705 |
The exponential growth is similar:
|
|
|
2706 |
\begin{center}
|
|
|
2707 |
\begin{tabular}{ll}
|
|
|
2708 |
$r^{\{n\}} $ & $\longrightarrow_{\backslash c}$\\
|
|
|
2709 |
$(r\backslash c) \cdot
|
|
|
2710 |
r^{\{n - 1\}}*$ & $\longrightarrow_{\backslash c'}$\\
|
|
|
2711 |
\\
|
|
|
2712 |
$r \backslash cc' \cdot r^{\{n - 2\}}* +
|
|
|
2713 |
r \backslash c' \cdot r^{\{n - 1\}}*$ &
|
|
|
2714 |
$\longrightarrow_{\backslash c''}$\\
|
|
|
2715 |
\\
|
|
|
2716 |
$(r_1 \backslash cc'c'' \cdot r^{\{n-3\}}* +
|
|
|
2717 |
r \backslash c''\cdot r^{\{n-1\}}) +
|
|
|
2718 |
(r \backslash c'c'' \cdot r^{\{n-2\}}* +
|
|
|
2719 |
r \backslash c'' \cdot r^{\{n-1\}}*)$ &
|
|
|
2720 |
$\longrightarrow_{\backslash c'''}$ \\
|
|
|
2721 |
\\
|
|
|
2722 |
$\ldots$\\
|
|
|
2723 |
\end{tabular}
|
|
|
2724 |
\end{center}
|
|
|
2725 |
Again, we assume that $r\backslash c$, $r \backslash cc'$ and so on
|
|
|
2726 |
are all nullable.
|
|
|
2727 |
The flattened list of terms for $r^{\{n\}} \backslash_{rs} s$
|
|
|
2728 |
\begin{center}
|
|
|
2729 |
$[r_1 \backslash cc'c'' \cdot r^{\{n-3\}}*,\;
|
|
|
2730 |
r \backslash c''\cdot r^{\{n-1\}}, \;
|
|
|
2731 |
r \backslash c'c'' \cdot r^{\{n-2\}}*, \;
|
|
|
2732 |
r \backslash c'' \cdot r^{\{n-1\}}*,\; \ldots ]$
|
|
|
2733 |
\end{center}
|
|
|
2734 |
that comes from
|
|
|
2735 |
\begin{center}
|
|
|
2736 |
$(r_1 \backslash cc'c'' \cdot r^{\{n-3\}}* +
|
|
|
2737 |
r \backslash c''\cdot r^{\{n-1\}}) +
|
|
|
2738 |
(r \backslash c'c'' \cdot r^{\{n-2\}}* +
|
|
|
2739 |
r \backslash c'' \cdot r^{\{n-1\}}*)+ \ldots$
|
|
|
2740 |
\end{center}
|
|
|
2741 |
are made of sequences with different tails, where the counters
|
|
|
2742 |
might differ.
|
|
|
2743 |
The observation for maintaining the bound is that
|
|
|
2744 |
these counters never exceed $n$, the original
|
|
|
2745 |
counter. With the number of counters staying finite,
|
|
|
2746 |
$\rDistinct$ will deduplicate and keep the list finite.
|
|
|
2747 |
We introduce this idea as a lemma once we describe all
|
|
|
2748 |
the necessary helper functions.
|
|
|
2749 |
|
|
|
2750 |
Similar to the star case, we want
|
|
|
2751 |
\begin{center}
|
|
|
2752 |
$\rderssimp{r^{\{n\}}}{s} = \rsimp{\sum rs}$.
|
|
|
2753 |
\end{center}
|
|
|
2754 |
where $rs$
|
|
|
2755 |
shall be in the form of
|
|
|
2756 |
$\map \; f \; Ss$, where $f$ is a function and
|
|
|
2757 |
$Ss$ a list of objects to act on.
|
|
|
2758 |
For star, the object's datatype is string.
|
|
|
2759 |
The list of strings $Ss$
|
|
|
2760 |
is generated using functions
|
|
|
2761 |
$\starupdate$ and $\starupdates$.
|
|
|
2762 |
The function that takes a string and returns a regular expression
|
|
|
2763 |
is the anonymous function $
|
|
|
2764 |
(\lambda s'. \; r\backslash s' \cdot r^{\{m\}})$.
|
|
|
2765 |
In the NTIMES setting,
|
|
|
2766 |
the $\starupdate$ and $\starupdates$ functions are replaced by
|
|
|
2767 |
$\textit{nupdate}$ and $\textit{nupdates}$:
|
|
|
2768 |
\begin{center}
|
|
|
2769 |
\begin{tabular}{lcl}
|
|
|
2770 |
$\nupdate \; c \; r \; [] $ & $\dn$ & $[]$\\
|
|
|
2771 |
$\nupdate \; c \; r \;
|
|
|
2772 |
(\Some \; (s, \; n + 1) \; :: \; Ss)$ & $\dn$ & %\\
|
|
|
2773 |
$\textit{if} \;
|
|
|
2774 |
(\rnullable \; (r \backslash_{rs} s))$ \\
|
|
|
2775 |
& & $\;\;\textit{then}
|
|
|
2776 |
\;\; \Some \; (s @ [c], n + 1) :: \Some \; ([c], n) :: (
|
|
|
2777 |
\nupdate \; c \; r \; Ss)$ \\
|
|
|
2778 |
& & $\textit{else} \;\; \Some \; (s @ [c], n+1) :: (
|
|
|
2779 |
\nupdate \; c \; r \; Ss)$\\
|
|
|
2780 |
$\nupdate \; c \; r \; (\textit{None} :: Ss)$ & $\dn$ &
|
|
|
2781 |
$(\None :: \nupdate \; c \; r \; Ss)$\\
|
|
|
2782 |
& & \\
|
|
|
2783 |
%\end{tabular}
|
|
|
2784 |
%\end{center}
|
|
|
2785 |
%\begin{center}
|
|
|
2786 |
%\begin{tabular}{lcl}
|
|
|
2787 |
$\nupdates \; [] \; r \; Ss$ & $\dn$ & $Ss$\\
|
|
|
2788 |
$\nupdates \; (c :: cs) \; r \; Ss$ & $\dn$ & $\nupdates \; cs \; r \; (
|
|
|
2789 |
\nupdate \; c \; r \; Ss)$
|
|
|
2790 |
\end{tabular}
|
|
|
2791 |
\end{center}
|
|
|
2792 |
\noindent
|
|
|
2793 |
which take into account when a subterm
|
|
|
2794 |
\begin{center}
|
|
|
2795 |
$r \backslash_s s \cdot r^{\{n\}}$
|
|
|
2796 |
\end{center}
|
|
|
2797 |
counter $n$
|
|
|
2798 |
is 0, and therefore expands to
|
|
|
2799 |
\begin{center}
|
|
|
2800 |
$r \backslash_s (s@[c]) \cdot r^{\{n\}} \;+
|
|
|
2801 |
\; \ZERO$
|
|
|
2802 |
\end{center}
|
|
|
2803 |
after taking a derivative.
|
|
|
2804 |
The object now has type
|
|
|
2805 |
\begin{center}
|
|
|
2806 |
$\textit{option} \;(\textit{string}, \textit{nat})$
|
|
|
2807 |
\end{center}
|
|
|
2808 |
and therefore the function for converting such an option into
|
|
|
2809 |
a regular expression term is called $\opterm$:
|
|
|
2810 |
|
|
|
2811 |
\begin{center}
|
|
|
2812 |
\begin{tabular}{lcl}
|
|
|
2813 |
$\opterm \; r \; SN$ & $\dn$ & $\textit{case} \; SN\; of$\\
|
|
|
2814 |
& & $\;\;\Some \; (s, n) \Rightarrow
|
|
|
2815 |
(r\backslash_{rs} s)\cdot r^{\{n\}}$\\
|
|
|
2816 |
& & $\;\;\None \Rightarrow
|
|
|
2817 |
\ZERO$\\
|
|
|
2818 |
\end{tabular}
|
|
|
2819 |
\end{center}
|
|
|
2820 |
\noindent
|
|
|
2821 |
Put together, the list $\map \; f \; Ss$ is instantiated as
|
|
|
2822 |
\begin{center}
|
|
|
2823 |
$\map \; (\opterm \; r) \; (\nupdates \; s \; r \;
|
|
|
2824 |
[\Some \; ([c], n)])$.
|
|
|
2825 |
\end{center}
|
|
|
2826 |
For the closed form to be bounded, we would like
|
|
|
2827 |
simplification to be applied to each term in the list.
|
|
|
2828 |
Therefore we introduce some variants of $\opterm$,
|
|
|
2829 |
which help conveniently express the rewriting steps
|
|
|
2830 |
needed in the closed form proof.
|
|
639
|
2831 |
We have $\optermOsimp$, $\optermosimp$ and $\optermsimp$
|
|
|
2832 |
with slightly different spellings because they help the proof to go through:
|
|
625
|
2833 |
\begin{center}
|
|
|
2834 |
\begin{tabular}{lcl}
|
|
|
2835 |
$\optermOsimp \; r \; SN$ & $\dn$ & $\textit{case} \; SN\; of$\\
|
|
|
2836 |
& & $\;\;\Some \; (s, n) \Rightarrow
|
|
|
2837 |
\textit{rsimp} \; ((r\backslash_{rs} s)\cdot r^{\{n\}})$\\
|
|
|
2838 |
& & $\;\;\None \Rightarrow
|
|
|
2839 |
\ZERO$\\
|
|
|
2840 |
\\
|
|
|
2841 |
$\optermosimp \; r \; SN$ & $\dn$ & $\textit{case} \; SN\; of$\\
|
|
|
2842 |
& & $\;\;\Some \; (s, n) \Rightarrow
|
|
|
2843 |
(\textit{rsimp} \; (r\backslash_{rs} s))
|
|
|
2844 |
\cdot r^{\{n\}}$\\
|
|
|
2845 |
& & $\;\;\None \Rightarrow
|
|
|
2846 |
\ZERO$\\
|
|
|
2847 |
\\
|
|
|
2848 |
$\optermsimp \; r \; SN$ & $\dn$ & $\textit{case} \; SN\; of$\\
|
|
|
2849 |
& & $\;\;\Some \; (s, n) \Rightarrow
|
|
|
2850 |
(r\backslash_{rsimps} s)\cdot r^{\{n\}}$\\
|
|
|
2851 |
& & $\;\;\None \Rightarrow
|
|
|
2852 |
\ZERO$\\
|
|
|
2853 |
\end{tabular}
|
|
|
2854 |
\end{center}
|
|
|
2855 |
|
|
|
2856 |
|
|
|
2857 |
For a list of
|
|
|
2858 |
$\textit{option} \;(\textit{string}, \textit{nat})$ elements,
|
|
|
2859 |
we define the highest power for it recursively:
|
|
|
2860 |
\begin{center}
|
|
|
2861 |
\begin{tabular}{lcl}
|
|
|
2862 |
$\hpa \; [] \; n $ & $\dn$ & $n$\\
|
|
|
2863 |
$\hpa \; (\None :: os) \; n $ & $\dn$ & $\hpa \; os \; n$\\
|
|
|
2864 |
$\hpa \; (\Some \; (s, n) :: os) \; m$ & $\dn$ &
|
|
|
2865 |
$\hpa \;os \; (\textit{max} \; n\; m)$\\
|
|
|
2866 |
\\
|
|
|
2867 |
$\hpower \; rs $ & $\dn$ & $\hpa \; rs \; 0$\\
|
|
|
2868 |
\end{tabular}
|
|
|
2869 |
\end{center}
|
|
|
2870 |
|
|
|
2871 |
Now the intuition that an NTIMES regular expression's power
|
|
|
2872 |
does not increase can be easily expressed as
|
|
|
2873 |
\begin{lemma}\label{nupdatesMono2}
|
|
|
2874 |
$\hpower \; (\nupdates \;s \; r \; [\Some \; ([c], n)]) \leq n$
|
|
|
2875 |
\end{lemma}
|
|
|
2876 |
\begin{proof}
|
|
|
2877 |
Note that the power is non-increasing after a $\nupdate$ application:
|
|
|
2878 |
\begin{center}
|
|
|
2879 |
$\hpa \;\; (\nupdate \; c \; r \; Ss)\;\; m \leq
|
|
|
2880 |
\hpa\; \; Ss \; m$.
|
|
|
2881 |
\end{center}
|
|
|
2882 |
This is also the case for $\nupdates$:
|
|
|
2883 |
\begin{center}
|
|
|
2884 |
$\hpa \;\; (\nupdates \; s \; r \; Ss)\;\; m \leq
|
|
|
2885 |
\hpa\; \; Ss \; m$.
|
|
|
2886 |
\end{center}
|
|
|
2887 |
Therefore we have that
|
|
|
2888 |
\begin{center}
|
|
|
2889 |
$\hpower \;\; (\nupdates \; s \; r \; Ss) \leq
|
|
|
2890 |
\hpower \;\; Ss$
|
|
|
2891 |
\end{center}
|
|
|
2892 |
which leads to the lemma being proven.
|
|
|
2893 |
|
|
|
2894 |
\end{proof}
|
|
|
2895 |
|
|
|
2896 |
|
|
|
2897 |
We also define the inductive rules for
|
|
|
2898 |
the shape of derivatives of the NTIMES regular expressions:\\[-3em]
|
|
|
2899 |
\begin{center}
|
|
|
2900 |
\begin{mathpar}
|
|
|
2901 |
\inferrule{\mbox{}}{\cbn \;\ZERO}
|
|
|
2902 |
|
|
|
2903 |
\inferrule{\mbox{}}{\cbn \; \; r_a \cdot (r^{\{n\}})}
|
|
|
2904 |
|
|
|
2905 |
\inferrule{\cbn \; r_1 \;\; \; \cbn \; r_2}{\cbn \; r_1 + r_2}
|
|
|
2906 |
|
|
|
2907 |
\inferrule{\cbn \; r}{\cbn \; r + \ZERO}
|
|
|
2908 |
\end{mathpar}
|
|
|
2909 |
\end{center}
|
|
|
2910 |
\noindent
|
|
|
2911 |
A derivative of NTIMES fits into the shape described by $\cbn$:
|
|
|
2912 |
\begin{lemma}\label{ntimesDersCbn}
|
|
|
2913 |
$\cbn \; ((r' \cdot r^{\{n\}}) \backslash_{rs} s)$ holds.
|
|
|
2914 |
\end{lemma}
|
|
|
2915 |
\begin{proof}
|
|
|
2916 |
By a reverse induction on $s$.
|
|
|
2917 |
For the inductive case, note that if $\cbn \; r$ holds,
|
|
|
2918 |
then $\cbn \; (r\backslash_r c)$ holds.
|
|
|
2919 |
\end{proof}
|
|
|
2920 |
\noindent
|
|
|
2921 |
In addition, for $\cbn$-shaped regular expressioins, one can flatten
|
|
|
2922 |
them:
|
|
|
2923 |
\begin{lemma}\label{ntimesHfauPushin}
|
|
|
2924 |
If $\cbn \; r$ holds, then $\hflataux{r \backslash_r c} =
|
|
|
2925 |
\textit{concat} \; (\map \; \hflataux{\map \; (\_\backslash_r c) \;
|
|
|
2926 |
(\hflataux{r})})$
|
|
|
2927 |
\end{lemma}
|
|
|
2928 |
\begin{proof}
|
|
|
2929 |
By an induction on the inductive cases of $\cbn$.
|
|
|
2930 |
\end{proof}
|
|
|
2931 |
\noindent
|
|
|
2932 |
This time we do not need to define the flattening functions for NTIMES only,
|
|
|
2933 |
because $\hflat{\_}$ and $\hflataux{\_}$ work on NTIMES already.
|
|
|
2934 |
\begin{lemma}\label{ntimesHfauInduct}
|
|
|
2935 |
$\hflataux{( (r\backslash_r c) \cdot r^{\{n\}}) \backslash_{rsimps} s} =
|
|
|
2936 |
\map \; (\opterm \; r) \; (\nupdates \; s \; r \; [\Some \; ([c], n)])$
|
|
|
2937 |
\end{lemma}
|
|
|
2938 |
\begin{proof}
|
|
|
2939 |
By a reverse induction on $s$.
|
|
|
2940 |
The lemmas \ref{ntimesHfauPushin} and \ref{ntimesDersCbn} are used.
|
|
|
2941 |
\end{proof}
|
|
|
2942 |
\noindent
|
|
|
2943 |
We have a recursive property for NTIMES with $\nupdate$
|
|
|
2944 |
similar to that for STAR,
|
|
|
2945 |
and one for $\nupdates $ as well:
|
|
|
2946 |
\begin{lemma}\label{nupdateInduct1}
|
|
|
2947 |
\mbox{}
|
|
|
2948 |
\begin{itemize}
|
|
|
2949 |
\item
|
|
|
2950 |
\begin{center}
|
|
|
2951 |
$\textit{concat} \; (\map \; (\hflataux{\_} \circ (
|
|
|
2952 |
\opterm \; r)) \; Ss) = \map \; (\opterm \; r) \; (\nupdate \;
|
|
|
2953 |
c \; r \; Ss)$\\
|
|
|
2954 |
\end{center}
|
|
|
2955 |
holds.
|
|
|
2956 |
\item
|
|
|
2957 |
\begin{center}
|
|
|
2958 |
$\textit{concat} \; (\map \; \hflataux{\_}\;
|
|
|
2959 |
\map \; (\_\backslash_r x) \;
|
|
|
2960 |
(\map \; (\opterm \; r) \; (\nupdates \; xs \; r \; Ss)))$\\
|
|
|
2961 |
$=$\\
|
|
|
2962 |
$\map \; (\opterm \; r) \; (\nupdates \;(xs@[x]) \; r\;Ss)$
|
|
|
2963 |
\end{center}
|
|
|
2964 |
holds.
|
|
|
2965 |
\end{itemize}
|
|
|
2966 |
\end{lemma}
|
|
|
2967 |
\begin{proof}
|
|
|
2968 |
(i) is by an induction on $Ss$.
|
|
|
2969 |
(ii) is by an induction on $xs$.
|
|
|
2970 |
\end{proof}
|
|
|
2971 |
\noindent
|
|
|
2972 |
The $\nString$ predicate is defined for conveniently
|
|
|
2973 |
expressing that there are no empty strings in the
|
|
|
2974 |
$\Some \;(s, n)$ elements generated by $\nupdate$:
|
|
|
2975 |
\begin{center}
|
|
|
2976 |
\begin{tabular}{lcl}
|
|
|
2977 |
$\nString \; \None$ & $\dn$ & $ \textit{true}$\\
|
|
|
2978 |
$\nString \; (\Some \; ([], n))$ & $\dn$ & $ \textit{false}$\\
|
|
|
2979 |
$\nString \; (\Some \; (c::s, n))$ & $\dn$ & $ \textit{true}$\\
|
|
|
2980 |
\end{tabular}
|
|
|
2981 |
\end{center}
|
|
|
2982 |
\begin{lemma}\label{nupdatesNonempty}
|
|
|
2983 |
If for all elements $o \in \textit{set} \; Ss$,
|
|
|
2984 |
$\nString \; o$ holds, the we have that
|
|
|
2985 |
for all elements $o' \in \textit{set} \; (\nupdates \; s \; r \; Ss)$,
|
|
|
2986 |
$\nString \; o'$ holds.
|
|
|
2987 |
\end{lemma}
|
|
|
2988 |
\begin{proof}
|
|
|
2989 |
By an induction on $s$, where $Ss$ is set to vary over all possible values.
|
|
|
2990 |
\end{proof}
|
|
|
2991 |
|
|
|
2992 |
\noindent
|
|
|
2993 |
|
|
|
2994 |
\begin{lemma}\label{ntimesClosedFormsSteps}
|
|
|
2995 |
The following list of equalities or rewriting relations hold:\\
|
|
|
2996 |
(i) $r^{\{n+1\}} \backslash_{rsimps} (c::s) =
|
|
|
2997 |
\textit{rsimp} \; (\sum (\map \; (\opterm \;r \;\_) \; (\nupdates \;
|
|
|
2998 |
s \; r \; [\Some \; ([c], n)])))$\\
|
|
|
2999 |
(ii)
|
|
|
3000 |
\begin{center}
|
|
|
3001 |
$\sum (\map \; (\opterm \; r) \; (\nupdates \; s \; r \; [
|
|
|
3002 |
\Some \; ([c], n)]))$ \\ $ \sequal$\\
|
|
|
3003 |
$\sum (\map \; (\textit{rsimp} \circ (\opterm \; r))\; (\nupdates \;
|
|
|
3004 |
s\;r \; [\Some \; ([c], n)]))$\\
|
|
|
3005 |
\end{center}
|
|
|
3006 |
(iii)
|
|
|
3007 |
\begin{center}
|
|
|
3008 |
$\sum \;(\map \; (\optermosimp \; r) \; (\nupdates \; s \; r\; [\Some \;
|
|
|
3009 |
([c], n)]))$\\
|
|
|
3010 |
$\sequal$\\
|
|
|
3011 |
$\sum \;(\map \; (\optermsimp r) \; (\nupdates \; s \; r \; [\Some \;
|
|
|
3012 |
([c], n)])) $\\
|
|
|
3013 |
\end{center}
|
|
|
3014 |
(iv)
|
|
|
3015 |
\begin{center}
|
|
|
3016 |
$\sum \;(\map \; (\optermosimp \; r) \; (\nupdates \; s \; r\; [\Some \;
|
|
|
3017 |
([c], n)])) $ \\ $\sequal$\\
|
|
|
3018 |
$\sum \;(\map \; (\optermOsimp r) \; (\nupdates \; s \; r \; [\Some \;
|
|
|
3019 |
([c], n)])) $\\
|
|
|
3020 |
\end{center}
|
|
|
3021 |
(v)
|
|
|
3022 |
\begin{center}
|
|
|
3023 |
$\sum \;(\map \; (\optermOsimp r) \; (\nupdates \; s \; r \; [\Some \;
|
|
|
3024 |
([c], n)])) $ \\ $\sequal$\\
|
|
|
3025 |
$\sum \; (\map \; (\textit{rsimp} \circ (\opterm \; r)) \;
|
|
|
3026 |
(\nupdates \; s \; r \; [\Some \; ([c], n)]))$
|
|
|
3027 |
\end{center}
|
|
|
3028 |
\end{lemma}
|
|
|
3029 |
\begin{proof}
|
|
|
3030 |
Routine.
|
|
|
3031 |
(iii) and (iv) make use of the fact that all the strings $s$
|
|
|
3032 |
inside $\Some \; (s, m)$ which are elements of the list
|
|
|
3033 |
$\nupdates \; s\;r\;[\Some\; ([c], n)]$ are non-empty,
|
|
|
3034 |
which is from lemma \ref{nupdatesNonempty}.
|
|
|
3035 |
Once the string in $o = \Some \; (s, n)$ is
|
|
|
3036 |
nonempty, $\optermsimp \; r \;o$,
|
|
|
3037 |
$\optermosimp \; r \; o$ and $\optermosimp \; \; o$ are guaranteed
|
|
|
3038 |
to be equal.
|
|
|
3039 |
(v) uses \ref{nupdateInduct1}.
|
|
|
3040 |
\end{proof}
|
|
|
3041 |
\noindent
|
|
|
3042 |
Now we are ready to present the closed form for NTIMES:
|
|
|
3043 |
\begin{theorem}\label{ntimesClosedForm}
|
|
|
3044 |
The derivative of $r^{\{n+1\}}$ can be described as an alternative
|
|
|
3045 |
containing a list
|
|
|
3046 |
of terms:\\
|
|
|
3047 |
$r^{\{n+1\}} \backslash_{rsimps} (c::s) = \textit{rsimp} \; (
|
|
|
3048 |
\sum (\map \; (\optermsimp \; r) \; (\nupdates \; s \; r \;
|
|
|
3049 |
[\Some \; ([c], n)])))$
|
|
|
3050 |
\end{theorem}
|
|
|
3051 |
\begin{proof}
|
|
|
3052 |
By the rewriting steps described in lemma \ref{ntimesClosedFormsSteps}.
|
|
|
3053 |
\end{proof}
|
|
|
3054 |
\noindent
|
|
|
3055 |
The key observation for bounding this closed form
|
|
|
3056 |
is that the counter on $r^{\{n\}}$ will
|
|
|
3057 |
only decrement during derivatives:
|
|
|
3058 |
\begin{lemma}\label{nupdatesNLeqN}
|
|
|
3059 |
For an element $o$ in $\textit{set} \; (\nupdates \; s \; r \;
|
|
|
3060 |
[\Some \; ([c], n)])$, either $o = \None$, or $o = \Some
|
|
|
3061 |
\; (s', m)$ for some string $s'$ and number $m \leq n$.
|
|
|
3062 |
\end{lemma}
|
|
|
3063 |
\noindent
|
|
|
3064 |
The proof is routine and therefore omitted.
|
|
|
3065 |
This allows us to say what kind of terms
|
|
|
3066 |
are in the list $\textit{set} \; (\map \; (\optermsimp \; r) \; (
|
|
|
3067 |
\nupdates \; s \; r \; [\Some \; ([c], n)]))$:
|
|
|
3068 |
only $\ZERO_r$s or a sequence with the tail an $r^{\{m\}}$
|
|
|
3069 |
with a small $m$:
|
|
|
3070 |
\begin{lemma}\label{ntimesClosedFormListElemShape}
|
|
|
3071 |
For any element $r'$ in $\textit{set} \; (\map \; (\optermsimp \; r) \; (
|
|
|
3072 |
\nupdates \; s \; r \; [\Some \; ([c], n)]))$,
|
|
|
3073 |
we have that $r'$ is either $\ZERO$ or $r \backslash_{rsimps} s' \cdot
|
|
|
3074 |
r^{\{m\}}$ for some string $s'$ and number $m \leq n$.
|
|
|
3075 |
\end{lemma}
|
|
|
3076 |
\begin{proof}
|
|
|
3077 |
Using lemma \ref{nupdatesNLeqN}.
|
|
|
3078 |
\end{proof}
|
|
|
3079 |
|
|
|
3080 |
\begin{theorem}\label{ntimesClosedFormBounded}
|
|
|
3081 |
Assuming that for any string $s$, $\llbracket r \backslash_{rsimps} s
|
|
|
3082 |
\rrbracket_r \leq N$ holds, then we have that\\
|
|
|
3083 |
$\llbracket r^{\{n+1\}} \backslash_{rsimps} s \rrbracket_r \leq
|
|
|
3084 |
\textit{max} \; (c_N+1)* (N + \llbracket r^{\{n\}} \rrbracket+1)$,
|
|
|
3085 |
where $c_N = \textit{card} \; (\textit{sizeNregex} \; (
|
|
|
3086 |
N + \llbracket r^{\{n\}} \rrbracket_r+1))$.
|
|
|
3087 |
\end{theorem}
|
|
|
3088 |
\begin{proof}
|
|
639
|
3089 |
We have that for all regular expressions $r'$ in
|
|
|
3090 |
\begin{center}
|
|
|
3091 |
$\textit{set} \; (\map \; (\optermsimp \; r) \; (
|
|
625
|
3092 |
\nupdates \; s \; r \; [\Some \; ([c], n)]))$,
|
|
639
|
3093 |
\end{center}
|
|
625
|
3094 |
$r'$'s size is less than or equal to $N + \llbracket r^{\{n\}}
|
|
|
3095 |
\rrbracket_r + 1$
|
|
|
3096 |
because $r'$ can only be either a $\ZERO$ or $r \backslash_{rsimps} s' \cdot
|
|
|
3097 |
r^{\{m\}}$ for some string $s'$ and number
|
|
|
3098 |
$m \leq n$ (lemma \ref{ntimesClosedFormListElemShape}).
|
|
|
3099 |
In addition, we know that the list
|
|
|
3100 |
$\map \; (\optermsimp \; r) \; (
|
|
|
3101 |
\nupdates \; s \; r \; [\Some \; ([c], n)])$'s size is at most
|
|
|
3102 |
$c_N = \textit{card} \;
|
|
|
3103 |
(\sizeNregex \; ((N + \llbracket r^{\{n\}} \rrbracket) + 1))$.
|
|
|
3104 |
This gives us $\llbracket r \backslash_{rsimps} \;s \rrbracket_r
|
|
|
3105 |
\leq N * c_N$.
|
|
|
3106 |
\end{proof}
|
|
|
3107 |
|
|
|
3108 |
We aim to formalise the correctness and size bound
|
|
|
3109 |
for constructs like $r^{\{\ldots n\}}$, $r^{\{n \ldots\}}$
|
|
|
3110 |
and so on, which is still work in progress.
|
|
|
3111 |
They should more or less follow the same recipe described in this section.
|
|
|
3112 |
Once we know about how to deal with them recursively using suitable auxiliary
|
|
|
3113 |
definitions, we are able to routinely establish the proofs.
|
|
|
3114 |
|
|
532
|
3115 |
|
|
557
|
3116 |
%----------------------------------------------------------------------------------------
|
|
|
3117 |
% SECTION 3
|
|
|
3118 |
%----------------------------------------------------------------------------------------
|
|
|
3119 |
|
|
532
|
3120 |
|
|
618
|
3121 |
\section{Comments and Future Improvements}
|
|
|
3122 |
\subsection{Some Experimental Results}
|
|
532
|
3123 |
What guarantee does this bound give us?
|
|
639
|
3124 |
It states that whatever the regex is, it will not grow indefinitely.
|
|
532
|
3125 |
Take our previous example $(a + aa)^*$ as an example:
|
|
|
3126 |
\begin{center}
|
|
593
|
3127 |
\begin{tabular}{@{}c@{\hspace{0mm}}c@{\hspace{0mm}}c@{}}
|
|
|
3128 |
\begin{tikzpicture}
|
|
|
3129 |
\begin{axis}[
|
|
|
3130 |
xlabel={number of $a$'s},
|
|
|
3131 |
x label style={at={(1.05,-0.05)}},
|
|
|
3132 |
ylabel={regex size},
|
|
|
3133 |
enlargelimits=false,
|
|
|
3134 |
xtick={0,5,...,30},
|
|
|
3135 |
xmax=33,
|
|
|
3136 |
ymax= 40,
|
|
|
3137 |
ytick={0,10,...,40},
|
|
|
3138 |
scaled ticks=false,
|
|
|
3139 |
axis lines=left,
|
|
|
3140 |
width=5cm,
|
|
|
3141 |
height=4cm,
|
|
|
3142 |
legend entries={$(a + aa)^*$},
|
|
618
|
3143 |
legend pos=south east,
|
|
593
|
3144 |
legend cell align=left]
|
|
|
3145 |
\addplot[red,mark=*, mark options={fill=white}] table {a_aa_star.data};
|
|
|
3146 |
\end{axis}
|
|
|
3147 |
\end{tikzpicture}
|
|
|
3148 |
\end{tabular}
|
|
532
|
3149 |
\end{center}
|
|
|
3150 |
We are able to limit the size of the regex $(a + aa)^*$'s derivatives
|
|
593
|
3151 |
with our simplification
|
|
532
|
3152 |
rules very effectively.
|
|
|
3153 |
|
|
|
3154 |
|
|
|
3155 |
In our proof for the inductive case $r_1 \cdot r_2$, the dominant term in the bound
|
|
|
3156 |
is $l_{N_2} * N_2$, where $N_2$ is the bound we have for $\llbracket \bderssimp{r_2}{s} \rrbracket$.
|
|
|
3157 |
Given that $l_{N_2}$ is roughly the size $4^{N_2}$, the size bound $\llbracket \bderssimp{r_1 \cdot r_2}{s} \rrbracket$
|
|
|
3158 |
inflates the size bound of $\llbracket \bderssimp{r_2}{s} \rrbracket$ with the function
|
|
|
3159 |
$f(x) = x * 2^x$.
|
|
|
3160 |
This means the bound we have will surge up at least
|
|
|
3161 |
tower-exponentially with a linear increase of the depth.
|
|
|
3162 |
|
|
618
|
3163 |
One might be quite skeptical about what this non-elementary
|
|
|
3164 |
bound can bring us.
|
|
|
3165 |
It turns out that the giant bounds are far from being hit.
|
|
|
3166 |
Here we have some test data from randomly generated regular expressions:
|
|
|
3167 |
\begin{figure}[H]
|
|
|
3168 |
\begin{tabular}{@{}c@{\hspace{2mm}}c@{\hspace{0mm}}c@{}}
|
|
593
|
3169 |
\begin{tikzpicture}
|
|
|
3170 |
\begin{axis}[
|
|
618
|
3171 |
xlabel={$n$},
|
|
593
|
3172 |
x label style={at={(1.05,-0.05)}},
|
|
|
3173 |
ylabel={regex size},
|
|
|
3174 |
enlargelimits=false,
|
|
|
3175 |
xtick={0,5,...,30},
|
|
|
3176 |
xmax=33,
|
|
611
|
3177 |
%ymax=1000,
|
|
|
3178 |
%ytick={0,100,...,1000},
|
|
593
|
3179 |
scaled ticks=false,
|
|
|
3180 |
axis lines=left,
|
|
618
|
3181 |
width=4.75cm,
|
|
|
3182 |
height=3.8cm,
|
|
593
|
3183 |
legend entries={regex1},
|
|
618
|
3184 |
legend pos=north east,
|
|
593
|
3185 |
legend cell align=left]
|
|
|
3186 |
\addplot[red,mark=*, mark options={fill=white}] table {regex1_size_change.data};
|
|
|
3187 |
\end{axis}
|
|
|
3188 |
\end{tikzpicture}
|
|
618
|
3189 |
&
|
|
593
|
3190 |
\begin{tikzpicture}
|
|
|
3191 |
\begin{axis}[
|
|
|
3192 |
xlabel={$n$},
|
|
|
3193 |
x label style={at={(1.05,-0.05)}},
|
|
|
3194 |
%ylabel={time in secs},
|
|
|
3195 |
enlargelimits=false,
|
|
|
3196 |
xtick={0,5,...,30},
|
|
|
3197 |
xmax=33,
|
|
611
|
3198 |
%ymax=1000,
|
|
|
3199 |
%ytick={0,100,...,1000},
|
|
593
|
3200 |
scaled ticks=false,
|
|
|
3201 |
axis lines=left,
|
|
618
|
3202 |
width=4.75cm,
|
|
|
3203 |
height=3.8cm,
|
|
593
|
3204 |
legend entries={regex2},
|
|
618
|
3205 |
legend pos=south east,
|
|
593
|
3206 |
legend cell align=left]
|
|
|
3207 |
\addplot[blue,mark=*, mark options={fill=white}] table {regex2_size_change.data};
|
|
|
3208 |
\end{axis}
|
|
|
3209 |
\end{tikzpicture}
|
|
618
|
3210 |
&
|
|
593
|
3211 |
\begin{tikzpicture}
|
|
|
3212 |
\begin{axis}[
|
|
|
3213 |
xlabel={$n$},
|
|
|
3214 |
x label style={at={(1.05,-0.05)}},
|
|
|
3215 |
%ylabel={time in secs},
|
|
|
3216 |
enlargelimits=false,
|
|
|
3217 |
xtick={0,5,...,30},
|
|
|
3218 |
xmax=33,
|
|
611
|
3219 |
%ymax=1000,
|
|
|
3220 |
%ytick={0,100,...,1000},
|
|
593
|
3221 |
scaled ticks=false,
|
|
|
3222 |
axis lines=left,
|
|
618
|
3223 |
width=4.75cm,
|
|
|
3224 |
height=3.8cm,
|
|
593
|
3225 |
legend entries={regex3},
|
|
618
|
3226 |
legend pos=south east,
|
|
593
|
3227 |
legend cell align=left]
|
|
|
3228 |
\addplot[cyan,mark=*, mark options={fill=white}] table {regex3_size_change.data};
|
|
|
3229 |
\end{axis}
|
|
|
3230 |
\end{tikzpicture}\\
|
|
618
|
3231 |
\multicolumn{3}{c}{}
|
|
593
|
3232 |
\end{tabular}
|
|
618
|
3233 |
\caption{Graphs: size change of 3 randomly generated
|
|
|
3234 |
regular expressions $w.r.t.$ input string length.
|
|
|
3235 |
The x axis represents the length of input.}
|
|
611
|
3236 |
\end{figure}
|
|
532
|
3237 |
\noindent
|
|
|
3238 |
Most of the regex's sizes seem to stay within a polynomial bound $w.r.t$ the
|
|
|
3239 |
original size.
|
|
591
|
3240 |
We will discuss improvements to this bound in the next chapter.
|
|
532
|
3241 |
|
|
|
3242 |
|
|
|
3243 |
|
|
618
|
3244 |
\subsection{Possible Further Improvements}
|
|
639
|
3245 |
There are two problems with this finiteness result, though:\\
|
|
618
|
3246 |
(i)
|
|
|
3247 |
First, it is not yet a direct formalisation of our lexer's complexity,
|
|
593
|
3248 |
as a complexity proof would require looking into
|
|
|
3249 |
the time it takes to execute {\bf all} the operations
|
|
618
|
3250 |
involved in the lexer (simp, collect, decode), not just the derivative.\\
|
|
|
3251 |
(ii)
|
|
593
|
3252 |
Second, the bound is not yet tight, and we seek to improve $N_a$ so that
|
|
618
|
3253 |
it is polynomial on $\llbracket a \rrbracket$.\\
|
|
|
3254 |
Still, we believe this contribution is useful,
|
|
590
|
3255 |
because
|
|
|
3256 |
\begin{itemize}
|
|
|
3257 |
\item
|
|
|
3258 |
|
|
618
|
3259 |
The size proof can serve as a starting point for a complexity
|
|
590
|
3260 |
formalisation.
|
|
|
3261 |
Derivatives are the most important phases of our lexer algorithm.
|
|
|
3262 |
Size properties about derivatives covers the majority of the algorithm
|
|
|
3263 |
and is therefore a good indication of complexity of the entire program.
|
|
|
3264 |
\item
|
|
|
3265 |
The bound is already a strong indication that catastrophic
|
|
|
3266 |
backtracking is much less likely to occur in our $\blexersimp$
|
|
|
3267 |
algorithm.
|
|
|
3268 |
We refine $\blexersimp$ with $\blexerStrong$ in the next chapter
|
|
639
|
3269 |
so that we conjecture the bound becomes polynomial.
|
|
590
|
3270 |
\end{itemize}
|
|
593
|
3271 |
|
|
532
|
3272 |
%----------------------------------------------------------------------------------------
|
|
|
3273 |
% SECTION 4
|
|
|
3274 |
%----------------------------------------------------------------------------------------
|
|
593
|
3275 |
|
|
|
3276 |
|
|
|
3277 |
|
|
|
3278 |
|
|
|
3279 |
|
|
|
3280 |
|
|
|
3281 |
|
|
|
3282 |
|
|
532
|
3283 |
One might wonder the actual bound rather than the loose bound we gave
|
|
|
3284 |
for the convenience of an easier proof.
|
|
|
3285 |
How much can the regex $r^* \backslash s$ grow?
|
|
|
3286 |
As earlier graphs have shown,
|
|
|
3287 |
%TODO: reference that graph where size grows quickly
|
|
593
|
3288 |
they can grow at a maximum speed
|
|
|
3289 |
exponential $w.r.t$ the number of characters,
|
|
532
|
3290 |
but will eventually level off when the string $s$ is long enough.
|
|
|
3291 |
If they grow to a size exponential $w.r.t$ the original regex, our algorithm
|
|
|
3292 |
would still be slow.
|
|
|
3293 |
And unfortunately, we have concrete examples
|
|
576
|
3294 |
where such regular expressions grew exponentially large before levelling off:
|
|
618
|
3295 |
\begin{center}
|
|
532
|
3296 |
$(a ^ * + (aa) ^ * + (aaa) ^ * + \ldots +
|
|
618
|
3297 |
(\underbrace{a \ldots a}_{\text{n a's}})^*)^*$
|
|
|
3298 |
\end{center}
|
|
|
3299 |
will already have a maximum
|
|
593
|
3300 |
size that is exponential on the number $n$
|
|
532
|
3301 |
under our current simplification rules:
|
|
|
3302 |
%TODO: graph of a regex whose size increases exponentially.
|
|
|
3303 |
\begin{center}
|
|
593
|
3304 |
\begin{tikzpicture}
|
|
|
3305 |
\begin{axis}[
|
|
|
3306 |
height=0.5\textwidth,
|
|
|
3307 |
width=\textwidth,
|
|
|
3308 |
xlabel=number of a's,
|
|
|
3309 |
xtick={0,...,9},
|
|
|
3310 |
ylabel=maximum size,
|
|
|
3311 |
ymode=log,
|
|
|
3312 |
log basis y={2}
|
|
|
3313 |
]
|
|
|
3314 |
\addplot[mark=*,blue] table {re-chengsong.data};
|
|
|
3315 |
\end{axis}
|
|
|
3316 |
\end{tikzpicture}
|
|
532
|
3317 |
\end{center}
|
|
|
3318 |
|
|
618
|
3319 |
For convenience we use $(\sum_{i=1}^{n} (\underbrace{a \ldots a}_{\text{i a's}})^*)^*$
|
|
532
|
3320 |
to express $(a ^ * + (aa) ^ * + (aaa) ^ * + \ldots +
|
|
|
3321 |
(\underbrace{a \ldots a}_{\text{n a's}})^*$ in the below discussion.
|
|
|
3322 |
The exponential size is triggered by that the regex
|
|
618
|
3323 |
$\sum_{i=1}^{n} (\underbrace{a \ldots a}_{\text{i a's}})^*$
|
|
532
|
3324 |
inside the $(\ldots) ^*$ having exponentially many
|
|
|
3325 |
different derivatives, despite those difference being minor.
|
|
618
|
3326 |
$(\sum_{i=1}^{n} (\underbrace{a \ldots a}_{\text{i a's}})^*)^*\backslash \underbrace{a \ldots a}_{\text{m a's}}$
|
|
532
|
3327 |
will therefore contain the following terms (after flattening out all nested
|
|
|
3328 |
alternatives):
|
|
|
3329 |
\begin{center}
|
|
618
|
3330 |
$(\sum_{i = 1}^{n} (\underbrace{a \ldots a}_{\text{((i - (m' \% i))\%i) a's}})\cdot (\underbrace{a \ldots a}_{\text{i a's}})^* )\cdot (\sum_{i=1}^{n} (\underbrace{a \ldots a}_{\text{i a's}})^*)$\\
|
|
|
3331 |
[1mm]
|
|
593
|
3332 |
$(1 \leq m' \leq m )$
|
|
532
|
3333 |
\end{center}
|
|
639
|
3334 |
There are at least exponentially
|
|
618
|
3335 |
many such terms.\footnote{To be exact, these terms are
|
|
|
3336 |
distinct for $m' \leq L.C.M.(1, \ldots, n)$, the details are omitted,
|
|
|
3337 |
but the point is that the number is exponential.
|
|
|
3338 |
}
|
|
593
|
3339 |
With each new input character taking the derivative against the intermediate result, more and more such distinct
|
|
618
|
3340 |
terms will accumulate.
|
|
|
3341 |
The function $\textit{distinctBy}$ will not be able to de-duplicate any two of these terms
|
|
|
3342 |
\begin{center}
|
|
|
3343 |
$(\sum_{i = 1}^{n}
|
|
|
3344 |
(\underbrace{a \ldots a}_{\text{((i - (m' \% i))\%i) a's}})\cdot
|
|
|
3345 |
(\underbrace{a \ldots a}_{\text{i a's}})^* )\cdot
|
|
|
3346 |
(\sum_{i=1}^{n} (\underbrace{a \ldots a}_{\text{i a's}})^*)^*$\\
|
|
|
3347 |
$(\sum_{i = 1}^{n} (\underbrace{a \ldots a}_{\text{((i - (m'' \% i))\%i) a's}})\cdot
|
|
|
3348 |
(\underbrace{a \ldots a}_{\text{i a's}})^* )\cdot
|
|
|
3349 |
(\sum_{i=1}^{n} (\underbrace{a \ldots a}_{\text{i a's}})^*)^*$
|
|
|
3350 |
\end{center}
|
|
|
3351 |
\noindent
|
|
|
3352 |
where $m' \neq m''$
|
|
593
|
3353 |
as they are slightly different.
|
|
|
3354 |
This means that with our current simplification methods,
|
|
|
3355 |
we will not be able to control the derivative so that
|
|
618
|
3356 |
$\llbracket \bderssimp{r}{s} \rrbracket$ stays polynomial. %\leq O((\llbracket r\rrbacket)^c)$
|
|
593
|
3357 |
These terms are similar in the sense that the head of those terms
|
|
|
3358 |
are all consisted of sub-terms of the form:
|
|
|
3359 |
$(\underbrace{a \ldots a}_{\text{j a's}})\cdot (\underbrace{a \ldots a}_{\text{i a's}})^* $.
|
|
618
|
3360 |
For $\sum_{i=1}^{n} (\underbrace{a \ldots a}_{\text{i a's}})^*$, there will be at most
|
|
593
|
3361 |
$n * (n + 1) / 2$ such terms.
|
|
|
3362 |
For example, $(a^* + (aa)^* + (aaa)^*) ^*$'s derivatives
|
|
|
3363 |
can be described by 6 terms:
|
|
|
3364 |
$a^*$, $a\cdot (aa)^*$, $ (aa)^*$,
|
|
|
3365 |
$aa \cdot (aaa)^*$, $a \cdot (aaa)^*$, and $(aaa)^*$.
|
|
532
|
3366 |
The total number of different "head terms", $n * (n + 1) / 2$,
|
|
593
|
3367 |
is proportional to the number of characters in the regex
|
|
618
|
3368 |
$(\sum_{i=1}^{n} (\underbrace{a \ldots a}_{\text{i a's}})^*)^*$.
|
|
|
3369 |
If we can improve our deduplication process so that it becomes smarter
|
|
|
3370 |
and only keep track of these $n * (n+1) /2$ terms, then we can keep
|
|
|
3371 |
the size growth polynomial again.
|
|
|
3372 |
This example also suggests a slightly different notion of size, which we call the
|
|
532
|
3373 |
alphabetic width:
|
|
618
|
3374 |
\begin{center}
|
|
|
3375 |
\begin{tabular}{lcl}
|
|
|
3376 |
$\textit{awidth} \; \ZERO$ & $\dn$ & $0$\\
|
|
|
3377 |
$\textit{awidth} \; \ONE$ & $\dn$ & $0$\\
|
|
|
3378 |
$\textit{awidth} \; c$ & $\dn$ & $1$\\
|
|
|
3379 |
$\textit{awidth} \; r_1 + r_2$ & $\dn$ & $\textit{awidth} \;
|
|
|
3380 |
r_1 + \textit{awidth} \; r_2$\\
|
|
|
3381 |
$\textit{awidth} \; r_1 \cdot r_2$ & $\dn$ & $\textit{awidth} \;
|
|
|
3382 |
r_1 + \textit{awidth} \; r_2$\\
|
|
|
3383 |
$\textit{awidth} \; r^*$ & $\dn$ & $\textit{awidth} \; r$\\
|
|
|
3384 |
\end{tabular}
|
|
|
3385 |
\end{center}
|
|
|
3386 |
|
|
532
|
3387 |
|
|
593
|
3388 |
|
|
532
|
3389 |
Antimirov\parencite{Antimirov95} has proven that
|
|
618
|
3390 |
$\textit{PDER}_{UNIV}(r) \leq \textit{awidth}(r)$,
|
|
532
|
3391 |
where $\textit{PDER}_{UNIV}(r)$ is a set of all possible subterms
|
|
|
3392 |
created by doing derivatives of $r$ against all possible strings.
|
|
|
3393 |
If we can make sure that at any moment in our lexing algorithm our
|
|
|
3394 |
intermediate result hold at most one copy of each of the
|
|
|
3395 |
subterms then we can get the same bound as Antimirov's.
|
|
|
3396 |
This leads to the algorithm in the next chapter.
|
|
|
3397 |
|
|
|
3398 |
|
|
|
3399 |
|
|
|
3400 |
|
|
|
3401 |
|
|
|
3402 |
%----------------------------------------------------------------------------------------
|
|
|
3403 |
% SECTION 1
|
|
|
3404 |
%----------------------------------------------------------------------------------------
|
|
|
3405 |
|
|
|
3406 |
|
|
|
3407 |
%-----------------------------------
|
|
|
3408 |
% SUBSECTION 1
|
|
|
3409 |
%-----------------------------------
|
|
618
|
3410 |
%\subsection{Syntactic Equivalence Under $\simp$}
|
|
|
3411 |
%We prove that minor differences can be annhilated
|
|
|
3412 |
%by $\simp$.
|
|
|
3413 |
%For example,
|
|
|
3414 |
%\begin{center}
|
|
|
3415 |
% $\simp \;(\simpALTs\; (\map \;(\_\backslash \; x)\; (\distinct \; \mathit{rs}\; \phi))) =
|
|
|
3416 |
% \simp \;(\simpALTs \;(\distinct \;(\map \;(\_ \backslash\; x) \; \mathit{rs}) \; \phi))$
|
|
|
3417 |
%\end{center}
|
|
532
|
3418 |
|