15 bitcodes in the first place. |
15 bitcodes in the first place. |
16 |
16 |
17 \section{Simplification for Annotated Regular Expressions} |
17 \section{Simplification for Annotated Regular Expressions} |
18 The first thing we notice in the fast growth of examples such as $(a^*a^*)^*$'s |
18 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 |
19 and $(a^* + (aa)^*)^*$'s derivatives is that a lot of duplicated sub-patterns |
20 are scattered around different levels: |
20 are scattered around different levels, and therefore requires |
21 |
21 de-duplication at different levels: |
22 \begin{center} |
22 \begin{center} |
23 $(a^*a^*)^* \rightarrow (a^*a^* + a^*)\cdot(a^*a^*)^*$\\ |
23 $(a^*a^*)^* \rightarrow (a^*a^* + a^*)\cdot(a^*a^*)^* \rightarrow $\\ |
24 $((a^*a^* + a^*) + a^*)\cdot(a^*a^*)^* + (a^*a^* + a^*)\cdot(a^*a^*)^*$ |
24 $((a^*a^* + a^*) + a^*)\cdot(a^*a^*)^* + (a^*a^* + a^*)\cdot(a^*a^*)^*$ |
25 \end{center} |
25 \end{center} |
|
26 \noindent |
|
27 As we have already mentioned in \ref{eqn:growth2}, |
|
28 a simple-minded simplification function cannot simplify |
|
29 $((a^*a^* + a^*) + a^*)\cdot(a^*a^*)^* + (a^*a^* + a^*)\cdot(a^*a^*)^*$ |
|
30 any further. |
|
31 we would expect a better simplification function to work in the |
|
32 following way: |
|
33 \begin{gather*} |
|
34 ((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}.\\ |
|
36 \bigg\downarrow \\ |
|
37 (a^*a^* + a^* |
|
38 \color{gray} + a^* \color{black})\cdot(a^*a^*)^* + |
|
39 \underbrace{(a^*a^* + a^*)\cdot(a^*a^*)^*}_\text{further simp removes this} \\ |
|
40 \bigg\downarrow \\ |
|
41 (a^*a^* + a^* |
|
42 )\cdot(a^*a^*)^* |
|
43 \color{gray} + (a^*a^* + a^*) \cdot(a^*a^*)^* |
|
44 \end{gather*} |
|
45 \noindent |
|
46 This motivating example came from testing Sulzmann and Lu's |
|
47 algorithm: their simplification does |
|
48 not work! |
|
49 We quote their $\textit{simp}$ function verbatim here: |
|
50 \begin{center} |
|
51 \begin{tabular}{lcl} |
|
52 $\simp\; _{bs}(_{bs'}\ONE \cdot r)$ & $\dn$ & |
|
53 $\textit{if} \; (\textit{zeroable} \; r)\; \textit{then} \;\; \ZERO$\\ |
|
54 & &$\textit{else}\;\; \fuse \; (bs@ bs') \; r$\\ |
|
55 $\simp\;(_{bs}r_1\cdot r_2)$ & $\dn$ & $\textit{if} |
|
56 \; (\textit{zeroable} \; r_1 \; \textit{or} \; \textit{zeroable}\; r_2)\; |
|
57 \textit{then} \;\; \ZERO$\\ |
|
58 & & $\textit{else}\;\;_{bs}((\simp\;r_1)\cdot |
|
59 (\simp\; r_2))$\\ |
|
60 $\simp \; _{bs}\sum []$ & $\dn$ & $\ZERO$\\ |
|
61 $\simp \; _{bs}\sum ((_{bs'}\sum rs_1) :: rs_2)$ & $\dn$ & |
|
62 $_{bs}\sum ((\map \; (\fuse \; bs')\; rs_1) @ rs_2)$\\ |
|
63 $\simp \; _{bs}\sum[r]$ & $\dn$ & $\fuse \; bs \; (\simp \; r)$\\ |
|
64 $\simp \; _{bs}\sum(r::rs)$ & $\dn$ & $_{bs}\sum |
|
65 (\nub \; (\filter \; (\not \circ \zeroable)\;((\simp \; r) :: \map \; \simp \; rs)))$\\ |
|
66 |
|
67 \end{tabular} |
|
68 \end{center} |
|
69 \noindent |
|
70 the $\textit{zeroable}$ predicate |
|
71 which tests whether the regular expression |
|
72 is equivalent to $\ZERO$, |
|
73 is defined as: |
|
74 \begin{center} |
|
75 \begin{tabular}{lcl} |
|
76 $\zeroable \; _{bs}\sum (r::rs)$ & $\dn$ & $\zeroable \; r\;\; \land \;\; |
|
77 \zeroable \;_{[]}\sum\;rs $\\ |
|
78 $\zeroable\;_{bs}(r_1 \cdot r_2)$ & $\dn$ & $\zeroable\; r_1 \;\; \lor \;\; \zeroable \; r_2$\\ |
|
79 $\zeroable\;_{bs}r^*$ & $\dn$ & $\textit{false}$ \\ |
|
80 $\zeroable\;_{bs}c$ & $\dn$ & $\textit{false}$\\ |
|
81 $\zeroable\;_{bs}\ONE$ & $\dn$ & $\textit{false}$\\ |
|
82 $\zeroable\;_{bs}\ZERO$ & $\dn$ & $\textit{true}$ |
|
83 \end{tabular} |
|
84 \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 %\] |
26 \noindent |
95 \noindent |
27 Despite that we have already implemented the simple-minded simplifications |
96 Despite that we have already implemented the simple-minded simplifications |
28 such as throwing away useless $\ONE$s and $\ZERO$s. |
97 such as throwing away useless $\ONE$s and $\ZERO$s. |
29 The simplification rule $r + r \rightarrow $ cannot make a difference either |
98 The simplification rule $r + r \rightarrow $ cannot make a difference either |
30 since it only removes duplicates on the same level, not something like |
99 since it only removes duplicates on the same level, not something like |