1 % Chapter Template |
1 % Chapter Template |
2 |
2 |
3 \chapter{Common Identities In Simplification-Related Functions} % Main chapter title |
3 % Main chapter title |
4 |
4 |
5 \label{ChapterX} % Change X to a consecutive number; for referencing this chapter elsewhere, use \ref{ChapterX} |
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 |
6 |
11 |
7 |
12 |
8 |
13 |
9 %---------------------------------------------------------------------------------------- |
14 %---------------------------------------------------------------------------------------- |
10 % SECTION 1 |
15 % SECTION common identities |
11 %---------------------------------------------------------------------------------------- |
16 %---------------------------------------------------------------------------------------- |
|
17 \section{Common Identities In Simplification-Related Functions} |
|
18 Need to prove these before starting on the big correctness proof. |
12 |
19 |
13 \section{Idempotency of $\simp$} |
20 %----------------------------------- |
|
21 % SUBSECTION |
|
22 %----------------------------------- |
|
23 \subsection{Idempotency of $\simp$} |
14 |
24 |
15 \begin{equation} |
25 \begin{equation} |
16 \simp \;r = \simp\; \simp \; r |
26 \simp \;r = \simp\; \simp \; r |
17 \end{equation} |
27 \end{equation} |
18 This property means we do not have to repeatedly |
28 This property means we do not have to repeatedly |
21 It will also be useful in future proofs where properties such as |
31 It will also be useful in future proofs where properties such as |
22 closed forms are needed. |
32 closed forms are needed. |
23 The proof is by structural induction on $r$. |
33 The proof is by structural induction on $r$. |
24 |
34 |
25 %----------------------------------- |
35 %----------------------------------- |
26 % SUBSECTION 1 |
36 % SUBSECTION |
27 %----------------------------------- |
37 %----------------------------------- |
28 \subsection{Syntactic Equivalence Under $\simp$} |
38 \subsection{Syntactic Equivalence Under $\simp$} |
29 We prove that minor differences can be annhilated |
39 We prove that minor differences can be annhilated |
30 by $\simp$. |
40 by $\simp$. |
31 For example, |
41 For example, |
33 $\simp \;(\simpALTs\; (\map \;(\_\backslash \; x)\; (\distinct \; \mathit{rs}\; \phi))) = |
43 $\simp \;(\simpALTs\; (\map \;(\_\backslash \; x)\; (\distinct \; \mathit{rs}\; \phi))) = |
34 \simp \;(\simpALTs \;(\distinct \;(\map \;(\_ \backslash\; x) \; \mathit{rs}) \; \phi))$ |
44 \simp \;(\simpALTs \;(\distinct \;(\map \;(\_ \backslash\; x) \; \mathit{rs}) \; \phi))$ |
35 \end{center} |
45 \end{center} |
36 |
46 |
37 |
47 |
38 %----------------------------------- |
|
39 % SUBSECTION 2 |
|
40 %----------------------------------- |
|
41 |
48 |
42 \subsection{Subsection 2} |
49 |
43 Morbi rutrum odio eget arcu adipiscing sodales. Aenean et purus a est pulvinar pellentesque. Cras in elit neque, quis varius elit. Phasellus fringilla, nibh eu tempus venenatis, dolor elit posuere quam, quis adipiscing urna leo nec orci. Sed nec nulla auctor odio aliquet consequat. Ut nec nulla in ante ullamcorper aliquam at sed dolor. Phasellus fermentum magna in augue gravida cursus. Cras sed pretium lorem. Pellentesque eget ornare odio. Proin accumsan, massa viverra cursus pharetra, ipsum nisi lobortis velit, a malesuada dolor lorem eu neque. |
50 |
|
51 |
44 |
52 |
45 %---------------------------------------------------------------------------------------- |
53 %---------------------------------------------------------------------------------------- |
46 % SECTION 2 |
54 % SECTION corretness proof |
47 %---------------------------------------------------------------------------------------- |
55 %---------------------------------------------------------------------------------------- |
48 |
56 \section{Correctness of Bit-coded Algorithm with Simplification} |
49 \section{Main Section 2} |
57 The non-trivial part of proving the correctness of the algorithm with simplification |
50 |
58 compared with not having simplification is that we can no longer use the argument |
51 Sed ullamcorper quam eu nisl interdum at interdum enim egestas. Aliquam placerat justo sed lectus lobortis ut porta nisl porttitor. Vestibulum mi dolor, lacinia molestie gravida at, tempus vitae ligula. Donec eget quam sapien, in viverra eros. Donec pellentesque justo a massa fringilla non vestibulum metus vestibulum. Vestibulum in orci quis felis tempor lacinia. Vivamus ornare ultrices facilisis. Ut hendrerit volutpat vulputate. Morbi condimentum venenatis augue, id porta ipsum vulputate in. Curabitur luctus tempus justo. Vestibulum risus lectus, adipiscing nec condimentum quis, condimentum nec nisl. Aliquam dictum sagittis velit sed iaculis. Morbi tristique augue sit amet nulla pulvinar id facilisis ligula mollis. Nam elit libero, tincidunt ut aliquam at, molestie in quam. Aenean rhoncus vehicula hendrerit. |
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)) |