492 derivative operations on the annotated regular expressions. This |
492 derivative operations on the annotated regular expressions. This |
493 derivative operation is the same as what we had previously for the |
493 derivative operation is the same as what we had previously for the |
494 basic regular expressions, except that we beed to take care of |
494 basic regular expressions, except that we beed to take care of |
495 the bitcodes: |
495 the bitcodes: |
496 |
496 |
|
497 |
|
498 \iffalse |
497 %\begin{definition}{bder} |
499 %\begin{definition}{bder} |
498 \begin{center} |
500 \begin{center} |
499 \begin{tabular}{@{}lcl@{}} |
501 \begin{tabular}{@{}lcl@{}} |
500 $(\textit{ZERO})\,\backslash c$ & $\dn$ & $\textit{ZERO}$\\ |
502 $(\textit{ZERO})\,\backslash c$ & $\dn$ & $\textit{ZERO}$\\ |
501 $(\textit{ONE}\;bs)\,\backslash c$ & $\dn$ & $\textit{ZERO}$\\ |
503 $(\textit{ONE}\;bs)\,\backslash c$ & $\dn$ & $\textit{ZERO}$\\ |
514 (\textit{STAR}\,[]\,r)$ |
516 (\textit{STAR}\,[]\,r)$ |
515 \end{tabular} |
517 \end{tabular} |
516 \end{center} |
518 \end{center} |
517 %\end{definition} |
519 %\end{definition} |
518 |
520 |
|
521 \begin{center} |
|
522 \begin{tabular}{@{}lcl@{}} |
|
523 $(\textit{ZERO})\,\backslash c$ & $\dn$ & $\textit{ZERO}$\\ |
|
524 $(_{bs}\textit{ONE})\,\backslash c$ & $\dn$ & $\textit{ZERO}$\\ |
|
525 $(_{bs}\textit{CHAR}\;d)\,\backslash c$ & $\dn$ & |
|
526 $\textit{if}\;c=d\; \;\textit{then}\; |
|
527 _{bs}\textit{ONE}\;\textit{else}\;\textit{ZERO}$\\ |
|
528 $(_{bs}\textit{ALTS}\;as)\,\backslash c$ & $\dn$ & |
|
529 $_{bs}\textit{ALTS}\;(as.map(\backslash c))$\\ |
|
530 $(_{bs}\textit{SEQ}\;a_1\,a_2)\,\backslash c$ & $\dn$ & |
|
531 $\textit{if}\;\textit{bnullable}\,a_1$\\ |
|
532 & &$\textit{then}\;_{bs}\textit{ALTS}\,List((_{[]}\textit{SEQ}\,(a_1\,\backslash c)\,a_2),$\\ |
|
533 & &$\phantom{\textit{then}\;_{bs}\textit{ALTS}\,}(\textit{fuse}\,(\textit{bmkeps}\,a_1)\,(a_2\,\backslash c)))$\\ |
|
534 & &$\textit{else}\;_{bs}\textit{SEQ}\,(a_1\,\backslash c)\,a_2$\\ |
|
535 $(_{bs}\textit{STAR}\,a)\,\backslash c$ & $\dn$ & |
|
536 $_{bs}\textit{SEQ}\;(\textit{fuse}\, [\Z] (r\,\backslash c))\, |
|
537 (_{bs}\textit{STAR}\,[]\,r)$ |
|
538 \end{tabular} |
|
539 \end{center} |
|
540 %\end{definition} |
|
541 \fi |
|
542 |
|
543 \begin{center} |
|
544 \begin{tabular}{@{}lcl@{}} |
|
545 $(\ZERO)\,\backslash c$ & $\dn$ & $\ZERO$\\ |
|
546 $(_{bs}\ONE)\,\backslash c$ & $\dn$ & $\ZERO$\\ |
|
547 $(_{bs}{\bf d})\,\backslash c$ & $\dn$ & |
|
548 $\textit{if}\;c=d\; \;\textit{then}\; |
|
549 _{bs}\ONE\;\textit{else}\;\ZERO$\\ |
|
550 $(_{bs}\oplus \;as)\,\backslash c$ & $\dn$ & |
|
551 $_{bs}\oplus\;(as.map(\backslash c))$\\ |
|
552 $(_{bs}\;a_1\cdot a_2)\,\backslash c$ & $\dn$ & |
|
553 $\textit{if}\;\textit{bnullable}\,a_1$\\ |
|
554 & &$\textit{then}\;_{bs}\oplus\,[(_{[]}\,(a_1\,\backslash c)\cdot\,a_2),$\\ |
|
555 & &$\phantom{\textit{then},\;_{bs}\oplus\,}(\textit{fuse}\,(\textit{bmkeps}\,a_1)\,(a_2\,\backslash c))]$\\ |
|
556 & &$\textit{else}\;_{bs}\,(a_1\,\backslash c)\cdot a_2$\\ |
|
557 $(_{bs}a^*)\,\backslash c$ & $\dn$ & |
|
558 $_{bs}\;((\textit{fuse}\, [\Z] (r\,\backslash c))\cdot |
|
559 (_{[]}r^*))$ |
|
560 \end{tabular} |
|
561 \end{center} |
|
562 |
|
563 %\end{definition} |
519 \noindent |
564 \noindent |
520 For instance, when we unfold $\textit{STAR} \; bs \; a$ into a sequence, |
565 For instance, when we unfold $\textit{STAR} \; bs \; a$ into a sequence, |
521 we need to attach an additional bit $Z$ to the front of $r \backslash c$ |
566 we need to attach an additional bit $Z$ to the front of $r \backslash c$ |
522 to indicate that there is one more star iteration. Also the $SEQ$ clause |
567 to indicate that there is one more star iteration. Also the $SEQ$ clause |
523 is more subtle---when $a_1$ is $\textit{bnullable}$ (here |
568 is more subtle---when $a_1$ is $\textit{bnullable}$ (here |