--- 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