1652 $r \gg \retrieve \; r \; (r\downarrow) \; \textit{id} \; s \; v) \; c \; v)$\\ |
1652 $r \gg \retrieve \; r \; (r\downarrow) \; \textit{id} \; s \; v) \; c \; v)$\\ |
1653 \end{tabular} |
1653 \end{tabular} |
1654 \end{center} |
1654 \end{center} |
1655 Here $\gg$ is almost like an $\textit{NFA}$ in the sense that |
1655 Here $\gg$ is almost like an $\textit{NFA}$ in the sense that |
1656 it simulates the lexing process with respect to different strings. |
1656 it simulates the lexing process with respect to different strings. |
1657 \end{itemize} |
1657 |
1658 Our hope is that using $\gg$ we can prove the bits |
1658 Our hope is that using $\gg$ we can prove the bits |
1659 information are not lost when we simplify a regular expression, |
1659 information are not lost when we simplify a regular expression, |
1660 so we need to relate $\gg$ with simplifcation, for example, |
1660 so we need to relate $\gg$ with simplifcation, for example, |
1661 one of the lemmas we have proved about $\gg$ is that |
1661 one of the lemmas we have proved about $\gg$ is that |
1662 |
1662 \item |
1663 $\simp$ |
1663 \begin{center} |
|
1664 $\simp \; a \gg \textit{bs} \iff a \gg \textit{bs}$ |
|
1665 \end{center} |
|
1666 This could be a step towards our goal, as |
|
1667 it assures that after simplification none of the |
|
1668 bitsequence that can be created by |
|
1669 the original annotated regular expression |
|
1670 is lost. |
|
1671 If we could prove the following that would be |
|
1672 another step towards our proof, |
|
1673 |
|
1674 \item |
|
1675 \begin{center} |
|
1676 $(\simp \;a) \backslash s \gg \textit{bs} \iff a\backslash s \gg \textit{bs}$ |
|
1677 \end{center} |
|
1678 |
|
1679 as it says |
|
1680 the simplified regular expression after derivatives will |
|
1681 still have the full capacity of producing bitsequences |
|
1682 as the unsimplified ones-- pretty much |
|
1683 the intuition we try to establish. |
|
1684 And if we could prove |
|
1685 \item |
|
1686 \begin{center} |
|
1687 $a \backslash s \gg \textit{bs} \iff a\backslash_\textit{simp} s \gg \textit{bs}$ |
|
1688 \end{center} |
|
1689 That would be just a stone's throw away |
|
1690 from $\blexer \; r \; s = \blexers \; r \; s$. |
|
1691 |
|
1692 \end{itemize} |
|
1693 What we do after we work out |
|
1694 the proof of the above lemma |
|
1695 is still not clear. It is one of the next steps we need to |
|
1696 work on. |
|
1697 |
1664 \subsection{the $\textit{ders}_2$ Function} |
1698 \subsection{the $\textit{ders}_2$ Function} |
1665 If we want to prove the result |
1699 If we want to prove the result |
1666 \begin{center} |
1700 \begin{center} |
1667 $ \textit{blexer}\_{simp}(r, \; s) = \textit{blexer}(r, \; s)$ |
1701 $ \textit{blexer}\_{simp}(r, \; s) = \textit{blexer}(r, \; s)$ |
1668 \end{center} |
1702 \end{center} |
1669 inductively |
1703 inductively |
1670 on the structure of the regular expression, |
1704 on the structure of the regular expression, |
1671 then we need to induct on the case $r_1 \cdot r_2$, |
1705 then we need to induct on the case $r_1 \cdot r_2$, |
1672 it can be good if we could express $(r_1 \cdot r_2) \backslash s$ |
1706 it can be good if we could express $(r_1 \cdot r_2) \backslash s$ |
1673 in terms of $r_1 \backslash s$ and $r_2 \backslash s$, |
1707 in terms of $r_1 \backslash s_1$ and $r_2 \backslash s_1$, |
1674 and this naturally induces the $ders2$ function, |
1708 where $s_1$ is a substring of $s$. |
|
1709 For this we introduce the $\textit{ders2}$ function, |
1675 which does a "convolution" on $r_1$ and $r_2$ using the string |
1710 which does a "convolution" on $r_1$ and $r_2$ using the string |
1676 $s$. |
1711 $s$. |
1677 It is based on the observation that the derivative of $r_1 \cdot r_2$ |
1712 It is based on the observation that the derivative of $r_1 \cdot r_2$ |
1678 with respect to a string $s$ can actually be written in an "explicit form" |
1713 with respect to a string $s$ can actually be written in an "explicit form" |
1679 composed of $r_1$'s derivative of $s$ and $r_2$'s derivative of $s$. |
1714 composed of $r_1$'s derivative of $s$ and $r_2$'s derivative of $s$. |