lexing: comparison ChengsongTanPhdThesis/Chapters/Finite.tex

equal deleted inserted replaced

-:d5e9bcb384ec
+:233cf2b97d1a
 \label{Finite}
 %  In Chapter 4 \ref{Chapter4} we give the second guarantee
 %of our bitcoded algorithm, that is a finite bound on the size of any
 %regex's derivatives.
-\begin{figure}
-\begin{center}
+In this chapter we give a guarantee in terms of size of derivatives:
-	\begin{tabular}{ccc}
-		$\llbracket _{bs}\ONE \rrbracket$ & $\dn$ & $1$\\
-		$\llbracket \ZERO \rrbracket$ & $\dn$ & $1$ \\
-		$\llbracket _{bs} r_1 \cdot r_2 \rrbracket$ & $\dn$ & $\llbracket r_1 \rrbracket + \llbracket r_2 \rrbracket + 1$\\
-		$\llbracket _{bs}\mathbf{c} \rrbracket $ & $\dn$ & $1$\\
-		$\llbracket _{bs}\sum as \rrbracket $ & $\dn$ & $\map \; (\llbracket \_ \rrbracket)\; as   + 1$\\
-		$\llbracket _{bs} a^* \rrbracket $ & $\dn$ & $\llbracket a \rrbracket + 1$.
-	\end{tabular}
-\end{center}
-\caption{The size function of bitcoded regular expressions}\label{brexpSize}
-\end{figure}
-In this chapter we give a guarantee in terms of size:
 given an annotated regular expression $a$, for any string $s$
 our algorithm $\blexersimp$'s internal annotated regular expression
 size  is finitely bounded
-by a constant $N_a$ that only depends on $a$:
+by a constant  that only depends on $a$.
+Formally we show that there exists an $N_a$ such that
 \begin{center}
 	$\llbracket \bderssimp{a}{s} \rrbracket \leq N_a$
 \end{center}
 \noindent
-where the size of an annotated regular expression is defined
+where the size ($\llbracket \_ \rrbracket$) of
-in terms of the number of nodes in its tree structure (see figure \ref{brexpSize}).
+an annotated regular expression is defined
+in terms of the number of nodes in its
+tree structure (its recursive definition given in the next page).
 We believe this size bound
 is important in the context of POSIX lexing, because
 \begin{itemize}
 	\item
-		It is a stepping stone towards an ``absence of catastrophic-backtracking''
+		It is a stepping stone towards the goal
-		guarantee.
+		of eliminating ``catastrophic backtracking''.
-		If the internal data structures used by our algorithm cannot grow very large,
+		If the internal data structures used by our algorithm
-		then our algorithm (which traverses those structures) cannot be too slow.
+		grows beyond a finite bound, then clearly
+		the algorithm (which traverses these structures) will
+		be slow.
 		The next step would be to refine the bound $N_a$ so that it
 		is polynomial on $\llbracket a\rrbracket$.
 	\item
-		Having it formalised gives us a higher confidence that
+		Having the finite bound formalised
+		gives us a higher confidence that
 		our simplification algorithm $\simp$ does not ``mis-behave''
 		like $\simpsulz$ does.
-		The bound is universal, which is an advantage over work which
+		The bound is universal for a given regular expression,
-		only gives empirical evidence on some test cases.
+		which is an advantage over work which
+		only gives empirical evidence on some test cases (see Verbatim++\cite{Verbatimpp}).
 \end{itemize}
+In the next section we describe in more detail
+what the finite bound means in our algorithm
+and why the size of the internal data structures of
+a typical derivative-based lexer such as
+Sulzmann and Lu's need formal treatment.
 \section{Formalising About Size}
 \noindent
 In our lexer ($\blexersimp$),
 we take an annotated regular expression as input,
-and repeately take derivative of and simplify it:
+and repeately take derivative of and simplify it.
-\begin{figure}[H]
+\begin{figure}
+	\begin{center}
+		\begin{tabular}{lcl}
+			$\llbracket _{bs}\ONE \rrbracket$ & $\dn$ & $1$\\
+			$\llbracket \ZERO \rrbracket$ & $\dn$ & $1$ \\
+			$\llbracket _{bs} r_1 \cdot r_2 \rrbracket$ & $\dn$ & $\llbracket r_1 \rrbracket + \llbracket r_2 \rrbracket + 1$\\
+			$\llbracket _{bs}\mathbf{c} \rrbracket $ & $\dn$ & $1$\\
+			$\llbracket _{bs}\sum as \rrbracket $ & $\dn$ & $\map \; (\llbracket \_ \rrbracket)\; as   + 1$\\
+			$\llbracket _{bs} a^* \rrbracket $ & $\dn$ & $\llbracket a \rrbracket + 1$.
+		\end{tabular}
+	\end{center}
+	\caption{The size function of bitcoded regular expressions}\label{brexpSize}
+\end{figure}
+\begin{figure}
 	\begin{tikzpicture}[scale=2,
 		every node/.style={minimum size=11mm},
 		->,>=stealth',shorten >=1pt,auto,thick
 		]
 		\node (r0) [rectangle, draw=black, thick, minimum size = 5mm, draw=blue] {$a$};
 		\node (v) [circle, thick, draw, right=of rns, minimum size=6mm, right=1.7cm]{$v$};
 		\draw[->, line width=0.2mm](rns)--(v) node[above, midway] {\bmkeps} node [below, midway] {\decode};
 	\end{tikzpicture}
 	\caption{Regular expression size change during our $\blexersimp$ algorithm}\label{simpShrinks}
 \end{figure}
 \noindent
 Each time
 a derivative is taken, the regular expression might grow.
 However, the simplification that is immediately afterwards will always shrink it so that
-it stays small.
+it stays relatively small.
 This intuition is depicted by the relative size
 change between the black and blue nodes:
 After $\simp$ the node always shrinks.
-Our proof says that all the blue nodes
+Our proof states that all the blue nodes
 stay below a size bound $N_a$ determined by the input $a$.
 \noindent
 Sulzmann and Lu's assumed a similar picture about their algorithm,
 though in fact their algorithm's size might be better depicted by the following graph:
 	\caption{Regular expression size change during our $\blexersimp$ algorithm}\label{sulzShrinks}
 \end{figure}
 \noindent
 The picture means that on certain cases their lexer (where they use $\simpsulz$
 as the simplification function)
-will have an indefinite size explosion, causing the running time
+will have a size explosion, causing the running time
 of each derivative step to grow continuously (for example
 in \ref{SulzmannLuLexerTime}).
 They tested out the run time of their
 lexer on particular examples such as $(a+b+ab)^*$
 and claimed that their algorithm is linear w.r.t to the input.
 With our mecahnised proof, we avoid this type of unintentional
 generalisation.\\
 Before delving in to the details of the formalisation,
 we are going to provide an overview of it.
-In the next subsection, we draw a picture of the bird's eye view
+In the next subsection, we give a high-level view
 of the proof.
 \subsection{Overview of the Proof}
-Here is a bird's eye view of the main components of the finiteness proof,
+A high-level overview of the main components of the finiteness proof
-which involves three steps:
+is as follows:
 \begin{figure}[H]
 	\begin{tikzpicture}[scale=1,font=\bf,
 		node/.style={
 			rectangle,rounded corners=3mm,
 			ultra thick,draw=black!50,minimum height=18mm,
 We explain the steps one by one:
 \begin{itemize}
 	\item
 		We first introduce the operations such as
 		derivatives, simplification, size calculation, etc.
-		associated with $\rrexp$s, which we have given
+		associated with $\rrexp$s, which we have introduced
-		a very brief introduction to in chapter \ref{Bitcoded2}.
+		in chapter \ref{Bitcoded2}.
 		The operations on $\rrexp$s are identical to those on
-		annotated regular expressions except that they are unaware
+		annotated regular expressions except that they dispense with
-		of bitcodes. This means that all proofs about size of $\rrexp$s will apply to
+		bitcodes. This means that all proofs about size of $\rrexp$s will apply to
-		annotated regular expressions.
+		annotated regular expressions, because the size of a regular
+		expression is independent of the bitcodes.
 	\item
 		We prove that $\rderssimp{r}{s} = \textit{ClosedForm}(r, s)$,
 		where $\textit{ClosedForm}(r, s)$ is entirely
-		written in the derivatives of their children regular
+		given as the derivatives of their children regular
 		expressions.
 		We call the right-hand-side the \emph{Closed Form}
 		of the derivative $\rderssimp{r}{s}$.
 	\item
-		We estimate $\llbracket \textit{ClosedForm}(r, s) \rrbracket_r$.
+		Formally we give an estimate of
+		$\llbracket \textit{ClosedForm}(r, s) \rrbracket_r$.
 		The key observation is that $\distinctBy$'s output is
 		a list with a constant length bound.
 \end{itemize}
 We will expand on these steps in the next sections.\\
 \section{The $\textit{Rrexp}$ Datatype}
 The first step is to define
 $\textit{rrexp}$s.
-They are without bitcodes,
+They are annotated regular expressions without bitcodes,
 allowing a much simpler size bound proof.
-Of course, the bits which encode the lexing information
+%Of course, the bits which encode the lexing information
-would grow linearly with respect
+%would grow linearly with respect
-to the input, which should be taken into account when we wish to tackle the runtime comlexity.
+%to the input, which should be taken into account when we wish to tackle the runtime comlexity.
-But for the sake of the structural size
+%But for the sake of the structural size
-we can safely ignore them.\\
+%we can safely ignore them.\\
-To recapitulate, the datatype
+The datatype
 definition of the $\rrexp$, called
 \emph{r-regular expressions},
 was initially defined in \ref{rrexpDef}.
 The reason for the prefix $r$ is
 to make a distinction
 \]
 The size of an r-regular expression is
 written $\llbracket r\rrbracket_r$,
 whose definition mirrors that of an annotated regular expression.
 \begin{center}
-	\begin{tabular}{ccc}
+	\begin{tabular}{lcl}
 		$\llbracket _{bs}\ONE \rrbracket_r$ & $\dn$ & $1$\\
 		$\llbracket \ZERO \rrbracket_r$ & $\dn$ & $1$ \\
 		$\llbracket _{bs} r_1 \cdot r_2 \rrbracket_r$ & $\dn$ & $\llbracket r_1 \rrbracket_r + \llbracket r_2 \rrbracket_r + 1$\\
 		$\llbracket _{bs}\mathbf{c} \rrbracket_r $ & $\dn$ & $1$\\
 		$\llbracket _{bs}\sum as \rrbracket_r $ & $\dn$ & $\map \; (\llbracket \_ \rrbracket_r)\; as   + 1$\\
 		$\rerase{_{bs} a ^*}$ & $\dn$ & $\rerase{a} ^*$
 	\end{tabular}
 \end{center}
 \subsection{Why a New Datatype?}
-The reason we take all the trouble
+The reason we
-defining a new datatype is that $\erase$ makes things harder.
+define a new datatype is that
+the $\erase$ function
+does not preserve the structure of annotated
+regular expressions.
 We initially started by using
 plain regular expressions and tried to prove
-the lemma \ref{rsizeAsize},
+lemma \ref{rsizeAsize},
-however the $\erase$ function unavoidbly messes with the structure of the
+however the $\erase$ function messes with the structure of the
 annotated regular expression.
 The $+$ constructor
-of basic regular expressions is binary whereas $\sum$
+of basic regular expressions is only binary, whereas $\sum$
-takes a list, and one has to convert between them:
+takes a list. Therefore we need to convert between
-\begin{center}
+annotated and normal regular expressions as follows:
-	\begin{tabular}{ccc}
+\begin{center}
+	\begin{tabular}{lcl}
 		$\erase \; _{bs}\sum [] $ & $\dn$ & $\ZERO$\\
 		$\erase \; _{bs}\sum [a]$ & $\dn$ & $a$\\
 		$\erase \; _{bs}\sum a :: as$ & $\dn$ & $a + (\erase \; _{[]} \sum as)\quad \text{if $as$ length over 1}$
 	\end{tabular}
 \end{center}
 \noindent
-An alternative regular expression with an empty argument list
+As can be seen alternative regular expression with an empty argument list
 will be turned into a $\ZERO$.
-The singleton alternative $\sum [r]$ would have $r$ during the
+The singleton alternative $\sum [r]$ becomes $r$ during the
 $\erase$ function.
 The  annotated regular expression $\sum[a, b, c]$ would turn into
 $(a+(b+c))$.
 All these operations change the size and structure of
 an annotated regular expressions, adding unnecessary
 complexities to the size bound proof.\\
 For example, if we define the size of a basic plain regular expression
 in the usual way,
 \begin{center}
-	\begin{tabular}{ccc}
+	\begin{tabular}{lcl}
 		$\llbracket \ONE \rrbracket_p$ & $\dn$ & $1$\\
 		$\llbracket \ZERO \rrbracket_p$ & $\dn$ & $1$ \\
 		$\llbracket r_1 \cdot r_2 \rrbracket_p$ & $\dn$ & $\llbracket r_1 \rrbracket_p + \llbracket r_2 \rrbracket_p + 1$\\
 		$\llbracket \mathbf{c} \rrbracket_p $ & $\dn$ & $1$\\
 		$\llbracket r_1 \cdot r_2 \rrbracket_p $ & $\dn$ & $\llbracket r_1 \rrbracket_p \; + \llbracket r_2 \rrbracket_p + 1$\\
 does not hold.
 With $\textit{rerase}$, however,
 only the bitcodes are thrown away.
 Everything about the structure remains intact.
 Therefore it does not change the size
-of an annotated regular expression:
+of an annotated regular expression and we have:
 \begin{lemma}\label{rsizeAsize}
 	$\rsize{\rerase a} = \asize a$
 \end{lemma}
 \begin{proof}
 	By routine structural induction on $a$.
 $\llbracket a \rrbracket  \leq \llbracket  a_\downarrow \rrbracket_p $
 and then estimate $\llbracket  a_\downarrow \rrbracket_p$,
 but we found our approach more straightforward.\\
 \subsection{Functions for R-regular Expressions}
-We shall define the r-regular expression version
+In this section we shall define the r-regular expression version
-of $\blexer$ and $\blexersimp$ related functions.
+of $\blexer$, and $\blexersimp$ related functions.
 We use $r$ as the prefix or subscript to differentiate
 with the bitcoded version.
-For example,$\backslash_r$, $\rdistincts$, and $\rsimp$
+%For example,$\backslash_r$, $\rdistincts$, and $\rsimp$
-as opposed to $\backslash$, $\distinctBy$, and $\bsimp$.
+%as opposed to $\backslash$, $\distinctBy$, and $\bsimp$.
-As promised, they are much simpler than their bitcoded counterparts.
+%As promised, they are much simpler than their bitcoded counterparts.
 %The operations on r-regular expressions are
 %almost identical to those of the annotated regular expressions,
 %except that no bitcodes are used. For example,
-The derivative operation becomes simpler:\\
+The derivative operation for an r-regular expression is\\
 \begin{center}
 	\begin{tabular}{@{}lcl@{}}
 		$(\ZERO)\,\backslash_r c$ & $\dn$ & $\ZERO$\\
 		$(\ONE)\,\backslash_r c$ & $\dn$ &
 		$\textit{if}\;c=d\; \;\textit{then}\;
 		$( r\,\backslash_r c)\cdot
 		(_{[]}r^*))$
 	\end{tabular}
 \end{center}
 \noindent
