596 \begin{tabular}{lcl} |
596 \begin{tabular}{lcl} |
597 $\textit{bmkeps}\,(_{bs}\ONE)$ & $\dn$ & $bs$\\ |
597 $\textit{bmkeps}\,(_{bs}\ONE)$ & $\dn$ & $bs$\\ |
598 $\textit{bmkeps}\,(_{bs}\oplus a::\textit{as})$ & $\dn$ & |
598 $\textit{bmkeps}\,(_{bs}\oplus a::\textit{as})$ & $\dn$ & |
599 $\textit{if}\;\textit{bnullable}\,a$\\ |
599 $\textit{if}\;\textit{bnullable}\,a$\\ |
600 & &$\textit{then}\;bs\,@\,\textit{bmkeps}\,a$\\ |
600 & &$\textit{then}\;bs\,@\,\textit{bmkeps}\,a$\\ |
601 & &$\textit{else}\;bs\,@\,\textit{bmkeps}\,(_{bs}\textit{as})$\\ |
601 & &$\textit{else}\;bs\,@\,\textit{bmkeps}\,(_{bs}\oplus \textit{as})$\\ |
602 $\textit{bmkeps}\,(_{bs} a_1 \cdot a_2)$ & $\dn$ & |
602 $\textit{bmkeps}\,(_{bs} a_1 \cdot a_2)$ & $\dn$ & |
603 $bs \,@\,\textit{bmkeps}\,a_1\,@\, \textit{bmkeps}\,a_2$\\ |
603 $bs \,@\,\textit{bmkeps}\,a_1\,@\, \textit{bmkeps}\,a_2$\\ |
604 $\textit{bmkeps}\,(_{bs}a^*)$ & $\dn$ & |
604 $\textit{bmkeps}\,(_{bs}a^*)$ & $\dn$ & |
605 $bs \,@\, [1]$ |
605 $bs \,@\, [0]$ |
606 \end{tabular} |
606 \end{tabular} |
607 \end{center} |
607 \end{center} |
608 %\end{definition} |
608 %\end{definition} |
609 |
609 |
610 \noindent |
610 \noindent |
640 that the expected bound can be achieved. Obviously we could only |
640 that the expected bound can be achieved. Obviously we could only |
641 partially cover the search space as there are infinitely many regular |
641 partially cover the search space as there are infinitely many regular |
642 expressions and strings. |
642 expressions and strings. |
643 |
643 |
644 One modification we introduced is to allow a list of annotated regular |
644 One modification we introduced is to allow a list of annotated regular |
645 expressions in the \textit{ALTS} constructor. This allows us to not just |
645 expressions in the $\oplus$ constructor. This allows us to not just |
646 delete unnecessary $\ZERO$s and $\ONE$s from regular expressions, but |
646 delete unnecessary $\ZERO$s and $\ONE$s from regular expressions, but |
647 also unnecessary ``copies'' of regular expressions (very similar to |
647 also unnecessary ``copies'' of regular expressions (very similar to |
648 simplifying $r + r$ to just $r$, but in a more general setting). Another |
648 simplifying $r + r$ to just $r$, but in a more general setting). Another |
649 modification is that we use simplification rules inspired by Antimirov's |
649 modification is that we use simplification rules inspired by Antimirov's |
650 work on partial derivatives. They maintain the idea that only the first |
650 work on partial derivatives. They maintain the idea that only the first |
656 %Is it $ALTS$ or $ALTS$?}\\ |
656 %Is it $ALTS$ or $ALTS$?}\\ |
657 |
657 |
658 \begin{center} |
658 \begin{center} |
659 \begin{tabular}{@{}lcl@{}} |
659 \begin{tabular}{@{}lcl@{}} |
660 |
660 |
661 $\textit{simp} \; (\textit{SEQ}\;bs\,a_1\,a_2)$ & $\dn$ & $ (\textit{simp} \; a_1, \textit{simp} \; a_2) \; \textit{match} $ \\ |
661 $\textit{simp} \; (_{bs}a_1\cdot a_2)$ & $\dn$ & $ (\textit{simp} \; a_1, \textit{simp} \; a_2) \; \textit{match} $ \\ |
662 &&$\quad\textit{case} \; (\ZERO, \_) \Rightarrow \ZERO$ \\ |
662 &&$\quad\textit{case} \; (\ZERO, \_) \Rightarrow \ZERO$ \\ |
663 &&$\quad\textit{case} \; (\_, \ZERO) \Rightarrow \ZERO$ \\ |
663 &&$\quad\textit{case} \; (\_, \ZERO) \Rightarrow \ZERO$ \\ |
664 &&$\quad\textit{case} \; (\ONE, a_2') \Rightarrow \textit{fuse} \; bs \; a_2'$ \\ |
664 &&$\quad\textit{case} \; (\ONE, a_2') \Rightarrow \textit{fuse} \; bs \; a_2'$ \\ |
665 &&$\quad\textit{case} \; (a_1', \ONE) \Rightarrow \textit{fuse} \; bs \; a_1'$ \\ |
665 &&$\quad\textit{case} \; (a_1', \ONE) \Rightarrow \textit{fuse} \; bs \; a_1'$ \\ |
666 &&$\quad\textit{case} \; (a_1', a_2') \Rightarrow \textit{SEQ} \; bs \; a_1' \; a_2'$ \\ |
666 &&$\quad\textit{case} \; (a_1', a_2') \Rightarrow _{bs}a_1' \cdot a_2'$ \\ |
667 |
667 |
668 $\textit{simp} \; (\textit{ALTS}\;bs\,as)$ & $\dn$ & $\textit{distinct}( \textit{flatten} ( \textit{map simp as})) \; \textit{match} $ \\ |
668 $\textit{simp} \; (_{bs}\oplus \textit{as})$ & $\dn$ & $\textit{distinct}( \textit{flatten} ( \textit{map simp as})) \; \textit{match} $ \\ |
669 &&$\quad\textit{case} \; [] \Rightarrow \ZERO$ \\ |
669 &&$\quad\textit{case} \; [] \Rightarrow \ZERO$ \\ |
670 &&$\quad\textit{case} \; a :: [] \Rightarrow \textit{fuse bs a}$ \\ |
670 &&$\quad\textit{case} \; a :: [] \Rightarrow \textit{fuse bs a}$ \\ |
671 &&$\quad\textit{case} \; as' \Rightarrow \textit{ALTS}\;bs\;as'$\\ |
671 &&$\quad\textit{case} \; as' \Rightarrow _{bs}\oplus \textit{as'}$\\ |
672 |
672 |
673 $\textit{simp} \; a$ & $\dn$ & $\textit{a} \qquad \textit{otherwise}$ |
673 $\textit{simp} \; a$ & $\dn$ & $\textit{a} \qquad \textit{otherwise}$ |
674 \end{tabular} |
674 \end{tabular} |
675 \end{center} |
675 \end{center} |
676 |
676 |
678 The simplification does a pattern matching on the regular expression. |
678 The simplification does a pattern matching on the regular expression. |
679 When it detected that the regular expression is an alternative or |
679 When it detected that the regular expression is an alternative or |
680 sequence, it will try to simplify its children regular expressions |
680 sequence, it will try to simplify its children regular expressions |
681 recursively and then see if one of the children turn into $\ZERO$ or |
681 recursively and then see if one of the children turn into $\ZERO$ or |
682 $\ONE$, which might trigger further simplification at the current level. |
682 $\ONE$, which might trigger further simplification at the current level. |
683 The most involved part is the $\textit{ALTS}$ clause, where we use two |
683 The most involved part is the $\oplus$ clause, where we use two |
684 auxiliary functions $\textit{flatten}$ and $\textit{distinct}$ to open up nested |
684 auxiliary functions $\textit{flatten}$ and $\textit{distinct}$ to open up nested |
685 $\textit{ALTS}$ and reduce as many duplicates as possible. Function |
685 alternatives and reduce as many duplicates as possible. Function |
686 $\textit{distinct}$ keeps the first occurring copy only and remove all later ones |
686 $\textit{distinct}$ keeps the first occurring copy only and remove all later ones |
687 when detected duplicates. Function $\textit{flatten}$ opens up nested \textit{ALTS}. |
687 when detected duplicates. Function $\textit{flatten}$ opens up nested $\oplus$s. |
688 Its recursive definition is given below: |
688 Its recursive definition is given below: |
689 |
689 |
690 \begin{center} |
690 \begin{center} |
691 \begin{tabular}{@{}lcl@{}} |
691 \begin{tabular}{@{}lcl@{}} |
692 $\textit{flatten} \; (\textit{ALTS}\;bs\,as) :: as'$ & $\dn$ & $(\textit{map} \; |
692 $\textit{flatten} \; (_{bs}\oplus \textit{as}) :: \textit{as'}$ & $\dn$ & $(\textit{map} \; |
693 (\textit{fuse}\;bs)\; \textit{as}) \; @ \; \textit{flatten} \; as' $ \\ |
693 (\textit{fuse}\;bs)\; \textit{as}) \; @ \; \textit{flatten} \; as' $ \\ |
694 $\textit{flatten} \; \textit{ZERO} :: as'$ & $\dn$ & $ \textit{flatten} \; as' $ \\ |
694 $\textit{flatten} \; \ZERO :: as'$ & $\dn$ & $ \textit{flatten} \; \textit{as'} $ \\ |
695 $\textit{flatten} \; a :: as'$ & $\dn$ & $a :: \textit{flatten} \; as'$ \quad(otherwise) |
695 $\textit{flatten} \; a :: as'$ & $\dn$ & $a :: \textit{flatten} \; \textit{as'}$ \quad(otherwise) |
696 \end{tabular} |
696 \end{tabular} |
697 \end{center} |
697 \end{center} |
698 |
698 |
699 \noindent |
699 \noindent |
700 Here $\textit{flatten}$ behaves like the traditional functional programming flatten |
700 Here $\textit{flatten}$ behaves like the traditional functional programming flatten |
934 we use the helper function retrieve described by Sulzmann and Lu: |
934 we use the helper function retrieve described by Sulzmann and Lu: |
935 \begin{center} |
935 \begin{center} |
936 \begin{tabular}{@{}l@{\hspace{2mm}}c@{\hspace{2mm}}l@{}} |
936 \begin{tabular}{@{}l@{\hspace{2mm}}c@{\hspace{2mm}}l@{}} |
937 $\textit{retrieve}\,(_{bs}\ONE)\,\Empty$ & $\dn$ & $bs$\\ |
937 $\textit{retrieve}\,(_{bs}\ONE)\,\Empty$ & $\dn$ & $bs$\\ |
938 $\textit{retrieve}\,(_{bs}{\bf c})\,(\Char\,d)$ & $\dn$ & $bs$\\ |
938 $\textit{retrieve}\,(_{bs}{\bf c})\,(\Char\,d)$ & $\dn$ & $bs$\\ |
939 $\textit{retrieve}\,(\textit{ALTS}\,bs\,a::as)\,(\Left\,v)$ & $\dn$ & |
939 $\textit{retrieve}\,(_{bs}\oplus a::as)\,(\Left\,v)$ & $\dn$ & |
940 $bs \,@\, \textit{retrieve}\,a\,v$\\ |
940 $bs \,@\, \textit{retrieve}\,a\,v$\\ |
941 $\textit{retrieve}\,(\textit{ALTS}\,bs\,a::as)\,(\Right\,v)$ & $\dn$ & |
941 $\textit{retrieve}\,(_{bs}\oplus a::as)\,(\Right\,v)$ & $\dn$ & |
942 $bs \,@\, \textit{retrieve}\,(\textit{ALTS}\,bs\,as)\,v$\\ |
942 $\textit{bs} \,@\, \textit{retrieve}\,(_{[]}\oplus as)\,v$\\ |
943 $\textit{retrieve}\,(\textit{SEQ}\,bs\,a_1\,a_2)\,(\Seq\,v_1\,v_2)$ & $\dn$ & |
943 $\textit{retrieve}\,(_{bs}a_1\cdot a_2)\,(\Seq\,v_1\,v_2)$ & $\dn$ & |
944 $bs \,@\,\textit{retrieve}\,a_1\,v_1\,@\, \textit{retrieve}\,a_2\,v_2$\\ |
944 $bs \,@\,\textit{retrieve}\,a_1\,v_1\,@\, \textit{retrieve}\,a_2\,v_2$\\ |
945 $\textit{retrieve}\,(\textit{STAR}\,bs\,a)\,(\Stars\,[])$ & $\dn$ & |
945 $\textit{retrieve}\,(_{bs}a^*)\,(\Stars\,[])$ & $\dn$ & |
946 $bs \,@\, [\S]$\\ |
946 $bs \,@\, [0]$\\ |
947 $\textit{retrieve}\,(\textit{STAR}\,bs\,a)\,(\Stars\,(v\!::\!vs))$ & $\dn$ &\\ |
947 $\textit{retrieve}\,(_{bs}a^*)\,(\Stars\,(v\!::\!vs))$ & $\dn$ &\\ |
948 \multicolumn{3}{l}{ |
948 \multicolumn{3}{l}{ |
949 \hspace{3cm}$bs \,@\, [\Z] \,@\, \textit{retrieve}\,a\,v\,@\, |
949 \hspace{3cm}$bs \,@\, [1] \,@\, \textit{retrieve}\,a\,v\,@\, |
950 \textit{retrieve}\,(\textit{STAR}\,[]\,a)\,(\Stars\,vs)$}\\ |
950 \textit{retrieve}\,(_{[]}a^*)\,(\Stars\,vs)$}\\ |
951 \end{tabular} |
951 \end{tabular} |
952 \end{center} |
952 \end{center} |
953 %\comment{Did not read further}\\ |
953 %\comment{Did not read further}\\ |
954 This function assembles the bitcode |
954 This function assembles the bitcode |
955 %that corresponds to a lexical value for how |
955 %that corresponds to a lexical value for how |
981 through the same simplification step as $\textit{simp}(a)$, we are able |
981 through the same simplification step as $\textit{simp}(a)$, we are able |
982 to extract the bitcode that gives the same parsing information as the |
982 to extract the bitcode that gives the same parsing information as the |
983 unsimplified one. However, we noticed that constructing such a $v'$ |
983 unsimplified one. However, we noticed that constructing such a $v'$ |
984 from $v$ is not so straightforward. The point of this is that we might |
984 from $v$ is not so straightforward. The point of this is that we might |
985 be able to finally bridge the gap by proving |
985 be able to finally bridge the gap by proving |
986 |
|
987 |
|
988 \noindent\rule[1.5ex]{\linewidth}{4pt} |
|
989 There is no mention of retrieve yet .... this is the second trick in the |
|
990 existing proof. I am not sure whether you need to explain annotated regular |
|
991 expressions much earlier - maybe before the ``existing proof'' section, or |
|
992 evan earlier. |
|
993 |
|
994 \noindent\rule[1.5ex]{\linewidth}{4pt} |
|
995 |
986 |
996 \noindent |
987 \noindent |
997 By using a property of retrieve we have the $\textit{RHS}$ of the above equality is |
988 By using a property of retrieve we have the $\textit{RHS}$ of the above equality is |
998 $decode (retrieve (r^\uparrow \backslash(s @ [c])) v) r$, and this gives the |
989 $decode (retrieve (r^\uparrow \backslash(s @ [c])) v) r$, and this gives the |
999 main lemma result: |
990 main lemma result: |