equal
deleted
inserted
replaced
368 (_{[]}r^*))$ |
368 (_{[]}r^*))$ |
369 \end{tabular} |
369 \end{tabular} |
370 \end{center} |
370 \end{center} |
371 \noindent |
371 \noindent |
372 where we omit the definition of $\textit{rnullable}$. |
372 where we omit the definition of $\textit{rnullable}$. |
|
373 The generalisation from derivative w.r.t to character to |
|
374 derivative w.r.t string is given as |
|
375 \begin{center} |
|
376 \begin{tabular}{lcl} |
|
377 $r \backslash_{rs} []$ & $\dn$ & $r$\\ |
|
378 $r \backslash_{rs} c::s$ & $\dn$ & $(r\backslash_r c) \backslash_{rs} s$ |
|
379 \end{tabular} |
|
380 \end{center} |
373 |
381 |
374 The function $\distinctBy$ for r-regular expressions does not need |
382 The function $\distinctBy$ for r-regular expressions does not need |
375 a function checking equivalence because |
383 a function checking equivalence because |
376 there are no bit annotations. |
384 there are no bit annotations. |
377 Therefore we have |
385 Therefore we have |
776 By lemma \ref{distinctRdistinctAppend}. |
784 By lemma \ref{distinctRdistinctAppend}. |
777 \end{proof} |
785 \end{proof} |
778 |
786 |
779 \subsubsection{The Properties of $\textit{Rflts}$} |
787 \subsubsection{The Properties of $\textit{Rflts}$} |
780 We give in this subsection some properties |
788 We give in this subsection some properties |
781 involving $\backslash_r$, $\backslash_{rsimp}$, $\textit{rflts}$ and |
789 involving $\backslash_r$, $\backslash_{rsimps}$, $\textit{rflts}$ and |
782 $\textit{rsimp}_{ALTS} $, together with any non-trivial lemmas that lead to them. |
790 $\textit{rsimp}_{ALTS} $, together with any non-trivial lemmas that lead to them. |
783 These will be helpful in later closed form proofs, when |
791 These will be helpful in later closed form proofs, when |
784 we want to transform derivative terms which have |
792 we want to transform derivative terms which have |
785 %the ways in which multiple functions involving |
793 %the ways in which multiple functions involving |
786 %those are composed together |
794 %those are composed together |
1428 And this unlocks more equivalent terms: |
1436 And this unlocks more equivalent terms: |
1429 \begin{lemma}\label{Simpders} |
1437 \begin{lemma}\label{Simpders} |
1430 As corollaries of \ref{insideSimpRemoval}, we have |
1438 As corollaries of \ref{insideSimpRemoval}, we have |
1431 \begin{itemize} |
1439 \begin{itemize} |
1432 \item |
1440 \item |
1433 If $s \neq []$ then $\rderssimp{r}{s} = \rsimp{(\rders \; r \; s)}$. |
1441 If $s \neq []$ then $\rderssimp{r}{s} = \rsimp{( r \backslash_{rs} s)}$. |
1434 \item |
1442 \item |
1435 $\rsimpalts \; (\map \; (\_ \backslash_r x) \; |
1443 $\rsimpalts \; (\map \; (\_ \backslash_r x) \; |
1436 (\rdistinct{rs}{\varnothing})) \sequal |
1444 (\rdistinct{rs}{\varnothing})) \sequal |
1437 \rsimpalts \; (\rDistinct \; |
1445 \rsimpalts \; (\rDistinct \; |
1438 (\map \; (\_ \backslash_r x) rs) \;\varnothing )$ |
1446 (\map \; (\_ \backslash_r x) rs) \;\varnothing )$ |
1842 \begin{center} |
1850 \begin{center} |
1843 \begin{tabular}{lcl} |
1851 \begin{tabular}{lcl} |
1844 $\starupdate \; c \; r \; [] $ & $\dn$ & $[]$\\ |
1852 $\starupdate \; c \; r \; [] $ & $\dn$ & $[]$\\ |
1845 $\starupdate \; c \; r \; (s :: Ss)$ & $\dn$ & \\ |
1853 $\starupdate \; c \; r \; (s :: Ss)$ & $\dn$ & \\ |
1846 & & $\textit{if} \; |
1854 & & $\textit{if} \; |
1847 (\rnullable \; (\rders \; r \; s))$ \\ |
1855 (\rnullable \; (r \backslash_{rs} s))$ \\ |
1848 & & $\textit{then} \;\; (s @ [c]) :: [c] :: ( |
1856 & & $\textit{then} \;\; (s @ [c]) :: [c] :: ( |
1849 \starupdate \; c \; r \; Ss)$ \\ |
1857 \starupdate \; c \; r \; Ss)$ \\ |
1850 & & $\textit{else} \;\; (s @ [c]) :: ( |
1858 & & $\textit{else} \;\; (s @ [c]) :: ( |
1851 \starupdate \; c \; r \; Ss)$ |
1859 \starupdate \; c \; r \; Ss)$ |
1852 \end{tabular} |
1860 \end{tabular} |
2032 then flatten it out, |
2040 then flatten it out, |
2033 we obtain a list |
2041 we obtain a list |
2034 of the shape $\sum_{s' \in sS} (r\backslash_r s') \cdot r^*$, |
2042 of the shape $\sum_{s' \in sS} (r\backslash_r s') \cdot r^*$, |
2035 where $sS = \starupdates \; s \; r \; [[c]]$. Namely, |
2043 where $sS = \starupdates \; s \; r \; [[c]]$. Namely, |
2036 \begin{center} |
2044 \begin{center} |
2037 $\hflataux{(\rders{( (\rder{c}{r_0})\cdot(r_0^*))}{s})} = |
2045 $\hflataux{(( (\rder{c}{r_0})\cdot(r_0^*))\backslash_{rs} s)} = |
2038 \map \; (\lambda s_1. (r_0 \backslash_r s_1) \cdot (r_0^*)) \; |
2046 \map \; (\lambda s_1. (r_0 \backslash_r s_1) \cdot (r_0^*)) \; |
2039 (\starupdates \; s \; r_0 \; [[c]])$ |
2047 (\starupdates \; s \; r_0 \; [[c]])$ |
2040 \end{center} |
2048 \end{center} |
2041 holds. |
2049 holds. |
2042 \end{lemma} |
2050 \end{lemma} |
2093 $\textit{rsimp} \; (r^* \backslash_r (c::s)) |
2101 $\textit{rsimp} \; (r^* \backslash_r (c::s)) |
2094 \sequal |
2102 \sequal |
2095 \sum \; ( ( \sum (\lambda s. (r\backslash_r s) \cdot r^*) \; ( |
2103 \sum \; ( ( \sum (\lambda s. (r\backslash_r s) \cdot r^*) \; ( |
2096 \starupdates \; s \; r \; [ c::[]] ) ) )$ |
2104 \starupdates \; s \; r \; [ c::[]] ) ) )$ |
2097 \item |
2105 \item |
2098 $r \backslash_{rsimp} (c::s) = \textit{rsimp} \; ( ( |
2106 $r \backslash_{rsimps} (c::s) = \textit{rsimp} \; ( ( |
2099 \sum ( (\map \; (\lambda s_1. (r\backslash s_1) \; r^*) \; |
2107 \sum ( (\map \; (\lambda s_1. (r\backslash s_1) \; r^*) \; |
2100 (\starupdates \;s \; r \; [ c::[] ])))))$ |
2108 (\starupdates \;s \; r \; [ c::[] ])))))$ |
2101 \item |
2109 \item |
2102 $\sum ( (\map \; (\lambda s. (r\backslash s) \; r^*) \; Ss)) |
2110 $\sum ( (\map \; (\lambda s. (r\backslash s) \; r^*) \; Ss)) |
2103 \sequal |
2111 \sequal |
2111 $( ( \sum ( ( \map \ (\lambda s. \;\; |
2119 $( ( \sum ( ( \map \ (\lambda s. \;\; |
2112 (\textit{rsimp} \; (r \backslash_r s)) \cdot r^*) \; (\starupdates \; |
2120 (\textit{rsimp} \; (r \backslash_r s)) \cdot r^*) \; (\starupdates \; |
2113 s \; r \; [ c::[] ])))))$\\ |
2121 s \; r \; [ c::[] ])))))$\\ |
2114 $\sequal$\\ |
2122 $\sequal$\\ |
2115 $( ( \sum ( ( \map \ (\lambda s. \;\; |
2123 $( ( \sum ( ( \map \ (\lambda s. \;\; |
2116 ( r \backslash_{rsimp} s)) \cdot r^*) \; (\starupdates \; |
2124 ( r \backslash_{rsimps} s)) \cdot r^*) \; (\starupdates \; |
2117 s \; r \; [ c::[] ]))))$\\ |
2125 s \; r \; [ c::[] ]))))$\\ |
2118 \end{itemize} |
2126 \end{itemize} |
2119 \end{lemma} |
2127 \end{lemma} |
2120 \begin{proof} |
2128 \begin{proof} |
2121 Part 1 leads to part 2. |
2129 Part 1 leads to part 2. |
2481 When the string $s$ is not empty, we can reason as follows |
2489 When the string $s$ is not empty, we can reason as follows |
2482 % |
2490 % |
2483 \begin{center} |
2491 \begin{center} |
2484 \begin{tabular}{lcll} |
2492 \begin{tabular}{lcll} |
2485 & & $ \llbracket \rderssimp{r_1\cdot r_2 }{s} \rrbracket_r $\\ |
2493 & & $ \llbracket \rderssimp{r_1\cdot r_2 }{s} \rrbracket_r $\\ |
2486 & $ = $ & $\llbracket \rsimp{(\sum(r_1 \backslash_{rsimp} s \cdot r_2 \; \; :: \; \; |
2494 & $ = $ & $\llbracket \rsimp{(\sum(r_1 \backslash_{rsimps} s \cdot r_2 \; \; :: \; \; |
2487 \map \; (r_2\backslash_{rsimp} \_)\; (\vsuf{s}{r})))} \rrbracket_r $ & (1) \\ |
2495 \map \; (r_2\backslash_{rsimps} \_)\; (\vsuf{s}{r})))} \rrbracket_r $ & (1) \\ |
2488 & $\leq$ & $\llbracket \rdistinct{(r_1 \backslash_{rsimp} s \cdot r_2 \; \; :: \; \; |
2496 & $\leq$ & $\llbracket \rdistinct{(r_1 \backslash_{rsimps} s \cdot r_2 \; \; :: \; \; |
2489 \map \; (r_2\backslash_{rsimp} \_)\; (\vsuf{s}{r}))}{\varnothing} \rrbracket_r + 1$ & (2) \\ |
2497 \map \; (r_2\backslash_{rsimps} \_)\; (\vsuf{s}{r}))}{\varnothing} \rrbracket_r + 1$ & (2) \\ |
2490 & $\leq$ & $2 + N_1 + \rsize{r_2} + (N_2 * (card\;(\sizeNregex \; N_2)))$ & (3)\\ |
2498 & $\leq$ & $2 + N_1 + \rsize{r_2} + (N_2 * (card\;(\sizeNregex \; N_2)))$ & (3)\\ |
2491 \end{tabular} |
2499 \end{tabular} |
2492 \end{center} |
2500 \end{center} |
2493 \noindent |
2501 \noindent |
2494 (1) is by theorem \ref{seqClosedForm}. |
2502 (1) is by theorem \ref{seqClosedForm}. |
2512 Let $n_r = \llbracket r^* \rrbracket_r$. |
2520 Let $n_r = \llbracket r^* \rrbracket_r$. |
2513 When $s = c :: cs$ is not empty, |
2521 When $s = c :: cs$ is not empty, |
2514 \begin{center} |
2522 \begin{center} |
2515 \begin{tabular}{lcll} |
2523 \begin{tabular}{lcll} |
2516 & & $ \llbracket \rderssimp{r^* }{c::cs} \rrbracket_r $\\ |
2524 & & $ \llbracket \rderssimp{r^* }{c::cs} \rrbracket_r $\\ |
2517 & $ = $ & $\llbracket \rsimp{(\sum (\map \; (\lambda s. (r \backslash_{rsimp} s) \cdot r^*) \; (\starupdates\; |
2525 & $ = $ & $\llbracket \rsimp{(\sum (\map \; (\lambda s. (r \backslash_{rsimps} s) \cdot r^*) \; (\starupdates\; |
2518 cs \; r \; [[c]] )) )} \rrbracket_r $ & (5) \\ |
2526 cs \; r \; [[c]] )) )} \rrbracket_r $ & (5) \\ |
2519 & $\leq$ & $\llbracket |
2527 & $\leq$ & $\llbracket |
2520 \rdistinct{ |
2528 \rdistinct{ |
2521 (\map \; |
2529 (\map \; |
2522 (\lambda s. (r \backslash_{rsimp} s) \cdot r^*) \; |
2530 (\lambda s. (r \backslash_{rsimps} s) \cdot r^*) \; |
2523 (\starupdates\; cs \; r \; [[c]] ) |
2531 (\starupdates\; cs \; r \; [[c]] ) |
2524 )} |
2532 )} |
2525 {\varnothing} \rrbracket_r + 1$ & (6) \\ |
2533 {\varnothing} \rrbracket_r + 1$ & (6) \\ |
2526 & $\leq$ & $1 + (\textit{card} (\sizeNregex \; (N + n_r))) |
2534 & $\leq$ & $1 + (\textit{card} (\sizeNregex \; (N + n_r))) |
2527 * (1 + (N + n_r)) $ & (7)\\ |
2535 * (1 + (N + n_r)) $ & (7)\\ |
2545 is equivalent to $\exists N. \forall r \in (\map \; (\_ \backslash_r s) \; rs). \rsize{r} \leq N$. |
2553 is equivalent to $\exists N. \forall r \in (\map \; (\_ \backslash_r s) \; rs). \rsize{r} \leq N$. |
2546 In the case when $s = c::cs$, we have |
2554 In the case when $s = c::cs$, we have |
2547 \begin{center} |
2555 \begin{center} |
2548 \begin{tabular}{lcll} |
2556 \begin{tabular}{lcll} |
2549 & & $ \llbracket \rderssimp{\sum rs }{c::cs} \rrbracket_r $\\ |
2557 & & $ \llbracket \rderssimp{\sum rs }{c::cs} \rrbracket_r $\\ |
2550 & $ = $ & $\llbracket \rsimp{(\sum (\map \; (\_ \backslash_{rsimp} s) \; rs) )} \rrbracket_r $ & (9) \\ |
2558 & $ = $ & $\llbracket \rsimp{(\sum (\map \; (\_ \backslash_{rsimps} s) \; rs) )} \rrbracket_r $ & (9) \\ |
2551 & $\leq$ & $\llbracket (\sum (\map \; (\_ \backslash_{rsimp} s) \; rs) ) \rrbracket_r $ & (10) \\ |
2559 & $\leq$ & $\llbracket (\sum (\map \; (\_ \backslash_{rsimps} s) \; rs) ) \rrbracket_r $ & (10) \\ |
2552 & $\leq$ & $1 + N * (length \; rs) $ & (11)\\ |
2560 & $\leq$ & $1 + N * (length \; rs) $ & (11)\\ |
2553 \end{tabular} |
2561 \end{tabular} |
2554 \end{center} |
2562 \end{center} |
2555 \noindent |
2563 \noindent |
2556 (9) is by theorem \ref{altsClosedForm}, (10) by lemma \ref{rsimpMono} and (11) by inductive hypothesis. |
2564 (9) is by theorem \ref{altsClosedForm}, (10) by lemma \ref{rsimpMono} and (11) by inductive hypothesis. |