|
94
|
1 |
\documentclass[a4paper,UKenglish]{lipics}
|
|
|
2 |
\usepackage{graphic}
|
|
|
3 |
\usepackage{data}
|
|
|
4 |
\usepackage{tikz-cd}
|
|
114
|
5 |
\usepackage{tikz}
|
|
138
|
6 |
|
|
|
7 |
%\usetikzlibrary{graphs}
|
|
|
8 |
%\usetikzlibrary{graphdrawing}
|
|
|
9 |
%\usegdlibrary{trees}
|
|
|
10 |
|
|
94
|
11 |
%\usepackage{algorithm}
|
|
|
12 |
\usepackage{amsmath}
|
|
110
|
13 |
\usepackage{xcolor}
|
|
94
|
14 |
\usepackage[noend]{algpseudocode}
|
|
|
15 |
\usepackage{enumitem}
|
|
|
16 |
\usepackage{nccmath}
|
|
113
|
17 |
\usepackage{soul}
|
|
94
|
18 |
|
|
|
19 |
\definecolor{darkblue}{rgb}{0,0,0.6}
|
|
|
20 |
\hypersetup{colorlinks=true,allcolors=darkblue}
|
|
|
21 |
\newcommand{\comment}[1]%
|
|
|
22 |
{{\color{red}$\Rightarrow$}\marginpar{\raggedright\small{\bf\color{red}#1}}}
|
|
|
23 |
|
|
|
24 |
% \documentclass{article}
|
|
|
25 |
%\usepackage[utf8]{inputenc}
|
|
|
26 |
%\usepackage[english]{babel}
|
|
|
27 |
%\usepackage{listings}
|
|
|
28 |
% \usepackage{amsthm}
|
|
|
29 |
%\usepackage{hyperref}
|
|
|
30 |
% \usepackage[margin=0.5in]{geometry}
|
|
|
31 |
%\usepackage{pmboxdraw}
|
|
|
32 |
|
|
|
33 |
\title{POSIX Regular Expression Matching and Lexing}
|
|
|
34 |
\author{Chengsong Tan}
|
|
|
35 |
\affil{King's College London\\
|
|
|
36 |
London, UK\\
|
|
|
37 |
\texttt{chengsong.tan@kcl.ac.uk}}
|
|
|
38 |
\authorrunning{Chengsong Tan}
|
|
|
39 |
\Copyright{Chengsong Tan}
|
|
|
40 |
|
|
|
41 |
\newcommand{\dn}{\stackrel{\mbox{\scriptsize def}}{=}}%
|
|
|
42 |
\newcommand{\ZERO}{\mbox{\bf 0}}
|
|
|
43 |
\newcommand{\ONE}{\mbox{\bf 1}}
|
|
101
|
44 |
\def\erase{\textit{erase}}
|
|
94
|
45 |
\def\bders{\textit{bders}}
|
|
|
46 |
\def\lexer{\mathit{lexer}}
|
|
|
47 |
\def\blexer{\textit{blexer}}
|
|
107
|
48 |
\def\fuse{\textit{fuse}}
|
|
|
49 |
\def\flatten{\textit{flatten}}
|
|
|
50 |
\def\map{\textit{map}}
|
|
94
|
51 |
\def\blexers{\mathit{blexer\_simp}}
|
|
95
|
52 |
\def\simp{\mathit{simp}}
|
|
94
|
53 |
\def\mkeps{\mathit{mkeps}}
|
|
|
54 |
\def\bmkeps{\textit{bmkeps}}
|
|
|
55 |
\def\inj{\mathit{inj}}
|
|
|
56 |
\def\Empty{\mathit{Empty}}
|
|
|
57 |
\def\Left{\mathit{Left}}
|
|
|
58 |
\def\Right{\mathit{Right}}
|
|
|
59 |
\def\Stars{\mathit{Stars}}
|
|
|
60 |
\def\Char{\mathit{Char}}
|
|
|
61 |
\def\Seq{\mathit{Seq}}
|
|
|
62 |
\def\Der{\mathit{Der}}
|
|
|
63 |
\def\nullable{\mathit{nullable}}
|
|
|
64 |
\def\Z{\mathit{Z}}
|
|
|
65 |
\def\S{\mathit{S}}
|
|
|
66 |
\def\flex{\textit{flex}}
|
|
|
67 |
\def\rup{r^\uparrow}
|
|
|
68 |
\def\retrieve{\textit{retrieve}}
|
|
|
69 |
\def\AALTS{\textit{AALTS}}
|
|
|
70 |
\def\AONE{\textit{AONE}}
|
|
|
71 |
%\theoremstyle{theorem}
|
|
|
72 |
%\newtheorem{theorem}{Theorem}
|
|
|
73 |
%\theoremstyle{lemma}
|
|
|
74 |
%\newtheorem{lemma}{Lemma}
|
|
|
75 |
%\newcommand{\lemmaautorefname}{Lemma}
|
|
|
76 |
%\theoremstyle{definition}
|
|
|
77 |
%\newtheorem{definition}{Definition}
|
|
|
78 |
\algnewcommand\algorithmicswitch{\textbf{switch}}
|
|
|
79 |
\algnewcommand\algorithmiccase{\textbf{case}}
|
|
|
80 |
\algnewcommand\algorithmicassert{\texttt{assert}}
|
|
|
81 |
\algnewcommand\Assert[1]{\State \algorithmicassert(#1)}%
|
|
|
82 |
% New "environments"
|
|
|
83 |
\algdef{SE}[SWITCH]{Switch}{EndSwitch}[1]{\algorithmicswitch\ #1\ \algorithmicdo}{\algorithmicend\ \algorithmicswitch}%
|
|
|
84 |
\algdef{SE}[CASE]{Case}{EndCase}[1]{\algorithmiccase\ #1}{\algorithmicend\ \algorithmiccase}%
|
|
|
85 |
\algtext*{EndSwitch}%
|
|
|
86 |
\algtext*{EndCase}%
|
|
|
87 |
|
|
|
88 |
|
|
|
89 |
\begin{document}
|
|
|
90 |
|
|
|
91 |
\maketitle
|
|
|
92 |
|
|
|
93 |
\begin{abstract}
|
|
148
|
94 |
Regular expressions, a useful concept in computer science
|
|
|
95 |
that was initially designed to match string patterns,
|
|
|
96 |
need fast matching algorithms.
|
|
|
97 |
If we do matching by naively converting
|
|
|
98 |
the regular expression to a
|
|
|
99 |
Nondeterministic-Finite-Automaton(NFA) and simulating it,
|
|
|
100 |
they can run into trouble on certain evil regular expression and string
|
|
|
101 |
pairs.
|
|
|
102 |
This necessitates the introudction of a
|
|
|
103 |
method called derivatives of regular expressions\cite{Brzozowski1964}.
|
|
|
104 |
With some variation introduced by Sulzmann and Lu\cite{Sulzmann2014},
|
|
|
105 |
it circumvents the problem of
|
|
|
106 |
catastrphoic backtracking elegantly when
|
|
|
107 |
compared to backtracking NFA regex engines.
|
|
|
108 |
We believe that such a method can help to address
|
|
|
109 |
the status-quo where badly written code for
|
|
|
110 |
regular expression matching can cause a software grief.
|
|
|
111 |
We have come up with a set of simplification rules
|
|
|
112 |
that makes the space and time requirements below a tight bound.
|
|
|
113 |
We have proved certain properties of the algorithm
|
|
|
114 |
and simplification.
|
|
|
115 |
We have not yet worked out a proof for the correctness
|
|
|
116 |
although test data suggested this.
|
|
94
|
117 |
\end{abstract}
|
|
|
118 |
|
|
126
|
119 |
|
|
148
|
120 |
|
|
126
|
121 |
\section{Introduction}
|
|
148
|
122 |
The following brief introduction gives the background for
|
|
|
123 |
derivatives--how they are originally defined and the
|
|
|
124 |
variety\cite{Sulzmann2014} that is more suitable for lexing.
|
|
|
125 |
Regular expressions can be formalized as follows:\\
|
|
|
126 |
\begin{center}
|
|
|
127 |
$r ::= \ZERO | \ONE | c | r_1 +r_2 | r_1 \cdot r_2 | r^*$
|
|
|
128 |
\end{center}
|
|
|
129 |
Derivatives of regular expression can be
|
|
|
130 |
seen as the regular expression that corresponds to
|
|
|
131 |
the language derived by computing
|
|
|
132 |
the left quotient of the original regular language
|
|
|
133 |
w.r.t a character.
|
|
|
134 |
Derivative of regular expression is also a
|
|
|
135 |
regular expression because
|
|
|
136 |
the left quotient of a regular language is also regular.
|
|
|
137 |
With this we know such a function exist without having
|
|
|
138 |
to worry that it might not be defined.
|
|
|
139 |
In fact, regular expressions derivatives
|
|
|
140 |
are not just defined but also simple and elegant.
|
|
|
141 |
They are composed of two recursive functions,
|
|
|
142 |
and can be easily explained by intuition.
|
|
|
143 |
The function
|
|
|
144 |
$\nullable$ defined below,
|
|
|
145 |
tests whether the empty string belongs
|
|
|
146 |
to the regular expression being checked.
|
|
107
|
147 |
|
|
|
148 |
\begin{center}
|
|
|
149 |
\begin{tabular}{lcl}
|
|
|
150 |
$\nullable(\ZERO)$ & $\dn$ & $\mathit{false}$ \\
|
|
|
151 |
$\nullable(\ONE)$ & $\dn$ & $\mathit{true}$ \\
|
|
|
152 |
$\nullable(c)$ & $\dn$ & $\mathit{false}$ \\
|
|
|
153 |
$\nullable(r_1 + r_2)$ & $\dn$ & $\nullable(r_1) \vee \nullable(r_2)$ \\
|
|
|
154 |
$\nullable(r_1\cdot r_2)$ & $\dn$ & $\nullable(r_1) \wedge \nullable(r_2)$ \\
|
|
|
155 |
$\nullable(r^*)$ & $\dn$ & $\mathit{true}$ \\
|
|
|
156 |
\end{tabular}
|
|
148
|
157 |
\end{center}
|
|
|
158 |
\noindent
|
|
|
159 |
The empty set does not contain any string and
|
|
|
160 |
therefore not the empty string, the empty string
|
|
|
161 |
regular expression contains the empty string
|
|
|
162 |
by definition, the character regular expression
|
|
|
163 |
is the singleton that contains character only,
|
|
|
164 |
and therefore does not contain the empty string,
|
|
|
165 |
the alternative regular expression(or "or" expression)
|
|
|
166 |
might have one of its children regular expressions
|
|
|
167 |
being nullable and any one of its children being nullable
|
|
|
168 |
would suffice. The sequence regular expression
|
|
|
169 |
would require both children to have the empty string
|
|
|
170 |
to compose an empty string and the Kleene star
|
|
|
171 |
operation naturally introduced the empty string.
|
|
|
172 |
All nice and easy.
|
|
|
173 |
This definition is used in the derivative operation
|
|
|
174 |
as a condition:
|
|
107
|
175 |
|
|
|
176 |
\begin{center}
|
|
|
177 |
\begin{tabular}{lcl}
|
|
|
178 |
$\ZERO \backslash c$ & $\dn$ & $\ZERO$\\
|
|
|
179 |
$\ONE \backslash c$ & $\dn$ & $\ZERO$\\
|
|
|
180 |
$d \backslash c$ & $\dn$ &
|
|
|
181 |
$\mathit{if} \;c = d\;\mathit{then}\;\ONE\;\mathit{else}\;\ZERO$\\
|
|
|
182 |
$(r_1 + r_2)\backslash c$ & $\dn$ & $r_1 \backslash c \,+\, r_2 \backslash c$\\
|
|
|
183 |
$(r_1 \cdot r_2)\backslash c$ & $\dn$ & $\mathit{if} \, nullable(r_1)$\\
|
|
|
184 |
& & $\mathit{then}\;(r_1\backslash c) \cdot r_2 \,+\, r_2\backslash c$\\
|
|
|
185 |
& & $\mathit{else}\;(r_1\backslash c) \cdot r_2$\\
|
|
|
186 |
$(r^*)\backslash c$ & $\dn$ & $(r\backslash c) \cdot r^*$\\
|
|
|
187 |
\end{tabular}
|
|
|
188 |
\end{center}
|
|
130
|
189 |
\noindent
|
|
148
|
190 |
\noindent
|
|
|
191 |
The function derivative, written $\backslash c$,
|
|
|
192 |
defines how a regular expression evolves into
|
|
130
|
193 |
a new regular expression after all the string it contains
|
|
|
194 |
is chopped off a certain head character $c$.
|
|
148
|
195 |
The most involved cases are the sequence
|
|
|
196 |
and star case.
|
|
|
197 |
The sequence case says that if the first regular expression
|
|
|
198 |
contains an empty string then second component of the sequence
|
|
|
199 |
might be chosen as the target regular expression to be chopped
|
|
|
200 |
off its head character.
|
|
|
201 |
The star regular expression unwraps the iteration of
|
|
|
202 |
regular expression and attack the star regular expression
|
|
|
203 |
to its back again to make sure there are 0 or more iterations
|
|
|
204 |
following this unfolded iteration.
|
|
107
|
205 |
|
|
148
|
206 |
|
|
|
207 |
The main property of the derivative operation
|
|
|
208 |
that enables us to reason about the correctness of
|
|
|
209 |
an algorithm using derivatives is
|
|
107
|
210 |
|
|
|
211 |
\begin{center}
|
|
|
212 |
$c\!::\!s \in L(r)$ holds
|
|
|
213 |
if and only if $s \in L(r\backslash c)$.
|
|
|
214 |
\end{center}
|
|
|
215 |
|
|
|
216 |
\noindent
|
|
108
|
217 |
We can generalise the derivative operation shown above for single characters
|
|
|
218 |
to strings as follows:
|
|
107
|
219 |
|
|
|
220 |
\begin{center}
|
|
|
221 |
\begin{tabular}{lcl}
|
|
|
222 |
$r \backslash (c\!::\!s) $ & $\dn$ & $(r \backslash c) \backslash s$ \\
|
|
|
223 |
$r \backslash [\,] $ & $\dn$ & $r$
|
|
|
224 |
\end{tabular}
|
|
|
225 |
\end{center}
|
|
|
226 |
|
|
|
227 |
\noindent
|
|
108
|
228 |
and then define Brzozowski's regular-expression matching algorithm as:
|
|
|
229 |
|
|
107
|
230 |
\[
|
|
|
231 |
match\;s\;r \;\dn\; nullable(r\backslash s)
|
|
|
232 |
\]
|
|
|
233 |
|
|
|
234 |
\noindent
|
|
130
|
235 |
Assuming the a string is given as a sequence of characters, say $c_0c_1..c_n$,
|
|
108
|
236 |
this algorithm presented graphically is as follows:
|
|
|
237 |
|
|
107
|
238 |
\begin{equation}\label{graph:*}
|
|
|
239 |
\begin{tikzcd}
|
|
|
240 |
r_0 \arrow[r, "\backslash c_0"] & r_1 \arrow[r, "\backslash c_1"] & r_2 \arrow[r, dashed] & r_n \arrow[r,"\textit{nullable}?"] & \;\textrm{YES}/\textrm{NO}
|
|
|
241 |
\end{tikzcd}
|
|
|
242 |
\end{equation}
|
|
|
243 |
|
|
|
244 |
\noindent
|
|
|
245 |
where we start with a regular expression $r_0$, build successive
|
|
|
246 |
derivatives until we exhaust the string and then use \textit{nullable}
|
|
|
247 |
to test whether the result can match the empty string. It can be
|
|
|
248 |
relatively easily shown that this matcher is correct (that is given
|
|
|
249 |
an $s = c_0...c_{n-1}$ and an $r_0$, it generates YES if and only if $s \in L(r_0)$).
|
|
|
250 |
|
|
148
|
251 |
Beautiful and simple definition.
|
|
|
252 |
|
|
|
253 |
If we implement the above algorithm naively, however,
|
|
|
254 |
the algorithm can be excruciatingly slow. For example, when starting with the regular
|
|
|
255 |
expression $(a + aa)^*$ and building 12 successive derivatives
|
|
|
256 |
w.r.t.~the character $a$, one obtains a derivative regular expression
|
|
|
257 |
with more than 8000 nodes (when viewed as a tree). Operations like
|
|
|
258 |
$\backslash$ and $\nullable$ need to traverse such trees and
|
|
|
259 |
consequently the bigger the size of the derivative the slower the
|
|
|
260 |
algorithm.
|
|
|
261 |
|
|
|
262 |
Brzozowski was quick in finding that during this process a lot useless
|
|
|
263 |
$\ONE$s and $\ZERO$s are generated and therefore not optimal.
|
|
|
264 |
He also introduced some "similarity rules" such
|
|
|
265 |
as $P+(Q+R) = (P+Q)+R$ to merge syntactically
|
|
|
266 |
different but language-equivalent sub-regexes to further decrease the size
|
|
|
267 |
of the intermediate regexes.
|
|
|
268 |
|
|
|
269 |
More simplifications are possible, such as deleting duplicates
|
|
|
270 |
and opening up nested alternatives to trigger even more simplifications.
|
|
|
271 |
And suppose we apply simplification after each derivative step, and compose
|
|
|
272 |
these two operations together as an atomic one: $a \backslash_{simp}\,c \dn
|
|
|
273 |
\textit{simp}(a \backslash c)$. Then we can build
|
|
|
274 |
a matcher without having cumbersome regular expressions.
|
|
|
275 |
|
|
|
276 |
|
|
|
277 |
If we want the size of derivatives in the algorithm to
|
|
|
278 |
stay even lower, we would need more aggressive simplifications.
|
|
|
279 |
Essentially we need to delete useless $\ZERO$s and $\ONE$s, as well as
|
|
|
280 |
deleting duplicates whenever possible. For example, the parentheses in
|
|
|
281 |
$(a+b) \cdot c + b\cdot c$ can be opened up to get $a\cdot c + b \cdot c + b
|
|
|
282 |
\cdot c$, and then simplified to just $a \cdot c + b \cdot c$. Another
|
|
|
283 |
example is simplifying $(a^*+a) + (a^*+ \ONE) + (a +\ONE)$ to just
|
|
|
284 |
$a^*+a+\ONE$. Adding these more aggressive simplification rules help us
|
|
|
285 |
to achieve a very tight size bound, namely,
|
|
|
286 |
the same size bound as that of the \emph{partial derivatives}.
|
|
|
287 |
|
|
|
288 |
Building derivatives and then simplify them.
|
|
|
289 |
So far so good. But what if we want to
|
|
|
290 |
do lexing instead of just a YES/NO answer?
|
|
|
291 |
This requires us to go back again to the world
|
|
|
292 |
without simplification first for a moment.
|
|
|
293 |
Sulzmann and Lu~\cite{Sulzmann2014} first came up with a nice and
|
|
|
294 |
elegant(arguably as beautiful as the original
|
|
|
295 |
derivatives definition) solution for this.
|
|
|
296 |
|
|
108
|
297 |
\subsection*{Values and the Lexing Algorithm by Sulzmann and Lu}
|
|
107
|
298 |
|
|
148
|
299 |
|
|
|
300 |
They first defined the datatypes for storing the
|
|
|
301 |
lexing information called a \emph{value} or
|
|
107
|
302 |
sometimes also \emph{lexical value}. These values and regular
|
|
|
303 |
expressions correspond to each other as illustrated in the following
|
|
|
304 |
table:
|
|
|
305 |
|
|
|
306 |
\begin{center}
|
|
|
307 |
\begin{tabular}{c@{\hspace{20mm}}c}
|
|
|
308 |
\begin{tabular}{@{}rrl@{}}
|
|
|
309 |
\multicolumn{3}{@{}l}{\textbf{Regular Expressions}}\medskip\\
|
|
|
310 |
$r$ & $::=$ & $\ZERO$\\
|
|
|
311 |
& $\mid$ & $\ONE$ \\
|
|
|
312 |
& $\mid$ & $c$ \\
|
|
|
313 |
& $\mid$ & $r_1 \cdot r_2$\\
|
|
|
314 |
& $\mid$ & $r_1 + r_2$ \\
|
|
|
315 |
\\
|
|
|
316 |
& $\mid$ & $r^*$ \\
|
|
|
317 |
\end{tabular}
|
|
|
318 |
&
|
|
|
319 |
\begin{tabular}{@{\hspace{0mm}}rrl@{}}
|
|
|
320 |
\multicolumn{3}{@{}l}{\textbf{Values}}\medskip\\
|
|
|
321 |
$v$ & $::=$ & \\
|
|
|
322 |
& & $\Empty$ \\
|
|
|
323 |
& $\mid$ & $\Char(c)$ \\
|
|
|
324 |
& $\mid$ & $\Seq\,v_1\, v_2$\\
|
|
|
325 |
& $\mid$ & $\Left(v)$ \\
|
|
|
326 |
& $\mid$ & $\Right(v)$ \\
|
|
|
327 |
& $\mid$ & $\Stars\,[v_1,\ldots\,v_n]$ \\
|
|
|
328 |
\end{tabular}
|
|
|
329 |
\end{tabular}
|
|
|
330 |
\end{center}
|
|
|
331 |
|
|
|
332 |
\noindent
|
|
148
|
333 |
One regular expression can have multiple lexical values. For example
|
|
|
334 |
for the regular expression $(a+b)^*$, it has a infinite list of
|
|
|
335 |
values corresponding to it: $\Stars\,[]$, $\Stars\,[\Left(Char(a))]$,
|
|
|
336 |
$\Stars\,[\Right(Char(b))]$, $\Stars\,[\Left(Char(a),\,\Right(Char(b))]$,
|
|
|
337 |
$\ldots$, and vice versa.
|
|
|
338 |
Even for the regular expression matching a certain string, there could
|
|
|
339 |
still be more than one value corresponding to it.
|
|
|
340 |
Take the example where $r= (a^*\cdot a^*)^*$ and the string
|
|
|
341 |
$s=\underbrace{aa\ldots a}_\text{n \textit{a}s}$.
|
|
|
342 |
The number of different ways of matching
|
|
|
343 |
without allowing any value under a star to be flattened
|
|
|
344 |
to an empty string can be given by the following formula:
|
|
|
345 |
\begin{center}
|
|
|
346 |
$C_n = (n+1)+n C_1+\ldots + 2 C_{n-1}$
|
|
|
347 |
\end{center}
|
|
|
348 |
and a closed form formula can be calculated to be
|
|
|
349 |
\begin{equation}
|
|
|
350 |
C_n =\frac{(2+\sqrt{2})^n - (2-\sqrt{2})^n}{4\sqrt{2}}
|
|
|
351 |
\end{equation}
|
|
|
352 |
which is clearly in exponential order.
|
|
|
353 |
A lexer aimed at getting all the possible values has an exponential
|
|
|
354 |
worst case runtime. Therefore it is impractical to try to generate
|
|
|
355 |
all possible matches in a run. In practice, we are usually
|
|
|
356 |
interested about POSIX values, which by intuition always
|
|
|
357 |
match the leftmost regular expression when there is a choice
|
|
|
358 |
and always match a sub part as much as possible before proceeding
|
|
|
359 |
to the next token. For example, the above example has the POSIX value
|
|
|
360 |
$ \Stars\,[\Seq(Stars\,[\underbrace{\Char(a),\ldots,\Char(a)}_\text{n iterations}], Stars\,[])]$.
|
|
|
361 |
The output of an algorithm we want would be a POSIX matching
|
|
|
362 |
encoded as a value.
|
|
107
|
363 |
The contribution of Sulzmann and Lu is an extension of Brzozowski's
|
|
|
364 |
algorithm by a second phase (the first phase being building successive
|
|
|
365 |
derivatives---see \eqref{graph:*}). In this second phase, a POSIX value
|
|
|
366 |
is generated in case the regular expression matches the string.
|
|
|
367 |
Pictorially, the Sulzmann and Lu algorithm is as follows:
|
|
|
368 |
|
|
|
369 |
\begin{ceqn}
|
|
|
370 |
\begin{equation}\label{graph:2}
|
|
|
371 |
\begin{tikzcd}
|
|
|
372 |
r_0 \arrow[r, "\backslash c_0"] \arrow[d] & r_1 \arrow[r, "\backslash c_1"] \arrow[d] & r_2 \arrow[r, dashed] \arrow[d] & r_n \arrow[d, "mkeps" description] \\
|
|
|
373 |
v_0 & v_1 \arrow[l,"inj_{r_0} c_0"] & v_2 \arrow[l, "inj_{r_1} c_1"] & v_n \arrow[l, dashed]
|
|
|
374 |
\end{tikzcd}
|
|
|
375 |
\end{equation}
|
|
|
376 |
\end{ceqn}
|
|
|
377 |
|
|
|
378 |
\noindent
|
|
|
379 |
For convenience, we shall employ the following notations: the regular
|
|
|
380 |
expression we start with is $r_0$, and the given string $s$ is composed
|
|
|
381 |
of characters $c_0 c_1 \ldots c_{n-1}$. In the first phase from the
|
|
|
382 |
left to right, we build the derivatives $r_1$, $r_2$, \ldots according
|
|
|
383 |
to the characters $c_0$, $c_1$ until we exhaust the string and obtain
|
|
|
384 |
the derivative $r_n$. We test whether this derivative is
|
|
|
385 |
$\textit{nullable}$ or not. If not, we know the string does not match
|
|
|
386 |
$r$ and no value needs to be generated. If yes, we start building the
|
|
|
387 |
values incrementally by \emph{injecting} back the characters into the
|
|
|
388 |
earlier values $v_n, \ldots, v_0$. This is the second phase of the
|
|
|
389 |
algorithm from the right to left. For the first value $v_n$, we call the
|
|
148
|
390 |
function $\textit{mkeps}$, which builds a POSIX lexical value
|
|
107
|
391 |
for how the empty string has been matched by the (nullable) regular
|
|
|
392 |
expression $r_n$. This function is defined as
|
|
|
393 |
|
|
|
394 |
\begin{center}
|
|
|
395 |
\begin{tabular}{lcl}
|
|
|
396 |
$\mkeps(\ONE)$ & $\dn$ & $\Empty$ \\
|
|
|
397 |
$\mkeps(r_{1}+r_{2})$ & $\dn$
|
|
|
398 |
& \textit{if} $\nullable(r_{1})$\\
|
|
|
399 |
& & \textit{then} $\Left(\mkeps(r_{1}))$\\
|
|
|
400 |
& & \textit{else} $\Right(\mkeps(r_{2}))$\\
|
|
|
401 |
$\mkeps(r_1\cdot r_2)$ & $\dn$ & $\Seq\,(\mkeps\,r_1)\,(\mkeps\,r_2)$\\
|
|
|
402 |
$mkeps(r^*)$ & $\dn$ & $\Stars\,[]$
|
|
|
403 |
\end{tabular}
|
|
|
404 |
\end{center}
|
|
|
405 |
|
|
|
406 |
|
|
|
407 |
\noindent
|
|
|
408 |
After the $\mkeps$-call, we inject back the characters one by one in order to build
|
|
|
409 |
the lexical value $v_i$ for how the regex $r_i$ matches the string $s_i$
|
|
|
410 |
($s_i = c_i \ldots c_{n-1}$ ) from the previous lexical value $v_{i+1}$.
|
|
|
411 |
After injecting back $n$ characters, we get the lexical value for how $r_0$
|
|
148
|
412 |
matches $s$. The POSIX value is maintained throught out the process.
|
|
|
413 |
For this Sulzmann and Lu defined a function that reverses
|
|
107
|
414 |
the ``chopping off'' of characters during the derivative phase. The
|
|
|
415 |
corresponding function is called \emph{injection}, written
|
|
|
416 |
$\textit{inj}$; it takes three arguments: the first one is a regular
|
|
|
417 |
expression ${r_{i-1}}$, before the character is chopped off, the second
|
|
|
418 |
is a character ${c_{i-1}}$, the character we want to inject and the
|
|
|
419 |
third argument is the value ${v_i}$, into which one wants to inject the
|
|
|
420 |
character (it corresponds to the regular expression after the character
|
|
|
421 |
has been chopped off). The result of this function is a new value. The
|
|
|
422 |
definition of $\textit{inj}$ is as follows:
|
|
|
423 |
|
|
|
424 |
\begin{center}
|
|
|
425 |
\begin{tabular}{l@{\hspace{1mm}}c@{\hspace{1mm}}l}
|
|
|
426 |
$\textit{inj}\,(c)\,c\,Empty$ & $\dn$ & $Char\,c$\\
|
|
|
427 |
$\textit{inj}\,(r_1 + r_2)\,c\,\Left(v)$ & $\dn$ & $\Left(\textit{inj}\,r_1\,c\,v)$\\
|
|
|
428 |
$\textit{inj}\,(r_1 + r_2)\,c\,Right(v)$ & $\dn$ & $Right(\textit{inj}\,r_2\,c\,v)$\\
|
|
|
429 |
$\textit{inj}\,(r_1 \cdot r_2)\,c\,Seq(v_1,v_2)$ & $\dn$ & $Seq(\textit{inj}\,r_1\,c\,v_1,v_2)$\\
|
|
|
430 |
$\textit{inj}\,(r_1 \cdot r_2)\,c\,\Left(Seq(v_1,v_2))$ & $\dn$ & $Seq(\textit{inj}\,r_1\,c\,v_1,v_2)$\\
|
|
|
431 |
$\textit{inj}\,(r_1 \cdot r_2)\,c\,Right(v)$ & $\dn$ & $Seq(\textit{mkeps}(r_1),\textit{inj}\,r_2\,c\,v)$\\
|
|
|
432 |
$\textit{inj}\,(r^*)\,c\,Seq(v,Stars\,vs)$ & $\dn$ & $Stars((\textit{inj}\,r\,c\,v)\,::\,vs)$\\
|
|
|
433 |
\end{tabular}
|
|
|
434 |
\end{center}
|
|
|
435 |
|
|
|
436 |
\noindent This definition is by recursion on the ``shape'' of regular
|
|
|
437 |
expressions and values.
|
|
148
|
438 |
The clauses basically do one thing--identifying the ``holes'' on
|
|
|
439 |
value to inject the character back into.
|
|
|
440 |
For instance, in the last clause for injecting back to a value
|
|
|
441 |
that would turn into a new star value that corresponds to a star,
|
|
|
442 |
we know it must be a sequence value. And we know that the first
|
|
|
443 |
value of that sequence corresponds to the child regex of the star
|
|
|
444 |
with the first character being chopped off--an iteration of the star
|
|
|
445 |
that had just been unfolded. This value is followed by the already
|
|
|
446 |
matched star iterations we collected before. So we inject the character
|
|
|
447 |
back to the first value and form a new value with this new iteration
|
|
|
448 |
being added to the previous list of iterations, all under the $Stars$
|
|
|
449 |
top level.
|
|
107
|
450 |
|
|
148
|
451 |
We have mentioned before that derivatives without simplification
|
|
|
452 |
can get clumsy, and this is true for values as well--they reflect
|
|
|
453 |
the regular expressions size by definition.
|
|
107
|
454 |
|
|
148
|
455 |
One can introduce simplification on the regex and values, but have to
|
|
|
456 |
be careful in not breaking the correctness as the injection
|
|
|
457 |
function heavily relies on the structure of the regexes and values
|
|
|
458 |
being correct and match each other.
|
|
|
459 |
It can be achieved by recording some extra rectification functions
|
|
|
460 |
during the derivatives step, and applying these rectifications in
|
|
|
461 |
each run during the injection phase.
|
|
|
462 |
And we can prove that the POSIX value of how
|
|
131
|
463 |
regular expressions match strings will not be affected---although is much harder
|
|
107
|
464 |
to establish. Some initial results in this regard have been
|
|
|
465 |
obtained in \cite{AusafDyckhoffUrban2016}.
|
|
|
466 |
|
|
148
|
467 |
%Brzozowski, after giving the derivatives and simplification,
|
|
|
468 |
%did not explore lexing with simplification or he may well be
|
|
|
469 |
%stuck on an efficient simplificaiton with a proof.
|
|
|
470 |
%He went on to explore the use of derivatives together with
|
|
|
471 |
%automaton, and did not try lexing using derivatives.
|
|
131
|
472 |
|
|
148
|
473 |
We want to get rid of complex and fragile rectification of values.
|
|
|
474 |
Can we not create those intermediate values $v_1,\ldots v_n$,
|
|
|
475 |
and get the lexing information that should be already there while
|
|
|
476 |
doing derivatives in one pass, without a second phase of injection?
|
|
|
477 |
In the meantime, can we make sure that simplifications
|
|
|
478 |
are easily handled without breaking the correctness of the algorithm?
|
|
130
|
479 |
|
|
148
|
480 |
Sulzmann and Lu solved this problem by
|
|
|
481 |
introducing additional informtaion to the
|
|
|
482 |
regular expressions called \emph{bitcodes}.
|
|
130
|
483 |
|
|
148
|
484 |
\subsection*{Bit-coded Algorithm}
|
|
|
485 |
Bits and bitcodes (lists of bits) are defined as:
|
|
107
|
486 |
|
|
|
487 |
\begin{center}
|
|
114
|
488 |
$b ::= 1 \mid 0 \qquad
|
|
130
|
489 |
bs ::= [] \mid b::bs
|
|
107
|
490 |
$
|
|
|
491 |
\end{center}
|
|
|
492 |
|
|
|
493 |
\noindent
|
|
114
|
494 |
The $1$ and $0$ are not in bold in order to avoid
|
|
107
|
495 |
confusion with the regular expressions $\ZERO$ and $\ONE$. Bitcodes (or
|
|
130
|
496 |
bit-lists) can be used to encode values (or potentially incomplete values) in a
|
|
107
|
497 |
compact form. This can be straightforwardly seen in the following
|
|
|
498 |
coding function from values to bitcodes:
|
|
|
499 |
|
|
|
500 |
\begin{center}
|
|
|
501 |
\begin{tabular}{lcl}
|
|
|
502 |
$\textit{code}(\Empty)$ & $\dn$ & $[]$\\
|
|
|
503 |
$\textit{code}(\Char\,c)$ & $\dn$ & $[]$\\
|
|
114
|
504 |
$\textit{code}(\Left\,v)$ & $\dn$ & $0 :: code(v)$\\
|
|
|
505 |
$\textit{code}(\Right\,v)$ & $\dn$ & $1 :: code(v)$\\
|
|
107
|
506 |
$\textit{code}(\Seq\,v_1\,v_2)$ & $\dn$ & $code(v_1) \,@\, code(v_2)$\\
|
|
114
|
507 |
$\textit{code}(\Stars\,[])$ & $\dn$ & $[0]$\\
|
|
|
508 |
$\textit{code}(\Stars\,(v\!::\!vs))$ & $\dn$ & $1 :: code(v) \;@\;
|
|
107
|
509 |
code(\Stars\,vs)$
|
|
|
510 |
\end{tabular}
|
|
|
511 |
\end{center}
|
|
|
512 |
|
|
|
513 |
\noindent
|
|
|
514 |
Here $\textit{code}$ encodes a value into a bitcodes by converting
|
|
114
|
515 |
$\Left$ into $0$, $\Right$ into $1$, and marks the start of a non-empty
|
|
|
516 |
star iteration by $1$. The border where a local star terminates
|
|
|
517 |
is marked by $0$. This coding is lossy, as it throws away the information about
|
|
107
|
518 |
characters, and also does not encode the ``boundary'' between two
|
|
|
519 |
sequence values. Moreover, with only the bitcode we cannot even tell
|
|
114
|
520 |
whether the $1$s and $0$s are for $\Left/\Right$ or $\Stars$. The
|
|
107
|
521 |
reason for choosing this compact way of storing information is that the
|
|
|
522 |
relatively small size of bits can be easily manipulated and ``moved
|
|
|
523 |
around'' in a regular expression. In order to recover values, we will
|
|
|
524 |
need the corresponding regular expression as an extra information. This
|
|
|
525 |
means the decoding function is defined as:
|
|
|
526 |
|
|
|
527 |
|
|
|
528 |
%\begin{definition}[Bitdecoding of Values]\mbox{}
|
|
|
529 |
\begin{center}
|
|
|
530 |
\begin{tabular}{@{}l@{\hspace{1mm}}c@{\hspace{1mm}}l@{}}
|
|
|
531 |
$\textit{decode}'\,bs\,(\ONE)$ & $\dn$ & $(\Empty, bs)$\\
|
|
|
532 |
$\textit{decode}'\,bs\,(c)$ & $\dn$ & $(\Char\,c, bs)$\\
|
|
115
|
533 |
$\textit{decode}'\,(0\!::\!bs)\;(r_1 + r_2)$ & $\dn$ &
|
|
107
|
534 |
$\textit{let}\,(v, bs_1) = \textit{decode}'\,bs\,r_1\;\textit{in}\;
|
|
|
535 |
(\Left\,v, bs_1)$\\
|
|
115
|
536 |
$\textit{decode}'\,(1\!::\!bs)\;(r_1 + r_2)$ & $\dn$ &
|
|
107
|
537 |
$\textit{let}\,(v, bs_1) = \textit{decode}'\,bs\,r_2\;\textit{in}\;
|
|
|
538 |
(\Right\,v, bs_1)$\\
|
|
|
539 |
$\textit{decode}'\,bs\;(r_1\cdot r_2)$ & $\dn$ &
|
|
|
540 |
$\textit{let}\,(v_1, bs_1) = \textit{decode}'\,bs\,r_1\;\textit{in}$\\
|
|
|
541 |
& & $\textit{let}\,(v_2, bs_2) = \textit{decode}'\,bs_1\,r_2$\\
|
|
|
542 |
& & \hspace{35mm}$\textit{in}\;(\Seq\,v_1\,v_2, bs_2)$\\
|
|
115
|
543 |
$\textit{decode}'\,(0\!::\!bs)\,(r^*)$ & $\dn$ & $(\Stars\,[], bs)$\\
|
|
|
544 |
$\textit{decode}'\,(1\!::\!bs)\,(r^*)$ & $\dn$ &
|
|
107
|
545 |
$\textit{let}\,(v, bs_1) = \textit{decode}'\,bs\,r\;\textit{in}$\\
|
|
|
546 |
& & $\textit{let}\,(\Stars\,vs, bs_2) = \textit{decode}'\,bs_1\,r^*$\\
|
|
|
547 |
& & \hspace{35mm}$\textit{in}\;(\Stars\,v\!::\!vs, bs_2)$\bigskip\\
|
|
|
548 |
|
|
|
549 |
$\textit{decode}\,bs\,r$ & $\dn$ &
|
|
|
550 |
$\textit{let}\,(v, bs') = \textit{decode}'\,bs\,r\;\textit{in}$\\
|
|
|
551 |
& & $\textit{if}\;bs' = []\;\textit{then}\;\textit{Some}\,v\;
|
|
|
552 |
\textit{else}\;\textit{None}$
|
|
|
553 |
\end{tabular}
|
|
|
554 |
\end{center}
|
|
|
555 |
%\end{definition}
|
|
|
556 |
|
|
|
557 |
Sulzmann and Lu's integrated the bitcodes into regular expressions to
|
|
|
558 |
create annotated regular expressions \cite{Sulzmann2014}.
|
|
|
559 |
\emph{Annotated regular expressions} are defined by the following
|
|
|
560 |
grammar:%\comment{ALTS should have an $as$ in the definitions, not just $a_1$ and $a_2$}
|
|
|
561 |
|
|
|
562 |
\begin{center}
|
|
|
563 |
\begin{tabular}{lcl}
|
|
115
|
564 |
$\textit{a}$ & $::=$ & $\ZERO$\\
|
|
|
565 |
& $\mid$ & $_{bs}\ONE$\\
|
|
|
566 |
& $\mid$ & $_{bs}{\bf c}$\\
|
|
132
|
567 |
& $\mid$ & $_{bs}\sum\,as$\\
|
|
115
|
568 |
& $\mid$ & $_{bs}a_1\cdot a_2$\\
|
|
|
569 |
& $\mid$ & $_{bs}a^*$
|
|
107
|
570 |
\end{tabular}
|
|
|
571 |
\end{center}
|
|
|
572 |
%(in \textit{ALTS})
|
|
|
573 |
|
|
|
574 |
\noindent
|
|
|
575 |
where $bs$ stands for bitcodes, $a$ for $\bold{a}$nnotated regular
|
|
|
576 |
expressions and $as$ for a list of annotated regular expressions.
|
|
132
|
577 |
The alternative constructor($\sum$) has been generalized to
|
|
107
|
578 |
accept a list of annotated regular expressions rather than just 2.
|
|
|
579 |
We will show that these bitcodes encode information about
|
|
|
580 |
the (POSIX) value that should be generated by the Sulzmann and Lu
|
|
|
581 |
algorithm.
|
|
|
582 |
|
|
|
583 |
|
|
|
584 |
To do lexing using annotated regular expressions, we shall first
|
|
|
585 |
transform the usual (un-annotated) regular expressions into annotated
|
|
|
586 |
regular expressions. This operation is called \emph{internalisation} and
|
|
|
587 |
defined as follows:
|
|
|
588 |
|
|
|
589 |
%\begin{definition}
|
|
|
590 |
\begin{center}
|
|
|
591 |
\begin{tabular}{lcl}
|
|
116
|
592 |
$(\ZERO)^\uparrow$ & $\dn$ & $\ZERO$\\
|
|
|
593 |
$(\ONE)^\uparrow$ & $\dn$ & $_{[]}\ONE$\\
|
|
|
594 |
$(c)^\uparrow$ & $\dn$ & $_{[]}{\bf c}$\\
|
|
107
|
595 |
$(r_1 + r_2)^\uparrow$ & $\dn$ &
|
|
132
|
596 |
$_{[]}\sum[\textit{fuse}\,[0]\,r_1^\uparrow,\,
|
|
116
|
597 |
\textit{fuse}\,[1]\,r_2^\uparrow]$\\
|
|
107
|
598 |
$(r_1\cdot r_2)^\uparrow$ & $\dn$ &
|
|
116
|
599 |
$_{[]}r_1^\uparrow \cdot r_2^\uparrow$\\
|
|
107
|
600 |
$(r^*)^\uparrow$ & $\dn$ &
|
|
116
|
601 |
$_{[]}(r^\uparrow)^*$\\
|
|
107
|
602 |
\end{tabular}
|
|
|
603 |
\end{center}
|
|
|
604 |
%\end{definition}
|
|
|
605 |
|
|
|
606 |
\noindent
|
|
|
607 |
We use up arrows here to indicate that the basic un-annotated regular
|
|
|
608 |
expressions are ``lifted up'' into something slightly more complex. In the
|
|
|
609 |
fourth clause, $\textit{fuse}$ is an auxiliary function that helps to
|
|
|
610 |
attach bits to the front of an annotated regular expression. Its
|
|
|
611 |
definition is as follows:
|
|
|
612 |
|
|
|
613 |
\begin{center}
|
|
|
614 |
\begin{tabular}{lcl}
|
|
117
|
615 |
$\textit{fuse}\;bs \; \ZERO$ & $\dn$ & $\ZERO$\\
|
|
|
616 |
$\textit{fuse}\;bs\; _{bs'}\ONE$ & $\dn$ &
|
|
|
617 |
$_{bs @ bs'}\ONE$\\
|
|
|
618 |
$\textit{fuse}\;bs\;_{bs'}{\bf c}$ & $\dn$ &
|
|
|
619 |
$_{bs@bs'}{\bf c}$\\
|
|
132
|
620 |
$\textit{fuse}\;bs\,_{bs'}\sum\textit{as}$ & $\dn$ &
|
|
|
621 |
$_{bs@bs'}\sum\textit{as}$\\
|
|
117
|
622 |
$\textit{fuse}\;bs\; _{bs'}a_1\cdot a_2$ & $\dn$ &
|
|
|
623 |
$_{bs@bs'}a_1 \cdot a_2$\\
|
|
|
624 |
$\textit{fuse}\;bs\,_{bs'}a^*$ & $\dn$ &
|
|
|
625 |
$_{bs @ bs'}a^*$
|
|
107
|
626 |
\end{tabular}
|
|
|
627 |
\end{center}
|
|
|
628 |
|
|
|
629 |
\noindent
|
|
|
630 |
After internalising the regular expression, we perform successive
|
|
|
631 |
derivative operations on the annotated regular expressions. This
|
|
|
632 |
derivative operation is the same as what we had previously for the
|
|
|
633 |
basic regular expressions, except that we beed to take care of
|
|
|
634 |
the bitcodes:
|
|
|
635 |
|
|
109
|
636 |
|
|
|
637 |
\iffalse
|
|
107
|
638 |
%\begin{definition}{bder}
|
|
|
639 |
\begin{center}
|
|
|
640 |
\begin{tabular}{@{}lcl@{}}
|
|
|
641 |
$(\textit{ZERO})\,\backslash c$ & $\dn$ & $\textit{ZERO}$\\
|
|
|
642 |
$(\textit{ONE}\;bs)\,\backslash c$ & $\dn$ & $\textit{ZERO}$\\
|
|
|
643 |
$(\textit{CHAR}\;bs\,d)\,\backslash c$ & $\dn$ &
|
|
|
644 |
$\textit{if}\;c=d\; \;\textit{then}\;
|
|
|
645 |
\textit{ONE}\;bs\;\textit{else}\;\textit{ZERO}$\\
|
|
|
646 |
$(\textit{ALTS}\;bs\,as)\,\backslash c$ & $\dn$ &
|
|
|
647 |
$\textit{ALTS}\;bs\,(as.map(\backslash c))$\\
|
|
|
648 |
$(\textit{SEQ}\;bs\,a_1\,a_2)\,\backslash c$ & $\dn$ &
|
|
|
649 |
$\textit{if}\;\textit{bnullable}\,a_1$\\
|
|
|
650 |
& &$\textit{then}\;\textit{ALTS}\,bs\,List((\textit{SEQ}\,[]\,(a_1\,\backslash c)\,a_2),$\\
|
|
|
651 |
& &$\phantom{\textit{then}\;\textit{ALTS}\,bs\,}(\textit{fuse}\,(\textit{bmkeps}\,a_1)\,(a_2\,\backslash c)))$\\
|
|
|
652 |
& &$\textit{else}\;\textit{SEQ}\,bs\,(a_1\,\backslash c)\,a_2$\\
|
|
|
653 |
$(\textit{STAR}\,bs\,a)\,\backslash c$ & $\dn$ &
|
|
|
654 |
$\textit{SEQ}\;bs\,(\textit{fuse}\, [\Z] (r\,\backslash c))\,
|
|
|
655 |
(\textit{STAR}\,[]\,r)$
|
|
|
656 |
\end{tabular}
|
|
|
657 |
\end{center}
|
|
|
658 |
%\end{definition}
|
|
|
659 |
|
|
109
|
660 |
\begin{center}
|
|
|
661 |
\begin{tabular}{@{}lcl@{}}
|
|
|
662 |
$(\textit{ZERO})\,\backslash c$ & $\dn$ & $\textit{ZERO}$\\
|
|
|
663 |
$(_{bs}\textit{ONE})\,\backslash c$ & $\dn$ & $\textit{ZERO}$\\
|
|
|
664 |
$(_{bs}\textit{CHAR}\;d)\,\backslash c$ & $\dn$ &
|
|
|
665 |
$\textit{if}\;c=d\; \;\textit{then}\;
|
|
|
666 |
_{bs}\textit{ONE}\;\textit{else}\;\textit{ZERO}$\\
|
|
118
|
667 |
$(_{bs}\textit{ALTS}\;\textit{as})\,\backslash c$ & $\dn$ &
|
|
|
668 |
$_{bs}\textit{ALTS}\;(\textit{as}.\textit{map}(\backslash c))$\\
|
|
109
|
669 |
$(_{bs}\textit{SEQ}\;a_1\,a_2)\,\backslash c$ & $\dn$ &
|
|
|
670 |
$\textit{if}\;\textit{bnullable}\,a_1$\\
|
|
|
671 |
& &$\textit{then}\;_{bs}\textit{ALTS}\,List((_{[]}\textit{SEQ}\,(a_1\,\backslash c)\,a_2),$\\
|
|
|
672 |
& &$\phantom{\textit{then}\;_{bs}\textit{ALTS}\,}(\textit{fuse}\,(\textit{bmkeps}\,a_1)\,(a_2\,\backslash c)))$\\
|
|
|
673 |
& &$\textit{else}\;_{bs}\textit{SEQ}\,(a_1\,\backslash c)\,a_2$\\
|
|
|
674 |
$(_{bs}\textit{STAR}\,a)\,\backslash c$ & $\dn$ &
|
|
118
|
675 |
$_{bs}\textit{SEQ}\;(\textit{fuse}\, [0] \; r\,\backslash c )\,
|
|
109
|
676 |
(_{bs}\textit{STAR}\,[]\,r)$
|
|
|
677 |
\end{tabular}
|
|
|
678 |
\end{center}
|
|
|
679 |
%\end{definition}
|
|
|
680 |
\fi
|
|
|
681 |
|
|
|
682 |
\begin{center}
|
|
|
683 |
\begin{tabular}{@{}lcl@{}}
|
|
|
684 |
$(\ZERO)\,\backslash c$ & $\dn$ & $\ZERO$\\
|
|
|
685 |
$(_{bs}\ONE)\,\backslash c$ & $\dn$ & $\ZERO$\\
|
|
|
686 |
$(_{bs}{\bf d})\,\backslash c$ & $\dn$ &
|
|
|
687 |
$\textit{if}\;c=d\; \;\textit{then}\;
|
|
|
688 |
_{bs}\ONE\;\textit{else}\;\ZERO$\\
|
|
132
|
689 |
$(_{bs}\sum \;\textit{as})\,\backslash c$ & $\dn$ &
|
|
|
690 |
$_{bs}\sum\;(\textit{as.map}(\backslash c))$\\
|
|
109
|
691 |
$(_{bs}\;a_1\cdot a_2)\,\backslash c$ & $\dn$ &
|
|
|
692 |
$\textit{if}\;\textit{bnullable}\,a_1$\\
|
|
132
|
693 |
& &$\textit{then}\;_{bs}\sum\,[(_{[]}\,(a_1\,\backslash c)\cdot\,a_2),$\\
|
|
|
694 |
& &$\phantom{\textit{then},\;_{bs}\sum\,}(\textit{fuse}\,(\textit{bmkeps}\,a_1)\,(a_2\,\backslash c))]$\\
|
|
109
|
695 |
& &$\textit{else}\;_{bs}\,(a_1\,\backslash c)\cdot a_2$\\
|
|
|
696 |
$(_{bs}a^*)\,\backslash c$ & $\dn$ &
|
|
119
|
697 |
$_{bs}(\textit{fuse}\, [0] \; r\,\backslash c)\cdot
|
|
109
|
698 |
(_{[]}r^*))$
|
|
|
699 |
\end{tabular}
|
|
|
700 |
\end{center}
|
|
|
701 |
|
|
|
702 |
%\end{definition}
|
|
107
|
703 |
\noindent
|
|
119
|
704 |
For instance, when we do derivative of $_{bs}a^*$ with respect to c,
|
|
|
705 |
we need to unfold it into a sequence,
|
|
|
706 |
and attach an additional bit $0$ to the front of $r \backslash c$
|
|
118
|
707 |
to indicate that there is one more star iteration. Also the sequence clause
|
|
107
|
708 |
is more subtle---when $a_1$ is $\textit{bnullable}$ (here
|
|
|
709 |
\textit{bnullable} is exactly the same as $\textit{nullable}$, except
|
|
|
710 |
that it is for annotated regular expressions, therefore we omit the
|
|
118
|
711 |
definition). Assume that $\textit{bmkeps}$ correctly extracts the bitcode for how
|
|
107
|
712 |
$a_1$ matches the string prior to character $c$ (more on this later),
|
|
118
|
713 |
then the right branch of alternative, which is $\textit{fuse} \; \bmkeps \; a_1 (a_2
|
|
107
|
714 |
\backslash c)$ will collapse the regular expression $a_1$(as it has
|
|
|
715 |
already been fully matched) and store the parsing information at the
|
|
|
716 |
head of the regular expression $a_2 \backslash c$ by fusing to it. The
|
|
118
|
717 |
bitsequence $\textit{bs}$, which was initially attached to the
|
|
|
718 |
first element of the sequence $a_1 \cdot a_2$, has
|
|
132
|
719 |
now been elevated to the top-level of $\sum$, as this information will be
|
|
118
|
720 |
needed whichever way the sequence is matched---no matter whether $c$ belongs
|
|
107
|
721 |
to $a_1$ or $ a_2$. After building these derivatives and maintaining all
|
|
|
722 |
the lexing information, we complete the lexing by collecting the
|
|
|
723 |
bitcodes using a generalised version of the $\textit{mkeps}$ function
|
|
|
724 |
for annotated regular expressions, called $\textit{bmkeps}$:
|
|
|
725 |
|
|
|
726 |
|
|
|
727 |
%\begin{definition}[\textit{bmkeps}]\mbox{}
|
|
|
728 |
\begin{center}
|
|
|
729 |
\begin{tabular}{lcl}
|
|
119
|
730 |
$\textit{bmkeps}\,(_{bs}\ONE)$ & $\dn$ & $bs$\\
|
|
132
|
731 |
$\textit{bmkeps}\,(_{bs}\sum a::\textit{as})$ & $\dn$ &
|
|
107
|
732 |
$\textit{if}\;\textit{bnullable}\,a$\\
|
|
|
733 |
& &$\textit{then}\;bs\,@\,\textit{bmkeps}\,a$\\
|
|
132
|
734 |
& &$\textit{else}\;bs\,@\,\textit{bmkeps}\,(_{bs}\sum \textit{as})$\\
|
|
120
|
735 |
$\textit{bmkeps}\,(_{bs} a_1 \cdot a_2)$ & $\dn$ &
|
|
107
|
736 |
$bs \,@\,\textit{bmkeps}\,a_1\,@\, \textit{bmkeps}\,a_2$\\
|
|
119
|
737 |
$\textit{bmkeps}\,(_{bs}a^*)$ & $\dn$ &
|
|
121
|
738 |
$bs \,@\, [0]$
|
|
107
|
739 |
\end{tabular}
|
|
|
740 |
\end{center}
|
|
|
741 |
%\end{definition}
|
|
|
742 |
|
|
|
743 |
\noindent
|
|
|
744 |
This function completes the value information by travelling along the
|
|
|
745 |
path of the regular expression that corresponds to a POSIX value and
|
|
|
746 |
collecting all the bitcodes, and using $S$ to indicate the end of star
|
|
|
747 |
iterations. If we take the bitcodes produced by $\textit{bmkeps}$ and
|
|
|
748 |
decode them, we get the value we expect. The corresponding lexing
|
|
|
749 |
algorithm looks as follows:
|
|
|
750 |
|
|
|
751 |
\begin{center}
|
|
|
752 |
\begin{tabular}{lcl}
|
|
|
753 |
$\textit{blexer}\;r\,s$ & $\dn$ &
|
|
|
754 |
$\textit{let}\;a = (r^\uparrow)\backslash s\;\textit{in}$\\
|
|
|
755 |
& & $\;\;\textit{if}\; \textit{bnullable}(a)$\\
|
|
|
756 |
& & $\;\;\textit{then}\;\textit{decode}\,(\textit{bmkeps}\,a)\,r$\\
|
|
|
757 |
& & $\;\;\textit{else}\;\textit{None}$
|
|
|
758 |
\end{tabular}
|
|
|
759 |
\end{center}
|
|
|
760 |
|
|
|
761 |
\noindent
|
|
|
762 |
In this definition $\_\backslash s$ is the generalisation of the derivative
|
|
|
763 |
operation from characters to strings (just like the derivatives for un-annotated
|
|
|
764 |
regular expressions).
|
|
|
765 |
|
|
148
|
766 |
Remember tha one of the important reasons we introduced bitcodes
|
|
|
767 |
is that they can make simplification more structured and therefore guaranteeing
|
|
|
768 |
the correctness.
|
|
108
|
769 |
|
|
|
770 |
\subsection*{Our Simplification Rules}
|
|
|
771 |
|
|
148
|
772 |
In this section we introduce aggressive (in terms of size) simplification rules
|
|
|
773 |
on annotated regular expressions
|
|
|
774 |
in order to keep derivatives small. Such simplifications are promising
|
|
|
775 |
as we have
|
|
|
776 |
generated test data that show
|
|
|
777 |
that a good tight bound can be achieved. Obviously we could only
|
|
107
|
778 |
partially cover the search space as there are infinitely many regular
|
|
|
779 |
expressions and strings.
|
|
|
780 |
|
|
|
781 |
One modification we introduced is to allow a list of annotated regular
|
|
132
|
782 |
expressions in the $\sum$ constructor. This allows us to not just
|
|
107
|
783 |
delete unnecessary $\ZERO$s and $\ONE$s from regular expressions, but
|
|
|
784 |
also unnecessary ``copies'' of regular expressions (very similar to
|
|
|
785 |
simplifying $r + r$ to just $r$, but in a more general setting). Another
|
|
|
786 |
modification is that we use simplification rules inspired by Antimirov's
|
|
|
787 |
work on partial derivatives. They maintain the idea that only the first
|
|
|
788 |
``copy'' of a regular expression in an alternative contributes to the
|
|
|
789 |
calculation of a POSIX value. All subsequent copies can be pruned away from
|
|
|
790 |
the regular expression. A recursive definition of our simplification function
|
|
|
791 |
that looks somewhat similar to our Scala code is given below:
|
|
|
792 |
%\comment{Use $\ZERO$, $\ONE$ and so on.
|
|
|
793 |
%Is it $ALTS$ or $ALTS$?}\\
|
|
|
794 |
|
|
|
795 |
\begin{center}
|
|
|
796 |
\begin{tabular}{@{}lcl@{}}
|
|
|
797 |
|
|
121
|
798 |
$\textit{simp} \; (_{bs}a_1\cdot a_2)$ & $\dn$ & $ (\textit{simp} \; a_1, \textit{simp} \; a_2) \; \textit{match} $ \\
|
|
107
|
799 |
&&$\quad\textit{case} \; (\ZERO, \_) \Rightarrow \ZERO$ \\
|
|
|
800 |
&&$\quad\textit{case} \; (\_, \ZERO) \Rightarrow \ZERO$ \\
|
|
|
801 |
&&$\quad\textit{case} \; (\ONE, a_2') \Rightarrow \textit{fuse} \; bs \; a_2'$ \\
|
|
|
802 |
&&$\quad\textit{case} \; (a_1', \ONE) \Rightarrow \textit{fuse} \; bs \; a_1'$ \\
|
|
121
|
803 |
&&$\quad\textit{case} \; (a_1', a_2') \Rightarrow _{bs}a_1' \cdot a_2'$ \\
|
|
107
|
804 |
|
|
133
|
805 |
$\textit{simp} \; (_{bs}\sum \textit{as})$ & $\dn$ & $\textit{distinct}( \textit{flatten} ( \textit{as.map(simp)})) \; \textit{match} $ \\
|
|
107
|
806 |
&&$\quad\textit{case} \; [] \Rightarrow \ZERO$ \\
|
|
|
807 |
&&$\quad\textit{case} \; a :: [] \Rightarrow \textit{fuse bs a}$ \\
|
|
132
|
808 |
&&$\quad\textit{case} \; as' \Rightarrow _{bs}\sum \textit{as'}$\\
|
|
107
|
809 |
|
|
|
810 |
$\textit{simp} \; a$ & $\dn$ & $\textit{a} \qquad \textit{otherwise}$
|
|
|
811 |
\end{tabular}
|
|
|
812 |
\end{center}
|
|
|
813 |
|
|
|
814 |
\noindent
|
|
|
815 |
The simplification does a pattern matching on the regular expression.
|
|
|
816 |
When it detected that the regular expression is an alternative or
|
|
|
817 |
sequence, it will try to simplify its children regular expressions
|
|
|
818 |
recursively and then see if one of the children turn into $\ZERO$ or
|
|
|
819 |
$\ONE$, which might trigger further simplification at the current level.
|
|
132
|
820 |
The most involved part is the $\sum$ clause, where we use two
|
|
107
|
821 |
auxiliary functions $\textit{flatten}$ and $\textit{distinct}$ to open up nested
|
|
121
|
822 |
alternatives and reduce as many duplicates as possible. Function
|
|
107
|
823 |
$\textit{distinct}$ keeps the first occurring copy only and remove all later ones
|
|
132
|
824 |
when detected duplicates. Function $\textit{flatten}$ opens up nested $\sum$s.
|
|
107
|
825 |
Its recursive definition is given below:
|
|
|
826 |
|
|
|
827 |
\begin{center}
|
|
|
828 |
\begin{tabular}{@{}lcl@{}}
|
|
132
|
829 |
$\textit{flatten} \; (_{bs}\sum \textit{as}) :: \textit{as'}$ & $\dn$ & $(\textit{map} \;
|
|
107
|
830 |
(\textit{fuse}\;bs)\; \textit{as}) \; @ \; \textit{flatten} \; as' $ \\
|
|
121
|
831 |
$\textit{flatten} \; \ZERO :: as'$ & $\dn$ & $ \textit{flatten} \; \textit{as'} $ \\
|
|
|
832 |
$\textit{flatten} \; a :: as'$ & $\dn$ & $a :: \textit{flatten} \; \textit{as'}$ \quad(otherwise)
|
|
107
|
833 |
\end{tabular}
|
|
|
834 |
\end{center}
|
|
|
835 |
|
|
|
836 |
\noindent
|
|
|
837 |
Here $\textit{flatten}$ behaves like the traditional functional programming flatten
|
|
|
838 |
function, except that it also removes $\ZERO$s. Or in terms of regular expressions, it
|
|
|
839 |
removes parentheses, for example changing $a+(b+c)$ into $a+b+c$.
|
|
|
840 |
|
|
131
|
841 |
Having defined the $\simp$ function,
|
|
|
842 |
we can use the previous notation of natural
|
|
|
843 |
extension from derivative w.r.t.~character to derivative
|
|
|
844 |
w.r.t.~string:%\comment{simp in the [] case?}
|
|
|
845 |
|
|
|
846 |
\begin{center}
|
|
|
847 |
\begin{tabular}{lcl}
|
|
|
848 |
$r \backslash_{simp} (c\!::\!s) $ & $\dn$ & $(r \backslash_{simp}\, c) \backslash_{simp}\, s$ \\
|
|
|
849 |
$r \backslash_{simp} [\,] $ & $\dn$ & $r$
|
|
|
850 |
\end{tabular}
|
|
|
851 |
\end{center}
|
|
|
852 |
|
|
|
853 |
\noindent
|
|
|
854 |
to obtain an optimised version of the algorithm:
|
|
|
855 |
|
|
|
856 |
\begin{center}
|
|
|
857 |
\begin{tabular}{lcl}
|
|
|
858 |
$\textit{blexer\_simp}\;r\,s$ & $\dn$ &
|
|
|
859 |
$\textit{let}\;a = (r^\uparrow)\backslash_{simp}\, s\;\textit{in}$\\
|
|
|
860 |
& & $\;\;\textit{if}\; \textit{bnullable}(a)$\\
|
|
|
861 |
& & $\;\;\textit{then}\;\textit{decode}\,(\textit{bmkeps}\,a)\,r$\\
|
|
|
862 |
& & $\;\;\textit{else}\;\textit{None}$
|
|
|
863 |
\end{tabular}
|
|
|
864 |
\end{center}
|
|
|
865 |
|
|
|
866 |
\noindent
|
|
|
867 |
This algorithm keeps the regular expression size small, for example,
|
|
|
868 |
with this simplification our previous $(a + aa)^*$ example's 8000 nodes
|
|
|
869 |
will be reduced to just 6 and stays constant, no matter how long the
|
|
|
870 |
input string is.
|
|
107
|
871 |
|
|
|
872 |
|
|
|
873 |
|
|
126
|
874 |
\section{Current Work and Progress}
|
|
105
|
875 |
For reasons beyond this report, it turns out that a complete set of
|
|
|
876 |
simplification rules depends on values being encoded as
|
|
|
877 |
bitsequences.\footnote{Values are the results the lexing algorithms
|
|
|
878 |
generate; they encode how a regular expression matched a string.} We
|
|
|
879 |
already know that the lexing algorithm using bitsequences but
|
|
|
880 |
\emph{without} simplification is correct, albeilt horribly
|
|
106
|
881 |
slow. Therefore in the past 6 months I was trying to prove that the
|
|
105
|
882 |
algorithm using bitsequences plus our simplification rules is
|
|
106
|
883 |
also correct. Formally this amounts to show that
|
|
100
|
884 |
|
|
|
885 |
\begin{equation}\label{mainthm}
|
|
|
886 |
\blexers \; r \; s = \blexer \;r\;s
|
|
|
887 |
\end{equation}
|
|
|
888 |
|
|
94
|
889 |
\noindent
|
|
105
|
890 |
whereby $\blexers$ simplifies (makes derivatives smaller) in each
|
|
145
|
891 |
step. This
|
|
106
|
892 |
would be an important milestone for my thesis, because we already
|
|
105
|
893 |
have a very good idea how to establish that our set our simplification
|
|
145
|
894 |
rules keep the size of derivatives below a relatively tight bound.
|
|
100
|
895 |
|
|
106
|
896 |
In order to prove the main theorem in \eqref{mainthm}, we need to prove that the
|
|
|
897 |
two functions produce the same output. The definition of these two functions
|
|
100
|
898 |
is shown below.
|
|
|
899 |
|
|
94
|
900 |
\begin{center}
|
|
|
901 |
\begin{tabular}{lcl}
|
|
|
902 |
$\textit{blexer}\;r\,s$ & $\dn$ &
|
|
|
903 |
$\textit{let}\;a = (r^\uparrow)\backslash s\;\textit{in}$\\
|
|
|
904 |
& & $\;\;\textit{if}\; \textit{bnullable}(a)$\\
|
|
|
905 |
& & $\;\;\textit{then}\;\textit{decode}\,(\textit{bmkeps}\,a)\,r$\\
|
|
|
906 |
& & $\;\;\textit{else}\;\textit{None}$
|
|
|
907 |
\end{tabular}
|
|
|
908 |
\end{center}
|
|
|
909 |
|
|
100
|
910 |
\begin{center}
|
|
94
|
911 |
\begin{tabular}{lcl}
|
|
100
|
912 |
$\blexers \; r \, s$ &$\dn$ &
|
|
|
913 |
$\textit{let} \; a = (r^\uparrow)\backslash_{simp}\, s\; \textit{in}$\\
|
|
|
914 |
& & $\; \; \textit{if} \; \textit{bnullable}(a)$\\
|
|
|
915 |
& & $\; \; \textit{then} \; \textit{decode}\,(\textit{bmkeps}\,a)\,r$\\
|
|
|
916 |
& & $\;\; \textit{else}\;\textit{None}$
|
|
94
|
917 |
\end{tabular}
|
|
|
918 |
\end{center}
|
|
|
919 |
\noindent
|
|
105
|
920 |
In these definitions $(r^\uparrow)$ is a kind of coding function that
|
|
|
921 |
is the same in each case, similarly the decode and the \textit{bmkeps}
|
|
106
|
922 |
are functions that are the same in each case. Our main
|
|
|
923 |
theorem~\eqref{mainthm} therefore boils down to proving the following
|
|
|
924 |
two propositions (depending on which branch the if-else clause
|
|
|
925 |
takes). They establish how the derivatives \emph{with} simplification
|
|
|
926 |
do not change the computed result:
|
|
94
|
927 |
|
|
|
928 |
\begin{itemize}
|
|
105
|
929 |
\item{(a)} If a string $s$ is in the language of $L(r)$, then \\
|
|
100
|
930 |
$\textit{bmkeps} (r^\uparrow)\backslash_{simp}\,s = \textit{bmkeps} (r^\uparrow)\backslash s$,\\
|
|
105
|
931 |
\item{(b)} If a string $s$ is in the language $L(r)$, then
|
|
100
|
932 |
$\rup \backslash_{simp} \,s$ is not nullable.
|
|
94
|
933 |
\end{itemize}
|
|
100
|
934 |
|
|
94
|
935 |
\noindent
|
|
106
|
936 |
We have already proved the second part in Isabelle. This is actually
|
|
105
|
937 |
not too difficult because we can show that simplification does not
|
|
|
938 |
change the language of simplified regular expressions.
|
|
100
|
939 |
|
|
105
|
940 |
If we can prove the first part, that is the bitsequence algorithm with
|
|
|
941 |
simplification produces the same result as the one without
|
|
|
942 |
simplification, then we are done. Unfortunately that part requires
|
|
|
943 |
more effort, because simplification does not only need to \emph{not}
|
|
|
944 |
change the language, but also not change the value (that is the
|
|
|
945 |
computed result).
|
|
100
|
946 |
|
|
105
|
947 |
%\bigskip\noindent\rule[1.5ex]{\linewidth}{5pt}
|
|
|
948 |
%Do you want to keep this? You essentially want to say that the old
|
|
|
949 |
%method used retrieve, which unfortunately cannot be adopted to
|
|
|
950 |
%the simplification rules. You could just say that and give an example.
|
|
|
951 |
%However you have to think about how you give the example....nobody knows
|
|
|
952 |
%about AZERO etc yet. Maybe it might be better to use normal regexes
|
|
|
953 |
%like $a + aa$, but annotate bitsequences as subscript like $_1(_0a + _1aa)$.
|
|
104
|
954 |
|
|
105
|
955 |
%\bigskip\noindent\rule[1.5ex]{\linewidth}{5pt}
|
|
|
956 |
%REPLY:\\
|
|
|
957 |
%Yes, I am essentially saying that the old method
|
|
|
958 |
%cannot be adopted without adjustments.
|
|
|
959 |
%But this does not mean we should skip
|
|
|
960 |
%the proof of the bit-coded algorithm
|
|
|
961 |
%as it is still the main direction we are looking into
|
|
|
962 |
%to prove things. We are trying to modify
|
|
|
963 |
%the old proof to suit our needs, but not give
|
|
|
964 |
%up it totally, that is why i believe the old
|
|
|
965 |
%proof is fundamental in understanding
|
|
|
966 |
%what we are doing in the past 6 months.
|
|
|
967 |
%\bigskip\noindent\rule[1.5ex]{\linewidth}{5pt}
|
|
100
|
968 |
|
|
106
|
969 |
\subsubsection*{Existing Proof}
|
|
100
|
970 |
|
|
134
|
971 |
For this we have started with looking at the proof of
|
|
105
|
972 |
\begin{equation}\label{lexer}
|
|
134
|
973 |
\blexer \; (r^\uparrow) s = \lexer \;r \;s,
|
|
105
|
974 |
\end{equation}
|
|
|
975 |
|
|
|
976 |
%\noindent
|
|
|
977 |
%might provide us insight into proving
|
|
|
978 |
%\begin{center}
|
|
|
979 |
%$\blexer \; r^\uparrow \;s = \blexers \; r^\uparrow \;s$
|
|
|
980 |
%\end{center}
|
|
104
|
981 |
|
|
94
|
982 |
\noindent
|
|
143
|
983 |
which established that the bit-sequence algorithm produces the same
|
|
134
|
984 |
result as the original algorithm, which does not use
|
|
145
|
985 |
bit-sequences.
|
|
106
|
986 |
The proof uses two ``tricks''. One is that it uses a \flex-function
|
|
104
|
987 |
|
|
94
|
988 |
\begin{center}
|
|
|
989 |
\begin{tabular}{lcl}
|
|
|
990 |
$\textit{flex} \;r\; f\; (c\!::\!s) $ & $\dn$ & $\textit{flex} \; (r\backslash c) \;(\lambda v. f (inj \; r \; c \; v)) \;s$ \\
|
|
|
991 |
$\textit{flex} \;r\; f\; [\,] $ & $\dn$ & $f$
|
|
|
992 |
\end{tabular}
|
|
|
993 |
\end{center}
|
|
104
|
994 |
|
|
94
|
995 |
\noindent
|
|
134
|
996 |
to prove for the right-hand side in \eqref{lexer}
|
|
104
|
997 |
|
|
|
998 |
\begin{center}
|
|
134
|
999 |
$\lexer \;r\; s = \flex \;\textit{id} \; r\;s \;(\mkeps \; (r\backslash s))$.
|
|
|
1000 |
\end{center}
|
|
104
|
1001 |
|
|
106
|
1002 |
|
|
104
|
1003 |
|
|
|
1004 |
\noindent
|
|
144
|
1005 |
This property links $\flex$ and $\lexer$,
|
|
134
|
1006 |
it essentially does lexing by
|
|
|
1007 |
stacking up injection functions while doing derivatives,
|
|
94
|
1008 |
explicitly showing the order of characters being
|
|
|
1009 |
injected back in each step.
|
|
106
|
1010 |
|
|
94
|
1011 |
\noindent
|
|
135
|
1012 |
The other trick, which is the crux in the existing proof,
|
|
144
|
1013 |
is the use of the $\retrieve$-function by Sulzmann and Lu:
|
|
107
|
1014 |
\begin{center}
|
|
|
1015 |
\begin{tabular}{@{}l@{\hspace{2mm}}c@{\hspace{2mm}}l@{}}
|
|
110
|
1016 |
$\textit{retrieve}\,(_{bs}\ONE)\,\Empty$ & $\dn$ & $bs$\\
|
|
|
1017 |
$\textit{retrieve}\,(_{bs}{\bf c})\,(\Char\,d)$ & $\dn$ & $bs$\\
|
|
132
|
1018 |
$\textit{retrieve}\,(_{bs}\sum a::as)\,(\Left\,v)$ & $\dn$ &
|
|
107
|
1019 |
$bs \,@\, \textit{retrieve}\,a\,v$\\
|
|
132
|
1020 |
$\textit{retrieve}\,(_{bs}\sum a::as)\,(\Right\,v)$ & $\dn$ &
|
|
|
1021 |
$\textit{bs} \,@\, \textit{retrieve}\,(_{[]}\sum as)\,v$\\
|
|
121
|
1022 |
$\textit{retrieve}\,(_{bs}a_1\cdot a_2)\,(\Seq\,v_1\,v_2)$ & $\dn$ &
|
|
107
|
1023 |
$bs \,@\,\textit{retrieve}\,a_1\,v_1\,@\, \textit{retrieve}\,a_2\,v_2$\\
|
|
121
|
1024 |
$\textit{retrieve}\,(_{bs}a^*)\,(\Stars\,[])$ & $\dn$ &
|
|
|
1025 |
$bs \,@\, [0]$\\
|
|
|
1026 |
$\textit{retrieve}\,(_{bs}a^*)\,(\Stars\,(v\!::\!vs))$ & $\dn$ &\\
|
|
107
|
1027 |
\multicolumn{3}{l}{
|
|
121
|
1028 |
\hspace{3cm}$bs \,@\, [1] \,@\, \textit{retrieve}\,a\,v\,@\,
|
|
|
1029 |
\textit{retrieve}\,(_{[]}a^*)\,(\Stars\,vs)$}\\
|
|
107
|
1030 |
\end{tabular}
|
|
|
1031 |
\end{center}
|
|
135
|
1032 |
|
|
|
1033 |
\noindent
|
|
107
|
1034 |
This function assembles the bitcode
|
|
|
1035 |
using information from both the derivative regular expression and the
|
|
135
|
1036 |
value. Sulzmann and Lu proposed this function, but did not prove
|
|
144
|
1037 |
anything about it. Ausaf and Urban made use of the
|
|
|
1038 |
fact about $\retrieve$ in their proof:
|
|
107
|
1039 |
|
|
135
|
1040 |
\begin{center}
|
|
144
|
1041 |
$\retrieve\; \rup \backslash c \; v = \retrieve \; \rup (\inj \;r \;c \; v)$
|
|
107
|
1042 |
\end{center}
|
|
|
1043 |
|
|
|
1044 |
\noindent
|
|
135
|
1045 |
whereby $r^\uparrow$ stands for the internalised version of $r$.
|
|
|
1046 |
This fact, together with the fact of how $\flex$ relates to injection:
|
|
|
1047 |
|
|
|
1048 |
\begin{equation}\label{flex}
|
|
|
1049 |
\flex \; r \; id \; (s@[c]) \; v = \flex \; r \; id \; s \; (inj \; (r\backslash s) \; c\; v).
|
|
|
1050 |
\end{equation}
|
|
|
1051 |
|
|
|
1052 |
\noindent
|
|
|
1053 |
can be used to prove what we want:
|
|
|
1054 |
\begin{center}
|
|
|
1055 |
$ \flex \; r\; id\; s\; v = \textit{decode} \;( \textit{bmkeps}\; (\rup \backslash s) ) r$
|
|
|
1056 |
\end{center}
|
|
|
1057 |
\noindent
|
|
|
1058 |
If we state the inductive hypothesis to be
|
|
|
1059 |
\begin{center}
|
|
|
1060 |
$ \flex \; r\; id\; s\; v = \textit{decode} \;( \textit{retrieve}\; (\rup \backslash s) \; v \;) r$
|
|
|
1061 |
\end{center}
|
|
|
1062 |
\noindent
|
|
|
1063 |
where $\mkeps(r\backslash s) $ is denoted using $v$,
|
|
144
|
1064 |
then a reverse induction
|
|
|
1065 |
helps with using
|
|
135
|
1066 |
the fact~\eqref{flex} in proving the $n+1$ step:
|
|
|
1067 |
\begin{center}
|
|
|
1068 |
$ \flex \; r\; id\; (s@[c])\; v = \textit{decode} \;( \textit{retrieve}\; (\rup \backslash s) \; (\inj \; (r\backslash s) \;c\;v)\;) r$
|
|
|
1069 |
\end{center}
|
|
144
|
1070 |
Using a lemma that
|
|
135
|
1071 |
\begin{center}
|
|
|
1072 |
$\textit{retrieve}\; (\rup \backslash s) \; (\inj \; (r\backslash s) \;c\;v)\; = \textit{retrieve}\; (\rup \backslash s@[c]) \; v\; $
|
|
|
1073 |
\end{center}
|
|
|
1074 |
we get
|
|
|
1075 |
\begin{center}
|
|
|
1076 |
$ \textit{decode} \;( \textit{retrieve}\; (\rup \backslash s) \; (\inj \; (r\backslash s) \;c\;v)\;) r = \textit{decode} \;( \textit{retrieve}\; (\rup \backslash s@[c]) \; v\;) r $
|
|
|
1077 |
\end{center}
|
|
|
1078 |
and the inductive step is done because
|
|
|
1079 |
\begin{center}
|
|
144
|
1080 |
$ \textit{retrieve}\; (\rup \backslash s@[c]) \; \mkeps(r\backslash s) = \bmkeps \;(\rup \backslash s@[c])$.
|
|
135
|
1081 |
\end{center}
|
|
|
1082 |
|
|
144
|
1083 |
\noindent
|
|
|
1084 |
To use
|
|
|
1085 |
$ \flex \; r\; id\; s\; v = \textit{decode} \;( \textit{retrieve}\; (\rup \backslash s) \; v \;) r$
|
|
|
1086 |
for our
|
|
|
1087 |
correctness proof, simply replace the $v$ with
|
|
|
1088 |
$\mkeps\;(r\backslash s)$, and apply the lemma that
|
|
|
1089 |
\begin{center}
|
|
|
1090 |
$ \; \bmkeps \; \rup = (\textit{retrieve} \; \rup \; \mkeps(r))$
|
|
|
1091 |
\end{center}
|
|
|
1092 |
\noindent
|
|
|
1093 |
We get the correctness of our bit-coded algorithm:
|
|
|
1094 |
\begin{center}
|
|
|
1095 |
$\flex \;r\; id \; s \; (\mkeps \; (r\backslash s)) = \textit{decode} \; (\bmkeps \; \rup\backslash s) \; r$.
|
|
|
1096 |
\end{center}
|
|
|
1097 |
\noindent
|
|
|
1098 |
|
|
|
1099 |
|
|
|
1100 |
|
|
135
|
1101 |
\subsubsection{Using Retrieve Function In a New Setting}
|
|
|
1102 |
Ausaf
|
|
|
1103 |
and Urban used $\retrieve$ to prove the correctness of bitcoded
|
|
|
1104 |
algorithm without simplification. Our purpose of using it, however,
|
|
107
|
1105 |
is to establish
|
|
|
1106 |
|
|
|
1107 |
\begin{center}
|
|
|
1108 |
$ \textit{retrieve} \;
|
|
|
1109 |
a \; v \;=\; \textit{retrieve} \; (\textit{simp}\,a) \; v'.$
|
|
|
1110 |
\end{center}
|
|
|
1111 |
The idea is that using $v'$, a simplified version of $v$ that had gone
|
|
|
1112 |
through the same simplification step as $\textit{simp}(a)$, we are able
|
|
145
|
1113 |
to extract the bitcode that gives the same lexing information as the
|
|
144
|
1114 |
unsimplified one.
|
|
|
1115 |
If we want to use a similar technique as
|
|
|
1116 |
that of the existing proof,
|
|
94
|
1117 |
we face the problem that in the above
|
|
|
1118 |
equalities,
|
|
|
1119 |
$\retrieve \; a \; v$ is not always defined.
|
|
145
|
1120 |
For example,
|
|
100
|
1121 |
$\retrieve \; _0(_1a+_0a) \; \Left(\Empty)$
|
|
101
|
1122 |
is defined, but not $\retrieve \; (_{01}a) \;\Left(\Empty)$,
|
|
94
|
1123 |
though we can extract the same POSIX
|
|
|
1124 |
bits from the two annotated regular expressions.
|
|
95
|
1125 |
The latter might occur when we try to retrieve from
|
|
|
1126 |
a simplified regular expression using the same value
|
|
145
|
1127 |
underlying the unsimplified one.
|
|
95
|
1128 |
This is because $\Left(\Empty)$ corresponds to
|
|
101
|
1129 |
the regular expression structure $\ONE+r_2$ instead of
|
|
|
1130 |
$\ONE$.
|
|
94
|
1131 |
That means, if we
|
|
|
1132 |
want to prove that
|
|
|
1133 |
\begin{center}
|
|
145
|
1134 |
$\bmkeps \; \rup\backslash s = \bmkeps \; \rup\backslash_{simp} s$
|
|
94
|
1135 |
\end{center}
|
|
|
1136 |
\noindent
|
|
|
1137 |
holds by using $\retrieve$,
|
|
|
1138 |
we probably need to prove an equality like below:
|
|
|
1139 |
\begin{center}
|
|
|
1140 |
%$\retrieve \; \rup\backslash_{simp} s \; \mkeps(r\backslash_{simp} s)=\textit{retrieve} \; \rup\backslash s \; \mkeps(r\backslash s)$
|
|
101
|
1141 |
$\retrieve \; \rup\backslash_{simp} s \; \mkeps(f(r\backslash s))=\textit{retrieve} \; \rup\backslash s \; \mkeps(r\backslash s)$
|
|
94
|
1142 |
\end{center}
|
|
|
1143 |
\noindent
|
|
101
|
1144 |
$f$ rectifies $r\backslash s$ so the value $\mkeps(f(r\backslash s))$ becomes
|
|
|
1145 |
something simpler
|
|
94
|
1146 |
to make the retrieve function defined.\\
|
|
145
|
1147 |
\subsubsection{Ways to Rectify Values}
|
|
95
|
1148 |
One way to do this is to prove the following:
|
|
|
1149 |
\begin{center}
|
|
|
1150 |
$\retrieve \; \rup\backslash_{simp} s \; \mkeps(\simp(r\backslash s))=\textit{retrieve} \; \rup\backslash s \; \mkeps(r\backslash s)$
|
|
|
1151 |
\end{center}
|
|
|
1152 |
\noindent
|
|
101
|
1153 |
The reason why we choose $\simp$ as $f$ is because
|
|
|
1154 |
$\rup\backslash_{simp} \, s$ and $\simp(\rup\backslash \, s)$
|
|
|
1155 |
have the same shape:
|
|
|
1156 |
\begin{center}
|
|
|
1157 |
$\erase (\rup\backslash_{simp} \, s) = \erase(\simp(\rup\backslash s))$
|
|
|
1158 |
\end{center}
|
|
|
1159 |
|
|
|
1160 |
\noindent
|
|
|
1161 |
$\erase$ in the above equality means to remove the bit-codes
|
|
|
1162 |
in an annotated regular expression and only keep the original
|
|
|
1163 |
regular expression(just like "erasing" the bits). Its definition is omitted.
|
|
|
1164 |
$\rup\backslash_{simp} \, s$ and $\simp(\rup\backslash s)$
|
|
|
1165 |
are very closely related, but not identical.
|
|
107
|
1166 |
\subsubsection{Example for $\rup\backslash_{simp} \, s \neq \simp(\rup\backslash s)$}
|
|
101
|
1167 |
For example, let $r$ be the regular expression
|
|
|
1168 |
$(a+b)(a+a*)$ and $s$ be the string $aa$, then
|
|
103
|
1169 |
both $\erase (\rup\backslash_{simp} \, s)$ and $\erase (\simp (\rup\backslash s))$
|
|
|
1170 |
are $\ONE + a^*$. However, without $\erase$
|
|
101
|
1171 |
\begin{center}
|
|
|
1172 |
$\rup\backslash_{simp} \, s$ is equal to $_0(_0\ONE +_{11}a^*)$
|
|
|
1173 |
\end{center}
|
|
|
1174 |
\noindent
|
|
|
1175 |
whereas
|
|
|
1176 |
\begin{center}
|
|
103
|
1177 |
$\simp(\rup\backslash s)$ is equal to $(_{00}\ONE +_{011}a^*)$
|
|
101
|
1178 |
\end{center}
|
|
103
|
1179 |
|
|
107
|
1180 |
What makes the difference?
|
|
|
1181 |
|
|
|
1182 |
%Two "rules" might be inferred from the above example.
|
|
103
|
1183 |
|
|
107
|
1184 |
%First, after erasing the bits the two regular expressions
|
|
|
1185 |
%are exactly the same: both become $1+a^*$. Here the
|
|
|
1186 |
%function $\simp$ exhibits the "one in the end equals many times
|
|
|
1187 |
%at the front"
|
|
|
1188 |
%property: one simplification in the end causes the
|
|
|
1189 |
%same regular expression structure as
|
|
|
1190 |
%successive simplifications done alongside derivatives.
|
|
|
1191 |
%$\rup\backslash_{simp} \, s$ unfolds to
|
|
|
1192 |
%$\simp((\simp(r\backslash a))\backslash a)$
|
|
|
1193 |
%and $\simp(\rup\backslash s)$ unfolds to
|
|
|
1194 |
%$\simp((r\backslash a)\backslash a)$. The one simplification
|
|
|
1195 |
%in the latter causes the resulting regular expression to
|
|
|
1196 |
%become $1+a^*$, exactly the same as the former with
|
|
|
1197 |
%two simplifications.
|
|
103
|
1198 |
|
|
107
|
1199 |
%Second, the bit-codes are different, but they are essentially
|
|
|
1200 |
%the same: if we push the outmost bits ${\bf_0}(_0\ONE +_{11}a^*)$ of $\rup\backslash_{simp} \, s$
|
|
|
1201 |
%inside then we get $(_{00}\ONE +_{011}a^*)$, exactly the
|
|
|
1202 |
%same as that of $\rup\backslash \, s$. And this difference
|
|
|
1203 |
%does not matter when we try to apply $\bmkeps$ or $\retrieve$
|
|
|
1204 |
%to it. This seems a good news if we want to use $\retrieve$
|
|
|
1205 |
%to prove things.
|
|
103
|
1206 |
|
|
107
|
1207 |
%If we look into the difference above, we could see that the
|
|
|
1208 |
%difference is not fundamental: the bits are just being moved
|
|
|
1209 |
%around in a way that does not hurt the correctness.
|
|
103
|
1210 |
During the first derivative operation,
|
|
|
1211 |
$\rup\backslash a=(_0\ONE + \ZERO)(_0a + _1a^*)$ is
|
|
107
|
1212 |
in the form of a sequence regular expression with
|
|
|
1213 |
two components, the first
|
|
|
1214 |
one $\ONE + \ZERO$ being nullable.
|
|
103
|
1215 |
Recall the simplification function definition:
|
|
|
1216 |
\begin{center}
|
|
|
1217 |
\begin{tabular}{@{}lcl@{}}
|
|
|
1218 |
|
|
|
1219 |
$\textit{simp} \; (\textit{SEQ}\;bs\,a_1\,a_2)$ & $\dn$ & $ (\textit{simp} \; a_1, \textit{simp} \; a_2) \; \textit{match} $ \\
|
|
|
1220 |
&&$\quad\textit{case} \; (\ZERO, \_) \Rightarrow \ZERO$ \\
|
|
|
1221 |
&&$\quad\textit{case} \; (\_, \ZERO) \Rightarrow \ZERO$ \\
|
|
|
1222 |
&&$\quad\textit{case} \; (\ONE, a_2') \Rightarrow \textit{fuse} \; bs \; a_2'$ \\
|
|
|
1223 |
&&$\quad\textit{case} \; (a_1', \ONE) \Rightarrow \textit{fuse} \; bs \; a_1'$ \\
|
|
|
1224 |
&&$\quad\textit{case} \; (a_1', a_2') \Rightarrow \textit{SEQ} \; bs \; a_1' \; a_2'$ \\
|
|
|
1225 |
|
|
131
|
1226 |
$\textit{simp} \; (\textit{ALTS}\;bs\,as)$ & $\dn$ & $\textit{distinct}( \textit{flatten} ( \textit{as.map(simp)})) \; \textit{match} $ \\
|
|
103
|
1227 |
&&$\quad\textit{case} \; [] \Rightarrow \ZERO$ \\
|
|
|
1228 |
&&$\quad\textit{case} \; a :: [] \Rightarrow \textit{fuse bs a}$ \\
|
|
|
1229 |
&&$\quad\textit{case} \; as' \Rightarrow \textit{ALTS}\;bs\;as'$\\
|
|
|
1230 |
|
|
|
1231 |
$\textit{simp} \; a$ & $\dn$ & $\textit{a} \qquad \textit{otherwise}$
|
|
|
1232 |
\end{tabular}
|
|
|
1233 |
\end{center}
|
|
|
1234 |
|
|
|
1235 |
\noindent
|
|
107
|
1236 |
|
|
132
|
1237 |
and the definition of $\flatten$:
|
|
107
|
1238 |
\begin{center}
|
|
|
1239 |
\begin{tabular}{c c c}
|
|
|
1240 |
$\flatten \; []$ & $\dn$ & $[]$\\
|
|
|
1241 |
$\flatten \; \ZERO::rs$ & $\dn$ & $rs$\\
|
|
132
|
1242 |
$\flatten \;(_{\textit{bs}_1}\sum \textit{rs}_1 ::rs)$ & $\dn$ & $(\map \, (\fuse \, \textit{bs}_1) \,\textit{rs}_1) ::: \flatten(rs)$\\
|
|
107
|
1243 |
$\flatten \; r :: rs$ & $\dn$ & $r::\flatten(rs)$
|
|
|
1244 |
\end{tabular}
|
|
|
1245 |
\end{center}
|
|
|
1246 |
|
|
|
1247 |
\noindent
|
|
|
1248 |
If we call $\simp$ on $\rup\backslash a$, just as $\backslash_{simp}$
|
|
132
|
1249 |
requires, then we would go through the third clause of
|
|
103
|
1250 |
the sequence case:$\quad\textit{case} \; (\ONE, a_2') \Rightarrow \textit{fuse} \; bs \; a_2'$.
|
|
107
|
1251 |
The $\ZERO$ of $(_0\ONE + \ZERO)$ is thrown away
|
|
|
1252 |
by $\flatten$ and
|
|
|
1253 |
$_0\ONE$ merged into $(_0a + _1a^*)$ by simply
|
|
103
|
1254 |
putting its bits($_0$) to the front of the second component:
|
|
|
1255 |
${\bf_0}(_0a + _1a^*)$.
|
|
|
1256 |
After a second derivative operation,
|
|
|
1257 |
namely, $(_0(_0a + _1a^*))\backslash a$, we get
|
|
|
1258 |
$
|
|
|
1259 |
_0(_0 \ONE + _1(_1\ONE \cdot a^*))
|
|
|
1260 |
$, and this simplifies to $_0(_0 \ONE + _{11} a^*)$
|
|
|
1261 |
by the third clause of the alternative case:
|
|
132
|
1262 |
\begin{center}
|
|
|
1263 |
$\quad\textit{case} \; as' \Rightarrow _{bs}\sum{as'}$.
|
|
|
1264 |
\end{center}
|
|
|
1265 |
|
|
|
1266 |
\noindent
|
|
107
|
1267 |
The outmost bit $_0$ stays with
|
|
145
|
1268 |
the outermost regular expression, rather than being fused to
|
|
107
|
1269 |
its child regular expressions, as what we will later see happens
|
|
|
1270 |
to $\simp(\rup\backslash \, s)$.
|
|
|
1271 |
If we choose to not simplify in the midst of derivative operations,
|
|
|
1272 |
but only do it at the end after the string has been exhausted,
|
|
|
1273 |
namely, $\simp(\rup\backslash \, s)=\simp((\rup\backslash a)\backslash a)$,
|
|
|
1274 |
then at the {\bf second} derivative of
|
|
|
1275 |
$(\rup\backslash a)\bf{\backslash a}$
|
|
|
1276 |
we will go throught the clause of $\backslash$:
|
|
|
1277 |
\begin{center}
|
|
|
1278 |
\begin{tabular}{lcl}
|
|
|
1279 |
$(\textit{SEQ}\;bs\,a_1\,a_2)\,\backslash c$ & $\dn$ &
|
|
|
1280 |
$(when \; \textit{bnullable}\,a_1)$\\
|
|
133
|
1281 |
& &$_{bs}\sum\,\;[_{[]}((a_1\,\backslash c) \cdot \,a_2),$\\
|
|
|
1282 |
& &$(\textit{fuse}\,(\textit{bmkeps}\,a_1)\,(a_2\,\backslash c))]$\\
|
|
107
|
1283 |
\end{tabular}
|
|
|
1284 |
\end{center}
|
|
145
|
1285 |
\noindent
|
|
107
|
1286 |
because
|
|
|
1287 |
$\rup\backslash a = (_0\ONE + \ZERO)(_0a + _1a^*)$
|
|
|
1288 |
is a sequence
|
|
|
1289 |
with the first component being nullable
|
|
|
1290 |
(unsimplified, unlike the first round of running$\backslash_{simp}$).
|
|
103
|
1291 |
Therefore $((_0\ONE + \ZERO)(_0a + _1a^*))\backslash a$ splits into
|
|
|
1292 |
$([(\ZERO + \ZERO)\cdot(_0a + _1a^*)] + _0( _0\ONE + _1[_1\ONE \cdot a^*]))$.
|
|
|
1293 |
After these two successive derivatives without simplification,
|
|
|
1294 |
we apply $\simp$ to this regular expression, which goes through
|
|
107
|
1295 |
the alternative clause, and each component of
|
|
|
1296 |
$([(\ZERO + \ZERO)\cdot(_0a + _1a^*)] + _0( _0\ONE + _1[_1\ONE \cdot a^*]))$
|
|
|
1297 |
will be simplified, giving us the list:$[\ZERO, _0(_0\ONE + _{11}a^*)]$
|
|
|
1298 |
This list is then "flattened"--$\ZERO$ will be
|
|
|
1299 |
thrown away by $\textit{flatten}$; $ _0(_0\ONE + _{11}a^*)$
|
|
|
1300 |
is opened up to make the list consisting of two separate elements
|
|
|
1301 |
$_{00}\ONE$ and $_{011}a^*$, note that $flatten$
|
|
|
1302 |
$\fuse$s the bit(s) $_0$ to the front of $_0\ONE $ and $_{11}a^*$.
|
|
122
|
1303 |
The order of simplification, which impacts the order that alternatives
|
|
|
1304 |
are opened up, causes
|
|
107
|
1305 |
the bits to be moved differently.
|
|
|
1306 |
|
|
|
1307 |
\subsubsection{A Failed Attempt To Remedy the Problem Above}
|
|
111
|
1308 |
A simple class of regular expression and string
|
|
|
1309 |
pairs $(r, s)$ can be deduced from the above example
|
|
|
1310 |
which trigger the difference between
|
|
107
|
1311 |
$\rup\backslash_{simp} \, s$
|
|
|
1312 |
and $\simp(\rup\backslash s)$:
|
|
111
|
1313 |
\begin{center}
|
|
|
1314 |
\begin{tabular}{lcl}
|
|
|
1315 |
$D =\{ (r_1 \cdot r_2,\; [c_1c_2]) \mid $ & $\simp(r_2) = r_2, \simp(r_1 \backslash c_1) = \ONE,$\\
|
|
132
|
1316 |
$r_1 \; not \; \nullable, c_2 \in L(r_2),$ & $\exists \textit{rs},\textit{bs}.\; r_2 \backslash c_2 = _{bs}{\sum rs}$\\
|
|
|
1317 |
$\exists \textit{rs}_1. \; \simp(r_2 \backslash c_2) = _{bs}{\sum \textit{rs}_1}$ & $and \;\simp(r_1 \backslash [c_1c_2]) = \ZERO\}$\\
|
|
111
|
1318 |
\end{tabular}
|
|
|
1319 |
\end{center}
|
|
|
1320 |
We take a pair $(r, \;s)$ from the set $D$.
|
|
|
1321 |
|
|
145
|
1322 |
Now we compute $ \rup \backslash_{simp} s$, we get:
|
|
110
|
1323 |
\begin{center}
|
|
|
1324 |
\begin{tabular}{lcl}
|
|
|
1325 |
$(r_1\cdot r_2)\backslash_{simp} \, [c_1c_2]$ & $= \simp\left[ \big(\simp\left[ \left( r_1\cdot r_2 \right) \backslash c_1\right] \big)\backslash c_2\right]$\\
|
|
|
1326 |
& $= \simp\left[ \big(\simp \left[ \left(r_1 \backslash c_1\right) \cdot r_2 \right] \big) \backslash c_2 \right]$\\
|
|
111
|
1327 |
& $= \simp \left[ (\fuse \; \bmkeps(r_1\backslash c_1) \; \simp(r_2) ) \backslash c_2 \right]$,\\
|
|
|
1328 |
& $= \simp \left[ (\fuse \; \bmkeps(r_1\backslash c_1) \; r_2 ) \backslash c_2 \right]$,
|
|
110
|
1329 |
\end{tabular}
|
|
|
1330 |
\end{center}
|
|
|
1331 |
\noindent
|
|
|
1332 |
from the definition of $D$ we know $r_1 \backslash c_1$ is nullable, therefore
|
|
|
1333 |
$\bmkeps(r_1\backslash c_1)$ returns a bitcode, we shall call it
|
|
111
|
1334 |
$\textit{bs}_2$.
|
|
|
1335 |
The above term can be rewritten as
|
|
|
1336 |
\begin{center}
|
|
|
1337 |
$ \simp \left[ \fuse \; \textit{bs}_2\; r_2 \backslash c_2 \right]$,
|
|
|
1338 |
\end{center}
|
|
|
1339 |
which is equal to
|
|
110
|
1340 |
\begin{center}
|
|
132
|
1341 |
$\simp \left[ \fuse \; \textit{bs}_2 \; _{bs}{\sum rs} \right]$\\
|
|
|
1342 |
$=\simp \left[ \; _{bs_2++bs}{\sum rs} \right]$\\
|
|
|
1343 |
$= \; _{bs_2++bs}{\sum \textit{rs}_1} $
|
|
111
|
1344 |
\end{center}
|
|
|
1345 |
\noindent
|
|
|
1346 |
by using the properties from the set $D$ again
|
|
|
1347 |
and again(The reason why we set so many conditions
|
|
|
1348 |
that the pair $(r,s)$ need to satisfy is because we can
|
|
|
1349 |
rewrite them easily to construct the difference.)
|
|
|
1350 |
|
|
|
1351 |
Now we compute ${\bf \simp(\rup \backslash s)}$:
|
|
|
1352 |
\begin{center}
|
|
|
1353 |
$\simp \big[(r_1\cdot r_2) \backslash [c_1c_2] \big]= \simp \left[ ((r_1 \cdot r_2 )\backslash c_1) \backslash c_2 \right]$
|
|
110
|
1354 |
\end{center}
|
|
111
|
1355 |
\noindent
|
|
|
1356 |
Again, using the properties above, we obtain
|
|
|
1357 |
the following chain of equalities:
|
|
110
|
1358 |
\begin{center}
|
|
111
|
1359 |
$\simp(\rup \backslash s)= \simp \left[ ((r_1 \cdot r_2 )\backslash c_1) \backslash c_2 \right]= \simp\left[ \left(r_1 \backslash c_1\right) \cdot r_2 \big) \backslash c_2 \right]$\\
|
|
132
|
1360 |
$= \simp \left[ \sum[\big( \left(r_1 \backslash c_1\right) \backslash c_2 \big) \cdot r_2 \; , \; \fuse \; (\bmkeps \;r_1\backslash c_1) \; r_2 \backslash c_2 ] \right]$,
|
|
111
|
1361 |
\end{center}
|
|
|
1362 |
\noindent
|
|
|
1363 |
as before, we call the bitcode returned by
|
|
|
1364 |
$\bmkeps(r_1\backslash c_1)$ as
|
|
|
1365 |
$\textit{bs}_2$.
|
|
|
1366 |
Also, $\simp(r_2 \backslash c_2)$ is
|
|
132
|
1367 |
$_{bs}\sum \textit{rs}_1$,
|
|
111
|
1368 |
and $( \left(r_1 \backslash c_1\right) \backslash c_2 \cdot r_2)$
|
|
|
1369 |
simplifies to $\ZERO$,
|
|
|
1370 |
so the above term can be expanded as
|
|
|
1371 |
\begin{center}
|
|
|
1372 |
\begin{tabular}{l}
|
|
132
|
1373 |
$\textit{distinct}(\flatten[\ZERO\;, \; _{\textit{bs}_2++\textit{bs}}\sum \textit{rs}_1] ) \; \textit{match} $ \\
|
|
111
|
1374 |
$\textit{case} \; [] \Rightarrow \ZERO$ \\
|
|
|
1375 |
$\textit{case} \; a :: [] \Rightarrow \textit{\fuse \; \textit{bs} a}$ \\
|
|
132
|
1376 |
$\textit{case} \; as' \Rightarrow _{[]}\sum as'$\\
|
|
110
|
1377 |
\end{tabular}
|
|
|
1378 |
\end{center}
|
|
|
1379 |
\noindent
|
|
111
|
1380 |
Applying the definition of $\flatten$, we get
|
|
|
1381 |
\begin{center}
|
|
132
|
1382 |
$_{[]}\sum (\textit{map} \; \fuse (\textit{bs}_2 ++ bs) rs_1)$
|
|
111
|
1383 |
\end{center}
|
|
|
1384 |
\noindent
|
|
|
1385 |
compared to the result
|
|
110
|
1386 |
\begin{center}
|
|
132
|
1387 |
$ \; _{bs_2++bs}{\sum \textit{rs}_1} $
|
|
110
|
1388 |
\end{center}
|
|
111
|
1389 |
\noindent
|
|
|
1390 |
Note how these two regular expressions only
|
|
|
1391 |
differ in terms of the position of the bits
|
|
|
1392 |
$\textit{bs}_2++\textit{bs}$. They are the same otherwise.
|
|
|
1393 |
What caused this difference to happen?
|
|
|
1394 |
The culprit is the $\flatten$ function, which spills
|
|
|
1395 |
out the bitcodes in the inner alternatives when
|
|
|
1396 |
there exists an outer alternative.
|
|
|
1397 |
Note how the absence of simplification
|
|
|
1398 |
caused $\simp(\rup \backslash s)$ to
|
|
|
1399 |
generate the nested alternatives structure:
|
|
|
1400 |
\begin{center}
|
|
132
|
1401 |
$ \sum[\ZERO \;, \; _{bs}\sum \textit{rs} ]$
|
|
111
|
1402 |
\end{center}
|
|
|
1403 |
and this will always trigger the $\flatten$ to
|
|
112
|
1404 |
spill out the inner alternative's bitcode $\textit{bs}$,
|
|
111
|
1405 |
whereas when
|
|
|
1406 |
simplification is done along the way,
|
|
|
1407 |
the structure of nested alternatives is never created(we can
|
|
|
1408 |
actually prove that simplification function never allows nested
|
|
|
1409 |
alternatives to happen, more on this later).
|
|
110
|
1410 |
|
|
113
|
1411 |
How about we do not allow the function $\simp$
|
|
|
1412 |
to fuse out the bits when it is unnecessary?
|
|
|
1413 |
Like, for the above regular expression, we might
|
|
|
1414 |
just delete the outer layer of alternative
|
|
|
1415 |
\begin{center}
|
|
132
|
1416 |
\st{$ {\sum[\ZERO \;,}$} $_{bs}\sum \textit{rs}$ \st{$]$}
|
|
113
|
1417 |
\end{center}
|
|
132
|
1418 |
and get $_{bs}\sum \textit{rs}$ instead, without
|
|
113
|
1419 |
fusing the bits $\textit{bs}$ inside to every element
|
|
|
1420 |
of $\textit{rs}$.
|
|
|
1421 |
This idea can be realized by making the following
|
|
|
1422 |
changes to the $\simp$-function:
|
|
|
1423 |
\begin{center}
|
|
|
1424 |
\begin{tabular}{@{}lcl@{}}
|
|
|
1425 |
|
|
114
|
1426 |
$\textit{simp}' \; (_{\textit{bs}}(a_1 \cdot a_2))$ & $\dn$ & $\textit{as} \; \simp \; \textit{was} \; \textit{before} $ \\
|
|
113
|
1427 |
|
|
132
|
1428 |
$\textit{simp}' \; (_{bs}\sum as)$ & $\dn$ & \st{$\textit{distinct}( \textit{flatten} ( \textit{map simp as})) \; \textit{match} $} \\
|
|
114
|
1429 |
&&\st{$\quad\textit{case} \; [] \Rightarrow \ZERO$} \\
|
|
|
1430 |
&&\st{$\quad\textit{case} \; a :: [] \Rightarrow \textit{fuse bs a}$} \\
|
|
|
1431 |
&&\st{$\quad\textit{case} \; as' \Rightarrow \textit{ALTS}\;bs\;as'$}\\
|
|
|
1432 |
&&$\textit{if}(\textit{hollowAlternatives}( \textit{map \; simp \; as}))$\\
|
|
|
1433 |
&&$\textit{then} \; \fuse \; \textit{bs}\; \textit{extractAlt}(\textit{map} \; \simp \; \textit{as} )$\\
|
|
132
|
1434 |
&&$\textit{else} \; \simp(_{bs} \sum \textit{as})$\\
|
|
114
|
1435 |
|
|
113
|
1436 |
|
|
114
|
1437 |
$\textit{simp}' \; a$ & $\dn$ & $\textit{a} \qquad \textit{otherwise}$
|
|
113
|
1438 |
\end{tabular}
|
|
|
1439 |
\end{center}
|
|
|
1440 |
|
|
|
1441 |
\noindent
|
|
114
|
1442 |
given the definition of $\textit{hollowAlternatives}$ and $\textit{extractAlt}$ :
|
|
|
1443 |
\begin{center}
|
|
|
1444 |
$\textit{hollowAlternatives}( \textit{rs}) \dn
|
|
132
|
1445 |
\exists r = (_{\textit{bs}_1}\sum \textit{rs}_1) \in \textit{rs}. \forall r' \in \textit{rs}, \;
|
|
114
|
1446 |
\textit{either} \; r' = \ZERO \; \textit{or} \; r' = r $
|
|
|
1447 |
$\textit{extractAlt}( \textit{rs}) \dn \textit{if}\big(
|
|
132
|
1448 |
\exists r = (_{\textit{bs}_1}\sum \textit{rs}_1) \in \textit{rs}. \forall r' \in \textit{rs}, \;
|
|
114
|
1449 |
\textit{either} \; r' = \ZERO \; \textit{or} \; r' = r \big)\; \textit{then} \; \textit{return} \; r$
|
|
|
1450 |
\end{center}
|
|
|
1451 |
\noindent
|
|
|
1452 |
Basically, $\textit{hollowAlternatives}$ captures the feature of
|
|
|
1453 |
a list of regular expression of the shape
|
|
|
1454 |
\begin{center}
|
|
132
|
1455 |
$ \sum[\ZERO \;, \; _{bs}\sum \textit{rs} ]$
|
|
114
|
1456 |
\end{center}
|
|
|
1457 |
and this means we can simply elevate the
|
|
132
|
1458 |
inner regular expression $_{bs}\sum \textit{rs}$
|
|
114
|
1459 |
to the outmost
|
|
|
1460 |
and throw away the useless $\ZERO$s and
|
|
132
|
1461 |
the outer $\sum$ wrapper.
|
|
114
|
1462 |
Using this new definition of simp,
|
|
|
1463 |
under the example where $r$ is the regular expression
|
|
|
1464 |
$(a+b)(a+a*)$ and $s$ is the string $aa$
|
|
|
1465 |
the problem of $\rup\backslash_{simp} \, s \neq \simp(\rup\backslash s)$
|
|
|
1466 |
is resolved.
|
|
113
|
1467 |
|
|
114
|
1468 |
Unfortunately this causes new problems:
|
|
|
1469 |
for the counterexample where
|
|
|
1470 |
\begin{center}
|
|
|
1471 |
$r$ is the regular expression
|
|
|
1472 |
$(ab+(a^*+aa))$ and $s$ is the string $aa$
|
|
|
1473 |
\end{center}
|
|
122
|
1474 |
|
|
|
1475 |
\noindent
|
|
|
1476 |
$\rup\backslash_{simp} \, s$ is equal to
|
|
125
|
1477 |
$ _1(_{011}a^* + _1\ONE) $ whereas
|
|
|
1478 |
$ \simp(\rup\backslash s) = (_{1011}a^* + _{11}\ONE)$.
|
|
|
1479 |
This discrepancy does not appear for the old
|
|
114
|
1480 |
version of $\simp$.
|
|
125
|
1481 |
|
|
|
1482 |
Why?
|
|
|
1483 |
|
|
135
|
1484 |
We shall illustrate in detail again of what happened in each recursive call of
|
|
|
1485 |
$\backslash$ and $\backslash_{simp}$.
|
|
125
|
1486 |
During the first derivative operation,
|
|
|
1487 |
\begin{center}
|
|
135
|
1488 |
$\rup\backslash a=( _0[ \ONE\cdot {\bf b}] + _1( _0[ _1\ONE \cdot {\bf a}^*] + _1[ \ONE \cdot {\bf a}]) )$,
|
|
125
|
1489 |
\end{center}
|
|
|
1490 |
\noindent
|
|
|
1491 |
the second derivative gives us
|
|
|
1492 |
\begin{center}
|
|
135
|
1493 |
$(\rup\backslash a)\backslash a=(_0( [\ZERO\cdot {\bf b}] + 0) + _1( _0( [\ZERO\cdot {\bf a}^*] + _1[ _1\ONE \cdot {\bf a}^*]) + _1( [\ZERO \cdot {\bf a}] + \ONE) ))$,
|
|
125
|
1494 |
\end{center}
|
|
|
1495 |
|
|
|
1496 |
\noindent
|
|
|
1497 |
and this simplifies to
|
|
|
1498 |
\begin{center}
|
|
|
1499 |
$ _1(_{011}{\bf a}^* + _1\ONE) $
|
|
|
1500 |
\end{center}
|
|
135
|
1501 |
because when $(\rup\backslash a)\backslash a$ goes
|
|
|
1502 |
through simplification, according to our new $\simp$
|
|
|
1503 |
clause,
|
|
|
1504 |
each component of the list
|
|
|
1505 |
$[_0( [\ZERO\cdot {\bf b}] + 0) , _1( _0( [\ZERO\cdot {\bf a}^*] + _1[ _1\ONE \cdot {\bf a}^*]) + _1( [\ZERO \cdot {\bf a}] + \ONE) )]$
|
|
|
1506 |
is simplified into
|
|
|
1507 |
$[\ZERO, _1(_{011}{\bf a}^* + _1\ONE) ]$,
|
|
|
1508 |
this fits into the definition of $\textit{hollowAlternatives}$,
|
|
|
1509 |
so the structure of the annotated regular expression
|
|
|
1510 |
\begin{center}
|
|
|
1511 |
$_1(_{011}{\bf a}^* + _1\ONE) $
|
|
|
1512 |
\end{center}
|
|
|
1513 |
is preserved, in the sense that the outside bit $_1$
|
|
|
1514 |
is not fused inside.
|
|
125
|
1515 |
If, after the first derivative we apply simplification we get
|
|
|
1516 |
$(_0{\bf b} + _{101}{\bf a}^* + _{11}{\bf a} )$,
|
|
|
1517 |
and we do another derivative, getting
|
|
|
1518 |
$(\ZERO + (_{101}(\ONE \cdot _1{\bf a}^*)+_{11}\ONE)$,
|
|
|
1519 |
which simplifies to
|
|
|
1520 |
\begin{center}
|
|
|
1521 |
$ (_{1011}a^* + _{11}\ONE) $
|
|
|
1522 |
\end{center}
|
|
|
1523 |
|
|
|
1524 |
|
|
|
1525 |
|
|
|
1526 |
|
|
|
1527 |
|
|
145
|
1528 |
We have changed the algorithm to avoid the old
|
|
122
|
1529 |
counterexample, but this gives rise to new counterexamples.
|
|
114
|
1530 |
This dilemma causes this amendment not a successful
|
|
|
1531 |
attempt to make $\rup\backslash_{simp} \, s = \simp(\rup\backslash s)$
|
|
|
1532 |
under every possible regular expression and string.
|
|
112
|
1533 |
\subsection{Properties of the Function $\simp$}
|
|
|
1534 |
|
|
|
1535 |
We have proved in Isabelle quite a few properties
|
|
|
1536 |
of the $\simp$-function, which helps the proof to go forward
|
|
|
1537 |
and we list them here to aid comprehension.
|
|
|
1538 |
|
|
|
1539 |
To start, we need a bit of auxiliary notations,
|
|
|
1540 |
which is quite basic and is only written here
|
|
|
1541 |
for clarity.
|
|
113
|
1542 |
|
|
|
1543 |
$\textit{sub}(r)$ computes the set of the
|
|
|
1544 |
sub-regular expression of $r$:
|
|
|
1545 |
\begin{center}
|
|
|
1546 |
$\textit{sub}(\ONE) \dn \{\ONE\}$\\
|
|
|
1547 |
$\textit{sub}(r_1 \cdot r_2) \dn \textit{sub}(r_1) \cup \textit{sub}(r_2) \cup \{r_1 \cdot r_2\}$\\
|
|
112
|
1548 |
$\textit{sub}(r_1 + r_2) \dn \textit{sub}(r_1) \cup \textit{sub}(r_2) \cup \{r_1+r_2\}$\\
|
|
113
|
1549 |
\end{center}
|
|
112
|
1550 |
$\textit{good}(r) \dn r \neq \ZERO \land \\
|
|
132
|
1551 |
\forall r' \in \textit{sub}(r), \textit{if} \; r' = _{bs_1}\sum(rs_1), \;
|
|
112
|
1552 |
\textit{then} \nexists r'' \in \textit{rs}_1 \; s.t.\;
|
|
132
|
1553 |
r'' = _{bs_2}\sum \textit{rs}_2 $
|
|
112
|
1554 |
|
|
|
1555 |
The properties are mainly the ones below:
|
|
|
1556 |
\begin{itemize}
|
|
|
1557 |
\item
|
|
|
1558 |
\begin{center}
|
|
|
1559 |
$\simp(\simp(r)) = \simp(r)$
|
|
|
1560 |
\end{center}
|
|
|
1561 |
\item
|
|
|
1562 |
\begin{center}
|
|
145
|
1563 |
$\textit{if}\; r = \simp(r') \textit{then} \; \textit{good}(r) $
|
|
112
|
1564 |
\end{center}
|
|
|
1565 |
\end{itemize}
|
|
145
|
1566 |
\subsection{The Contains relation}
|
|
114
|
1567 |
$\retrieve$ is a too strong relation in that
|
|
|
1568 |
it only extracts one bitcode instead of a set of them.
|
|
|
1569 |
Therefore we try to define another relation(predicate)
|
|
|
1570 |
to capture the fact the regular expression has bits
|
|
|
1571 |
being moved around but still has all the bits needed.
|
|
|
1572 |
The contains symbol, written$\gg$, is a relation that
|
|
|
1573 |
takes two arguments in an infix form
|
|
|
1574 |
and returns a truth value.
|
|
112
|
1575 |
|
|
114
|
1576 |
|
|
|
1577 |
In other words, from the set of regular expression and
|
|
|
1578 |
bitcode pairs
|
|
|
1579 |
$\textit{RV} = \{(r, v) \mid r \text{r is a regular expression, v is a value}\}$,
|
|
|
1580 |
those that satisfy the following requirements are in the set
|
|
|
1581 |
$\textit{RV}_Contains$.
|
|
|
1582 |
Unlike the $\retrieve$
|
|
|
1583 |
function, which takes two arguments $r$ and $v$ and
|
|
|
1584 |
produces an only answer $\textit{bs}$, it takes only
|
|
|
1585 |
one argument $r$ and returns a set of bitcodes that
|
|
|
1586 |
can be generated by $r$.
|
|
|
1587 |
\begin{center}
|
|
|
1588 |
\begin{tabular}{llclll}
|
|
|
1589 |
& & & $_{bs}\ONE$ & $\gg$ & $\textit{bs}$\\
|
|
|
1590 |
& & & $_{bs}{\bf c}$ & $\gg$ & $\textit{bs}$\\
|
|
|
1591 |
$\textit{if} \; r_1 \gg \textit{bs}_1$ & $r_2 \; \gg \textit{bs}_2$
|
|
|
1592 |
& $\textit{then}$ &
|
|
|
1593 |
$_{bs}{r_1 \cdot r_2}$ &
|
|
|
1594 |
$\gg$ &
|
|
|
1595 |
$\textit{bs} @ \textit{bs}_1 @ \textit{bs}_2$\\
|
|
|
1596 |
|
|
|
1597 |
$\textit{if} \; r \gg \textit{bs}_1$ & & $\textit{then}$ &
|
|
132
|
1598 |
$_{bs}{\sum(r :: \textit{rs}})$ &
|
|
114
|
1599 |
$\gg$ &
|
|
|
1600 |
$\textit{bs} @ \textit{bs}_1 $\\
|
|
|
1601 |
|
|
132
|
1602 |
$\textit{if} \; _{bs}(\sum \textit{rs}) \gg \textit{bs} @ \textit{bs}_1$ & & $\textit{then}$ &
|
|
|
1603 |
$_{bs}{\sum(r :: \textit{rs}})$ &
|
|
114
|
1604 |
$\gg$ &
|
|
|
1605 |
$\textit{bs} @ \textit{bs}_1 $\\
|
|
|
1606 |
|
|
|
1607 |
$\textit{if} \; r \gg \textit{bs}_1\; \textit{and}$ & $_{bs}r^* \gg \textit{bs} @ \textit{bs}_2$ & $\textit{then}$ &
|
|
|
1608 |
$_{bs}r^* $ &
|
|
|
1609 |
$\gg$ &
|
|
|
1610 |
$\textit{bs} @ [0] @ \textit{bs}_1@ \textit{bs}_2 $\\
|
|
|
1611 |
|
|
|
1612 |
& & & $_{bs}r^*$ & $\gg$ & $\textit{bs} @ [1]$\\
|
|
|
1613 |
\end{tabular}
|
|
|
1614 |
\end{center}
|
|
|
1615 |
It is a predicate in the sense that given
|
|
|
1616 |
a regular expression and a bitcode, it
|
|
|
1617 |
returns true or false, depending on whether
|
|
|
1618 |
or not the regular expression can actually produce that
|
|
|
1619 |
value. If the predicates returns a true, then
|
|
|
1620 |
we say that the regular expression $r$ contains
|
|
|
1621 |
the bitcode $\textit{bs}$, written
|
|
|
1622 |
$r \gg \textit{bs}$.
|
|
|
1623 |
The $\gg$ operator with the
|
|
|
1624 |
regular expression $r$ may also be seen as a
|
|
138
|
1625 |
regular language by itself on the alphabet
|
|
|
1626 |
$\Sigma = {0,1}$.
|
|
|
1627 |
The definition of contains relation
|
|
|
1628 |
is given in an inductive form, similar to that
|
|
|
1629 |
of regular expressions, it might not be surprising
|
|
|
1630 |
that the set it denotes contains basically
|
|
|
1631 |
everything a regular expression can
|
|
|
1632 |
produce during the derivative and lexing process.
|
|
|
1633 |
This can be seen in the subsequent lemmas we have
|
|
|
1634 |
proved about contains:
|
|
|
1635 |
\begin{itemize}
|
|
|
1636 |
\item
|
|
139
|
1637 |
\begin{center}
|
|
|
1638 |
\begin{equation}\label{contains1}
|
|
|
1639 |
\textit{if}\; \models v:r \; \textit{then} \; \rup \gg \textit{code}(v)
|
|
|
1640 |
\end{equation}
|
|
|
1641 |
\end{center}
|
|
|
1642 |
This lemma states that the set
|
|
|
1643 |
$\{\textit{bs}\; | \rup \gg \textit{bs} \}$
|
|
|
1644 |
"contains" all the underlying value $v$ of $r$ in which they are
|
|
|
1645 |
in a coded form.
|
|
|
1646 |
These values include the ones created in the
|
|
|
1647 |
lexing process, for example, when the regular
|
|
|
1648 |
expression $r$ is nullable, then we have:
|
|
|
1649 |
\item
|
|
|
1650 |
\begin{center}
|
|
|
1651 |
$r \gg \textit{bmkeps}(r)$
|
|
|
1652 |
\end{center}
|
|
|
1653 |
This can be seen as a corollary of the previous lemma,
|
|
|
1654 |
because $\models \textit{mkeps}((r\downarrow)):(r\downarrow)$
|
|
|
1655 |
and $\textit{code}(\mkeps((r\downarrow))) = \bmkeps(r)$.
|
|
|
1656 |
Another corollary we have of \eqref{contains1}
|
|
|
1657 |
\item
|
|
|
1658 |
\begin{center}
|
|
|
1659 |
$\textit{if}\; \models v:r \; \textit{then} \; \rup \gg \textit{retrieve} \; \rup \; v$
|
|
|
1660 |
\end{center}
|
|
|
1661 |
as $\textit{retrieve} \; \rup \; v = \textit{code}(v)$
|
|
|
1662 |
It says that if you can extract a bitsequence using
|
|
|
1663 |
retrieve guided by $v$, then such bitsequence is already there in the set
|
|
|
1664 |
$\{\textit{bs}\; | \rup \gg \textit{bs} \}$.
|
|
|
1665 |
This lemma has a slightly different form:
|
|
|
1666 |
\item
|
|
|
1667 |
\begin{center}
|
|
|
1668 |
$\textit{if}\; \models v:a\downarrow \; \textit{then} \; a \gg \textit{retrieve} \; a \; v$
|
|
|
1669 |
\end{center}
|
|
|
1670 |
This is almost identical to the previous lemma, except
|
|
|
1671 |
this time we might have arbitrary bits attached
|
|
|
1672 |
to anywhere of the annotated regular expression $a$.
|
|
|
1673 |
$a$ can be any "made up" annotated regular expressions
|
|
|
1674 |
that does not belong to the "natural" ones created by
|
|
|
1675 |
internalising an unannotated regular expression.
|
|
|
1676 |
For example, a regular expression $r = (a+b)$ after internalisation
|
|
|
1677 |
becomes $\rup = (_0a+_1b)$. For an underlying value $v = \Left(\Char(a))$
|
|
|
1678 |
we have $\retrieve \; (_0a+_1b) \;v = 0$ and $(_0a+_1b) \gg 0$. We could
|
|
|
1679 |
attach arbitrary bits to the regular expression $\rup$
|
|
|
1680 |
without breaking the structure,
|
|
|
1681 |
for example we could make up $a = _{0100111}(_{1011}a+1b)$,
|
|
|
1682 |
and we still have $\models v:a\downarrow$, and
|
|
|
1683 |
therefore $a \gg \retrieve \; a \; v$, this time the bitsequence
|
|
|
1684 |
being $01001111011$.
|
|
|
1685 |
This shows that the inductive clauses defining $\gg$
|
|
|
1686 |
simulates what $\retrieve$ does guided by different
|
|
|
1687 |
values.
|
|
|
1688 |
Set $\{\textit{bs}\; | \rup \gg \textit{bs} \}$ contains
|
|
|
1689 |
a wide range of values coded as bitsequences,
|
|
|
1690 |
the following property can be routinely established
|
|
|
1691 |
from the previous lemma
|
|
|
1692 |
\item
|
|
|
1693 |
\begin{center}
|
|
|
1694 |
$r \gg \retrieve \; r \; (\inj \; (r\downarrow) \; c \; v) \;\;\; \textit{if} \; \models v: \textit{der} \; c \; (\erase(r))$
|
|
|
1695 |
\end{center}
|
|
|
1696 |
because $\inj \; (r\downarrow)\; c\; v$ is a value
|
|
|
1697 |
underlying $r$.
|
|
|
1698 |
Using this we can get something that looks much
|
|
|
1699 |
less obvious:
|
|
|
1700 |
\item
|
|
|
1701 |
|
|
|
1702 |
\begin{center}
|
|
|
1703 |
\begin{tabular}{c}
|
|
|
1704 |
$\textit{if} \models v: \erase(r)\backslash c \; \textit{then}$\\
|
|
|
1705 |
$r\backslash c \gg \retrieve \; r \; (\inj \; (r\downarrow) \; c \; v) \; \textit{and}$\\
|
|
|
1706 |
$r \gg \retrieve \; r \; (\inj \; (r\downarrow) \; c \; v)$\\
|
|
|
1707 |
\end{tabular}
|
|
|
1708 |
\end{center}
|
|
|
1709 |
It says that the derivative operation $\backslash c$ is basically
|
|
|
1710 |
an operation that does not change the bits an annotated regular
|
|
|
1711 |
expression is able to produce, both
|
|
|
1712 |
$r\backslash c$ and $r$ can produce
|
|
|
1713 |
the bitsequence $\inj \; (r\downarrow) \; c \;v)$.
|
|
|
1714 |
This invariance with respect to derivative can be
|
|
|
1715 |
further extended to a more surprising property:
|
|
|
1716 |
\item
|
|
|
1717 |
\begin{center}
|
|
|
1718 |
\begin{tabular}{c}
|
|
|
1719 |
$\textit{if} \models v: \erase(r) \backslash s$\\
|
|
|
1720 |
$r\backslash s \gg \retrieve \; r \; (\flex \; (r\downarrow) \; \textit{id} \; s \; v) \; \textit{and}$\\
|
|
|
1721 |
$r \gg \retrieve \; r \; (r\downarrow) \; \textit{id} \; s \; v) \; c \; v)$\\
|
|
|
1722 |
\end{tabular}
|
|
|
1723 |
\end{center}
|
|
|
1724 |
Here $\gg$ is almost like an $\textit{NFA}$ in the sense that
|
|
|
1725 |
it simulates the lexing process with respect to different strings.
|
|
140
|
1726 |
|
|
139
|
1727 |
Our hope is that using $\gg$ we can prove the bits
|
|
145
|
1728 |
information are not lost when we simplify a regular expression.
|
|
|
1729 |
So we need to relate $\gg$ with simplifcation, for example,
|
|
139
|
1730 |
one of the lemmas we have proved about $\gg$ is that
|
|
140
|
1731 |
\item
|
|
|
1732 |
\begin{center}
|
|
|
1733 |
$\simp \; a \gg \textit{bs} \iff a \gg \textit{bs}$
|
|
|
1734 |
\end{center}
|
|
|
1735 |
This could be a step towards our goal, as
|
|
|
1736 |
it assures that after simplification none of the
|
|
|
1737 |
bitsequence that can be created by
|
|
|
1738 |
the original annotated regular expression
|
|
|
1739 |
is lost.
|
|
|
1740 |
If we could prove the following that would be
|
|
|
1741 |
another step towards our proof,
|
|
|
1742 |
|
|
|
1743 |
\item
|
|
|
1744 |
\begin{center}
|
|
|
1745 |
$(\simp \;a) \backslash s \gg \textit{bs} \iff a\backslash s \gg \textit{bs}$
|
|
|
1746 |
\end{center}
|
|
|
1747 |
|
|
|
1748 |
as it says
|
|
|
1749 |
the simplified regular expression after derivatives will
|
|
|
1750 |
still have the full capacity of producing bitsequences
|
|
|
1751 |
as the unsimplified ones-- pretty much
|
|
|
1752 |
the intuition we try to establish.
|
|
|
1753 |
And if we could prove
|
|
|
1754 |
\item
|
|
|
1755 |
\begin{center}
|
|
|
1756 |
$a \backslash s \gg \textit{bs} \iff a\backslash_\textit{simp} s \gg \textit{bs}$
|
|
|
1757 |
\end{center}
|
|
|
1758 |
That would be just a stone's throw away
|
|
|
1759 |
from $\blexer \; r \; s = \blexers \; r \; s$.
|
|
|
1760 |
|
|
|
1761 |
\end{itemize}
|
|
|
1762 |
What we do after we work out
|
|
|
1763 |
the proof of the above lemma
|
|
|
1764 |
is still not clear. It is one of the next steps we need to
|
|
|
1765 |
work on.
|
|
|
1766 |
|
|
145
|
1767 |
\subsection{The $\textit{ders}_2$ Function}
|
|
114
|
1768 |
If we want to prove the result
|
|
|
1769 |
\begin{center}
|
|
|
1770 |
$ \textit{blexer}\_{simp}(r, \; s) = \textit{blexer}(r, \; s)$
|
|
|
1771 |
\end{center}
|
|
|
1772 |
inductively
|
|
|
1773 |
on the structure of the regular expression,
|
|
|
1774 |
then we need to induct on the case $r_1 \cdot r_2$,
|
|
|
1775 |
it can be good if we could express $(r_1 \cdot r_2) \backslash s$
|
|
140
|
1776 |
in terms of $r_1 \backslash s_1$ and $r_2 \backslash s_1$,
|
|
|
1777 |
where $s_1$ is a substring of $s$.
|
|
|
1778 |
For this we introduce the $\textit{ders2}$ function,
|
|
114
|
1779 |
which does a "convolution" on $r_1$ and $r_2$ using the string
|
|
141
|
1780 |
$s$. We omit the bits here as they are not affecting the
|
|
|
1781 |
structure of the regular expression, and we are mainly
|
|
|
1782 |
focusing on structure here.
|
|
114
|
1783 |
It is based on the observation that the derivative of $r_1 \cdot r_2$
|
|
|
1784 |
with respect to a string $s$ can actually be written in an "explicit form"
|
|
141
|
1785 |
composed of $r_1$ and $r_2$'s derivatives.
|
|
145
|
1786 |
For example, we can look at how $r_1\cdot r_2$ expands
|
|
141
|
1787 |
when being derived with a two-character string:
|
|
114
|
1788 |
\begin{center}
|
|
141
|
1789 |
\begin{tabular}{lcl}
|
|
|
1790 |
$ (r_1 \cdot r_2) \backslash [c_1c_2]$ & $=$ & $ (\textit{if} \; \nullable(r_1)\; \textit{then} \; ((r_1 \backslash c_1) \cdot r_2 + r_2 \backslash c_1) \; \textit{else} \; (r_1\backslash c_1) \cdot r_2) \backslash c_2$\\
|
|
|
1791 |
& $=$ & $\textit{if} \; \textit{nullable}(r_1) \;\textit{and} \; \nullable(r_1\backslash c_1) \; \textit{then} \;
|
|
|
1792 |
(((r_1\backslash c_1c_2)\cdot r_2 +( r_1 \backslash c_1 )\cdot r_2\backslash c_2 )+ r_2 \backslash c_1c_2)$\\
|
|
|
1793 |
&& $\textit{else if} \; \nullable(r_1) \textit{and} \;\textit{not} \; \nullable(r_1 \backslash c_1)\; \textit{then} \;
|
|
|
1794 |
((r_1\backslash c_1c_2)\cdot r_2 + r_2 \backslash c_1c_2)$\\
|
|
|
1795 |
&& $\textit{else} \;(r_1\backslash c_1c_2) \cdot r_2$
|
|
|
1796 |
\end{tabular}
|
|
114
|
1797 |
\end{center}
|
|
|
1798 |
which can also be written in a "convoluted sum"
|
|
141
|
1799 |
format if we omit the order in which the alternatives
|
|
|
1800 |
are being nested:
|
|
114
|
1801 |
\begin{center}
|
|
141
|
1802 |
\begin{tabular}{lcl}
|
|
|
1803 |
$(r_1 \cdot r_2) \backslash [c_1c_2] $ & $=$ & $\textit{if} \; \textit{nullable}(r_1) \;\textit{and} \; \nullable(r_1\backslash c_1) \; \textit{then} \;
|
|
|
1804 |
(r_1 \backslash c_1c_2) \cdot r_2 + (r_1 \backslash c_1)\cdot (r_2 \backslash c_2) + r_2 \backslash c_1c_2$\\
|
|
|
1805 |
&& $\textit{else if} \; \nullable(r_1) \textit{and} \;\textit{not} \; \nullable(r_1 \backslash c_1)\; \textit{then} \;
|
|
|
1806 |
((r_1\backslash c_1c_2)\cdot r_2 + r_2 \backslash c_1c_2)$\\
|
|
|
1807 |
&& $\textit{else} \;(r_1\backslash c_1c_2) \cdot r_2$\\
|
|
142
|
1808 |
& $=$ & $(r_1\backslash s) \cdot r_2 + \sum\limits_{s_j=c_2, c_1c_2 }{r_2 \backslash s_j} \; \text{where} \; \nullable(r_1\backslash s_i) \; \text{and} \;s_i @s_j = [c_1c_2]$
|
|
|
1809 |
\end{tabular}
|
|
|
1810 |
\end{center}
|
|
|
1811 |
In a more general form,
|
|
|
1812 |
\begin{center}
|
|
|
1813 |
\begin{tabular}{lcl}
|
|
|
1814 |
$(r_1 \cdot r_2) \backslash s $ & $=$ & $(r_1\backslash s) \cdot r_2 + \sum\limits_{s_i }{r_2 \backslash s_j} \; \text{where} \; s_i \; \text{is} \; \text{true prefix}\; \text{of} \; s \;\text{and} \; s_i @s_j = s \; \text{and} \;\nullable(r_1\backslash s_i)$
|
|
141
|
1815 |
\end{tabular}
|
|
114
|
1816 |
\end{center}
|
|
142
|
1817 |
We have formalized and proved the correctness of this
|
|
145
|
1818 |
alternative definition of derivative and call it $\textit{ders}_2$ to
|
|
142
|
1819 |
make a distinction of it with the $\textit{ders}$-function.
|
|
|
1820 |
Note this differentiates from the lexing algorithm in the sense that
|
|
|
1821 |
it calculates the results $r_1\backslash s_i , r_2 \backslash s_j$ first
|
|
|
1822 |
and then glue them together
|
|
145
|
1823 |
into nested alternatives.
|
|
|
1824 |
$\lexer$, on the other hand, can only produce each element of the list
|
|
142
|
1825 |
in the resulting alternatives regular expression
|
|
145
|
1826 |
altogether in the last derivative step.
|
|
|
1827 |
$\lexer$ does lexing in a "breadth first" manner,
|
|
|
1828 |
generating all the children nodes simultaneously
|
|
|
1829 |
whereas
|
|
|
1830 |
$\textit{ders}_2$ does it in a "depth first" manner.
|
|
142
|
1831 |
Using this intuition we can also define the annotated regular expression version of
|
|
145
|
1832 |
derivative and call it $\textit{bders}_2$ and prove the equivalence with $\textit{bders}$.
|
|
142
|
1833 |
Our hope is to use this alternative definition as a guide
|
|
|
1834 |
for our induction.
|
|
145
|
1835 |
Using $\textit{bders}_2$ we have a clearer idea
|
|
142
|
1836 |
of what $r\backslash s$ and $\simp(r\backslash s)$ looks like.
|
|
114
|
1837 |
\section{Conclusion}
|
|
|
1838 |
Under the exhaustive tests we believe the main
|
|
|
1839 |
result holds, yet a proof still seems elusive.
|
|
|
1840 |
We have tried out different approaches, and
|
|
|
1841 |
found a lot of properties of the function $\simp$.
|
|
|
1842 |
The counterexamples where $\rup\backslash_{simp} \, s \neq \simp(\rup\backslash s)$
|
|
|
1843 |
are also valuable in the sense that
|
|
|
1844 |
we get to know better why they are not equal and what
|
|
|
1845 |
are the subtle differences between a
|
|
|
1846 |
nested simplified regular expression and a
|
|
|
1847 |
regular expression that is simplified at the final moment.
|
|
|
1848 |
We are almost there, but a last step is needed to make the proof work.
|
|
|
1849 |
Hopefully in the next few weeks we will be able to find one.
|
|
145
|
1850 |
This would be an important milestone for my dissertation.
|
|
94
|
1851 |
|
|
148
|
1852 |
|
|
|
1853 |
\section{Future Plans}
|
|
|
1854 |
|
|
|
1855 |
Before the proof comes out, a plan is needed to make
|
|
|
1856 |
sure some progress is happening.
|
|
|
1857 |
We plan to get
|
|
|
1858 |
a practical implementation of our current
|
|
|
1859 |
method, which would involve extending the set of allowed syntax
|
|
|
1860 |
to include common regular expression constructs
|
|
|
1861 |
such as bounded repitions, negation(complement)
|
|
|
1862 |
and character range or even Boolean functions.
|
|
|
1863 |
Adding these concise way of expressing regular expressions
|
|
|
1864 |
while keeping the correctness of the simplification
|
|
|
1865 |
makes the work more practical.
|
|
|
1866 |
For example, using the added constructs we can
|
|
|
1867 |
demonstrate that our implementation can actually
|
|
|
1868 |
help the cloudflare web-application firewall
|
|
|
1869 |
to run smoothly even if it had been fed with
|
|
|
1870 |
evil regular expression
|
|
|
1871 |
$.*(?:.*=.*)))$
|
|
|
1872 |
and strings like $x=xxxxxxxxxx....$.
|
|
|
1873 |
This could help prove that our algorithm is not just
|
|
|
1874 |
some nice theory work but is actually competent in reality
|
|
|
1875 |
as this regular expression and string pair made the cloudflare
|
|
|
1876 |
servers to grind
|
|
|
1877 |
to a halt on July 2nd, 2019.
|
|
|
1878 |
After all, simply the "basic" regular expressions
|
|
|
1879 |
we gave in the introduction is really so basic, that
|
|
|
1880 |
even Brzozowski's 1964 paper has included more
|
|
|
1881 |
varieties than that(Boolean functions instead of
|
|
|
1882 |
just alternatives)\cite{Brzozowski1964}.
|
|
|
1883 |
A function only implementing the basic ones
|
|
|
1884 |
would lack practical interests.
|
|
|
1885 |
Making the algorithm practical also means to make it fast.
|
|
|
1886 |
Right now the Scala implementation
|
|
|
1887 |
is slower than the naive algorithm without bitcodes, even with those
|
|
|
1888 |
drastic simplification measures, which is not suggested by theory.
|
|
|
1889 |
We might need to implement it in other languages such as C
|
|
|
1890 |
to see if the problem is language specific.
|
|
|
1891 |
This is about 3 months' work.
|
|
|
1892 |
|
|
|
1893 |
We believe that there
|
|
|
1894 |
is still potential for more simplification as there are a lot
|
|
|
1895 |
of rules for regular expression similarity, however,
|
|
|
1896 |
this needs to be explored and checked.
|
|
|
1897 |
Looking for maximal simplification and
|
|
|
1898 |
best size bound and proving them would take around 3 months to complete.
|
|
|
1899 |
|
|
|
1900 |
Context-free languages are a bit harder to deal with by derivatives
|
|
|
1901 |
when compared with regular expressions.
|
|
|
1902 |
The main reason is that the child node of a context grammar
|
|
|
1903 |
can be the grammar itself--this left-recursion makes
|
|
|
1904 |
the computation procedure an impossibility when trying to solve directly.
|
|
|
1905 |
An example would be the following\cite{might2011cfgder}:
|
|
|
1906 |
\begin{center}
|
|
|
1907 |
$L = L \cdot x | \ONE$
|
|
|
1908 |
\end{center}
|
|
|
1909 |
then a derivative would give us the following:
|
|
|
1910 |
\begin{center}
|
|
|
1911 |
$L\backslash x = (L \backslash x)\cdot x | \ONE$
|
|
|
1912 |
\end{center}
|
|
|
1913 |
which is essentially what we have previously.
|
|
|
1914 |
This recursion can go on forever if we do not use some
|
|
|
1915 |
other methods such as introducing methods
|
|
|
1916 |
or manually decide that the two equations
|
|
|
1917 |
are actually equivalent and $L$ and $L\backslash x$
|
|
|
1918 |
denote the same language. And then give a mathematical proof
|
|
|
1919 |
that this is actually the case.
|
|
|
1920 |
This seems well beyond any mechanical algorithm one can
|
|
|
1921 |
expect to be able to do.....
|
|
|
1922 |
People have tried various ways to deal with the problems
|
|
|
1923 |
of looping when computing derivatives of context-free grammars
|
|
|
1924 |
such as memoization and laziness, with some degree of success\cite{might2011cfgder}.
|
|
|
1925 |
However this field seems largely unexplored and further
|
|
|
1926 |
optimizations seem possible. It would be great
|
|
|
1927 |
if we could find a simple augmentation to the current
|
|
|
1928 |
derivative method so that the subset of context free language
|
|
|
1929 |
of interest can be handled.
|
|
|
1930 |
This may take longer than the two previous tasks, but we still
|
|
|
1931 |
give it 3 months time and see how it goes.
|
|
|
1932 |
|
|
|
1933 |
|
|
|
1934 |
|
|
|
1935 |
|
|
|
1936 |
|
|
|
1937 |
|
|
94
|
1938 |
\bibliographystyle{plain}
|
|
|
1939 |
\bibliography{root}
|
|
|
1940 |
|
|
|
1941 |
|
|
|
1942 |
\end{document}
|
|
118
|
1943 |
|