|
532
|
1 |
% Chapter Template
|
|
|
2 |
|
|
|
3 |
\chapter{Regular Expressions and POSIX Lexing} % Main chapter title
|
|
|
4 |
|
|
|
5 |
\label{Inj} % In chapter 2 \ref{Chapter2} we will introduce the concepts
|
|
|
6 |
%and notations we
|
|
564
|
7 |
% used for describing the lexing algorithm by Sulzmann and Lu,
|
|
|
8 |
%and then give the algorithm and its variant and discuss
|
|
532
|
9 |
%why more aggressive simplifications are needed.
|
|
|
10 |
|
|
538
|
11 |
In this chapter, we define the basic notions
|
|
|
12 |
for regular languages and regular expressions.
|
|
564
|
13 |
This is essentially a description in ``English"
|
|
|
14 |
of our formalisation in Isabelle/HOL.
|
|
|
15 |
We also give the definition of what $\POSIX$ lexing means,
|
|
|
16 |
followed by an algorithm by Sulzmanna and Lu\parencite{Sulzmann2014}
|
|
|
17 |
that produces the output conforming
|
|
|
18 |
to the $\POSIX$ standard.
|
|
|
19 |
It is also worth mentioning that
|
|
|
20 |
we choose to use the ML-style notation
|
|
|
21 |
for function applications, where
|
|
|
22 |
the parameters of a function is not enclosed
|
|
|
23 |
inside a pair of parentheses (e.g. $f \;x \;y$
|
|
|
24 |
instead of $f(x,\;y)$). This is mainly
|
|
|
25 |
to make the text visually more concise.
|
|
532
|
26 |
|
|
538
|
27 |
\section{Basic Concepts}
|
|
564
|
28 |
Usually, formal language theory starts with an alphabet
|
|
538
|
29 |
denoting a set of characters.
|
|
541
|
30 |
Here we just use the datatype of characters from Isabelle,
|
|
|
31 |
which roughly corresponds to the ASCII characters.
|
|
564
|
32 |
In what follows, we shall leave the information about the alphabet
|
|
541
|
33 |
implicit.
|
|
|
34 |
Then using the usual bracket notation for lists,
|
|
|
35 |
we can define strings made up of characters:
|
|
532
|
36 |
\begin{center}
|
|
|
37 |
\begin{tabular}{lcl}
|
|
541
|
38 |
$\textit{s}$ & $\dn$ & $[] \; |\; c :: s$
|
|
532
|
39 |
\end{tabular}
|
|
|
40 |
\end{center}
|
|
541
|
41 |
Where $c$ is a variable ranging over characters.
|
|
|
42 |
Strings can be concatenated to form longer strings in the same
|
|
564
|
43 |
way as we concatenate two lists, which we shall write as $s_1 @ s_2$.
|
|
541
|
44 |
We omit the precise
|
|
538
|
45 |
recursive definition here.
|
|
|
46 |
We overload this concatenation operator for two sets of strings:
|
|
532
|
47 |
\begin{center}
|
|
|
48 |
\begin{tabular}{lcl}
|
|
541
|
49 |
$A @ B $ & $\dn$ & $\{s_A @ s_B \mid s_A \in A \land s_B \in B \}$\\
|
|
532
|
50 |
\end{tabular}
|
|
|
51 |
\end{center}
|
|
538
|
52 |
We also call the above \emph{language concatenation}.
|
|
532
|
53 |
The power of a language is defined recursively, using the
|
|
|
54 |
concatenation operator $@$:
|
|
|
55 |
\begin{center}
|
|
|
56 |
\begin{tabular}{lcl}
|
|
|
57 |
$A^0 $ & $\dn$ & $\{ [] \}$\\
|
|
541
|
58 |
$A^{n+1}$ & $\dn$ & $A @ A^n$
|
|
532
|
59 |
\end{tabular}
|
|
|
60 |
\end{center}
|
|
564
|
61 |
The union of all powers of a language
|
|
|
62 |
can be used to define the Kleene star operator:
|
|
532
|
63 |
\begin{center}
|
|
|
64 |
\begin{tabular}{lcl}
|
|
536
|
65 |
$A*$ & $\dn$ & $\bigcup_{i \geq 0} A^i$ \\
|
|
532
|
66 |
\end{tabular}
|
|
|
67 |
\end{center}
|
|
|
68 |
|
|
538
|
69 |
\noindent
|
|
564
|
70 |
However, to obtain a more convenient induction principle
|
|
538
|
71 |
in Isabelle/HOL,
|
|
536
|
72 |
we instead define the Kleene star
|
|
532
|
73 |
as an inductive set:
|
|
538
|
74 |
|
|
532
|
75 |
\begin{center}
|
|
538
|
76 |
\begin{mathpar}
|
|
564
|
77 |
\inferrule{\mbox{}}{[] \in A*\\}
|
|
538
|
78 |
|
|
564
|
79 |
\inferrule{s_1 \in A \;\; s_2 \in A*}{s_1 @ s_2 \in A*}
|
|
538
|
80 |
\end{mathpar}
|
|
532
|
81 |
\end{center}
|
|
564
|
82 |
\noindent
|
|
541
|
83 |
We also define an operation of "chopping off" a character from
|
|
|
84 |
a language, which we call $\Der$, meaning \emph{Derivative} (for a language):
|
|
532
|
85 |
\begin{center}
|
|
|
86 |
\begin{tabular}{lcl}
|
|
|
87 |
$\textit{Der} \;c \;A$ & $\dn$ & $\{ s \mid c :: s \in A \}$\\
|
|
|
88 |
\end{tabular}
|
|
|
89 |
\end{center}
|
|
538
|
90 |
\noindent
|
|
541
|
91 |
This can be generalised to "chopping off" a string from all strings within set $A$,
|
|
|
92 |
namely:
|
|
532
|
93 |
\begin{center}
|
|
|
94 |
\begin{tabular}{lcl}
|
|
541
|
95 |
$\textit{Ders} \;s \;A$ & $\dn$ & $\{ s' \mid s@s' \in A \}$\\
|
|
532
|
96 |
\end{tabular}
|
|
|
97 |
\end{center}
|
|
538
|
98 |
\noindent
|
|
541
|
99 |
which is essentially the left quotient $A \backslash L$ of $A$ against
|
|
|
100 |
the singleton language with $L = \{w\}$
|
|
532
|
101 |
in formal language theory.
|
|
564
|
102 |
However, for the purposes here, the $\textit{Ders}$ definition with
|
|
541
|
103 |
a single string is sufficient.
|
|
532
|
104 |
|
|
577
|
105 |
The reason for defining derivatives
|
|
|
106 |
is that it provides a different approach
|
|
|
107 |
to test membership of a string in
|
|
|
108 |
a set of strings.
|
|
|
109 |
For example, to test whether the string
|
|
|
110 |
$bar$ is contained in the set $\{foo, bar, brak\}$, one takes derivative of the set with
|
|
|
111 |
respect to the string $bar$:
|
|
|
112 |
\begin{center}
|
|
|
113 |
\begin{tabular}{lclll}
|
|
|
114 |
$S = \{foo, bar, brak\}$ & $ \stackrel{\backslash b}{\rightarrow }$ &
|
|
|
115 |
$\{ar, rak\}$ &
|
|
|
116 |
$\stackrel{\backslash a}{\rightarrow}$ &
|
|
|
117 |
\\
|
|
|
118 |
$\{r \}$ & $\stackrel{\backslash r}{\rightarrow}$ & $\{[]\}$ &
|
|
|
119 |
$\stackrel{[] \in S \backslash bar}{\longrightarrow}$ & $bar \in S$\\
|
|
|
120 |
\end{tabular}
|
|
|
121 |
\end{center}
|
|
|
122 |
\noindent
|
|
|
123 |
and in the end test whether the set
|
|
|
124 |
has the empty string \footnote{ we use the infix notation $A\backslash c$
|
|
|
125 |
instead of $\Der \; c \; A$ for brevity, as it is clear we are operating
|
|
|
126 |
on languages rather than regular expressions }.
|
|
|
127 |
In general, if we have a language $S_{start}$,
|
|
|
128 |
then we can test whether $s$ is in $S_{start}$
|
|
|
129 |
by testing whether $[] \in S \backslash s$.
|
|
|
130 |
|
|
564
|
131 |
With the sequencing, Kleene star, and $\textit{Der}$ operator on languages,
|
|
532
|
132 |
we have a few properties of how the language derivative can be defined using
|
|
|
133 |
sub-languages.
|
|
577
|
134 |
For example, for the sequence operator, we have
|
|
|
135 |
something similar to the ``chain rule'' of the calculus derivative:
|
|
532
|
136 |
\begin{lemma}
|
|
536
|
137 |
\[
|
|
|
138 |
\Der \; c \; (A @ B) =
|
|
|
139 |
\begin{cases}
|
|
538
|
140 |
((\Der \; c \; A) \, @ \, B ) \cup (\Der \; c\; B) , & \text{if} \; [] \in A \\
|
|
|
141 |
(\Der \; c \; A) \, @ \, B, & \text{otherwise}
|
|
536
|
142 |
\end{cases}
|
|
|
143 |
\]
|
|
532
|
144 |
\end{lemma}
|
|
|
145 |
\noindent
|
|
|
146 |
This lemma states that if $A$ contains the empty string, $\Der$ can "pierce" through it
|
|
|
147 |
and get to $B$.
|
|
536
|
148 |
The language $A*$'s derivative can be described using the language derivative
|
|
532
|
149 |
of $A$:
|
|
|
150 |
\begin{lemma}
|
|
538
|
151 |
$\textit{Der} \;c \;(A*) = (\textit{Der}\; c A) @ (A*)$\\
|
|
532
|
152 |
\end{lemma}
|
|
|
153 |
\begin{proof}
|
|
564
|
154 |
There are too inclusions to prove:
|
|
532
|
155 |
\begin{itemize}
|
|
564
|
156 |
\item{$\subseteq$}:\\
|
|
532
|
157 |
The set
|
|
536
|
158 |
\[ \{s \mid c :: s \in A*\} \]
|
|
532
|
159 |
is enclosed in the set
|
|
564
|
160 |
\[ \{s_1 @ s_2 \mid s_1 \, s_2.\; s_1 \in \{s \mid c :: s \in A\} \land s_2 \in A* \} \]
|
|
532
|
161 |
because whenever you have a string starting with a character
|
|
538
|
162 |
in the language of a Kleene star $A*$,
|
|
|
163 |
then that character together with some sub-string
|
|
|
164 |
immediately after it will form the first iteration,
|
|
|
165 |
and the rest of the string will
|
|
536
|
166 |
be still in $A*$.
|
|
564
|
167 |
\item{$\supseteq$}:\\
|
|
532
|
168 |
Note that
|
|
538
|
169 |
\[ \Der \; c \; (A*) = \Der \; c \; (\{ [] \} \cup (A @ A*) ) \]
|
|
564
|
170 |
hold.
|
|
|
171 |
Also this holds:
|
|
536
|
172 |
\[ \Der \; c \; (\{ [] \} \cup (A @ A*) ) = \Der\; c \; (A @ A*) \]
|
|
564
|
173 |
where the $\textit{RHS}$ can be rewritten
|
|
|
174 |
as \[ (\Der \; c\; A) @ A* \cup (\Der \; c \; (A*)) \]
|
|
|
175 |
which of course contains $\Der \; c \; A @ A*$.
|
|
532
|
176 |
\end{itemize}
|
|
|
177 |
\end{proof}
|
|
538
|
178 |
|
|
|
179 |
\noindent
|
|
532
|
180 |
Before we define the $\textit{Der}$ and $\textit{Ders}$ counterpart
|
|
|
181 |
for regular languages, we need to first give definitions for regular expressions.
|
|
|
182 |
|
|
536
|
183 |
\subsection{Regular Expressions and Their Meaning}
|
|
564
|
184 |
The \emph{basic regular expressions} are defined inductively
|
|
532
|
185 |
by the following grammar:
|
|
|
186 |
\[ r ::= \ZERO \mid \ONE
|
|
|
187 |
\mid c
|
|
|
188 |
\mid r_1 \cdot r_2
|
|
|
189 |
\mid r_1 + r_2
|
|
|
190 |
\mid r^*
|
|
|
191 |
\]
|
|
538
|
192 |
\noindent
|
|
564
|
193 |
We call them basic because we will introduce
|
|
|
194 |
additional constructors in later chapters such as negation
|
|
538
|
195 |
and bounded repetitions.
|
|
564
|
196 |
We use $\ZERO$ for the regular expression that
|
|
|
197 |
matches no string, and $\ONE$ for the regular
|
|
|
198 |
expression that matches only the empty string\footnote{
|
|
|
199 |
some authors
|
|
|
200 |
also use $\phi$ and $\epsilon$ for $\ZERO$ and $\ONE$
|
|
|
201 |
but we prefer our notation}.
|
|
|
202 |
The sequence regular expression is written $r_1\cdot r_2$
|
|
|
203 |
and sometimes we omit the dot if it is clear which
|
|
|
204 |
regular expression is meant; the alternative
|
|
|
205 |
is written $r_1 + r_2$.
|
|
|
206 |
The \emph{language} or meaning of
|
|
|
207 |
a regular expression is defined recursively as
|
|
|
208 |
a set of strings:
|
|
532
|
209 |
%TODO: FILL in the other defs
|
|
|
210 |
\begin{center}
|
|
|
211 |
\begin{tabular}{lcl}
|
|
564
|
212 |
$L \; \ZERO$ & $\dn$ & $\phi$\\
|
|
|
213 |
$L \; \ONE$ & $\dn$ & $\{[]\}$\\
|
|
|
214 |
$L \; c$ & $\dn$ & $\{[c]\}$\\
|
|
|
215 |
$L \; r_1 + r_2$ & $\dn$ & $ L \; r_1 \cup L \; r_2$\\
|
|
|
216 |
$L \; r_1 \cdot r_2$ & $\dn$ & $ L \; r_1 @ L \; r_2$\\
|
|
|
217 |
$L \; r^*$ & $\dn$ & $ (L\;r)*$
|
|
532
|
218 |
\end{tabular}
|
|
|
219 |
\end{center}
|
|
536
|
220 |
\noindent
|
|
532
|
221 |
Now with semantic derivatives of a language and regular expressions and
|
|
|
222 |
their language interpretations in place, we are ready to define derivatives on regexes.
|
|
|
223 |
\subsection{Brzozowski Derivatives and a Regular Expression Matcher}
|
|
564
|
224 |
%Recall, the language derivative acts on a set of strings
|
|
|
225 |
%and essentially chops off a particular character from
|
|
|
226 |
%all strings in that set, Brzozowski defined a derivative operation on regular expressions
|
|
|
227 |
%so that after derivative $L(r\backslash c)$
|
|
|
228 |
%will look as if it was obtained by doing a language derivative on $L(r)$:
|
|
577
|
229 |
Recall that the semantic derivative acts on a
|
|
|
230 |
language (set of strings).
|
|
|
231 |
One can decide whether a string $s$ belongs
|
|
|
232 |
to a language $S$ by taking derivative with respect to
|
|
|
233 |
that string and then checking whether the empty
|
|
|
234 |
string is in the derivative:
|
|
|
235 |
\begin{center}
|
|
|
236 |
\parskip \baselineskip
|
|
|
237 |
\def\myupbracefill#1{\rotatebox{90}{\stretchto{\{}{#1}}}
|
|
|
238 |
\def\rlwd{.5pt}
|
|
|
239 |
\newcommand\notate[3]{%
|
|
|
240 |
\unskip\def\useanchorwidth{T}%
|
|
|
241 |
\setbox0=\hbox{#1}%
|
|
|
242 |
\def\stackalignment{c}\stackunder[-6pt]{%
|
|
|
243 |
\def\stackalignment{c}\stackunder[-1.5pt]{%
|
|
|
244 |
\stackunder[-2pt]{\strut #1}{\myupbracefill{\wd0}}}{%
|
|
|
245 |
\rule{\rlwd}{#2\baselineskip}}}{%
|
|
|
246 |
\strut\kern7pt$\hookrightarrow$\rlap{ \footnotesize#3}}\ignorespaces%
|
|
|
247 |
}
|
|
|
248 |
\Longstack{
|
|
|
249 |
\notate{$\{ \ldots ,\;$
|
|
|
250 |
\notate{s}{1}{$(c_1 :: s_1)$}
|
|
|
251 |
$, \; \ldots \}$
|
|
|
252 |
}{1}{$S_{start}$}
|
|
|
253 |
}
|
|
|
254 |
\Longstack{
|
|
|
255 |
$\stackrel{\backslash c_1}{\longrightarrow}$
|
|
|
256 |
}
|
|
|
257 |
\Longstack{
|
|
|
258 |
$\{ \ldots,\;$ \notate{$s_1$}{1}{$(c_2::s_2)$}
|
|
|
259 |
$,\; \ldots \}$
|
|
|
260 |
}
|
|
|
261 |
\Longstack{
|
|
|
262 |
$\stackrel{\backslash c_2}{\longrightarrow}$
|
|
|
263 |
}
|
|
|
264 |
\Longstack{
|
|
|
265 |
$\{ \ldots,\; s_2
|
|
|
266 |
,\; \ldots \}$
|
|
|
267 |
}
|
|
|
268 |
\Longstack{
|
|
|
269 |
$ \xdashrightarrow{\backslash c_3\ldots\ldots} $
|
|
|
270 |
}
|
|
|
271 |
\Longstack{
|
|
|
272 |
\notate{$\{\ldots, [], \ldots\}$}{1}{$S_{end} =
|
|
|
273 |
S_{start}\backslash s$}
|
|
|
274 |
}
|
|
|
275 |
\end{center}
|
|
|
276 |
\begin{center}
|
|
|
277 |
$s \in S_{start} \iff [] \in S_{end}$
|
|
|
278 |
\end{center}
|
|
|
279 |
\noindent
|
|
|
280 |
Brzozowski noticed that this operation
|
|
579
|
281 |
can be ``mirrored'' on regular expressions which
|
|
564
|
282 |
he calls the derivative of a regular expression $r$
|
|
|
283 |
with respect to a character $c$, written
|
|
577
|
284 |
$r \backslash c$. This infix operator
|
|
|
285 |
takes an original regular expression $r$ as input
|
|
|
286 |
and a character as a right operand and
|
|
|
287 |
outputs a result, which is a new regular expression.
|
|
|
288 |
The derivative operation on regular expression
|
|
|
289 |
is defined such that the language of the derivative result
|
|
|
290 |
coincides with the language of the original
|
|
579
|
291 |
regular expression being taken
|
|
577
|
292 |
derivative with respect to the same character:
|
|
579
|
293 |
\begin{property}
|
|
|
294 |
|
|
|
295 |
\[
|
|
|
296 |
L \; (r \backslash c) = \Der \; c \; (L \; r)
|
|
|
297 |
\]
|
|
|
298 |
\end{property}
|
|
|
299 |
\noindent
|
|
|
300 |
Pictorially, this looks as follows:
|
|
|
301 |
|
|
577
|
302 |
\parskip \baselineskip
|
|
|
303 |
\def\myupbracefill#1{\rotatebox{90}{\stretchto{\{}{#1}}}
|
|
|
304 |
\def\rlwd{.5pt}
|
|
|
305 |
\newcommand\notate[3]{%
|
|
|
306 |
\unskip\def\useanchorwidth{T}%
|
|
|
307 |
\setbox0=\hbox{#1}%
|
|
|
308 |
\def\stackalignment{c}\stackunder[-6pt]{%
|
|
|
309 |
\def\stackalignment{c}\stackunder[-1.5pt]{%
|
|
|
310 |
\stackunder[-2pt]{\strut #1}{\myupbracefill{\wd0}}}{%
|
|
|
311 |
\rule{\rlwd}{#2\baselineskip}}}{%
|
|
|
312 |
\strut\kern8pt$\hookrightarrow$\rlap{ \footnotesize#3}}\ignorespaces%
|
|
|
313 |
}
|
|
|
314 |
\Longstack{
|
|
|
315 |
\notate{$r$}{1}{$L \; r = \{\ldots, \;c::s_1,
|
|
|
316 |
\;\ldots\}$}
|
|
|
317 |
}
|
|
|
318 |
\Longstack{
|
|
579
|
319 |
$\stackrel{\backslash c}{\xrightarrow{\hspace*{8cm}}}$
|
|
577
|
320 |
}
|
|
|
321 |
\Longstack{
|
|
579
|
322 |
\notate{$r\backslash c$}{1}{$L \; (r\backslash c)=
|
|
577
|
323 |
\{\ldots,\;s_1,\;\ldots\}$}
|
|
|
324 |
}
|
|
579
|
325 |
\\
|
|
|
326 |
The derivatives on regular expression can again be
|
|
|
327 |
generalised to a string.
|
|
|
328 |
One could compute $r\backslash s$ and test membership of $s$
|
|
|
329 |
in $L \; r$ by checking
|
|
|
330 |
whether the empty string is in the language of
|
|
|
331 |
$r\backslash s$.
|
|
|
332 |
|
|
532
|
333 |
|
|
579
|
334 |
\Longstack{
|
|
|
335 |
\notate{$r_{start}$}{4}{
|
|
|
336 |
\Longstack{$L \; r_{start} = \{\ldots, \;$
|
|
|
337 |
\notate{$s$}{1}{$c_1::s_1$}
|
|
|
338 |
$, \ldots\} $
|
|
|
339 |
}
|
|
|
340 |
}
|
|
|
341 |
}
|
|
|
342 |
\Longstack{
|
|
|
343 |
$\stackrel{\backslash c_1}{ \xrightarrow{\hspace*{1.8cm}} }$
|
|
|
344 |
}
|
|
|
345 |
\Longstack{
|
|
|
346 |
\notate{$r_1$}{3}{
|
|
|
347 |
$r_1 = r_{start}\backslash c_1$,
|
|
|
348 |
$L \; r_1 = $
|
|
|
349 |
\Longstack{
|
|
|
350 |
$\{ \ldots,\;$ \notate{$s_1$}{1}{$c_2::s_2$}
|
|
|
351 |
$,\; \ldots \}$
|
|
|
352 |
}
|
|
|
353 |
}
|
|
|
354 |
}
|
|
|
355 |
\Longstack{
|
|
|
356 |
$\stackrel{\backslash c_2}{\xrightarrow{\hspace*{1.8cm}}}$
|
|
|
357 |
}
|
|
|
358 |
\Longstack{
|
|
|
359 |
$r_2$
|
|
|
360 |
}
|
|
|
361 |
\Longstack{
|
|
|
362 |
$ \xdashrightarrow{\hspace*{0.3cm} \backslash c_3 \ldots \ldots \ldots \hspace*{0.3cm}} $
|
|
|
363 |
}
|
|
|
364 |
\Longstack{
|
|
|
365 |
\notate{$r_{end}$}{1}{
|
|
|
366 |
$L \; r_{end} = \{\ldots, \; [], \ldots\}$}
|
|
|
367 |
}
|
|
|
368 |
|
|
|
369 |
|
|
|
370 |
|
|
|
371 |
\begin{property}
|
|
|
372 |
$s \in L \; r_{start} \iff [] \in L \; r_{end}$
|
|
|
373 |
\end{property}
|
|
|
374 |
\noindent
|
|
|
375 |
Now we give the recursive definition of derivative on
|
|
|
376 |
regular expressions, so that it satisfies the properties above.
|
|
|
377 |
The derivative function, written $r\backslash c$,
|
|
|
378 |
defines how a regular expression evolves into
|
|
|
379 |
a new one after all the string it contains is acted on:
|
|
|
380 |
if it starts with $c$, then the character is chopped of,
|
|
|
381 |
if not, that string is removed.
|
|
|
382 |
\begin{center}
|
|
|
383 |
\begin{tabular}{lcl}
|
|
|
384 |
$\ZERO \backslash c$ & $\dn$ & $\ZERO$\\
|
|
|
385 |
$\ONE \backslash c$ & $\dn$ & $\ZERO$\\
|
|
|
386 |
$d \backslash c$ & $\dn$ &
|
|
|
387 |
$\mathit{if} \;c = d\;\mathit{then}\;\ONE\;\mathit{else}\;\ZERO$\\
|
|
|
388 |
$(r_1 + r_2)\backslash c$ & $\dn$ & $r_1 \backslash c \,+\, r_2 \backslash c$\\
|
|
|
389 |
$(r_1 \cdot r_2)\backslash c$ & $\dn$ & $\mathit{if} \, [] \in L(r_1)$\\
|
|
|
390 |
& & $\mathit{then}\;(r_1\backslash c) \cdot r_2 \,+\, r_2\backslash c$\\
|
|
|
391 |
& & $\mathit{else}\;(r_1\backslash c) \cdot r_2$\\
|
|
|
392 |
$(r^*)\backslash c$ & $\dn$ & $(r\backslash c) \cdot r^*$\\
|
|
|
393 |
\end{tabular}
|
|
564
|
394 |
\end{center}
|
|
|
395 |
\noindent
|
|
579
|
396 |
The most involved cases are the sequence case
|
|
|
397 |
and the star case.
|
|
|
398 |
The sequence case says that if the first regular expression
|
|
|
399 |
contains an empty string, then the second component of the sequence
|
|
|
400 |
needs to be considered, as its derivative will contribute to the
|
|
|
401 |
result of this derivative:
|
|
|
402 |
\begin{center}
|
|
|
403 |
\begin{tabular}{lcl}
|
|
|
404 |
$(r_1 \cdot r_2 ) \backslash c$ & $\dn$ & $\textit{if}\;\,([] \in L(r_1))\; r_1 \backslash c \cdot r_2 + r_2 \backslash c$ \\
|
|
|
405 |
& & $\textit{else} \; (r_1 \backslash c) \cdot r_2$
|
|
|
406 |
\end{tabular}
|
|
|
407 |
\end{center}
|
|
|
408 |
\noindent
|
|
|
409 |
Notice how this closely resembles
|
|
|
410 |
the language derivative operation $\Der$:
|
|
564
|
411 |
\begin{center}
|
|
|
412 |
\begin{tabular}{lcl}
|
|
|
413 |
$\Der \; c \; (A @ B)$ & $\dn$ &
|
|
|
414 |
$ \textit{if} \;\, [] \in A \;
|
|
|
415 |
\textit{then} \;\, ((\Der \; c \; A) @ B ) \cup
|
|
|
416 |
\Der \; c\; B$\\
|
|
|
417 |
& & $\textit{else}\; (\Der \; c \; A) @ B$\\
|
|
|
418 |
\end{tabular}
|
|
|
419 |
\end{center}
|
|
|
420 |
\noindent
|
|
579
|
421 |
The star regular expression $r^*$'s derivative
|
|
|
422 |
unwraps one iteration of $r$, turns it into $r\backslash c$,
|
|
|
423 |
and attaches the original $r^*$
|
|
|
424 |
after $r\backslash c$, so that
|
|
|
425 |
we can further unfold it as many times as needed:
|
|
|
426 |
\[
|
|
|
427 |
(r^*) \backslash c \dn (r \backslash c)\cdot r^*.
|
|
|
428 |
\]
|
|
|
429 |
Again,
|
|
|
430 |
the structure is the same as the semantic derivative of Kleene star:
|
|
532
|
431 |
\[
|
|
564
|
432 |
\textit{Der} \;c \;(A*) \dn (\textit{Der}\; c A) @ (A*)
|
|
532
|
433 |
\]
|
|
564
|
434 |
In the above definition of $(r_1\cdot r_2) \backslash c$,
|
|
|
435 |
the $\textit{if}$ clause's
|
|
|
436 |
boolean condition
|
|
|
437 |
$[] \in L(r_1)$ needs to be
|
|
|
438 |
somehow recursively computed.
|
|
|
439 |
We call such a function that checks
|
|
|
440 |
whether the empty string $[]$ is
|
|
|
441 |
in the language of a regular expression $\nullable$:
|
|
|
442 |
\begin{center}
|
|
|
443 |
\begin{tabular}{lcl}
|
|
|
444 |
$\nullable(\ZERO)$ & $\dn$ & $\mathit{false}$ \\
|
|
|
445 |
$\nullable(\ONE)$ & $\dn$ & $\mathit{true}$ \\
|
|
|
446 |
$\nullable(c)$ & $\dn$ & $\mathit{false}$ \\
|
|
|
447 |
$\nullable(r_1 + r_2)$ & $\dn$ & $\nullable(r_1) \vee \nullable(r_2)$ \\
|
|
|
448 |
$\nullable(r_1\cdot r_2)$ & $\dn$ & $\nullable(r_1) \wedge \nullable(r_2)$ \\
|
|
|
449 |
$\nullable(r^*)$ & $\dn$ & $\mathit{true}$ \\
|
|
|
450 |
\end{tabular}
|
|
|
451 |
\end{center}
|
|
|
452 |
\noindent
|
|
|
453 |
The $\ZERO$ regular expression
|
|
|
454 |
does not contain any string and
|
|
|
455 |
therefore is not \emph{nullable}.
|
|
|
456 |
$\ONE$ is \emph{nullable}
|
|
|
457 |
by definition.
|
|
|
458 |
The character regular expression $c$
|
|
|
459 |
corresponds to the singleton set $\{c\}$,
|
|
|
460 |
and therefore does not contain the empty string.
|
|
|
461 |
The alternative regular expression is nullable
|
|
|
462 |
if at least one of its children is nullable.
|
|
|
463 |
The sequence regular expression
|
|
|
464 |
would require both children to have the empty string
|
|
|
465 |
to compose an empty string, and the Kleene star
|
|
|
466 |
is always nullable because it naturally
|
|
579
|
467 |
contains the empty string.
|
|
532
|
468 |
\noindent
|
|
564
|
469 |
We have the following correspondence between
|
|
|
470 |
derivatives on regular expressions and
|
|
|
471 |
derivatives on a set of strings:
|
|
|
472 |
\begin{lemma}\label{derDer}
|
|
579
|
473 |
\begin{itemize}
|
|
|
474 |
\item
|
|
532
|
475 |
$\textit{Der} \; c \; L(r) = L (r\backslash c)$
|
|
579
|
476 |
\item
|
|
|
477 |
$c\!::\!s \in L(r)$ \textit{iff} $s \in L(r\backslash c)$.
|
|
|
478 |
\end{itemize}
|
|
532
|
479 |
\end{lemma}
|
|
579
|
480 |
\begin{proof}
|
|
|
481 |
By induction on $r$.
|
|
|
482 |
\end{proof}
|
|
532
|
483 |
\noindent
|
|
|
484 |
The main property of the derivative operation
|
|
564
|
485 |
(that enables us to reason about the correctness of
|
|
|
486 |
derivative-based matching)
|
|
|
487 |
is
|
|
532
|
488 |
|
|
|
489 |
|
|
|
490 |
\noindent
|
|
|
491 |
We can generalise the derivative operation shown above for single characters
|
|
|
492 |
to strings as follows:
|
|
|
493 |
|
|
|
494 |
\begin{center}
|
|
|
495 |
\begin{tabular}{lcl}
|
|
|
496 |
$r \backslash_s (c\!::\!s) $ & $\dn$ & $(r \backslash c) \backslash_s s$ \\
|
|
|
497 |
$r \backslash [\,] $ & $\dn$ & $r$
|
|
|
498 |
\end{tabular}
|
|
|
499 |
\end{center}
|
|
|
500 |
|
|
|
501 |
\noindent
|
|
564
|
502 |
When there is no ambiguity, we will
|
|
|
503 |
omit the subscript and use $\backslash$ instead
|
|
|
504 |
of $\backslash_r$ to denote
|
|
532
|
505 |
string derivatives for brevity.
|
|
539
|
506 |
Brzozowski's regular-expression matcher algorithm can then be described as:
|
|
532
|
507 |
|
|
|
508 |
\begin{definition}
|
|
564
|
509 |
$\textit{match}\;s\;r \;\dn\; \nullable \; (r\backslash s)$
|
|
532
|
510 |
\end{definition}
|
|
|
511 |
|
|
|
512 |
\noindent
|
|
|
513 |
Assuming the string is given as a sequence of characters, say $c_0c_1..c_n$,
|
|
|
514 |
this algorithm presented graphically is as follows:
|
|
|
515 |
|
|
|
516 |
\begin{equation}\label{graph:successive_ders}
|
|
|
517 |
\begin{tikzcd}
|
|
|
518 |
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}
|
|
|
519 |
\end{tikzcd}
|
|
|
520 |
\end{equation}
|
|
|
521 |
|
|
|
522 |
\noindent
|
|
539
|
523 |
It can be
|
|
|
524 |
relatively easily shown that this matcher is correct:
|
|
|
525 |
\begin{lemma}
|
|
564
|
526 |
$\textit{match} \; s\; r = \textit{true} \; \textit{iff} \; s \in L(r)$
|
|
539
|
527 |
\end{lemma}
|
|
|
528 |
\begin{proof}
|
|
579
|
529 |
By the stepwise property of derivatives
|
|
|
530 |
(lemma \ref{derDer}).
|
|
539
|
531 |
\end{proof}
|
|
|
532 |
\noindent
|
|
564
|
533 |
\begin{center}
|
|
|
534 |
\begin{figure}
|
|
539
|
535 |
\begin{tikzpicture}
|
|
|
536 |
\begin{axis}[
|
|
|
537 |
xlabel={$n$},
|
|
|
538 |
ylabel={time in secs},
|
|
|
539 |
ymode = log,
|
|
|
540 |
legend entries={Naive Matcher},
|
|
|
541 |
legend pos=north west,
|
|
|
542 |
legend cell align=left]
|
|
|
543 |
\addplot[red,mark=*, mark options={fill=white}] table {NaiveMatcher.data};
|
|
|
544 |
\end{axis}
|
|
|
545 |
\end{tikzpicture}
|
|
|
546 |
\caption{Matching $(a^*)^*b$ against $\protect\underbrace{aa\ldots a}_\text{n \textit{a}s}$}\label{NaiveMatcher}
|
|
|
547 |
\end{figure}
|
|
564
|
548 |
\end{center}
|
|
539
|
549 |
\noindent
|
|
564
|
550 |
If we implement the above algorithm naively, however,
|
|
|
551 |
the algorithm can be excruciatingly slow, as shown in
|
|
|
552 |
\ref{NaiveMatcher}.
|
|
|
553 |
Note that both axes are in logarithmic scale.
|
|
|
554 |
Around two dozens characters
|
|
|
555 |
would already explode the matcher on regular expression
|
|
|
556 |
$(a^*)^*b$.
|
|
|
557 |
For this, we need to introduce certain
|
|
539
|
558 |
rewrite rules for the intermediate results,
|
|
|
559 |
such as $r + r \rightarrow r$,
|
|
|
560 |
and make sure those rules do not change the
|
|
|
561 |
language of the regular expression.
|
|
564
|
562 |
One simpled-minded simplification function
|
|
|
563 |
that achieves these requirements is given below:
|
|
|
564 |
\begin{center}
|
|
|
565 |
\begin{tabular}{lcl}
|
|
|
566 |
$\simp \; r_1 \cdot r_2 $ & $ \dn$ &
|
|
|
567 |
$(\simp \; r_1, \simp \; r_2) \; \textit{match}$\\
|
|
|
568 |
& & $\quad \case \; (\ZERO, \_) \Rightarrow \ZERO$\\
|
|
|
569 |
& & $\quad \case \; (\_, \ZERO) \Rightarrow \ZERO$\\
|
|
|
570 |
& & $\quad \case \; (\ONE, r_2') \Rightarrow r_2'$\\
|
|
|
571 |
& & $\quad \case \; (r_1', \ONE) \Rightarrow r_1'$\\
|
|
|
572 |
& & $\quad \case \; (r_1', r_2') \Rightarrow r_1'\cdot r_2'$\\
|
|
|
573 |
$\simp \; r_1 + r_2$ & $\dn$ & $(\simp \; r_1, \simp \; r_2) \textit{match}$\\
|
|
|
574 |
& & $\quad \; \case \; (\ZERO, r_2') \Rightarrow r_2'$\\
|
|
|
575 |
& & $\quad \; \case \; (r_1', \ZERO) \Rightarrow r_1'$\\
|
|
|
576 |
& & $\quad \; \case \; (r_1', r_2') \Rightarrow r_1' + r_2'$\\
|
|
|
577 |
$\simp \; r$ & $\dn$ & $r$
|
|
|
578 |
|
|
|
579 |
\end{tabular}
|
|
|
580 |
\end{center}
|
|
|
581 |
If we repeatedly apply this simplification
|
|
|
582 |
function during the matching algorithm,
|
|
|
583 |
we have a matcher with simplification:
|
|
|
584 |
\begin{center}
|
|
|
585 |
\begin{tabular}{lcl}
|
|
|
586 |
$\derssimp \; [] \; r$ & $\dn$ & $r$\\
|
|
|
587 |
$\derssimp \; c :: cs \; r$ & $\dn$ & $\derssimp \; cs \; (\simp \; (r \backslash c))$\\
|
|
|
588 |
$\textit{matcher}_{simp}\; s \; r $ & $\dn$ & $\nullable \; (\derssimp \; s\;r)$
|
|
|
589 |
\end{tabular}
|
|
|
590 |
\end{center}
|
|
|
591 |
\begin{figure}
|
|
539
|
592 |
\begin{tikzpicture}
|
|
|
593 |
\begin{axis}[
|
|
|
594 |
xlabel={$n$},
|
|
|
595 |
ylabel={time in secs},
|
|
|
596 |
ymode = log,
|
|
|
597 |
xmode = log,
|
|
564
|
598 |
grid = both,
|
|
539
|
599 |
legend entries={Matcher With Simp},
|
|
|
600 |
legend pos=north west,
|
|
|
601 |
legend cell align=left]
|
|
|
602 |
\addplot[red,mark=*, mark options={fill=white}] table {BetterMatcher.data};
|
|
|
603 |
\end{axis}
|
|
564
|
604 |
\end{tikzpicture}
|
|
|
605 |
\caption{$(a^*)^*b$
|
|
|
606 |
against
|
|
|
607 |
$\protect\underbrace{aa\ldots a}_\text{n \textit{a}s}$ Using $\textit{matcher}_{simp}$}\label{BetterMatcher}
|
|
|
608 |
\end{figure}
|
|
|
609 |
\noindent
|
|
|
610 |
The running time of $\textit{ders}\_\textit{simp}$
|
|
|
611 |
on the same example of \ref{NaiveMatcher}
|
|
|
612 |
is now very tame in terms of the length of inputs,
|
|
|
613 |
as shown in \ref{BetterMatcher}.
|
|
539
|
614 |
|
|
538
|
615 |
Building derivatives and then testing the existence
|
|
539
|
616 |
of empty string in the resulting regular expression's language,
|
|
564
|
617 |
adding simplifications when necessary.
|
|
538
|
618 |
So far, so good. But what if we want to
|
|
|
619 |
do lexing instead of just getting a YES/NO answer?
|
|
564
|
620 |
Sulzmanna and Lu \cite{Sulzmann2014} first came up with a nice and
|
|
538
|
621 |
elegant (arguably as beautiful as the definition of the original derivative) solution for this.
|
|
|
622 |
|
|
539
|
623 |
\section{Values and the Lexing Algorithm by Sulzmann and Lu}
|
|
564
|
624 |
In this section, we present a two-phase regular expression lexing
|
|
|
625 |
algorithm.
|
|
|
626 |
The first phase takes successive derivatives with
|
|
|
627 |
respect to the input string,
|
|
|
628 |
and the second phase does the reverse, \emph{injecting} back
|
|
|
629 |
characters, in the meantime constructing a lexing result.
|
|
|
630 |
We will introduce the injection phase in detail slightly
|
|
|
631 |
later, but as a preliminary we have to first define
|
|
|
632 |
the datatype for lexing results,
|
|
|
633 |
called \emph{value} or
|
|
|
634 |
sometimes also \emph{lexical value}. Values and regular
|
|
538
|
635 |
expressions correspond to each other as illustrated in the following
|
|
|
636 |
table:
|
|
|
637 |
|
|
|
638 |
\begin{center}
|
|
|
639 |
\begin{tabular}{c@{\hspace{20mm}}c}
|
|
|
640 |
\begin{tabular}{@{}rrl@{}}
|
|
|
641 |
\multicolumn{3}{@{}l}{\textbf{Regular Expressions}}\medskip\\
|
|
|
642 |
$r$ & $::=$ & $\ZERO$\\
|
|
|
643 |
& $\mid$ & $\ONE$ \\
|
|
|
644 |
& $\mid$ & $c$ \\
|
|
|
645 |
& $\mid$ & $r_1 \cdot r_2$\\
|
|
|
646 |
& $\mid$ & $r_1 + r_2$ \\
|
|
|
647 |
\\
|
|
|
648 |
& $\mid$ & $r^*$ \\
|
|
|
649 |
\end{tabular}
|
|
|
650 |
&
|
|
|
651 |
\begin{tabular}{@{\hspace{0mm}}rrl@{}}
|
|
|
652 |
\multicolumn{3}{@{}l}{\textbf{Values}}\medskip\\
|
|
|
653 |
$v$ & $::=$ & \\
|
|
|
654 |
& & $\Empty$ \\
|
|
|
655 |
& $\mid$ & $\Char(c)$ \\
|
|
|
656 |
& $\mid$ & $\Seq\,v_1\, v_2$\\
|
|
|
657 |
& $\mid$ & $\Left(v)$ \\
|
|
|
658 |
& $\mid$ & $\Right(v)$ \\
|
|
|
659 |
& $\mid$ & $\Stars\,[v_1,\ldots\,v_n]$ \\
|
|
|
660 |
\end{tabular}
|
|
|
661 |
\end{tabular}
|
|
|
662 |
\end{center}
|
|
|
663 |
\noindent
|
|
564
|
664 |
A value has an underlying string, which
|
|
|
665 |
can be calculated by the ``flatten" function $|\_|$:
|
|
|
666 |
\begin{center}
|
|
|
667 |
\begin{tabular}{lcl}
|
|
|
668 |
$|\Empty|$ & $\dn$ & $[]$\\
|
|
|
669 |
$|\Char \; c|$ & $ \dn$ & $ [c]$\\
|
|
|
670 |
$|\Seq(v_1, v_2)|$ & $ \dn$ & $ v_1| @ |v_2|$\\
|
|
|
671 |
$|\Left(v)|$ & $ \dn$ & $ |v|$\\
|
|
|
672 |
$|\Right(v)|$ & $ \dn$ & $ |v|$\\
|
|
|
673 |
$|\Stars([])|$ & $\dn$ & $[]$\\
|
|
|
674 |
$|\Stars(v::vs)|$ & $\dn$ & $ |v| @ |\Stars(vs)|$
|
|
|
675 |
\end{tabular}
|
|
|
676 |
\end{center}
|
|
|
677 |
Sulzmann and Lu used a binary predicate, written $\vdash v:r $,
|
|
|
678 |
to indicate that a value $v$ could be generated from a lexing algorithm
|
|
|
679 |
with input $r$. They call it the value inhabitation relation.
|
|
538
|
680 |
\begin{mathpar}
|
|
564
|
681 |
\inferrule{\mbox{}}{\vdash \Char(c) : \mathbf{c}} \hspace{2em}
|
|
|
682 |
|
|
|
683 |
\inferrule{\mbox{}}{\vdash \Empty : \ONE} \hspace{2em}
|
|
|
684 |
|
|
|
685 |
\inferrule{\vdash v_1 : r_1 \;\; \vdash v_2 : r_2 }{\vdash \Seq(v_1, v_2) : (r_1 \cdot r_2)}
|
|
|
686 |
|
|
|
687 |
\inferrule{\vdash v_1 : r_1}{\vdash \Left(v_1):r_1+r_2}
|
|
|
688 |
|
|
|
689 |
\inferrule{\vdash v_2 : r_2}{\vdash \Right(v_2):r_1 + r_2}
|
|
538
|
690 |
|
|
564
|
691 |
\inferrule{\forall v \in vs. \vdash v:r \land |v| \neq []}{\vdash \Stars(vs):r^*}
|
|
|
692 |
\end{mathpar}
|
|
|
693 |
\noindent
|
|
|
694 |
The condition $|v| \neq []$ in the premise of star's rule
|
|
|
695 |
is to make sure that for a given pair of regular
|
|
|
696 |
expression $r$ and string $s$, the number of values
|
|
|
697 |
satisfying $|v| = s$ and $\vdash v:r$ is finite.
|
|
|
698 |
Given the same string and regular expression, there can be
|
|
|
699 |
multiple values for it. For example, both
|
|
|
700 |
$\vdash \Seq(\Left \; ab)(\Right \; c):(ab+a)(bc+c)$ and
|
|
|
701 |
$\vdash \Seq(\Right\; a)(\Left \; bc ):(ab+a)(bc+c)$ hold
|
|
|
702 |
and the values both flatten to $abc$.
|
|
|
703 |
Lexers therefore have to disambiguate and choose only
|
|
|
704 |
one of the values to output. $\POSIX$ is one of the
|
|
|
705 |
disambiguation strategies that is widely adopted.
|
|
|
706 |
|
|
|
707 |
Ausaf and Urban\parencite{AusafDyckhoffUrban2016}
|
|
|
708 |
formalised the property
|
|
|
709 |
as a ternary relation.
|
|
|
710 |
The $\POSIX$ value $v$ for a regular expression
|
|
538
|
711 |
$r$ and string $s$, denoted as $(s, r) \rightarrow v$, can be specified
|
|
564
|
712 |
in the following set of rules\footnote{The names of the rules are used
|
|
|
713 |
as they were originally given in \cite{AusafDyckhoffUrban2016}}:
|
|
|
714 |
\noindent
|
|
|
715 |
\begin{figure}
|
|
|
716 |
\begin{mathpar}
|
|
|
717 |
\inferrule[P1]{\mbox{}}{([], \ONE) \rightarrow \Empty}
|
|
|
718 |
|
|
|
719 |
\inferrule[PC]{\mbox{}}{([c], c) \rightarrow \Char \; c}
|
|
|
720 |
|
|
|
721 |
\inferrule[P+L]{(s,r_1)\rightarrow v_1}{(s, r_1+r_2)\rightarrow \Left \; v_1}
|
|
|
722 |
|
|
|
723 |
\inferrule[P+R]{(s,r_2)\rightarrow v_2\\ s \notin L \; r_1}{(s, r_1+r_2)\rightarrow \Right \; v_2}
|
|
|
724 |
|
|
|
725 |
\inferrule[PS]{(s_1, v_1) \rightarrow r_1 \\ (s_2, v_2)\rightarrow r_2\\
|
|
|
726 |
\nexists s_3 \; s_4. s_3 \neq [] \land s_3 @ s_4 = s_2 \land
|
|
|
727 |
s_1@ s_3 \in L \; r_1 \land s_4 \in L \; r_2}{(s_1 @ s_2, r_1\cdot r_2) \rightarrow
|
|
|
728 |
\Seq \; v_1 \; v_2}
|
|
|
729 |
|
|
|
730 |
\inferrule[P{[]}]{\mbox{}}{([], r^*) \rightarrow \Stars([])}
|
|
|
731 |
|
|
|
732 |
\inferrule[P*]{(s_1, v) \rightarrow v \\ (s_2, r^*) \rightarrow \Stars \; vs \\
|
|
|
733 |
|v| \neq []\\ \nexists s_3 \; s_4. s_3 \neq [] \land s_3@s_4 = s_2 \land
|
|
|
734 |
s_1@s_3 \in L \; r \land s_4 \in L \; r^*}{(s_1@s_2, r^*)\rightarrow \Stars \;
|
|
|
735 |
(v::vs)}
|
|
|
736 |
\end{mathpar}
|
|
|
737 |
\caption{POSIX Lexing Rules}
|
|
|
738 |
\end{figure}
|
|
538
|
739 |
\noindent
|
|
579
|
740 |
|
|
|
741 |
\begin{figure}
|
|
|
742 |
\begin{tikzpicture}[]
|
|
|
743 |
\node [minimum width = 6cm, rectangle split, rectangle split horizontal,
|
|
|
744 |
rectangle split parts=2, rectangle split part fill={red!30,blue!20}, style={draw, rounded corners, inner sep=10pt}]
|
|
|
745 |
(node1)
|
|
|
746 |
{$r_{token1}$
|
|
|
747 |
\nodepart{two} $\;\;\; \quad r_{token2}\;\;\;\quad$ };
|
|
|
748 |
%\node [left = 6.0cm of node1] (start1) {hi};
|
|
|
749 |
\node [left = 0.2cm of node1] (middle) {$v.s.$};
|
|
|
750 |
\node [minimum width = 6cm, left = 0.2cm of middle, rectangle split, rectangle split horizontal,
|
|
|
751 |
rectangle split parts=2, rectangle split part fill={red!30,blue!20}, style={draw, rounded corners, inner sep=10pt}]
|
|
|
752 |
(node2)
|
|
|
753 |
{$\quad\;\;\;r_{token1}\quad\;\;\;$
|
|
|
754 |
\nodepart{two} $r_{token2}$ };
|
|
|
755 |
\node [below = 0.1cm of node2] (text1) {\checkmark preferred by POSIX};
|
|
|
756 |
\node [above = 1.5cm of middle, minimum width = 6cm,
|
|
|
757 |
rectangle, style={draw, rounded corners, inner sep=10pt}]
|
|
|
758 |
(topNode) {$s$};
|
|
|
759 |
\path[->,draw]
|
|
|
760 |
(topNode) edge node {split $A$} (node2)
|
|
|
761 |
(topNode) edge node {split $B$} (node1)
|
|
|
762 |
;
|
|
|
763 |
|
|
|
764 |
|
|
|
765 |
\end{tikzpicture}
|
|
|
766 |
\caption{Maximum munch example: $s$ matches $r_{token1} \cdot r_{token2}$}\label{munch}
|
|
|
767 |
\end{figure}
|
|
564
|
768 |
The above $\POSIX$ rules follows the intuition described below:
|
|
538
|
769 |
\begin{itemize}
|
|
564
|
770 |
\item (Left Priority)\\
|
|
|
771 |
Match the leftmost regular expression when multiple options of matching
|
|
|
772 |
are available.
|
|
|
773 |
\item (Maximum munch)\\
|
|
|
774 |
Always match a subpart as much as possible before proceeding
|
|
|
775 |
to the next token.
|
|
579
|
776 |
For example, when the string $s$ matches
|
|
|
777 |
$r_{token1}\cdot r_{token2}$, and we have two ways $s$ can be split:
|
|
|
778 |
Then the split that matches a longer string for the first token
|
|
|
779 |
$r_{token1}$ is preferred by this maximum munch rule (See
|
|
|
780 |
\ref{munch} for an illustration).
|
|
|
781 |
\noindent
|
|
|
782 |
|
|
538
|
783 |
\end{itemize}
|
|
564
|
784 |
\noindent
|
|
|
785 |
These disambiguation strategies can be
|
|
|
786 |
quite practical.
|
|
538
|
787 |
For instance, when lexing a code snippet
|
|
564
|
788 |
\[
|
|
|
789 |
\textit{iffoo} = 3
|
|
|
790 |
\]
|
|
|
791 |
using the regular expression (with
|
|
|
792 |
keyword and identifier having their
|
|
|
793 |
usualy definitions on any formal
|
|
|
794 |
language textbook, for instance
|
|
|
795 |
keyword is a nonempty string starting with letters
|
|
|
796 |
followed by alphanumeric characters or underscores):
|
|
|
797 |
\[
|
|
|
798 |
\textit{keyword} + \textit{identifier},
|
|
|
799 |
\]
|
|
|
800 |
we want $\textit{iffoo}$ to be recognized
|
|
|
801 |
as an identifier rather than a keyword (if)
|
|
|
802 |
followed by
|
|
|
803 |
an identifier (foo).
|
|
|
804 |
POSIX lexing achieves this.
|
|
|
805 |
|
|
|
806 |
We know that a $\POSIX$ value is also a normal underlying
|
|
|
807 |
value:
|
|
541
|
808 |
\begin{lemma}
|
|
|
809 |
$(r, s) \rightarrow v \implies \vdash v: r$
|
|
|
810 |
\end{lemma}
|
|
|
811 |
\noindent
|
|
538
|
812 |
The good property about a $\POSIX$ value is that
|
|
|
813 |
given the same regular expression $r$ and string $s$,
|
|
|
814 |
one can always uniquely determine the $\POSIX$ value for it:
|
|
|
815 |
\begin{lemma}
|
|
|
816 |
$\textit{if} \,(s, r) \rightarrow v_1 \land (s, r) \rightarrow v_2\quad \textit{then} \; v_1 = v_2$
|
|
|
817 |
\end{lemma}
|
|
539
|
818 |
\begin{proof}
|
|
564
|
819 |
By induction on $s$, $r$ and $v_1$. The inductive cases
|
|
|
820 |
are all the POSIX rules.
|
|
|
821 |
Probably the most cumbersome cases are
|
|
|
822 |
the sequence and star with non-empty iterations.
|
|
567
|
823 |
We shall give the details for proving the sequence case here.
|
|
539
|
824 |
|
|
567
|
825 |
When we have
|
|
|
826 |
\[
|
|
|
827 |
(s_1, r_1) \rightarrow v_1 \;\, and \;\,
|
|
|
828 |
(s_2, r_2) \rightarrow v_2 \;\, and \;\,\\
|
|
|
829 |
\nexists s_3 \; s_4. s_3 \neq [] \land s_3 @ s_4 = s_2 \land
|
|
|
830 |
s_1@ s_3 \in L \; r_1 \land s_4 \in L \; r_2
|
|
|
831 |
\]
|
|
|
832 |
we know that the last condition
|
|
|
833 |
excludes the possibility of a
|
|
|
834 |
string $s_1'$ longer than $s_1$ such that
|
|
|
835 |
\[
|
|
|
836 |
(s_1', r_1) \rightarrow v_1' \;\;
|
|
|
837 |
and\;\; (s_2', r_2) \rightarrow v_2'\;\; and \;\;s_1' @s_2' = s
|
|
|
838 |
\]
|
|
|
839 |
hold.
|
|
|
840 |
A shorter string $s_1''$ with $s_2''$ satisfying
|
|
|
841 |
\[
|
|
|
842 |
(s_1'', r_1) \rightarrow v_1''
|
|
|
843 |
\;\;and\;\; (s_2'', r_2) \rightarrow v_2'' \;\;and \;\;s_1'' @s_2'' = s
|
|
|
844 |
\]
|
|
|
845 |
cannot possibly form a $\POSIX$ value either, because
|
|
|
846 |
by definition there is a candidate
|
|
|
847 |
with longer initial string
|
|
|
848 |
$s_1$. Therefore, we know that the POSIX
|
|
|
849 |
value $\Seq \; a \; b$ for $r_1 \cdot r_2$ matching
|
|
|
850 |
$s$ must have the
|
|
|
851 |
property that
|
|
|
852 |
\[
|
|
|
853 |
|a| = s_1 \;\; and \;\; |b| = s_2.
|
|
|
854 |
\]
|
|
|
855 |
The goal is to prove that $a = v_1 $ and $b = v_2$.
|
|
|
856 |
If we have some other POSIX values $v_{10}$ and $v_{20}$ such that
|
|
|
857 |
$(s_1, r_1) \rightarrow v_{10}$ and $(s_2, r_2) \rightarrow v_{20}$ hold,
|
|
|
858 |
then by induction hypothesis $v_{10} = v_1$ and $v_{20}= v_2$,
|
|
|
859 |
which means this "other" $\POSIX$ value $\Seq(v_{10}, v_{20})$
|
|
539
|
860 |
is the same as $\Seq(v_1, v_2)$.
|
|
|
861 |
\end{proof}
|
|
567
|
862 |
\noindent
|
|
|
863 |
Now we know what a $\POSIX$ value is and why it is unique;
|
|
|
864 |
the problem is generating
|
|
|
865 |
such a value in a lexing algorithm using derivatives.
|
|
538
|
866 |
|
|
|
867 |
\subsection{Sulzmann and Lu's Injection-based Lexing Algorithm}
|
|
|
868 |
|
|
567
|
869 |
Sulzmann and Lu extended Brzozowski's
|
|
|
870 |
derivative-based matching
|
|
|
871 |
to a lexing algorithm by a second pass
|
|
|
872 |
after the initial phase of successive derivatives.
|
|
|
873 |
This second phase generates a POSIX value
|
|
|
874 |
if the regular expression matches the string.
|
|
538
|
875 |
Two functions are involved: $\inj$ and $\mkeps$.
|
|
567
|
876 |
The first one used is $\mkeps$, which constructs a POSIX value from the last
|
|
|
877 |
derivative $r_n$:
|
|
538
|
878 |
\begin{ceqn}
|
|
|
879 |
\begin{equation}\label{graph:mkeps}
|
|
|
880 |
\begin{tikzcd}
|
|
567
|
881 |
r_0 \arrow[r, "\backslash c_0"] & r_1 \arrow[r, "\backslash c_1"] & r_2 \arrow[r, dashed, "\ldots"] & r_n \arrow[d, "mkeps" description] \\
|
|
538
|
882 |
& & & v_n
|
|
|
883 |
\end{tikzcd}
|
|
|
884 |
\end{equation}
|
|
|
885 |
\end{ceqn}
|
|
567
|
886 |
\noindent
|
|
|
887 |
In the above diagram, again we assume that
|
|
|
888 |
the input string $s$ is made of $n$ characters
|
|
|
889 |
$c_0c_1 \ldots c_{n-1}$, and the input regular expression $r$
|
|
|
890 |
is given label $0$ and after each character $c_i$ is taken off
|
|
|
891 |
by the derivative operation the resulting derivative regular
|
|
|
892 |
expressioin is $r_{i+1}$.The last derivative operation
|
|
|
893 |
$\backslash c_{n-1}$ gives back $r_n$, which is transformed into
|
|
|
894 |
a value $v_n$ by $\mkeps$.
|
|
|
895 |
$v_n$ tells us how an empty string is matched by the (nullable)
|
|
|
896 |
regular expression $r_n$, in a $\POSIX$ way.
|
|
|
897 |
The definition of $\mkeps$ is
|
|
538
|
898 |
\begin{center}
|
|
|
899 |
\begin{tabular}{lcl}
|
|
564
|
900 |
$\mkeps \; \ONE$ & $\dn$ & $\Empty$ \\
|
|
567
|
901 |
$\mkeps \; (r_{1}+r_{2})$ & $\dn$
|
|
|
902 |
& $\textit{if}\; (\nullable \; r_{1}) \;\,
|
|
|
903 |
\textit{then}\;\, \Left \; (\mkeps \; r_{1})$\\
|
|
|
904 |
& & $\phantom{if}\; \textit{else}\;\, \Right \;(\mkeps \; r_{2})$\\
|
|
|
905 |
$\mkeps \; (r_1 \cdot r_2)$ & $\dn$ & $\Seq\;(\mkeps\;r_1)\;(\mkeps \; r_2)$\\
|
|
564
|
906 |
$\mkeps \; r^* $ & $\dn$ & $\Stars\;[]$
|
|
538
|
907 |
\end{tabular}
|
|
|
908 |
\end{center}
|
|
|
909 |
|
|
|
910 |
|
|
|
911 |
\noindent
|
|
567
|
912 |
We favour the left child $r_1$ of $r_1 + r_2$
|
|
|
913 |
to match an empty string if there is a choice.
|
|
538
|
914 |
When there is a star for us to match the empty string,
|
|
|
915 |
we give the $\Stars$ constructor an empty list, meaning
|
|
567
|
916 |
no iteration is taken.
|
|
538
|
917 |
The result of a call to $\mkeps$ on a $\nullable$ $r$ would
|
|
|
918 |
be a $\POSIX$ value corresponding to $r$:
|
|
567
|
919 |
\begin{lemma}\label{mePosix}
|
|
|
920 |
$\nullable\; r \implies (r, []) \rightarrow (\mkeps\; v)$
|
|
|
921 |
\end{lemma}
|
|
|
922 |
\begin{proof}
|
|
|
923 |
By induction on the shape of $r$.
|
|
|
924 |
\end{proof}
|
|
|
925 |
\noindent
|
|
|
926 |
After the $\mkeps$-call, we inject back the characters one by one
|
|
|
927 |
in reverse order as they were chopped off in the derivative phase.
|
|
|
928 |
The fucntion for this is called $\inj$. $\inj$ and $\backslash$
|
|
|
929 |
are not exactly reverse operations of one another, as $\inj$
|
|
|
930 |
operates on values instead of regular
|
|
|
931 |
expressions.
|
|
|
932 |
In the diagram below, $v_i$ stands for the (POSIX) value
|
|
|
933 |
for how the regular expression
|
|
|
934 |
$r_i$ matches the string $s_i$ consisting of the last $n-i$ characters
|
|
|
935 |
of $s$ (i.e. $s_i = c_i \ldots c_{n-1}$ ) from the previous lexical value $v_{i+1}$.
|
|
538
|
936 |
After injecting back $n$ characters, we get the lexical value for how $r_0$
|
|
|
937 |
matches $s$.
|
|
|
938 |
\begin{ceqn}
|
|
|
939 |
\begin{equation}\label{graph:inj}
|
|
|
940 |
\begin{tikzcd}
|
|
567
|
941 |
r_0 \arrow[r, dashed] \arrow[d]& r_i \arrow[r, "\backslash c_i"] \arrow[d] & r_{i+1} \arrow[r, dashed] \arrow[d] & r_n \arrow[d, "mkeps" description] \\
|
|
|
942 |
v_0 \arrow[u] & v_i \arrow[l, dashed] & v_{i+1} \arrow[l,"inj_{r_i} c_i"] & v_n \arrow[l, dashed]
|
|
538
|
943 |
\end{tikzcd}
|
|
|
944 |
\end{equation}
|
|
|
945 |
\end{ceqn}
|
|
|
946 |
\noindent
|
|
567
|
947 |
$\textit{inj}$ takes three arguments: a regular
|
|
|
948 |
expression ${r_{i}}$, before the character is chopped off,
|
|
|
949 |
a character ${c_{i}}$, the character we want to inject back and
|
|
|
950 |
the third argument $v_{i+1}$ the value we want to inject into.
|
|
568
|
951 |
The result of an application
|
|
|
952 |
$\inj \; r_i \; c_i \; v_{i+1}$ is a new value $v_i$ such that
|
|
|
953 |
\[
|
|
|
954 |
(s_i, r_i) \rightarrow v_i
|
|
|
955 |
\]
|
|
|
956 |
holds.
|
|
567
|
957 |
The definition of $\textit{inj}$ is as follows:
|
|
538
|
958 |
\begin{center}
|
|
568
|
959 |
\begin{tabular}{l@{\hspace{1mm}}c@{\hspace{5mm}}l}
|
|
|
960 |
$\textit{inj}\;(c)\;c\,Empty$ & $\dn$ & $\Char\,c$\\
|
|
|
961 |
$\textit{inj}\;(r_1 + r_2)\;c\; (\Left\; v)$ & $\dn$ & $\Left \; (\textit{inj}\; r_1 \; c\,v)$\\
|
|
|
962 |
$\textit{inj}\;(r_1 + r_2)\,c\; (\Right\;v)$ & $\dn$ & $\Right \; (\textit{inj}\;r_2\;c \; v)$\\
|
|
|
963 |
$\textit{inj}\;(r_1 \cdot r_2)\; c\;(\Seq \; v_1 \; v_2)$ & $\dn$ &
|
|
|
964 |
$\Seq \; (\textit{inj}\;r_1\;c\;v_1) \; v_2$\\
|
|
|
965 |
$\textit{inj}\;(r_1 \cdot r_2)\; c\;(\Left \; (\Seq \; v_1\;v_2) )$ &
|
|
|
966 |
$\dn$ & $\Seq \; (\textit{inj}\,r_1\,c\,v_1)\; v_2$\\
|
|
|
967 |
$\textit{inj}\;(r_1 \cdot r_2)\; c\; (\Right\; v)$ & $\dn$ & $\Seq\; (\textit{mkeps}\; r_1) \; (\textit{inj} \; r_2\;c\;v)$\\
|
|
|
968 |
$\textit{inj}\;(r^*)\; c \; (\Seq \; v\; (\Stars\;vs))$ & $\dn$ & $\Stars\;\,((\textit{inj}\;r\;c\;v)\,::\,vs)$\\
|
|
538
|
969 |
\end{tabular}
|
|
|
970 |
\end{center}
|
|
|
971 |
|
|
|
972 |
\noindent
|
|
568
|
973 |
The function does a recursion on
|
|
|
974 |
the shape of regular
|
|
|
975 |
expression $r_i$ and value $v_{i+1}$.
|
|
|
976 |
Intuitively, each clause analyses
|
|
|
977 |
how $r_i$ could have transformed when being
|
|
|
978 |
derived by $c$, identifying which subpart
|
|
|
979 |
of $v_{i+1}$ has the ``hole''
|
|
|
980 |
to inject the character back into.
|
|
|
981 |
Once the character is
|
|
|
982 |
injected back to that sub-value;
|
|
|
983 |
$\inj$ assembles all things together
|
|
|
984 |
to form a new value.
|
|
|
985 |
|
|
|
986 |
For instance, the last clause is an
|
|
|
987 |
injection into a sequence value $v_{i+1}$
|
|
|
988 |
whose second child
|
|
|
989 |
value is a star, and the shape of the
|
|
|
990 |
regular expression $r_i$ before injection
|
|
|
991 |
is a star.
|
|
|
992 |
We therefore know
|
|
|
993 |
the derivative
|
|
|
994 |
starts on a star and ends as a sequence:
|
|
|
995 |
\[
|
|
|
996 |
(r^*) \backslash c \longrightarrow r\backslash c \cdot r^*
|
|
|
997 |
\]
|
|
|
998 |
during which an iteration of the star
|
|
|
999 |
had just been unfolded, giving the below
|
|
|
1000 |
value inhabitation relation:
|
|
|
1001 |
\[
|
|
|
1002 |
\vdash \Seq \; v \; (\Stars \; vs) : (r\backslash c) \cdot r^*.
|
|
|
1003 |
\]
|
|
|
1004 |
The value list $vs$ corresponds to
|
|
|
1005 |
matched star iterations,
|
|
|
1006 |
and the ``hole'' lies in $v$ because
|
|
|
1007 |
\[
|
|
|
1008 |
\vdash v: r\backslash c.
|
|
|
1009 |
\]
|
|
|
1010 |
Finally,
|
|
|
1011 |
$\inj \; r \;c \; v$ is prepended
|
|
|
1012 |
to the previous list of iterations, and then
|
|
|
1013 |
wrapped under the $\Stars$
|
|
|
1014 |
constructor, giving us $\Stars \; ((\inj \; r \; c \; v) ::vs)$.
|
|
538
|
1015 |
|
|
568
|
1016 |
Recall that lemma
|
|
|
1017 |
\ref{mePosix} tells us
|
|
|
1018 |
$\mkeps$ always selects the POSIX matching among
|
|
|
1019 |
multiple values that flatten to the empty string.
|
|
|
1020 |
Now $\inj$ preserves the POSIXness, provided
|
|
|
1021 |
the value before injection is POSIX:
|
|
|
1022 |
\begin{lemma}\label{injPosix}
|
|
|
1023 |
If
|
|
|
1024 |
\[
|
|
|
1025 |
(r \backslash c, s) \rightarrow v
|
|
|
1026 |
\]
|
|
|
1027 |
then
|
|
|
1028 |
\[
|
|
|
1029 |
(r, c :: s) \rightarrow (\inj r \; c\; v).
|
|
|
1030 |
\]
|
|
|
1031 |
\end{lemma}
|
|
|
1032 |
\begin{proof}
|
|
|
1033 |
By induction on $r$.
|
|
|
1034 |
The involved cases are sequence and star.
|
|
|
1035 |
When $r = a \cdot b$, there could be
|
|
|
1036 |
three cases for the value $v$ satisfying $\vdash v:a\backslash c$.
|
|
|
1037 |
We give the reasoning why $\inj \; r \; c \; v$ is POSIX in each
|
|
|
1038 |
case.
|
|
|
1039 |
\begin{itemize}
|
|
|
1040 |
\item
|
|
|
1041 |
$v = \Seq \; v_a \; v_b$.\\
|
|
|
1042 |
The ``not nullable'' clause of the $\inj$ function is taken:
|
|
|
1043 |
\begin{center}
|
|
|
1044 |
\begin{tabular}{lcl}
|
|
|
1045 |
$\inj \; r \; c \; v$ & $=$ & $ \inj \;\; (a \cdot b) \;\; c \;\; (\Seq \; v_a \; v_b) $\\
|
|
|
1046 |
& $=$ & $\Seq \; (\inj \;a \; c \; v_a) \; v_b$
|
|
|
1047 |
\end{tabular}
|
|
|
1048 |
\end{center}
|
|
|
1049 |
We know that there exists a unique pair of
|
|
|
1050 |
$s_a$ and $s_b$ satisfaying
|
|
|
1051 |
$(a \backslash c, s_a) \rightarrow v_a$,
|
|
|
1052 |
$(b , s_b) \rightarrow v_b$, and
|
|
|
1053 |
$\nexists s_3 \; s_4. s_3 \neq [] \land s_a @ s_3 \in
|
|
|
1054 |
L \; (a\backslash c) \land
|
|
|
1055 |
s_4 \in L \; b$.
|
|
|
1056 |
The last condition gives us
|
|
|
1057 |
$\nexists s_3 \; s_4. s_3 \neq [] \land (c :: s_a )@ s_3 \in
|
|
|
1058 |
L \; a \land
|
|
|
1059 |
s_4 \in L \; b$.
|
|
|
1060 |
By induction hypothesis, $(a, c::s_a) \rightarrow \inj \; a \; c \; v_a $ holds,
|
|
|
1061 |
and this gives us
|
|
|
1062 |
\[
|
|
|
1063 |
(a\cdot b, (c::s_a)@s_b) \rightarrow \Seq \; (\inj \; a\;c \;v_a) \; v_b.
|
|
|
1064 |
\]
|
|
|
1065 |
\item
|
|
|
1066 |
$v = \Left \; (\Seq \; v_a \; v_b)$\\
|
|
|
1067 |
The argument is almost identical to the above case,
|
|
|
1068 |
except that a different clause of $\inj$ is taken:
|
|
|
1069 |
\begin{center}
|
|
|
1070 |
\begin{tabular}{lcl}
|
|
|
1071 |
$\inj \; r \; c \; v$ & $=$ & $ \inj \;\; (a \cdot b) \;\; c \;\; (\Left \; (\Seq \; v_a \; v_b)) $\\
|
|
|
1072 |
& $=$ & $\Seq \; (\inj \;a \; c \; v_a) \; v_b$
|
|
|
1073 |
\end{tabular}
|
|
|
1074 |
\end{center}
|
|
|
1075 |
With a similar reasoning,
|
|
538
|
1076 |
|
|
568
|
1077 |
\[
|
|
|
1078 |
(a\cdot b, (c::s_a)@s_b) \rightarrow \Seq \; (\inj \; a\;c \;v_a) \; v_b.
|
|
|
1079 |
\]
|
|
|
1080 |
again holds.
|
|
|
1081 |
\item
|
|
|
1082 |
$v = \Right \; v_b$\\
|
|
|
1083 |
Again the injection result would be
|
|
|
1084 |
\begin{center}
|
|
|
1085 |
\begin{tabular}{lcl}
|
|
|
1086 |
$\inj \; r \; c \; v$ & $=$ & $ \inj \;\; (a \cdot b) \;\; c \;\; \Right \; (v_b) $\\
|
|
|
1087 |
& $=$ & $\Seq \; (\mkeps \; a) \; (\inj \;b \; c\; v_b)$
|
|
|
1088 |
\end{tabular}
|
|
|
1089 |
\end{center}
|
|
|
1090 |
We know that $a$ must be nullable,
|
|
|
1091 |
allowing us to call $\mkeps$ and get
|
|
|
1092 |
\[
|
|
|
1093 |
(a, []) \rightarrow \mkeps \; a.
|
|
|
1094 |
\]
|
|
|
1095 |
Also by inductive hypothesis
|
|
|
1096 |
\[
|
|
|
1097 |
(b, c::s) \rightarrow \inj\; b \; c \; v_b
|
|
|
1098 |
\]
|
|
|
1099 |
holds.
|
|
|
1100 |
In addition, as
|
|
|
1101 |
$\Right \;v_b$ instead of $\Left \ldots$ is
|
|
|
1102 |
the POSIX value for $v$, it must be the case
|
|
|
1103 |
that $s \notin L \;( (a\backslash c)\cdot b)$.
|
|
|
1104 |
This tells us that
|
|
|
1105 |
\[
|
|
|
1106 |
\nexists s_3 \; s_4.
|
|
|
1107 |
s_3 @s_4 = s \land s_3 \in L \; (a\backslash c)
|
|
|
1108 |
\land s_4 \in L \; b
|
|
|
1109 |
\]
|
|
|
1110 |
which translates to
|
|
|
1111 |
\[
|
|
|
1112 |
\nexists s_3 \; s_4. \; s_3 \neq [] \land
|
|
|
1113 |
s_3 @s_4 = c::s \land s_3 \in L \; a
|
|
|
1114 |
\land s_4 \in L \; b.
|
|
|
1115 |
\]
|
|
|
1116 |
(Which basically says there cannot be a longer
|
|
|
1117 |
initial split for $s$ other than the empty string.)
|
|
|
1118 |
Therefore we have $\Seq \; (\mkeps \; a) \;(\inj \;b \; c\; v_b)$
|
|
|
1119 |
as the POSIX value for $a\cdot b$.
|
|
|
1120 |
\end{itemize}
|
|
|
1121 |
The star case can be proven similarly.
|
|
|
1122 |
\end{proof}
|
|
|
1123 |
\noindent
|
|
|
1124 |
Putting all the functions $\inj$, $\mkeps$, $\backslash$ together
|
|
|
1125 |
by following the procedure outlined in the diagram \ref{graph:inj},
|
|
538
|
1126 |
and taking into consideration the possibility of a non-match,
|
|
568
|
1127 |
a lexer can be built with the following recursive definition:
|
|
538
|
1128 |
\begin{center}
|
|
539
|
1129 |
\begin{tabular}{lcl}
|
|
568
|
1130 |
$\lexer \; r \; [] $ & $=$ & $\textit{if} \; (\nullable \; r)\; \textit{then}\; \Some(\mkeps \; r) \; \textit{else} \; \None$\\
|
|
|
1131 |
$\lexer \; r \;c::s$ & $=$ & $\textit{case}\; (\lexer \; (r\backslash c) \; s) \;\textit{of}\; $\\
|
|
|
1132 |
& & $\quad \phantom{\mid}\; \None \implies \None$\\
|
|
|
1133 |
& & $\quad \mid \Some(v) \implies \Some(\inj \; r\; c\; v)$
|
|
538
|
1134 |
\end{tabular}
|
|
|
1135 |
\end{center}
|
|
568
|
1136 |
\noindent
|
|
|
1137 |
The central property of the $\lexer$ is that it gives the correct result by
|
|
|
1138 |
$\POSIX$ standards:
|
|
573
|
1139 |
\begin{theorem}\label{lexerCorrectness}
|
|
568
|
1140 |
The $\lexer$ based on derivatives and injections is correct:
|
|
|
1141 |
\begin{center}
|
|
|
1142 |
\begin{tabular}{lcl}
|
|
|
1143 |
$\lexer \; r \; s = \Some(v)$ & $ \Longleftrightarrow$ & $ (r, \; s) \rightarrow v$\\
|
|
|
1144 |
$\lexer \;r \; s = \None $ & $\Longleftrightarrow$ & $ \neg(\exists v. (r, s) \rightarrow v)$
|
|
|
1145 |
\end{tabular}
|
|
|
1146 |
\end{center}
|
|
|
1147 |
\end{theorem}
|
|
|
1148 |
\begin{proof}
|
|
|
1149 |
By induction on $s$. $r$ is allowed to be an arbitrary regular expression.
|
|
|
1150 |
The $[]$ case is proven by lemma \ref{mePosix}, and the inductive case
|
|
|
1151 |
by lemma \ref{injPosix}.
|
|
|
1152 |
\end{proof}
|
|
538
|
1153 |
\noindent
|
|
539
|
1154 |
As we did earlier in this chapter on the matcher, one can
|
|
|
1155 |
introduce simplification on the regex.
|
|
568
|
1156 |
However, now one needs to do a backward phase and make sure
|
|
539
|
1157 |
the values align with the regular expressions.
|
|
|
1158 |
Therefore one has to
|
|
538
|
1159 |
be careful not to break the correctness, as the injection
|
|
|
1160 |
function heavily relies on the structure of the regexes and values
|
|
|
1161 |
being correct and matching each other.
|
|
|
1162 |
It can be achieved by recording some extra rectification functions
|
|
|
1163 |
during the derivatives step, and applying these rectifications in
|
|
|
1164 |
each run during the injection phase.
|
|
568
|
1165 |
With extra care
|
|
|
1166 |
one can show that POSIXness will not be affected---although it is much harder
|
|
538
|
1167 |
to establish.
|
|
|
1168 |
Some initial results in this regard have been
|
|
|
1169 |
obtained in \cite{AusafDyckhoffUrban2016}.
|
|
|
1170 |
|
|
568
|
1171 |
However, with all the simplification rules allowed
|
|
|
1172 |
in an injection-based lexer, one could still end up in
|
|
|
1173 |
trouble, when cases that require more involved and aggressive
|
|
|
1174 |
simplifications arise.
|
|
|
1175 |
\section{A Case Requring More Aggressive Simplifications}
|
|
539
|
1176 |
For example, when starting with the regular
|
|
|
1177 |
expression $(a^* \cdot a^*)^*$ and building a few successive derivatives (around 10)
|
|
|
1178 |
w.r.t.~the character $a$, one obtains a derivative regular expression
|
|
|
1179 |
with more than 9000 nodes (when viewed as a tree)
|
|
|
1180 |
even with simplification.
|
|
|
1181 |
\begin{figure}
|
|
|
1182 |
\begin{tikzpicture}
|
|
|
1183 |
\begin{axis}[
|
|
|
1184 |
xlabel={$n$},
|
|
|
1185 |
ylabel={size},
|
|
|
1186 |
legend entries={Naive Matcher},
|
|
|
1187 |
legend pos=north west,
|
|
|
1188 |
legend cell align=left]
|
|
|
1189 |
\addplot[red,mark=*, mark options={fill=white}] table {BetterWaterloo.data};
|
|
|
1190 |
\end{axis}
|
|
|
1191 |
\end{tikzpicture}
|
|
|
1192 |
\caption{Size of $(a^*\cdot a^*)^*$ against $\protect\underbrace{aa\ldots a}_\text{n \textit{a}s}$}
|
|
|
1193 |
\end{figure}\label{fig:BetterWaterloo}
|
|
|
1194 |
|
|
568
|
1195 |
That is because Sulzmann and Lu's
|
|
|
1196 |
injection-based lexing algorithm keeps a lot of
|
|
541
|
1197 |
"useless" values that will not be used.
|
|
539
|
1198 |
These different ways of matching will grow exponentially with the string length.
|
|
568
|
1199 |
Take
|
|
|
1200 |
\[
|
|
|
1201 |
r= (a^*\cdot a^*)^* \quad and \quad
|
|
|
1202 |
s=\underbrace{aa\ldots a}_\text{n \textit{a}s}
|
|
|
1203 |
\]
|
|
|
1204 |
as an example.
|
|
|
1205 |
This is a highly ambiguous regular expression, with
|
|
|
1206 |
many ways to split up the string into multiple segments for
|
|
|
1207 |
different star iteratioins,
|
|
573
|
1208 |
and for each segment
|
|
|
1209 |
multiple ways of splitting between
|
|
568
|
1210 |
the two $a^*$ sub-expressions.
|
|
573
|
1211 |
When $n$ is equal to $1$, there are two lexical values for
|
|
|
1212 |
the match:
|
|
|
1213 |
\[
|
|
|
1214 |
\Stars \; [\Seq \; (\Stars \; [\Char \; a])\; (\Stars \; [])] \quad (value 1)
|
|
|
1215 |
\]
|
|
|
1216 |
and
|
|
|
1217 |
\[
|
|
|
1218 |
\Stars \; [\Seq \; (\Stars \; [])\; (\Stars \; [\Char \; a])] \quad (value 2)
|
|
|
1219 |
\]
|
|
|
1220 |
The derivative of $\derssimp \;s \; r$ is
|
|
|
1221 |
\[
|
|
|
1222 |
(a^*a^* + a^*)\cdot(a^*a^*)^*.
|
|
|
1223 |
\]
|
|
|
1224 |
The $a^*a^*$ and $a^*$ in the first child of the above sequence
|
|
|
1225 |
correspond to value 1 and value 2, respectively.
|
|
|
1226 |
When $n=2$, the number goes up to 7:
|
|
|
1227 |
\[
|
|
|
1228 |
\Stars \; [\Seq \; (\Stars \; [\Char \; a, \Char \; a])\; (\Stars \; [])]
|
|
|
1229 |
\]
|
|
|
1230 |
,
|
|
|
1231 |
\[
|
|
|
1232 |
\Stars \; [\Seq \; (\Stars \; [\Char \; a])\; (\Stars \; [\Char \; a])]
|
|
|
1233 |
\]
|
|
|
1234 |
,
|
|
|
1235 |
\[
|
|
|
1236 |
\Stars \; [\Seq \; (\Stars \; [])\; (\Stars \; [\Char \; a, \Char \; a])]
|
|
|
1237 |
\]
|
|
|
1238 |
,
|
|
|
1239 |
\[
|
|
|
1240 |
\Stars \; [\Seq \; (\Stars \; [\Char \; a])\; (\Stars \; []), \Seq \; (\Stars \; [\Char\;a])\; (\Stars\; []) ]
|
|
|
1241 |
\]
|
|
|
1242 |
,
|
|
|
1243 |
\[
|
|
|
1244 |
\Stars \; [\Seq \; (\Stars \; [\Char \; a])\; (\Stars \; []),
|
|
|
1245 |
\Seq \; (\Stars \; [])\; (\Stars \; [\Char \; a])
|
|
|
1246 |
]
|
|
|
1247 |
\]
|
|
|
1248 |
,
|
|
|
1249 |
\[
|
|
|
1250 |
\Stars \; [
|
|
|
1251 |
\Seq \; (\Stars \; [])\; (\Stars \; [\Char \; a]),
|
|
|
1252 |
\Seq \; (\Stars \; [])\; (\Stars \; [\Char \; a])
|
|
|
1253 |
]
|
|
|
1254 |
\]
|
|
|
1255 |
and
|
|
|
1256 |
\[
|
|
|
1257 |
\Stars \; [
|
|
|
1258 |
\Seq \; (\Stars \; [])\; (\Stars \; [\Char \; a]),
|
|
|
1259 |
\Seq \; (\Stars \; [\Char \; a])\; (\Stars \; [])
|
|
|
1260 |
]
|
|
|
1261 |
\]
|
|
|
1262 |
And $\derssimp \; aa \; (a^*a^*)^*$ would be
|
|
|
1263 |
\[
|
|
|
1264 |
((a^*a^* + a^*)+a^*)\cdot(a^*a^*)^* +
|
|
|
1265 |
(a^*a^* + a^*)\cdot(a^*a^*)^*.
|
|
|
1266 |
\]
|
|
|
1267 |
which removes two out of the seven terms corresponding to the
|
|
|
1268 |
seven distinct lexical values.
|
|
|
1269 |
|
|
|
1270 |
It is not surprising that there are exponentially many
|
|
|
1271 |
distinct lexical values that cannot be eliminated by
|
|
|
1272 |
the simple-minded simplification of $\derssimp$.
|
|
|
1273 |
|
|
568
|
1274 |
A lexer without a good enough strategy to
|
|
|
1275 |
deduplicate will naturally
|
|
|
1276 |
have an exponential runtime on ambiguous regular expressions.
|
|
538
|
1277 |
|
|
573
|
1278 |
On the other hand, the
|
|
|
1279 |
$\POSIX$ value for $r= (a^*\cdot a^*)^*$ and
|
|
|
1280 |
$s=\underbrace{aa\ldots a}_\text{n \textit{a}s}$ is
|
|
|
1281 |
\[
|
|
|
1282 |
\Stars\,
|
|
|
1283 |
[\Seq \; (\Stars\,[\underbrace{\Char(a),\ldots,\Char(a)}_\text{n iterations}]), \Stars\,[]]
|
|
|
1284 |
\]
|
|
|
1285 |
and at any moment the subterms in a regular expression
|
|
|
1286 |
that will result in a POSIX value is only
|
|
|
1287 |
a minority among the many other terms,
|
|
|
1288 |
and one can remove ones that are absolutely not possible to
|
|
|
1289 |
be POSIX.
|
|
|
1290 |
In the above example,
|
|
579
|
1291 |
\begin{equation}\label{eqn:growth2}
|
|
573
|
1292 |
((a^*a^* + \underbrace{a^*}_\text{A})+\underbrace{a^*}_\text{duplicate of A})\cdot(a^*a^*)^* +
|
|
|
1293 |
\underbrace{(a^*a^* + a^*)\cdot(a^*a^*)^*}_\text{further simp removes this}.
|
|
579
|
1294 |
\end{equation}
|
|
573
|
1295 |
can be further simplified by
|
|
|
1296 |
removing the underlined term first,
|
|
|
1297 |
which would open up possibilities
|
|
|
1298 |
of further simplification that removes the
|
|
|
1299 |
underbraced part.
|
|
|
1300 |
The result would be
|
|
|
1301 |
\[
|
|
|
1302 |
(\underbrace{a^*a^*}_\text{term 1} + \underbrace{a^*}_\text{term 2})\cdot(a^*a^*)^*.
|
|
|
1303 |
\]
|
|
|
1304 |
with corresponding values
|
|
|
1305 |
\begin{center}
|
|
|
1306 |
\begin{tabular}{lr}
|
|
|
1307 |
$\Stars \; [\Seq \; (\Stars \; [\Char \; a, \Char \; a])\; (\Stars \; [])]$ & $(\text{term 1})$\\
|
|
|
1308 |
$\Stars \; [\Seq \; (\Stars \; [\Char \; a])\; (\Stars \; [\Char \; a])] $ & $(\text{term 2})$
|
|
|
1309 |
\end{tabular}
|
|
|
1310 |
\end{center}
|
|
|
1311 |
Other terms with an underlying value such as
|
|
|
1312 |
\[
|
|
|
1313 |
\Stars \; [\Seq \; (\Stars \; [])\; (\Stars \; [\Char \; a, \Char \; a])]
|
|
|
1314 |
\]
|
|
|
1315 |
is simply too hopeless to contribute a POSIX lexical value,
|
|
|
1316 |
and is therefore thrown away.
|
|
538
|
1317 |
|
|
573
|
1318 |
Ausaf and Dyckhoff and Urban \cite{AusafDyckhoffUrban2016}
|
|
|
1319 |
have come up with some simplification steps, however those steps
|
|
|
1320 |
are not yet sufficiently strong so that they achieve the above effects.
|
|
|
1321 |
And even with these relatively mild simplifications the proof
|
|
|
1322 |
is already quite a bit complicated than the theorem \ref{lexerCorrectness}.
|
|
|
1323 |
One would prove something like:
|
|
|
1324 |
\[
|
|
|
1325 |
\textit{If}\; (\textit{snd} \; (\textit{simp} \; r\backslash c), s) \rightarrow v \;\;
|
|
|
1326 |
\textit{then}\;\; (r, c::s) \rightarrow
|
|
|
1327 |
\inj\;\, r\, \;c \;\, ((\textit{fst} \; (\textit{simp} \; r \backslash c))\; v)
|
|
|
1328 |
\]
|
|
|
1329 |
instead of the simple lemma \ref{injPosix}, where now $\textit{simp}$
|
|
|
1330 |
not only has to return a simplified regular expression,
|
|
|
1331 |
but also what specific simplifications
|
|
|
1332 |
has been done as a function on values
|
|
|
1333 |
showing how one can transform the value
|
|
|
1334 |
underlying the simplified regular expression
|
|
|
1335 |
to the unsimplified one.
|
|
|
1336 |
|
|
|
1337 |
We therefore choose a slightly different approach to
|
|
|
1338 |
get better simplifications, which uses
|
|
|
1339 |
some augmented data structures compared to
|
|
|
1340 |
plain regular expressions.
|
|
|
1341 |
We call them \emph{annotated}
|
|
|
1342 |
regular expressions.
|
|
|
1343 |
With annotated regular expressions,
|
|
|
1344 |
we can avoid creating the intermediate values $v_1,\ldots v_n$ and a
|
|
|
1345 |
second phase altogether.
|
|
|
1346 |
In the meantime, we can also ensure that simplifications
|
|
|
1347 |
are easily handled without breaking the correctness of the algorithm.
|
|
|
1348 |
We introduce this new datatype and the
|
|
|
1349 |
corresponding algorithm in the next chapter.
|
|
538
|
1350 |
|
|
|
1351 |
|
|
|
1352 |
|
|
|
1353 |
|