--- a/ChengsongTanPhdThesis/Chapters/Bitcoded1.tex Sat Jul 08 22:18:22 2023 +0100
+++ b/ChengsongTanPhdThesis/Chapters/Bitcoded1.tex Sun Jul 09 00:29:02 2023 +0100
@@ -1181,7 +1181,23 @@
final derivative $a_n$, guided by $v_n$. This can be proved
as follows:
\begin{lemma}\label{bmkepsRetrieve}
- $\bnullable \; a \implies \bmkeps \; a = \retrieve \; a \; (\mkeps \; (\erase \; a))$
+ \mbox{}
+ \begin{itemize}
+ \item
+If $\forall v \in vs. \vdash v : r$, and $\code \; v = \retrieve \; (\internalise\; r) \; v$\\
+then $\code \; (\Stars \; vs) = \retrieve \; _{[]}((\internalise \; r)^*) \; (\Stars \; vs)$
+ \item
+ $\vdash v : r \implies \retrieve \; (r)^\uparrow \; v = \code \; v$
+ \item
+ $\bnullable \; a \implies \bmkeps \; a = \retrieve \; a \; (\mkeps \; (a_\downarrow))$
+ \end{itemize}
+\begin{proof}
+ The first part is by induction on the value list $vs$.
+ The second part is by induction on $r$,
+ and the star case uses the first part.
+ The last part is by a routine induction on $a$.
+\end{proof}
+\noindent
\end{lemma}
\begin{proof}
By a routine induction on $a$.
@@ -1190,34 +1206,34 @@
%The design of $\retrieve$ enables us to extract bitcodes
%from both annotated regular expressions and values.
%$\retrieve$ always ``sucks up'' all the information.
-When more information is stored in the value, we would be able to
-extract more from the value, and vice versa.
-For example in star iterations, $\retrieve$ will be able to extract from $\Stars \; vs$
-exactly the same bitcodes as $\code \; (\Stars \; vs)$:
-\begin{lemma}\label{retrieveEncodeSTARS}
- If $\forall v \in vs. \vdash v : r$, and $\code \; v = \retrieve \; (\internalise\; r) \; v$\\
- then $\code \; (\Stars \; vs) = \retrieve \; _{[]}((\internalise \; r)^*) \; (\Stars \; vs)$
-\end{lemma}
-\begin{proof}
- By induction on the value list $vs$.
-\end{proof}
-\noindent
-Similarly, when the value list does not hold information,
-only the bitcodes plus some delimiter will be recorded:
-\begin{center}
- $\retrieve \; _{bs}((\internalise \; r)^*) \; (\Stars \; [] ) = bs @ [S]$.
-\end{center}
-In general, if we have a regular expression that is just internalised
-and the final lexing result value, we can $\retrieve$ the bitcodes
-that look as if we have en$\code$-ed the value as bitcodes:
-\begin{lemma}
- $\vdash v : r \implies \retrieve \; (r)^\uparrow \; v = \code \; v$
-\end{lemma}
-\begin{proof}
- By induction on $r$.
- The star case uses lemma \ref{retrieveEncodeSTARS}.
-\end{proof}
-\noindent
+%When more information is stored in the value, we would be able to
+%extract more from the value, and vice versa.
+%For example in star iterations, $\retrieve$ will be able to extract from $\Stars \; vs$
+%exactly the same bitcodes as $\code \; (\Stars \; vs)$:
+%\begin{lemma}\label{retrieveEncodeSTARS}
+% If $\forall v \in vs. \vdash v : r$, and $\code \; v = \retrieve \; (\internalise\; r) \; v$\\
+% then $\code \; (\Stars \; vs) = \retrieve \; _{[]}((\internalise \; r)^*) \; (\Stars \; vs)$
+%\end{lemma}
+%\begin{proof}
+% By induction on the value list $vs$.
+%\end{proof}
+%\noindent
+%Similarly, when the value list does not hold information,
+%only the bitcodes plus some delimiter will be recorded:
+%\begin{center}
+% $\retrieve \; _{bs}((\internalise \; r)^*) \; (\Stars \; [] ) = bs @ [S]$.
+%\end{center}
+%In general, if we have a regular expression that is just internalised
+%and the final lexing result value, we can $\retrieve$ the bitcodes
+%that look as if we have en$\code$-ed the value as bitcodes:
+%\begin{lemma}
+% $\vdash v : r \implies \retrieve \; (r)^\uparrow \; v = \code \; v$
+%\end{lemma}
+%\begin{proof}
+% By induction on $r$.
+% The star case uses lemma \ref{retrieveEncodeSTARS}.
+%\end{proof}
+%\noindent
The following property of $\retrieve$ is crucial, as
it provides a "bridge" between $a_0$ and $a_n $ in the
lexing diagram by linking adjacent regular expressions $a_i$ and
@@ -1228,7 +1244,8 @@
before the derivative took place,
provided that the corresponding values are used respectively:
\begin{lemma}\label{retrieveStepwise}
- $\vdash v : (r\backslash c) \implies \retrieve \; (r \backslash c) \; v= \retrieve \; r \; (\inj \; r\; c\; v)$
+ $\vdash v : (a\backslash c)_\downarrow \implies \retrieve \; (a \backslash c) \; v=
+ \retrieve \; a \; (\inj \; a_\downarrow\; c\; v)$
\end{lemma}
\begin{proof}
We do an induction on $r$, generalising over $v$.
@@ -1242,16 +1259,16 @@
holds with simplifications which takes away certain sub-expressions
corresponding to non-POSIX lexical values.
-Before we move on to the next
-helper function, we rewrite $\blexer$ in
-the following way which makes later proofs more convenient:
-\begin{lemma}\label{blexer_retrieve}
-$\blexer \; r \; s = \decode \; (\retrieve \; (\internalise \; r) \; (\mkeps \; (r \backslash s) )) \; r$
-\end{lemma}
-\begin{proof}
- Using lemma \ref{bmkepsRetrieve}.
-\end{proof}
-\noindent
+%Before we move on to the next
+%helper function, we rewrite $\blexer$ in
+%the following way which makes later proofs more convenient:
+%\begin{lemma}\label{blexer_retrieve}
+%$\blexer \; r \; s = \decode \; (\retrieve \; (\internalise \; r) \; (\mkeps \; (r \backslash s) )) \; r$
+%\end{lemma}
+%\begin{proof}
+% Using lemma \ref{bmkepsRetrieve}.
+%\end{proof}
+%\noindent
The function $\retrieve$ allows connecting
between the intermediate
results $a_i$ and $a_{i+1}$ in $\blexer$.
@@ -1351,13 +1368,25 @@
$\blexer\; r \; s = \lexer \; r \; s$
\end{theorem}
\begin{proof}
- From \ref{flex_retrieve} we have that
- $\textit{flex} \; r \; \textit{id} \; s \; \mkeps(r \backslash s) = \blexer \; r \; s$,
- which immediately implies this theorem.
+ We can rewrite the expression $\blexer \; r \; s$ by using lemma \ref{bmkepsRetrieve}:
+\[
+ \blexer \; r \; s = \decode \; (\retrieve \; (\; r^\uparrow) \; (\mkeps \; (r \backslash s) )) \; r
+\]
+ From \ref{flex_retrieve} we have that the left-hand-side is equal to
+\[
+ \textit{flex} \; r \; \textit{id} \; s \; \mkeps \; (r \backslash s),
+\]
+which in turn equals
+\[
+ \lexer \; r \; s.
+\]
+ %which immediately implies this theorem.
\end{proof}
\noindent
-To piece things together and spell out the correctness
-result of the bitcoded lexer more explicitly,
+To piece things together
+%and spell out the correctness
+%result of the bitcoded lexer more explicitly,
+and give the correctness result explicitly,
we use the fact from the previous chapter that
\[
(r, s) \rightarrow v \;\; \textit{iff} \;\; \lexer \; r \; s =\Some \; v
@@ -1366,9 +1395,13 @@
\]
to obtain this corollary:
\begin{corollary}\label{blexerPOSIX}
- The $\blexer$ function correctly implements a POSIX lexer, namely\\
- $(r, s) \rightarrow v \;\; \textit{iff} \;\; \blexer \; r \; s = \Some \; v$\\
+ The $\blexer$ function correctly implements a POSIX lexer, namely
+ \begin{itemize}
+ \item
+ $(r, s) \rightarrow v \;\; \textit{iff} \;\; \blexer \; r \; s = \Some \; v$
+ \item
$\nexists v. (r, s) \rightarrow v\;\; \textit{iff} \;\; \blexer \;r\;s = None$
+ \end{itemize}
\end{corollary}
Our main reason for analysing the bit-coded algorithm over
the injection-based one is that it allows us to define
--- a/ChengsongTanPhdThesis/Chapters/Bitcoded2.tex Sat Jul 08 22:18:22 2023 +0100
+++ b/ChengsongTanPhdThesis/Chapters/Bitcoded2.tex Sun Jul 09 00:29:02 2023 +0100
@@ -453,7 +453,7 @@
we add it as a phase after a derivative is taken.
\begin{center}
\begin{tabular}{lcl}
- $r \backslash_{bsimp} c$ & $\dn$ & $\textit{bsimp}(r \backslash c)$
+ $a \backslash_{bsimp} c$ & $\dn$ & $\textit{bsimp}(a \backslash c)$
\end{tabular}
\end{center}
%Following previous notations
@@ -463,8 +463,8 @@
We extend this from characters to strings:
\begin{center}
\begin{tabular}{lcl}
-$r \backslash_{bsimps} (c\!::\!s) $ & $\dn$ & $(r \backslash_{bsimp}\, c) \backslash_{bsimps}\, s$ \\
-$r \backslash_{bsimps} [\,] $ & $\dn$ & $r$
+$a \backslash_{bsimps} (c\!::\!s) $ & $\dn$ & $(a \backslash_{bsimp}\, c) \backslash_{bsimps}\, s$ \\
+$a \backslash_{bsimps} [\,] $ & $\dn$ & $a$
\end{tabular}
\end{center}
@@ -532,15 +532,27 @@
Given the size difference, it is not
surprising that our $\blexersimp$ significantly outperforms
$\textit{blexer\_SLSimp}$ by Sulzmann and Lu.
+Indeed $\blexersimp$ seems to be a correct algorithm that effectively
+bounds the size of intermediate representations.
+\marginpar{\em more connecting material to make narration more coherent.}
+As promised we will use formal proofs to show that our speculation
+based on these experimental results indeed hold.
+%intuitions indeed hold.
In the next section we are going to establish that our
simplification preserves the correctness of the algorithm.
-
+\section{Correctness of $\blexersimp$}
+A natural thought would be to directly re-use the formal
+proof of $\blexer$'s correctness, with some minor modifications
+but keeping the way the induction is done.
+However we were not able to find a simple way to re-factor
+proof of \ref{blexerCorrect} in chapter \ref{Bitcoded1}.
-\section{Why $\textit{Blexer}$'s Proof Does Not Work}
-The fundamental reason is we cannot extend the correctness proof of theorem 4
-because lemma 13 does not hold anymore when simplifications are involved.
+\subsection{Why $\textit{Blexer}$'s Proof Does Not Work}
+The fundamental reason is %we cannot extend the correctness proof of theorem 4
+because lemma \ref{retrieveStepwise} does not hold
+anymore when simplifications are involved.
\marginpar{\em rephrased things \\so why new \\proof makes sense.}
%The proof details are necessary materials for this thesis
%because it provides necessary context to explain why we need a
@@ -569,34 +581,132 @@
relies crucially on lemma \ref{retrieveStepwise} that says
any value can be retrieved in a stepwise manner, namely:
\begin{equation}\label{eq:stepwise}%eqref: this proposition needs to be referred
- \vdash v : (r\backslash c) \implies \retrieve \; (r \backslash c) \; v= \retrieve \; r \; (\inj \; r\; c\; v)
+ \vdash v : ((a_\downarrow) \backslash c) \implies \retrieve \; (a \backslash c) \; v= \retrieve \; a \; (\inj \; (a_\downarrow) \; c\; v)
\end{equation}
%This no longer holds once we introduce simplifications.
-Simplifications are necessary to control the size of derivatives,
-but they also destroy the structures of the regular expressions
-such that \ref{eq:stepwise} does not hold.
+The regular expressions $a$ and $a\backslash c$ correspond to the intermediate
+result before and after the derivative with respect to $c$, and similarly
+$\inj\; a_\downarrow \; c \; v$ and $v$ correspond to the value before and after the derivative.
+They go in lockstep pairs
+\[
+ (a, \; \inj\; a_\downarrow \; c \; v)\; \text{and} \; (a\backslash c,\; v)
+\]
+and the structure of annotated regular expression and
+value within a pair always align with each other.
-
-We want to prove the correctness of $\blexersimp$ which integrates
-$\textit{bsimp}$ by applying it after each call to the derivative:
+As $\blexersimp$ integrates
+$\textit{bsimp}$ by applying it after each call to the derivatives function,
+%Simplifications are necessary to control the size of derivatives,
+%but they also destroy the structures of the regular expressions
+%such that \ref{eq:stepwise} does not hold.
\begin{center}
\begin{tabular}{lcl}
- $r \backslash_{bsimps} (c\!::\!s) $ & $\dn$ & $(\textit{bsimp} \; (r \backslash\, c)) \backslash_{bsimps}\, s$ \\
-$r \backslash_{bsimps} [\,] $ & $\dn$ & $r$
+ $a \backslash_{bsimps} (c\!::\!s) $ & $\dn$ & $(\textit{bsimp} \; (a \backslash\, c)) \backslash_{bsimps}\, s$ \\
+%$r \backslash_{bsimps} [\,] $ & $\dn$ & $r$
\end{tabular}
-\begin{tabular}{lcl}
- $\textit{blexer\_simp}\;r\,s$ & $\dn$ &
- $\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}
+%\begin{tabular}{lcl}
+% $\textit{blexer\_simp}\;r\,s$ & $\dn$ &
+% $\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
+it becomes a problem to maintain a similar property as \ref{retrieveStepwise}.
Previously without $\textit{bsimp}$ the exact structure of each intermediate
-regular expression is preserved, allowing pairs of inhabitation relations
-in the form $\vdash v : r \backslash c $ and
-$\vdash \inj \; r\; c \; v : r $ to hold in \ref{eq:stepwise}.
+regular expression is preserved,
+%allowing pairs of inhabitation relations
+%in the form $\vdash v : r \backslash c $ and
+%$\vdash \inj \; r\; c \; v : r $ to hold in \ref{eq:stepwise}.
+We can illustrate this using the diagram \ref{fig:inj} in chapter \ref{Inj},
+by zooming in to the middle bit involving $r_i$, $r_{i+1}$, $v_i$ and $v_{i+1}$,
+and adding the bottom row to show how bitcodes encoding the lexing information
+can be extracted from every pair $(r_i, \; v_i)$:
+\begin{center}
+ \begin{tikzpicture}[->, >=stealth', shorten >= 1pt, auto, thick]
+ %\node [rectangle ] (1) at (-7, 2) {$\ldots$};
+ %\node [rectangle, draw] (2) at (-4, 2) {$r_i = _{bs'}(_Za+_Saa)^*$};
+ %\node [rectangle, draw] (3) at (4, 2) {$r_{i+1} = _{bs'}(_Z(_Z\ONE + _S(\ONE \cdot a)))\cdot(_Za+_Saa)^*$};
+ %\node [rectangle] (4) at (9, 2) {$\ldots$};
+ %\node [rectangle] (5) at (-7, -2) {$\ldots$};
+ %\node [rectangle, draw] (6) at (-4, -2) {$v_i = \Stars \; [\Left (a)]$};
+ %\node [rectangle, draw] (7) at ( 4, -2) {$v_{i+1} = \Seq (\Alt (\Left \; \Empty)) \; \Stars \, []$};
+ %\node [rectangle] (8) at ( 9, -2) {$\ldots$};
+ %\node [rectangle] (9) at (-7, -6) {$\ldots$};
+ %\node [rectangle, draw] (10) at (-4, -6) {$\textit{bits}_{i} = bs' @ ZZS$};
+ %\node [rectangle, draw] (11) at (4, -6) {$\textit{bits}_{i+1} = bs'@ ZZS$};
+ %\node [rectangle] (12) at (9, -6) {$\ldots$};
+
+ \node [rectangle ] (1) at (-8, 2) {$\ldots$};
+ \node [rectangle, draw] (2) at (-5, 2) {$r_i = a_\downarrow$};
+ \node [rectangle, draw] (3) at (3, 2) {$r_{i+1} = (a\backslash c)_\downarrow$};
+ \node [rectangle] (4) at (8, 2) {$\ldots$};
+ \node [rectangle] (5) at (-8, -2) {$\ldots$};
+ \node [rectangle, draw] (6) at (-5, -2) {$v_i = \inj\; r \; c \; v$};
+ \node [rectangle, draw] (7) at ( 3, -2) {$v_{i+1} = v$};
+ \node [rectangle] (8) at ( 8, -2) {$\ldots$};
+ \node [rectangle] (9) at (-8, -6) {$\ldots$};
+ \node [rectangle, draw] (10) at (-5, -6) {$\textit{bits}_{i} = bs' @ ZZS$};
+ \node [rectangle, draw] (11) at (3, -6) {$\textit{bits}_{i+1} = bs'@ ZZS$};
+ \node [rectangle] (12) at (8, -6) {$\ldots$};
+
+
+
+ \path (1) edge [] node {} (2);
+ \path (6) edge [] node {} (5);
+ \path (9) edge [] node {} (10);
+
+ \path (11) edge [] node {} (12);
+ \path (8) edge [] node {} (7);
+ \path (3) edge [] node {} (4);
+
+
+ \path (6) edge [dashed,bend right = 30] node {$\retrieve \; a_i \; v_i$} (10);
+ \path (2) edge [dashed,bend left = 48] node {} (10);
+
+ \path (7) edge [dashed,bend right = 30] node {$\retrieve \; a_{i+1} \; v_{i+1}$} (11);
+ \path (3) edge [dashed,bend left = 45] node {} (11);
+
+ \path (2) edge [] node {$\backslash c$} (3);
+ \path (2) edge [dashed, <->] node {$\vdash v_i : r_i$} (6);
+ \path (3) edge [dashed, <->] node {$\vdash v_{i+1} : r_{i+1}$} (7);
+ %\path (6) edge [] node {$\vdash v_i : r_i$} (10);
+ %\path (7) edge [dashed, <->] node {$\vdash v_i : r_i$} (11);
+
+ \path (10) edge [dashed, <->] node {$=$} (11);
+
+ \path (7) edge [] node {$\inj \; r_{i+1} \; a \; v_i$} (6);
+
+% \node [rectangle, draw] (r) at (-6, -1) {$(aa)^*(b+c)$};
+% \node [rectangle, draw] (a) at (-6, 4) {$(aa)^*(_{Z}b + _{S}c)$};
+% \path (r)
+% edge [] node {$\internalise$} (a);
+% \node [rectangle, draw] (a1) at (-3, 1) {$(_{Z}(\ONE \cdot a) \cdot (aa)^*) (_{Z}b + _Sc)$};
+% \path (a)
+% edge [] node {$\backslash a$} (a1);
+%
+% \node [rectangle, draw, three sided] (a21) at (-2.5, 4) {$(_{Z}\ONE \cdot (aa)^*)$};
+% \node [rectangle, draw, three sided1] (a22) at (-0.8, 4) {$(_{Z}b + _{S}c)$};
+% \path (a1)
+% edge [] node {$\backslash a$} (a21);
+% \node [rectangle, draw] (a3) at (0.5, 2) {$_{ZS}(_{Z}\ONE + \ZERO)$};
+% \path (a22)
+% edge [] node {$\backslash b$} (a3);
+% \path (a21)
+% edge [dashed, bend right] node {} (a3);
+% \node [rectangle, draw] (bs) at (2, 4) {$ZSZ$};
+% \path (a3)
+% edge [below] node {$\bmkeps$} (bs);
+% \node [rectangle, draw] (v) at (3, 0) {$\Seq \; (\Stars\; [\Seq \; a \; a]) \; (\Left \; b)$};
+% \path (bs)
+% edge [] node {$\decode$} (v);
+
+
+ \end{tikzpicture}
+ %\caption{$\blexer$ with the regular expression $(aa)^*(b+c)$ and $aab$}
+\end{center}
+
But $\blexersimp$ introduces simplification after the derivative,
making it difficult to align the structures of values and regular expressions.
If we change the form of property \ref{eq:stepwise} to
@@ -661,7 +771,7 @@
-\section{Why Lemma \ref{retrieveStepwise}'s Requirement is too Strong}
+\subsection{Why Lemma \ref{retrieveStepwise}'s Requirement is too Strong}
%From this chapter we start with the main contribution of this thesis, which
@@ -796,9 +906,6 @@
It does not require $v_i$ to be a POSIX value
-{\color{red} \rule{\linewidth}{0.5mm}}
-New content ends
-{\color{red} \rule{\linewidth}{0.5mm}}
@@ -825,7 +932,6 @@
%----------------------------------------------------------------------------------------
% SECTION rewrite relation
%----------------------------------------------------------------------------------------
-\section{Correctness of $\blexersimp$}
We first introduce the rewriting relation \emph{rrewrite}
($\rrewrite$) between two regular expressions,
which stands for an atomic