lexing: comparison ChengsongTanPhdThesis/Chapters/Finite.tex

equal deleted inserted replaced

-:3ea82d8f0aa4
+:0f00d440f484
 (in file BasicIdentities.thy) for the exact definition.
 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.
 \begin{lemma}
+	The following equalities hold:
 	\begin{itemize}
 		\item
 $\asize{\bsimp{a}} = \rsize{\rsimp{\rerase{a}}}$
 \item
 $\asize{\bderssimp{r}{s}} =  \rsize{\rderssimp{\rerase{r}}{s}}$
 %-----------------------------------
 %	SECTION ?
 %-----------------------------------
-\section{Roadmap to a Finiteness Proof}
+\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$.
-The way we do it is by two steps:
+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}$}
+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.
-		The functions $f$ and $g$ are usually from $\flts$ $\distinctBy$ and other appearing in $\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$.
 	\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. The closed form $f\; (g\; (\sum rs)) $ is controlled
+		reduce the size of a regular expression, not adding to it.
-		by the size of $rs'$, where every element in $rs'$ is distinct, and each element can be described by som e inductive sub-structures (for example when $r = r_1 \cdot r_2$ then $rs'$ will be solely comprised of $r_1 \backslash s'$ and $r_2 \backslash s''$, $s'$ and $s''$ being sub-strings of $s$), which will have a numeric uppder bound according to inductive hypothesis, which controls $r \backslash s$.
 \end{itemize}
-\section{Closed Forms}
+\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$.
 \subsection{Basic Properties needed for Closed Forms}
 \subsubsection{$\textit{rdistinct}$'s Deduplicates Successfully}
 The $\textit{rdistinct}$ function, as its name suggests, will
-remove duplicates according to the accumulator
+remove duplicates in an \emph{r}$\textit{rexp}$ list,
+according to the accumulator
 and leave only one of each different element in a list:
 \begin{lemma}
 	The function $\textit{rdistinct}$ satisfies the following
 	properties:
 	\begin{itemize}
 for any prefix of an input list, in other words, when can
 we ``push out" the arguments of $\rdistinct{\_}{\_}$:
 \begin{lemma}
 	If $rs_1$'s elements are all unique, and not appearing in the accumulator $acc$,
 	then it can be taken out and left untouched in the output:
-	\[\textit{rdistinct}\;  rs_1 @ rsa\;\, acc
+	\[\textit{rdistinct}\;  (rs_1 @ rsa)\;\, acc
-	= rs_1@(\textit{rdistinct} rsa \; (acc \cup rs_1)\]
+	= rs_1@(\textit{rdistinct} rsa \; (acc \cup rs_1))\]
 \end{lemma}
 \begin{proof}
 By an induction on $rs_1$, where $rsa$ and $acc$ are allowed to be arbitrary.
 \end{proof}
-\subsubsection{The properties of $\backslash_r$, $\backslash_{rsimp}$, $\textit{Rflts}$ and $\textit{Rsimp}_{ALTS}$}
+\subsubsection{The Properties of $\backslash_r$, $\backslash_{rsimp}$, $\textit{Rflts}$ and $\textit{Rsimp}_{ALTS}$}
-We give in this subsection some properties of how $\backslash_r$, $\backslash_{rsimp}$, $\textit{Rflts}$ and $\textit{Rsimp}_{ALTS} $ interact with each other and  with $@$, the concatenation operator.
+We give in this subsection some properties of how $\backslash_r$, $\backslash_{rsimp}$, $\textit{Rflts}$ and $\textit{Rsimp}_{ALTS} $ interact with each other and with $@$, the concatenation operator.
 These will be helpful in later closed form proofs, when
 we want to transform the ways in which multiple functions involving
 those are composed together
 in interleaving derivative and  simplification steps.
 \end{lemma}
 Fortunately this is provable by induction on the list $rs$
+\section{Estimating the Closed Forms' sizes}
+		The closed form $f\; (g\; (\sum rs)) $ is controlled
+		by the size of $rs'$, where every element in $rs'$ is distinct, and each element can be described by som e inductive sub-structures (for example when $r = r_1 \cdot r_2$ then $rs'$ will be solely comprised of $r_1 \backslash s'$ and $r_2 \backslash s''$, $s'$ and $s''$ being sub-strings of $s$), which will have a numeric uppder bound according to inductive hypothesis, which controls $r \backslash s$.
 %-----------------------------------
 %	SECTION 2
 %-----------------------------------
 \begin{theorem}

changeset 553	0f00d440f484
parent 543	b2bea5968b89
child 554	15d182ffbc76