# HG changeset patch # User Chengsong # Date 1582065870 0 # Node ID 5ca3b84e0eba029801d9d21c5a352e7a158680c5 # Parent 0172d422e93e79be15fa421ddadcb808f87ff3bb v diff -r 0172d422e93e -r 5ca3b84e0eba etnms/etnms.tex --- a/etnms/etnms.tex Sun Feb 16 22:37:26 2020 +0000 +++ b/etnms/etnms.tex Tue Feb 18 22:44:30 2020 +0000 @@ -873,13 +873,9 @@ \subsubsection*{Existing Proof} -For this we have started with looking at the original proof that -established that the bitsequence algorrithm produces the same result -as the algorithm not using bitsequences. Formally this proof -established - +For this we have started with looking at the proof of \begin{equation}\label{lexer} -\blexer \; (r^\uparrow) s = \lexer \;r \;s +\blexer \; (r^\uparrow) s = \lexer \;r \;s, \end{equation} %\noindent @@ -889,6 +885,9 @@ %\end{center} \noindent +which established the bit-sequence algorithm produces the same +result as the original algorithm, which does not use +bit-sequence. The proof uses two ``tricks''. One is that it uses a \flex-function \begin{center} @@ -899,19 +898,18 @@ \end{center} \noindent -and then proves for the right-hand side in \eqref{lexer} +to prove for the right-hand side in \eqref{lexer} \begin{center} -$\lexer \;r\; s = \flex \;\textit{id} \; r\;s \;(\mkeps \; (r\backslash s))$ -\end{center}. - +$\lexer \;r\; s = \flex \;\textit{id} \; r\;s \;(\mkeps \; (r\backslash s))$. +\end{center} \noindent -The $\flex$-function essentially does lexing by -stacking up injection functions while doing derivatives. - +linking $\flex$ and $\lexer$, +it essentially does lexing by +stacking up injection functions while doing derivatives, explicitly showing the order of characters being injected back in each step. With $\flex$ we can write $\lexer$ this way: