217 |
217 |
218 %---------------------------------------------------------------------------------------- |
218 %---------------------------------------------------------------------------------------- |
219 % SECTION rewrite relation |
219 % SECTION rewrite relation |
220 %---------------------------------------------------------------------------------------- |
220 %---------------------------------------------------------------------------------------- |
221 \section{The Rewriting Relation $\rrewrite$($\rightsquigarrow$)} |
221 \section{The Rewriting Relation $\rrewrite$($\rightsquigarrow$)} |
222 The overall idea for the correctness |
222 In the $\blexer$'s correctness proof, we |
223 \begin{conjecture} |
223 did not directly derive the fact that $\blexer$ gives out the POSIX value, |
224 $\blexersimp \; r \; s = \blexer \; r\; s$ |
224 but first prove that $\blexer$ is linked with $\lexer$. |
225 \end{conjecture} |
225 Then we re-use |
|
226 the correctness of $\lexer$. |
|
227 Here we follow suit by first proving that |
|
228 $\blexersimp \; r \; s $ |
|
229 produces the same output as $\blexer \; r\; s$, |
|
230 and then putting it together with |
|
231 $\blexer$'s correctness result |
|
232 ($(r, s) \rightarrow v \implies \blexer \; r \;s = v$) |
|
233 to obtain half of the correctness property (the other half |
|
234 being when $s$ is not $L \; r$ which is routine to establish) |
|
235 \begin{center} |
|
236 $(r, s) \rightarrow v \implies \blexersimp \; r \; s = v$ |
|
237 \end{center} |
|
238 \noindent |
|
239 because it makes the proof simpler |
|
240 The overall idea for the correctness of our simplified bitcoded lexer |
|
241 \noindent |
226 is that the $\textit{bsimp}$ will not change the regular expressions so much that |
242 is that the $\textit{bsimp}$ will not change the regular expressions so much that |
227 it becomes impossible to extract the $\POSIX$ values. |
243 it becomes impossible to extract the $\POSIX$ values. |
228 To capture this "similarity" between unsimplified regular expressions and simplified ones, |
244 To capture this "similarity" between unsimplified regular expressions and simplified ones, |
229 we devise the rewriting relation $\rrewrite$, written infix as $\rightsquigarrow$: |
245 we devise the rewriting relation $\rrewrite$, written infix as $\rightsquigarrow$: |
230 |
246 |
454 \noindent |
470 \noindent |
455 And now we are ready to prove the key property that if you |
471 And now we are ready to prove the key property that if you |
456 have two regular expressions, one rewritable in many steps to the other, |
472 have two regular expressions, one rewritable in many steps to the other, |
457 and one of them is $\bnullable$, then they will both yield the same bits under $\bmkeps$: |
473 and one of them is $\bnullable$, then they will both yield the same bits under $\bmkeps$: |
458 \begin{lemma} |
474 \begin{lemma} |
459 $(r \stackrel{*}{\rightsquigarrow} r'\land \bnullable \; r_1) \implies \bmkeps \; r = \bmkeps \; r'$ |
475 $\text{If} \;\; r \stackrel{*}{\rightsquigarrow} r' \;\; \text{and} \;\; \bnullable \; r_1 \;\; \text{then} \;\; \bmkeps \; r = \bmkeps \; r'$ |
460 \end{lemma} |
476 \end{lemma} |
461 \begin{proof} |
477 \begin{proof} |
462 By rule induction of $\stackrel{*}{\rightsquigarrow} $, using \ref{rewriteBmkepsAux} and $\ref{rewritesBnullable}$. |
478 By rule induction of $\stackrel{*}{\rightsquigarrow} $, using \ref{rewriteBmkepsAux} and $\ref{rewritesBnullable}$. |
463 \end{proof} |
479 \end{proof} |
464 \noindent |
480 \noindent |
514 which we know is correct value as $\blexer$ is correct: |
530 which we know is correct value as $\blexer$ is correct: |
515 \begin{theorem} |
531 \begin{theorem} |
516 $\blexer \; r \; s = \blexersimp{r}{s}$ |
532 $\blexer \; r \; s = \blexersimp{r}{s}$ |
517 \end{theorem} |
533 \end{theorem} |
518 \noindent |
534 \noindent |
|
535 \begin{proof} |
|
536 One can rewrite in many steps from the original lexer's derivative regular expressions to the |
|
537 lexer with simplification applied: |
|
538 $a \backslash s \stackrel{*}{\rightsquigarrow} \bderssimp{a}{s} $. |
|
539 If two regular expressions are rewritable, then they produce the same bits. |
|
540 Under the condition that $ r_1$ is nullable, we have |
|
541 $\text{If} \;\; r \stackrel{*}{\rightsquigarrow} r', \;\;\text{then} \;\; \bmkeps \; r = \bmkeps \; r'$. |
|
542 This proves the \emph{if} (interesting) branch of |
|
543 $\blexer \; r \; s = \blexersimp{r}{s}$. |
|
544 |
|
545 \end{proof} |
|
546 \noindent |
|
547 As a corollary, |
|
548 we link this result with the lemma we proved earlier that |
|
549 \begin{center} |
|
550 $(r, s) \rightarrow v \implies \blexer \; r \; s = v$ |
|
551 \end{center} |
|
552 and obtain the corollary that the bit-coded lexer with simplification is |
|
553 indeed correctly outputting POSIX lexing result, if such a result exists. |
|
554 \begin{corollary} |
|
555 $(r, s) \rightarrow v \implies \blexersimp{r}{s}$ |
|
556 \end{corollary} |
519 |
557 |
520 \subsection{Comments on the Proof Techniques Used} |
558 \subsection{Comments on the Proof Techniques Used} |
521 The non-trivial part of proving the correctness of the algorithm with simplification |
559 The non-trivial part of proving the correctness of the algorithm with simplification |
522 compared with not having simplification is that we can no longer use the argument |
560 compared with not having simplification is that we can no longer use the argument |
523 in \cref{flex_retrieve}. |
561 in \cref{flex_retrieve}. |