-Similarly, $\distinctBy$ does not need
+where we omit the definition of $\textit{rnullable}$.
+The function $\distinctBy$ for r-regular expressions does not need
 a function checking equivalence because
-there are no bit annotations causing superficial differences
+there are no bit annotations.
-between syntactically equal terms.
+Therefore we have
 \begin{center}
 	\begin{tabular}{lcl}
 		$\rdistinct{[]}{rset} $ & $\dn$ & $[]$\\
 		$\rdistinct{r :: rs}{rset}$ & $\dn$ &
 		$\textit{if}(r \in \textit{rset}) \; \textit{then} \; \rdistinct{rs}{rset}$\\
 					    r::\rdistinct{rs}{(rset \cup \{r\})}$
 	\end{tabular}
 \end{center}
 %TODO: definition of rsimp (maybe only the alternative clause)
 \noindent
-We would like to make clear
+%We would like to make clear
-a difference between our $\rdistincts$ and
+%a difference between our $\rdistincts$ and
-the Isabelle $\textit {distinct}$ predicate.
+%the Isabelle $\textit {distinct}$ predicate.
-In Isabelle $\textit{distinct}$ is a function that returns a boolean
+%In Isabelle $\textit{distinct}$ is a function that returns a boolean
-rather than a list.
+%rather than a list.
-It tests if all the elements of a list are unique.\\
+%It tests if all the elements of a list are unique.\\
-With $\textit{rdistinct}$,
+With $\textit{rdistinct}$ in place,
-and the flatten function for $\rrexp$s:
+the flatten function for $\rrexp$ is as follows:
 \begin{center}
 \begin{tabular}{@{}lcl@{}}
 $\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
+The function
-such as $\rsimpalts$:
+$\rsimpalts$ corresponds to $\textit{bsimp}_{ALTS}$:
 \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$:
+Similarly, we have $\rsimpseq$ which corresponds to $\textit{bsimp}_{SEQ}$:
 \begin{center}
 \begin{tabular}{@{}lcl@{}}
 	  $\rsimpseq \;\; \RZERO \; \_ $ &   $=$ &   $\RZERO$\\
 	  $\rsimpseq \;\; \_ \; \RZERO $ &   $=$ &   $\RZERO$\\
 	  $\rsimpseq \;\; \RONE \cdot r_2$ & $\dn$ & $r_2$\\
 $r \backslash_{rsimps} [\,] $ & $\dn$ & $r$
 	\end{tabular}
 \end{center}
 \noindent
 We do not define an r-regular expression version of $\blexersimp$,
-as our proof does not involve its use
+as our proof does not depend on it.
-(and there is no bitcode to decode into a lexical value).
 Now we are ready to introduce how r-regular expressions allow
 us to prove the size bound on bitcoded regular expressions.
 \subsection{Using R-regular Expressions to Bound Bit-coded Regular Expressions}
 Everything about the size of annotated regular expressions after the application
 of function $\bsimp$ and $\backslash_{simps}$
 can be calculated via the size of r-regular expressions after the application
 of $\rsimp$ and $\backslash_{rsimps}$:
 \begin{lemma}\label{sizeRelations}
-	The following equalities hold:
+	The following two equalities hold:
 	\begin{itemize}
 		\item
 			$\asize{\bsimps \; a} = \rsize{\rsimp{ \rerase{a}}}$
 		\item
 			$\asize{\bderssimp{a}{s}} =  \rsize{\rderssimp{\rerase{a}}{s}}$
 \begin{center}
 	$\rsize{\rderssimp{\rerase{a}}{s}} \leq N_r \quad$
 	implies
 	$\quad \llbracket a \backslash_{bsimps} s \rrbracket \leq N_r$.
 \end{center}
-From now on we
+%From now on we
-Unless stated otherwise in the rest of this
+%Unless stated otherwise in the rest of this
-chapter all regular expressions without
+%chapter all regular expressions without
-bitcodes are seen as r-regular expressions ($\rrexp$s).
+%bitcodes are seen as r-regular expressions ($\rrexp$s).
-For the binary alternative r-regular expression $\RALTS{[r_1, r_2]}$,
+%For the binary alternative r-regular expression $\RALTS{[r_1, r_2]}$,
-we use the notation $r_1 + r_2$
+%we use the notation $r_1 + r_2$
-for brevity.
+%for brevity.
 %-----------------------------------
 %	SUB SECTION ROADMAP RREXP BOUND
 %-----------------------------------
 \end{center}
 The problem is that it is not clear what
 $(r_1\cdot r_2) \backslash_{rsimps} s$ looks like,
 and therefore $N_{r_1}$ and $N_{r_2}$ in the
 inductive hypotheses cannot be directly used.
-We have already seen that $(r_1 \cdot r_2)\backslash s$
+%We have already seen that $(r_1 \cdot r_2)\backslash s$
-and $(r^*)\backslash s$ can grow in a wild way.
+%and $(r^*)\backslash s$ can grow in a wild way.
-The point is that they will be equivalent to a list of
+The point however, is that they will be equivalent to a list of
 terms $\sum rs$, where each term in $rs$ will
 be made of $r_1 \backslash s' $, $r_2\backslash s'$,
-and $r \backslash s'$ with $s' \in \textit{SubString} \; s$.
+and $r \backslash s'$ with $s' \in \textit{SubString} \; s$ (which stands
+for the set of substrings of $s$).
 The list $\sum rs$ will then be de-duplicated by $\textit{rdistinct}$
-in the simplification which saves $rs$ from growing indefinitely.
+in the simplification, which prevents the $rs$ from growing indefinitely.
 Based on this idea, we develop a proof in two steps.
 First, we show the equality (where
 $f$ and $g$ are functions that do not increase the size of the input)
 \begin{center}
 	\end{center}
 We call the right-hand-side the
 \emph{Closed Form} of $(r_1 \cdot r_2)\backslash_{rsimps} s$.
 Second, we will bound the closed form of r-regular expressions
 using some estimation techniques
-and then piece it together
+and then apply
-with lemma \ref{sizeRelations} to show the bitcoded regular expressions
+lemma \ref{sizeRelations} to show that the bitcoded regular expressions
 in our $\blexersimp$ are finitely bounded.
-We will flesh out the first step of the proof we
+We will describe in detail the first step of the proof
-sketched just now in the next section.
+in the next section.
 \section{Closed Forms}
 In this section we introduce in detail
-how the closed forms are obtained for regular expressions'
+how we express the string derivatives
-derivatives.
+of regular expressions (i.e. $r \backslash_r s$ where $s$ is a string
+rather than a single character) in a different way than
+our previous definition.
+In previous chapters, the derivative of a
+regular expression $r$ w.r.t a string $s$
+was recursively defined on the string:
+\begin{center}
+	$r \backslash_s (c::s) \dn (r \backslash c) \backslash_s s$
+\end{center}
+The problem is that
+this definition does not provide much information
+on what $r \backslash_s s$ looks like.
+If we are interested in the size of a derivative like
+$(r_1 \cdot r_2)\backslash s$,
+we have to somehow get a more concrete form to begin.
+We call such more concrete representations the ``closed forms'' of
+string derivatives as opposed to their original definitions.
+The terminology ``closed form'' is borrowed from mathematics,
+which usually describe expressions that are solely comprised of
+well-known and easy-to-compute operations such as
+additions, multiplications, exponential functions.
 We start by proving some basic identities
 involving the simplification functions for r-regular expressions.
 After that we introduce the rewrite relations
 $\rightsquigarrow_h$, $\rightsquigarrow^*_{scf}$
 $\rightsquigarrow_f$ and $\rightsquigarrow_g$.
-These relations involves similar techniques in chapter \ref{Bitcoded2}.
+These relations involves similar techniques as in chapter \ref{Bitcoded2}
+for annotated regular expressions.
 Finally, we use these identities to establish the
 closed forms of the alternative regular expression,
 the sequence regular expression, and the star regular expression.
 %$r_1\cdot r_2$, $r^*$ and $\sum rs$.
 \subsection{Some Basic Identities}
-We now introduce lemmas
+In what follows we will often convert between lists
-that are repeatedly used in later proofs.
+and sets.
-Note that for the $\textit{rdistinct}$ function there
+We use Isabelle's $set$ to refere to the
-will be a lot of conversion from lists to sets.
-We use $set$ to refere to the
 function that converts a list $rs$ to the set
 containing all the elements in $rs$.
 \subsubsection{$\textit{rdistinct}$'s Does the Job of De-duplication}
 The $\textit{rdistinct}$ function, as its name suggests, will
 de-duplicate an r-regular expression list.
 is already in the accumulator set.
 \begin{lemma}\label{rdistinctDoesTheJob}
 	%The function $\textit{rdistinct}$ satisfies the following
 	%properties:
 	Assume we have the predicate $\textit{isDistinct}$\footnote{We omit its
-	recursive definition here, its Isabelle counterpart would be $\textit{distinct}$.}
+	recursive definition here. Its Isabelle counterpart would be $\textit{distinct}$.}
-	readily defined
 	for testing
 	whether a list's elements are unique. Then the following
 	properties about $\textit{rdistinct}$ hold:
 	\begin{itemize}
 		\item
 \end{lemma}
 \noindent
 \begin{proof}
 	By induction on $rs$. All other variables are allowed to be arbitrary.
 	The second part of the lemma requires the first.
-	Note that for each part, the two sub-propositions need to be proven concurrently,
+	Note that for each part, the two sub-propositions need to be proven
+	at the same time,
 	so that the induction goes through.
 \end{proof}
 \noindent
 This allows us to prove a few more equivalence relations involving
-$\textit{rdistinct}$ (it will be useful later):
+$\textit{rdistinct}$ (they will be useful later):
 \begin{lemma}\label{rdistinctConcatGeneral}
 	\mbox{}
 	\begin{itemize}
 		\item
 			$\rdistinct{(rs @ rs')}{\varnothing} = \rdistinct{((\rdistinct{rs}{\varnothing})@ rs')}{\varnothing}$
 	By an induction on
 	$rs_1$, where $rsa$ and $acc$ are allowed to be arbitrary.
 \end{proof}
 \noindent
 $\textit{rdistinct}$ needs to be applied only once, and
-applying it multiple times does not cause any difference:
+applying it multiple times does not make any difference:
 \begin{corollary}\label{distinctOnceEnough}
 	$\textit{rdistinct} \; (rs @ rsa) {} = \textit{rdistinct} \; (rdistinct \;
 	rs \{ \} @ (\textit{rdistinct} \; rs_a \; (set \; rs)))$
 \end{corollary}
 \begin{proof}
 %When the function $\textit{Rflts}$
 %is applied to the concatenation of two lists, the output can be calculated by first applying the
 %functions on two lists separately, and then concatenating them together.
 $\textit{Rflts}$ is composable in terms of concatenation:
 \begin{lemma}\label{rfltsProps}
-	The function $\rflts$ has the below properties:\\
+	The function $\rflts$ has the properties below:\\
 	\begin{itemize}
 		\item
 			$\rflts \; (rs_1 @ rs_2) = \rflts \; rs_1 @ \rflts \; rs_2$
 		\item
 			If $r \neq \RZERO$ and $\nexists rs_1. r = \RALTS{rs}_1$, then $\rflts \; (r::rs) = r :: \rflts \; rs$
 	last sub-lemma.
 \end{proof}
 \noindent
 Now we introduce the property that the operations
 derivative and $\rsimpalts$
-commute, this will be used later in deriving the closed form for
+commute, this will be used later on, when deriving the closed form for
 the alternative regular expression:
 \begin{lemma}\label{rderRsimpAltsCommute}
 	$\rder{x}{(\rsimpalts \; rs)} = \rsimpalts \; (\map \; (\rder{x}{\_}) \; rs)$
 \end{lemma}
+\begin{proof}
+	By induction on $rs$.
+\end{proof}
 \noindent
 \subsubsection{The $RL$ Function: Language Interpretation of $\textit{Rrexp}$s}
-Much like the definition of $L$ on plain regular expressions, one could also
+Much like the definition of $L$ on plain regular expressions, one can also
 define the language interpretation of $\rrexp$s.
 \begin{center}
 	\begin{tabular}{lcl}
 		$RL \; (\ZERO)$ & $\dn$ & $\phi$\\
 		$RL \; (\ONE)$ & $\dn$ & $\{[]\}$\\
 \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
+are fully simplified in terms of our $\textit{rsimp}$ function.
-do not contain any nested alternatives like
+For alternative regular expressions that means they
-\[ r_1 + (r_2 + r_3) \], un-removed $\RZERO$s like \[\RZERO + r\]
+do not contain any nested alternatives, un-eliminated $\RZERO$s
-or duplicate elements in a children regular expression list like \[ \sum [r, r, \ldots]\]:
+or duplicate elements (for example,
+$r_1 + (r_2 + r_3)$, $\RZERO + r$ and $ \sum [r, r, \ldots]$).
+The clauses for $\good$ are:
 \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')$\\
+						   & & $\land \; (\forall r' \in (r_1 :: r_2 :: rs).\; \good \; r'\; \,  \land \; \, \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
+We omit the recursive definition of the predicate $\textit{nonAlt}$,
+which 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}
 The $\rflts$ function
 always opens up nested alternatives,
 which enables $\rsimp$ to be non-nested:
 \begin{lemma}\label{nonnestedRsimp}
