306 The reason why we use $\rerases$ instead of $\erase$ is that |
306 The reason why we use $\rerases$ instead of $\erase$ is that |
307 it keeps the structures of alternative |
307 it keeps the structures of alternative |
308 annotated regular expressions |
308 annotated regular expressions |
309 whereas $\erase$ would turn it back into a binary structure. |
309 whereas $\erase$ would turn it back into a binary structure. |
310 Not having to mess with the structure |
310 Not having to mess with the structure |
311 greatly simplifies the finiteness proof in chapter \ref{Finite}. |
311 greatly simplifies the finiteness proof in chapter |
|
312 \ref{Finite} (we will follow up with more details there). |
312 We give the definitions of $\rerases$ here together with |
313 We give the definitions of $\rerases$ here together with |
313 the new datatype used by $\rerases$ (as our plain |
314 the new datatype used by $\rerases$ (as our plain |
314 regular expression datatype does not allow non-binary alternatives), |
315 regular expression datatype does not allow non-binary alternatives). |
315 and explain in detail |
|
316 why we want it in the next chapter. |
|
317 For the moment the reader can just think of |
316 For the moment the reader can just think of |
318 $\rerases$ as $\erase$ and $\rrexp$ as plain regular expressions. |
317 $\rerases$ as $\erase$ and $\rrexp$ as plain regular expressions. |
319 \[ \rrexp ::= \RZERO \mid \RONE |
318 \begin{figure}[H] |
|
319 \begin{center} |
|
320 $\rrexp ::= \RZERO \mid \RONE |
320 \mid \RCHAR{c} |
321 \mid \RCHAR{c} |
321 \mid \RSEQ{r_1}{r_2} |
322 \mid \RSEQ{r_1}{r_2} |
322 \mid \RALTS{rs} |
323 \mid \RALTS{rs} |
323 \mid \RSTAR{r} |
324 \mid \RSTAR{r} $ |
324 \] |
325 \end{center} |
|
326 \caption{$\rrexp$: plain regular expressions, but with $\sum$ alternative |
|
327 constructor}\label{rrexpDef} |
|
328 \end{figure} |
325 The notation of $\rerases$ also follows that of $\erase$, |
329 The notation of $\rerases$ also follows that of $\erase$, |
326 which is a postfix operator written as a subscript, |
330 which is a postfix operator written as a subscript, |
327 except that it has an \emph{r} attached to it to distinguish against $\erase$: |
331 except that it has an \emph{r} attached to it to distinguish against $\erase$: |
328 \begin{center} |
332 \begin{center} |
329 \begin{tabular}{lcl} |
333 \begin{tabular}{lcl} |