# HG changeset patch # User Chengsong # Date 1665580086 -3600 # Node ID d5e9bcb384ecf54b36f1d1eb25eaa73deb8bbb41 # Parent b0f0d884a547680b9db5ebf84c6e39846d135d24 reorder diff -r b0f0d884a547 -r d5e9bcb384ec ChengsongTanPhdThesis/Chapters/Finite.tex --- a/ChengsongTanPhdThesis/Chapters/Finite.tex Wed Oct 12 14:01:33 2022 +0100 +++ b/ChengsongTanPhdThesis/Chapters/Finite.tex Wed Oct 12 14:08:06 2022 +0100 @@ -785,6 +785,320 @@ $\rder{x}{(\rsimpalts \; rs)} = \rsimpalts \; (\map \; (\rder{x}{\_}) \; rs)$ \end{lemma} \noindent + +\subsubsection{The $RL$ Function: Language Interpretation of $\textit{Rrexp}$s} +Much like the definition of $L$ on plain regular expressions, one could also +define the language interpretation of $\rrexp$s. +\begin{center} + \begin{tabular}{lcl} + $RL \; (\ZERO)$ & $\dn$ & $\phi$\\ + $RL \; (\ONE)$ & $\dn$ & $\{[]\}$\\ + $RL \; (c)$ & $\dn$ & $\{[c]\}$\\ + $RL \; \sum rs$ & $\dn$ & $ \bigcup_{r \in rs} (RL \; r)$\\ + $RL \; (r_1 \cdot r_2)$ & $\dn$ & $ RL \; (r_1) @ RL \; (r_2)$\\ + $RL \; (r^*)$ & $\dn$ & $ (RL(r))^*$ + \end{tabular} +\end{center} +\noindent +The main use of $RL$ is to establish some connections between $\rsimp{}$ +and $\rnullable{}$: +\begin{lemma} + The following properties hold: + \begin{itemize} + \item + If $\rnullable{r}$, then $\rsimp{r} \neq \RZERO$. + \item + $\rnullable{r \backslash s} \quad $ if and only if $\quad \rnullable{\rderssimp{r}{s}}$. + \end{itemize} +\end{lemma} +\begin{proof} + The first part is by induction on $r$. + The second part is true because property + \[ RL \; r = RL \; (\rsimp{r})\] holds. +\end{proof} + +\subsubsection{Simplified $\textit{Rrexp}$s are Good} +We formalise the notion of ``good" regular expressions, +which means regular expressions that +are not fully simplified. For alternative regular expressions that means they +do not contain any nested alternatives like +\[ r_1 + (r_2 + r_3) \], un-removed $\RZERO$s like \[\RZERO + r\] +or duplicate elements in a children regular expression list like \[ \sum [r, r, \ldots]\]: +\begin{center} + \begin{tabular}{@{}lcl@{}} + $\good\; \RZERO$ & $\dn$ & $\textit{false}$\\ + $\good\; \RONE$ & $\dn$ & $\textit{true}$\\ + $\good\; \RCHAR{c}$ & $\dn$ & $\btrue$\\ + $\good\; \RALTS{[]}$ & $\dn$ & $\bfalse$\\ + $\good\; \RALTS{[r]}$ & $\dn$ & $\bfalse$\\ + $\good\; \RALTS{r_1 :: r_2 :: rs}$ & $\dn$ & + $\textit{isDistinct} \; (r_1 :: r_2 :: rs) \;$\\ + & & $\textit{and}\; (\forall r' \in (r_1 :: r_2 :: rs).\; \good \; r'\; \, \textit{and}\; \, \textit{nonAlt}\; r')$\\ + $\good \; \RSEQ{\RZERO}{r}$ & $\dn$ & $\bfalse$\\ + $\good \; \RSEQ{\RONE}{r}$ & $\dn$ & $\bfalse$\\ + $\good \; \RSEQ{r}{\RZERO}$ & $\dn$ & $\bfalse$\\ + $\good \; \RSEQ{r_1}{r_2}$ & $\dn$ & $\good \; r_1 \;\, \textit{and} \;\, \good \; r_2$\\ + $\good \; \RSTAR{r}$ & $\dn$ & $\btrue$\\ + \end{tabular} +\end{center} +\noindent +The predicate $\textit{nonAlt}$ evaluates to true when the regular expression is not an +alternative, and false otherwise. +The $\good$ property is preserved under $\rsimp_{ALTS}$, provided that +its non-empty argument list of expressions are all good themsleves, and $\textit{nonAlt}$, +and unique: +\begin{lemma}\label{rsimpaltsGood} + If $rs \neq []$ and forall $r \in rs. \textit{nonAlt} \; r$ and $\textit{isDistinct} \; rs$, + then $\good \; (\rsimpalts \; rs)$ if and only if forall $r \in rs. \; \good \; r$. +\end{lemma} +\noindent +We also note that +if a regular expression $r$ is good, then $\rflts$ on the singleton +list $[r]$ will not break goodness: +\begin{lemma}\label{flts2} + If $\good \; r$, then forall $r' \in \rflts \; [r]. \; \good \; r'$ and $\textit{nonAlt} \; r'$. +\end{lemma} +\begin{proof} + By an induction on $r$. +\end{proof} +\noindent +The other observation we make about $\rsimp{r}$ is that it never +comes with nested alternatives, which we describe as the $\nonnested$ +property: +\begin{center} + \begin{tabular}{lcl} + $\nonnested \; \, \sum []$ & $\dn$ & $\btrue$\\ + $\nonnested \; \, \sum ((\sum rs_1) :: rs_2)$ & $\dn$ & $\bfalse$\\ + $\nonnested \; \, \sum (r :: rs)$ & $\dn$ & $\nonnested (\sum rs)$\\ + $\nonnested \; \, r $ & $\dn$ & $\btrue$ + \end{tabular} +\end{center} +\noindent +The $\rflts$ function +always opens up nested alternatives, +which enables $\rsimp$ to be non-nested: + +\begin{lemma}\label{nonnestedRsimp} + $\nonnested \; (\rsimp{r})$ +\end{lemma} +\begin{proof} + By an induction on $r$. +\end{proof} +\noindent +With this we could prove that a regular expressions +after simplification and flattening and de-duplication, +will not contain any alternative regular expression directly: +\begin{lemma}\label{nonaltFltsRd} + If $x \in \rdistinct{\rflts\; (\map \; \rsimp{} \; rs)}{\varnothing}$ + then $\textit{nonAlt} \; x$. +\end{lemma} +\begin{proof} + By \ref{nonnestedRsimp}. +\end{proof} +\noindent +The other thing we know is that once $\rsimp{}$ had finished +processing an alternative regular expression, it will not +contain any $\RZERO$s, this is because all the recursive +calls to the simplification on the children regular expressions +make the children good, and $\rflts$ will not take out +any $\RZERO$s out of a good regular expression list, +and $\rdistinct{}$ will not mess with the result. +\begin{lemma}\label{flts3Obv} + The following are true: + \begin{itemize} + \item + If for all $r \in rs. \, \good \; r $ or $r = \RZERO$, + then for all $r \in \rflts\; rs. \, \good \; r$. + \item + If $x \in \rdistinct{\rflts\; (\map \; rsimp{}\; rs)}{\varnothing}$ + and for all $y$ such that $\llbracket y \rrbracket_r$ less than + $\llbracket rs \rrbracket_r + 1$, either + $\good \; (\rsimp{y})$ or $\rsimp{y} = \RZERO$, + then $\good \; x$. + \end{itemize} +\end{lemma} +\begin{proof} + The first part is by induction on $rs$, where the induction + rule is the inductive cases for $\rflts$. + The second part is a corollary from the first part. +\end{proof} + +And this leads to good structural property of $\rsimp{}$, +that after simplification, a regular expression is +either good or $\RZERO$: +\begin{lemma}\label{good1} + For any r-regular expression $r$, $\good \; \rsimp{r}$ or $\rsimp{r} = \RZERO$. +\end{lemma} +\begin{proof} + By an induction on $r$. The inductive measure is the size $\llbracket \rrbracket_r$. + Lemma \ref{rsimpSize} says that + $\llbracket \rsimp{r}\rrbracket_r$ is smaller than or equal to + $\llbracket r \rrbracket_r$. + Therefore, in the $r_1 \cdot r_2$ and $\sum rs$ case, + Inductive hypothesis applies to the children regular expressions + $r_1$, $r_2$, etc. The lemma \ref{flts3Obv}'s precondition is satisfied + by that as well. + The lemmas \ref{nonnestedRsimp} and \ref{nonaltFltsRd} are used + to ensure that goodness is preserved at the topmost level. +\end{proof} +We shall prove that any good regular expression is +a fixed-point for $\rsimp{}$. +First we prove an auxiliary lemma: +\begin{lemma}\label{goodaltsNonalt} + If $\good \; \sum rs$, then $\rflts\; rs = rs$. +\end{lemma} +\begin{proof} + By an induction on $\sum rs$. The inductive rules are the cases + for $\good$. +\end{proof} +\noindent +Now we are ready to prove that good regular expressions are invariant +of $\rsimp{}$ application: +\begin{lemma}\label{test} + If $\good \;r$ then $\rsimp{r} = r$. +\end{lemma} +\begin{proof} + By an induction on the inductive cases of $\good$, using lemmas + \ref{goodaltsNonalt} and \ref{rdistinctOnDistinct}. + The lemma \ref{goodaltsNonalt} is used in the alternative + case where 2 or more elements are present in the list. +\end{proof} +\noindent +Given below is a property involving $\rflts$, $\rdistinct{}{}$, $\rsimp{}$ and $\rsimp_{ALTS}$, +which requires $\ref{good1}$ to go through smoothly. +It says that an application of $\rsimp_{ALTS}$ can be "absorbed", +if it its output is concatenated with a list and then applied to $\rflts$. +\begin{lemma}\label{flattenRsimpalts} + $\rflts \; ( (\rsimp_{ALTS} \; + (\rdistinct{(\rflts \; (\map \; \rsimp{}\; rs))}{\varnothing})) :: + \map \; \rsimp{} \; rs' ) = + \rflts \; ( (\rdistinct{(\rflts \; (\map \; \rsimp{}\; rs))}{\varnothing}) @ ( + \map \; \rsimp{rs'}))$ + + +\end{lemma} +\begin{proof} + By \ref{good1}. +\end{proof} +\noindent + + + + + +We are also ready to prove that $\textit{rsimp}$ is idempotent. +\subsubsection{$\rsimp$ is Idempotent} +The idempotency of $\rsimp$ is very useful in +manipulating regular expression terms into desired +forms so that key steps allowing further rewriting to closed forms +are possible. +\begin{lemma}\label{rsimpIdem} + $\rsimp{r} = \rsimp{\rsimp{r}}$ +\end{lemma} + +\begin{proof} + By \ref{test} and \ref{good1}. +\end{proof} +\noindent +This property means we do not have to repeatedly +apply simplification in each step, which justifies +our definition of $\blexersimp$. + + +On the other hand, we could repeat the same $\rsimp{}$ applications +on regular expressions as many times as we want, if we have at least +one simplification applied to it, and apply it wherever we would like to: +\begin{corollary}\label{headOneMoreSimp} + The following properties hold, directly from \ref{rsimpIdem}: + + \begin{itemize} + \item + $\map \; \rsimp{(r :: rs)} = \map \; \rsimp{} \; (\rsimp{r} :: rs)$ + \item + $\rsimp{(\RALTS{rs})} = \rsimp{(\RALTS{\map \; \rsimp{} \; rs})}$ + \end{itemize} +\end{corollary} +\noindent +This will be useful in later closed form proof's rewriting steps. +Similarly, we point out the following useful facts below: +\begin{lemma} + The following equalities hold if $r = \rsimp{r'}$ for some $r'$: + \begin{itemize} + \item + If $r = \sum rs$ then $\rsimpalts \; rs = \sum rs$. + \item + If $r = \sum rs$ then $\rdistinct{rs}{\varnothing} = rs$. + \item + $\rsimpalts \; (\rdistinct{\rflts \; [r]}{\varnothing}) = r$. + \end{itemize} +\end{lemma} +\begin{proof} + By application of lemmas \ref{rsimpIdem} and \ref{good1}. +\end{proof} + +\noindent +With the idempotency of $\rsimp{}$ and its corollaries, +we can start proving some key equalities leading to the +closed forms. +Now presented are a few equivalent terms under $\rsimp{}$. +We use $r_1 \sequal r_2 $ here to denote $\rsimp{r_1} = \rsimp{r_2}$. +\begin{lemma} + \begin{itemize} + The following equivalence hold: + \item + $\rsimpalts \; (\RZERO :: rs) \sequal \rsimpalts\; rs$ + \item + $\rsimpalts \; rs \sequal \rsimpalts (\map \; \rsimp{} \; rs)$ + \item + $\RALTS{\RALTS{rs}} \sequal \RALTS{rs}$ + \item + $\sum ((\sum rs_a) :: rs_b) \sequal \sum rs_a @ rs_b$ + \item + $\RALTS{rs} = \RALTS{\map \; \rsimp{} \; rs}$ +\end{itemize} +\end{lemma} +\begin{proof} + By induction on the lists involved. +\end{proof} +\noindent +The above allows us to prove +two similar equalities (which are a bit more involved). +It says that we could flatten out the elements +before simplification and still get the same result. +\begin{lemma}\label{simpFlatten3} + One can flatten the inside $\sum$ of a $\sum$ if it is being + simplified. Concretely, + \begin{itemize} + \item + If for all $r \in rs, rs', rs''$, we have $\good \; r $ + or $r = \RZERO$, then $\sum (rs' @ rs @ rs'') \sequal + \sum (rs' @ [\sum rs] @ rs'')$ holds. As a corollary, + \item + $\sum (rs' @ [\sum rs] @ rs'') \sequal \sum (rs' @ rs @ rs'')$ + \end{itemize} +\end{lemma} +\begin{proof} + By rewriting steps involving the use of \ref{test} and \ref{rdistinctConcatGeneral}. + The second sub-lemma is a corollary of the previous. +\end{proof} +%Rewriting steps not put in--too long and complicated------------------------------- +\begin{comment} + \begin{center} + $\rsimp{\sum (rs' @ rs @ rs'')} \stackrel{def of bsimp}{=}$ \\ + $\rsimpalts \; (\rdistinct{\rflts \; ((\map \; \rsimp{}\; rs') @ (\map \; \rsimp{} \; rs ) @ (\map \; \rsimp{} \; rs''))}{\varnothing})$ \\ + $\stackrel{by \ref{test}}{=} + \rsimpalts \; (\rdistinct{(\rflts \; rs' @ \rflts \; rs @ \rflts \; rs'')}{ + \varnothing})$\\ + $\stackrel{by \ref{rdistinctConcatGeneral}}{=} + \rsimpalts \; (\rdistinct{\rflts \; rs'}{\varnothing} @ \rdistinct{( + \rflts\; rs @ \rflts \; rs'')}{\rflts \; rs'})$\\ + + \end{center} +\end{comment} +%Rewriting steps not put in--too long and complicated------------------------------- +\noindent + + We need more equalities like the above to enable a closed form, for which we need to introduce a few rewrite relations to help @@ -1629,317 +1943,6 @@ By \ref{rsimpMonoLemmas}. \end{proof} -\subsubsection{The $RL$ Function: Language Interpretation of $\textit{Rrexp}$s} -Much like the definition of $L$ on plain regular expressions, one could also -define the language interpretation of $\rrexp$s. -\begin{center} - \begin{tabular}{lcl} - $RL \; (\ZERO)$ & $\dn$ & $\phi$\\ - $RL \; (\ONE)$ & $\dn$ & $\{[]\}$\\ - $RL \; (c)$ & $\dn$ & $\{[c]\}$\\ - $RL \; \sum rs$ & $\dn$ & $ \bigcup_{r \in rs} (RL \; r)$\\ - $RL \; (r_1 \cdot r_2)$ & $\dn$ & $ RL \; (r_1) @ RL \; (r_2)$\\ - $RL \; (r^*)$ & $\dn$ & $ (RL(r))^*$ - \end{tabular} -\end{center} -\noindent -The main use of $RL$ is to establish some connections between $\rsimp{}$ -and $\rnullable{}$: -\begin{lemma} - The following properties hold: - \begin{itemize} - \item - If $\rnullable{r}$, then $\rsimp{r} \neq \RZERO$. - \item - $\rnullable{r \backslash s} \quad $ if and only if $\quad \rnullable{\rderssimp{r}{s}}$. - \end{itemize} -\end{lemma} -\begin{proof} - The first part is by induction on $r$. - The second part is true because property - \[ RL \; r = RL \; (\rsimp{r})\] holds. -\end{proof} - -\subsubsection{Simplified $\textit{Rrexp}$s are Good} -We formalise the notion of ``good" regular expressions, -which means regular expressions that -are not fully simplified. For alternative regular expressions that means they -do not contain any nested alternatives like -\[ r_1 + (r_2 + r_3) \], un-removed $\RZERO$s like \[\RZERO + r\] -or duplicate elements in a children regular expression list like \[ \sum [r, r, \ldots]\]: -\begin{center} - \begin{tabular}{@{}lcl@{}} - $\good\; \RZERO$ & $\dn$ & $\textit{false}$\\ - $\good\; \RONE$ & $\dn$ & $\textit{true}$\\ - $\good\; \RCHAR{c}$ & $\dn$ & $\btrue$\\ - $\good\; \RALTS{[]}$ & $\dn$ & $\bfalse$\\ - $\good\; \RALTS{[r]}$ & $\dn$ & $\bfalse$\\ - $\good\; \RALTS{r_1 :: r_2 :: rs}$ & $\dn$ & - $\textit{isDistinct} \; (r_1 :: r_2 :: rs) \;$\\ - & & $\textit{and}\; (\forall r' \in (r_1 :: r_2 :: rs).\; \good \; r'\; \, \textit{and}\; \, \textit{nonAlt}\; r')$\\ - $\good \; \RSEQ{\RZERO}{r}$ & $\dn$ & $\bfalse$\\ - $\good \; \RSEQ{\RONE}{r}$ & $\dn$ & $\bfalse$\\ - $\good \; \RSEQ{r}{\RZERO}$ & $\dn$ & $\bfalse$\\ - $\good \; \RSEQ{r_1}{r_2}$ & $\dn$ & $\good \; r_1 \;\, \textit{and} \;\, \good \; r_2$\\ - $\good \; \RSTAR{r}$ & $\dn$ & $\btrue$\\ - \end{tabular} -\end{center} -\noindent -The predicate $\textit{nonAlt}$ evaluates to true when the regular expression is not an -alternative, and false otherwise. -The $\good$ property is preserved under $\rsimp_{ALTS}$, provided that -its non-empty argument list of expressions are all good themsleves, and $\textit{nonAlt}$, -and unique: -\begin{lemma}\label{rsimpaltsGood} - If $rs \neq []$ and forall $r \in rs. \textit{nonAlt} \; r$ and $\textit{isDistinct} \; rs$, - then $\good \; (\rsimpalts \; rs)$ if and only if forall $r \in rs. \; \good \; r$. -\end{lemma} -\noindent -We also note that -if a regular expression $r$ is good, then $\rflts$ on the singleton -list $[r]$ will not break goodness: -\begin{lemma}\label{flts2} - If $\good \; r$, then forall $r' \in \rflts \; [r]. \; \good \; r'$ and $\textit{nonAlt} \; r'$. -\end{lemma} -\begin{proof} - By an induction on $r$. -\end{proof} -\noindent -The other observation we make about $\rsimp{r}$ is that it never -comes with nested alternatives, which we describe as the $\nonnested$ -property: -\begin{center} - \begin{tabular}{lcl} - $\nonnested \; \, \sum []$ & $\dn$ & $\btrue$\\ - $\nonnested \; \, \sum ((\sum rs_1) :: rs_2)$ & $\dn$ & $\bfalse$\\ - $\nonnested \; \, \sum (r :: rs)$ & $\dn$ & $\nonnested (\sum rs)$\\ - $\nonnested \; \, r $ & $\dn$ & $\btrue$ - \end{tabular} -\end{center} -\noindent -The $\rflts$ function -always opens up nested alternatives, -which enables $\rsimp$ to be non-nested: - -\begin{lemma}\label{nonnestedRsimp} - $\nonnested \; (\rsimp{r})$ -\end{lemma} -\begin{proof} - By an induction on $r$. -\end{proof} -\noindent -With this we could prove that a regular expressions -after simplification and flattening and de-duplication, -will not contain any alternative regular expression directly: -\begin{lemma}\label{nonaltFltsRd} - If $x \in \rdistinct{\rflts\; (\map \; \rsimp{} \; rs)}{\varnothing}$ - then $\textit{nonAlt} \; x$. -\end{lemma} -\begin{proof} - By \ref{nonnestedRsimp}. -\end{proof} -\noindent -The other thing we know is that once $\rsimp{}$ had finished -processing an alternative regular expression, it will not -contain any $\RZERO$s, this is because all the recursive -calls to the simplification on the children regular expressions -make the children good, and $\rflts$ will not take out -any $\RZERO$s out of a good regular expression list, -and $\rdistinct{}$ will not mess with the result. -\begin{lemma}\label{flts3Obv} - The following are true: - \begin{itemize} - \item - If for all $r \in rs. \, \good \; r $ or $r = \RZERO$, - then for all $r \in \rflts\; rs. \, \good \; r$. - \item - If $x \in \rdistinct{\rflts\; (\map \; rsimp{}\; rs)}{\varnothing}$ - and for all $y$ such that $\llbracket y \rrbracket_r$ less than - $\llbracket rs \rrbracket_r + 1$, either - $\good \; (\rsimp{y})$ or $\rsimp{y} = \RZERO$, - then $\good \; x$. - \end{itemize} -\end{lemma} -\begin{proof} - The first part is by induction on $rs$, where the induction - rule is the inductive cases for $\rflts$. - The second part is a corollary from the first part. -\end{proof} - -And this leads to good structural property of $\rsimp{}$, -that after simplification, a regular expression is -either good or $\RZERO$: -\begin{lemma}\label{good1} - For any r-regular expression $r$, $\good \; \rsimp{r}$ or $\rsimp{r} = \RZERO$. -\end{lemma} -\begin{proof} - By an induction on $r$. The inductive measure is the size $\llbracket \rrbracket_r$. - Lemma \ref{rsimpSize} says that - $\llbracket \rsimp{r}\rrbracket_r$ is smaller than or equal to - $\llbracket r \rrbracket_r$. - Therefore, in the $r_1 \cdot r_2$ and $\sum rs$ case, - Inductive hypothesis applies to the children regular expressions - $r_1$, $r_2$, etc. The lemma \ref{flts3Obv}'s precondition is satisfied - by that as well. - The lemmas \ref{nonnestedRsimp} and \ref{nonaltFltsRd} are used - to ensure that goodness is preserved at the topmost level. -\end{proof} -We shall prove that any good regular expression is -a fixed-point for $\rsimp{}$. -First we prove an auxiliary lemma: -\begin{lemma}\label{goodaltsNonalt} - If $\good \; \sum rs$, then $\rflts\; rs = rs$. -\end{lemma} -\begin{proof} - By an induction on $\sum rs$. The inductive rules are the cases - for $\good$. -\end{proof} -\noindent -Now we are ready to prove that good regular expressions are invariant -of $\rsimp{}$ application: -\begin{lemma}\label{test} - If $\good \;r$ then $\rsimp{r} = r$. -\end{lemma} -\begin{proof} - By an induction on the inductive cases of $\good$, using lemmas - \ref{goodaltsNonalt} and \ref{rdistinctOnDistinct}. - The lemma \ref{goodaltsNonalt} is used in the alternative - case where 2 or more elements are present in the list. -\end{proof} -\noindent -Given below is a property involving $\rflts$, $\rdistinct{}{}$, $\rsimp{}$ and $\rsimp_{ALTS}$, -which requires $\ref{good1}$ to go through smoothly. -It says that an application of $\rsimp_{ALTS}$ can be "absorbed", -if it its output is concatenated with a list and then applied to $\rflts$. -\begin{lemma}\label{flattenRsimpalts} - $\rflts \; ( (\rsimp_{ALTS} \; - (\rdistinct{(\rflts \; (\map \; \rsimp{}\; rs))}{\varnothing})) :: - \map \; \rsimp{} \; rs' ) = - \rflts \; ( (\rdistinct{(\rflts \; (\map \; \rsimp{}\; rs))}{\varnothing}) @ ( - \map \; \rsimp{rs'}))$ - - -\end{lemma} -\begin{proof} - By \ref{good1}. -\end{proof} -\noindent - - - - - -We are also ready to prove that $\textit{rsimp}$ is idempotent. -\subsubsection{$\rsimp$ is Idempotent} -The idempotency of $\rsimp$ is very useful in -manipulating regular expression terms into desired -forms so that key steps allowing further rewriting to closed forms -are possible. -\begin{lemma}\label{rsimpIdem} - $\rsimp{r} = \rsimp{\rsimp{r}}$ -\end{lemma} - -\begin{proof} - By \ref{test} and \ref{good1}. -\end{proof} -\noindent -This property means we do not have to repeatedly -apply simplification in each step, which justifies -our definition of $\blexersimp$. - - -On the other hand, we could repeat the same $\rsimp{}$ applications -on regular expressions as many times as we want, if we have at least -one simplification applied to it, and apply it wherever we would like to: -\begin{corollary}\label{headOneMoreSimp} - The following properties hold, directly from \ref{rsimpIdem}: - - \begin{itemize} - \item - $\map \; \rsimp{(r :: rs)} = \map \; \rsimp{} \; (\rsimp{r} :: rs)$ - \item - $\rsimp{(\RALTS{rs})} = \rsimp{(\RALTS{\map \; \rsimp{} \; rs})}$ - \end{itemize} -\end{corollary} -\noindent -This will be useful in later closed form proof's rewriting steps. -Similarly, we point out the following useful facts below: -\begin{lemma} - The following equalities hold if $r = \rsimp{r'}$ for some $r'$: - \begin{itemize} - \item - If $r = \sum rs$ then $\rsimpalts \; rs = \sum rs$. - \item - If $r = \sum rs$ then $\rdistinct{rs}{\varnothing} = rs$. - \item - $\rsimpalts \; (\rdistinct{\rflts \; [r]}{\varnothing}) = r$. - \end{itemize} -\end{lemma} -\begin{proof} - By application of lemmas \ref{rsimpIdem} and \ref{good1}. -\end{proof} - -\noindent -With the idempotency of $\rsimp{}$ and its corollaries, -we can start proving some key equalities leading to the -closed forms. -Now presented are a few equivalent terms under $\rsimp{}$. -We use $r_1 \sequal r_2 $ here to denote $\rsimp{r_1} = \rsimp{r_2}$. -\begin{lemma} - \begin{itemize} - The following equivalence hold: - \item - $\rsimpalts \; (\RZERO :: rs) \sequal \rsimpalts\; rs$ - \item - $\rsimpalts \; rs \sequal \rsimpalts (\map \; \rsimp{} \; rs)$ - \item - $\RALTS{\RALTS{rs}} \sequal \RALTS{rs}$ - \item - $\sum ((\sum rs_a) :: rs_b) \sequal \sum rs_a @ rs_b$ - \item - $\RALTS{rs} = \RALTS{\map \; \rsimp{} \; rs}$ -\end{itemize} -\end{lemma} -\begin{proof} - By induction on the lists involved. -\end{proof} -\noindent -The above allows us to prove -two similar equalities (which are a bit more involved). -It says that we could flatten out the elements -before simplification and still get the same result. -\begin{lemma}\label{simpFlatten3} - One can flatten the inside $\sum$ of a $\sum$ if it is being - simplified. Concretely, - \begin{itemize} - \item - If for all $r \in rs, rs', rs''$, we have $\good \; r $ - or $r = \RZERO$, then $\sum (rs' @ rs @ rs'') \sequal - \sum (rs' @ [\sum rs] @ rs'')$ holds. As a corollary, - \item - $\sum (rs' @ [\sum rs] @ rs'') \sequal \sum (rs' @ rs @ rs'')$ - \end{itemize} -\end{lemma} -\begin{proof} - By rewriting steps involving the use of \ref{test} and \ref{rdistinctConcatGeneral}. - The second sub-lemma is a corollary of the previous. -\end{proof} -%Rewriting steps not put in--too long and complicated------------------------------- -\begin{comment} - \begin{center} - $\rsimp{\sum (rs' @ rs @ rs'')} \stackrel{def of bsimp}{=}$ \\ - $\rsimpalts \; (\rdistinct{\rflts \; ((\map \; \rsimp{}\; rs') @ (\map \; \rsimp{} \; rs ) @ (\map \; \rsimp{} \; rs''))}{\varnothing})$ \\ - $\stackrel{by \ref{test}}{=} - \rsimpalts \; (\rdistinct{(\rflts \; rs' @ \rflts \; rs @ \rflts \; rs'')}{ - \varnothing})$\\ - $\stackrel{by \ref{rdistinctConcatGeneral}}{=} - \rsimpalts \; (\rdistinct{\rflts \; rs'}{\varnothing} @ \rdistinct{( - \rflts\; rs @ \rflts \; rs'')}{\rflts \; rs'})$\\ - - \end{center} -\end{comment} -%Rewriting steps not put in--too long and complicated------------------------------- -\noindent \subsection{Estimating the Closed Forms' sizes} We now summarize the closed forms below: \begin{itemize}