# HG changeset patch
# User Chengsong
# Date 1687824576 -3600
# Node ID deb35fd780fe98c2468707460f6dd13fb1bf15f4
# Parent  a365d1364640a6dbc7eeb55cfa14286e9347fe8c
more

diff -r a365d1364640 -r deb35fd780fe ChengsongTanPhdThesis/Chapters/Bitcoded2.tex
--- 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.
diff -r a365d1364640 -r deb35fd780fe ChengsongTanPhdThesis/Chapters/Inj.tex
--- 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$,