18 This chapter |
18 This chapter |
19 is the point from which novel contributions of this PhD project are introduced |
19 is the point from which novel contributions of this PhD project are introduced |
20 in detail. |
20 in detail. |
21 The material in the |
21 The material in the |
22 previous |
22 previous |
23 chapters is necessary |
23 chapters is necessary for this thesis, |
24 material for setting the scene of the formal proof we |
24 because it provides the context for why we need a new framework for |
25 are about to describe. |
25 the proof of $\blexersimp$. |
26 |
26 %material for setting the scene of the formal proof we |
27 The fundamental reason is we cannot extend the correctness proof of theorem 4, |
27 %are about to describe. |
|
28 The fundamental reason is we cannot extend the correctness proof of theorem 4 |
28 because lemma 13 does not hold anymore when simplifications are involved. |
29 because lemma 13 does not hold anymore when simplifications are involved. |
29 |
30 \marginpar{\em rephrased things so they make better sense.} |
30 The proof details are necessary materials for this thesis |
31 %The proof details are necessary materials for this thesis |
31 because it provides necessary context to explain why we need a |
32 %because it provides necessary context to explain why we need a |
32 new framework for the proof of $\blexersimp$, which involves |
33 %new framework for the proof of $\blexersimp$, which involves |
33 simplifications that cause structural changes to the regular expression. |
34 %simplifications that cause structural changes to the regular expression. |
34 A new formal proof of the correctness of $\blexersimp$, where the |
35 %A new formal proof of the correctness of $\blexersimp$, where the |
35 proof of $\blexer$ |
36 %proof of $\blexer$ |
36 is not applicatble in the sense that we cannot straightforwardly extend the |
37 %is not applicatble in the sense that we cannot straightforwardly extend the |
37 proof of theorem \ref{blexerCorrect} because lemma \ref{retrieveStepwise} does |
38 %proof of theorem \ref{blexerCorrect} because lemma \ref{retrieveStepwise} does |
38 not hold anymore. |
39 %not hold anymore. |
39 %This is because the structural induction on the stepwise correctness |
40 %This is because the structural induction on the stepwise correctness |
40 %of $\inj$ breaks due to each pair of $r_i$ and $v_i$ described |
41 %of $\inj$ breaks due to each pair of $r_i$ and $v_i$ described |
41 %in chapter \ref{Inj} and \ref{Bitcoded1} no longer correspond to |
42 %in chapter \ref{Inj} and \ref{Bitcoded1} no longer correspond to |
42 %each other. |
43 %each other. |
43 %In this chapter we introduce simplifications |
44 %In this chapter we introduce simplifications |
51 In particular, the correctness theorem |
52 In particular, the correctness theorem |
52 of the un-optimised bit-coded lexer $\blexer$ in |
53 of the un-optimised bit-coded lexer $\blexer$ in |
53 chapter \ref{Bitcoded1} formalised by Ausaf et al. |
54 chapter \ref{Bitcoded1} formalised by Ausaf et al. |
54 relies crucially on lemma \ref{retrieveStepwise} that says |
55 relies crucially on lemma \ref{retrieveStepwise} that says |
55 any value can be retrieved in a stepwise manner, namely: |
56 any value can be retrieved in a stepwise manner, namely: |
56 \begin{center}%eqref: this proposition needs to be referred |
57 \begin{equation}\label{eq:stepwise}%eqref: this proposition needs to be referred |
57 $\vdash v : (r\backslash c) \implies \retrieve \; (r \backslash c) \; v= \retrieve \; r \; (\inj \; r\; c\; v)$ |
58 \vdash v : (r\backslash c) \implies \retrieve \; (r \backslash c) \; v= \retrieve \; r \; (\inj \; r\; c\; v) |
58 \end{center} |
59 \end{equation} |
59 This no longer holds once we introduce simplifications. |
60 %This no longer holds once we introduce simplifications. |
60 Simplifications are necessary to control the size of derivatives |
61 Simplifications are necessary to control the size of derivatives, |
|
62 but they also destroy the structures of the regular expressions |
|
63 such that \ref{eq:stepwise} does not hold. |
61 |
64 |
62 |
65 |
63 We want to prove the correctness of $\blexersimp$ which integrates |
66 We want to prove the correctness of $\blexersimp$ which integrates |
64 $\textit{bsimp}$ by applying it after each call to the derivative: |
67 $\textit{bsimp}$ by applying it after each call to the derivative: |
65 \begin{center} |
68 \begin{center} |