178 result as the one without simplification, then we are done. |
178 result as the one without simplification, then we are done. |
179 Unfortunately that part requires more effort, because simplification does not |
179 Unfortunately that part requires more effort, because simplification does not |
180 only.need to \emph{not} change the language, but also not change |
180 only.need to \emph{not} change the language, but also not change |
181 the value (computed result). |
181 the value (computed result). |
182 |
182 |
183 \bigskip\noindent\rule[1.5ex]{\linewidth}{5pt} |
183 |
184 Do you want to keep this? You essentially want to say that the old |
184 |
185 method used retrieve, which unfortunately cannot be adopted to |
185 For this we have started with looking at the original proof that |
186 the simplification rules. You could just say that and give an example. |
186 established that the bitsequence algorithm produces the same result as |
187 However you have to think about how you give the example....nobody knows |
187 the algorithm not using bitsequences. Formally this proof estabilshed |
188 about AZERO etc yet. Maybe it might be better to use normal regexes |
188 |
189 like $a + aa$, but annotate bitsequences as subscript like $_1(_0a + _1aa)$. |
|
190 |
|
191 \bigskip\noindent\rule[1.5ex]{\linewidth}{5pt} |
|
192 REPLY:\\ |
|
193 Yes, I am essentially saying that the old method |
|
194 cannot be adopted without adjustments. |
|
195 But this does not mean we should skip |
|
196 the proof of the bit-coded algorithm |
|
197 as it is still the main direction we are looking into |
|
198 to prove things. We are trying to modify |
|
199 the old proof to suit our needs, but not give |
|
200 up it totally, that is why i believe the old |
|
201 proof is fundamental in understanding |
|
202 what we are doing in the past 6 months. |
|
203 |
|
204 \bigskip\noindent\rule[1.5ex]{\linewidth}{5pt} |
|
205 |
|
206 The correctness proof of |
|
207 \begin{center} |
189 \begin{center} |
208 $\blexer \; r^\uparrow s = \lexer \;r \;s$ |
190 $\blexer \; r^\uparrow s = \lexer \;r \;s$ |
209 \end{center} |
191 \end{center} |
210 \noindent |
192 |
211 might provide us insight into proving |
193 \noindent |
212 \begin{center} |
194 The proof used two ''tricks", One is that it defined |
213 $\blexer \; r^\uparrow \;s = \blexers \; r^\uparrow \;s$ |
195 a $\flex$-function |
214 \end{center} |
196 |
215 \noindent |
|
216 (that is also |
|
217 why we say the new proof builds on the older one). |
|
218 The proof defined the function $\flex$ as another way of |
|
219 expressing the $\lexer$ function: |
|
220 \begin{center} |
|
221 $\lexer \;r\; s = \flex \;\textit{id} \; r\;s \;(\mkeps \; r\backslash s)$ |
|
222 \end{center}. |
|
223 \noindent |
|
224 (proof for the above equality will be explained later) |
|
225 The definition of $flex$ is as follows: |
|
226 \begin{center} |
197 \begin{center} |
227 \begin{tabular}{lcl} |
198 \begin{tabular}{lcl} |
228 $\textit{flex} \;r\; f\; (c\!::\!s) $ & $\dn$ & $\textit{flex} \; (r\backslash c) \;(\lambda v. f (inj \; r \; c \; v)) \;s$ \\ |
199 $\textit{flex} \;r\; f\; (c\!::\!s) $ & $\dn$ & $\textit{flex} \; (r\backslash c) \;(\lambda v. f (inj \; r \; c \; v)) \;s$ \\ |
229 $\textit{flex} \;r\; f\; [\,] $ & $\dn$ & $f$ |
200 $\textit{flex} \;r\; f\; [\,] $ & $\dn$ & $f$ |
230 \end{tabular} |
201 \end{tabular} |
231 \end{center} |
202 \end{center} |
232 \noindent |
203 |
233 here $\flex$ essentially does lexing by |
204 \noindent |
|
205 and then proved for the right-hand side in \eqref{lexer} |
|
206 |
|
207 \begin{center} |
|
208 $\lexer \;r\; s = \flex \;\textit{id} \; r\;s \;(\mkeps \; r\backslash s)$ |
|
209 \end{center}. |
|
210 |
|
211 |
|
212 \noindent\rule[1.5ex]{\linewidth}{1pt} |
|
213 |
|
214 \noindent |
|
215 The $\flex$-function essentially does lexing by |
234 stacking up injection functions while doing derivatives, |
216 stacking up injection functions while doing derivatives, |
235 explicitly showing the order of characters being |
217 explicitly showing the order of characters being |
236 injected back in each step. |
218 injected back in each step. |
237 With $\flex$ we can write $\lexer$ this way: |
219 With $\flex$ we can write $\lexer$ this way: |
238 \begin{center} |
220 \begin{center} |