|
532
|
1 |
% Chapter Template
|
|
|
2 |
|
|
|
3 |
\chapter{A Better Bound and Other Extensions} % Main chapter title
|
|
|
4 |
|
|
|
5 |
\label{Cubic} %In Chapter 5\ref{Chapter5} we discuss stronger simplifications to improve the finite bound
|
|
|
6 |
%in Chapter 4 to a polynomial one, and demonstrate how one can extend the
|
|
|
7 |
%algorithm to include constructs such as bounded repetitions and negations.
|
|
590
|
8 |
\lstset{style=myScalastyle}
|
|
|
9 |
|
|
|
10 |
|
|
|
11 |
This chapter is a ``miscellaneous''
|
|
|
12 |
chapter which records various
|
|
|
13 |
extensions to our $\blexersimp$'s formalisations.\\
|
|
|
14 |
Firstly we present further improvements
|
|
|
15 |
made to our lexer algorithm $\blexersimp$.
|
|
|
16 |
We devise a stronger simplification algorithm,
|
|
|
17 |
called $\bsimpStrong$, which can prune away
|
|
|
18 |
similar components in two regular expressions at the same
|
|
|
19 |
alternative level,
|
|
|
20 |
even if these regular expressions are not exactly the same.
|
|
|
21 |
We call the lexer that uses this stronger simplification function
|
|
|
22 |
$\blexerStrong$.
|
|
|
23 |
We conjecture that both
|
|
|
24 |
\begin{center}
|
|
|
25 |
$\blexerStrong \;r \; s = \blexer\; r\;s$
|
|
|
26 |
\end{center}
|
|
|
27 |
and
|
|
|
28 |
\begin{center}
|
|
|
29 |
$\llbracket \bdersStrong{a}{s} \rrbracket = O(\llbracket a \rrbracket^3)$
|
|
|
30 |
\end{center}
|
|
|
31 |
hold, but formalising
|
|
|
32 |
them is still work in progress.
|
|
|
33 |
We give reasons why the correctness and cubic size bound proofs
|
|
|
34 |
can be achieved,
|
|
|
35 |
by exploring the connection between the internal
|
|
|
36 |
data structure of our $\blexerStrong$ and
|
|
|
37 |
Animirov's partial derivatives.\\
|
|
|
38 |
Secondly, we extend our $\blexersimp$
|
|
|
39 |
to support bounded repetitions ($r^{\{n\}}$).
|
|
|
40 |
We update our formalisation of
|
|
|
41 |
the correctness and finiteness properties to
|
|
621
|
42 |
include this new construct.
|
|
|
43 |
we can out-compete other verified lexers such as
|
|
|
44 |
Verbatim++ on bounded regular expressions.
|
|
|
45 |
%We also present the idempotency property proof
|
|
620
|
46 |
%of $\bsimp$, which leverages the idempotency proof of $\rsimp$.
|
|
|
47 |
%This reinforces our claim that the fixpoint construction
|
|
|
48 |
%originally required by Sulzmann and Lu can be removed in $\blexersimp$.
|
|
621
|
49 |
|
|
|
50 |
%Last but not least, we present our efforts and challenges we met
|
|
|
51 |
%in further improving the algorithm by data
|
|
|
52 |
%structures such as zippers.
|
|
590
|
53 |
|
|
|
54 |
|
|
|
55 |
|
|
532
|
56 |
%----------------------------------------------------------------------------------------
|
|
|
57 |
% SECTION strongsimp
|
|
|
58 |
%----------------------------------------------------------------------------------------
|
|
|
59 |
\section{A Stronger Version of Simplification}
|
|
|
60 |
%TODO: search for isabelle proofs of algorithms that check equivalence
|
|
590
|
61 |
In our bitcoded lexing algorithm, (sub)terms represent (sub)matches.
|
|
591
|
62 |
For example, the regular expression
|
|
|
63 |
\[
|
|
|
64 |
aa \cdot a^*+ a \cdot a^* + aa\cdot a^*
|
|
|
65 |
\]
|
|
|
66 |
contains three terms,
|
|
|
67 |
expressing three possibilities it will match future input.
|
|
|
68 |
The first and the third terms are identical, which means we can eliminate
|
|
|
69 |
the latter as we know it will not be picked up by $\bmkeps$.
|
|
|
70 |
In $\bsimps$, the $\distinctBy$ function takes care of this.
|
|
|
71 |
The criteria $\distinctBy$ uses for removing a duplicate
|
|
|
72 |
$a_2$ in the list
|
|
|
73 |
\begin{center}
|
|
|
74 |
$rs_a@[a_1]@rs_b@[a_2]@rs_c$
|
|
|
75 |
\end{center}
|
|
|
76 |
is that
|
|
533
|
77 |
\begin{center}
|
|
591
|
78 |
$\rerase{a_1} = \rerase{a_2}$.
|
|
|
79 |
\end{center}
|
|
|
80 |
It can be characterised as the $LD$
|
|
|
81 |
rewrite rule in \ref{rrewriteRules}.\\
|
|
|
82 |
The problem , however, is that identical components
|
|
|
83 |
in two slightly different regular expressions cannot be removed:
|
|
|
84 |
\begin{figure}[H]
|
|
|
85 |
\[
|
|
|
86 |
(a+b+d) \cdot r_1 + (a+c+e) \cdot r_1 \stackrel{?}{\rightsquigarrow} (a+b+d) \cdot r_1 + (c+e) \cdot r_1
|
|
|
87 |
\]
|
|
|
88 |
\caption{Desired simplification, but not done in $\blexersimp$}\label{partialDedup}
|
|
|
89 |
\end{figure}
|
|
|
90 |
\noindent
|
|
|
91 |
A simplification like this actually
|
|
|
92 |
cannot be omitted,
|
|
621
|
93 |
as without it the size could blow up even with our $\textit{bsimp}$
|
|
|
94 |
function: for the chapter \ref{Finite} example
|
|
|
95 |
$\protect((a^* + (aa)^* + \ldots + (\underbrace{a\ldots a}_{n a's})^* )^*)^*$,
|
|
|
96 |
by just setting n to a small number,
|
|
|
97 |
we get exponential growth that does not stop before it becomes huge:
|
|
591
|
98 |
\begin{figure}[H]
|
|
|
99 |
\centering
|
|
|
100 |
\begin{tikzpicture}
|
|
|
101 |
\begin{axis}[
|
|
|
102 |
%xlabel={$n$},
|
|
|
103 |
myplotstyle,
|
|
|
104 |
xlabel={input length},
|
|
|
105 |
ylabel={size},
|
|
|
106 |
]
|
|
|
107 |
\addplot[blue,mark=*, mark options={fill=white}] table {bsimpExponential.data};
|
|
|
108 |
\end{axis}
|
|
533
|
109 |
\end{tikzpicture}
|
|
591
|
110 |
\caption{Runtime of $\blexersimp$ for matching
|
|
|
111 |
$\protect((a^* + (aa)^* + \ldots + (aaaaa)^* )^*)^*$
|
|
|
112 |
with strings
|
|
|
113 |
of the form $\protect\underbrace{aa..a}_{n}$.}\label{blexerExp}
|
|
|
114 |
\end{figure}
|
|
|
115 |
\noindent
|
|
|
116 |
We would like to apply the rewriting at some stage
|
|
|
117 |
\begin{figure}[H]
|
|
|
118 |
\[
|
|
|
119 |
(a+b+d) \cdot r_1 \longrightarrow a \cdot r_1 + b \cdot r_1 + d \cdot r_1
|
|
|
120 |
\]
|
|
|
121 |
\caption{Desired simplification, but not done in $\blexersimp$}\label{desiredSimp}
|
|
533
|
122 |
\end{figure}
|
|
|
123 |
\noindent
|
|
591
|
124 |
in our $\simp$ function,
|
|
|
125 |
so that it makes the simplification in \ref{partialDedup} possible.
|
|
621
|
126 |
Translating the rule into our $\textit{bsimp}$ function simply
|
|
|
127 |
involves adding a new clause to the $\textit{bsimp}_{ASEQ}$ function:
|
|
|
128 |
\begin{center}
|
|
|
129 |
\begin{tabular}{@{}lcl@{}}
|
|
|
130 |
$\textit{bsimp}_{ASEQ} \; bs\; a \; b$ & $\dn$ & $ (a,\; b) \textit{match}$\\
|
|
|
131 |
&& $\ldots$\\
|
|
|
132 |
&&$\quad\textit{case} \; (_{bs1}\sum as, a_2') \Rightarrow _{bs1}\sum (
|
|
|
133 |
\map \; (_{[]}\textit{ASEQ} \; \_ \; a_2') \; as)$\\
|
|
|
134 |
&&$\quad\textit{case} \; (a_1', a_2') \Rightarrow _{bs}a_1' \cdot a_2'$ \\
|
|
|
135 |
\end{tabular}
|
|
|
136 |
\end{center}
|
|
|
137 |
|
|
|
138 |
|
|
533
|
139 |
|
|
591
|
140 |
Unfortunately,
|
|
|
141 |
if we introduce them in our
|
|
|
142 |
setting we would lose the POSIX property of our calculated values.
|
|
|
143 |
For example given the regular expression
|
|
|
144 |
\begin{center}
|
|
|
145 |
$(a + ab)(bc + c)$
|
|
|
146 |
\end{center}
|
|
|
147 |
and the string
|
|
|
148 |
\begin{center}
|
|
|
149 |
$ab$,
|
|
533
|
150 |
\end{center}
|
|
591
|
151 |
then our algorithm generates the following
|
|
|
152 |
correct POSIX value
|
|
|
153 |
\begin{center}
|
|
|
154 |
$\Seq \; (\Right \; ab) \; (\Right \; c)$.
|
|
533
|
155 |
\end{center}
|
|
591
|
156 |
Essentially it matches the string with the longer Right-alternative
|
|
|
157 |
in the first sequence (and
|
|
|
158 |
then the 'rest' with the character regular expression $c$ from the second sequence).
|
|
|
159 |
If we add the simplification above, then we obtain the following value
|
|
|
160 |
\begin{center}
|
|
|
161 |
$\Left \; (\Seq \; a \; (\Left \; bc))$
|
|
|
162 |
\end{center}
|
|
|
163 |
where the $\Left$-alternatives get priority.
|
|
|
164 |
However this violates the POSIX rules.
|
|
|
165 |
The reason for getting this undesired value
|
|
|
166 |
is that the new rule splits this regular expression up into
|
|
|
167 |
\begin{center}
|
|
|
168 |
$a\cdot(b c + c) + ab \cdot (bc + c)$,
|
|
533
|
169 |
\end{center}
|
|
591
|
170 |
which becomes a regular expression with a
|
|
|
171 |
totally different structure--the original
|
|
|
172 |
was a sequence, and now it becomes an alternative.
|
|
|
173 |
With an alternative the maximum munch rule no longer works.\\
|
|
|
174 |
A method to reconcile this is to do the
|
|
|
175 |
transformation in \ref{desiredSimp} ``non-invasively'',
|
|
|
176 |
meaning that we traverse the list of regular expressions
|
|
|
177 |
\begin{center}
|
|
|
178 |
$rs_a@[a]@rs_c$
|
|
|
179 |
\end{center}
|
|
|
180 |
in the alternative
|
|
|
181 |
\begin{center}
|
|
|
182 |
$\sum ( rs_a@[a]@rs_c)$
|
|
533
|
183 |
\end{center}
|
|
591
|
184 |
using a function similar to $\distinctBy$,
|
|
|
185 |
but this time
|
|
|
186 |
we allow a more general list rewrite:
|
|
592
|
187 |
\begin{mathpar}\label{cubicRule}
|
|
621
|
188 |
\inferrule * [Right = cubicRule]{\vspace{0mm} }{rs_a@[a]@rs_c
|
|
591
|
189 |
\stackrel{s}{\rightsquigarrow }
|
|
|
190 |
rs_a@[\textit{prune} \; a \; rs_a]@rs_c }
|
|
592
|
191 |
\end{mathpar}
|
|
591
|
192 |
%L \; a_1' = L \; a_1 \setminus (\cup_{a \in rs_a} L \; a)
|
|
|
193 |
where $\textit{prune} \;a \; acc$ traverses $a$
|
|
|
194 |
without altering the structure of $a$, removing components in $a$
|
|
|
195 |
that have appeared in the accumulator $acc$.
|
|
|
196 |
For example
|
|
|
197 |
\begin{center}
|
|
|
198 |
$\textit{prune} \;\;\; (r_a+r_f+r_g+r_h)r_d \;\; \; [(r_a+r_b+r_c)r_d, (r_e+r_f)r_d] $
|
|
|
199 |
\end{center}
|
|
|
200 |
should be equal to
|
|
|
201 |
\begin{center}
|
|
|
202 |
$(r_g+r_h)r_d$
|
|
|
203 |
\end{center}
|
|
|
204 |
because $r_gr_d$ and
|
|
|
205 |
$r_hr_d$ are the only terms
|
|
|
206 |
that have not appeared in the accumulator list
|
|
|
207 |
\begin{center}
|
|
|
208 |
$[(r_a+r_b+r_c)r_d, (r_e+r_f)r_d]$.
|
|
|
209 |
\end{center}
|
|
|
210 |
We implemented
|
|
|
211 |
function $\textit{prune}$ in Scala,
|
|
|
212 |
and incorporated into our lexer,
|
|
|
213 |
by replacing the $\simp$ function
|
|
|
214 |
with a stronger version called $\bsimpStrong$
|
|
|
215 |
that prunes regular expressions.
|
|
590
|
216 |
\begin{figure}[H]
|
|
621
|
217 |
|
|
591
|
218 |
\begin{lstlisting}
|
|
|
219 |
def atMostEmpty(r: Rexp) : Boolean = r match {
|
|
|
220 |
case ZERO => true
|
|
|
221 |
case ONE => true
|
|
|
222 |
case STAR(r) => atMostEmpty(r)
|
|
|
223 |
case SEQ(r1, r2) => atMostEmpty(r1) && atMostEmpty(r2)
|
|
|
224 |
case ALTS(r1, r2) => atMostEmpty(r1) && atMostEmpty(r2)
|
|
|
225 |
case CHAR(_) => false
|
|
|
226 |
}
|
|
|
227 |
|
|
|
228 |
|
|
|
229 |
def isOne(r: Rexp) : Boolean = r match {
|
|
|
230 |
case ONE => true
|
|
|
231 |
case SEQ(r1, r2) => isOne(r1) && isOne(r2)
|
|
|
232 |
case ALTS(r1, r2) => (isOne(r1) || isOne(r2)) && (atMostEmpty(r1) && atMostEmpty(r2))//rs.forall(atMostEmpty) && rs.exists(isOne)
|
|
|
233 |
case STAR(r0) => atMostEmpty(r0)
|
|
|
234 |
case CHAR(c) => false
|
|
|
235 |
case ZERO => false
|
|
|
236 |
}
|
|
|
237 |
|
|
|
238 |
//r = r' ~ tail' : If tail' matches tail => returns r'
|
|
|
239 |
def removeSeqTail(r: Rexp, tail: Rexp) : Rexp = r match {
|
|
|
240 |
case SEQ(r1, r2) =>
|
|
|
241 |
if(r2 == tail)
|
|
|
242 |
r1
|
|
|
243 |
else
|
|
|
244 |
ZERO
|
|
|
245 |
case r => ZERO
|
|
|
246 |
}
|
|
|
247 |
|
|
|
248 |
def prune(r: ARexp, acc: Set[Rexp]) : ARexp = r match{
|
|
|
249 |
case AALTS(bs, rs) => rs.map(r => prune(r, acc)).filter(_ != ZERO) match
|
|
|
250 |
{
|
|
|
251 |
//all components have been removed, meaning this is effectively a duplicate
|
|
|
252 |
//flats will take care of removing this AZERO
|
|
|
253 |
case Nil => AZERO
|
|
|
254 |
case r::Nil => fuse(bs, r)
|
|
|
255 |
case rs1 => AALTS(bs, rs1)
|
|
|
256 |
}
|
|
|
257 |
case ASEQ(bs, r1, r2) =>
|
|
|
258 |
//remove the r2 in (ra + rb)r2 to identify the duplicate contents of r1
|
|
|
259 |
prune(r1, acc.map(r => removeSeqTail(r, erase(r2)))) match {
|
|
|
260 |
//after pruning, returns 0
|
|
|
261 |
case AZERO => AZERO
|
|
|
262 |
//after pruning, got r1'.r2, where r1' is equal to 1
|
|
|
263 |
case r1p if(isOne(erase(r1p))) => fuse(bs ++ mkepsBC(r1p), r2)
|
|
|
264 |
//assemble the pruned head r1p with r2
|
|
|
265 |
case r1p => ASEQ(bs, r1p, r2)
|
|
|
266 |
}
|
|
|
267 |
//this does the duplicate component removal task
|
|
|
268 |
case r => if(acc(erase(r))) AZERO else r
|
|
|
269 |
}
|
|
|
270 |
\end{lstlisting}
|
|
|
271 |
\caption{pruning function together with its helper functions}
|
|
|
272 |
\end{figure}
|
|
|
273 |
\noindent
|
|
|
274 |
The benefits of using
|
|
|
275 |
$\textit{prune}$ such as refining the finiteness bound
|
|
|
276 |
to a cubic bound has not been formalised yet.
|
|
|
277 |
Therefore we choose to use Scala code rather than an Isabelle-style formal
|
|
|
278 |
definition like we did for $\simp$, as the definitions might change
|
|
|
279 |
to suit proof needs.
|
|
|
280 |
In the rest of the chapter we will use this convention consistently.
|
|
|
281 |
\begin{figure}[H]
|
|
|
282 |
\begin{lstlisting}
|
|
|
283 |
def distinctWith(rs: List[ARexp],
|
|
|
284 |
pruneFunction: (ARexp, Set[Rexp]) => ARexp,
|
|
|
285 |
acc: Set[Rexp] = Set()) : List[ARexp] =
|
|
|
286 |
rs match{
|
|
|
287 |
case Nil => Nil
|
|
|
288 |
case r :: rs =>
|
|
|
289 |
if(acc(erase(r)))
|
|
|
290 |
distinctWith(rs, pruneFunction, acc)
|
|
|
291 |
else {
|
|
|
292 |
val pruned_r = pruneFunction(r, acc)
|
|
|
293 |
pruned_r ::
|
|
|
294 |
distinctWith(rs,
|
|
|
295 |
pruneFunction,
|
|
|
296 |
turnIntoTerms(erase(pruned_r)) ++: acc
|
|
|
297 |
)
|
|
|
298 |
}
|
|
|
299 |
}
|
|
|
300 |
\end{lstlisting}
|
|
|
301 |
\caption{A Stronger Version of $\textit{distinctBy}$}
|
|
|
302 |
\end{figure}
|
|
|
303 |
\noindent
|
|
|
304 |
The function $\textit{prune}$ is used in $\distinctWith$.
|
|
|
305 |
$\distinctWith$ is a stronger version of $\distinctBy$
|
|
|
306 |
which not only removes duplicates as $\distinctBy$ would
|
|
|
307 |
do, but also uses the $\textit{pruneFunction}$
|
|
|
308 |
argument to prune away verbose components in a regular expression.\\
|
|
|
309 |
\begin{figure}[H]
|
|
|
310 |
\begin{lstlisting}
|
|
|
311 |
//a stronger version of simp
|
|
|
312 |
def bsimpStrong(r: ARexp): ARexp =
|
|
|
313 |
{
|
|
|
314 |
r match {
|
|
|
315 |
case ASEQ(bs1, r1, r2) => (bsimpStrong(r1), bsimpStrong(r2)) match {
|
|
|
316 |
//normal clauses same as simp
|
|
|
317 |
case (AZERO, _) => AZERO
|
|
|
318 |
case (_, AZERO) => AZERO
|
|
|
319 |
case (AONE(bs2), r2s) => fuse(bs1 ++ bs2, r2s)
|
|
|
320 |
//bs2 can be discarded
|
|
|
321 |
case (r1s, AONE(bs2)) => fuse(bs1, r1s) //assert bs2 == Nil
|
|
|
322 |
case (r1s, r2s) => ASEQ(bs1, r1s, r2s)
|
|
|
323 |
}
|
|
|
324 |
case AALTS(bs1, rs) => {
|
|
|
325 |
//distinctBy(flat_res, erase)
|
|
|
326 |
distinctWith(flats(rs.map(bsimpStrong(_))), prune) match {
|
|
|
327 |
case Nil => AZERO
|
|
|
328 |
case s :: Nil => fuse(bs1, s)
|
|
|
329 |
case rs => AALTS(bs1, rs)
|
|
|
330 |
}
|
|
|
331 |
}
|
|
|
332 |
//stars that can be treated as 1
|
|
|
333 |
case ASTAR(bs, r0) if(atMostEmpty(erase(r0))) => AONE(bs)
|
|
|
334 |
case r => r
|
|
|
335 |
}
|
|
|
336 |
}
|
|
|
337 |
\end{lstlisting}
|
|
|
338 |
\caption{The function $\bsimpStrong$ and $\bdersStrongs$}
|
|
|
339 |
\end{figure}
|
|
|
340 |
\noindent
|
|
|
341 |
$\distinctWith$, is in turn used in $\bsimpStrong$:
|
|
|
342 |
\begin{figure}[H]
|
|
|
343 |
\begin{lstlisting}
|
|
|
344 |
//Conjecture: [| bdersStrong(s, r) |] = O([| r |]^3)
|
|
|
345 |
def bdersStrong(s: List[Char], r: ARexp) : ARexp = s match {
|
|
|
346 |
case Nil => r
|
|
|
347 |
case c::s => bdersStrong(s, bsimpStrong(bder(c, r)))
|
|
|
348 |
}
|
|
|
349 |
\end{lstlisting}
|
|
|
350 |
\caption{The function $\bsimpStrong$ and $\bdersStrongs$}
|
|
|
351 |
\end{figure}
|
|
|
352 |
\noindent
|
|
|
353 |
We conjecture that the above Scala function $\bdersStrongs$,
|
|
|
354 |
written $\bdersStrong{\_}{\_}$ as an infix notation,
|
|
|
355 |
satisfies the following property:
|
|
|
356 |
\begin{conjecture}
|
|
|
357 |
$\llbracket \bdersStrong{a}{s} \rrbracket = O(\llbracket a \rrbracket^3)$
|
|
|
358 |
\end{conjecture}
|
|
|
359 |
The stronger version of $\blexersimp$'s
|
|
|
360 |
code in Scala looks like:
|
|
|
361 |
\begin{figure}[H]
|
|
|
362 |
\begin{lstlisting}
|
|
|
363 |
def strongBlexer(r: Rexp, s: String) : Option[Val] = {
|
|
|
364 |
Try(Some(decode(r, strong_blex_simp(internalise(r), s.toList)))).getOrElse(None)
|
|
|
365 |
}
|
|
|
366 |
def strong_blex_simp(r: ARexp, s: List[Char]) : Bits = s match {
|
|
|
367 |
case Nil => {
|
|
|
368 |
if (bnullable(r)) {
|
|
|
369 |
mkepsBC(r)
|
|
|
370 |
}
|
|
|
371 |
else
|
|
|
372 |
throw new Exception("Not matched")
|
|
|
373 |
}
|
|
|
374 |
case c::cs => {
|
|
|
375 |
strong_blex_simp(strongBsimp(bder(c, r)), cs)
|
|
|
376 |
}
|
|
|
377 |
}
|
|
|
378 |
\end{lstlisting}
|
|
|
379 |
\end{figure}
|
|
|
380 |
\noindent
|
|
621
|
381 |
We call this lexer $\blexerStrong$.
|
|
|
382 |
$\blexerStrong$ is able to drastically reduce the
|
|
|
383 |
internal data structure size which could
|
|
|
384 |
trigger exponential behaviours in
|
|
|
385 |
$\blexersimp$.
|
|
|
386 |
\begin{figure}[H]
|
|
|
387 |
\centering
|
|
|
388 |
\begin{tabular}{@{}c@{\hspace{0mm}}c@{\hspace{0mm}}c@{}}
|
|
|
389 |
\begin{tikzpicture}
|
|
|
390 |
\begin{axis}[
|
|
|
391 |
%xlabel={$n$},
|
|
|
392 |
myplotstyle,
|
|
|
393 |
xlabel={input length},
|
|
|
394 |
ylabel={size},
|
|
|
395 |
width = 7cm,
|
|
|
396 |
height = 5cm,
|
|
|
397 |
]
|
|
|
398 |
\addplot[red,mark=*, mark options={fill=white}] table {strongSimpCurve.data};
|
|
|
399 |
\end{axis}
|
|
|
400 |
\end{tikzpicture}
|
|
|
401 |
&
|
|
|
402 |
\begin{tikzpicture}
|
|
|
403 |
\begin{axis}[
|
|
|
404 |
%xlabel={$n$},
|
|
|
405 |
myplotstyle,
|
|
|
406 |
xlabel={input length},
|
|
|
407 |
ylabel={size},
|
|
|
408 |
width = 7cm,
|
|
|
409 |
height = 5cm,
|
|
|
410 |
]
|
|
|
411 |
\addplot[blue,mark=*, mark options={fill=white}] table {bsimpExponential.data};
|
|
|
412 |
\end{axis}
|
|
|
413 |
\end{tikzpicture}\\
|
|
|
414 |
\multicolumn{2}{l}{}
|
|
|
415 |
\end{tabular}
|
|
|
416 |
\caption{Runtime for matching
|
|
|
417 |
$\protect((a^* + (aa)^* + \ldots + (aaaaa)^* )^*)^*$ with strings
|
|
|
418 |
of the form $\protect\underbrace{aa..a}_{n}$.}\label{fig:aaaaaStarStar}
|
|
|
419 |
\end{figure}
|
|
|
420 |
\noindent
|
|
591
|
421 |
We would like to preserve the correctness like the one
|
|
|
422 |
we had for $\blexersimp$:
|
|
|
423 |
\begin{conjecture}\label{cubicConjecture}
|
|
|
424 |
$\blexerStrong \;r \; s = \blexer\; r\;s$
|
|
|
425 |
\end{conjecture}
|
|
592
|
426 |
\noindent
|
|
621
|
427 |
The idea is to maintain key lemmas in
|
|
|
428 |
chapter \ref{Bitcoded2} like
|
|
|
429 |
$r \stackrel{*}{\rightsquigarrow} \textit{bsimp} \; r$
|
|
|
430 |
with the new rewriting rule \ref{cubicRule} .
|
|
591
|
431 |
|
|
621
|
432 |
In the next sub-section,
|
|
592
|
433 |
we will describe why we
|
|
|
434 |
believe a cubic bound can be achieved.
|
|
|
435 |
We give an introduction to the
|
|
|
436 |
partial derivatives,
|
|
|
437 |
which was invented by Antimirov \cite{Antimirov95},
|
|
|
438 |
and then link it with the result of the function
|
|
|
439 |
$\bdersStrongs$.
|
|
|
440 |
|
|
621
|
441 |
\subsection{Antimirov's partial derivatives}
|
|
|
442 |
Partial derivatives were first introduced by
|
|
|
443 |
Antimirov \cite{Antimirov95}.
|
|
|
444 |
It does derivatives in a similar way as suggested by Brzozowski,
|
|
|
445 |
but splits children of alternative regular expressions into
|
|
|
446 |
multiple independent terms, causing the output to become a
|
|
|
447 |
set of regular expressions:
|
|
|
448 |
\begin{center}
|
|
|
449 |
\begin{tabular}{lcl}
|
|
|
450 |
$\partial_x \; (a \cdot b)$ &
|
|
|
451 |
$\dn$ & $\partial_x \; a\cdot b \cup
|
|
|
452 |
\partial_x \; b \; \textit{if} \; \; \nullable\; a$\\
|
|
|
453 |
& & $\partial_x \; a\cdot b \quad\quad
|
|
|
454 |
\textit{otherwise}$\\
|
|
|
455 |
$\partial_x \; r^*$ & $\dn$ & $\partial_x \; r \cdot r^*$\\
|
|
|
456 |
$\partial_x \; c $ & $\dn$ & $\textit{if} \; x = c \;
|
|
|
457 |
\textit{then} \;
|
|
|
458 |
\{ \ONE\} \;\;\textit{else} \; \varnothing$\\
|
|
|
459 |
$\partial_x(a+b)$ & $=$ & $\partial_x(a) \cup \partial_x(b)$\\
|
|
|
460 |
$\partial_x(\ONE)$ & $=$ & $\varnothing$\\
|
|
|
461 |
$\partial_x(\ZERO)$ & $\dn$ & $\varnothing$\\
|
|
|
462 |
\end{tabular}
|
|
591
|
463 |
\end{center}
|
|
621
|
464 |
\noindent
|
|
|
465 |
The $\cdot$ between for example
|
|
|
466 |
$\partial_x \; a\cdot b $
|
|
|
467 |
is a shorthand notation for the cartesian product
|
|
|
468 |
$\partial_x \; a \times \{ b\}$.
|
|
|
469 |
%Each element in the set generated by a partial derivative
|
|
|
470 |
%corresponds to a (potentially partial) match
|
|
|
471 |
%TODO: define derivatives w.r.t string s
|
|
591
|
472 |
Rather than joining the calculated derivatives $\partial_x a$ and $\partial_x b$ together
|
|
621
|
473 |
using the $\sum$ constructor, Antimirov put them into
|
|
|
474 |
a set. This causes maximum de-duplication to happen,
|
|
591
|
475 |
allowing us to understand what are the "atomic" components of it.
|
|
|
476 |
For example, To compute what regular expression $x^*(xx + y)^*$'s
|
|
|
477 |
derivative against $x$ is made of, one can do a partial derivative
|
|
|
478 |
of it and get two singleton sets $\{x^* \cdot (xx + y)^*\}$ and $\{x \cdot (xx + y) ^* \}$
|
|
|
479 |
from $\partial_x(x^*) \cdot (xx + y) ^*$ and $\partial_x((xx + y)^*)$.
|
|
621
|
480 |
|
|
|
481 |
The set of all possible partial derivatives is defined
|
|
|
482 |
as the union of derivatives w.r.t all the strings in the universe:
|
|
|
483 |
\begin{center}
|
|
|
484 |
\begin{tabular}{lcl}
|
|
|
485 |
$\textit{PDER}_{UNIV} \; r $ & $\dn $ & $\bigcup_{w \in A^*}\partial_w \; r$
|
|
|
486 |
\end{tabular}
|
|
591
|
487 |
\end{center}
|
|
621
|
488 |
\noindent
|
|
591
|
489 |
|
|
621
|
490 |
Back to our
|
|
|
491 |
\begin{center}
|
|
|
492 |
$((a^* + (aa)^* + \ldots + (\underbrace{a\ldots a}_{n a's})^* )^*)^*$
|
|
|
493 |
\end{center}
|
|
|
494 |
example, if we denote this regular expression as $A$,
|
|
|
495 |
we have that
|
|
|
496 |
\begin{center}
|
|
|
497 |
$\textit{PDER}_{UNIV} \; A =
|
|
|
498 |
\bigcup_{i=1}^{n}\bigcup_{j=0}^{i-1} \{
|
|
|
499 |
(\underbrace{a \ldots a}_{\text{j a's}}\cdot
|
|
|
500 |
(\underbrace{a \ldots a}_{\text{i a's}})^*)\cdot A \}$,
|
|
591
|
501 |
\end{center}
|
|
621
|
502 |
with exactly $n * (n + 1) / 2$ terms.
|
|
|
503 |
This is in line with our speculation that only $n*(n+1)/2$ terms are
|
|
|
504 |
needed. We conjecture that $\bsimpStrong$ is also able to achieve this
|
|
|
505 |
upper limit in general
|
|
|
506 |
\begin{conjecture}\label{bsimpStrongInclusionPder}
|
|
|
507 |
Using a suitable transformation $f$, we have
|
|
|
508 |
\begin{center}
|
|
|
509 |
$\forall s.\; f \; (r \bdersStrong \; s) \subseteq
|
|
|
510 |
\textit{PDER}_{UNIV} \; r$
|
|
|
511 |
\end{center}
|
|
|
512 |
\end{conjecture}
|
|
|
513 |
\noindent
|
|
|
514 |
because our \ref{cubicRule} will keep only one copy of each term,
|
|
|
515 |
where the function $\textit{prune}$ takes care of maintaining
|
|
|
516 |
a set like structure similar to partial derivatives.
|
|
|
517 |
It is anticipated we might need to adjust $\textit{prune}$
|
|
|
518 |
slightly to make sure all duplicate terms are eliminated,
|
|
|
519 |
which should be doable.
|
|
591
|
520 |
|
|
621
|
521 |
Antimirov had proven that the sum of all the partial derivative
|
|
|
522 |
terms' sizes is bounded by the cubic of the size of that regular
|
|
|
523 |
expression:
|
|
|
524 |
\begin{property}\label{pderBound}
|
|
|
525 |
$\llbracket \textit{PDER}_{UNIV} \; r \rrbracket \leq O((\llbracket r \rrbracket)^3)$
|
|
|
526 |
\end{property}
|
|
|
527 |
This property was formalised by Urban, and the details are in the PDERIVS.thy file
|
|
|
528 |
in our repository.
|
|
|
529 |
Once conjecture \ref{bsimpStrongInclusionPder} is proven, then property \ref{pderBound}
|
|
|
530 |
would yield us a cubic bound for our $\blexerStrong$ algorithm:
|
|
|
531 |
\begin{conjecture}\label{strongCubic}
|
|
|
532 |
$\llbracket r \bdersStrong\; s \rrbracket \leq \llbracket r \rrbracket^3$
|
|
|
533 |
\end{conjecture}
|
|
591
|
534 |
|
|
|
535 |
|
|
621
|
536 |
%To get all the "atomic" components of a regular expression's possible derivatives,
|
|
|
537 |
%there is a procedure Antimirov called $\textit{lf}$, short for "linear forms", that takes
|
|
|
538 |
%whatever character is available at the head of the string inside the language of a
|
|
|
539 |
%regular expression, and gives back the character and the derivative regular expression
|
|
|
540 |
%as a pair (which he called "monomial"):
|
|
|
541 |
% \begin{center}
|
|
|
542 |
% \begin{tabular}{ccc}
|
|
|
543 |
% $\lf(\ONE)$ & $=$ & $\phi$\\
|
|
|
544 |
%$\lf(c)$ & $=$ & $\{(c, \ONE) \}$\\
|
|
|
545 |
% $\lf(a+b)$ & $=$ & $\lf(a) \cup \lf(b)$\\
|
|
|
546 |
% $\lf(r^*)$ & $=$ & $\lf(r) \bigodot \lf(r^*)$\\
|
|
|
547 |
%\end{tabular}
|
|
|
548 |
%\end{center}
|
|
|
549 |
%%TODO: completion
|
|
|
550 |
%
|
|
|
551 |
%There is a slight difference in the last three clauses compared
|
|
|
552 |
%with $\partial$: instead of a dot operator $ \textit{rset} \cdot r$ that attaches the regular
|
|
|
553 |
%expression $r$ with every element inside $\textit{rset}$ to create a set of
|
|
|
554 |
%sequence derivatives, it uses the "circle dot" operator $\bigodot$ which operates
|
|
|
555 |
%on a set of monomials (which Antimirov called "linear form") and a regular
|
|
|
556 |
%expression, and returns a linear form:
|
|
|
557 |
% \begin{center}
|
|
|
558 |
% \begin{tabular}{ccc}
|
|
|
559 |
% $l \bigodot (\ZERO)$ & $=$ & $\phi$\\
|
|
|
560 |
% $l \bigodot (\ONE)$ & $=$ & $l$\\
|
|
|
561 |
% $\phi \bigodot t$ & $=$ & $\phi$\\
|
|
|
562 |
% $\{ (x, \ZERO) \} \bigodot t$ & $=$ & $\{(x,\ZERO) \}$\\
|
|
|
563 |
% $\{ (x, \ONE) \} \bigodot t$ & $=$ & $\{(x,t) \}$\\
|
|
|
564 |
% $\{ (x, p) \} \bigodot t$ & $=$ & $\{(x,p\cdot t) \}$\\
|
|
|
565 |
% $\lf(a+b)$ & $=$ & $\lf(a) \cup \lf(b)$\\
|
|
|
566 |
% $\lf(r^*)$ & $=$ & $\lf(r) \cdot \lf(r^*)$\\
|
|
|
567 |
%\end{tabular}
|
|
|
568 |
%\end{center}
|
|
|
569 |
%%TODO: completion
|
|
|
570 |
%
|
|
|
571 |
% Some degree of simplification is applied when doing $\bigodot$, for example,
|
|
|
572 |
% $l \bigodot (\ZERO) = \phi$ corresponds to $r \cdot \ZERO \rightsquigarrow \ZERO$,
|
|
|
573 |
% and $l \bigodot (\ONE) = l$ to $l \cdot \ONE \rightsquigarrow l$, and
|
|
|
574 |
% $\{ (x, \ZERO) \} \bigodot t = \{(x,\ZERO) \}$ to $\ZERO \cdot x \rightsquigarrow \ZERO$,
|
|
|
575 |
% and so on.
|
|
|
576 |
%
|
|
|
577 |
% With the function $\lf$ one can compute all possible partial derivatives $\partial_{UNIV}(r)$ of a regular expression $r$ with
|
|
|
578 |
% an iterative procedure:
|
|
|
579 |
% \begin{center}
|
|
|
580 |
% \begin{tabular}{llll}
|
|
|
581 |
%$\textit{while}$ & $(\Delta_i \neq \phi)$ & & \\
|
|
|
582 |
% & $\Delta_{i+1}$ & $ =$ & $\lf(\Delta_i) - \PD_i$ \\
|
|
|
583 |
% & $\PD_{i+1}$ & $ =$ & $\Delta_{i+1} \cup \PD_i$ \\
|
|
|
584 |
%$\partial_{UNIV}(r)$ & $=$ & $\PD$ &
|
|
|
585 |
%\end{tabular}
|
|
|
586 |
%\end{center}
|
|
|
587 |
%
|
|
|
588 |
%
|
|
|
589 |
% $(r_1 + r_2) \cdot r_3 \longrightarrow (r_1 \cdot r_3) + (r_2 \cdot r_3)$,
|
|
591
|
590 |
|
|
|
591 |
|
|
532
|
592 |
|
|
|
593 |
|
|
|
594 |
%----------------------------------------------------------------------------------------
|
|
|
595 |
% SECTION 2
|
|
|
596 |
%----------------------------------------------------------------------------------------
|
|
|
597 |
|
|
|
598 |
\section{Bounded Repetitions}
|
|
612
|
599 |
We have promised in chapter \ref{Introduction}
|
|
|
600 |
that our lexing algorithm can potentially be extended
|
|
|
601 |
to handle bounded repetitions
|
|
|
602 |
in natural and elegant ways.
|
|
|
603 |
Now we fulfill our promise by adding support for
|
|
|
604 |
the ``exactly-$n$-times'' bounded regular expression $r^{\{n\}}$.
|
|
|
605 |
We add clauses in our derivatives-based lexing algorithms (with simplifications)
|
|
|
606 |
introduced in chapter \ref{Bitcoded2}.
|
|
|
607 |
|
|
|
608 |
\subsection{Augmented Definitions}
|
|
621
|
609 |
There are a number of definitions that need to be augmented.
|
|
612
|
610 |
The most notable one would be the POSIX rules for $r^{\{n\}}$:
|
|
621
|
611 |
\begin{center}
|
|
|
612 |
\begin{mathpar}
|
|
|
613 |
\inferrule{\forall v \in vs_1. \vdash v:r \land
|
|
|
614 |
|v| \neq []\\ \forall v \in vs_2. \vdash v:r \land |v| = []\\
|
|
|
615 |
\textit{length} \; (vs_1 @ vs_2) = n}{\textit{Stars} \;
|
|
|
616 |
(vs_1 @ vs_2) : r^{\{n\}} }
|
|
|
617 |
\end{mathpar}
|
|
|
618 |
\end{center}
|
|
|
619 |
As Ausaf had pointed out \cite{Ausaf},
|
|
|
620 |
sometimes empty iterations have to be taken to get
|
|
|
621 |
a match with exactly $n$ repetitions,
|
|
|
622 |
and hence the $vs_2$ part.
|
|
|
623 |
|
|
|
624 |
Another important definition would be the size:
|
|
|
625 |
\begin{center}
|
|
|
626 |
\begin{tabular}{lcl}
|
|
|
627 |
$\llbracket r^{\{n\}} \rrbracket_r$ & $\dn$ &
|
|
|
628 |
$\llbracket r \rrbracket_r + n$\\
|
|
|
629 |
\end{tabular}
|
|
|
630 |
\end{center}
|
|
|
631 |
\noindent
|
|
|
632 |
Arguably we should use $\log \; n$ for the size because
|
|
|
633 |
the number of digits increase logarithmically w.r.t $n$.
|
|
|
634 |
For simplicity we choose to add the counter directly to the size.
|
|
|
635 |
|
|
|
636 |
The derivative w.r.t a bounded regular expression
|
|
|
637 |
is given as
|
|
|
638 |
\begin{center}
|
|
|
639 |
\begin{tabular}{lcl}
|
|
|
640 |
$r^{\{n\}} \backslash_r c$ & $\dn$ &
|
|
|
641 |
$r\backslash_r c \cdot r^{\{n-1\}} \;\; \textit{if} \; n \geq 1$\\
|
|
|
642 |
& & $\RZERO \;\quad \quad\quad \quad
|
|
|
643 |
\textit{otherwise}$\\
|
|
|
644 |
\end{tabular}
|
|
|
645 |
\end{center}
|
|
|
646 |
\noindent
|
|
|
647 |
For brevity, we sometimes use NTIMES to refer to bounded
|
|
|
648 |
regular expressions.
|
|
|
649 |
The $\mkeps$ function clause for NTIMES would be
|
|
|
650 |
\begin{center}
|
|
|
651 |
\begin{tabular}{lcl}
|
|
|
652 |
$\mkeps \; r^{\{n\}} $ & $\dn$ & $\Stars \;
|
|
|
653 |
(\textit{replicate} \; n\; (\mkeps \; r))$
|
|
|
654 |
\end{tabular}
|
|
|
655 |
\end{center}
|
|
|
656 |
\noindent
|
|
|
657 |
The injection looks like
|
|
|
658 |
\begin{center}
|
|
|
659 |
\begin{tabular}{lcl}
|
|
|
660 |
$\inj \; r^{\{n\}} \; c\; (\Seq \;v \; (\Stars \; vs)) $ &
|
|
|
661 |
$\dn$ & $\Stars \;
|
|
|
662 |
((\inj \; r \;c \;v ) :: vs)$
|
|
|
663 |
\end{tabular}
|
|
|
664 |
\end{center}
|
|
|
665 |
\noindent
|
|
612
|
666 |
|
|
|
667 |
|
|
|
668 |
\subsection{Proofs for the Augmented Lexing Algorithm}
|
|
|
669 |
We need to maintain two proofs with the additional $r^{\{n\}}$
|
|
|
670 |
construct: the
|
|
|
671 |
correctness proof in chapter \ref{Bitcoded2},
|
|
|
672 |
and the finiteness proof in chapter \ref{Finite}.
|
|
|
673 |
|
|
|
674 |
\subsubsection{Correctness Proof Augmentation}
|
|
|
675 |
The correctness of $\textit{lexer}$ and $\textit{blexer}$ with bounded repetitions
|
|
|
676 |
have been proven by Ausaf and Urban\cite{AusafDyckhoffUrban2016}.
|
|
|
677 |
As they have commented, once the definitions are in place,
|
|
|
678 |
the proofs given for the basic regular expressions will extend to
|
|
|
679 |
bounded regular expressions, and there are no ``surprises''.
|
|
|
680 |
We confirm this point because the correctness theorem would also
|
|
|
681 |
extend without surprise to $\blexersimp$.
|
|
|
682 |
The rewrite rules such as $\rightsquigarrow$, $\stackrel{s}{\rightsquigarrow}$ and so on
|
|
|
683 |
do not need to be changed,
|
|
|
684 |
and only a few lemmas such as lemma \ref{fltsPreserves} need to be adjusted to
|
|
|
685 |
add one more line which can be solved by sledgehammer
|
|
|
686 |
to solve the $r^{\{n\}}$ inductive case.
|
|
|
687 |
|
|
|
688 |
|
|
|
689 |
\subsubsection{Finiteness Proof Augmentation}
|
|
620
|
690 |
The bounded repetitions are
|
|
|
691 |
very similar to stars, and therefore the treatment
|
|
|
692 |
is similar, with minor changes to handle some slight complications
|
|
|
693 |
when the counter reaches 0.
|
|
|
694 |
The exponential growth is similar:
|
|
|
695 |
\begin{center}
|
|
|
696 |
\begin{tabular}{ll}
|
|
|
697 |
$r^{\{n\}} $ & $\longrightarrow_{\backslash c}$\\
|
|
|
698 |
$(r\backslash c) \cdot
|
|
|
699 |
r^{\{n - 1\}}*$ & $\longrightarrow_{\backslash c'}$\\
|
|
|
700 |
\\
|
|
|
701 |
$r \backslash cc' \cdot r^{\{n - 2\}}* +
|
|
|
702 |
r \backslash c' \cdot r^{\{n - 1\}}*$ &
|
|
|
703 |
$\longrightarrow_{\backslash c''}$\\
|
|
|
704 |
\\
|
|
|
705 |
$(r_1 \backslash cc'c'' \cdot r^{\{n-3\}}* +
|
|
|
706 |
r \backslash c''\cdot r^{\{n-1\}}) +
|
|
|
707 |
(r \backslash c'c'' \cdot r^{\{n-2\}}* +
|
|
|
708 |
r \backslash c'' \cdot r^{\{n-1\}}*)$ &
|
|
|
709 |
$\longrightarrow_{\backslash c'''}$ \\
|
|
|
710 |
\\
|
|
|
711 |
$\ldots$\\
|
|
|
712 |
\end{tabular}
|
|
|
713 |
\end{center}
|
|
|
714 |
Again, we assume that $r\backslash c$, $r \backslash cc'$ and so on
|
|
|
715 |
are all nullable.
|
|
|
716 |
The flattened list of terms for $r^{\{n\}} \backslash_{rs} s$
|
|
|
717 |
\begin{center}
|
|
|
718 |
$[r_1 \backslash cc'c'' \cdot r^{\{n-3\}}*,\;
|
|
|
719 |
r \backslash c''\cdot r^{\{n-1\}}, \;
|
|
|
720 |
r \backslash c'c'' \cdot r^{\{n-2\}}*, \;
|
|
|
721 |
r \backslash c'' \cdot r^{\{n-1\}}*,\; \ldots ]$
|
|
|
722 |
\end{center}
|
|
|
723 |
that comes from
|
|
|
724 |
\begin{center}
|
|
|
725 |
$(r_1 \backslash cc'c'' \cdot r^{\{n-3\}}* +
|
|
|
726 |
r \backslash c''\cdot r^{\{n-1\}}) +
|
|
|
727 |
(r \backslash c'c'' \cdot r^{\{n-2\}}* +
|
|
|
728 |
r \backslash c'' \cdot r^{\{n-1\}}*)+ \ldots$
|
|
|
729 |
\end{center}
|
|
|
730 |
are made of sequences with different tails, where the counters
|
|
|
731 |
might differ.
|
|
|
732 |
The observation for maintaining the bound is that
|
|
|
733 |
these counters never exceed $n$, the original
|
|
|
734 |
counter. With the number of counters staying finite,
|
|
|
735 |
$\rDistinct$ will deduplicate and keep the list finite.
|
|
|
736 |
We introduce this idea as a lemma once we describe all
|
|
|
737 |
the necessary helper functions.
|
|
|
738 |
|
|
|
739 |
Similar to the star case, we want
|
|
|
740 |
\begin{center}
|
|
|
741 |
$\rderssimp{r^{\{n\}}}{s} = \rsimp{\sum rs}$.
|
|
|
742 |
\end{center}
|
|
|
743 |
where $rs$
|
|
|
744 |
shall be in the form of
|
|
|
745 |
$\map \; f \; Ss$, where $f$ is a function and
|
|
|
746 |
$Ss$ a list of objects to act on.
|
|
|
747 |
For star, the object's datatype is string.
|
|
|
748 |
The list of strings $Ss$
|
|
|
749 |
is generated using functions
|
|
|
750 |
$\starupdate$ and $\starupdates$.
|
|
|
751 |
The function that takes a string and returns a regular expression
|
|
|
752 |
is the anonymous function $
|
|
|
753 |
(\lambda s'. \; r\backslash s' \cdot r^{\{m\}})$.
|
|
|
754 |
In the NTIMES setting,
|
|
|
755 |
the $\starupdate$ and $\starupdates$ functions are replaced by
|
|
|
756 |
$\textit{nupdate}$ and $\textit{nupdates}$:
|
|
|
757 |
\begin{center}
|
|
|
758 |
\begin{tabular}{lcl}
|
|
|
759 |
$\nupdate \; c \; r \; [] $ & $\dn$ & $[]$\\
|
|
|
760 |
$\nupdate \; c \; r \;
|
|
|
761 |
(\Some \; (s, \; n + 1) \; :: \; Ss)$ & $\dn$ & %\\
|
|
|
762 |
$\textit{if} \;
|
|
|
763 |
(\rnullable \; (r \backslash_{rs} s))$ \\
|
|
|
764 |
& & $\;\;\textit{then}
|
|
|
765 |
\;\; \Some \; (s @ [c], n + 1) :: \Some \; ([c], n) :: (
|
|
|
766 |
\nupdate \; c \; r \; Ss)$ \\
|
|
|
767 |
& & $\textit{else} \;\; \Some \; (s @ [c], n+1) :: (
|
|
|
768 |
\nupdate \; c \; r \; Ss)$\\
|
|
|
769 |
$\nupdate \; c \; r \; (\textit{None} :: Ss)$ & $\dn$ &
|
|
|
770 |
$(\None :: \nupdate \; c \; r \; Ss)$\\
|
|
|
771 |
& & \\
|
|
|
772 |
%\end{tabular}
|
|
|
773 |
%\end{center}
|
|
|
774 |
%\begin{center}
|
|
|
775 |
%\begin{tabular}{lcl}
|
|
|
776 |
$\nupdates \; [] \; r \; Ss$ & $\dn$ & $Ss$\\
|
|
|
777 |
$\nupdates \; (c :: cs) \; r \; Ss$ & $\dn$ & $\nupdates \; cs \; r \; (
|
|
|
778 |
\nupdate \; c \; r \; Ss)$
|
|
|
779 |
\end{tabular}
|
|
|
780 |
\end{center}
|
|
|
781 |
\noindent
|
|
|
782 |
which take into account when a subterm
|
|
|
783 |
\begin{center}
|
|
|
784 |
$r \backslash_s s \cdot r^{\{n\}}$
|
|
|
785 |
\end{center}
|
|
|
786 |
counter $n$
|
|
|
787 |
is 0, and therefore expands to
|
|
|
788 |
\begin{center}
|
|
|
789 |
$r \backslash_s (s@[c]) \cdot r^{\{n\}} \;+
|
|
|
790 |
\; \ZERO$
|
|
|
791 |
\end{center}
|
|
|
792 |
after taking a derivative.
|
|
|
793 |
The object now has type
|
|
|
794 |
\begin{center}
|
|
|
795 |
$\textit{option} \;(\textit{string}, \textit{nat})$
|
|
|
796 |
\end{center}
|
|
|
797 |
and therefore the function for converting such an option into
|
|
|
798 |
a regular expression term is called $\opterm$:
|
|
|
799 |
|
|
|
800 |
\begin{center}
|
|
|
801 |
\begin{tabular}{lcl}
|
|
|
802 |
$\opterm \; r \; SN$ & $\dn$ & $\textit{case} \; SN\; of$\\
|
|
|
803 |
& & $\;\;\Some \; (s, n) \Rightarrow
|
|
|
804 |
(r\backslash_{rs} s)\cdot r^{\{n\}}$\\
|
|
|
805 |
& & $\;\;\None \Rightarrow
|
|
|
806 |
\ZERO$\\
|
|
|
807 |
\end{tabular}
|
|
|
808 |
\end{center}
|
|
|
809 |
\noindent
|
|
|
810 |
Put together, the list $\map \; f \; Ss$ is instantiated as
|
|
|
811 |
\begin{center}
|
|
|
812 |
$\map \; (\opterm \; r) \; (\nupdates \; s \; r \;
|
|
|
813 |
[\Some \; ([c], n)])$.
|
|
|
814 |
\end{center}
|
|
|
815 |
For the closed form to be bounded, we would like
|
|
|
816 |
simplification to be applied to each term in the list.
|
|
|
817 |
Therefore we introduce some variants of $\opterm$,
|
|
|
818 |
which help conveniently express the rewriting steps
|
|
|
819 |
needed in the closed form proof.
|
|
|
820 |
\begin{center}
|
|
|
821 |
\begin{tabular}{lcl}
|
|
|
822 |
$\optermOsimp \; r \; SN$ & $\dn$ & $\textit{case} \; SN\; of$\\
|
|
|
823 |
& & $\;\;\Some \; (s, n) \Rightarrow
|
|
|
824 |
\textit{rsimp} \; ((r\backslash_{rs} s)\cdot r^{\{n\}})$\\
|
|
|
825 |
& & $\;\;\None \Rightarrow
|
|
|
826 |
\ZERO$\\
|
|
|
827 |
\\
|
|
|
828 |
$\optermosimp \; r \; SN$ & $\dn$ & $\textit{case} \; SN\; of$\\
|
|
|
829 |
& & $\;\;\Some \; (s, n) \Rightarrow
|
|
|
830 |
(\textit{rsimp} \; (r\backslash_{rs} s))
|
|
|
831 |
\cdot r^{\{n\}}$\\
|
|
|
832 |
& & $\;\;\None \Rightarrow
|
|
|
833 |
\ZERO$\\
|
|
|
834 |
\\
|
|
|
835 |
$\optermsimp \; r \; SN$ & $\dn$ & $\textit{case} \; SN\; of$\\
|
|
|
836 |
& & $\;\;\Some \; (s, n) \Rightarrow
|
|
|
837 |
(r\backslash_{rsimps} s)\cdot r^{\{n\}}$\\
|
|
|
838 |
& & $\;\;\None \Rightarrow
|
|
|
839 |
\ZERO$\\
|
|
|
840 |
\end{tabular}
|
|
|
841 |
\end{center}
|
|
|
842 |
|
|
|
843 |
|
|
|
844 |
For a list of
|
|
|
845 |
$\textit{option} \;(\textit{string}, \textit{nat})$ elements,
|
|
|
846 |
we define the highest power for it recursively:
|
|
|
847 |
\begin{center}
|
|
|
848 |
\begin{tabular}{lcl}
|
|
|
849 |
$\hpa \; [] \; n $ & $\dn$ & $n$\\
|
|
|
850 |
$\hpa \; (\None :: os) \; n $ & $\dn$ & $\hpa \; os \; n$\\
|
|
|
851 |
$\hpa \; (\Some \; (s, n) :: os) \; m$ & $\dn$ &
|
|
|
852 |
$\hpa \;os \; (\textit{max} \; n\; m)$\\
|
|
|
853 |
\\
|
|
|
854 |
$\hpower \; rs $ & $\dn$ & $\hpa \; rs \; 0$\\
|
|
|
855 |
\end{tabular}
|
|
|
856 |
\end{center}
|
|
|
857 |
|
|
|
858 |
Now the intuition that an NTIMES regular expression's power
|
|
|
859 |
does not increase can be easily expressed as
|
|
|
860 |
\begin{lemma}\label{nupdatesMono2}
|
|
|
861 |
$\hpower \; (\nupdates \;s \; r \; [\Some \; ([c], n)]) \leq n$
|
|
|
862 |
\end{lemma}
|
|
|
863 |
\begin{proof}
|
|
|
864 |
Note that the power is non-increasing after a $\nupdate$ application:
|
|
|
865 |
\begin{center}
|
|
|
866 |
$\hpa \;\; (\nupdate \; c \; r \; Ss)\;\; m \leq
|
|
|
867 |
\hpa\; \; Ss \; m$.
|
|
|
868 |
\end{center}
|
|
|
869 |
This is also the case for $\nupdates$:
|
|
|
870 |
\begin{center}
|
|
|
871 |
$\hpa \;\; (\nupdates \; s \; r \; Ss)\;\; m \leq
|
|
|
872 |
\hpa\; \; Ss \; m$.
|
|
|
873 |
\end{center}
|
|
|
874 |
Therefore we have that
|
|
|
875 |
\begin{center}
|
|
|
876 |
$\hpower \;\; (\nupdates \; s \; r \; Ss) \leq
|
|
|
877 |
\hpower \;\; Ss$
|
|
|
878 |
\end{center}
|
|
|
879 |
which leads to the lemma being proven.
|
|
|
880 |
|
|
|
881 |
\end{proof}
|
|
|
882 |
|
|
|
883 |
|
|
|
884 |
We also define the inductive rules for
|
|
|
885 |
the shape of derivatives of the NTIMES regular expressions:\\[-3em]
|
|
|
886 |
\begin{center}
|
|
|
887 |
\begin{mathpar}
|
|
|
888 |
\inferrule{\mbox{}}{\cbn \;\ZERO}
|
|
|
889 |
|
|
|
890 |
\inferrule{\mbox{}}{\cbn \; \; r_a \cdot (r^{\{n\}})}
|
|
|
891 |
|
|
|
892 |
\inferrule{\cbn \; r_1 \;\; \; \cbn \; r_2}{\cbn \; r_1 + r_2}
|
|
|
893 |
|
|
|
894 |
\inferrule{\cbn \; r}{\cbn \; r + \ZERO}
|
|
|
895 |
\end{mathpar}
|
|
|
896 |
\end{center}
|
|
|
897 |
\noindent
|
|
|
898 |
A derivative of NTIMES fits into the shape described by $\cbn$:
|
|
|
899 |
\begin{lemma}\label{ntimesDersCbn}
|
|
|
900 |
$\cbn \; ((r' \cdot r^{\{n\}}) \backslash_{rs} s)$ holds.
|
|
|
901 |
\end{lemma}
|
|
|
902 |
\begin{proof}
|
|
|
903 |
By a reverse induction on $s$.
|
|
|
904 |
For the inductive case, note that if $\cbn \; r$ holds,
|
|
|
905 |
then $\cbn \; (r\backslash_r c)$ holds.
|
|
|
906 |
\end{proof}
|
|
621
|
907 |
\noindent
|
|
620
|
908 |
In addition, for $\cbn$-shaped regular expressioins, one can flatten
|
|
|
909 |
them:
|
|
|
910 |
\begin{lemma}\label{ntimesHfauPushin}
|
|
|
911 |
If $\cbn \; r$ holds, then $\hflataux{r \backslash_r c} =
|
|
|
912 |
\textit{concat} \; (\map \; \hflataux{\map \; (\_\backslash_r c) \;
|
|
|
913 |
(\hflataux{r})})$
|
|
|
914 |
\end{lemma}
|
|
|
915 |
\begin{proof}
|
|
|
916 |
By an induction on the inductive cases of $\cbn$.
|
|
|
917 |
\end{proof}
|
|
621
|
918 |
\noindent
|
|
620
|
919 |
This time we do not need to define the flattening functions for NTIMES only,
|
|
621
|
920 |
because $\hflat{\_}$ and $\hflataux{\_}$ work on NTIMES already.
|
|
620
|
921 |
\begin{lemma}\label{ntimesHfauInduct}
|
|
|
922 |
$\hflataux{( (r\backslash_r c) \cdot r^{\{n\}}) \backslash_{rsimps} s} =
|
|
|
923 |
\map \; (\opterm \; r) \; (\nupdates \; s \; r \; [\Some \; ([c], n)])$
|
|
|
924 |
\end{lemma}
|
|
|
925 |
\begin{proof}
|
|
|
926 |
By a reverse induction on $s$.
|
|
621
|
927 |
The lemmas \ref{ntimesHfauPushin} and \ref{ntimesDersCbn} are used.
|
|
620
|
928 |
\end{proof}
|
|
|
929 |
\noindent
|
|
|
930 |
We have a recursive property for NTIMES with $\nupdate$
|
|
|
931 |
similar to that for STAR,
|
|
|
932 |
and one for $\nupdates $ as well:
|
|
|
933 |
\begin{lemma}\label{nupdateInduct1}
|
|
621
|
934 |
\mbox{}
|
|
|
935 |
\begin{itemize}
|
|
|
936 |
\item
|
|
|
937 |
\begin{center}
|
|
|
938 |
$\textit{concat} \; (\map \; (\hflataux{\_} \circ (
|
|
620
|
939 |
\opterm \; r)) \; Ss) = \map \; (\opterm \; r) \; (\nupdate \;
|
|
|
940 |
c \; r \; Ss)$\\
|
|
621
|
941 |
\end{center}
|
|
|
942 |
holds.
|
|
|
943 |
\item
|
|
|
944 |
\begin{center}
|
|
|
945 |
$\textit{concat} \; (\map \; \hflataux{\_}\;
|
|
620
|
946 |
\map \; (\_\backslash_r x) \;
|
|
621
|
947 |
(\map \; (\opterm \; r) \; (\nupdates \; xs \; r \; Ss)))$\\
|
|
|
948 |
$=$\\
|
|
|
949 |
$\map \; (\opterm \; r) \; (\nupdates \;(xs@[x]) \; r\;Ss)$
|
|
|
950 |
\end{center}
|
|
|
951 |
holds.
|
|
|
952 |
\end{itemize}
|
|
620
|
953 |
\end{lemma}
|
|
|
954 |
\begin{proof}
|
|
|
955 |
(i) is by an induction on $Ss$.
|
|
|
956 |
(ii) is by an induction on $xs$.
|
|
|
957 |
\end{proof}
|
|
621
|
958 |
\noindent
|
|
620
|
959 |
The $\nString$ predicate is defined for conveniently
|
|
|
960 |
expressing that there are no empty strings in the
|
|
|
961 |
$\Some \;(s, n)$ elements generated by $\nupdate$:
|
|
|
962 |
\begin{center}
|
|
|
963 |
\begin{tabular}{lcl}
|
|
|
964 |
$\nString \; \None$ & $\dn$ & $ \textit{true}$\\
|
|
|
965 |
$\nString \; (\Some \; ([], n))$ & $\dn$ & $ \textit{false}$\\
|
|
|
966 |
$\nString \; (\Some \; (c::s, n))$ & $\dn$ & $ \textit{true}$\\
|
|
|
967 |
\end{tabular}
|
|
|
968 |
\end{center}
|
|
|
969 |
\begin{lemma}\label{nupdatesNonempty}
|
|
621
|
970 |
If for all elements $o \in \textit{set} \; Ss$,
|
|
|
971 |
$\nString \; o$ holds, the we have that
|
|
|
972 |
for all elements $o' \in \textit{set} \; (\nupdates \; s \; r \; Ss)$,
|
|
|
973 |
$\nString \; o'$ holds.
|
|
620
|
974 |
\end{lemma}
|
|
|
975 |
\begin{proof}
|
|
|
976 |
By an induction on $s$, where $Ss$ is set to vary over all possible values.
|
|
|
977 |
\end{proof}
|
|
|
978 |
|
|
|
979 |
\noindent
|
|
|
980 |
|
|
|
981 |
\begin{lemma}\label{ntimesClosedFormsSteps}
|
|
|
982 |
The following list of equalities or rewriting relations hold:\\
|
|
|
983 |
(i) $r^{\{n+1\}} \backslash_{rsimps} (c::s) =
|
|
|
984 |
\textit{rsimp} \; (\sum (\map \; (\opterm \;r \;\_) \; (\nupdates \;
|
|
|
985 |
s \; r \; [\Some \; ([c], n)])))$\\
|
|
|
986 |
(ii)
|
|
|
987 |
\begin{center}
|
|
|
988 |
$\sum (\map \; (\opterm \; r) \; (\nupdates \; s \; r \; [
|
|
|
989 |
\Some \; ([c], n)]))$ \\ $ \sequal$\\
|
|
|
990 |
$\sum (\map \; (\textit{rsimp} \circ (\opterm \; r))\; (\nupdates \;
|
|
|
991 |
s\;r \; [\Some \; ([c], n)]))$\\
|
|
|
992 |
\end{center}
|
|
|
993 |
(iii)
|
|
|
994 |
\begin{center}
|
|
|
995 |
$\sum \;(\map \; (\optermosimp \; r) \; (\nupdates \; s \; r\; [\Some \;
|
|
|
996 |
([c], n)]))$\\
|
|
|
997 |
$\sequal$\\
|
|
|
998 |
$\sum \;(\map \; (\optermsimp r) \; (\nupdates \; s \; r \; [\Some \;
|
|
|
999 |
([c], n)])) $\\
|
|
|
1000 |
\end{center}
|
|
|
1001 |
(iv)
|
|
|
1002 |
\begin{center}
|
|
|
1003 |
$\sum \;(\map \; (\optermosimp \; r) \; (\nupdates \; s \; r\; [\Some \;
|
|
|
1004 |
([c], n)])) $ \\ $\sequal$\\
|
|
|
1005 |
$\sum \;(\map \; (\optermOsimp r) \; (\nupdates \; s \; r \; [\Some \;
|
|
|
1006 |
([c], n)])) $\\
|
|
|
1007 |
\end{center}
|
|
|
1008 |
(v)
|
|
|
1009 |
\begin{center}
|
|
|
1010 |
$\sum \;(\map \; (\optermOsimp r) \; (\nupdates \; s \; r \; [\Some \;
|
|
|
1011 |
([c], n)])) $ \\ $\sequal$\\
|
|
|
1012 |
$\sum \; (\map \; (\textit{rsimp} \circ (\opterm \; r)) \;
|
|
|
1013 |
(\nupdates \; s \; r \; [\Some \; ([c], n)]))$
|
|
|
1014 |
\end{center}
|
|
|
1015 |
\end{lemma}
|
|
|
1016 |
\begin{proof}
|
|
|
1017 |
Routine.
|
|
|
1018 |
(iii) and (iv) make use of the fact that all the strings $s$
|
|
|
1019 |
inside $\Some \; (s, m)$ which are elements of the list
|
|
|
1020 |
$\nupdates \; s\;r\;[\Some\; ([c], n)]$ are non-empty,
|
|
|
1021 |
which is from lemma \ref{nupdatesNonempty}.
|
|
|
1022 |
Once the string in $o = \Some \; (s, n)$ is
|
|
|
1023 |
nonempty, $\optermsimp \; r \;o$,
|
|
|
1024 |
$\optermosimp \; r \; o$ and $\optermosimp \; \; o$ are guaranteed
|
|
|
1025 |
to be equal.
|
|
621
|
1026 |
(v) uses \ref{nupdateInduct1}.
|
|
620
|
1027 |
\end{proof}
|
|
621
|
1028 |
\noindent
|
|
|
1029 |
Now we are ready to present the closed form for NTIMES:
|
|
620
|
1030 |
\begin{theorem}\label{ntimesClosedForm}
|
|
|
1031 |
The derivative of $r^{\{n+1\}}$ can be described as an alternative
|
|
|
1032 |
containing a list
|
|
|
1033 |
of terms:\\
|
|
|
1034 |
$r^{\{n+1\}} \backslash_{rsimps} (c::s) = \textit{rsimp} \; (
|
|
|
1035 |
\sum (\map \; (\optermsimp \; r) \; (\nupdates \; s \; r \;
|
|
|
1036 |
[\Some \; ([c], n)])))$
|
|
|
1037 |
\end{theorem}
|
|
|
1038 |
\begin{proof}
|
|
|
1039 |
By the rewriting steps described in lemma \ref{ntimesClosedFormsSteps}.
|
|
|
1040 |
\end{proof}
|
|
621
|
1041 |
\noindent
|
|
|
1042 |
The key observation for bounding this closed form
|
|
|
1043 |
is that the counter on $r^{\{n\}}$ will
|
|
|
1044 |
only decrement during derivatives:
|
|
620
|
1045 |
\begin{lemma}\label{nupdatesNLeqN}
|
|
|
1046 |
For an element $o$ in $\textit{set} \; (\nupdates \; s \; r \;
|
|
|
1047 |
[\Some \; ([c], n)])$, either $o = \None$, or $o = \Some
|
|
|
1048 |
\; (s', m)$ for some string $s'$ and number $m \leq n$.
|
|
|
1049 |
\end{lemma}
|
|
621
|
1050 |
\noindent
|
|
|
1051 |
The proof is routine and therefore omitted.
|
|
|
1052 |
This allows us to say what kind of terms
|
|
|
1053 |
are in the list $\textit{set} \; (\map \; (\optermsimp \; r) \; (
|
|
|
1054 |
\nupdates \; s \; r \; [\Some \; ([c], n)]))$:
|
|
|
1055 |
only $\ZERO_r$s or a sequence with the tail an $r^{\{m\}}$
|
|
|
1056 |
with a small $m$:
|
|
620
|
1057 |
\begin{lemma}\label{ntimesClosedFormListElemShape}
|
|
|
1058 |
For any element $r'$ in $\textit{set} \; (\map \; (\optermsimp \; r) \; (
|
|
|
1059 |
\nupdates \; s \; r \; [\Some \; ([c], n)]))$,
|
|
|
1060 |
we have that $r'$ is either $\ZERO$ or $r \backslash_{rsimps} s' \cdot
|
|
|
1061 |
r^{\{m\}}$ for some string $s'$ and number $m \leq n$.
|
|
|
1062 |
\end{lemma}
|
|
|
1063 |
\begin{proof}
|
|
|
1064 |
Using lemma \ref{nupdatesNLeqN}.
|
|
|
1065 |
\end{proof}
|
|
|
1066 |
|
|
|
1067 |
\begin{theorem}\label{ntimesClosedFormBounded}
|
|
|
1068 |
Assuming that for any string $s$, $\llbracket r \backslash_{rsimps} s
|
|
|
1069 |
\rrbracket_r \leq N$ holds, then we have that\\
|
|
|
1070 |
$\llbracket r^{\{n+1\}} \backslash_{rsimps} s \rrbracket_r \leq
|
|
|
1071 |
\textit{max} \; (c_N+1)* (N + \llbracket r^{\{n\}} \rrbracket+1)$,
|
|
|
1072 |
where $c_N = \textit{card} \; (\textit{sizeNregex} \; (
|
|
|
1073 |
N + \llbracket r^{\{n\}} \rrbracket_r+1))$.
|
|
|
1074 |
\end{theorem}
|
|
|
1075 |
\begin{proof}
|
|
|
1076 |
We have that for all regular expressions $r'$ in $\textit{set} \; (\map \; (\optermsimp \; r) \; (
|
|
|
1077 |
\nupdates \; s \; r \; [\Some \; ([c], n)]))$,
|
|
|
1078 |
$r'$'s size is less than or equal to $N + \llbracket r^{\{n\}}
|
|
|
1079 |
\rrbracket_r + 1$
|
|
|
1080 |
because $r'$ can only be either a $\ZERO$ or $r \backslash_{rsimps} s' \cdot
|
|
|
1081 |
r^{\{m\}}$ for some string $s'$ and number
|
|
|
1082 |
$m \leq n$ (lemma \ref{ntimesClosedFormListElemShape}).
|
|
|
1083 |
In addition, we know that the list
|
|
|
1084 |
$\map \; (\optermsimp \; r) \; (
|
|
|
1085 |
\nupdates \; s \; r \; [\Some \; ([c], n)])$'s size is at most
|
|
|
1086 |
$c_N = \textit{card} \;
|
|
|
1087 |
(\sizeNregex \; ((N + \llbracket r^{\{n\}} \rrbracket) + 1))$.
|
|
621
|
1088 |
This gives us $\llbracket r \backslash_{rsimps} \;s \rrbracket_r
|
|
620
|
1089 |
\leq N * c_N$.
|
|
|
1090 |
\end{proof}
|
|
|
1091 |
|
|
621
|
1092 |
We aim to formalise the correctness and size bound
|
|
|
1093 |
for constructs like $r^{\{\ldots n\}}$, $r^{\{n \ldots\}}$
|
|
|
1094 |
and so on, which is still work in progress.
|
|
|
1095 |
They should more or less follow the same recipe described in this section.
|
|
|
1096 |
Once we know about how to deal with them recursively using suitable auxiliary
|
|
|
1097 |
definitions, we are able to routinely establish the proofs.
|
|
620
|
1098 |
|
|
|
1099 |
|
|
621
|
1100 |
%The closed form for them looks like:
|
|
|
1101 |
%%\begin{center}
|
|
|
1102 |
%% \begin{tabular}{llrclll}
|
|
|
1103 |
%% $r^{\{n+1\}}$ & $ \backslash_{rsimps}$ & $(c::s)$ & $=$ & & \\
|
|
|
1104 |
%% $\textit{rsimp}$ & $($ & $
|
|
|
1105 |
%% \sum \; ( $ & $\map$ & $(\textit{optermsimp}\;r)$ & $($\\
|
|
|
1106 |
%% & & & & $\textit{nupdates} \;$ &
|
|
|
1107 |
%% $ s \; r_0 \; [ \textit{Some} \; ([c], n)]$\\
|
|
|
1108 |
%% & & & & $)$ &\\
|
|
|
1109 |
%% & & $)$ & & &\\
|
|
|
1110 |
%% & $)$ & & & &\\
|
|
|
1111 |
%% \end{tabular}
|
|
|
1112 |
%%\end{center}
|
|
620
|
1113 |
%\begin{center}
|
|
621
|
1114 |
% \begin{tabular}{llrcllrllll}
|
|
|
1115 |
% $r^{\{n+1\}}$ & $ \backslash_{rsimps}$ & $(c::s)$ & $=$ & & &&&&\\
|
|
|
1116 |
% &&&&$\textit{rsimp}$ & $($ & $
|
|
|
1117 |
% \sum \; ( $ & $\map$ & $(\textit{optermsimp}\;r)$ & $($\\
|
|
|
1118 |
% &&&& & & & & $\;\; \textit{nupdates} \;$ &
|
|
|
1119 |
% $ s \; r_0 \; [ \textit{Some} \; ([c], n)]$\\
|
|
|
1120 |
% &&&& & & & & $)$ &\\
|
|
|
1121 |
% &&&& & & $)$ & & &\\
|
|
|
1122 |
% &&&& & $)$ & & & &\\
|
|
|
1123 |
% \end{tabular}
|
|
620
|
1124 |
%\end{center}
|
|
621
|
1125 |
%The $\textit{optermsimp}$ function with the argument $r$
|
|
|
1126 |
%chooses from two options: $\ZERO$ or
|
|
|
1127 |
%We define for the $r^{\{n\}}$ constructor something similar to $\starupdate$
|
|
|
1128 |
%and $\starupdates$:
|
|
620
|
1129 |
%\begin{center}
|
|
621
|
1130 |
% \begin{tabular}{lcl}
|
|
|
1131 |
% $\starupdate \; c \; r \; [] $ & $\dn$ & $[]$\\
|
|
|
1132 |
% $\starupdate \; c \; r \; (s :: Ss)$ & $\dn$ & \\
|
|
|
1133 |
% & & $\textit{if} \;
|
|
|
1134 |
% (\rnullable \; (\rders \; r \; s))$ \\
|
|
|
1135 |
% & & $\textit{then} \;\; (s @ [c]) :: [c] :: (
|
|
|
1136 |
% \starupdate \; c \; r \; Ss)$ \\
|
|
|
1137 |
% & & $\textit{else} \;\; (s @ [c]) :: (
|
|
|
1138 |
% \starupdate \; c \; r \; Ss)$
|
|
|
1139 |
% \end{tabular}
|
|
620
|
1140 |
%\end{center}
|
|
621
|
1141 |
%\noindent
|
|
|
1142 |
%As a generalisation from characters to strings,
|
|
|
1143 |
%$\starupdates$ takes a string instead of a character
|
|
|
1144 |
%as the first input argument, and is otherwise the same
|
|
|
1145 |
%as $\starupdate$.
|
|
|
1146 |
%\begin{center}
|
|
|
1147 |
% \begin{tabular}{lcl}
|
|
|
1148 |
% $\starupdates \; [] \; r \; Ss$ & $=$ & $Ss$\\
|
|
|
1149 |
% $\starupdates \; (c :: cs) \; r \; Ss$ & $=$ & $\starupdates \; cs \; r \; (
|
|
|
1150 |
% \starupdate \; c \; r \; Ss)$
|
|
|
1151 |
% \end{tabular}
|
|
|
1152 |
%\end{center}
|
|
|
1153 |
%\noindent
|
|
620
|
1154 |
|
|
|
1155 |
|
|
|
1156 |
|
|
621
|
1157 |
%\section{Zippers}
|
|
|
1158 |
%Zipper is a data structure designed to operate on
|
|
|
1159 |
%and navigate between local parts of a tree.
|
|
|
1160 |
%It was first formally described by Huet \cite{HuetZipper}.
|
|
|
1161 |
%Typical applications of zippers involve text editor buffers
|
|
|
1162 |
%and proof system databases.
|
|
|
1163 |
%In our setting, the idea is to compactify the representation
|
|
|
1164 |
%of derivatives with zippers, thereby making our algorithm faster.
|
|
|
1165 |
%Some initial results
|
|
|
1166 |
%We first give a brief introduction to what zippers are,
|
|
|
1167 |
%and other works
|
|
|
1168 |
%that apply zippers to derivatives
|
|
|
1169 |
%When dealing with large trees, it would be a waste to
|
|
|
1170 |
%traverse the entire tree if
|
|
|
1171 |
%the operation only
|
|
|
1172 |
%involves a small fraction of it.
|
|
|
1173 |
%The idea is to put the focus on that subtree, turning other parts
|
|
|
1174 |
%of the tree into a context
|
|
|
1175 |
%
|
|
|
1176 |
%
|
|
|
1177 |
%One observation about our derivative-based lexing algorithm is that
|
|
|
1178 |
%the derivative operation sometimes traverses the entire regular expression
|
|
|
1179 |
%unnecessarily:
|
|
620
|
1180 |
|
|
|
1181 |
|
|
612
|
1182 |
%----------------------------------------------------------------------------------------
|
|
|
1183 |
% SECTION 1
|
|
|
1184 |
%----------------------------------------------------------------------------------------
|
|
532
|
1185 |
|
|
612
|
1186 |
%\section{Adding Support for the Negation Construct, and its Correctness Proof}
|
|
|
1187 |
%We now add support for the negation regular expression:
|
|
|
1188 |
%\[ r ::= \ZERO \mid \ONE
|
|
|
1189 |
% \mid c
|
|
|
1190 |
% \mid r_1 \cdot r_2
|
|
|
1191 |
% \mid r_1 + r_2
|
|
|
1192 |
% \mid r^*
|
|
|
1193 |
% \mid \sim r
|
|
|
1194 |
%\]
|
|
|
1195 |
%The $\textit{nullable}$ function's clause for it would be
|
|
|
1196 |
%\[
|
|
|
1197 |
%\textit{nullable}(~r) = \neg \nullable(r)
|
|
|
1198 |
%\]
|
|
|
1199 |
%The derivative would be
|
|
|
1200 |
%\[
|
|
|
1201 |
%~r \backslash c = ~ (r \backslash c)
|
|
|
1202 |
%\]
|
|
|
1203 |
%
|
|
|
1204 |
%The most tricky part of lexing for the $~r$ regular expression
|
|
|
1205 |
% is creating a value for it.
|
|
|
1206 |
% For other regular expressions, the value aligns with the
|
|
|
1207 |
% structure of the regular expression:
|
|
|
1208 |
% \[
|
|
|
1209 |
% \vdash \Seq(\Char(a), \Char(b)) : a \cdot b
|
|
|
1210 |
% \]
|
|
|
1211 |
%But for the $~r$ regular expression, $s$ is a member of it if and only if
|
|
|
1212 |
%$s$ does not belong to $L(r)$.
|
|
|
1213 |
%That means when there
|
|
|
1214 |
%is a match for the not regular expression, it is not possible to generate how the string $s$ matched
|
|
|
1215 |
%with $r$.
|
|
|
1216 |
%What we can do is preserve the information of how $s$ was not matched by $r$,
|
|
|
1217 |
%and there are a number of options to do this.
|
|
|
1218 |
%
|
|
|
1219 |
%We could give a partial value when there is a partial match for the regular expression inside
|
|
|
1220 |
%the $\mathbf{not}$ construct.
|
|
|
1221 |
%For example, the string $ab$ is not in the language of $(a\cdot b) \cdot c$,
|
|
|
1222 |
%A value for it could be
|
|
|
1223 |
% \[
|
|
|
1224 |
% \vdash \textit{Not}(\Seq(\Char(a), \Char(b))) : ~((a \cdot b ) \cdot c)
|
|
|
1225 |
% \]
|
|
|
1226 |
% The above example demonstrates what value to construct
|
|
|
1227 |
% when the string $s$ is at most a real prefix
|
|
|
1228 |
% of the strings in $L(r)$. When $s$ instead is not a prefix of any strings
|
|
|
1229 |
% in $L(r)$, it becomes unclear what to return as a value inside the $\textit{Not}$
|
|
|
1230 |
% constructor.
|
|
|
1231 |
%
|
|
|
1232 |
% Another option would be to either store the string $s$ that resulted in
|
|
|
1233 |
% a mis-match for $r$ or a dummy value as a placeholder:
|
|
|
1234 |
% \[
|
|
|
1235 |
% \vdash \textit{Not}(abcd) : ~( r_1 )
|
|
|
1236 |
% \]
|
|
|
1237 |
%or
|
|
|
1238 |
% \[
|
|
|
1239 |
% \vdash \textit{Not}(\textit{Dummy}) : ~( r_1 )
|
|
|
1240 |
% \]
|
|
|
1241 |
% We choose to implement this as it is most straightforward:
|
|
|
1242 |
% \[
|
|
|
1243 |
% \mkeps(~(r)) = \textit{if}(\nullable(r)) \; \textit{Error} \; \textit{else} \; \textit{Not}(\textit{Dummy})
|
|
|
1244 |
% \]
|
|
|
1245 |
%
|
|
|
1246 |
%
|
|
620
|
1247 |
%\begin{center}
|
|
|
1248 |
% \begin{tabular}{lcl}
|
|
|
1249 |
% $\ntset \; r \; (n+1) \; c::cs $ & $\dn$ & $\nupdates \;
|
|
|
1250 |
% cs \; r \; [\Some \; ([c], n)]$\\
|
|
|
1251 |
% $\ntset \; r\; 0 \; \_$ & $\dn$ & $\None$\\
|
|
|
1252 |
% $\ntset \; r \; \_ \; [] $ & $ \dn$ & $[]$\\
|
|
|
1253 |
% \end{tabular}
|
|
|
1254 |
%\end{center}
|