713 $\textit{pder} \; c \; r_1+r_2$ & $\dn$ & $pder \; c \; r_1 \cup pder \; c \; r_2$ \\ |
713 $\textit{pder} \; c \; r_1+r_2$ & $\dn$ & $pder \; c \; r_1 \cup pder \; c \; r_2$ \\ |
714 $\textit{pder} \; c \; r_1 \cdot r_2$ & $\dn$ & $\textit{if} \; nullable \; r_1 \; \{ r \cdot r_2 \mid r \in pder \; c \; r_1 \} \cup pder \; c \; r_2 \; \textit{else} \; \{ r \cdot r_2 \mid r \in pder \; c \; r_1 \} $ \\ |
714 $\textit{pder} \; c \; r_1 \cdot r_2$ & $\dn$ & $\textit{if} \; nullable \; r_1 \; \{ r \cdot r_2 \mid r \in pder \; c \; r_1 \} \cup pder \; c \; r_2 \; \textit{else} \; \{ r \cdot r_2 \mid r \in pder \; c \; r_1 \} $ \\ |
715 $\textit{pder} \; c \; r^*$ & $\dn$ & $ \{ r' \cdot r^* \mid r' \in pder \; c \; r \} $ \\ |
715 $\textit{pder} \; c \; r^*$ & $\dn$ & $ \{ r' \cdot r^* \mid r' \in pder \; c \; r \} $ \\ |
716 \end{tabular} |
716 \end{tabular} |
717 \end{center} |
717 \end{center} |
718 it is essentially a set of regular expressions that come from the sub-structure of the original regular expression. |
718 A partial derivative of a regular expression $r$ is essentially a set of regular expressions that are either $r$'s children expressions or a concatenation of them. |
719 Antimirov has proved a nice size bound of the size of partial derivatives. Roughly speaking the size will not exceed the fourth power of the number of nodes in that regular expression. Interestingly, we observed from experiment that after the simplification step, our regular expression has the same size or is smaller than the partial derivatives. This allows us to prove a tight bound on the size of regular expression during the running time of the algorithm if we can establish the connection between our simplification rules and partial derivatives. |
719 Antimirov has proved a nice size bound of the size of partial derivatives. Roughly speaking the size will not exceed the fourth power of the number of nodes in that regular expression. Interestingly, we observed from experiment that after the simplification step, our regular expression has the same size or is smaller than the partial derivatives. This allows us to prove a tight bound on the size of regular expression during the running time of the algorithm if we can establish the connection between our simplification rules and partial derivatives. |
720 |
720 |
721 %We believe, and have generated test |
721 %We believe, and have generated test |
722 %data, that a similar bound can be obtained for the derivatives in |
722 %data, that a similar bound can be obtained for the derivatives in |
723 %Sulzmann and Lu's algorithm. Let us give some details about this next. |
723 %Sulzmann and Lu's algorithm. Let us give some details about this next. |
724 |
724 |
725 Bit-codes look like this: |
725 Bit-codes look like this: |
726 \[ b ::= S \mid Z \; \;\; |
726 \begin{center} |
|
727 $b ::= S \mid Z \; \;\; |
727 bs ::= [] \mid b:bs |
728 bs ::= [] \mid b:bs |
728 \] |
729 $ |
729 They are just a string of bits, the names "S" and "Z" here are kind of arbitrary, we can use 0 and 1 or binary symbol to substitute them. They are a compact form of parse trees. |
730 \end{center} |
|
731 They are just a string of bits, the names $S$ and $Z$ here are quite arbitrary, we can use 0 and 1 or any other set of binary symbols to substitute them. They are a compact form of parse trees. |
730 Here is how values and bit-codes are related: |
732 Here is how values and bit-codes are related: |
731 Bitcodes are essentially incomplete values. |
733 Bitcodes are essentially incomplete values. |
732 This can be straightforwardly seen in the following transformation: |
734 This can be straightforwardly seen in the following transformation: |
733 \begin{center} |
735 \begin{center} |
734 \begin{tabular}{lcl} |
736 \begin{tabular}{lcl} |