9 %its correctness proof in |
9 %its correctness proof in |
10 %Chapter 3\ref{Chapter3}. |
10 %Chapter 3\ref{Chapter3}. |
11 |
11 |
12 |
12 |
13 |
13 |
14 Now we introduce the simplifications, which is why we introduce the |
14 In this chapter we introduce the simplifications |
15 bitcodes in the first place. |
15 on annotated regular expressions that can be applied to |
|
16 each intermediate derivative result. This allows |
|
17 us to make $\blexer$ much more efficient. |
|
18 We contrast this simplification function |
|
19 with Sulzmann and Lu's original |
|
20 simplifications, indicating the simplicity of our algorithm and |
|
21 improvements we made, demostrating |
|
22 the usefulness and reliability of formal proofs on algorithms. |
|
23 These ``aggressive'' simplifications would not be possible in the injection-based |
|
24 lexing we introduced in chapter \ref{Inj}. |
|
25 We then go on to prove the correctness with the improved version of |
|
26 $\blexer$, called $\blexersimp$, by establishing |
|
27 $\blexer \; r \; s= \blexersimp \; r \; s$ using a term rewriting system. |
16 |
28 |
17 \section{Simplification for Annotated Regular Expressions} |
29 \section{Simplification for Annotated Regular Expressions} |
18 The first thing we notice in the fast growth of examples such as $(a^*a^*)^*$'s |
30 The first thing we notice in the fast growth of examples such as $(a^*a^*)^*$'s |
19 and $(a^* + (aa)^*)^*$'s derivatives is that a lot of duplicated sub-patterns |
31 and $(a^* + (aa)^*)^*$'s derivatives is that a lot of duplicated sub-patterns |
20 are scattered around different levels, and therefore requires |
32 are scattered around different levels, and therefore requires |
21 de-duplication at different levels: |
33 de-duplication at different levels: |
22 \begin{center} |
34 \begin{center} |
23 $(a^*a^*)^* \rightarrow (a^*a^* + a^*)\cdot(a^*a^*)^* \rightarrow $\\ |
35 $(a^*a^*)^* \rightarrow (a^*a^* + a^*)\cdot(a^*a^*)^* \rightarrow $\\ |
24 $((a^*a^* + a^*) + a^*)\cdot(a^*a^*)^* + (a^*a^* + a^*)\cdot(a^*a^*)^*$ |
36 $((a^*a^* + a^*) + a^*)\cdot(a^*a^*)^* + (a^*a^* + a^*)\cdot(a^*a^*)^* \rightarrow \ldots$ |
25 \end{center} |
37 \end{center} |
26 \noindent |
38 \noindent |
27 As we have already mentioned in \ref{eqn:growth2}, |
39 As we have already mentioned in \ref{eqn:growth2}, |
28 a simple-minded simplification function cannot simplify |
40 a simple-minded simplification function cannot simplify |
|
41 \begin{center} |
29 $((a^*a^* + a^*) + a^*)\cdot(a^*a^*)^* + (a^*a^* + a^*)\cdot(a^*a^*)^*$ |
42 $((a^*a^* + a^*) + a^*)\cdot(a^*a^*)^* + (a^*a^* + a^*)\cdot(a^*a^*)^*$ |
30 any further. |
43 \end{center} |
31 we would expect a better simplification function to work in the |
44 any further, one would expect a better simplification function to work in the |
32 following way: |
45 following way: |
33 \begin{gather*} |
46 \begin{gather*} |
34 ((a^*a^* + \underbrace{a^*}_\text{A})+\underbrace{a^*}_\text{duplicate of A})\cdot(a^*a^*)^* + |
47 ((a^*a^* + \underbrace{a^*}_\text{A})+\underbrace{a^*}_\text{duplicate of A})\cdot(a^*a^*)^* + |
35 \underbrace{(a^*a^* + a^*)\cdot(a^*a^*)^*}_\text{further simp removes this}.\\ |
48 \underbrace{(a^*a^* + a^*)\cdot(a^*a^*)^*}_\text{further simp removes this}.\\ |
36 \bigg\downarrow \\ |
49 \bigg\downarrow \\ |
80 $\zeroable\;_{bs}c$ & $\dn$ & $\textit{false}$\\ |
96 $\zeroable\;_{bs}c$ & $\dn$ & $\textit{false}$\\ |
81 $\zeroable\;_{bs}\ONE$ & $\dn$ & $\textit{false}$\\ |
97 $\zeroable\;_{bs}\ONE$ & $\dn$ & $\textit{false}$\\ |
82 $\zeroable\;_{bs}\ZERO$ & $\dn$ & $\textit{true}$ |
98 $\zeroable\;_{bs}\ZERO$ & $\dn$ & $\textit{true}$ |
83 \end{tabular} |
99 \end{tabular} |
84 \end{center} |
100 \end{center} |
85 %\[ |
|
86 %\begin{aligned} |
|
87 %&\textit{isPhi} \left(b s @ r i^{*}\right)=\text { False } \\ |
|
88 %&\textit{isPhi}\left(b s @ r i_{1} r i_{2}\right)=\textit{isPhi} r i_{1} \vee \textit{isPhi} r i_{2} \\ |
|
89 %&\textit{isPhi} \left(b s @ r i_{1} \oplus r i_{2}\right)=\textit{isPhi} r i_{1} \wedge \textit{isPhi} r i_{2} \\ |
|
90 %&\textit{isPhi}(b s @ l)= False \\ |
|
91 %&\textit{isPhi}(b s @ \epsilon)= False \\ |
|
92 %&\textit{isPhi} \; \ZERO = True |
|
93 %\end{aligned} |
|
94 %\] |
|
95 \noindent |
101 \noindent |
96 Despite that we have already implemented the simple-minded simplifications |
102 Despite that we have already implemented the simple-minded simplifications |
97 such as throwing away useless $\ONE$s and $\ZERO$s. |
103 such as throwing away useless $\ONE$s and $\ZERO$s. |
98 The simplification rule $r + r \rightarrow $ cannot make a difference either |
104 The simplification rule $r + r \rightarrow $ cannot make a difference either |
99 since it only removes duplicates on the same level, not something like |
105 since it only removes duplicates on the same level, not something like |