907 \end{center} |
907 \end{center} |
908 |
908 |
909 |
909 |
910 |
910 |
911 \noindent |
911 \noindent |
912 linking $\flex$ and $\lexer$, |
912 This property links $\flex$ and $\lexer$, |
913 it essentially does lexing by |
913 it essentially does lexing by |
914 stacking up injection functions while doing derivatives, |
914 stacking up injection functions while doing derivatives, |
915 explicitly showing the order of characters being |
915 explicitly showing the order of characters being |
916 injected back in each step. |
916 injected back in each step. |
917 With $\flex$ we can write $\lexer$ this way: |
|
918 |
|
919 \begin{center} |
|
920 $\lexer \;r\; s = \flex \;id \; r\;s \;(\mkeps (r\backslash s))$ |
|
921 \end{center} |
|
922 |
917 |
923 \noindent |
918 \noindent |
924 The other trick, which is the crux in the existing proof, |
919 The other trick, which is the crux in the existing proof, |
925 is the use of $\retrieve$-function by Sulzmann and Lu: |
920 is the use of the $\retrieve$-function by Sulzmann and Lu: |
926 \begin{center} |
921 \begin{center} |
927 \begin{tabular}{@{}l@{\hspace{2mm}}c@{\hspace{2mm}}l@{}} |
922 \begin{tabular}{@{}l@{\hspace{2mm}}c@{\hspace{2mm}}l@{}} |
928 $\textit{retrieve}\,(_{bs}\ONE)\,\Empty$ & $\dn$ & $bs$\\ |
923 $\textit{retrieve}\,(_{bs}\ONE)\,\Empty$ & $\dn$ & $bs$\\ |
929 $\textit{retrieve}\,(_{bs}{\bf c})\,(\Char\,d)$ & $\dn$ & $bs$\\ |
924 $\textit{retrieve}\,(_{bs}{\bf c})\,(\Char\,d)$ & $\dn$ & $bs$\\ |
930 $\textit{retrieve}\,(_{bs}\sum a::as)\,(\Left\,v)$ & $\dn$ & |
925 $\textit{retrieve}\,(_{bs}\sum a::as)\,(\Left\,v)$ & $\dn$ & |
944 |
939 |
945 \noindent |
940 \noindent |
946 This function assembles the bitcode |
941 This function assembles the bitcode |
947 using information from both the derivative regular expression and the |
942 using information from both the derivative regular expression and the |
948 value. Sulzmann and Lu proposed this function, but did not prove |
943 value. Sulzmann and Lu proposed this function, but did not prove |
949 anything about it. Ausaf and Urban made this important use of the |
944 anything about it. Ausaf and Urban made use of the |
950 fact about $\retrieve$ in the proof: |
945 fact about $\retrieve$ in their proof: |
951 |
946 |
952 \begin{center} |
947 \begin{center} |
953 $\retrieve \rup \backslash c \; v = \retrieve \rup (\inj \;r \;c \; v)$ |
948 $\retrieve\; \rup \backslash c \; v = \retrieve \; \rup (\inj \;r \;c \; v)$ |
954 \end{center} |
949 \end{center} |
955 |
950 |
956 \noindent |
951 \noindent |
957 whereby $r^\uparrow$ stands for the internalised version of $r$. |
952 whereby $r^\uparrow$ stands for the internalised version of $r$. |
958 This fact, together with the fact of how $\flex$ relates to injection: |
953 This fact, together with the fact of how $\flex$ relates to injection: |
971 \begin{center} |
966 \begin{center} |
972 $ \flex \; r\; id\; s\; v = \textit{decode} \;( \textit{retrieve}\; (\rup \backslash s) \; v \;) r$ |
967 $ \flex \; r\; id\; s\; v = \textit{decode} \;( \textit{retrieve}\; (\rup \backslash s) \; v \;) r$ |
973 \end{center} |
968 \end{center} |
974 \noindent |
969 \noindent |
975 where $\mkeps(r\backslash s) $ is denoted using $v$, |
970 where $\mkeps(r\backslash s) $ is denoted using $v$, |
976 then a reverse induction technique is |
971 then a reverse induction |
977 best suited here to make use of |
972 helps with using |
978 the fact~\eqref{flex} in proving the $n+1$ step: |
973 the fact~\eqref{flex} in proving the $n+1$ step: |
979 \begin{center} |
974 \begin{center} |
980 $ \flex \; r\; id\; (s@[c])\; v = \textit{decode} \;( \textit{retrieve}\; (\rup \backslash s) \; (\inj \; (r\backslash s) \;c\;v)\;) r$ |
975 $ \flex \; r\; id\; (s@[c])\; v = \textit{decode} \;( \textit{retrieve}\; (\rup \backslash s) \; (\inj \; (r\backslash s) \;c\;v)\;) r$ |
981 \end{center} |
976 \end{center} |
982 and using a lemma that |
977 Using a lemma that |
983 \begin{center} |
978 \begin{center} |
984 $\textit{retrieve}\; (\rup \backslash s) \; (\inj \; (r\backslash s) \;c\;v)\; = \textit{retrieve}\; (\rup \backslash s@[c]) \; v\; $ |
979 $\textit{retrieve}\; (\rup \backslash s) \; (\inj \; (r\backslash s) \;c\;v)\; = \textit{retrieve}\; (\rup \backslash s@[c]) \; v\; $ |
985 \end{center} |
980 \end{center} |
986 we get |
981 we get |
987 \begin{center} |
982 \begin{center} |
988 $ \textit{decode} \;( \textit{retrieve}\; (\rup \backslash s) \; (\inj \; (r\backslash s) \;c\;v)\;) r = \textit{decode} \;( \textit{retrieve}\; (\rup \backslash s@[c]) \; v\;) r $ |
983 $ \textit{decode} \;( \textit{retrieve}\; (\rup \backslash s) \; (\inj \; (r\backslash s) \;c\;v)\;) r = \textit{decode} \;( \textit{retrieve}\; (\rup \backslash s@[c]) \; v\;) r $ |
989 \end{center} |
984 \end{center} |
990 and the inductive step is done because |
985 and the inductive step is done because |
991 \begin{center} |
986 \begin{center} |
992 $ \textit{retrieve}\; (\rup \backslash s@[c]) \; \mkeps(r\backslash s) = \bmkeps \;(\rup \backslash s@[c])$ |
987 $ \textit{retrieve}\; (\rup \backslash s@[c]) \; \mkeps(r\backslash s) = \bmkeps \;(\rup \backslash s@[c])$. |
993 \end{center} |
988 \end{center} |
|
989 |
|
990 \noindent |
|
991 To use |
|
992 $ \flex \; r\; id\; s\; v = \textit{decode} \;( \textit{retrieve}\; (\rup \backslash s) \; v \;) r$ |
|
993 for our |
|
994 correctness proof, simply replace the $v$ with |
|
995 $\mkeps\;(r\backslash s)$, and apply the lemma that |
|
996 \begin{center} |
|
997 $ \; \bmkeps \; \rup = (\textit{retrieve} \; \rup \; \mkeps(r))$ |
|
998 \end{center} |
|
999 \noindent |
|
1000 We get the correctness of our bit-coded algorithm: |
|
1001 \begin{center} |
|
1002 $\flex \;r\; id \; s \; (\mkeps \; (r\backslash s)) = \textit{decode} \; (\bmkeps \; \rup\backslash s) \; r$. |
|
1003 \end{center} |
|
1004 \noindent |
|
1005 |
|
1006 |
994 |
1007 |
995 \subsubsection{Using Retrieve Function In a New Setting} |
1008 \subsubsection{Using Retrieve Function In a New Setting} |
996 Ausaf |
1009 Ausaf |
997 and Urban used $\retrieve$ to prove the correctness of bitcoded |
1010 and Urban used $\retrieve$ to prove the correctness of bitcoded |
998 algorithm without simplification. Our purpose of using it, however, |
1011 algorithm without simplification. Our purpose of using it, however, |
1003 a \; v \;=\; \textit{retrieve} \; (\textit{simp}\,a) \; v'.$ |
1016 a \; v \;=\; \textit{retrieve} \; (\textit{simp}\,a) \; v'.$ |
1004 \end{center} |
1017 \end{center} |
1005 The idea is that using $v'$, a simplified version of $v$ that had gone |
1018 The idea is that using $v'$, a simplified version of $v$ that had gone |
1006 through the same simplification step as $\textit{simp}(a)$, we are able |
1019 through the same simplification step as $\textit{simp}(a)$, we are able |
1007 to extract the bitcode that gives the same parsing information as the |
1020 to extract the bitcode that gives the same parsing information as the |
1008 unsimplified one. However, we noticed that constructing such a $v'$ |
1021 unsimplified one. |
1009 from $v$ is not so straightforward. The point of this is that we might |
1022 If we want to use a similar technique as |
1010 be able to finally bridge the gap by proving |
1023 that of the existing proof, |
1011 |
|
1012 \noindent |
|
1013 By using a property of retrieve we have the $\textit{RHS}$ of the above equality is |
|
1014 $decode (retrieve (r^\uparrow \backslash(s @ [c])) v) r$, and this gives the |
|
1015 main lemma result: |
|
1016 |
|
1017 \begin{center} |
|
1018 $ \flex \;r\; id \; (s@[c]) \; v =\textit{decode}(\textit{retrieve} (\rup \backslash (s@[c])) \;v) r$ |
|
1019 \end{center} |
|
1020 |
|
1021 |
|
1022 |
|
1023 |
|
1024 \noindent |
|
1025 To use this lemma result for our |
|
1026 correctness proof, simply replace the $v$ in the |
|
1027 $\textit{RHS}$ of the above equality with |
|
1028 $\mkeps\;(r\backslash (s@[c]))$, and apply the lemma that |
|
1029 |
|
1030 \begin{center} |
|
1031 $\textit{decode} \; \bmkeps \; \rup \; r = \textit{decode} \; (\textit{retrieve} \; \rup \; \mkeps(r)) \;r$ |
|
1032 \end{center} |
|
1033 \noindent |
|
1034 We get the correctness of our bit-coded algorithm: |
|
1035 \begin{center} |
|
1036 $\flex \;r\; id \; s \; (\mkeps \; r\backslash s) = \textit{decode} \; \bmkeps \; \rup\backslash s \; r$ |
|
1037 \end{center} |
|
1038 \noindent |
|
1039 The bridge between the above chain of equalities |
|
1040 is the use of $\retrieve$, |
|
1041 if we want to use a similar technique for the |
|
1042 simplified version of algorithm, |
|
1043 we face the problem that in the above |
1024 we face the problem that in the above |
1044 equalities, |
1025 equalities, |
1045 $\retrieve \; a \; v$ is not always defined. |
1026 $\retrieve \; a \; v$ is not always defined. |
1046 for example, |
1027 for example, |
1047 $\retrieve \; _0(_1a+_0a) \; \Left(\Empty)$ |
1028 $\retrieve \; _0(_1a+_0a) \; \Left(\Empty)$ |