-	$\nonnested \; (\rsimp{r})$
+	It is always the case that
-\end{lemma}
+	\begin{center}
-\begin{proof}
+		$\nonnested \; (\rsimp{r})$
-	By an induction on $r$.
+	\end{center}
+\end{lemma}
+\begin{proof}
+	By 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:
 \end{lemma}
 \begin{proof}
 	By \ref{nonnestedRsimp}.
 \end{proof}
 \noindent
-The other thing we know is that once $\rsimp{}$ had finished
+The other fact we know is that once $\rsimp{}$ has finished
 processing an alternative regular expression, it will not
-contain any $\RZERO$s, this is because all the recursive
+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
+make the children good, and $\rflts$ will not delete
 any $\RZERO$s out of a good regular expression list,
-and $\rdistinct{}$ will not mess with the result.
+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$,
 \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
+	Lemma \ref{rsimpMono} 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 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:
+with respect to $\rsimp{}$:
 \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}$,
+Given below is a property involving $\rflts$, $\textit{rdistinct}$,
-which requires $\ref{good1}$ to go through smoothly.
+$\rsimp{}$ and $\rsimp_{ALTS}$,
-It says that an application of $\rsimp_{ALTS}$ can be "absorbed",
+which requires $\ref{good1}$ to go through smoothly:
-if it its output is concatenated with a list and then applied to $\rflts$.
 \begin{lemma}\label{flattenRsimpalts}
+An application of $\rsimp_{ALTS}$ can be ``absorbed'',
+if its output is concatenated with a list and then applied to $\rflts$.
+\begin{center}
 	$\rflts \; ( (\rsimp_{ALTS} \;
 	(\rdistinct{(\rflts \; (\map \; \rsimp{}\; rs))}{\varnothing})) ::
 	\map \; \rsimp{} \; rs' ) =
 	\rflts \; ( (\rdistinct{(\rflts \; (\map \; \rsimp{}\; rs))}{\varnothing}) @ (
 	\map \; \rsimp{rs'}))$
+\end{center}
 \end{lemma}
 \begin{proof}
 	By \ref{good1}.
 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}}$
+	$\rsimp{r} = \rsimp{(\rsimp{r})}$
 \end{lemma}
 \begin{proof}
 	By \ref{test} and \ref{good1}.
 \end{proof}
 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 the other hand, we can 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}:
 		\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.
+This will be useful in the later closed form proof's rewriting steps.
-Similarly, we point out the following useful facts below:
+Similarly, we state 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$.
 \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}$.
+To make the notation more concise
+We use $r_1 \sequal r_2 $ to denote that $\rsimp{r_1} = \rsimp{r_2}$:
+\begin{center}
+\begin{tabular}{lcl}
+	$a \sequal b$ & $ \dn$ & $ \textit{rsimp} \; a = \textit{rsimp} \; b$
+\end{tabular}
+\end{center}
+\noindent
+%\vspace{0em}
 \begin{lemma}
+	The following equivalence hold:
 	\begin{itemize}
-		The following equivalence hold:
 	\item
 		$\rsimpalts \; (\RZERO :: rs) \sequal \rsimpalts\; rs$
 	\item
 		$\rsimpalts \; rs \sequal \rsimpalts (\map \; \rsimp{} \; rs)$
 	\item
 	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
+It says that we could flatten 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}
 \end{comment}
 %Rewriting steps not put in--too long and complicated-------------------------------
 \noindent
-We need more equalities like the above to enable a closed form,
+We need more equalities like the above to enable a closed form lemma,
 for which we need to introduce a few rewrite relations
 to help
 us obtain them.
 \subsection{The rewrite relation $\hrewrite$ , $\scfrewrites$ , $\frewrite$ and $\grewrite$}
 \end{center}
 \caption{List of one-step rewrite rules characterising the $\rflts$ and $\textit{rdistinct}$
 operations}\label{gRewrite}
 \end{figure}
 \noindent
-We defined
+We define
 two separate list rewriting relations $\frewrite$ and $\grewrite$.
 The rewriting steps that take place during
 flattening is characterised by $\frewrite$.
-$\grewrite$ characterises both flattening and de-duplicating.
+The rewrite relation $\grewrite$ characterises both flattening and de-duplicating.
 Sometimes $\grewrites$ is slightly too powerful
 so we would rather use $\frewrites$ to prove
 %because we only
 equalities related to $\rflts$.
 %certain equivalence under the rewriting steps of $\frewrites$.
 	$\map \; (\_ \backslash x) \;  (\rflts \; rs) \frewrites
 	\rflts \; (\map \; (\_ \backslash x) \; rs)$
 \end{lemma}
 \noindent
 and then the equivalence between two terms
-that can reduce in many steps to each other.
+that can reduce in many steps to each other:
 \begin{lemma}\label{frewritesSimpeq}
 	If $rs_1 \frewrites rs_2 $, then $\sum (\rDistinct \; rs_1 \; \varnothing) \sequal
 	\sum (\rDistinct \;  rs_2 \;  \varnothing)$.
 \end{lemma}
 \noindent
+These two lemmas can both be proven using a straightforward induction (and
+the proofs for them are therefore omitted).
+Now the above equalities can be derived like a breeze:
 \begin{corollary}
 	$\sum (\rDistinct \;\; (\map \; (\_ \backslash x) \; (\rflts \; rs)) \;\; \varnothing) \sequal
 	\sum (\rDistinct \;\;  (\rflts \; (\map \; (\_ \backslash x) \; rs)) \;\; \varnothing)
 	$
 \end{corollary}
+\begin{proof}
+	By lemmas \ref{earlyLaterDerFrewrites} and \ref{frewritesSimpeq}.
+\end{proof}
 But this trick will not work for $\grewrites$.
 For example, a rewriting step in proving
 closed forms is:
 \begin{center}
 	$\rsimp{(\rsimpalts \; (\map \; (\_ \backslash x) \; (\rdistinct{(\rflts \; (\map \; (\rsimp{} \; \circ \; (\lambda r. \rderssimp{r}{xs}))))}{\varnothing})))}$\\
 	$=$ \\
 	$\rsimp{(\rsimpalts \; (\rdistinct{(\map \; (\_ \backslash x) \; (\rflts \; (\map \; (\rsimp{} \; \circ \; (\lambda r. \rderssimp{r}{xs})))) ) }{\varnothing}))} $
 	\noindent
 \end{center}
-For this one would hope to have a rewriting relation between the two lists involved,
+For this, one would hope to have a rewriting relation between the two lists involved,
 similar to \ref{earlyLaterDerFrewrites}. However, it turns out that
 \begin{center}
 	$\map \; (\_ \backslash x) \; (\rDistinct \; rs \; rset) \grewrites \rDistinct \; (\map \;
 	(\_ \backslash x) \; rs) \; ( rset \backslash x)$
 \end{center}
 \noindent
 does $\mathbf{not}$ hold in general.
 For this rewriting step we will introduce some slightly more cumbersome
-proof technique in later sections.
+proof technique later.
 The point is that $\frewrite$
 allows us to prove equivalence in a straightforward way that is
 not possible for $\grewrite$.
 \subsubsection{Terms That Can Be Rewritten Using $\hrewrites$, $\grewrites$, and $\frewrites$}
 In this part, we present lemmas stating
-pairs of r-regular expressions or r-regular expression lists
+pairs of r-regular expressions and r-regular expression lists
 where one could rewrite from one in many steps to the other.
 Most of the proofs to these lemmas are straightforward, using
-an induction on the inductive cases of the corresponding rewriting relations.
+an induction on the corresponding rewriting relations.
 These proofs will therefore be omitted when this is the case.
-We present in the below lemma a few pairs of terms that are rewritable via
+We present in the following lemma a few pairs of terms that are rewritable via
 $\grewrites$:
 \begin{lemma}\label{gstarRdistinctGeneral}
 	\mbox{}
 	\begin{itemize}
 		\item
 \end{lemma}
 \noindent
 If a pair of terms $rs_1, rs_2$ are rewritable via $\grewrites$ to each other,
 then they are equivalent under $\rsimp{}$:
 \begin{lemma}\label{grewritesSimpalts}
+	\mbox{}
 	If $rs_1 \grewrites rs_2$, then
 	we have the following equivalence:
 	\begin{itemize}
 		\item
 			$\sum rs_1 \sequal \sum rs_2$
 			If $rs_1 \scfrewrites rs_2$ then $\sum rs_1 \hrewrites \sum rs_2$
 	\end{itemize}
 \end{lemma}
 \noindent
-Here comes the meat of the proof,
+Now comes the core of the proof,
 which says that once two lists are rewritable to each other,
 then they are equivalent under $\rsimp{}$:
 \begin{lemma}
 	If $r_1 \hrewrites r_2$ then $r_1 \sequal r_2$.
 \end{lemma}
 \noindent
