1 % Chapter Template

     2 

     3 % Main chapter title

     4 \chapter{Correctness of Bit-coded Algorithm with Simplification}

     5 

     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 

     8 %simplifications and therefore introduce our version of the bitcoded algorithm and 

     9 %its correctness proof in 

    10 %Chapter 3\ref{Chapter3}. 

    11 

    12 

    13 

    14 

    15 %----------------------------------------------------------------------------------------

    16 %	SECTION common identities

    17 %----------------------------------------------------------------------------------------

    18 \section{Common Identities In Simplification-Related Functions} 

    19 Need to prove these before starting on the big correctness proof.

    20 

    21 %-----------------------------------

    22 %	SUBSECTION 

    23 %-----------------------------------

    24 \subsection{Idempotency of $\simp$}

    25 

    26 \begin{equation}

    27 	\simp \;r = \simp\; \simp \; r 

    28 \end{equation}

    29 This property means we do not have to repeatedly

    30 apply simplification in each step, which justifies

    31 our definition of $\blexersimp$.

    32 It will also be useful in future proofs where properties such as 

    33 closed forms are needed.

    34 The proof is by structural induction on $r$.

    35 

    36 %-----------------------------------

    37 %	SUBSECTION 

    38 %-----------------------------------

    39 \subsection{Syntactic Equivalence Under $\simp$}

    40 We prove that minor differences can be annhilated

    41 by $\simp$.

    42 For example,

    43 \begin{center}

    44 $\simp \;(\simpALTs\; (\map \;(\_\backslash \; x)\; (\distinct \; \mathit{rs}\; \phi))) = 

    45  \simp \;(\simpALTs \;(\distinct \;(\map \;(\_ \backslash\; x) \; \mathit{rs}) \; \phi))$

    46 \end{center}

    47 

    48 

    49 

    50 

    51 

    52 

    53 

    54 %----------------------------------------------------------------------------------------

    55 %	SECTION corretness proof

    56 %----------------------------------------------------------------------------------------

    57 \section{Proof Technique of Correctness of Bit-coded Algorithm with Simplification}

    58 The non-trivial part of proving the correctness of the algorithm with simplification

    59 compared with not having simplification is that we can no longer use the argument 

    60 in \cref{flex_retrieve}.

    61 The function \retrieve needs the structure of the annotated regular expression to 

    62 agree with the structure of the value, but simplification will always mess with the 

    63 structure:

    64 %TODO: after simp does not agree with each other: (a + 0) --> a v.s. Left(Char(a))