diff -r 1ca011142964 -r df9e966ecb6d etnms/etnms.tex --- a/etnms/etnms.tex Wed Feb 05 12:02:21 2020 +0000 +++ b/etnms/etnms.tex Wed Feb 05 12:41:30 2020 +0000 @@ -598,11 +598,11 @@ $\textit{bmkeps}\,(_{bs}\oplus a::\textit{as})$ & $\dn$ & $\textit{if}\;\textit{bnullable}\,a$\\ & &$\textit{then}\;bs\,@\,\textit{bmkeps}\,a$\\ - & &$\textit{else}\;bs\,@\,\textit{bmkeps}\,(_{bs}\textit{as})$\\ + & &$\textit{else}\;bs\,@\,\textit{bmkeps}\,(_{bs}\oplus \textit{as})$\\ $\textit{bmkeps}\,(_{bs} a_1 \cdot a_2)$ & $\dn$ & $bs \,@\,\textit{bmkeps}\,a_1\,@\, \textit{bmkeps}\,a_2$\\ $\textit{bmkeps}\,(_{bs}a^*)$ & $\dn$ & - $bs \,@\, [1]$ + $bs \,@\, [0]$ \end{tabular} \end{center} %\end{definition} @@ -642,7 +642,7 @@ expressions and strings. One modification we introduced is to allow a list of annotated regular -expressions in the \textit{ALTS} constructor. This allows us to not just +expressions in the $\oplus$ constructor. This allows us to not just delete unnecessary $\ZERO$s and $\ONE$s from regular expressions, but also unnecessary ``copies'' of regular expressions (very similar to simplifying $r + r$ to just $r$, but in a more general setting). Another @@ -658,17 +658,17 @@ \begin{center} \begin{tabular}{@{}lcl@{}} - $\textit{simp} \; (\textit{SEQ}\;bs\,a_1\,a_2)$ & $\dn$ & $ (\textit{simp} \; a_1, \textit{simp} \; a_2) \; \textit{match} $ \\ + $\textit{simp} \; (_{bs}a_1\cdot a_2)$ & $\dn$ & $ (\textit{simp} \; a_1, \textit{simp} \; a_2) \; \textit{match} $ \\ &&$\quad\textit{case} \; (\ZERO, \_) \Rightarrow \ZERO$ \\ &&$\quad\textit{case} \; (\_, \ZERO) \Rightarrow \ZERO$ \\ &&$\quad\textit{case} \; (\ONE, a_2') \Rightarrow \textit{fuse} \; bs \; a_2'$ \\ &&$\quad\textit{case} \; (a_1', \ONE) \Rightarrow \textit{fuse} \; bs \; a_1'$ \\ - &&$\quad\textit{case} \; (a_1', a_2') \Rightarrow \textit{SEQ} \; bs \; a_1' \; a_2'$ \\ + &&$\quad\textit{case} \; (a_1', a_2') \Rightarrow _{bs}a_1' \cdot a_2'$ \\ - $\textit{simp} \; (\textit{ALTS}\;bs\,as)$ & $\dn$ & $\textit{distinct}( \textit{flatten} ( \textit{map simp as})) \; \textit{match} $ \\ + $\textit{simp} \; (_{bs}\oplus \textit{as})$ & $\dn$ & $\textit{distinct}( \textit{flatten} ( \textit{map simp as})) \; \textit{match} $ \\ &&$\quad\textit{case} \; [] \Rightarrow \ZERO$ \\ &&$\quad\textit{case} \; a :: [] \Rightarrow \textit{fuse bs a}$ \\ - &&$\quad\textit{case} \; as' \Rightarrow \textit{ALTS}\;bs\;as'$\\ + &&$\quad\textit{case} \; as' \Rightarrow _{bs}\oplus \textit{as'}$\\ $\textit{simp} \; a$ & $\dn$ & $\textit{a} \qquad \textit{otherwise}$ \end{tabular} @@ -680,19 +680,19 @@ sequence, it will try to simplify its children regular expressions recursively and then see if one of the children turn into $\ZERO$ or $\ONE$, which might trigger further simplification at the current level. -The most involved part is the $\textit{ALTS}$ clause, where we use two +The most involved part is the $\oplus$ clause, where we use two auxiliary functions $\textit{flatten}$ and $\textit{distinct}$ to open up nested -$\textit{ALTS}$ and reduce as many duplicates as possible. Function +alternatives and reduce as many duplicates as possible. Function $\textit{distinct}$ keeps the first occurring copy only and remove all later ones -when detected duplicates. Function $\textit{flatten}$ opens up nested \textit{ALTS}. +when detected duplicates. Function $\textit{flatten}$ opens up nested $\oplus$s. Its recursive definition is given below: \begin{center} \begin{tabular}{@{}lcl@{}} - $\textit{flatten} \; (\textit{ALTS}\;bs\,as) :: as'$ & $\dn$ & $(\textit{map} \; + $\textit{flatten} \; (_{bs}\oplus \textit{as}) :: \textit{as'}$ & $\dn$ & $(\textit{map} \; (\textit{fuse}\;bs)\; \textit{as}) \; @ \; \textit{flatten} \; as' $ \\ - $\textit{flatten} \; \textit{ZERO} :: as'$ & $\dn$ & $ \textit{flatten} \; as' $ \\ - $\textit{flatten} \; a :: as'$ & $\dn$ & $a :: \textit{flatten} \; as'$ \quad(otherwise) + $\textit{flatten} \; \ZERO :: as'$ & $\dn$ & $ \textit{flatten} \; \textit{as'} $ \\ + $\textit{flatten} \; a :: as'$ & $\dn$ & $a :: \textit{flatten} \; \textit{as'}$ \quad(otherwise) \end{tabular} \end{center} @@ -936,18 +936,18 @@ \begin{tabular}{@{}l@{\hspace{2mm}}c@{\hspace{2mm}}l@{}} $\textit{retrieve}\,(_{bs}\ONE)\,\Empty$ & $\dn$ & $bs$\\ $\textit{retrieve}\,(_{bs}{\bf c})\,(\Char\,d)$ & $\dn$ & $bs$\\ - $\textit{retrieve}\,(\textit{ALTS}\,bs\,a::as)\,(\Left\,v)$ & $\dn$ & + $\textit{retrieve}\,(_{bs}\oplus a::as)\,(\Left\,v)$ & $\dn$ & $bs \,@\, \textit{retrieve}\,a\,v$\\ - $\textit{retrieve}\,(\textit{ALTS}\,bs\,a::as)\,(\Right\,v)$ & $\dn$ & - $bs \,@\, \textit{retrieve}\,(\textit{ALTS}\,bs\,as)\,v$\\ - $\textit{retrieve}\,(\textit{SEQ}\,bs\,a_1\,a_2)\,(\Seq\,v_1\,v_2)$ & $\dn$ & + $\textit{retrieve}\,(_{bs}\oplus a::as)\,(\Right\,v)$ & $\dn$ & + $\textit{bs} \,@\, \textit{retrieve}\,(_{[]}\oplus as)\,v$\\ + $\textit{retrieve}\,(_{bs}a_1\cdot a_2)\,(\Seq\,v_1\,v_2)$ & $\dn$ & $bs \,@\,\textit{retrieve}\,a_1\,v_1\,@\, \textit{retrieve}\,a_2\,v_2$\\ - $\textit{retrieve}\,(\textit{STAR}\,bs\,a)\,(\Stars\,[])$ & $\dn$ & - $bs \,@\, [\S]$\\ - $\textit{retrieve}\,(\textit{STAR}\,bs\,a)\,(\Stars\,(v\!::\!vs))$ & $\dn$ &\\ + $\textit{retrieve}\,(_{bs}a^*)\,(\Stars\,[])$ & $\dn$ & + $bs \,@\, [0]$\\ + $\textit{retrieve}\,(_{bs}a^*)\,(\Stars\,(v\!::\!vs))$ & $\dn$ &\\ \multicolumn{3}{l}{ - \hspace{3cm}$bs \,@\, [\Z] \,@\, \textit{retrieve}\,a\,v\,@\, - \textit{retrieve}\,(\textit{STAR}\,[]\,a)\,(\Stars\,vs)$}\\ + \hspace{3cm}$bs \,@\, [1] \,@\, \textit{retrieve}\,a\,v\,@\, + \textit{retrieve}\,(_{[]}a^*)\,(\Stars\,vs)$}\\ \end{tabular} \end{center} %\comment{Did not read further}\\ @@ -984,15 +984,6 @@ from $v$ is not so straightforward. The point of this is that we might be able to finally bridge the gap by proving - -\noindent\rule[1.5ex]{\linewidth}{4pt} -There is no mention of retrieve yet .... this is the second trick in the -existing proof. I am not sure whether you need to explain annotated regular -expressions much earlier - maybe before the ``existing proof'' section, or -evan earlier. - -\noindent\rule[1.5ex]{\linewidth}{4pt} - \noindent By using a property of retrieve we have the $\textit{RHS}$ of the above equality is $decode (retrieve (r^\uparrow \backslash(s @ [c])) v) r$, and this gives the