-And similar to \ref{Bitcoded2} one can preserve rewritability after taking derivative
+Similar to what we did in \ref{Bitcoded2},
-of two regular expressions on both sides:
+we prove that if one can rewrite from one r-regular expression ($r$)
+to the other ($r'$), after taking derivatives one could still rewrite
+the first ($r\backslash c$) to the other ($r'\backslash c$).
 \begin{lemma}\label{interleave}
 	If $r \hrewrites r' $ then $\rder{c}{r} \hrewrites \rder{c}{r'}$
 \end{lemma}
 \noindent
-This allows proving more $\mathbf{rsimp}$-equivalent terms, involving $\backslash_r$ now.
+This allows us proving more $\mathbf{rsimp}$-equivalent terms, involving $\backslash_r$.
 \begin{lemma}\label{insideSimpRemoval}
-	$\rsimp{\rder{c}{\rsimp{r}}} = \rsimp{\rder{c}{r}}  $
+	$\rsimp{(\rder{c}{(\rsimp{r})})} = \rsimp{(\rder{c}{r})}  $
 \end{lemma}
 \noindent
 \begin{proof}
 	By \ref{interleave} and \ref{rsimpIdem}.
 \end{proof}
 	part 2 is by lemma \ref{insideSimpRemoval} .%and \ref{distinctDer}.
 \end{proof}
 \noindent
 \subsection{Closed Forms for $\sum rs$, $r_1\cdot r_2$ and $r^*$}
-\subsubsection{Closed Form for Alternative Regular Expression}
+Lemma \ref{Simpders} leads to our first closed form,
-Lemma \ref{Simpders} leads to the first closed form--
+which is for the alternative regular expression:
-\begin{lemma}\label{altsClosedForm}
+\begin{theorem}\label{altsClosedForm}
+	\mbox{}
 	\begin{center}
 		$\rderssimp{(\sum rs)}{s} \sequal
 		\sum \; (\map \; (\rderssimp{\_}{s}) \; rs)$
 	\end{center}
-\end{lemma}
+\end{theorem}
 \noindent
 \begin{proof}
 	By a reverse induction on the string $s$.
 	One rewriting step, as we mentioned earlier,
 	involves
 	\ref{grewritesSimpalts}, \ref{gstarRdistinctGeneral}, \ref{rderRsimpAltsCommute}, and
 	\ref{insideSimpRemoval}.
 \end{proof}
 \noindent
 This closed form has a variant which can be more convenient in later proofs:
-\begin{corollary}{altsClosedForm1}
+\begin{corollary}\label{altsClosedForm1}
 	If $s \neq []$ then
 	$\rderssimp \; (\sum \; rs) \; s =
 	\rsimp{(\sum \; (\map \; \rderssimp{\_}{s} \; rs))}$.
 \end{corollary}
 \noindent
 Before we obtain them, some preliminary definitions
 are needed to make proof statements concise.
 \subsubsection{Closed Form for Sequence Regular Expressions}
-First let's look at a series of derivatives steps on a sequence
+For the sequence regular expression,
-regular expression, assuming that each time the first
+let's first look at a series of derivative steps on it
-component of the sequence is always nullable):
+(assuming that each time when a derivative is taken,
-\begin{center}
+the head of the sequence is always nullable):
+\begin{center}
-	$r_1 \cdot r_2 \quad \longrightarrow_{\backslash c}  \quad   r_1  \backslash c \cdot r_2 + r_2 \backslash c \quad \longrightarrow_{\backslash c'} \quad (r_1 \backslash cc' \cdot r_2 + r_2 \backslash c') + r_2 \backslash cc' \longrightarrow_{\backslash c''} \quad$\\
+	\begin{tabular}{llll}
-	$((r_1 \backslash cc'c'' \cdot r_2 + r_2 \backslash c'') + r_2 \backslash c'c'') + r_2 \backslash cc'c''   \longrightarrow_{\backslash c''} \quad
+		$r_1 \cdot r_2$ &
-	\ldots$
+		$\longrightarrow_{\backslash c}$ &
+		$r_1\backslash c \cdot r_2 + r_2 \backslash c$ &
+		$ \longrightarrow_{\backslash c'} $ \\
+		\\
+		$(r_1 \backslash cc' \cdot r_2 + r_2 \backslash c') + r_2 \backslash cc'$ &
+		$\longrightarrow_{\backslash c''} $ &
+		$((r_1 \backslash cc'c'' \cdot r_2 + r_2 \backslash c'') + r_2 \backslash c'c'')
+		+ r_2 \backslash cc'c''$ &
+		$   \longrightarrow_{\backslash c''} \quad \ldots$\\
+	\end{tabular}
 \end{center}
 Roughly speaking $r_1 \cdot r_2 \backslash s$ can be expresssed as
 a giant alternative taking a list of terms
 $[r_1 \backslash_r s \cdot r_2, r_2 \backslash_r s'', r_2 \backslash_r s_1'', \ldots]$,
 where the head of the list is always the term
 representing a match involving only $r_1$, and the tail of the list consisting of
 terms of the shape $r_2 \backslash_r s''$, $s''$ being a suffix of $s$.
-This intuition is also echoed by IndianPaper, where they gave
+This intuition is also echoed by Murugesan and Sundaram \cite{Murugesan2014},
+where they gave
 a pencil-and-paper derivation of $(r_1 \cdot r_2)\backslash s$:
 \begin{center}
-	\begin{tabular}{c}
+	\begin{tabular}{lc}
-		$(r_1 \cdot r_2) \backslash_r (c_1 :: c_2 :: \ldots c_n) \myequiv$\\
+		$L \; [ (r_1 \cdot r_2) \backslash_r (c_1 :: c_2 :: \ldots c_n) ]$ & $ =$\\
-		\rule{0pt}{3ex} $((r_1 \backslash_r c_1) \cdot r_2 + (\delta\; (\rnullable \; r_1) \; r_2 \backslash_r c_1)) \backslash_r (c_2 :: \ldots c_n)
+		\\
-		\myequiv$\\
+		\rule{0pt}{3ex} $L \; [ ((r_1 \backslash_r c_1) \cdot r_2 +
-		\rule{0pt}{3ex} $((r_1 \backslash_r c_1c_2 \cdot r_2 + (\delta \; (\rnullable \; r_1) \; r_2 \backslash_r c_1c_2))
+		(\delta\; (\nullable \; r_1) \; (r_2 \backslash_r c_1) )) \backslash_r
-		+ (\delta \ (\rnullable \; r_1 \backslash_r c)\; r_2 \backslash_r c_2)) \backslash_r (c_3 \ldots c_n)
+		(c_2 :: \ldots c_n) ]$ &
-		$
+		$=$\\
-	\end{tabular}
+		\\
-\end{center}
+		\rule{0pt}{3ex} $L \; [ ((r_1 \backslash_r c_1c_2 \cdot r_2 +
-\noindent
+		(\delta \; (\nullable \; r_1) \; (r_2 \backslash_r c_1c_2)))
-The equality in above should be interpretated
+		$ & \\
-as language equivalence.
+		\\
-The $\delta$ function works similarly to that of
+		$\quad + (\delta \ (\nullable \; r_1 \backslash_r c)\; (r_2 \backslash_r c_2) ))
-a Kronecker delta function:
+		\backslash_r (c_3 \ldots c_n) ]$ & $\ldots$ \\
-\[ \delta \; b\; r\]
+	\end{tabular}
-will produce $r$
+\end{center}
-if $b$ evaluates to true,
+\noindent
-and $\RZERO$ otherwise.
+The $\delta$ function
-Note that their formulation
+returns $r$ when the boolean condition
-\[
+$b$ evaluates to true and
-	((r_1 \backslash_r \, c_1c_2 \cdot r_2 + (\delta \; (\rnullable) \; r_1, r_2 \backslash_r c_1c_2)
+$\ZERO$ otherwise:
-	+ (\delta \; (\rnullable \; r_1 \backslash_r c)\; r_2 \backslash_r c_2)
+\begin{center}
-\]
+	\begin{tabular}{lcl}
+		$\delta \; b\; r$ & $\dn$ & $r \quad \textit{if} \; b \; is \;\textit{true}$\\
+				  & $\dn$ & $\ZERO \quad otherwise$
+	\end{tabular}
+\end{center}
+\noindent
+Note that the term
+\begin{center}
+	\begin{tabular}{lc}
+		\rule{0pt}{3ex} $((r_1 \backslash_r c_1c_2 \cdot r_2 +
+		(\delta \; (\nullable \; r_1) \; (r_2 \backslash_r c_1c_2)))
+		$ & \\
+		\\
+		$\quad + (\delta \ (\nullable \; r_1 \backslash_r c)\; (r_2 \backslash_r c_2) ))
+		\backslash_r (c_3 \ldots c_n)$ &\\
+	\end{tabular}
+\end{center}
+\noindent
 does not faithfully
 represent what the intermediate derivatives would actually look like
 when one or more intermediate results $r_1 \backslash s' \cdot r_2$ are not
 nullable in the head of the sequence.
 For example, when $r_1$ and $r_1 \backslash_r c_1$ are not nullable,
 the regular expression would not look like
 \[
-	(r_1 \backslash_r c_1c_2 + \RZERO ) + \RZERO,
+	r_1 \backslash_r c_1c_2
 \]
-but actually $r_1 \backslash_r c_1c_2$, the redundant $\RZERO$s will not be created in the
+instead of
+\[
+	(r_1 \backslash_r c_1c_2 + \ZERO ) + \ZERO.
+\]
+The redundant $\ZERO$s will not be created in the
 first place.
-In a closed-form one would want to take into account this
+In a closed-form one needs to take into account this (because
-and generate the list of
+closed forms require exact equality rather than language equivalence)
-regular expressions $r_2 \backslash_r s''$ with
+and only generate the
-string pairs $(s', s'')$ where $s'@s'' = s$ and
+$r_2 \backslash_r s''$ terms satisfying the property
-$r_1 \backslash s'$ nullable.
+\begin{center}
-We denote the list consisting of such
+$\exists  s'.  such \; that \; s'@s'' = s \;\; \land \;\;
-strings $s''$ as $\vsuf{s}{r_1}$.
+r_1 \backslash s' \; is \; nullable$.
+\end{center}
-The function $\vsuf{\_}{\_}$ is defined recursively on the structure of the string:
+Given the arguments $s$ and $r_1$, we denote the list of strings
+$s''$ satisfying the above property as $\vsuf{s}{r_1}$.
+The function $\vsuf{\_}{\_}$ is defined recursively on the structure of the string\footnote{
+	Perhaps a better name of it would be ``NullablePrefixSuffix''
+	to differentiate with the list of \emph{all} prefixes of $s$, but
+	that is a bit too long for a function name and we are yet to find
+a more concise and easy-to-understand name.}
 \begin{center}
 	\begin{tabular}{lcl}
 		$\vsuf{[]}{\_} $ & $=$ &  $[]$\\
-		$\vsuf{c::cs}{r_1}$ & $ =$ & $ \textit{if} (\rnullable{r_1}) \textit{then} \; (\vsuf{cs}{(\rder{c}{r_1})}) @ [c :: cs]$\\
+		$\vsuf{c::cs}{r_1}$ & $ =$ & $ \textit{if} \; (\rnullable{r_1}) \; \textit{then} \; (\vsuf{cs}{(\rder{c}{r_1})}) @ [c :: cs]$\\
 				    && $\textit{else} \; (\vsuf{cs}{(\rder{c}{r_1}) })  $
 	\end{tabular}
 \end{center}
 \noindent
-The list is sorted in the order $r_2\backslash s''$
+The list starts with shorter suffixes
-appears in $(r_1\cdot r_2)\backslash s$.
+and ends with longer ones (in other words, the string elements $s''$
+in the list $\vsuf{s}{r_1}$ are sorted
+in the same order as that of the terms $r_2\backslash s''$
+appearing in $(r_1\cdot r_2)\backslash s$).
 In essence, $\vsuf{\_}{\_}$ is doing a
 "virtual derivative" of $r_1 \cdot r_2$, but instead of producing
 the entire result $(r_1 \cdot r_2) \backslash s$,
-it only stores all the strings $s''$ such that $r_2 \backslash s''$
+it only stores strings,
-are occurring terms in $(r_1\cdot r_2)\backslash s$.
+with each string $s''$ representing a term such that $r_2 \backslash s''$
+is occurring in $(r_1\cdot r_2)\backslash s$.
-To make the closed form representation
-more straightforward,
+With $\textit{Suffix}$ we are ready to express the
-the flattetning function $\sflat{\_}$ is used to enable the transformation from
+sequence regular expression's closed form,
+but before doing so
+more devices are needed.
+The first thing is the flattening function $\sflat{\_}$,
+which takes an alternative regular expression and produces a flattened version
+of that alternative regular expression.
+It is needed to convert
 a left-associative nested sequence of alternatives into
 a flattened list:
 \[
-	\sum [r_1, r_2, r_3, \ldots] \stackrel{\sflat{\_}}{\rightarrow}
+	\sum(\ldots ((r_1 + r_2) + r_3) + \ldots)
-	(\ldots ((r_1 + r_2) + r_3) + \ldots)
+	\stackrel{\sflat{\_}}{\rightarrow}
+	\sum[r_1, r_2, r_3, \ldots]
 \]
 \noindent
-The definitions $\sflat{\_}$, $\sflataux{\_}$ are given below.
+The definitions of $\sflat{\_}$ and helper functions
+$\sflataux{\_}$ and $\llparenthesis \_ \rrparenthesis''$ are given below.
 \begin{center}
-	\begin{tabular}{ccc}
+	\begin{tabular}{lcl}
-		$\sflataux{\AALTS{ }{r :: rs}}$ & $=$ & $\sflataux{r} @ rs$\\
+		$\sflataux{\sum r :: rs}$ & $\dn$ & $\sflataux{r} @ rs$\\
-		$\sflataux{\AALTS{ }{[]}}$ & $ = $ & $ []$\\
+		$\sflataux{\sum []}$ & $ \dn $ & $ []$\\
-		$\sflataux r$ & $=$ & $ [r]$
+		$\sflataux r$ & $\dn$ & $ [r]$
 	\end{tabular}
 \end{center}
 \begin{center}
-	\begin{tabular}{ccc}
+	\begin{tabular}{lcl}
-		$\sflat{(\sum r :: rs)}$ & $=$ & $\sum (\sflataux{r} @ rs)$\\
+		$\sflat{(\sum r :: rs)}$ & $\dn$ & $\sum (\sflataux{r} @ rs)$\\
-		$\sflat{\sum []}$ & $ = $ & $ \sum []$\\
+		$\sflat{\sum []}$ & $ \dn $ & $ \sum []$\\
-		$\sflat r$ & $=$ & $ r$
+		$\sflat r$ & $\dn$ & $ r$
+	\end{tabular}
+\end{center}
+\begin{center}
+	\begin{tabular}{lcl}
+		$\sflataux{[]}'$ & $ \dn $ & $ []$\\
+		$\sflataux{ (r_1 + r_2) :: rs }'$ & $\dn$ & $r_1 :: r_2 :: rs$\\
+		$\sflataux{r :: rs}$ & $\dn$ & $ r::rs$
 	\end{tabular}
 \end{center}
 \noindent
 $\sflataux{\_}$ breaks up nested alternative regular expressions
 of the $(\ldots((r_1 + r_2) + r_3) + \ldots )$(left-associated) shape
 It will return the singleton list $[r]$ otherwise.
 $\sflat{\_}$ works the same  as $\sflataux{\_}$, except that it keeps
 the output type a regular expression, not a list.
 $\sflataux{\_}$  and $\sflat{\_}$ are only recursive on the
 first element of the list.
+$\sflataux{\_}'$ takes a list of regular expressions as input, and outputs
-With $\sflataux{}$ a preliminary to the closed form can be stated,
+a list of regular expressions.
-where the derivative of $r_1 \cdot r_2 \backslash s$ can be
+The use of $\sflataux{\_}$ and $\sflataux{\_}'$ is clear once we have
-flattened into a list whose head and tail meet the description
+$\textit{createdBySequence}$ defined:
-we gave earlier.
+\begin{center}
+	\begin{mathpar}
+		\inferrule{\mbox{}}{\textit{createdBySequence}\; (r_1 \cdot r_2)}
+		\inferrule{\textit{createdBySequence} \; r_1}{\textit{createdBySequence} \;
+		(r_1 + r_2)}
+	\end{mathpar}
+\end{center}
+\noindent
+The predicate $\textit{createdBySequence}$ is used to describe the shape of
+the derivative regular expressions $(r_1\cdot r_2) \backslash s$:
+\begin{lemma}\label{recursivelyDerseq}
+	It is always the case that
+	\begin{center}
+		$\textit{createdBySequence} \; ( (r_1\cdot r_2) \backslash_r s) $
+	\end{center}
+	holds.
+\end{lemma}
+\begin{proof}
+	By a reverse induction on the string $s$, where the inductive cases are $[]$
+	and $xs  @ [x]$.
+\end{proof}
+\noindent
+If we have a regular expression $r$ whose shpae
+fits into those described by $\textit{createdBySequence}$,
+then we can convert between
+$r \backslash_r c$ and $(\sflataux{r}) \backslash_r c$ with
+$\sflataux{\_}'$:
+\begin{lemma}\label{sfauIdemDer}
+	If $\textit{createdBySequence} \; r$, then
+	\begin{center}
+		$\sflataux{ r \backslash_r c} =
+		\llparenthesis (\map \; (\_ \backslash_r c) \; (\sflataux{r}) ) \rrparenthesis''$
+	\end{center}
+	holds.
+\end{lemma}
+\begin{proof}
+	By a simple induction on the inductive cases of $\textit{createdBySequence}.
+	$
+\end{proof}
+Now we are ready to express
+the shape of $r_1 \cdot r_2 \backslash s$
 \begin{lemma}\label{seqSfau0}
-	$\sflataux{\rders{(r_1 \cdot r_2) \backslash s }} = (r_1 \backslash_r s) \cdot r_2
+	$\sflataux{(r_1 \cdot r_2) \backslash_r s} = (r_1 \backslash_r s) \cdot r_2
 	:: (\map \; (r_2 \backslash_r \_) \; (\textit{Suffix} \; s \; r1))$
 \end{lemma}
 \begin{proof}
-	By an induction on the string $s$, where the inductive cases
+	By a reverse induction on the string $s$, where the inductive cases
-	are split as $[]$ and $xs @ [x]$.
+	are $[]$ and $xs @ [x]$.
-	Note the key identify holds:
+	For the inductive case, we know that $\textit{createdBySequence} \; ((r_1 \cdot r_2)
+	\backslash_r xs)$ holds from lemma \ref{recursivelyDerseq},
+	which can be used to prove
 	\[
 		\map \; (r_2 \backslash_r \_) \; (\vsuf{[x]}{(r_1 \backslash_r xs)}) \;\; @ \;\;
 		\map \; (\_ \backslash_r x) \; (\map \; (r_2 \backslash \_) \; (\vsuf{xs}{r_1}))
 	\]
 	=
 	\[
 		\map \; (r_2 \backslash_r \_) \; (\vsuf{xs @ [x]}{r_1})
 	\]
-	This enables the inductive case to go through.
+	using lemma \ref{sfauIdemDer}.
+	This equality enables the inductive case to go through.
 \end{proof}
 \noindent
-Note that this lemma does $\mathbf{not}$ depend on any
+This lemma says that $(r_1\cdot r_2)\backslash s$
-specific definitions we used,
+can be flattened into a list whose head and tail meet the description
-allowing people investigating derivatives to get an alternative
+we gave earlier.
-view of what $r_1 \cdot r_2$ is.
+%Note that this lemma does $\mathbf{not}$ depend on any
+%specific definitions we used,
-Now we are able to use this for the intuition that
+%allowing people investigating derivatives to get an alternative
-the different ways in which regular expressions are
+%view of what $r_1 \cdot r_2$ is.
-nested do not matter under $\rsimp{}$:
-\begin{center}
+We now use $\textit{createdBySequence}$ and
-	$\rsimp{r} \stackrel{?}{\sequal} \rsimp{r'}$ if $r = \sum [r_1, r_2, r_3, \ldots]$
+$\sflataux{\_}$ to describe an intuition
-	and $r' =(\ldots ((r_1 + r_2) + r_3) + \ldots)$
+behind the closed form of the sequence closed form.
-\end{center}
+If two regular expressions only differ in the way their
-Simply wrap with $\sum$ constructor and add
+alternatives are nested, then we should be able to get the same result
-simplifications to both sides of \ref{seqSfau0}
+once we apply simplification to both of them:
-and one gets
+\begin{lemma}\label{sflatRsimpeq}
-\begin{corollary}\label{seqClosedFormGeneral}
+	If $r$ is created from a sequence through
+	a series of derivatives
+	(i.e. if $\textit{createdBySequence} \; r$ holds),
+	and that $\sflataux{r} = rs$,
+	then we have
+	that
+	\begin{center}
+		$\textit{rsimp} \; r = \textit{rsimp} \; (\sum \; rs)$
+	\end{center}
+	holds.
+\end{lemma}
+\begin{proof}
+	By an induction on the inductive cases of $\textit{createdBySequence}$.
+\end{proof}
+Now we are ready for the closed form
+for the sequence regular expressions (without the inner applications
+of simplifications):
+\begin{lemma}\label{seqClosedFormGeneral}
 	$\rsimp{\sflat{(r_1 \cdot r_2) \backslash s} }
 	=\rsimp{(\sum (  (r_1 \backslash s) \cdot r_2 ::
 	\map\; (r_2 \backslash \_) \; (\vsuf{s}{r_1})))}$
-\end{corollary}
+\end{lemma}
+\begin{proof}
+	We know that
+	$\sflataux{(r_1 \cdot r_2) \backslash_r s} = (r_1 \backslash_r s) \cdot r_2
+	:: (\map \; (r_2 \backslash_r \_) \; (\textit{Suffix} \; s \; r1))$
+	holds
+	by lemma \ref{seqSfau0}.
+	This allows the theorem to go through because of lemma \ref{sflatRsimpeq}.
+\end{proof}
 Together with the idempotency property of $\rsimp{}$ (lemma \ref{rsimpIdem}),
-it is possible to convert the above lemma to obtain a "closed form"
+it is possible to convert the above lemma to obtain the
+proper closed form for $\backslash_{rsimps}$ rather than $\backslash_r$:
 for  derivatives nested with simplification:
-\begin{lemma}\label{seqClosedForm}
+\begin{theorem}\label{seqClosedForm}
 	$\rderssimp{(r_1 \cdot r_2)}{s} = \rsimp{(\sum ((r_1 \backslash s) \cdot r_2 )
 	:: (\map \; (r_2 \backslash \_) (\vsuf{s}{r_1})))}$
-\end{lemma}
+\end{theorem}
 \begin{proof}
-	By a case analysis of string $s$.
+	By a case analysis of the string $s$.
-	When $s$ is empty list, the rewrite is straightforward.
+	When $s$ is an empty list, the rewrite is straightforward.
-	When $s$ is a list, one could use the corollary \ref{seqSfau0},
+	When $s$ is a non-empty list, the
-	and lemma \ref{Simpders} to rewrite the left-hand-side.
+	lemmas \ref{seqClosedFormGeneral} and \ref{Simpders} apply,
-\end{proof}
+	making the proof go through.
-As a corollary for this closed form, one can estimate the size
+\end{proof}
-of the sequence derivative $r_1 \cdot r_2 \backslash_r s$ using
-an easier-to-handle expression:
-\begin{corollary}\label{seqEstimate1}
-	\begin{center}
-		$\llbracket \rderssimp{(r_1 \cdot r_2)}{s} \rrbracket_r = \llbracket \rsimp{(\sum ((r_1 \backslash s) \cdot r_2 )
-		:: (\map \; (r_2 \backslash \_) (\vsuf{s}{r_1})))} \rrbracket_r$
-	\end{center}
-\end{corollary}
-\noindent
 \subsubsection{Closed Forms for Star Regular Expressions}
-We have shown how to control the size of the sequence regular expression $r_1\cdot r_2$ using
+The closed form for the star regular expression involves similar tricks
-the "closed form" of $(r_1 \cdot r_2) \backslash s$ and then
+for the sequence regular expression.
-the property of the $\distinct$ function.
+The $\textit{Suffix}$ function is now replaced by something
-Now we try to get a bound on $r^* \backslash s$ as well.
+slightly more complex, because the growth pattern of star
-Again, we first look at how a star's derivatives evolve, if they grow maximally:
+regular expressions' derivatives is a bit different:
 \begin{center}
+	\begin{tabular}{lclc}
-	$r^* \quad \longrightarrow_{\backslash c}  \quad   (r\backslash c)  \cdot  r^* \quad \longrightarrow_{\backslash c'}  \quad
+		$r^* $ & $\longrightarrow_{\backslash c}$ &
-	r \backslash cc'  \cdot r^* + r \backslash c' \cdot r^*  \quad \longrightarrow_{\backslash c''} \quad
+		$(r\backslash c)  \cdot  r^*$ & $\longrightarrow_{\backslash c'}$\\
-	(r_1 \backslash cc'c'' \cdot r^* + r \backslash c'') + (r \backslash c'c'' \cdot r^* + r \backslash c'' \cdot r^*)   \quad \longrightarrow_{\backslash c'''}
+		\\
-	\quad \ldots$
+		$r \backslash cc'  \cdot r^* + r \backslash c' \cdot r^*$ &
+		$\longrightarrow_{\backslash c''}$ &
+		$(r_1 \backslash cc'c'' \cdot r^* + r \backslash c'') +
+		(r \backslash c'c'' \cdot r^* + r \backslash c'' \cdot r^*)$ &
+		$\longrightarrow_{\backslash c'''}$ \\
+		\\
+		$\ldots$\\
+	\end{tabular}
 \end{center}
 When we have a string $s = c :: c' :: c'' \ldots$  such that $r \backslash c$, $r \backslash cc'$, $r \backslash c'$,
 $r \backslash cc'c''$, $r \backslash c'c''$, $r\backslash c''$ etc. are all nullable,
-the number of terms in $r^* \backslash s$ will grow exponentially, causing the size
+the number of terms in $r^* \backslash s$ will grow exponentially rather than linearly
-of the derivatives $r^* \backslash s$ to grow exponentially, even if we do not
+in the sequence case.
-count the possible size explosions of $r \backslash c$ themselves.
+The good news is that the function $\textit{rsimp}$ will again
+ignore the difference between differently nesting patterns of alternatives,
-Thanks to $\rflts$ and $\rDistinct$, we are able to open up regular expressions like
+and the exponentially growing star derivative like
-$(r_1 \backslash cc'c'' \cdot r^* + r \backslash c'') +
+\begin{center}
-(r \backslash c'c'' \cdot r^* + r \backslash c'' \cdot r^*) $
+	$(r_1 \backslash cc'c'' \cdot r^* + r \backslash c'') +
-into $\RALTS{[r_1 \backslash cc'c'' \cdot r^*, r \backslash c'',
+	(r \backslash c'c'' \cdot r^* + r \backslash c'' \cdot r^*) $
-r \backslash c'c'' \cdot r^*, r \backslash c'' \cdot r^*]}$
+\end{center}
-and then de-duplicate terms of the form $r\backslash s' \cdot r^*$ ($s'$ being a substring of $s$).
+can be treated as
+\begin{center}
+	$\RALTS{[r_1 \backslash cc'c'' \cdot r^*, r \backslash c'',
+	r \backslash c'c'' \cdot r^*, r \backslash c'' \cdot r^*]}$
+\end{center}
+which can be de-duplicated by $\rDistinct$
+and therefore bounded finitely.
+and then de-duplicate terms of the form  ($s'$ being a substring of $s$).
 This allows us to use a similar technique as $r_1 \cdot r_2$ case,
-where the crux is to get an equivalent form of
-$\rderssimp{r^*}{s}$ with shape $\rsimp{\sum rs}$.
+Now the crux of this section is finding a suitable description
-This requires generating
+for $rs$ where
-all possible sub-strings $s'$ of $s$
+\begin{center}
-such that $r\backslash s' \cdot r^*$ will appear
+	$\rderssimp{r^*}{s} = \rsimp{\sum rs}$.
-as a term in $(r^*) \backslash s$.
+\end{center}
-The first function we define is a single-step
+holds.
-updating function $\starupdate$, which takes three arguments as input:
+In addition, the list $rs$
-the new character $c$ to take derivative with,
+shall be in the form of
-the regular expression
+$\map \; (\lambda s'. r\backslash s' \cdot r^*) \; Ss$.
-$r$ directly under the star $r^*$, and the
+The $Ss$ is a list of strings, and for example in the sequence
-list of strings $sSet$ for the derivative $r^* \backslash s$
+closed form it is specified as $\textit{Suffix} \; s \; r_1$.
-up til this point
+To get $Ss$ for the star regular expression,
-such that $(r^*) \backslash s = \sum_{s' \in sSet} (r\backslash s') \cdot r^*$
+we need to introduce $\starupdate$ and $\starupdates$:
-(the equality is not exact, more on this later).
 \begin{center}
 	\begin{tabular}{lcl}
 		$\starupdate \; c \; r \; [] $ & $\dn$ & $[]$\\
 		$\starupdate \; c \; r \; (s :: Ss)$ & $\dn$ & \\
 						     & & $\textit{if} \;
 						     \starupdate \; c \; r \; Ss)$ \\
 						     & & $\textit{else} \;\; (s @ [c]) :: (
 						     \starupdate \; c \; r \; Ss)$
 	\end{tabular}
 \end{center}
-\noindent
-As a generalisation from characters to strings,
-$\starupdates$ takes a string instead of a character
-as the first input argument, and is otherwise the same
-as $\starupdate$.
 \begin{center}
 	\begin{tabular}{lcl}
 		$\starupdates \; [] \; r \; Ss$ & $=$ & $Ss$\\
 		$\starupdates \; (c :: cs) \; r \; Ss$ &  $=$ &  $\starupdates \; cs \; r \; (
 		\starupdate \; c \; r \; Ss)$
 	\end{tabular}
 \end{center}
 \noindent
-For the star regular expression,
+Assuming we have that
-its derivatives can be seen as  a nested gigantic
+\begin{center}
-alternative similar to that of sequence regular expression's derivatives,
+	$\rderssimp{r^*}{s} = \rsimp{(\sum \map \; (\lambda s'. r\backslash s' \cdot r^*) \; Ss)}$.
-and therefore need
+\end{center}
-to be ``straightened out" as well.
+holds.
-The function for this would be $\hflat{}$ and $\hflataux{}$.
+The idea of $\starupdate$ and $\starupdates$
+is to update $Ss$ when another
+derivative is taken on $\rderssimp{r^*}{s}$
+w.r.t a character $c$ and a string $s'$
+respectively.
+Both $\starupdate$ and $\starupdates$ take three arguments as input:
+the new character $c$ or string $s$ to take derivative with,
+the regular expression
+$r$ under the star $r^*$, and the
+list of strings $Ss$ for the derivative $r^* \backslash s$
+up until this point
+such that
+\begin{center}
+$(r^*) \backslash s = \sum_{s' \in sSet} (r\backslash s') \cdot r^*$
+\end{center}
+is satisfied.
+Functions $\starupdate$ and $\starupdates$ characterise what the
+star derivatives will look like once ``straightened out'' into lists.
+The helper functions for such operations will be similar to
+$\sflat{\_}$, $\sflataux{\_}$ and $\sflataux{\_}$, which we defined for sequence.
+We use similar symbols to denote them, with a $*$ subscript to mark the difference.
 \begin{center}
 	\begin{tabular}{lcl}
 		$\hflataux{r_1 + r_2}$ & $\dn$ & $\hflataux{r_1} @ \hflataux{r_2}$\\
 		$\hflataux{r}$ & $\dn$ & $[r]$
 	\end{tabular}
 		$\hflat{r_1 + r_2}$ & $\dn$ & $\sum (\hflataux {r_1} @ \hflataux {r_2}) $\\
 		$\hflat{r}$ & $\dn$ & $r$
 	\end{tabular}
 \end{center}
 \noindent
-%MAYBE TODO: introduce createdByStar
+These definitions are tailor-made for dealing with alternatives that have
-Again these definitions are tailor-made for dealing with alternatives that have
+originated from a star's derivatives.
-originated from a star's derivatives, so we do not attempt to open up all possible
+A typical star derivative always has the structure of a balanced binary tree:
-regular expressions of the form $\RALTS{rs}$, where $\textit{rs}$ might not contain precisely 2
+\begin{center}
-elements.
+	$(r_1 \backslash cc'c'' \cdot r^* + r \backslash c'') +
-We give a predicate for such "star-created" regular expressions:
+	(r \backslash c'c'' \cdot r^* + r \backslash c'' \cdot r^*) $
-\begin{center}
+\end{center}
-	\begin{tabular}{lcr}
+All of the nested structures of alternatives
-	 &    &       $\createdByStar{(\RSEQ{ra}{\RSTAR{rb}}) }$\\
+generated from derivatives are binary, and therefore
-		$\createdByStar{r_1} \land \createdByStar{r_2} $ & $ \Longrightarrow$ & $\createdByStar{(r_1 + r_2)}$
+$\hflat{\_}$ and $\hflataux{\_}$ only deal with binary alternatives.
-	\end{tabular}
+$\hflat{\_}$ ``untangles'' like the following:
-\end{center}
+\[
+	\sum ((r_1 + r_2) + (r_3 + r_4))  + \ldots \;
-These definitions allows us the flexibility to talk about
+	\stackrel{\hflat{\_}}{\longrightarrow} \;
-regular expressions in their most convenient format,
+	\RALTS{[r_1, r_2, \ldots, r_n]}
-for example, flattened out $\RALTS{[r_1, r_2, \ldots, r_n]} $
+\]
-instead of binary-nested: $((r_1 + r_2) + (r_3 + r_4)) + \ldots$.
+Here is a lemma stating the recursive property of $\starupdate$ and $\starupdates$,
-These definitions help express that certain classes of syntatically
+with the helpers $\hflat{\_}$ and $\hflataux{\_}$\footnote{The function $\textit{concat}$ takes a list of lists
-distinct regular expressions are actually the same under simplification.
+			and merges each of the element lists to form a flattened list.}:
-This is not entirely true for annotated regular expressions:
+\begin{lemma}\label{stupdateInduct1}
-%TODO: bsimp bders \neq bderssimp
+	\mbox
-\begin{center}
+	For a list of strings $Ss$, the following hold.
-	$(1+ (c\cdot \ASEQ{bs}{c^*}{c} ))$
+	\begin{itemize}
-\end{center}
+		\item
-For bit-codes, the order in which simplification is applied
+			If we do a derivative on the terms
-might cause a difference in the location they are placed.
+			$r\backslash_r s \cdot r^*$ (where $s$ is taken from the list $Ss$),
-If we want something like
+			the result will be the same as if we apply $\starupdate$ to $Ss$.
-\begin{center}
+			\begin{center}
-	$\bderssimp{r}{s} \myequiv \bsimp{\bders{r}{s}}$
+				\begin{tabular}{c}
-\end{center}
+			$\textit{concat} \; (\map \; (\hflataux{\_} \circ ( (\_\backslash_r x)
-Some "canonicalization" procedure is required,
+			\circ (\lambda s.\;\; (r \backslash_r s) \cdot r^*)))\; Ss )\;
-which either pushes all the common bitcodes to nodes
+			$\\
-as senior as possible:
+			\\
-\begin{center}
+			$=$ \\
-	$_{bs}(_{bs_1 @ bs'}r_1 + _{bs_1 @ bs''}r_2) \rightarrow _{bs @ bs_1}(_{bs'}r_1 + _{bs''}r_2) $
+			\\
-\end{center}
+			$\map \; (\lambda s. (r \backslash_r s) \cdot (r^*)) \;
-or does the reverse. However bitcodes are not of interest if we are talking about
+			(\starupdate \; x \; r \; Ss)$
-the $\llbracket r \rrbracket$ size of a regex.
+				\end{tabular}
-Therefore for the ease and simplicity of producing a
+			\end{center}
-proof for a size bound, we are happy to restrict ourselves to
+		\item
-unannotated regular expressions, and obtain such equalities as
+			$\starupdates$ is ``composable'' w.r.t a derivative.
-\begin{lemma}
+			It piggybacks the character $x$ to the tail of the string
-	$\rsimp{r_1 + r_2} = \rsimp{\RALTS{\hflataux{r_1} @ \hflataux{r_2}}}$
+			$xs$.
+			\begin{center}
+				\begin{tabular}{c}
+					$\textit{concat} \; (\map \; \hflataux{\_} \;
+					(\map \; (\_\backslash_r x) \;
+					(\map \; (\lambda s.\;\; (r \backslash_r s) \cdot
+					(r^*) ) \; (\starupdates \; xs \; r \; Ss))))$\\
+					\\
+					$=$\\
+					\\
+					$\map \; (\lambda s.\;\; (r\backslash_r s) \cdot (r^*)) \;
+					(\starupdates \; (xs @ [x]) \; r \; Ss)$
+				\end{tabular}
+			\end{center}
+	\end{itemize}
+\end{lemma}
+\begin{proof}
+	Part 1 is by induction on $Ss$.
+	Part 2 is by induction on $xs$, where $Ss$ is left to take arbitrary values.
+\end{proof}
+Like $\textit{createdBySequence}$, we need
+a predicate for ``star-created'' regular expressions:
+\begin{center}
+	\begin{mathpar}
+		\inferrule{\mbox{}}{ \textit{createdByStar}\; \RSEQ{ra}{\RSTAR{rb}} }
+		\inferrule{  \textit{createdByStar} \; r_1\; \land  \; \textit{createdByStar} \; r_2 }{\textit{createdByStar} \; (r_1 + r_2) }
+	\end{mathpar}
+\end{center}
+\noindent
+All regular expressions created by taking derivatives of
+$r_1 \cdot (r_2)^*$ satisfy the $\textit{createdByStar}$ predicate:
+\begin{lemma}\label{starDersCbs}
+	$\textit{createdByStar} \; ((r_1 \cdot r_2^*) \backslash_r s) $ holds.
+\end{lemma}
+\begin{proof}
+	By a reverse induction on $s$.
+\end{proof}
+If a regular expression conforms to the shape of a star's derivative,
+then we can push an application of $\hflataux{\_}$ inside a derivative of it:
+\begin{lemma}\label{hfauPushin}
+	If $\textit{createdByStar} \; r$ holds, then
+	\begin{center}
+		$\hflataux{r \backslash_r c} = \textit{concat} \; (
+		\map \; \hflataux{\_} (\map \; (\_\backslash_r c) \;(\hflataux{r})))$
+	\end{center}
+	holds.
+\end{lemma}
+\begin{proof}
+	By an induction on the inductivev cases of $\textit{createdByStar}$.
+\end{proof}
+%This is not entirely true for annotated regular expressions:
+%%TODO: bsimp bders \neq bderssimp
+%\begin{center}
+%	$(1+ (c\cdot \ASEQ{bs}{c^*}{c} ))$
+%\end{center}
+%For bit-codes, the order in which simplification is applied
+%might cause a difference in the location they are placed.
+%If we want something like
+%\begin{center}
+%	$\bderssimp{r}{s} \myequiv \bsimp{\bders{r}{s}}$
+%\end{center}
+%Some "canonicalization" procedure is required,
+%which either pushes all the common bitcodes to nodes
+%as senior as possible:
+%\begin{center}
+%	$_{bs}(_{bs_1 @ bs'}r_1 + _{bs_1 @ bs''}r_2) \rightarrow _{bs @ bs_1}(_{bs'}r_1 + _{bs''}r_2) $
+%\end{center}
+%or does the reverse. However bitcodes are not of interest if we are talking about
+%the $\llbracket r \rrbracket$ size of a regex.
+%Therefore for the ease and simplicity of producing a
+%proof for a size bound, we are happy to restrict ourselves to
+%unannotated regular expressions, and obtain such equalities as
+%TODO: rsimp sflat
+% The simplification of a flattened out regular expression, provided it comes
+%from the derivative of a star, is the same as the one nested.
+Now we introduce an inductive property
+for $\starupdate$ and $\hflataux{\_}$.
+\begin{lemma}\label{starHfauInduct}
+	If we do derivatives of $r^*$
+	with a string that starts with $c$,
+	then flatten it out,
+	we obtain a list
+	of the shape $\sum_{s' \in sS} (r\backslash_r s') \cdot r^*$,
+	where $sS = \starupdates \; s \; r \; [[c]]$. Namely,
+	\begin{center}
+		$\hflataux{(\rders{( (\rder{c}{r_0})\cdot(r_0^*))}{s})} =
+		\map \; (\lambda s_1. (r_0 \backslash_r s_1) \cdot (r_0^*)) \;
+		(\starupdates \; s \; r_0 \; [[c]])$
+	\end{center}
+holds.
+\end{lemma}
+\begin{proof}
+	By an induction on $s$, the inductive cases
+	being $[]$ and $s@[c]$. The lemmas \ref{hfauPushin} and \ref{starDersCbs} are used.
+\end{proof}
+\noindent
+$\hflataux{\_}$ has a similar effect as $\textit{flatten}$:
+\begin{lemma}\label{hflatauxGrewrites}
+	$a :: rs \grewrites \hflataux{a} @ rs$
+\end{lemma}
+\begin{proof}
+	By induction on $a$. $rs$ is set to take arbitrary values.
+\end{proof}
+It is also not surprising that $\textit{rsimp}$ will cover
+the effect of $\hflataux{\_}$:
+\begin{lemma}\label{cbsHfauRsimpeq1}
+	$\rsimp{(r_1 + r_2)} = \rsimp{(\RALTS{\hflataux{r_1} @ \hflataux{r_2}})}$
 \end{lemma}
 \begin{proof}
 	By using the rewriting relation $\rightsquigarrow$
 \end{proof}
-%TODO: rsimp sflat
 And from this we obtain a proof that a star's derivative will be the same
 as if it had all its nested alternatives created during deriving being flattened out:
 For example,
-\begin{lemma}
+\begin{lemma}\label{hfauRsimpeq2}
 	$\createdByStar{r} \implies \rsimp{r} = \rsimp{\RALTS{\hflataux{r}}}$
 \end{lemma}
 \begin{proof}
-	By structural induction on $r$, where the induction rules are these of $\createdByStar{_}$.
+	By structural induction on $r$, where the induction rules
-\end{proof}
+	are these of $\createdByStar{\_}$.
-% The simplification of a flattened out regular expression, provided it comes
+	Lemma \ref{cbsHfauRsimpeq1} is used in the inductive case.
-%from the derivative of a star, is the same as the one nested.
+\end{proof}
+%Here is a corollary that states the lemma in
-We first introduce an inductive property
+%a more intuitive way:
-for $\starupdate$ and $\hflataux{\_}$,
+%\begin{corollary}
-it says if we do derivatives of $r^*$
+%	$\hflataux{r^* \backslash_r (c::xs)} = \map \; (\lambda s. (r \backslash_r s) \cdot
-with a string that starts with $c$,
+%	(r^*))\; (\starupdates \; c\; r\; [[c]])$
-then flatten it out,
+%\end{corollary}
-we obtain a list
+%\noindent
-of the shape $\sum_{s' \in sSet} (r\backslash_r s') \cdot r^*$,
+%Note that this is also agnostic of the simplification
-where $sSet = \starupdates \; s \; r \; [[c]]$.
+%function we defined, and is therefore of more general interest.
-\begin{lemma}\label{starHfauInduct}
-	$\hflataux{(\rders{( (\rder{c}{r_0})\cdot(r_0^*))}{s})} =
-	\map \; (\lambda s_1. (r_0 \backslash_r s_1) \cdot (r_0^*)) \;
-	(\starupdates \; s \; r_0 \; [[c]])$
-\end{lemma}
-\begin{proof}
-	By an induction on $s$, the inductive cases
-	being $[]$ and $s@[c]$.
-\end{proof}
-\noindent
-Here is a corollary that states the lemma in
-a more intuitive way:
-\begin{corollary}
-	$\hflataux{r^* \backslash_r (c::xs)} = \map \; (\lambda s. (r \backslash_r s) \cdot
-	(r^*))\; (\starupdates \; c\; r\; [[c]])$
-\end{corollary}
-\noindent
-Note that this is also agnostic of the simplification
-function we defined, and is therefore of more general interest.
-Now adding the $\rsimp{}$ bit for closed forms,
-we have
-\begin{lemma}
-	$a :: rs \grewrites \hflataux{a} @ rs$
-\end{lemma}
-\noindent
-giving us
-\begin{lemma}\label{cbsHfauRsimpeq1}
-	$\rsimp{a+b} = \rsimp{(\sum \hflataux{a} @ \hflataux{b})}$.
-\end{lemma}
-\noindent
-This yields
-\begin{lemma}\label{hfauRsimpeq2}
-	$\rsimp{r} = \rsimp{(\sum \hflataux{r})}$
-\end{lemma}
-\noindent
 Together with the rewriting relation
 \begin{lemma}\label{starClosedForm6Hrewrites}
-	$\map \; (\lambda s. (\rsimp{r \backslash_r s}) \cdot (r^*)) \; Ss
+	We have the following set of rewriting relations or equalities:
-	\scfrewrites
+	\begin{itemize}
-	\map \; (\lambda s. (\rsimp{r \backslash_r s}) \cdot (r^*)) \; Ss$
+		\item
-\end{lemma}
+			$\textit{rsimp} \; (r^* \backslash_r (c::s))
-\noindent
+			\sequal
-We obtain the closed form for star regular expression:
+			\sum \; ( ( \sum (\lambda s. (r\backslash_r s) \cdot r^*) \; (
-\begin{lemma}\label{starClosedForm}
+			\starupdates \; s \; r \; [ c::[]] ) ) )$
+		\item
+			$r \backslash_{rsimp} (c::s) = \textit{rsimp} \; ( (
+			\sum ( (\map \; (\lambda s_1. (r\backslash s_1) \; r^*) \;
+			(\starupdates \;s \; r \; [ c::[] ])))))$
+		\item
+			$\sum ( (\map \; (\lambda s. (r\backslash s) \; r^*) \; Ss))
+			\sequal
+			 \sum ( (\map \; (\lambda s. \textit{rsimp} \; (r\backslash s) \;
+			 r^*) \; Ss) )$
+		\item
+			$\map \; (\lambda s. (\rsimp{r \backslash_r s}) \cdot (r^*)) \; Ss
+			\scfrewrites
+			\map \; (\lambda s. (\rsimp{r \backslash_r s}) \cdot (r^*)) \; Ss$
+		\item
+			$( ( \sum ( ( \map \ (\lambda s. \;\;
+			(\textit{rsimp} \; (r \backslash_r s)) \cdot r^*) \; (\starupdates \;
+			s \; r \; [ c::[] ])))))$\\
+			$\sequal$\\
+			$( ( \sum ( ( \map \ (\lambda s. \;\;
+			( r \backslash_{rsimp} s)) \cdot r^*) \; (\starupdates \;
+			s \; r \; [ c::[] ]))))$\\
+	\end{itemize}
+\end{lemma}
+\begin{proof}
+	Part 1 leads to part 2.
+	The rest of them are routine.
+\end{proof}
+\noindent
+Next the closed form for star regular expressions can be derived:
+\begin{theorem}\label{starClosedForm}
 	$\rderssimp{r^*}{c::s} =
 	\rsimp{
 		(\sum (\map \; (\lambda s. (\rderssimp{r}{s})\cdot r^*) \;
 		(\starupdates \; s\; r \; [[c]])
 		)
 		)
 	}
 	$
-\end{lemma}
+\end{theorem}
 \begin{proof}
 	By an induction on $s$.
-	The lemmas \ref{rsimpIdem}, \ref{starHfauInduct}, and \ref{hfauRsimpeq2}
+	The lemmas \ref{rsimpIdem}, \ref{starHfauInduct}, \ref{starClosedForm6Hrewrites}
+	and \ref{hfauRsimpeq2}
 	are used.
+	In \ref{starClosedForm6Hrewrites}, the equalities are
+	used to link the LHS and RHS.
 \end{proof}
 %\end{center}
 \section{Bounding Closed Forms}
 In this section, we introduce how we formalised the bound
 on closed forms.
-We first prove that functions such as $\rflts$
+We first show that in general regular expressions up to a certain
+size are finite.
+Then we prove that functions such as $\rflts$
 will not cause the size of r-regular expressions to grow.
 Putting this together with a general bound
 on the finiteness of distinct regular expressions
-smaller than a certain size, we obtain a bound on
+up to a certain size, we obtain a bound on
 the closed forms.
+\subsection{Finiteness of Distinct Regular Expressions}
+We define the set of regular expressions whose size are no more than
+a certain size $N$ as $\textit{sizeNregex} \; N$:
+\[
+	\textit{sizeNregex} \; N \dn \{r\; \mid \;  \llbracket r \rrbracket_r \leq N \}
+\]
+We have that $\textit{sizeNregex} \; N$ is always a finite set:
+\begin{lemma}\label{finiteSizeN}
+	$\textit{finite} \; (\textit{sizeNregex} \; N)$ holds.
+\end{lemma}
+\begin{proof}
+	By splitting the set $\textit{sizeNregex} \; (N + 1)$ into
+	subsets by their categories:
+	$\{\ZERO, \ONE, c\}$, $\{* `` \textit{sizeNregex} \; N\}$,
+	and so on. Each of these subsets are finitely bounded.
+\end{proof}
+\noindent
+From this we get a corollary that
+if forall $r \in rs$, $\rsize{r} \leq N$, then the output of
+$\rdistinct{rs}{\varnothing}$ is a list of regular
+expressions of finite size depending on $N$ only.
+\begin{corollary}\label{finiteSizeNCorollary}
+	$\rsize{\rdistinct{rs}{\varnothing}} \leq c_N * N$ holds,
+	where the constant $c_N$ is equal to $\textit{card} \; (\textit{sizeNregex} \;
+	N)$.
+\end{corollary}
+\begin{proof}
+	For all $r$ in
+	$\textit{set} \; (\rdistinct{rs}{\varnothing})$,
+	it is always the case that $\rsize{r} \leq N$.
+	In addition, the list length is bounded by
+	$c_N$, yielding the desired bound.
+\end{proof}
+\noindent
+This fact will be handy in estimating the closed form sizes.
+%We have proven that the size of the
+%output of $\textit{rdistinct} \; rs' \; \varnothing$
+%is bounded by a constant $N * c_N$ depending only on $N$,
+%provided that each of $rs'$'s element
+%is bounded by $N$.
 \subsection{$\textit{rsimp}$ Does Not Increment the Size}
 Although it seems evident, we need a series
 of non-trivial lemmas to establish that functions such as $\rflts$
 do not cause the regular expressions to grow.
 \begin{proof}
 	By \ref{rsimpMonoLemmas}.
 \end{proof}
 \subsection{Estimating the Closed Forms' sizes}
-We now summarize the closed forms below:
+We recap the closed forms we obtained
+earlier by putting them together down below:
 \begin{itemize}
 	\item
 		$\rderssimp{(\sum rs)}{s} \sequal
 		\sum \; (\map \; (\rderssimp{\_}{s}) \; rs)$
 	\item
 which will each have a size uppder bound
 according to inductive hypothesis, which controls $r \backslash s$.
 We elaborate the above reasoning by a series of lemmas
 below, where straightforward proofs are omitted.
-\begin{lemma}
-	If $\forall r \in rs. \rsize{r} $ is less than or equal to $N$,
-	and $\textit{length} \; rs$ is less than or equal to $l$,
-	then $\rsize{\sum rs}$ is less than or equal to $l*N + 1$.
-\end{lemma}
-\noindent
-If we define all regular expressions with size no
-more than $N$ as $\sizeNregex \; N$:
-\[
-	\sizeNregex \; N \dn  \{r \mid \rsize{r} \leq N \}
-\]
-Then such set is finite:
-\begin{lemma}\label{finiteSizeN}
-	$\textit{isFinite}\; (\sizeNregex \; N)$
-\end{lemma}
-\begin{proof}
-	By overestimating the set $\sizeNregex \; N + 1$
-	using union of sets like
-	$\{r_1 \cdot r_2 \mid r_1 \in A
-		\text{and}
-	r_2 \in A\}
-	$ where $A = \sizeNregex \; N$.
-\end{proof}
-\noindent
-From this we get a corollary that
-if forall $r \in rs$, $\rsize{r} \leq N$, then the output of
-$\rdistinct{rs}{\varnothing}$ is a list of regular
-expressions of finite size depending on $N$ only.
-\begin{corollary}\label{finiteSizeNCorollary}
-	Assumes that for all $r \in rs. \rsize{r} \leq N$,
-	and the cardinality of $\sizeNregex \; N$ is $c_N$
-	then$\rsize{\rdistinct{rs}{\varnothing}} \leq c*N$.
-\end{corollary}
-\noindent
-We have proven that the output of $\rdistinct{rs'}{\varnothing}$
-is bounded by a constant $c_N$ depending only on $N$,
-provided that each of $rs'$'s element
-is bounded by $N$.
 We want to apply it to our setting $\rsize{\rsimp{\sum rs}}$.
 We show that $\rdistinct$ and $\rflts$
 working together is at least as
 good as $\rdistinct{}{}$ alone, which can be written as
 We cannot simply prove how each helper function
 reduces the size and then put them together:
 From
 \begin{center}
 $\llbracket  \textit{rflts}\; rs \rrbracket_r \leq
-	\llbracket \; \textit{rs} \rrbracket_r$
+	\llbracket  \textit{rs} \rrbracket_r$
 \end{center}
 and
 \begin{center}
 $\llbracket  \textit{rdistinct} \; rs \; \varnothing \leq
 \llbracket rs \rrbracket_r$
 \end{center}
-one cannot imply
+one cannot infer
 \begin{center}
 	$\llbracket \rdistinct{(\rflts \; \textit{rs})}{\varnothing} \rrbracket_r
 	\leq
 	\llbracket \rdistinct{rs}{\varnothing}  \rrbracket_r  $.
 \end{center}
-What we can imply is that
+What we can infer is that
 \begin{center}
 	$\llbracket \rdistinct{(\rflts \; \textit{rs})}{\varnothing} \rrbracket_r
 	\leq
 	\llbracket rs \rrbracket_r$
 \end{center}
 but this estimate is too rough and $\llbracket rs \rrbracket_r$	is unbounded.
 The way we
-get through this is by first proving a more general lemma
+get around this is by first proving a more general lemma
 (so that the inductive case goes through):
 \begin{lemma}\label{fltsSizeReductionAlts}
 	If we have three accumulator sets:
 	$noalts\_set$, $alts\_set$ and $corr\_set$,
 	satisfying:
 	\end{tabular}
 	\end{center}
 		holds.
 \end{lemma}
 \noindent
-We need to split the accumulator into two parts: the part
+We split the accumulator into two parts: the part
 which contains alternative regular expressions ($alts\_set$), and
 the part without any of them($noalts\_set$).
+This is because $\rflts$ opens up the alternatives in $as$,
+causing the accumulators on both sides of the inequality
+to diverge slightly.
+If we want to compare the accumulators that are not
+perfectly in sync, we need to consider the alternatives and non-alternatives
+separately.
 The set $corr\_set$ is the corresponding set
-of $alts\_set$ with all elements under the $\sum$ constructor
+of $alts\_set$ with all elements under the alternative constructor
 spilled out.
 \begin{proof}
 	By induction on the list $as$. We make use of lemma \ref{rdistinctConcat}.
 \end{proof}
 By setting all three sets to the empty set, one gets the desired size estimate:
 \end{corollary}
 \begin{proof}
 	By using the lemma \ref{fltsSizeReductionAlts}.
 \end{proof}
 \noindent
-The intuition is that if we remove duplicates from the $\textit{LHS}$, at least the same amount of
+The intuition for why this is true
+is that if we remove duplicates from the $\textit{LHS}$, at least the same amount of
 duplicates will be removed from the list $\textit{rs}$ in the $\textit{RHS}$.
 Now this $\rsimp{\sum rs}$ can be estimated using $\rdistinct{rs}{\varnothing}$:
 \begin{lemma}\label{altsSimpControl}
 	$\rsize{\rsimp{\sum rs}} \leq \rsize{\rdistinct{rs}{\varnothing}}+ 1$
 \end{lemma}
 \begin{proof}
-	By using \ref{interactionFltsDB}.
+	By using corollary \ref{interactionFltsDB}.
 \end{proof}
 \noindent
 This is a key lemma in establishing the bounds on all the
 closed forms.
 With this we are now ready to control the sizes of
-$(r_1 \cdot r_2 )\backslash s$, $r^* \backslash s$.
+$(r_1 \cdot r_2 )\backslash s$ and $r^* \backslash s$.
-\begin{theorem}
+\begin{theorem}\label{rBound}
 	For any regex $r$, $\exists N_r. \forall s. \; \rsize{\rderssimp{r}{s}} \leq N_r$
 \end{theorem}
 \noindent
 \begin{proof}
 	We prove this by induction on $r$. The base cases for $\RZERO$,
 	\map \; (r_2\backslash_{rsimp} \_)\; (\vsuf{s}{r}))}{\varnothing} \rrbracket_r  + 1$ & (2) \\
 											     & $\leq$ & $2 + N_1 + \rsize{r_2} + (N_2 * (card\;(\sizeNregex \; N_2)))$ & (3)\\
 \end{tabular}
 \end{center}
 \noindent
-(1) is by the corollary \ref{seqEstimate1}.
+(1) is by theorem \ref{seqClosedForm}.
 (2) is by \ref{altsSimpControl}.
 (3) is by \ref{finiteSizeNCorollary}.
 Combining the cases when $s = []$ and $s \neq []$, we get (4):
 					 & $\leq$ & $1 + (\textit{card} (\sizeNregex \; (N + n_r)))
 	* (1 + (N + n_r)) $ & (7)\\
 \end{tabular}
 \end{center}
 \noindent
-(5) is by the lemma  \ref{starClosedForm}.
+(5) is by theorem \ref{starClosedForm}.
 (6) is by \ref{altsSimpControl}.
-(7) is by \ref{finiteSizeNCorollary}.
+(7) is by corollary \ref{finiteSizeNCorollary}.
 Combining with the case when $s = []$, one gets
 \begin{center}
 	\begin{tabular}{lcll}
 		$\rsize{r^* \backslash_r s}$ & $\leq$ & $max \; n_r \; 1 + (\textit{card} (\sizeNregex \; (N + n_r)))
 		* (1 + (N + n_r)) $ & (8)\\
 & $\leq$ & $\llbracket (\sum (\map \; (\_ \backslash_{rsimp} s)  \; rs) ) \rrbracket_r $  & (10) \\
 & $\leq$ & $1 + N * (length \; rs) $ & (11)\\
 	\end{tabular}
 \end{center}
 \noindent
-(9) is by \ref{altsClosedForm}, (10) by \ref{rsimpSize} and (11) by inductive hypothesis.
+(9) is by theorem \ref{altsClosedForm}, (10) by lemma \ref{rsimpMono} and (11) by inductive hypothesis.
 Combining with the case when $s = []$, one gets
 \begin{center}
 	\begin{tabular}{lcll}
 		$\rsize{\sum rs \backslash_r s}$ & $\leq$ & $max \; \rsize{\sum rs} \; 1+N*(length \; rs)$
 						 & (12)\\
 	\end{tabular}
 \end{center}
-(4), (8), and (12) are all the inductive cases proven.
+We have all the inductive cases proven.
 \end{proof}
+This leads to our main result on the size bound:
 \begin{corollary}
-	For any regex $a$, $\exists N_r. \forall s. \; \rsize{\bderssimp{a}{s}} \leq N_r$
+	For any annotated regular expression $a$, $\exists N_r. \forall s. \; \rsize{\bderssimp{a}{s}} \leq N_r$
 \end{corollary}
 \begin{proof}
-	By \ref{sizeRelations}.
+	By lemma \ref{sizeRelations} and theorem \ref{rBound}.
 \end{proof}
 \noindent
 %----------------------------------------------------------------------------------------
 %	SECTION 3
 %----------------------------------------------------------------------------------------
-\subsection{A Closed Form for the Sequence Regular Expression}
+\section{Comments and Future Improvements}
-\noindent
+\subsection{Some Experimental Results}
-Before we get to the proof that says the intermediate result of our lexer will
-remain finitely bounded, which is an important efficiency/liveness guarantee,
-we shall first develop a few preparatory properties and definitions to
-make the process of proving that a breeze.
-We define rewriting relations for $\rrexp$s, which allows us to do the
-same trick as we did for the correctness proof,
-but this time we will have stronger equalities established.
 What guarantee does this bound give us?
 Whatever the regex is, it will not grow indefinitely.
 Take our previous example $(a + aa)^*$ as an example:
 \begin{center}
 	\begin{tabular}{@{}c@{\hspace{0mm}}c@{\hspace{0mm}}c@{}}
 		\begin{tikzpicture}
 				scaled ticks=false,
 				axis lines=left,
 				width=5cm,
 				height=4cm,
 				legend entries={$(a + aa)^*$},
-				legend pos=north west,
+				legend pos=south east,
 				legend cell align=left]
 				\addplot[red,mark=*, mark options={fill=white}] table {a_aa_star.data};
 			\end{axis}
 		\end{tikzpicture}
 	\end{tabular}
 Given that $l_{N_2}$ is roughly the size $4^{N_2}$, the size bound $\llbracket \bderssimp{r_1 \cdot r_2}{s} \rrbracket$
 inflates the size bound of $\llbracket \bderssimp{r_2}{s} \rrbracket$ with the function
 $f(x) = x * 2^x$.
 This means the bound we have will surge up at least
 tower-exponentially with a linear increase of the depth.
-For a regex of depth $n$, the bound
-would be approximately $4^n$.
+One might be quite skeptical about what this non-elementary
+bound can bring us.
-Test data in the graphs from randomly generated regular expressions
+It turns out that the giant bounds are far from being hit.
-shows that the giant bounds are far from being hit.
+Here we have some test data from randomly generated regular expressions:
-%a few sample regular experessions' derivatives
+\begin{figure}[H]
-%size change
+	\begin{tabular}{@{}c@{\hspace{2mm}}c@{\hspace{0mm}}c@{}}
-%TODO: giving regex1_size_change.data showing a few regular expressions' size changes
-%w;r;t the input characters number, where the size is usually cubic in terms of original size
-%a*, aa*, aaa*, .....
-%randomly generated regular expressions
-\begin{figure}{H}
-	\begin{tabular}{@{}c@{\hspace{0mm}}c@{\hspace{0mm}}c@{}}
 		\begin{tikzpicture}
 			\begin{axis}[
-				xlabel={number of characters},
+				xlabel={$n$},
 				x label style={at={(1.05,-0.05)}},
 				ylabel={regex size},
 				enlargelimits=false,
 				xtick={0,5,...,30},
 				xmax=33,
 				%ymax=1000,
 				%ytick={0,100,...,1000},
 				scaled ticks=false,
 				axis lines=left,
-				width=5cm,
+				width=4.75cm,
-				height=4cm,
+				height=3.8cm,
 				legend entries={regex1},
-				legend pos=north west,
+				legend pos=north east,
 				legend cell align=left]
 				\addplot[red,mark=*, mark options={fill=white}] table {regex1_size_change.data};
 			\end{axis}
 		\end{tikzpicture}
 &
 \begin{tikzpicture}
 	  \begin{axis}[
 		  xlabel={$n$},
 		  x label style={at={(1.05,-0.05)}},
 		  %ylabel={time in secs},
 		  xmax=33,
 		  %ymax=1000,
 		  %ytick={0,100,...,1000},
 		  scaled ticks=false,
 		  axis lines=left,
-		  width=5cm,
+		  width=4.75cm,
-		  height=4cm,
+		  height=3.8cm,
 		  legend entries={regex2},
-		  legend pos=north west,
+		  legend pos=south east,
 		  legend cell align=left]
 		  \addplot[blue,mark=*, mark options={fill=white}] table {regex2_size_change.data};
 	  \end{axis}
 \end{tikzpicture}
 &
 \begin{tikzpicture}
 	  \begin{axis}[
 		  xlabel={$n$},
 		  x label style={at={(1.05,-0.05)}},
 		  %ylabel={time in secs},
 		  xmax=33,
 		  %ymax=1000,
 		  %ytick={0,100,...,1000},
 		  scaled ticks=false,
 		  axis lines=left,
-		  width=5cm,
+		  width=4.75cm,
-		  height=4cm,
+		  height=3.8cm,
 		  legend entries={regex3},
-		  legend pos=north west,
+		  legend pos=south east,
 		  legend cell align=left]
 		  \addplot[cyan,mark=*, mark options={fill=white}] table {regex3_size_change.data};
 	  \end{axis}
 \end{tikzpicture}\\
-\multicolumn{3}{c}{Graphs: size change of 3 randomly generated regular expressions $w.r.t.$ input string length.}
+\multicolumn{3}{c}{}
 	\end{tabular}
+\caption{Graphs: size change of 3 randomly generated
+regular expressions $w.r.t.$ input string length.
+The x axis represents the length of input.}
 \end{figure}
 \noindent
 Most of the regex's sizes seem to stay within a polynomial bound $w.r.t$ the
 original size.
 We will discuss improvements to this bound in the next chapter.
-\section{Possible Further Improvements}
+\subsection{Possible Further Improvements}
-There are two problems with this finiteness result, though.
+There are two problems with this finiteness result, though.\\
-\begin{itemize}
+(i)
-	\item
+		First, it is not yet a direct formalisation of our lexer's complexity,
-		First, It is not yet a direct formalisation of our lexer's complexity,
 		as a complexity proof would require looking into
 		the time it takes to execute {\bf all} the operations
-		involved in the lexer (simp, collect, decode), not just the derivative.
+		involved in the lexer (simp, collect, decode), not just the derivative.\\
-	\item
+(ii)
 		Second, the bound is not yet tight, and we seek to improve $N_a$ so that
-		it is polynomial on $\llbracket a \rrbracket$.
+		it is polynomial on $\llbracket a \rrbracket$.\\
-\end{itemize}
+Still, we believe this contribution is useful,
-Still, we believe this contribution is fruitful,
 because
 \begin{itemize}
 	\item
-		The size proof can serve as a cornerstone for a complexity
+		The size proof can serve as a starting point for a complexity
 		formalisation.
 		Derivatives are the most important phases of our lexer algorithm.
 		Size properties about derivatives covers the majority of the algorithm
 		and is therefore a good indication of complexity of the entire program.
 	\item
 but will eventually level off when the string $s$ is long enough.
 If they grow to a size exponential $w.r.t$ the original regex, our algorithm
 would still be slow.
 And unfortunately, we have concrete examples
 where such regular expressions grew exponentially large before levelling off:
+\begin{center}
 $(a ^ * + (aa) ^ * + (aaa) ^ * + \ldots +
-(\underbrace{a \ldots a}_{\text{n a's}})^*$ will already have a maximum
+(\underbrace{a \ldots a}_{\text{n a's}})^*)^*$
+\end{center}
+will already have a maximum
 size that is  exponential on the number $n$
 under our current simplification rules:
 %TODO: graph of a regex whose size increases exponentially.
 \begin{center}
 	\begin{tikzpicture}
 			\addplot[mark=*,blue] table {re-chengsong.data};
 		\end{axis}
 	\end{tikzpicture}
 \end{center}
-For convenience we use $(\oplus_{i=1}^{n} (\underbrace{a \ldots a}_{\text{i a's}})^*)^*$
+For convenience we use $(\sum_{i=1}^{n} (\underbrace{a \ldots a}_{\text{i a's}})^*)^*$
 to express $(a ^ * + (aa) ^ * + (aaa) ^ * + \ldots +
 (\underbrace{a \ldots a}_{\text{n a's}})^*$ in the below discussion.
 The exponential size is triggered by that the regex
-$\oplus_{i=1}^{n} (\underbrace{a \ldots a}_{\text{i a's}})^*$
+$\sum_{i=1}^{n} (\underbrace{a \ldots a}_{\text{i a's}})^*$
 inside the $(\ldots) ^*$ having exponentially many
 different derivatives, despite those difference being minor.
-$(\oplus_{i=1}^{n} (\underbrace{a \ldots a}_{\text{i a's}})^*)^*\backslash \underbrace{a \ldots a}_{\text{m a's}}$
+$(\sum_{i=1}^{n} (\underbrace{a \ldots a}_{\text{i a's}})^*)^*\backslash \underbrace{a \ldots a}_{\text{m a's}}$
 will therefore contain the following terms (after flattening out all nested
 alternatives):
 \begin{center}
-	$(\oplus_{i = 1]{n}  (\underbrace{a \ldots a}_{\text{((i - (m' \% i))\%i) a's}})\cdot  (\underbrace{a \ldots a}_{\text{i a's}})^* })\cdot (\oplus_{i=1}^{n} (\underbrace{a \ldots a}_{\text{i a's}})^*)$\\
+$(\sum_{i = 1}^{n}  (\underbrace{a \ldots a}_{\text{((i - (m' \% i))\%i) a's}})\cdot  (\underbrace{a \ldots a}_{\text{i a's}})^* )\cdot (\sum_{i=1}^{n} (\underbrace{a \ldots a}_{\text{i a's}})^*)$\\
+[1mm]
 	$(1 \leq m' \leq m )$
 \end{center}
-These terms are distinct for $m' \leq L.C.M.(1, \ldots, n)$ (will be explained in appendix).
+There at at least exponentially
+many such terms.\footnote{To be exact, these terms are
+distinct for $m' \leq L.C.M.(1, \ldots, n)$, the details are omitted,
+but the point is that the number is exponential.
+}
 With each new input character taking the derivative against the intermediate result, more and more such distinct
-terms will accumulate,
+terms will accumulate.
-until the length reaches $L.C.M.(1, \ldots, n)$.
+The function $\textit{distinctBy}$ will not be able to de-duplicate any two of these terms
-$\textit{distinctBy}$ will not be able to de-duplicate any two of these terms
+\begin{center}
-$(\oplus_{i = 1}^{n}  (\underbrace{a \ldots a}_{\text{((i - (m' \% i))\%i) a's}})\cdot  (\underbrace{a \ldots a}_{\text{i a's}})^* )\cdot (\oplus_{i=1}^{n} (\underbrace{a \ldots a}_{\text{i a's}})^*)^*$\\
+$(\sum_{i = 1}^{n}
+(\underbrace{a \ldots a}_{\text{((i - (m' \% i))\%i) a's}})\cdot
-$(\oplus_{i = 1}^{n}  (\underbrace{a \ldots a}_{\text{((i - (m'' \% i))\%i) a's}})\cdot  (\underbrace{a \ldots a}_{\text{i a's}})^* )\cdot (\oplus_{i=1}^{n} (\underbrace{a \ldots a}_{\text{i a's}})^*)^*$\\
+(\underbrace{a \ldots a}_{\text{i a's}})^* )\cdot
-where $m' \neq m''$ \\
+(\sum_{i=1}^{n} (\underbrace{a \ldots a}_{\text{i a's}})^*)^*$\\
+$(\sum_{i = 1}^{n}  (\underbrace{a \ldots a}_{\text{((i - (m'' \% i))\%i) a's}})\cdot
+(\underbrace{a \ldots a}_{\text{i a's}})^* )\cdot
+(\sum_{i=1}^{n} (\underbrace{a \ldots a}_{\text{i a's}})^*)^*$
+\end{center}
+\noindent
+where $m' \neq m''$
 as they are slightly different.
 This means that with our current simplification methods,
 we will not be able to control the derivative so that
-$\llbracket \bderssimp{r}{s} \rrbracket$ stays polynomial %\leq O((\llbracket r\rrbacket)^c)$
+$\llbracket \bderssimp{r}{s} \rrbracket$ stays polynomial. %\leq O((\llbracket r\rrbacket)^c)$
-as there are already exponentially many terms.
 These terms are similar in the sense that the head of those terms
 are all consisted of sub-terms of the form:
 $(\underbrace{a \ldots a}_{\text{j a's}})\cdot  (\underbrace{a \ldots a}_{\text{i a's}})^* $.
-For  $\oplus_{i=1}^{n} (\underbrace{a \ldots a}_{\text{i a's}})^*$, there will be at most
+For  $\sum_{i=1}^{n} (\underbrace{a \ldots a}_{\text{i a's}})^*$, there will be at most
 $n * (n + 1) / 2$ such terms.
 For example, $(a^* + (aa)^* + (aaa)^*) ^*$'s derivatives
 can be described by 6 terms:
 $a^*$, $a\cdot (aa)^*$, $ (aa)^*$,
 $aa \cdot (aaa)^*$, $a \cdot (aaa)^*$, and $(aaa)^*$.
 The total number of different "head terms",  $n * (n + 1) / 2$,
 is proportional to the number of characters in the regex
-$(\oplus_{i=1}^{n} (\underbrace{a \ldots a}_{\text{i a's}})^*)^*$.
+$(\sum_{i=1}^{n} (\underbrace{a \ldots a}_{\text{i a's}})^*)^*$.
-This suggests a slightly different notion of size, which we call the
+If we can improve our deduplication process so that it becomes smarter
+and only keep track of these $n * (n+1) /2$ terms, then we can keep
+the size growth polynomial again.
+This example also suggests a slightly different notion of size, which we call the
 alphabetic width:
-%TODO:
+\begin{center}
-(TODO: Alphabetic width def.)
+	\begin{tabular}{lcl}
+		$\textit{awidth} \; \ZERO$ & $\dn$ & $0$\\
+		$\textit{awidth} \; \ONE$ & $\dn$ & $0$\\
+		$\textit{awidth} \; c$ & $\dn$ & $1$\\
+		$\textit{awidth} \; r_1 + r_2$ & $\dn$ & $\textit{awidth} \;
+		r_1 + \textit{awidth} \; r_2$\\
+		$\textit{awidth} \; r_1 \cdot r_2$ & $\dn$ & $\textit{awidth} \;
+		r_1 + \textit{awidth} \; r_2$\\
+		$\textit{awidth} \; r^*$ & $\dn$ & $\textit{awidth} \; r$\\
+	\end{tabular}
+\end{center}
 Antimirov\parencite{Antimirov95} has proven that
-$\textit{PDER}_{UNIV}(r) \leq \textit{awidth}(r)$.
+$\textit{PDER}_{UNIV}(r) \leq \textit{awidth}(r)$,
 where $\textit{PDER}_{UNIV}(r)$ is a set of all possible subterms
 created by doing derivatives of $r$ against all possible strings.
 If we can make sure that at any moment in our lexing algorithm our
 intermediate result hold at most one copy of each of the
 subterms then we can get the same bound as Antimirov's.
 %-----------------------------------
 %	SUBSECTION 1
 %-----------------------------------
-\subsection{Syntactic Equivalence Under $\simp$}
+%\subsection{Syntactic Equivalence Under $\simp$}
-We prove that minor differences can be annhilated
+%We prove that minor differences can be annhilated
-by $\simp$.
+%by $\simp$.
-For example,
+%For example,
-\begin{center}
+%\begin{center}
-	$\simp \;(\simpALTs\; (\map \;(\_\backslash \; x)\; (\distinct \; \mathit{rs}\; \phi))) =
+%	$\simp \;(\simpALTs\; (\map \;(\_\backslash \; x)\; (\distinct \; \mathit{rs}\; \phi))) =
-	\simp \;(\simpALTs \;(\distinct \;(\map \;(\_ \backslash\; x) \; \mathit{rs}) \; \phi))$
+%	\simp \;(\simpALTs \;(\distinct \;(\map \;(\_ \backslash\; x) \; \mathit{rs}) \; \phi))$
-\end{center}
+%\end{center}

changeset 618	233cf2b97d1a
parent 614	d5e9bcb384ec
child 620	ae6010c14e49