6 \label{Bitcoded2} % Change X to a consecutive number; for referencing this chapter elsewhere, use \ref{ChapterX} |
6 \label{Bitcoded2} % Change X to a consecutive number; for referencing this chapter elsewhere, use \ref{ChapterX} |
7 %Then we illustrate how the algorithm without bitcodes falls short for such aggressive |
7 %Then we illustrate how the algorithm without bitcodes falls short for such aggressive |
8 %simplifications and therefore introduce our version of the bitcoded algorithm and |
8 %simplifications and therefore introduce our version of the bitcoded algorithm and |
9 %its correctness proof in |
9 %its correctness proof in |
10 %Chapter 3\ref{Chapter3}. |
10 %Chapter 3\ref{Chapter3}. |
11 {\color{red} \rule{\linewidth}{0.5mm}} |
|
12 New content starts. |
|
13 {\color{red} \rule{\linewidth}{0.5mm}} |
|
14 \marginpar{\em Added a completely new overview section, highlighting the contributions.} |
|
15 |
|
16 \section{Overview} |
11 \section{Overview} |
|
12 \marginpar{\em Added a completely new \\overview section, \\highlighting contributions.} |
17 |
13 |
18 This chapter |
14 This chapter |
19 is the point from which novel contributions of this PhD project are introduced |
15 is the point from which novel contributions of this PhD project are introduced |
20 in detail. |
16 in detail. |
21 The material in the |
17 The material in the |
25 the proof of $\blexersimp$. |
21 the proof of $\blexersimp$. |
26 %material for setting the scene of the formal proof we |
22 %material for setting the scene of the formal proof we |
27 %are about to describe. |
23 %are about to describe. |
28 The fundamental reason is we cannot extend the correctness proof of theorem 4 |
24 The fundamental reason is we cannot extend the correctness proof of theorem 4 |
29 because lemma 13 does not hold anymore when simplifications are involved. |
25 because lemma 13 does not hold anymore when simplifications are involved. |
30 \marginpar{\em rephrased things so they make better sense.} |
26 \marginpar{\em rephrased things \\so why new \\proof makes sense.} |
31 %The proof details are necessary materials for this thesis |
27 %The proof details are necessary materials for this thesis |
32 %because it provides necessary context to explain why we need a |
28 %because it provides necessary context to explain why we need a |
33 %new framework for the proof of $\blexersimp$, which involves |
29 %new framework for the proof of $\blexersimp$, which involves |
34 %simplifications that cause structural changes to the regular expression. |
30 %simplifications that cause structural changes to the regular expression. |
35 %A new formal proof of the correctness of $\blexersimp$, where the |
31 %A new formal proof of the correctness of $\blexersimp$, where the |
153 edge([shift={(1.0\pgflinewidth,+0.5\pgflinewidth)}]\tikzlastnode.south west) |
149 edge([shift={(1.0\pgflinewidth,+0.5\pgflinewidth)}]\tikzlastnode.south west) |
154 } |
150 } |
155 } |
151 } |
156 } |
152 } |
157 |
153 |
158 \begin{figure}[H] |
154 \begin{center} |
159 \begin{tikzpicture}[->, >=stealth', shorten >= 1pt, auto, thick] |
155 \begin{tikzpicture}[->, >=stealth', shorten >= 1pt, auto, thick] |
160 \node [rectangle, draw] (1) at (-7, 2) {$\ldots$}; |
156 \node [rectangle ] (1) at (-7, 2) {$\ldots$}; |
161 \node [rectangle, draw] (2) at (-4, 2) {$_{bs'}(_Za+_Saa)^*$}; |
157 \node [rectangle, draw] (2) at (-4, 2) {$r_i = _{bs'}(_Za+_Saa)^*$}; |
162 \node [rectangle, draw] (3) at (4, 2) {$_{bs'}(_Z(_Z\ONE + _S(\ONE \cdot a)))\cdot(_0a+_1aa)^*$}; |
158 \node [rectangle, draw] (3) at (4, 2) {$r_{i+1} = _{bs'}(_Z(_Z\ONE + _S(\ONE \cdot a)))\cdot(_0a+_1aa)^*$}; |
163 \node [rectangle, draw] (4) at (7, 2) {$\ldots$}; |
159 \node [rectangle] (4) at (9, 2) {$\ldots$}; |
164 \node [rectangle, draw] (5) at (-7, -2) {$\ldots$}; |
160 \node [rectangle] (5) at (-7, -2) {$\ldots$}; |
165 \node [rectangle, draw] (6) at (-4, -2) {$\Stars \; [\Left (a)]$}; |
161 \node [rectangle, draw] (6) at (-4, -2) {$v_i = \Stars \; [\Left (a)]$}; |
166 \node [rectangle, draw] (7) at ( 4, -2) {$\Seq (\Alt (\Left \; \Empty)) \; \Stars \, []$}; |
162 \node [rectangle, draw] (7) at ( 4, -2) {$v_{i+1} = \Seq (\Alt (\Left \; \Empty)) \; \Stars \, []$}; |
167 \node [rectangle, draw] (8) at ( 7, -2) {$\ldots$}; |
163 \node [rectangle] (8) at ( 9, -2) {$\ldots$}; |
168 \node [rectangle, draw] (9) at (-7, -6) {$\ldots$}; |
164 \node [rectangle] (9) at (-7, -6) {$\ldots$}; |
169 \node [rectangle, draw] (10) at (-4, -6) {$\textit{bits} = \retrieve \; r_i\;v_i$}; |
165 \node [rectangle, draw] (10) at (-4, -6) {$\textit{bits}_{i} = \retrieve \; r_i\;v_i$}; |
170 \node [rectangle, draw] (11) at (4, -6) {$\textit{bits} = \retrieve \; r_{i+1}\;v_{i+1}$}; |
166 \node [rectangle, draw] (11) at (4, -6) {$\textit{bits}_{i+1} = \retrieve \; r_{i+1}\;v_{i+1}$}; |
171 \node [rectangle, draw] (12) at (7, -6) {$\ldots$}; |
167 \node [rectangle] (12) at (9, -6) {$\ldots$}; |
172 |
168 |
173 |
169 |
174 \path (1) edge [] node {} (2); |
170 \path (1) edge [] node {} (2); |
|
171 \path (5) edge [] node {} (6); |
|
172 \path (9) edge [] node {} (10); |
|
173 |
|
174 \path (11) edge [] node {} (12); |
|
175 \path (7) edge [] node {} (8); |
|
176 \path (3) edge [] node {} (4); |
|
177 |
|
178 |
175 \path (2) edge [] node {$\backslash a$} (3); |
179 \path (2) edge [] node {$\backslash a$} (3); |
|
180 \path (2) edge [dashed, <->] node {$\vdash v_i : r_i$} (6); |
|
181 \path (3) edge [dashed, <->] node {$\vdash v_{i+1} : r_{i+1}$} (7); |
|
182 %\path (6) edge [] node {$\vdash v_i : r_i$} (10); |
|
183 %\path (7) edge [dashed, <->] node {$\vdash v_i : r_i$} (11); |
|
184 |
|
185 \path (10) edge [dashed, <->] node {$=$} (11); |
|
186 |
|
187 \path (7) edge [] node {$\inj \; r_{i+1} \; a \; v_i$} (6); |
176 |
188 |
177 % \node [rectangle, draw] (r) at (-6, -1) {$(aa)^*(b+c)$}; |
189 % \node [rectangle, draw] (r) at (-6, -1) {$(aa)^*(b+c)$}; |
178 % \node [rectangle, draw] (a) at (-6, 4) {$(aa)^*(_{Z}b + _{S}c)$}; |
190 % \node [rectangle, draw] (a) at (-6, 4) {$(aa)^*(_{Z}b + _{S}c)$}; |
179 % \path (r) |
191 % \path (r) |
180 % edge [] node {$\internalise$} (a); |
192 % edge [] node {$\internalise$} (a); |