--- a/ChengsongTanPhdThesis/Chapters/Bitcoded2.tex Fri Jul 07 20:03:05 2023 +0100
+++ b/ChengsongTanPhdThesis/Chapters/Bitcoded2.tex Sat Jul 08 01:36:08 2023 +0100
@@ -8,12 +8,8 @@
%simplifications and therefore introduce our version of the bitcoded algorithm and
%its correctness proof in
%Chapter 3\ref{Chapter3}.
-{\color{red} \rule{\linewidth}{0.5mm}}
-New content starts.
-{\color{red} \rule{\linewidth}{0.5mm}}
-\marginpar{\em Added a completely new overview section, highlighting the contributions.}
-
\section{Overview}
+\marginpar{\em Added a completely new \\overview section, \\highlighting contributions.}
This chapter
is the point from which novel contributions of this PhD project are introduced
@@ -27,7 +23,7 @@
%are about to describe.
The fundamental reason is we cannot extend the correctness proof of theorem 4
because lemma 13 does not hold anymore when simplifications are involved.
-\marginpar{\em rephrased things so they make better sense.}
+\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
%new framework for the proof of $\blexersimp$, which involves
@@ -155,24 +151,40 @@
}
}
-\begin{figure}[H]
+\begin{center}
\begin{tikzpicture}[->, >=stealth', shorten >= 1pt, auto, thick]
- \node [rectangle, draw] (1) at (-7, 2) {$\ldots$};
- \node [rectangle, draw] (2) at (-4, 2) {$_{bs'}(_Za+_Saa)^*$};
- \node [rectangle, draw] (3) at (4, 2) {$_{bs'}(_Z(_Z\ONE + _S(\ONE \cdot a)))\cdot(_0a+_1aa)^*$};
- \node [rectangle, draw] (4) at (7, 2) {$\ldots$};
- \node [rectangle, draw] (5) at (-7, -2) {$\ldots$};
- \node [rectangle, draw] (6) at (-4, -2) {$\Stars \; [\Left (a)]$};
- \node [rectangle, draw] (7) at ( 4, -2) {$\Seq (\Alt (\Left \; \Empty)) \; \Stars \, []$};
- \node [rectangle, draw] (8) at ( 7, -2) {$\ldots$};
- \node [rectangle, draw] (9) at (-7, -6) {$\ldots$};
- \node [rectangle, draw] (10) at (-4, -6) {$\textit{bits} = \retrieve \; r_i\;v_i$};
- \node [rectangle, draw] (11) at (4, -6) {$\textit{bits} = \retrieve \; r_{i+1}\;v_{i+1}$};
- \node [rectangle, draw] (12) at (7, -6) {$\ldots$};
+ \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(_0a+_1aa)^*$};
+ \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} = \retrieve \; r_i\;v_i$};
+ \node [rectangle, draw] (11) at (4, -6) {$\textit{bits}_{i+1} = \retrieve \; r_{i+1}\;v_{i+1}$};
+ \node [rectangle] (12) at (9, -6) {$\ldots$};
\path (1) edge [] node {} (2);
+ \path (5) edge [] node {} (6);
+ \path (9) edge [] node {} (10);
+
+ \path (11) edge [] node {} (12);
+ \path (7) edge [] node {} (8);
+ \path (3) edge [] node {} (4);
+
+
\path (2) edge [] node {$\backslash a$} (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)$};
@@ -200,8 +212,8 @@
\end{tikzpicture}
- \caption{$\blexer$ with the regular expression $(aa)^*(b+c)$ and $aab$}
-\end{figure}
+ %\caption{$\blexer$ with the regular expression $(aa)^*(b+c)$ and $aab$}
+\end{center}
When simplifications are added, the inhabitation relation no longer holds,
causing the above diagram to break.