559 $\textit{if}\;\textit{bnullable}\,a_1$\\ |
559 $\textit{if}\;\textit{bnullable}\,a_1$\\ |
560 & &$\textit{then}\;_{bs}\oplus\,[(_{[]}\,(a_1\,\backslash c)\cdot\,a_2),$\\ |
560 & &$\textit{then}\;_{bs}\oplus\,[(_{[]}\,(a_1\,\backslash c)\cdot\,a_2),$\\ |
561 & &$\phantom{\textit{then},\;_{bs}\oplus\,}(\textit{fuse}\,(\textit{bmkeps}\,a_1)\,(a_2\,\backslash c))]$\\ |
561 & &$\phantom{\textit{then},\;_{bs}\oplus\,}(\textit{fuse}\,(\textit{bmkeps}\,a_1)\,(a_2\,\backslash c))]$\\ |
562 & &$\textit{else}\;_{bs}\,(a_1\,\backslash c)\cdot a_2$\\ |
562 & &$\textit{else}\;_{bs}\,(a_1\,\backslash c)\cdot a_2$\\ |
563 $(_{bs}a^*)\,\backslash c$ & $\dn$ & |
563 $(_{bs}a^*)\,\backslash c$ & $\dn$ & |
564 $_{bs}\;((\textit{fuse}\, [0] (r\,\backslash c))\cdot |
564 $_{bs}(\textit{fuse}\, [0] \; r\,\backslash c)\cdot |
565 (_{[]}r^*))$ |
565 (_{[]}r^*))$ |
566 \end{tabular} |
566 \end{tabular} |
567 \end{center} |
567 \end{center} |
568 |
568 |
569 %\end{definition} |
569 %\end{definition} |
570 \noindent |
570 \noindent |
571 For instance, when we unfold $_{bs}a^*$ into a sequence, |
571 For instance, when we do derivative of $_{bs}a^*$ with respect to c, |
572 we need to attach an additional bit $0$ to the front of $r \backslash c$ |
572 we need to unfold it into a sequence, |
|
573 and attach an additional bit $0$ to the front of $r \backslash c$ |
573 to indicate that there is one more star iteration. Also the sequence clause |
574 to indicate that there is one more star iteration. Also the sequence clause |
574 is more subtle---when $a_1$ is $\textit{bnullable}$ (here |
575 is more subtle---when $a_1$ is $\textit{bnullable}$ (here |
575 \textit{bnullable} is exactly the same as $\textit{nullable}$, except |
576 \textit{bnullable} is exactly the same as $\textit{nullable}$, except |
576 that it is for annotated regular expressions, therefore we omit the |
577 that it is for annotated regular expressions, therefore we omit the |
577 definition). Assume that $\textit{bmkeps}$ correctly extracts the bitcode for how |
578 definition). Assume that $\textit{bmkeps}$ correctly extracts the bitcode for how |
591 |
592 |
592 |
593 |
593 %\begin{definition}[\textit{bmkeps}]\mbox{} |
594 %\begin{definition}[\textit{bmkeps}]\mbox{} |
594 \begin{center} |
595 \begin{center} |
595 \begin{tabular}{lcl} |
596 \begin{tabular}{lcl} |
596 $\textit{bmkeps}\,(\textit{ONE}\;bs)$ & $\dn$ & $bs$\\ |
597 $\textit{bmkeps}\,(_{bs}\ONE)$ & $\dn$ & $bs$\\ |
597 $\textit{bmkeps}\,(\textit{ALTS}\;bs\,a::as)$ & $\dn$ & |
598 $\textit{bmkeps}\,(_{bs}\oplus a::\textit{as})$ & $\dn$ & |
598 $\textit{if}\;\textit{bnullable}\,a$\\ |
599 $\textit{if}\;\textit{bnullable}\,a$\\ |
599 & &$\textit{then}\;bs\,@\,\textit{bmkeps}\,a$\\ |
600 & &$\textit{then}\;bs\,@\,\textit{bmkeps}\,a$\\ |
600 & &$\textit{else}\;bs\,@\,\textit{bmkeps}\,(\textit{ALTS}\;bs\,as)$\\ |
601 & &$\textit{else}\;bs\,@\,\textit{bmkeps}\,(_{bs}\textit{as})$\\ |
601 $\textit{bmkeps}\,(\textit{SEQ}\;bs\,a_1\,a_2)$ & $\dn$ & |
602 $\textit{bmkeps}\,(_{bs} a_1 \cdota_2)$ & $\dn$ & |
602 $bs \,@\,\textit{bmkeps}\,a_1\,@\, \textit{bmkeps}\,a_2$\\ |
603 $bs \,@\,\textit{bmkeps}\,a_1\,@\, \textit{bmkeps}\,a_2$\\ |
603 $\textit{bmkeps}\,(\textit{STAR}\;bs\,a)$ & $\dn$ & |
604 $\textit{bmkeps}\,(_{bs}a^*)$ & $\dn$ & |
604 $bs \,@\, [\S]$ |
605 $bs \,@\, [1]$ |
605 \end{tabular} |
606 \end{tabular} |
606 \end{center} |
607 \end{center} |
607 %\end{definition} |
608 %\end{definition} |
608 |
609 |
609 \noindent |
610 \noindent |