871 %what we are doing in the past 6 months. |
871 %what we are doing in the past 6 months. |
872 %\bigskip\noindent\rule[1.5ex]{\linewidth}{5pt} |
872 %\bigskip\noindent\rule[1.5ex]{\linewidth}{5pt} |
873 |
873 |
874 \subsubsection*{Existing Proof} |
874 \subsubsection*{Existing Proof} |
875 |
875 |
876 For this we have started with looking at the original proof that |
876 For this we have started with looking at the proof of |
877 established that the bitsequence algorrithm produces the same result |
|
878 as the algorithm not using bitsequences. Formally this proof |
|
879 established |
|
880 |
|
881 \begin{equation}\label{lexer} |
877 \begin{equation}\label{lexer} |
882 \blexer \; (r^\uparrow) s = \lexer \;r \;s |
878 \blexer \; (r^\uparrow) s = \lexer \;r \;s, |
883 \end{equation} |
879 \end{equation} |
884 |
880 |
885 %\noindent |
881 %\noindent |
886 %might provide us insight into proving |
882 %might provide us insight into proving |
887 %\begin{center} |
883 %\begin{center} |
888 %$\blexer \; r^\uparrow \;s = \blexers \; r^\uparrow \;s$ |
884 %$\blexer \; r^\uparrow \;s = \blexers \; r^\uparrow \;s$ |
889 %\end{center} |
885 %\end{center} |
890 |
886 |
891 \noindent |
887 \noindent |
|
888 which established the bit-sequence algorithm produces the same |
|
889 result as the original algorithm, which does not use |
|
890 bit-sequence. |
892 The proof uses two ``tricks''. One is that it uses a \flex-function |
891 The proof uses two ``tricks''. One is that it uses a \flex-function |
893 |
892 |
894 \begin{center} |
893 \begin{center} |
895 \begin{tabular}{lcl} |
894 \begin{tabular}{lcl} |
896 $\textit{flex} \;r\; f\; (c\!::\!s) $ & $\dn$ & $\textit{flex} \; (r\backslash c) \;(\lambda v. f (inj \; r \; c \; v)) \;s$ \\ |
895 $\textit{flex} \;r\; f\; (c\!::\!s) $ & $\dn$ & $\textit{flex} \; (r\backslash c) \;(\lambda v. f (inj \; r \; c \; v)) \;s$ \\ |
897 $\textit{flex} \;r\; f\; [\,] $ & $\dn$ & $f$ |
896 $\textit{flex} \;r\; f\; [\,] $ & $\dn$ & $f$ |
898 \end{tabular} |
897 \end{tabular} |
899 \end{center} |
898 \end{center} |
900 |
899 |
901 \noindent |
900 \noindent |
902 and then proves for the right-hand side in \eqref{lexer} |
901 to prove for the right-hand side in \eqref{lexer} |
903 |
902 |
904 \begin{center} |
903 \begin{center} |
905 $\lexer \;r\; s = \flex \;\textit{id} \; r\;s \;(\mkeps \; (r\backslash s))$ |
904 $\lexer \;r\; s = \flex \;\textit{id} \; r\;s \;(\mkeps \; (r\backslash s))$. |
906 \end{center}. |
905 \end{center} |
907 |
906 |
908 |
907 |
909 |
908 |
910 |
909 \noindent |
911 \noindent |
910 linking $\flex$ and $\lexer$, |
912 The $\flex$-function essentially does lexing by |
911 it essentially does lexing by |
913 stacking up injection functions while doing derivatives. |
912 stacking up injection functions while doing derivatives, |
914 |
|
915 explicitly showing the order of characters being |
913 explicitly showing the order of characters being |
916 injected back in each step. |
914 injected back in each step. |
917 With $\flex$ we can write $\lexer$ this way: |
915 With $\flex$ we can write $\lexer$ this way: |
918 |
916 |
919 \begin{center} |
917 \begin{center} |