--- a/ChengsongTanPhdThesis/Chapters/Bitcoded2.tex Wed Jun 21 22:43:04 2023 +0100
+++ b/ChengsongTanPhdThesis/Chapters/Bitcoded2.tex Tue Jun 27 01:09:36 2023 +0100
@@ -81,25 +81,58 @@
in the inhabitation relation, something different than $v_{r}^{c}$ needs to be plugged
in for the above statement to hold.
Ausaf et al. \cite{AusafUrbanDyckhoff2016}
-made some initial attempts on the un-annotated lexer (to be continued)
+made some initial attempts with this idea, see \cite{FahadThesis}
+for details.
+The other route is to dispose of lemma \ref{retrieveStepwise},
+and prove a slightly weakened inductive invariant instead.
+We adopt this approach in this thesis.
-
+We first introduce why the inductive invariant in $\blexer$'s proof
+is too strong, and suggest a few possible fixes, which leads to
+our proof which we believe was the most natural and effective method.
-From this chapter we start with the main contribution of this thesis, which
+\section{Why Lemma \ref{retrieveStepwise}'s Requirement is too Strong}
-o
-In particular, the $\blexer$ proof relies on a lockstep POSIX
+%From this chapter we start with the main contribution of this thesis, which
+
+The $\blexer$ proof relies on a lockstep POSIX
correspondence between the lexical value and the
regular expression in each derivative and injection.
+If we zoom into the diagram \ref{fig:Inj} and look specifically at
+the pairs $v_i, r_i$ and $v_{i+1} r_{i+1}$, and the invariant of these
+pairs, we get the following correspondence
+\begin{tikzpicture}[
+ -{Stealth[scale=1.5]}, % arrow style
+ shorten >=1pt, % distance from node to arrow head
+ node distance=2cm,
+ font=\sffamily
+]
-which is essential for getting an understanding this thesis
-in chapter \ref{Bitcoded1}, which is necessary for understanding why
-the proof
+\matrix (M) [matrix of nodes, nodes in empty cells, column sep=2cm, row sep=2cm,
+nodes={execute at begin node=\phantom}]
+{
+ 1 & {$b_{s}(a_{0}+a_{1a})^{*}$} & 3 & 4\\
+ 5 & 6 & 7 & 8\\
+ 9 & 10 & 11 & 12\\
+};
+
+\foreach \i in {2,...,3} % go through each column
+ \draw[dotted] (M-1-\i) -- (M-2-\i) -- (M-3-\i);
-In this chapter,
+\foreach \i in {1,2} % go through each row
+ \draw[->] (M-\i-2.east) -- (M-\i-3.west);
+\end{tikzpicture}
+
+%
+%
+%which is essential for getting an understanding this thesis
+%in chapter \ref{Bitcoded1}, which is necessary for understanding why
+%the proof
+%
+%In this chapter,
%We contrast our simplification function
%with Sulzmann and Lu's, indicating the simplicity of our algorithm.
--- a/ChengsongTanPhdThesis/Chapters/Inj.tex Wed Jun 21 22:43:04 2023 +0100
+++ b/ChengsongTanPhdThesis/Chapters/Inj.tex Tue Jun 27 01:09:36 2023 +0100
@@ -1346,83 +1346,6 @@
\]
\end{property}
\noindent
-Pictorially, this looks as follows:\\
-\vspace{3mm}
-
-\parskip \baselineskip
-\def\myupbracefill#1{\rotatebox{90}{\stretchto{\{}{#1}}}
-\def\rlwd{.5pt}
-\newcommand\notate[3]{%
- \unskip\def\useanchorwidth{T}%
- \setbox0=\hbox{#1}%
- \def\stackalignment{c}\stackunder[-6pt]{%
- \def\stackalignment{c}\stackunder[-1.5pt]{%
- \stackunder[-2pt]{\strut #1}{\myupbracefill{\wd0}}}{%
- \rule{\rlwd}{#2\baselineskip}}}{%
- \strut\kern8pt$\hookrightarrow$\rlap{ \footnotesize#3}}\ignorespaces%
-}
-\Longstack{
- \notate{$r$}{1}{$L \; r = \{\ldots, \;c::s_1,
-\;\ldots\}$}
-}
-\Longstack{
- $\stackrel{\backslash c}{\xrightarrow{\hspace*{8cm}}}$
-}
-\Longstack{
- \notate{$r\backslash c$}{1}{$L \; (r\backslash c)=
- \{\ldots,\;s_1,\;\ldots\}$}
-}\\
-\vspace{ 3mm }
-
-The derivatives on regular expression can again be
-generalised to strings.
-One could compute $r_{start} \backslash s$ and test membership of $s$
-in $L \; r_{start}$ by checking
-whether the empty string is in the language of
-$r_{end}$ (that is $r_{start}\backslash s$).\\
-
-\vspace{2mm}
-\Longstack{
- \notate{$r_{start}$}{4}{
- \Longstack{$L \; r_{start} = \{\ldots, \;$
- \notate{$s$}{1}{$c_1::s_1$}
- $, \ldots\} $
- }
- }
-}
-\Longstack{
- $\stackrel{\backslash c_1}{ \xrightarrow{\hspace*{1.8cm}} }$
-}
-\Longstack{
- \notate{$r_1$}{3}{
- $r_1 = r_{start}\backslash c_1$,
- $L \; r_1 = $
- \Longstack{
- $\{ \ldots,\;$ \notate{$s_1$}{1}{$c_2::s_2$}
- $,\; \ldots \}$
- }
-}
-}
-\Longstack{
- $\stackrel{\backslash c_2}{\xrightarrow{\hspace*{1.8cm}}}$
-}
-\Longstack{
- $r_2$
-}
-\Longstack{
- $ \xdashrightarrow{\hspace*{0.3cm} \backslash c_3 \ldots \ldots \ldots \hspace*{0.3cm}} $
-}
-\Longstack{
- \notate{$r_{end}$}{1}{
- $L \; r_{end} = \{\ldots, \; [], \ldots\}$}
-}
-
-
-We have the property that
-\begin{property}
- $s \in L \; r_{start} \iff [] \in L \; r_{end}$
-\end{property}
-\noindent
Next, we give the recursive definition of derivative on
regular expressions so that it satisfies the properties above.
%The derivative function, written $r\backslash c$,