--- a/thys2/Paper/document/root.tex Sun Feb 06 00:02:04 2022 +0000
+++ b/thys2/Paper/document/root.tex Mon Feb 07 01:11:25 2022 +0000
@@ -49,7 +49,7 @@
\def\S{\mathit{S}}
\newcommand{\ZERO}{\mbox{\bf 0}}
\newcommand{\ONE}{\mbox{\bf 1}}
-
+\def\rs{\mathit{rs}}
\def\Brz{Brzozowski}
\def\der{\backslash}
@@ -83,17 +83,19 @@
of the regular expression. The purpose of the bitcodes is to generate POSIX values incrementally while
derivatives are calculated. They also help with designing
an ``aggressive'' simplification function that keeps the size of
- derivatives small. Without simplification the size derivatives can grow
- exponentially resulting in an extremely slow lexing algorithm. In this
+ derivatives finite. Without simplification the size derivatives can grow
+ arbitrarily big resulting in an extremely slow lexing algorithm. In this
paper we describe a variant of Sulzmann and Lu's algorithm: Our
algorithm is a recursive functional program, whereas Sulzmann
and Lu's version involves a fixpoint construction. We \textit{(i)}
prove in Isabelle/HOL that our program is correct and generates
- unique POSIX values; we also \textit{(ii)} establish a polynomial
- bound for the size of the derivatives. The size can be seen as a
- proxy measure for the efficiency of the lexing algorithm: because of
- the polynomial bound our algorithm does not suffer from
- the exponential blowup in earlier works.
+ unique POSIX values; we also \textit{(ii)} establish a finite
+ bound for the size of the derivatives.
+
+ %The size can be seen as a
+ %proxy measure for the efficiency of the lexing algorithm: because of
+ %the polynomial bound our algorithm does not suffer from
+ %the exponential blowup in earlier works.
% Brzozowski introduced the notion of derivatives for regular
% expressions. They can be used for a very simple regular expression