--- a/ChengsongTanPhdThesis/Chapters/Bitcoded2.tex Fri Dec 30 01:52:32 2022 +0000
+++ b/ChengsongTanPhdThesis/Chapters/Bitcoded2.tex Fri Dec 30 17:37:51 2022 +0000
@@ -16,7 +16,7 @@
each intermediate derivative result. This allows
us to make $\blexer$ much more efficient.
Sulzmann and Lu already introduced some simplifications for bitcoded regular expressions,
-but their simplification functions were inefficient and in some cases needs fixing.
+but their simplification functions were inefficient and in some cases needed fixing.
%We contrast our simplification function
%with Sulzmann and Lu's, indicating the simplicity of our algorithm.
%This is another case for the usefulness
@@ -51,7 +51,7 @@
\end{center}
because the duplicates are
not next to each other and therefore the rule
-$r+ r \rightarrow r$ does not fire.
+$r+ r \rightarrow r$ from $\textit{simp}$ does not fire.
One would expect a better simplification function to work in the
following way:
\begin{gather*}
@@ -94,7 +94,7 @@
$_{bs}\sum ((\map \; (\fuse \; bs')\; rs_1) @ rs_2)$\\
$\textit{simp}\_{SL} \; _{bs}\sum[r]$ & $\dn$ & $\fuse \; bs \; (\textit{simp}\_{SL} \; r)$\\
$\textit{simp}\_{SL} \; _{bs}\sum(r::rs)$ & $\dn$ & $_{bs}\sum
- (\nub \; (\filter \; (\not \circ \zeroable)\;((\textit{simp}\_{SL} \; r) :: \map \; \textit{simp}\_{SL} \; rs)))$\\
+ (\nub \; (\filter \; (\neg\zeroable)\;((\textit{simp}\_{SL} \; r) :: \map \; \textit{simp}\_{SL} \; rs)))$\\
\end{tabular}
\end{center}
@@ -163,7 +163,7 @@
\noindent
We implemented this lexing algorithm in Scala,
and found that the final derivative regular expression
-size grows exponentially fast (note the logarithmic scale):
+size still grows exponentially (note the logarithmic scale):
\begin{figure}[H]
\centering
\begin{tikzpicture}
@@ -206,17 +206,18 @@
\end{figure}
\noindent
which seems like a counterexample for
-their linear complexity claim:
+Sulzmann and Lu's linear complexity claim
+in their paper \cite{Sulzmann2014}:
\begin{quote}\it
-Linear-Time Complexity Claim \\It is easy to see that each call of one of the functions/operations:
-simp, fuse, mkEpsBC and isPhi leads to subcalls whose number is bound by the size of the regular expression involved. We claim that thanks to aggressively applying simp this size remains finite. Hence, we can argue that the above mentioned functions/operations have constant time complexity which implies that we can incrementally compute bit-coded parse trees in linear time in the size of the input.
+``Linear-Time Complexity Claim \\It is easy to see that each call of one of the functions/operations:
+simp, fuse, mkEpsBC and isPhi leads to subcalls whose number is bound by the size of the regular expression involved. We claim that thanks to aggressively applying simp this size remains finite. Hence, we can argue that the above mentioned functions/operations have constant time complexity which implies that we can incrementally compute bit-coded parse trees in linear time in the size of the input.''
\end{quote}
\noindent
The assumption that the size of the regular expressions
in the algorithm
-would stay below a finite constant is not true, not in the
+would stay below a finite constant is not true, at least not in the
examples we considered.
-The main reason behind this is that (i) the $\textit{nub}$
+The main reason behind this is that (i) Haskell's $\textit{nub}$
function requires identical annotations between two
annotated regular expressions to qualify as duplicates,
and therefore cannot simplify cases like $_{SZZ}a^*+_{SZS}a^*$
@@ -232,24 +233,24 @@
\end{center}
\noindent
clause, and therefore is not strong enough to simplify all
-needed parts of the regular expression. Moreover, even if the regular expressions size
-do stay finite, one has to take into account that
-the $\textit{simp}\_{SL}$ function is applied many times
-in each derivative step, and that number is not necessarily
-a constant with respect to the size of the regular expression.
+needed parts of the regular expression. Moreover,
+the $\textit{simp}\_{SL}$ function is applied repeatedly
+in each derivative step until a fixed point is reached,
+which makes the algorithm even more
+unpredictable and inefficient.
%To not get ``caught off guard'' by
%these counterexamples,
%one needs to be more careful when designing the
%simplification function and making claims about them.
\section{Our $\textit{Simp}$ Function}
-We will now introduce our simplification function.
+We will now introduce our own simplification function.
%by making a contrast with $\textit{simp}\_{SL}$.
We also describe
the ideas behind Sulzmann and Lu's $\textit{simp}\_{SL}$
algorithm
-and why it fails to achieve the desired effect.
-Our simplification function comes with a formal
+and why it fails to achieve the desired effect of keeping the sizes of derivatives finitely bounded.
+In addition, our simplification function will come with a formal
correctness proof.
\subsection{Flattening Nested Alternatives}
The idea behind the clause
@@ -282,7 +283,7 @@
$((a^* a^*)+\underline{(a^* + a^*)})\cdot (a^*a^*)^*+
((a^*a^*)+a^*)\cdot (a^*a^*)^*$
\end{center}
-due to the underlined part not being in the head
+due to the underlined part not being the head
of the alternative.
We define our flatten operation so that it flattens
@@ -400,7 +401,7 @@
\noindent
The simplification (named $\textit{bsimp}$ for \emph{b}it-coded)
does a pattern matching on the regular expression.
-When it detected that the regular expression is an alternative or
+When it detects that the regular expression is an alternative or
sequence, it will try to simplify its children regular expressions
recursively and then see if one of the children turns into $\ZERO$ or
$\ONE$, which might trigger further simplification at the current level.
@@ -459,15 +460,15 @@
\begin{center}
\begin{tabular}{lcl}
$\textit{blexer\_simp}\;r\,s$ & $\dn$ &
- $\textit{let}\;a = (r^\uparrow)\backslash_{simp}\, s\;\textit{in}$\\
+ $\textit{let}\;a = (r^\uparrow)\backslash_{bsimp}\, s\;\textit{in}$\\
& & $\;\;\textit{if}\; \textit{bnullable}(a)$\\
& & $\;\;\textit{then}\;\textit{decode}\,(\textit{bmkeps}\,a)\,r$\\
& & $\;\;\textit{else}\;\textit{None}$
\end{tabular}
\end{center}
-
\noindent
-This algorithm keeps the regular expression size small.
+This algorithm keeps the regular expression size small,
+as we shall demonstrate with some examples in the next section.
\subsection{Examples $(a+aa)^*$ and $(a^*\cdot a^*)^*$
@@ -510,12 +511,12 @@
\end{tikzpicture}
\end{tabular}
\end{center}
-\caption{Our Improvement over Sulzmann and Lu's in terms of size}
+\caption{Our Improvement over Sulzmann and Lu's in terms of size of the derivatives.}
\end{figure}
\noindent
Given the size difference, it is not
surprising that our $\blexersimp$ significantly outperforms
-$\textit{blexer\_SLSimp}$.
+$\textit{blexer\_SLSimp}$ by Sulzmann and Lu.
In the next section we are going to establish that our
simplification preserves the correctness of the algorithm.
%----------------------------------------------------------------------------------------
@@ -621,7 +622,8 @@
such that one regular expression
in the left-hand-side list is rewritable in one step
to the right-hand-side's regular expression at the same position.
-This helps with defining the ``context rule'' $AL$.\\
+This helps with defining the ``context rule'' $AL$.
+
The reflexive transitive closure of $\rightsquigarrow$ and $\stackrel{s}{\rightsquigarrow}$
are defined in the usual way:
\begin{figure}[H]
@@ -775,7 +777,8 @@
extract the same bitcodes using $\bmkeps$ from the nullable
components of two regular expressions $r$ and $r'$,
if we can rewrite from one to the other in finitely
-many steps.\\
+many steps.
+
For convenience,
we define a predicate for a list of regular expressions
having at least one nullable regular expressions:
@@ -850,7 +853,8 @@
which says that our simplification's helper functions
such as $\distinctBy$ and $\flts$ describe
reducts of $\stackrel{s*}{\rightsquigarrow}$ and
-$\rightsquigarrow^* $.\\
+$\rightsquigarrow^* $.
+
The first lemma to prove is a more general version of
$rs_ 1 \rightsquigarrow^* \distinctBy \; rs_1 \; \phi$:
\begin{lemma}
@@ -972,7 +976,7 @@
derivative regular expressions to the
lexer with simplification applied (by lemma \ref{bderBderssimp}):
\begin{center}
- $a \backslash s \stackrel{*}{\rightsquigarrow} \bderssimp{a}{s} $.
+ $a \backslash s \rightsquigarrow^* \bderssimp{a}{s} $.
\end{center}
We know that they generate the same bits, if the lexing result is a match:
\begin{center}
@@ -998,8 +1002,8 @@
$\nexists v. \; (r, s) \rightarrow v \;\; \textit{iff} \;\; \blexer\;
r\;s = \None$.
\end{center}
-and obtain the corollary that the bit-coded lexer with simplification is
-indeed correctly outputting POSIX lexing result, if such a result exists.
+and obtain the property that the bit-coded lexer with simplification is
+indeed correctly generating a POSIX lexing result, if such a result exists.
\begin{corollary}
$(r, s) \rightarrow v \;\; \textit{iff} \;\; \blexersimp \; r\; s = \Some \; v$\\
$\nexists v. \; (r, s) \rightarrow v \;\; \textit{iff} \;\; \blexersimp\;
@@ -1015,17 +1019,15 @@
that the annotated regular expressions stay unsimplified,
so that one can
correctly compare $v_{i+1}$ and $r_i$ and $v_i$
-in diagram \ref{graph:inj} and
-``fit the key into the lock hole''.
+in diagram \ref{graph:inj}.
-\noindent
We also tried to prove
\begin{center}
$\textit{bsimp} \;\; (\bderssimp{a}{s}) =
\textit{bsimp} \;\; (a\backslash s)$,
\end{center}
but this turns out to be not true.
-A counterexample would be
+A counterexample is
\[ a = [(_{Z}1+_{S}c)\cdot [bb \cdot (_{Z}1+_{S}c)]] \;\;
\text{and} \;\; s = bb.
\]
@@ -1046,7 +1048,8 @@
we will always have this discrepancy.
This is due to
the $\map \; (\fuse\; bs) \; as$ operation
-happening at different locations in the regular expression.\\
+happening at different locations in the regular expression.
+
The rewriting relation
$\rightsquigarrow^*$
allows us to ignore this discrepancy
@@ -1058,7 +1061,8 @@
\end{center}
as equal, because they were both re-written
-from the same expression.\\
+from the same expression.
+
The simplification rewriting rules
given in \ref{rrewriteRules} are by no means
final,