equal
deleted
inserted
replaced
35 \newcommand{\ONE}{\mbox{\bf 1}} |
35 \newcommand{\ONE}{\mbox{\bf 1}} |
36 \def\bders{\textit{bders}} |
36 \def\bders{\textit{bders}} |
37 \def\lexer{\mathit{lexer}} |
37 \def\lexer{\mathit{lexer}} |
38 \def\blexer{\textit{blexer}} |
38 \def\blexer{\textit{blexer}} |
39 \def\blexers{\mathit{blexer\_simp}} |
39 \def\blexers{\mathit{blexer\_simp}} |
|
40 \def\simp{\mathit{simp}} |
40 \def\mkeps{\mathit{mkeps}} |
41 \def\mkeps{\mathit{mkeps}} |
41 \def\bmkeps{\textit{bmkeps}} |
42 \def\bmkeps{\textit{bmkeps}} |
42 \def\inj{\mathit{inj}} |
43 \def\inj{\mathit{inj}} |
43 \def\Empty{\mathit{Empty}} |
44 \def\Empty{\mathit{Empty}} |
44 \def\Left{\mathit{Left}} |
45 \def\Left{\mathit{Left}} |
248 for example, |
249 for example, |
249 $\retrieve \; \AALTS(Z, \AONE(S), \AONE(S)) \; \Left(\Empty)$ |
250 $\retrieve \; \AALTS(Z, \AONE(S), \AONE(S)) \; \Left(\Empty)$ |
250 is defined, but not $\retrieve \; \AONE(\Z\S) \; \Left(\Empty)$, |
251 is defined, but not $\retrieve \; \AONE(\Z\S) \; \Left(\Empty)$, |
251 though we can extract the same POSIX |
252 though we can extract the same POSIX |
252 bits from the two annotated regular expressions. |
253 bits from the two annotated regular expressions. |
|
254 The latter might occur when we try to retrieve from |
|
255 a simplified regular expression using the same value |
|
256 as the unsimplified one. |
|
257 This is because $\Left(\Empty)$ corresponds to |
|
258 the regular expression structure $\AALTS$ instead of |
|
259 $\AONE$, this v |
253 That means, if we |
260 That means, if we |
254 want to prove that |
261 want to prove that |
255 \begin{center} |
262 \begin{center} |
256 $\textit{decode} \; \bmkeps \; \rup\backslash s \; r = \textit{decode} \; \bmkeps \; \rup\backslash_{simp} s \; r$ |
263 $\textit{decode} \; \bmkeps \; \rup\backslash s \; r = \textit{decode} \; \bmkeps \; \rup\backslash_{simp} s \; r$ |
257 \end{center} |
264 \end{center} |
263 $\retrieve \; \rup\backslash_{simp} s \; \mkeps(r\backslash s)=\textit{retrieve} \; \rup\backslash s \; \mkeps(r\backslash s)$ |
270 $\retrieve \; \rup\backslash_{simp} s \; \mkeps(r\backslash s)=\textit{retrieve} \; \rup\backslash s \; \mkeps(r\backslash s)$ |
264 \end{center} |
271 \end{center} |
265 \noindent |
272 \noindent |
266 we would need to rectify the value $\mkeps(r\backslash s)$ into something simpler |
273 we would need to rectify the value $\mkeps(r\backslash s)$ into something simpler |
267 to make the retrieve function defined.\\ |
274 to make the retrieve function defined.\\ |
|
275 One way to do this is to prove the following: |
|
276 \begin{center} |
|
277 $\retrieve \; \rup\backslash_{simp} s \; \mkeps(\simp(r\backslash s))=\textit{retrieve} \; \rup\backslash s \; \mkeps(r\backslash s)$ |
|
278 \end{center} |
|
279 \noindent |
268 %HERE CONSTRUCTION SITE |
280 %HERE CONSTRUCTION SITE |
269 The vsimp function, defined as follows |
281 The vsimp function, defined as follows |
270 tries to simplify the value in lockstep with |
282 tries to simplify the value in lockstep with |
271 regular expression:\\ |
283 regular expression:\\ |
272 |
284 |