diff -r fa92124d1fb7 -r b306628a0eab ChengsongTanPhdThesis/Chapters/Finite.tex --- a/ChengsongTanPhdThesis/Chapters/Finite.tex Fri Sep 02 19:35:55 2022 +0100 +++ b/ChengsongTanPhdThesis/Chapters/Finite.tex Sat Sep 03 00:14:20 2022 +0100 @@ -354,27 +354,53 @@ and the flatten function for $\rrexp$s: \begin{center} \begin{tabular}{@{}lcl@{}} - $\textit{rflts} \; (_{bs}\sum \textit{as}) :: \textit{as'}$ & $\dn$ & $(\textit{map} \; - (\textit{fuse}\;bs)\; \textit{as}) \; @ \; \textit{rflts} \; as' $ \\ + $\textit{rflts} \; (\sum \textit{as}) :: \textit{as'}$ & $\dn$ & $as \; @ \; \textit{rflts} \; as' $ \\ $\textit{rflts} \; \ZERO :: as'$ & $\dn$ & $ \textit{rflts} \; \textit{as'} $ \\ $\textit{rflts} \; a :: as'$ & $\dn$ & $a :: \textit{rflts} \; \textit{as'}$ \quad(otherwise) \end{tabular} \end{center} \noindent - one can chain together all the other modules -of $\bsimp{\_}$ (removing the functionalities related to bit-sequences) -and get $\textit{rsimp}$ and $\rderssimp{\_}{\_}$. +such as $\rsimpalts$: +\begin{center} + \begin{tabular}{@{}lcl@{}} + $\rsimpalts \;\; nil$ & $\dn$ & $\RZERO$\\ + $\rsimpalts \;\; r::nil$ & $\dn$ & $r$\\ + $\rsimpalts \;\; rs$ & $\dn$ & $\sum rs$\\ +\end{tabular} +\end{center} +\noindent +and $\rsimpseq$: +\begin{center} + \begin{tabular}{@{}lcl@{}} + $\rsimpseq \;\; \RZERO \; \_ $ & $=$ & $\RZERO$\\ + $\rsimpseq \;\; \_ \; \RZERO $ & $=$ & $\RZERO$\\ + $\rsimpseq \;\; \RONE \cdot r_2$ & $\dn$ & $r_2$\\ + $\rsimpseq \;\; r_1 r_2$ & $\dn$ & $r_1 \cdot r_2$\\ +\end{tabular} +\end{center} +and get $\textit{rsimp}$ and $\rderssimp{\_}{\_}$: \begin{center} \begin{tabular}{@{}lcl@{}} - $\textit{rsimp} \; (_{bs}a_1\cdot a_2)$ & $\dn$ & $ \textit{rsimp}_{ASEQ} \; bs \;(\textit{rsimp} \; a_1) \; (\textit{rsimp} \; a_2) $ \\ - $\textit{rsimp} \; (_{bs}\sum \textit{as})$ & $\dn$ & $\textit{rsimp}_{ALTS} \; \textit{bs} \; (\textit{rdistinct} \; ( \textit{rflts} ( \textit{map} \; rsimp \; as)) \; \rerases \; \varnothing) $ \\ - $\textit{rsimp} \; a$ & $\dn$ & $\textit{a} \qquad \textit{otherwise}$ + $\textit{rsimp} \; (r_1\cdot r_2)$ & $\dn$ & $ \textit{rsimp}_{SEQ} \; bs \;(\textit{rsimp} \; r_1) \; (\textit{rsimp} \; r_2) $ \\ + $\textit{rsimp} \; (_{bs}\sum \textit{rs})$ & $\dn$ & $\textit{rsimp}_{ALTS} \; \textit{bs} \; (\textit{rdistinct} \; ( \textit{rflts} ( \textit{map} \; rsimp \; rs)) \; \rerases \; \varnothing) $ \\ + $\textit{rsimp} \; r$ & $\dn$ & $\textit{r} \qquad \textit{otherwise}$ \end{tabular} \end{center} -We omit these functions, as they are routine. Please refer to the formalisation -(in file BasicIdentities.thy) for the exact definition. +\begin{center} + \begin{tabular}{@{}lcl@{}} + $r\backslash_{rsimp} \, c$ & $\dn$ & $\rsimp \; (r\backslash_r \, c)$ + \end{tabular} +\end{center} + +\begin{center} + \begin{tabular}{@{}lcl@{}} +$r \backslash_{rsimps} (c\!::\!s) $ & $\dn$ & $(r \backslash_{rsimp}\, c) \backslash_{rsimps}\, s$ \\ +$r \backslash_{rsimps} [\,] $ & $\dn$ & $r$ + \end{tabular} +\end{center} +\noindent With $\rrexp$ the size caclulation of annotated regular expressions' simplification and derivatives can be done by the size of their unlifted counterpart with the unlifted version of simplification and derivatives applied. @@ -384,14 +410,24 @@ \item $\asize{\bsimp{a}} = \rsize{\rsimp{\rerase{a}}}$ \item - $\asize{\bderssimp{r}{s}} = \rsize{\rderssimp{\rerase{r}}{s}}$ + $\asize{\bderssimp{a}{s}} = \rsize{\rderssimp{\rerase{a}}{s}}$ \end{itemize} \end{lemma} \noindent +With lemma \ref{sizeRelations}, +a bound on $\rsize{\rderssimp{\rerase{a}}{s}}$ +\[ + \llbracket \rderssimp{a}{s} \rrbracket_r \leq N_r +\] +\noindent +would apply to $\asize{\bderssimp{a}{s}}$ as well. +\[ + \llbracket a \backslash_{bsimps} s \rrbracket \leq N_r. +\] In the following content, we will focus on $\rrexp$'s size bound. -We will piece together this bound and show the same bound for annotated regular -expressions in the end. -Unless stated otherwise in this chapter all $\textit{rexp}$s without +Whatever bounds we proved for $ \rsize{\rderssimp{\rerase{r}}{s}}$ +will automatically apply to $\asize{\bderssimp{r}{s}}$.\\ +Unless stated otherwise in this chapter all regular expressions without bitcodes are seen as $\rrexp$s. We also use $r_1 + r_2$ and $\RALTS{[r_1, r_2]}$ interchageably as the former suits people's intuitive way of stating a binary alternative @@ -400,57 +436,46 @@ %----------------------------------- -% SECTION ? +% SUB SECTION ROADMAP RREXP BOUND %----------------------------------- -\subsection{Finiteness Proof Using $\rrexp$s} -Now that we have defined the $\rrexp$ datatype, and proven that its size changes -w.r.t derivatives and simplifications mirrors precisely those of annotated regular expressions, -we aim to bound the size of $r \backslash s$ for any $\rrexp$ $r$. -Once we have a bound like: -\[ - \llbracket r \backslash_{rsimp} s \rrbracket_r \leq N_r -\] -\noindent -we could easily extend that to -\[ - \llbracket a \backslash_{bsimps} s \rrbracket \leq N_r. -\] -\subsection{Roadmap to a Bound for $\textit{Rrexp}$} +%\subsection{Roadmap to a Bound for $\textit{Rrexp}$} -The way we obtain the bound for $\rrexp$s is by two steps: -\begin{itemize} - \item - First, we rewrite $r\backslash s$ into something else that is easier - to bound. This step is especially important for the inductive case - $r_1 \cdot r_2$ and $r^*$, where the derivative can grow and bloat in a wild way, - but after simplification they will always be equal or smaller to a form consisting of an alternative - list of regular expressions $f \; (g\; (\sum rs))$ with some functions applied to it, where each element will be distinct after the function application. - \item - Then, for such a sum list of regular expressions $f\; (g\; (\sum rs))$, we can control its size - by estimation, since $\distinctBy$ and $\flts$ are well-behaved and working together would only - reduce the size of a regular expression, not adding to it. -\end{itemize} - -\section{Step One: Closed Forms} -We transform the function application $\rderssimp{r}{s}$ -into an equivalent -form $f\; (g \; (\sum rs))$. -The functions $f$ and $g$ can be anything from $\flts$, $\distinctBy$ and other helper functions from $\bsimp{\_}$. -This way we get a different but equivalent way of expressing : $r\backslash s = f \; (g\; (\sum rs))$, we call the -right hand side the "closed form" of $r\backslash s$. - -\begin{quote}\it - Claim: For regular expressions $r_1 \cdot r_2$, we claim that - \begin{center} - $ \rderssimp{r_1 \cdot r_2}{s} = - \rsimp{(\sum (r_1 \backslash s \cdot r_2 ) \; :: \;(\map \; \rderssimp{r2}{\_} \;(\vsuf{s}{r_1})))}$ - \end{center} -\end{quote} -\noindent -We explain in detail how we reached those claims. +%The way we obtain the bound for $\rrexp$s is by two steps: +%\begin{itemize} +% \item +% First, we rewrite $r\backslash s$ into something else that is easier +% to bound. This step is especially important for the inductive case +% $r_1 \cdot r_2$ and $r^*$, where the derivative can grow and bloat in a wild way, +% but after simplification they will always be equal or smaller to a form consisting of an alternative +% list of regular expressions $f \; (g\; (\sum rs))$ with some functions applied to it, where each element will be distinct after the function application. +% \item +% Then, for such a sum list of regular expressions $f\; (g\; (\sum rs))$, we can control its size +% by estimation, since $\distinctBy$ and $\flts$ are well-behaved and working together would only +% reduce the size of a regular expression, not adding to it. +%\end{itemize} +% +%\section{Step One: Closed Forms} +%We transform the function application $\rderssimp{r}{s}$ +%into an equivalent +%form $f\; (g \; (\sum rs))$. +%The functions $f$ and $g$ can be anything from $\flts$, $\distinctBy$ and other helper functions from $\bsimp{\_}$. +%This way we get a different but equivalent way of expressing : $r\backslash s = f \; (g\; (\sum rs))$, we call the +%right hand side the "closed form" of $r\backslash s$. +% +%\begin{quote}\it +% Claim: For regular expressions $r_1 \cdot r_2$, we claim that +% \begin{center} +% $ \rderssimp{r_1 \cdot r_2}{s} = +% \rsimp{(\sum (r_1 \backslash s \cdot r_2 ) \; :: \;(\map \; \rderssimp{r2}{\_} \;(\vsuf{s}{r_1})))}$ +% \end{center} +%\end{quote} +%\noindent +%We explain in detail how we reached those claims. \subsection{Basic Properties needed for Closed Forms} - +The next steps involves getting a closed form for +$\rderssimp{r}{s}$ and then obtaining +an estimate for the closed form. \subsubsection{$\textit{rdistinct}$'s Deduplicates Successfully} The $\textit{rdistinct}$ function, as its name suggests, will remove duplicates in an \emph{r}$\textit{rexp}$ list,