--- a/ninems/ninems.tex Thu Jul 04 23:39:49 2019 +0100
+++ b/ninems/ninems.tex Fri Jul 05 16:54:25 2019 +0100
@@ -549,14 +549,17 @@
Antimirov defined the "partial derivatives" of regular expressions to be this:
%TODO definition of partial derivatives
-\[ pder c 0 = emtpy set\]
-\[pder c 1 = emptry set\]
-\[pder c c = if c is equal to d then set containing lambda only else empty set\]
-\[pder c r_1+r_2 = pder c r_1 \cup pder c r_2\]
-\[pder c r_1 \cdot r_2 = if r_1 nullable then set of r \cdot r_2' where r is in pder c r_1 \cup pder c r_2\]
-\[else set of r \cdot r_2' where r is in pder c r_1\]
-\[pder c r^* = set of r \cdot r^* where r \in pder c r\]
-
+\begin{center}
+\begin{tabular}{lcl}
+ $\textit{pder} \; c \; 0$ & $\dn$ & $\emptyset$\\
+ $\textit{pder} \; c \; 1$ & $\dn$ & $\emptyset$ \\
+ $\textit{pder} \; c \; d$ & $\dn$ & $\textit{if} \; c \,=\, d \; \{ 1 \} \; \textit{else} \; \emptyset$ \\
+ $\textit{pder} \; c \; r_1+r_2$ & $\dn$ & $pder \; c \; r_1 \cup pder \; c \; r_2$ \\
+ $\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 \} $ \\
+ $\textit{pder} \; c \; r^*$ & $\dn$ & $ \{ r' \cdot r^* \mid r' \in pder \; c \; r \} $ \\
+ \end{tabular}
+ \end{center}
+
it is essentially a set of regular expressions that come from the sub-structure of the original regular expression.
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.
@@ -755,19 +758,24 @@
alternative contributes to the calculation of a POSIX value. All
subsequent copies can be pruned from the regular expression.
-A psuedocode version of our algorithm is given below:\\
-\[simp r \dn r if r = ONE bs or CHAR bs c or STAR bs r
-simp SEQ bs r_1 r_2 \dn \\
-case (simp(r_1), simp(r_2) ) of (0, _) => 0
-(_,0) => 0
-(1, r) => fuse bs r
-(r,1) => fuse bs r
-(r_1, r_2) => SEQ bs r_1 r_2
-simp ALT bs rs = distinct(flatten( map simp rs)) match
-case Nil => ZERO
-case r::Nil => fuse bs r
-case rs => ALT bs rs
-\]
+A recursive definition of simplification function that looks similar to scala code is given below:\\
+\begin{center}
+ \begin{tabular}{@{}lcl@{}}
+ $\textit{simp} \; a$ & $\dn$ & $\textit{a} \; \textit{if} \; a = (\textit{ONE} \; bs) \; or\; (\textit{CHAR} \, bs \; c) \; or\; (\textit{STAR}\; bs\; a_1)$\\
+
+ $\textit{simp} \; \textit{SEQ}\;bs\,a_1\,a_2$ & $\dn$ & $ (\textit{simp} \; a_1, \textit{simp} \; a_2) \; \textit{match} $ \\
+ &&$\textit{case} \; (0, \_) \Rightarrow 0$ \\
+ &&$ \textit{case} \; (\_, 0) \Rightarrow 0$ \\
+ &&$ \textit{case} \; (1, a_2') \Rightarrow \textit{fuse} \; bs \; a_2'$ \\
+ &&$ \textit{case} \; (a_1', 1) \Rightarrow \textit{fuse} \; bs \; a_1'$ \\
+ &&$ \textit{case} \; (a_1', a_2') \Rightarrow \textit{SEQ} \; bs \; a_1' \; a_2'$ \\
+
+ $\textit{simp} \; \textit{ALT}\;bs\,as$ & $\dn$ & $\textit{ distinct}( \textit{flatten} ( \textit{map simp as})) \; \textit{match} $ \\
+ &&$\textit{case} \; [] \Rightarrow 0$ \\
+ &&$ \textit{case} \; a :: [] \Rightarrow \textit{fuse bs a}$ \\
+ &&$ \textit{case} \; as' \Rightarrow \textit{ALT bs as'}$
+\end{tabular}
+\end{center}
The simplification does a pattern matching on the regular expression. When it detected that
the regular expression is an alternative or sequence, it will try to simplify its children regular expressions