198 which exist for partial derivatives. However, if we introduce them in our |
198 which exist for partial derivatives. However, if we introduce them in our |
199 setting we would lose the POSIX property of our calculated values. We leave better |
199 setting we would lose the POSIX property of our calculated values. We leave better |
200 bounds for future work.\\[-6.5mm] |
200 bounds for future work.\\[-6.5mm] |
201 |
201 |
202 |
202 |
203 %---------------------------------------------------------------------------------------- |
203 |
204 % SECTION 2 |
204 %----------------------------------- |
|
205 % SECTION ? |
|
206 %----------------------------------- |
|
207 \section{preparatory properties for getting a finiteness bound} |
|
208 Before we get to the proof that says the intermediate result of our lexer will |
|
209 remain finitely bounded, which is an important efficiency/liveness guarantee, |
|
210 we shall first develop a few preparatory properties and definitions to |
|
211 make the process of proving that a breeze. |
|
212 |
|
213 We define rewriting relations for $\rrexp$s, which allows us to do the |
|
214 same trick as we did for the correctness proof, |
|
215 but this time we will have stronger equalities established. |
|
216 \subsection{"hrewrite" relation} |
|
217 List of simplifications for regular expressions simplification without bitcodes: |
|
218 \ |
|
219 |
|
220 |
|
221 |
|
222 |
|
223 %---------------------------------------------------------------------------------------- |
|
224 % SECTION ?? |
205 %---------------------------------------------------------------------------------------- |
225 %---------------------------------------------------------------------------------------- |
206 |
226 |
207 \section{"Closed Forms" of regular expressions' derivatives w.r.t strings} |
227 \section{"Closed Forms" of regular expressions' derivatives w.r.t strings} |
208 To embark on getting the "closed forms" of regexes, we first |
228 To embark on getting the "closed forms" of regexes, we first |
209 define a few auxiliary definitions to make expressing them smoothly. |
229 define a few auxiliary definitions to make expressing them smoothly. |