1 % Chapter Template

     2 

     3 % Main chapter title

     4 

     5 \label{Chapter3} % Change X to a consecutive number; for referencing this chapter elsewhere, use \ref{ChapterX}

     6 %Then we illustrate how the algorithm without bitcodes falls short for such aggressive 

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

     8 %its correctness proof in 

     9 %Chapter 3\ref{Chapter3}. 

    10 

    11 

    12 

    13 

    14 %----------------------------------------------------------------------------------------

    15 %	SECTION common identities

    16 %----------------------------------------------------------------------------------------

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

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

    19 

    20 %-----------------------------------

    21 %	SUBSECTION 

    22 %-----------------------------------

    23 \subsection{Idempotency of $\simp$}

    24 

    25 \begin{equation}

    26 	\simp \;r = \simp\; \simp \; r 

    27 \end{equation}

    28 This property means we do not have to repeatedly

    29 apply simplification in each step, which justifies

    30 our definition of $\blexersimp$.

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

    32 closed forms are needed.

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

    34 

    35 %-----------------------------------

    36 %	SUBSECTION 

    37 %-----------------------------------

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

    39 We prove that minor differences can be annhilated

    40 by $\simp$.

    41 For example,

    42 \begin{center}

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

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

    45 \end{center}

    46 

    47 

    48 

    49 

    50 

    51 

    52 

    53 %----------------------------------------------------------------------------------------

    54 %	SECTION corretness proof

    55 %----------------------------------------------------------------------------------------

    56 \section{Correctness of Bit-coded Algorithm with Simplification}

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

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

    59 in \cref{flex_retrieve}.

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

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

    62 structure:

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