|
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 |
|
|
625
|
11 |
This chapter is a ``work-in-progress''
|
|
|
12 |
chapter which records
|
|
|
13 |
extensions to our $\blexersimp$.
|
|
|
14 |
We intend to formalise this part, which
|
|
|
15 |
we have not been able to finish due to time constraints of the PhD.
|
|
|
16 |
Nevertheless, we outline the ideas we intend to use for the proof.
|
|
|
17 |
|
|
|
18 |
We present further improvements
|
|
628
|
19 |
for our lexer algorithm $\blexersimp$.
|
|
590
|
20 |
We devise a stronger simplification algorithm,
|
|
|
21 |
called $\bsimpStrong$, which can prune away
|
|
|
22 |
similar components in two regular expressions at the same
|
|
|
23 |
alternative level,
|
|
|
24 |
even if these regular expressions are not exactly the same.
|
|
|
25 |
We call the lexer that uses this stronger simplification function
|
|
|
26 |
$\blexerStrong$.
|
|
628
|
27 |
Unfortunately we did not have time to
|
|
|
28 |
work out the proofs, like in
|
|
|
29 |
the previous chapters.
|
|
590
|
30 |
We conjecture that both
|
|
|
31 |
\begin{center}
|
|
|
32 |
$\blexerStrong \;r \; s = \blexer\; r\;s$
|
|
|
33 |
\end{center}
|
|
|
34 |
and
|
|
|
35 |
\begin{center}
|
|
|
36 |
$\llbracket \bdersStrong{a}{s} \rrbracket = O(\llbracket a \rrbracket^3)$
|
|
|
37 |
\end{center}
|
|
628
|
38 |
hold, but a formalisation
|
|
|
39 |
is still future work.
|
|
|
40 |
We give an informal justification
|
|
|
41 |
why the correctness and cubic size bound proofs
|
|
|
42 |
can be achieved
|
|
590
|
43 |
by exploring the connection between the internal
|
|
|
44 |
data structure of our $\blexerStrong$ and
|
|
|
45 |
Animirov's partial derivatives.\\
|
|
621
|
46 |
%We also present the idempotency property proof
|
|
620
|
47 |
%of $\bsimp$, which leverages the idempotency proof of $\rsimp$.
|
|
|
48 |
%This reinforces our claim that the fixpoint construction
|
|
|
49 |
%originally required by Sulzmann and Lu can be removed in $\blexersimp$.
|
|
621
|
50 |
|
|
|
51 |
%Last but not least, we present our efforts and challenges we met
|
|
|
52 |
%in further improving the algorithm by data
|
|
|
53 |
%structures such as zippers.
|
|
590
|
54 |
|
|
|
55 |
|
|
|
56 |
|
|
532
|
57 |
%----------------------------------------------------------------------------------------
|
|
|
58 |
% SECTION strongsimp
|
|
|
59 |
%----------------------------------------------------------------------------------------
|
|
|
60 |
\section{A Stronger Version of Simplification}
|
|
|
61 |
%TODO: search for isabelle proofs of algorithms that check equivalence
|
|
590
|
62 |
In our bitcoded lexing algorithm, (sub)terms represent (sub)matches.
|
|
591
|
63 |
For example, the regular expression
|
|
|
64 |
\[
|
|
|
65 |
aa \cdot a^*+ a \cdot a^* + aa\cdot a^*
|
|
|
66 |
\]
|
|
|
67 |
contains three terms,
|
|
628
|
68 |
expressing three possibilities for how it can match some input.
|
|
591
|
69 |
The first and the third terms are identical, which means we can eliminate
|
|
628
|
70 |
the latter as it will not contribute to a POSIX value.
|
|
|
71 |
In $\bsimps$, the $\distinctBy$ function takes care of
|
|
|
72 |
such instances.
|
|
591
|
73 |
The criteria $\distinctBy$ uses for removing a duplicate
|
|
|
74 |
$a_2$ in the list
|
|
|
75 |
\begin{center}
|
|
|
76 |
$rs_a@[a_1]@rs_b@[a_2]@rs_c$
|
|
|
77 |
\end{center}
|
|
|
78 |
is that
|
|
533
|
79 |
\begin{center}
|
|
591
|
80 |
$\rerase{a_1} = \rerase{a_2}$.
|
|
|
81 |
\end{center}
|
|
628
|
82 |
It is characterised as the $LD$
|
|
|
83 |
rewrite rule in figure \ref{rrewriteRules}.\\
|
|
591
|
84 |
The problem , however, is that identical components
|
|
628
|
85 |
in two slightly different regular expressions cannot be removed.
|
|
|
86 |
Consider the simplification
|
|
|
87 |
\begin{equation}
|
|
|
88 |
\label{eqn:partialDedup}
|
|
591
|
89 |
(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
|
|
628
|
90 |
\end{equation}
|
|
|
91 |
where the $(a+\ldots)\cdot r_1$ is deleted in the right alternative.
|
|
|
92 |
This is permissible because we have $(a+\ldots)\cdot r_1$ in the left
|
|
|
93 |
alternative.
|
|
|
94 |
The difficulty is that such ``buried''
|
|
|
95 |
alternatives-sequences are not easily recognised.
|
|
|
96 |
But simplification like this actually
|
|
591
|
97 |
cannot be omitted,
|
|
628
|
98 |
as without it the size of derivatives can still
|
|
|
99 |
blow up even with our $\textit{bsimp}$
|
|
|
100 |
function:
|
|
|
101 |
consider again the example
|
|
621
|
102 |
$\protect((a^* + (aa)^* + \ldots + (\underbrace{a\ldots a}_{n a's})^* )^*)^*$,
|
|
628
|
103 |
and set $n$ to a relatively small number,
|
|
|
104 |
we get exponential growth:
|
|
591
|
105 |
\begin{figure}[H]
|
|
|
106 |
\centering
|
|
|
107 |
\begin{tikzpicture}
|
|
|
108 |
\begin{axis}[
|
|
|
109 |
%xlabel={$n$},
|
|
|
110 |
myplotstyle,
|
|
|
111 |
xlabel={input length},
|
|
|
112 |
ylabel={size},
|
|
|
113 |
]
|
|
|
114 |
\addplot[blue,mark=*, mark options={fill=white}] table {bsimpExponential.data};
|
|
|
115 |
\end{axis}
|
|
533
|
116 |
\end{tikzpicture}
|
|
628
|
117 |
\caption{Size of derivatives of $\blexersimp$ for matching
|
|
591
|
118 |
$\protect((a^* + (aa)^* + \ldots + (aaaaa)^* )^*)^*$
|
|
|
119 |
with strings
|
|
|
120 |
of the form $\protect\underbrace{aa..a}_{n}$.}\label{blexerExp}
|
|
|
121 |
\end{figure}
|
|
|
122 |
\noindent
|
|
628
|
123 |
One possible approach would be to apply the rewriting
|
|
|
124 |
rule
|
|
591
|
125 |
\[
|
|
|
126 |
(a+b+d) \cdot r_1 \longrightarrow a \cdot r_1 + b \cdot r_1 + d \cdot r_1
|
|
|
127 |
\]
|
|
533
|
128 |
\noindent
|
|
591
|
129 |
in our $\simp$ function,
|
|
628
|
130 |
so that it makes the simplification in \eqref{eqn:partialDedup} possible.
|
|
621
|
131 |
Translating the rule into our $\textit{bsimp}$ function simply
|
|
|
132 |
involves adding a new clause to the $\textit{bsimp}_{ASEQ}$ function:
|
|
|
133 |
\begin{center}
|
|
|
134 |
\begin{tabular}{@{}lcl@{}}
|
|
|
135 |
$\textit{bsimp}_{ASEQ} \; bs\; a \; b$ & $\dn$ & $ (a,\; b) \textit{match}$\\
|
|
|
136 |
&& $\ldots$\\
|
|
|
137 |
&&$\quad\textit{case} \; (_{bs1}\sum as, a_2') \Rightarrow _{bs1}\sum (
|
|
|
138 |
\map \; (_{[]}\textit{ASEQ} \; \_ \; a_2') \; as)$\\
|
|
|
139 |
&&$\quad\textit{case} \; (a_1', a_2') \Rightarrow _{bs}a_1' \cdot a_2'$ \\
|
|
|
140 |
\end{tabular}
|
|
|
141 |
\end{center}
|
|
628
|
142 |
\noindent
|
|
591
|
143 |
Unfortunately,
|
|
|
144 |
if we introduce them in our
|
|
|
145 |
setting we would lose the POSIX property of our calculated values.
|
|
|
146 |
For example given the regular expression
|
|
|
147 |
\begin{center}
|
|
|
148 |
$(a + ab)(bc + c)$
|
|
|
149 |
\end{center}
|
|
628
|
150 |
and the string $ab$,
|
|
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
|
|
628
|
171 |
quite different structure--the original
|
|
591
|
172 |
was a sequence, and now it becomes an alternative.
|
|
628
|
173 |
With an alternative the maximal munch rule no longer works.\\
|
|
591
|
174 |
A method to reconcile this is to do the
|
|
628
|
175 |
transformation in \eqref{eqn:partialDedup} ``non-invasively'',
|
|
591
|
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:
|
|
628
|
187 |
\begin{figure}[H]
|
|
|
188 |
\begin{mathpar}
|
|
621
|
189 |
\inferrule * [Right = cubicRule]{\vspace{0mm} }{rs_a@[a]@rs_c
|
|
591
|
190 |
\stackrel{s}{\rightsquigarrow }
|
|
|
191 |
rs_a@[\textit{prune} \; a \; rs_a]@rs_c }
|
|
592
|
192 |
\end{mathpar}
|
|
628
|
193 |
\caption{The rule capturing the pruning simplification needed to achieve
|
|
|
194 |
a cubic bound}
|
|
|
195 |
\label{fig:cubicRule}
|
|
|
196 |
\end{figure}
|
|
591
|
197 |
%L \; a_1' = L \; a_1 \setminus (\cup_{a \in rs_a} L \; a)
|
|
|
198 |
where $\textit{prune} \;a \; acc$ traverses $a$
|
|
|
199 |
without altering the structure of $a$, removing components in $a$
|
|
|
200 |
that have appeared in the accumulator $acc$.
|
|
|
201 |
For example
|
|
|
202 |
\begin{center}
|
|
|
203 |
$\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] $
|
|
|
204 |
\end{center}
|
|
|
205 |
should be equal to
|
|
|
206 |
\begin{center}
|
|
|
207 |
$(r_g+r_h)r_d$
|
|
|
208 |
\end{center}
|
|
|
209 |
because $r_gr_d$ and
|
|
|
210 |
$r_hr_d$ are the only terms
|
|
|
211 |
that have not appeared in the accumulator list
|
|
|
212 |
\begin{center}
|
|
|
213 |
$[(r_a+r_b+r_c)r_d, (r_e+r_f)r_d]$.
|
|
|
214 |
\end{center}
|
|
|
215 |
We implemented
|
|
628
|
216 |
function $\textit{prune}$ in Scala:
|
|
590
|
217 |
\begin{figure}[H]
|
|
591
|
218 |
\begin{lstlisting}
|
|
|
219 |
def prune(r: ARexp, acc: Set[Rexp]) : ARexp = r match{
|
|
628
|
220 |
case AALTS(bs, rs) => rs.map(r => prune(r, acc)).filter(_ != AZERO) match
|
|
591
|
221 |
{
|
|
|
222 |
//all components have been removed, meaning this is effectively a duplicate
|
|
|
223 |
//flats will take care of removing this AZERO
|
|
|
224 |
case Nil => AZERO
|
|
|
225 |
case r::Nil => fuse(bs, r)
|
|
|
226 |
case rs1 => AALTS(bs, rs1)
|
|
|
227 |
}
|
|
|
228 |
case ASEQ(bs, r1, r2) =>
|
|
|
229 |
//remove the r2 in (ra + rb)r2 to identify the duplicate contents of r1
|
|
|
230 |
prune(r1, acc.map(r => removeSeqTail(r, erase(r2)))) match {
|
|
|
231 |
//after pruning, returns 0
|
|
|
232 |
case AZERO => AZERO
|
|
|
233 |
//after pruning, got r1'.r2, where r1' is equal to 1
|
|
|
234 |
case r1p if(isOne(erase(r1p))) => fuse(bs ++ mkepsBC(r1p), r2)
|
|
|
235 |
//assemble the pruned head r1p with r2
|
|
|
236 |
case r1p => ASEQ(bs, r1p, r2)
|
|
|
237 |
}
|
|
|
238 |
//this does the duplicate component removal task
|
|
|
239 |
case r => if(acc(erase(r))) AZERO else r
|
|
|
240 |
}
|
|
|
241 |
\end{lstlisting}
|
|
628
|
242 |
\caption{The function $\textit{prune}$ }
|
|
591
|
243 |
\end{figure}
|
|
|
244 |
\noindent
|
|
628
|
245 |
The function $\textit{prune}$
|
|
|
246 |
is a stronger version of $\textit{distinctBy}$.
|
|
|
247 |
It does not just walk through a list looking for exact duplicates,
|
|
|
248 |
but prunes sub-expressions recursively.
|
|
|
249 |
It manages proper contexts by the helper functions
|
|
|
250 |
$\textit{removeSeqTail}$, $\textit{isOne}$ and $\textit{atMostEmpty}$.
|
|
591
|
251 |
\begin{figure}[H]
|
|
|
252 |
\begin{lstlisting}
|
|
628
|
253 |
def atMostEmpty(r: Rexp) : Boolean = r match {
|
|
|
254 |
case ZERO => true
|
|
|
255 |
case ONE => true
|
|
|
256 |
case STAR(r) => atMostEmpty(r)
|
|
|
257 |
case SEQ(r1, r2) => atMostEmpty(r1) && atMostEmpty(r2)
|
|
|
258 |
case ALTS(r1, r2) => atMostEmpty(r1) && atMostEmpty(r2)
|
|
|
259 |
case CHAR(_) => false
|
|
|
260 |
}
|
|
|
261 |
|
|
|
262 |
def isOne(r: Rexp) : Boolean = r match {
|
|
|
263 |
case ONE => true
|
|
|
264 |
case SEQ(r1, r2) => isOne(r1) && isOne(r2)
|
|
|
265 |
case ALTS(r1, r2) => (isOne(r1) || isOne(r2)) && (atMostEmpty(r1) && atMostEmpty(r2))
|
|
|
266 |
case STAR(r0) => atMostEmpty(r0)
|
|
|
267 |
case CHAR(c) => false
|
|
|
268 |
case ZERO => false
|
|
|
269 |
}
|
|
|
270 |
|
|
|
271 |
def removeSeqTail(r: Rexp, tail: Rexp) : Rexp =
|
|
|
272 |
if (r == tail)
|
|
|
273 |
ONE
|
|
|
274 |
else {
|
|
|
275 |
r match {
|
|
|
276 |
case SEQ(r1, r2) =>
|
|
|
277 |
if(r2 == tail)
|
|
|
278 |
r1
|
|
|
279 |
else
|
|
|
280 |
ZERO
|
|
|
281 |
case r => ZERO
|
|
|
282 |
}
|
|
591
|
283 |
}
|
|
628
|
284 |
|
|
|
285 |
|
|
|
286 |
\end{lstlisting}
|
|
|
287 |
\caption{The helper functions of $\textit{prune}$}
|
|
|
288 |
\end{figure}
|
|
|
289 |
\noindent
|
|
|
290 |
Suppose we feed
|
|
|
291 |
\begin{center}
|
|
|
292 |
$r= (\underline{\ONE}+(\underline{f}+b)\cdot g)\cdot (a\cdot(d\cdot e))$
|
|
|
293 |
\end{center}
|
|
|
294 |
and
|
|
|
295 |
\begin{center}
|
|
|
296 |
$acc = \{a\cdot(d\cdot e),f\cdot (g \cdot (a \cdot (d \cdot e))) \}$
|
|
|
297 |
\end{center}
|
|
|
298 |
as the input for $\textit{prune}$.
|
|
|
299 |
The end result will be
|
|
|
300 |
\[
|
|
|
301 |
b\cdot(g\cdot(a\cdot(d\cdot e)))
|
|
|
302 |
\]
|
|
|
303 |
where the underlined components in $r$ are eliminated.
|
|
|
304 |
Looking more closely, at the topmost call
|
|
|
305 |
\[
|
|
|
306 |
\textit{prune} \quad (\ONE+
|
|
|
307 |
(f+b)\cdot g)\cdot (a\cdot(d\cdot e)) \quad
|
|
|
308 |
\{a\cdot(d\cdot e),f\cdot (g \cdot (a \cdot (d \cdot e))) \}
|
|
|
309 |
\]
|
|
|
310 |
The sequence clause will be called,
|
|
|
311 |
where a sub-call
|
|
|
312 |
\[
|
|
|
313 |
\textit{prune} \;\; (\ONE+(f+b)\cdot g)\;\; \{\ONE, f\cdot g \}
|
|
|
314 |
\]
|
|
|
315 |
is made. The terms in the new accumulator $\{\ONE,\; f\cdot g \}$ come from
|
|
|
316 |
the two calls to $\textit{removeSeqTail}$:
|
|
|
317 |
\[
|
|
|
318 |
\textit{removeSeqTail} \quad\;\; a \cdot(d\cdot e) \quad\;\; a \cdot(d\cdot e)
|
|
|
319 |
\]
|
|
|
320 |
and
|
|
|
321 |
\[
|
|
|
322 |
\textit{removeSeqTail} \quad \;\;
|
|
|
323 |
f\cdot(g\cdot (a \cdot(d\cdot e)))\quad \;\; a \cdot(d\cdot e).
|
|
|
324 |
\]
|
|
|
325 |
The idea behind $\textit{removeSeqTail}$ is that
|
|
|
326 |
when pruning recursively, we need to ``zoom in''
|
|
|
327 |
to sub-expressions, and this ``zoom in'' needs to be performed
|
|
|
328 |
on the
|
|
|
329 |
accumulators as well, otherwise we will be comparing
|
|
|
330 |
apples with oranges.
|
|
|
331 |
The sub-call
|
|
|
332 |
$\textit{prune} \;\; (\ONE+(f+b)\cdot g)\;\; \{\ONE, f\cdot g \}$
|
|
|
333 |
is simpler, which will trigger the alternative clause, causing
|
|
|
334 |
a pruning on each element in $(\ONE+(f+b)\cdot g)$,
|
|
|
335 |
leaving us $b\cdot g$ only.
|
|
|
336 |
|
|
|
337 |
Our new lexer with stronger simplification
|
|
|
338 |
uses $\textit{prune}$ by making it
|
|
|
339 |
the core component of the deduplicating function
|
|
|
340 |
called $\textit{distinctWith}$.
|
|
|
341 |
$\textit{DistinctWith}$ ensures that all verbose
|
|
|
342 |
parts of a regular expression are pruned away.
|
|
|
343 |
|
|
|
344 |
\begin{figure}[H]
|
|
|
345 |
\begin{lstlisting}
|
|
|
346 |
def turnIntoTerms(r: Rexp): List[Rexp] = r match {
|
|
|
347 |
case SEQ(r1, r2) =>
|
|
|
348 |
turnIntoTerms(r1).flatMap(r11 => furtherSEQ(r11, r2))
|
|
|
349 |
case ALTS(r1, r2) => turnIntoTerms(r1) ::: turnIntoTerms(r2)
|
|
|
350 |
case ZERO => Nil
|
|
|
351 |
case _ => r :: Nil
|
|
|
352 |
}
|
|
|
353 |
|
|
|
354 |
def distinctWith(rs: List[ARexp],
|
|
|
355 |
pruneFunction: (ARexp, Set[Rexp]) => ARexp,
|
|
|
356 |
acc: Set[Rexp] = Set()) : List[ARexp] =
|
|
|
357 |
rs match{
|
|
|
358 |
case Nil => Nil
|
|
|
359 |
case r :: rs =>
|
|
|
360 |
if(acc(erase(r)))
|
|
|
361 |
distinctWith(rs, pruneFunction, acc)
|
|
|
362 |
else {
|
|
|
363 |
val pruned_r = pruneFunction(r, acc)
|
|
|
364 |
pruned_r ::
|
|
|
365 |
distinctWith(rs,
|
|
|
366 |
pruneFunction,
|
|
|
367 |
turnIntoTerms(erase(pruned_r)) ++: acc
|
|
|
368 |
)
|
|
|
369 |
}
|
|
|
370 |
}
|
|
|
371 |
|
|
591
|
372 |
\end{lstlisting}
|
|
|
373 |
\caption{A Stronger Version of $\textit{distinctBy}$}
|
|
|
374 |
\end{figure}
|
|
|
375 |
\noindent
|
|
628
|
376 |
Once a regular expression has been pruned,
|
|
|
377 |
all its components will be added to the accumulator
|
|
|
378 |
to remove any future regular expressions' duplicate components.
|
|
|
379 |
|
|
|
380 |
The function $\textit{bsimpStrong}$
|
|
|
381 |
is very much the same as $\textit{bsimp}$, just with
|
|
|
382 |
$\textit{distinctBy}$ replaced
|
|
|
383 |
by $\textit{distinctWith}$.
|
|
591
|
384 |
\begin{figure}[H]
|
|
|
385 |
\begin{lstlisting}
|
|
628
|
386 |
|
|
591
|
387 |
def bsimpStrong(r: ARexp): ARexp =
|
|
|
388 |
{
|
|
|
389 |
r match {
|
|
|
390 |
case ASEQ(bs1, r1, r2) => (bsimpStrong(r1), bsimpStrong(r2)) match {
|
|
|
391 |
case (AZERO, _) => AZERO
|
|
|
392 |
case (_, AZERO) => AZERO
|
|
|
393 |
case (AONE(bs2), r2s) => fuse(bs1 ++ bs2, r2s)
|
|
|
394 |
case (r1s, AONE(bs2)) => fuse(bs1, r1s) //assert bs2 == Nil
|
|
|
395 |
case (r1s, r2s) => ASEQ(bs1, r1s, r2s)
|
|
|
396 |
}
|
|
|
397 |
case AALTS(bs1, rs) => {
|
|
|
398 |
distinctWith(flats(rs.map(bsimpStrong(_))), prune) match {
|
|
|
399 |
case Nil => AZERO
|
|
|
400 |
case s :: Nil => fuse(bs1, s)
|
|
|
401 |
case rs => AALTS(bs1, rs)
|
|
|
402 |
}
|
|
|
403 |
}
|
|
|
404 |
case ASTAR(bs, r0) if(atMostEmpty(erase(r0))) => AONE(bs)
|
|
|
405 |
case r => r
|
|
|
406 |
}
|
|
|
407 |
}
|
|
628
|
408 |
def bdersStrong(s: List[Char], r: ARexp) : ARexp = s match {
|
|
591
|
409 |
case Nil => r
|
|
|
410 |
case c::s => bdersStrong(s, bsimpStrong(bder(c, r)))
|
|
|
411 |
}
|
|
628
|
412 |
|
|
591
|
413 |
\end{lstlisting}
|
|
628
|
414 |
\caption{The function
|
|
|
415 |
$\textit{bsimpStrong}$: a stronger version of $\textit{bsimp}$}
|
|
591
|
416 |
\end{figure}
|
|
|
417 |
\noindent
|
|
628
|
418 |
The benefits of using
|
|
|
419 |
$\textit{prune}$ refining the finiteness bound
|
|
|
420 |
to a cubic bound has not been formalised yet.
|
|
|
421 |
Therefore we choose to use Scala code rather than an Isabelle-style formal
|
|
|
422 |
definition like we did for $\simp$, as the definitions might change
|
|
|
423 |
to suit our proof needs.
|
|
|
424 |
In the rest of the chapter we will use this convention consistently.
|
|
|
425 |
|
|
|
426 |
%The function $\textit{prune}$ is used in $\distinctWith$.
|
|
|
427 |
%$\distinctWith$ is a stronger version of $\distinctBy$
|
|
|
428 |
%which not only removes duplicates as $\distinctBy$ would
|
|
|
429 |
%do, but also uses the $\textit{pruneFunction}$
|
|
|
430 |
%argument to prune away verbose components in a regular expression.\\
|
|
|
431 |
%\begin{figure}[H]
|
|
|
432 |
%\begin{lstlisting}
|
|
|
433 |
% //a stronger version of simp
|
|
|
434 |
% def bsimpStrong(r: ARexp): ARexp =
|
|
|
435 |
% {
|
|
|
436 |
% r match {
|
|
|
437 |
% case ASEQ(bs1, r1, r2) => (bsimpStrong(r1), bsimpStrong(r2)) match {
|
|
|
438 |
% //normal clauses same as simp
|
|
|
439 |
% case (AZERO, _) => AZERO
|
|
|
440 |
% case (_, AZERO) => AZERO
|
|
|
441 |
% case (AONE(bs2), r2s) => fuse(bs1 ++ bs2, r2s)
|
|
|
442 |
% //bs2 can be discarded
|
|
|
443 |
% case (r1s, AONE(bs2)) => fuse(bs1, r1s) //assert bs2 == Nil
|
|
|
444 |
% case (r1s, r2s) => ASEQ(bs1, r1s, r2s)
|
|
|
445 |
% }
|
|
|
446 |
% case AALTS(bs1, rs) => {
|
|
|
447 |
% //distinctBy(flat_res, erase)
|
|
|
448 |
% distinctWith(flats(rs.map(bsimpStrong(_))), prune) match {
|
|
|
449 |
% case Nil => AZERO
|
|
|
450 |
% case s :: Nil => fuse(bs1, s)
|
|
|
451 |
% case rs => AALTS(bs1, rs)
|
|
|
452 |
% }
|
|
|
453 |
% }
|
|
|
454 |
% //stars that can be treated as 1
|
|
|
455 |
% case ASTAR(bs, r0) if(atMostEmpty(erase(r0))) => AONE(bs)
|
|
|
456 |
% case r => r
|
|
|
457 |
% }
|
|
|
458 |
% }
|
|
|
459 |
% def bdersStrong(s: List[Char], r: ARexp) : ARexp = s match {
|
|
|
460 |
% case Nil => r
|
|
|
461 |
% case c::s => bdersStrong(s, bsimpStrong(bder(c, r)))
|
|
|
462 |
% }
|
|
|
463 |
%\end{lstlisting}
|
|
|
464 |
%\caption{The function $\bsimpStrong$ and $\bdersStrongs$}
|
|
|
465 |
%\end{figure}
|
|
|
466 |
%\noindent
|
|
|
467 |
%$\distinctWith$, is in turn used in $\bsimpStrong$:
|
|
|
468 |
%\begin{figure}[H]
|
|
|
469 |
%\begin{lstlisting}
|
|
|
470 |
% //Conjecture: [| bdersStrong(s, r) |] = O([| r |]^3)
|
|
|
471 |
% def bdersStrong(s: List[Char], r: ARexp) : ARexp = s match {
|
|
|
472 |
% case Nil => r
|
|
|
473 |
% case c::s => bdersStrong(s, bsimpStrong(bder(c, r)))
|
|
|
474 |
% }
|
|
|
475 |
%\end{lstlisting}
|
|
|
476 |
%\caption{The function $\bsimpStrong$ and $\bdersStrongs$}
|
|
|
477 |
%\end{figure}
|
|
|
478 |
%\noindent
|
|
591
|
479 |
We conjecture that the above Scala function $\bdersStrongs$,
|
|
|
480 |
written $\bdersStrong{\_}{\_}$ as an infix notation,
|
|
|
481 |
satisfies the following property:
|
|
|
482 |
\begin{conjecture}
|
|
|
483 |
$\llbracket \bdersStrong{a}{s} \rrbracket = O(\llbracket a \rrbracket^3)$
|
|
|
484 |
\end{conjecture}
|
|
628
|
485 |
\noindent
|
|
591
|
486 |
The stronger version of $\blexersimp$'s
|
|
|
487 |
code in Scala looks like:
|
|
|
488 |
\begin{figure}[H]
|
|
|
489 |
\begin{lstlisting}
|
|
|
490 |
def strongBlexer(r: Rexp, s: String) : Option[Val] = {
|
|
|
491 |
Try(Some(decode(r, strong_blex_simp(internalise(r), s.toList)))).getOrElse(None)
|
|
|
492 |
}
|
|
|
493 |
def strong_blex_simp(r: ARexp, s: List[Char]) : Bits = s match {
|
|
|
494 |
case Nil => {
|
|
|
495 |
if (bnullable(r)) {
|
|
|
496 |
mkepsBC(r)
|
|
|
497 |
}
|
|
|
498 |
else
|
|
|
499 |
throw new Exception("Not matched")
|
|
|
500 |
}
|
|
|
501 |
case c::cs => {
|
|
|
502 |
strong_blex_simp(strongBsimp(bder(c, r)), cs)
|
|
|
503 |
}
|
|
|
504 |
}
|
|
|
505 |
\end{lstlisting}
|
|
|
506 |
\end{figure}
|
|
|
507 |
\noindent
|
|
621
|
508 |
We call this lexer $\blexerStrong$.
|
|
628
|
509 |
This version is able to drastically reduce the
|
|
|
510 |
internal data structure size which
|
|
|
511 |
otherwise could
|
|
621
|
512 |
trigger exponential behaviours in
|
|
|
513 |
$\blexersimp$.
|
|
|
514 |
\begin{figure}[H]
|
|
|
515 |
\centering
|
|
|
516 |
\begin{tabular}{@{}c@{\hspace{0mm}}c@{\hspace{0mm}}c@{}}
|
|
|
517 |
\begin{tikzpicture}
|
|
|
518 |
\begin{axis}[
|
|
|
519 |
%xlabel={$n$},
|
|
|
520 |
myplotstyle,
|
|
|
521 |
xlabel={input length},
|
|
|
522 |
ylabel={size},
|
|
|
523 |
width = 7cm,
|
|
|
524 |
height = 5cm,
|
|
|
525 |
]
|
|
|
526 |
\addplot[red,mark=*, mark options={fill=white}] table {strongSimpCurve.data};
|
|
|
527 |
\end{axis}
|
|
|
528 |
\end{tikzpicture}
|
|
|
529 |
&
|
|
|
530 |
\begin{tikzpicture}
|
|
|
531 |
\begin{axis}[
|
|
|
532 |
%xlabel={$n$},
|
|
|
533 |
myplotstyle,
|
|
|
534 |
xlabel={input length},
|
|
|
535 |
ylabel={size},
|
|
|
536 |
width = 7cm,
|
|
|
537 |
height = 5cm,
|
|
|
538 |
]
|
|
|
539 |
\addplot[blue,mark=*, mark options={fill=white}] table {bsimpExponential.data};
|
|
|
540 |
\end{axis}
|
|
|
541 |
\end{tikzpicture}\\
|
|
|
542 |
\multicolumn{2}{l}{}
|
|
|
543 |
\end{tabular}
|
|
|
544 |
\caption{Runtime for matching
|
|
|
545 |
$\protect((a^* + (aa)^* + \ldots + (aaaaa)^* )^*)^*$ with strings
|
|
|
546 |
of the form $\protect\underbrace{aa..a}_{n}$.}\label{fig:aaaaaStarStar}
|
|
|
547 |
\end{figure}
|
|
|
548 |
\noindent
|
|
591
|
549 |
We would like to preserve the correctness like the one
|
|
|
550 |
we had for $\blexersimp$:
|
|
|
551 |
\begin{conjecture}\label{cubicConjecture}
|
|
|
552 |
$\blexerStrong \;r \; s = \blexer\; r\;s$
|
|
|
553 |
\end{conjecture}
|
|
592
|
554 |
\noindent
|
|
621
|
555 |
The idea is to maintain key lemmas in
|
|
|
556 |
chapter \ref{Bitcoded2} like
|
|
|
557 |
$r \stackrel{*}{\rightsquigarrow} \textit{bsimp} \; r$
|
|
628
|
558 |
with the new rewriting rule
|
|
|
559 |
shown in figure \ref{fig:cubicRule} .
|
|
591
|
560 |
|
|
621
|
561 |
In the next sub-section,
|
|
592
|
562 |
we will describe why we
|
|
628
|
563 |
believe a cubic size bound can be achieved with
|
|
|
564 |
the stronger simplification.
|
|
|
565 |
For this we give a short introduction to the
|
|
592
|
566 |
partial derivatives,
|
|
628
|
567 |
which were invented by Antimirov \cite{Antimirov95},
|
|
|
568 |
and then link them with the result of the function
|
|
592
|
569 |
$\bdersStrongs$.
|
|
|
570 |
|
|
621
|
571 |
\subsection{Antimirov's partial derivatives}
|
|
|
572 |
Partial derivatives were first introduced by
|
|
|
573 |
Antimirov \cite{Antimirov95}.
|
|
628
|
574 |
Partial derivatives are very similar
|
|
|
575 |
to Brzozowski derivatives,
|
|
621
|
576 |
but splits children of alternative regular expressions into
|
|
628
|
577 |
multiple independent terms. This means the output of
|
|
|
578 |
partial derivatives become a
|
|
621
|
579 |
set of regular expressions:
|
|
|
580 |
\begin{center}
|
|
|
581 |
\begin{tabular}{lcl}
|
|
628
|
582 |
$\partial_x \; (r_1 \cdot r_2)$ &
|
|
|
583 |
$\dn$ & $(\partial_x \; r_1) \cdot r_2 \cup
|
|
|
584 |
\partial_x \; r_2 \; \textit{if} \; \; \nullable\; r_1$\\
|
|
|
585 |
& & $(\partial_x \; r_1)\cdot r_2 \quad\quad
|
|
621
|
586 |
\textit{otherwise}$\\
|
|
628
|
587 |
$\partial_x \; r^*$ & $\dn$ & $(\partial_x \; r) \cdot r^*$\\
|
|
621
|
588 |
$\partial_x \; c $ & $\dn$ & $\textit{if} \; x = c \;
|
|
|
589 |
\textit{then} \;
|
|
|
590 |
\{ \ONE\} \;\;\textit{else} \; \varnothing$\\
|
|
628
|
591 |
$\partial_x(r_1+r_2)$ & $=$ & $\partial_x(r_1) \cup \partial_x(r_2)$\\
|
|
621
|
592 |
$\partial_x(\ONE)$ & $=$ & $\varnothing$\\
|
|
|
593 |
$\partial_x(\ZERO)$ & $\dn$ & $\varnothing$\\
|
|
|
594 |
\end{tabular}
|
|
591
|
595 |
\end{center}
|
|
621
|
596 |
\noindent
|
|
|
597 |
The $\cdot$ between for example
|
|
628
|
598 |
$(\partial_x \; r_1) \cdot r_2 $
|
|
621
|
599 |
is a shorthand notation for the cartesian product
|
|
628
|
600 |
$(\partial_x \; r_1) \times \{ r_2\}$.
|
|
621
|
601 |
%Each element in the set generated by a partial derivative
|
|
|
602 |
%corresponds to a (potentially partial) match
|
|
|
603 |
%TODO: define derivatives w.r.t string s
|
|
628
|
604 |
Rather than joining the calculated derivatives $\partial_x r_1$ and $\partial_x r_2$ together
|
|
621
|
605 |
using the $\sum$ constructor, Antimirov put them into
|
|
628
|
606 |
a set. This means many subterms will be de-duplicated
|
|
|
607 |
because they are sets,
|
|
|
608 |
For example, to compute what regular expression $x^*(xx + y)^*$'s
|
|
|
609 |
derivative w.r.t. $x$ is, one can compute a partial derivative
|
|
|
610 |
and get two singleton sets $\{x^* \cdot (xx + y)^*\}$ and $\{x \cdot (xx + y) ^* \}$
|
|
591
|
611 |
from $\partial_x(x^*) \cdot (xx + y) ^*$ and $\partial_x((xx + y)^*)$.
|
|
621
|
612 |
|
|
628
|
613 |
The partial derivative w.r.t. a string is defined recursively:
|
|
|
614 |
\[
|
|
|
615 |
\partial_{c::cs} r \dn \bigcup_{r'\in (\partial_c r)}
|
|
|
616 |
\partial_{cs} r'
|
|
|
617 |
\]
|
|
|
618 |
Given an alphabet $\Sigma$, we denote the set of all possible strings
|
|
|
619 |
from this alphabet as $\Sigma^*$.
|
|
621
|
620 |
The set of all possible partial derivatives is defined
|
|
|
621 |
as the union of derivatives w.r.t all the strings in the universe:
|
|
|
622 |
\begin{center}
|
|
|
623 |
\begin{tabular}{lcl}
|
|
628
|
624 |
$\textit{PDER}_{\Sigma^*} \; r $ & $\dn $ & $\bigcup_{w \in \Sigma^*}\partial_w \; r$
|
|
621
|
625 |
\end{tabular}
|
|
591
|
626 |
\end{center}
|
|
621
|
627 |
\noindent
|
|
628
|
628 |
Consider now again our pathological case where the derivatives
|
|
|
629 |
grow with a rather aggressive simplification
|
|
621
|
630 |
\begin{center}
|
|
|
631 |
$((a^* + (aa)^* + \ldots + (\underbrace{a\ldots a}_{n a's})^* )^*)^*$
|
|
|
632 |
\end{center}
|
|
628
|
633 |
example, if we denote this regular expression as $r$,
|
|
621
|
634 |
we have that
|
|
|
635 |
\begin{center}
|
|
628
|
636 |
$\textit{PDER}_{\Sigma^*} \; r =
|
|
621
|
637 |
\bigcup_{i=1}^{n}\bigcup_{j=0}^{i-1} \{
|
|
|
638 |
(\underbrace{a \ldots a}_{\text{j a's}}\cdot
|
|
628
|
639 |
(\underbrace{a \ldots a}_{\text{i a's}})^*)\cdot r \}$,
|
|
591
|
640 |
\end{center}
|
|
621
|
641 |
with exactly $n * (n + 1) / 2$ terms.
|
|
|
642 |
This is in line with our speculation that only $n*(n+1)/2$ terms are
|
|
|
643 |
needed. We conjecture that $\bsimpStrong$ is also able to achieve this
|
|
|
644 |
upper limit in general
|
|
|
645 |
\begin{conjecture}\label{bsimpStrongInclusionPder}
|
|
|
646 |
Using a suitable transformation $f$, we have
|
|
|
647 |
\begin{center}
|
|
|
648 |
$\forall s.\; f \; (r \bdersStrong \; s) \subseteq
|
|
628
|
649 |
\textit{PDER}_{\Sigma^*} \; r$
|
|
621
|
650 |
\end{center}
|
|
|
651 |
\end{conjecture}
|
|
|
652 |
\noindent
|
|
628
|
653 |
because our \ref{fig:cubicRule} will keep only one copy of each term,
|
|
621
|
654 |
where the function $\textit{prune}$ takes care of maintaining
|
|
|
655 |
a set like structure similar to partial derivatives.
|
|
628
|
656 |
We might need to adjust $\textit{prune}$
|
|
621
|
657 |
slightly to make sure all duplicate terms are eliminated,
|
|
|
658 |
which should be doable.
|
|
591
|
659 |
|
|
621
|
660 |
Antimirov had proven that the sum of all the partial derivative
|
|
|
661 |
terms' sizes is bounded by the cubic of the size of that regular
|
|
|
662 |
expression:
|
|
|
663 |
\begin{property}\label{pderBound}
|
|
628
|
664 |
$\llbracket \textit{PDER}_{\Sigma^*} \; r \rrbracket \leq O(\llbracket r \rrbracket^3)$
|
|
621
|
665 |
\end{property}
|
|
628
|
666 |
This property was formalised by Wu et al. \cite{Wu2014}, and the
|
|
|
667 |
details can be found in the archive of formal proofs. \footnote{https://www.isa-afp.org/entries/Myhill-Nerode.html}
|
|
621
|
668 |
Once conjecture \ref{bsimpStrongInclusionPder} is proven, then property \ref{pderBound}
|
|
628
|
669 |
would yield us also a cubic bound for our $\blexerStrong$ algorithm:
|
|
621
|
670 |
\begin{conjecture}\label{strongCubic}
|
|
|
671 |
$\llbracket r \bdersStrong\; s \rrbracket \leq \llbracket r \rrbracket^3$
|
|
|
672 |
\end{conjecture}
|
|
628
|
673 |
\noindent
|
|
|
674 |
We leave this as future work.
|
|
591
|
675 |
|
|
|
676 |
|
|
621
|
677 |
%To get all the "atomic" components of a regular expression's possible derivatives,
|
|
|
678 |
%there is a procedure Antimirov called $\textit{lf}$, short for "linear forms", that takes
|
|
|
679 |
%whatever character is available at the head of the string inside the language of a
|
|
|
680 |
%regular expression, and gives back the character and the derivative regular expression
|
|
|
681 |
%as a pair (which he called "monomial"):
|
|
|
682 |
% \begin{center}
|
|
|
683 |
% \begin{tabular}{ccc}
|
|
|
684 |
% $\lf(\ONE)$ & $=$ & $\phi$\\
|
|
|
685 |
%$\lf(c)$ & $=$ & $\{(c, \ONE) \}$\\
|
|
|
686 |
% $\lf(a+b)$ & $=$ & $\lf(a) \cup \lf(b)$\\
|
|
|
687 |
% $\lf(r^*)$ & $=$ & $\lf(r) \bigodot \lf(r^*)$\\
|
|
|
688 |
%\end{tabular}
|
|
|
689 |
%\end{center}
|
|
|
690 |
%%TODO: completion
|
|
|
691 |
%
|
|
|
692 |
%There is a slight difference in the last three clauses compared
|
|
|
693 |
%with $\partial$: instead of a dot operator $ \textit{rset} \cdot r$ that attaches the regular
|
|
|
694 |
%expression $r$ with every element inside $\textit{rset}$ to create a set of
|
|
|
695 |
%sequence derivatives, it uses the "circle dot" operator $\bigodot$ which operates
|
|
|
696 |
%on a set of monomials (which Antimirov called "linear form") and a regular
|
|
|
697 |
%expression, and returns a linear form:
|
|
|
698 |
% \begin{center}
|
|
|
699 |
% \begin{tabular}{ccc}
|
|
|
700 |
% $l \bigodot (\ZERO)$ & $=$ & $\phi$\\
|
|
|
701 |
% $l \bigodot (\ONE)$ & $=$ & $l$\\
|
|
|
702 |
% $\phi \bigodot t$ & $=$ & $\phi$\\
|
|
|
703 |
% $\{ (x, \ZERO) \} \bigodot t$ & $=$ & $\{(x,\ZERO) \}$\\
|
|
|
704 |
% $\{ (x, \ONE) \} \bigodot t$ & $=$ & $\{(x,t) \}$\\
|
|
|
705 |
% $\{ (x, p) \} \bigodot t$ & $=$ & $\{(x,p\cdot t) \}$\\
|
|
|
706 |
% $\lf(a+b)$ & $=$ & $\lf(a) \cup \lf(b)$\\
|
|
|
707 |
% $\lf(r^*)$ & $=$ & $\lf(r) \cdot \lf(r^*)$\\
|
|
|
708 |
%\end{tabular}
|
|
|
709 |
%\end{center}
|
|
|
710 |
%%TODO: completion
|
|
|
711 |
%
|
|
|
712 |
% Some degree of simplification is applied when doing $\bigodot$, for example,
|
|
|
713 |
% $l \bigodot (\ZERO) = \phi$ corresponds to $r \cdot \ZERO \rightsquigarrow \ZERO$,
|
|
|
714 |
% and $l \bigodot (\ONE) = l$ to $l \cdot \ONE \rightsquigarrow l$, and
|
|
|
715 |
% $\{ (x, \ZERO) \} \bigodot t = \{(x,\ZERO) \}$ to $\ZERO \cdot x \rightsquigarrow \ZERO$,
|
|
|
716 |
% and so on.
|
|
|
717 |
%
|
|
|
718 |
% With the function $\lf$ one can compute all possible partial derivatives $\partial_{UNIV}(r)$ of a regular expression $r$ with
|
|
|
719 |
% an iterative procedure:
|
|
|
720 |
% \begin{center}
|
|
|
721 |
% \begin{tabular}{llll}
|
|
|
722 |
%$\textit{while}$ & $(\Delta_i \neq \phi)$ & & \\
|
|
|
723 |
% & $\Delta_{i+1}$ & $ =$ & $\lf(\Delta_i) - \PD_i$ \\
|
|
|
724 |
% & $\PD_{i+1}$ & $ =$ & $\Delta_{i+1} \cup \PD_i$ \\
|
|
|
725 |
%$\partial_{UNIV}(r)$ & $=$ & $\PD$ &
|
|
|
726 |
%\end{tabular}
|
|
|
727 |
%\end{center}
|
|
|
728 |
%
|
|
|
729 |
%
|
|
|
730 |
% $(r_1 + r_2) \cdot r_3 \longrightarrow (r_1 \cdot r_3) + (r_2 \cdot r_3)$,
|
|
591
|
731 |
|
|
|
732 |
|
|
532
|
733 |
|
|
|
734 |
|
|
|
735 |
%----------------------------------------------------------------------------------------
|
|
|
736 |
% SECTION 2
|
|
|
737 |
%----------------------------------------------------------------------------------------
|
|
|
738 |
|
|
620
|
739 |
|
|
621
|
740 |
%The closed form for them looks like:
|
|
|
741 |
%%\begin{center}
|
|
|
742 |
%% \begin{tabular}{llrclll}
|
|
|
743 |
%% $r^{\{n+1\}}$ & $ \backslash_{rsimps}$ & $(c::s)$ & $=$ & & \\
|
|
|
744 |
%% $\textit{rsimp}$ & $($ & $
|
|
|
745 |
%% \sum \; ( $ & $\map$ & $(\textit{optermsimp}\;r)$ & $($\\
|
|
|
746 |
%% & & & & $\textit{nupdates} \;$ &
|
|
|
747 |
%% $ s \; r_0 \; [ \textit{Some} \; ([c], n)]$\\
|
|
|
748 |
%% & & & & $)$ &\\
|
|
|
749 |
%% & & $)$ & & &\\
|
|
|
750 |
%% & $)$ & & & &\\
|
|
|
751 |
%% \end{tabular}
|
|
|
752 |
%%\end{center}
|
|
620
|
753 |
%\begin{center}
|
|
621
|
754 |
% \begin{tabular}{llrcllrllll}
|
|
|
755 |
% $r^{\{n+1\}}$ & $ \backslash_{rsimps}$ & $(c::s)$ & $=$ & & &&&&\\
|
|
|
756 |
% &&&&$\textit{rsimp}$ & $($ & $
|
|
|
757 |
% \sum \; ( $ & $\map$ & $(\textit{optermsimp}\;r)$ & $($\\
|
|
|
758 |
% &&&& & & & & $\;\; \textit{nupdates} \;$ &
|
|
|
759 |
% $ s \; r_0 \; [ \textit{Some} \; ([c], n)]$\\
|
|
|
760 |
% &&&& & & & & $)$ &\\
|
|
|
761 |
% &&&& & & $)$ & & &\\
|
|
|
762 |
% &&&& & $)$ & & & &\\
|
|
|
763 |
% \end{tabular}
|
|
620
|
764 |
%\end{center}
|
|
621
|
765 |
%The $\textit{optermsimp}$ function with the argument $r$
|
|
|
766 |
%chooses from two options: $\ZERO$ or
|
|
|
767 |
%We define for the $r^{\{n\}}$ constructor something similar to $\starupdate$
|
|
|
768 |
%and $\starupdates$:
|
|
620
|
769 |
%\begin{center}
|
|
621
|
770 |
% \begin{tabular}{lcl}
|
|
|
771 |
% $\starupdate \; c \; r \; [] $ & $\dn$ & $[]$\\
|
|
|
772 |
% $\starupdate \; c \; r \; (s :: Ss)$ & $\dn$ & \\
|
|
|
773 |
% & & $\textit{if} \;
|
|
|
774 |
% (\rnullable \; (\rders \; r \; s))$ \\
|
|
|
775 |
% & & $\textit{then} \;\; (s @ [c]) :: [c] :: (
|
|
|
776 |
% \starupdate \; c \; r \; Ss)$ \\
|
|
|
777 |
% & & $\textit{else} \;\; (s @ [c]) :: (
|
|
|
778 |
% \starupdate \; c \; r \; Ss)$
|
|
|
779 |
% \end{tabular}
|
|
620
|
780 |
%\end{center}
|
|
621
|
781 |
%\noindent
|
|
|
782 |
%As a generalisation from characters to strings,
|
|
|
783 |
%$\starupdates$ takes a string instead of a character
|
|
|
784 |
%as the first input argument, and is otherwise the same
|
|
|
785 |
%as $\starupdate$.
|
|
|
786 |
%\begin{center}
|
|
|
787 |
% \begin{tabular}{lcl}
|
|
|
788 |
% $\starupdates \; [] \; r \; Ss$ & $=$ & $Ss$\\
|
|
|
789 |
% $\starupdates \; (c :: cs) \; r \; Ss$ & $=$ & $\starupdates \; cs \; r \; (
|
|
|
790 |
% \starupdate \; c \; r \; Ss)$
|
|
|
791 |
% \end{tabular}
|
|
|
792 |
%\end{center}
|
|
|
793 |
%\noindent
|
|
620
|
794 |
|
|
|
795 |
|
|
|
796 |
|
|
621
|
797 |
%\section{Zippers}
|
|
|
798 |
%Zipper is a data structure designed to operate on
|
|
|
799 |
%and navigate between local parts of a tree.
|
|
|
800 |
%It was first formally described by Huet \cite{HuetZipper}.
|
|
|
801 |
%Typical applications of zippers involve text editor buffers
|
|
|
802 |
%and proof system databases.
|
|
|
803 |
%In our setting, the idea is to compactify the representation
|
|
|
804 |
%of derivatives with zippers, thereby making our algorithm faster.
|
|
|
805 |
%Some initial results
|
|
|
806 |
%We first give a brief introduction to what zippers are,
|
|
|
807 |
%and other works
|
|
|
808 |
%that apply zippers to derivatives
|
|
|
809 |
%When dealing with large trees, it would be a waste to
|
|
|
810 |
%traverse the entire tree if
|
|
|
811 |
%the operation only
|
|
|
812 |
%involves a small fraction of it.
|
|
|
813 |
%The idea is to put the focus on that subtree, turning other parts
|
|
|
814 |
%of the tree into a context
|
|
|
815 |
%
|
|
|
816 |
%
|
|
|
817 |
%One observation about our derivative-based lexing algorithm is that
|
|
|
818 |
%the derivative operation sometimes traverses the entire regular expression
|
|
|
819 |
%unnecessarily:
|
|
620
|
820 |
|
|
|
821 |
|
|
612
|
822 |
%----------------------------------------------------------------------------------------
|
|
|
823 |
% SECTION 1
|
|
|
824 |
%----------------------------------------------------------------------------------------
|
|
532
|
825 |
|
|
612
|
826 |
%\section{Adding Support for the Negation Construct, and its Correctness Proof}
|
|
|
827 |
%We now add support for the negation regular expression:
|
|
|
828 |
%\[ r ::= \ZERO \mid \ONE
|
|
|
829 |
% \mid c
|
|
|
830 |
% \mid r_1 \cdot r_2
|
|
|
831 |
% \mid r_1 + r_2
|
|
|
832 |
% \mid r^*
|
|
|
833 |
% \mid \sim r
|
|
|
834 |
%\]
|
|
|
835 |
%The $\textit{nullable}$ function's clause for it would be
|
|
|
836 |
%\[
|
|
|
837 |
%\textit{nullable}(~r) = \neg \nullable(r)
|
|
|
838 |
%\]
|
|
|
839 |
%The derivative would be
|
|
|
840 |
%\[
|
|
|
841 |
%~r \backslash c = ~ (r \backslash c)
|
|
|
842 |
%\]
|
|
|
843 |
%
|
|
|
844 |
%The most tricky part of lexing for the $~r$ regular expression
|
|
|
845 |
% is creating a value for it.
|
|
|
846 |
% For other regular expressions, the value aligns with the
|
|
|
847 |
% structure of the regular expression:
|
|
|
848 |
% \[
|
|
|
849 |
% \vdash \Seq(\Char(a), \Char(b)) : a \cdot b
|
|
|
850 |
% \]
|
|
|
851 |
%But for the $~r$ regular expression, $s$ is a member of it if and only if
|
|
|
852 |
%$s$ does not belong to $L(r)$.
|
|
|
853 |
%That means when there
|
|
|
854 |
%is a match for the not regular expression, it is not possible to generate how the string $s$ matched
|
|
|
855 |
%with $r$.
|
|
|
856 |
%What we can do is preserve the information of how $s$ was not matched by $r$,
|
|
|
857 |
%and there are a number of options to do this.
|
|
|
858 |
%
|
|
|
859 |
%We could give a partial value when there is a partial match for the regular expression inside
|
|
|
860 |
%the $\mathbf{not}$ construct.
|
|
|
861 |
%For example, the string $ab$ is not in the language of $(a\cdot b) \cdot c$,
|
|
|
862 |
%A value for it could be
|
|
|
863 |
% \[
|
|
|
864 |
% \vdash \textit{Not}(\Seq(\Char(a), \Char(b))) : ~((a \cdot b ) \cdot c)
|
|
|
865 |
% \]
|
|
|
866 |
% The above example demonstrates what value to construct
|
|
|
867 |
% when the string $s$ is at most a real prefix
|
|
|
868 |
% of the strings in $L(r)$. When $s$ instead is not a prefix of any strings
|
|
|
869 |
% in $L(r)$, it becomes unclear what to return as a value inside the $\textit{Not}$
|
|
|
870 |
% constructor.
|
|
|
871 |
%
|
|
|
872 |
% Another option would be to either store the string $s$ that resulted in
|
|
|
873 |
% a mis-match for $r$ or a dummy value as a placeholder:
|
|
|
874 |
% \[
|
|
|
875 |
% \vdash \textit{Not}(abcd) : ~( r_1 )
|
|
|
876 |
% \]
|
|
|
877 |
%or
|
|
|
878 |
% \[
|
|
|
879 |
% \vdash \textit{Not}(\textit{Dummy}) : ~( r_1 )
|
|
|
880 |
% \]
|
|
|
881 |
% We choose to implement this as it is most straightforward:
|
|
|
882 |
% \[
|
|
|
883 |
% \mkeps(~(r)) = \textit{if}(\nullable(r)) \; \textit{Error} \; \textit{else} \; \textit{Not}(\textit{Dummy})
|
|
|
884 |
% \]
|
|
|
885 |
%
|
|
|
886 |
%
|
|
620
|
887 |
%\begin{center}
|
|
|
888 |
% \begin{tabular}{lcl}
|
|
|
889 |
% $\ntset \; r \; (n+1) \; c::cs $ & $\dn$ & $\nupdates \;
|
|
|
890 |
% cs \; r \; [\Some \; ([c], n)]$\\
|
|
|
891 |
% $\ntset \; r\; 0 \; \_$ & $\dn$ & $\None$\\
|
|
|
892 |
% $\ntset \; r \; \_ \; [] $ & $ \dn$ & $[]$\\
|
|
|
893 |
% \end{tabular}
|
|
|
894 |
%\end{center}
|
|
628
|
895 |
|