lexing: comparison ChengsongTanPhdThesis/Chapters/Finite.tex

equal deleted inserted replaced

-:d028c662a3df
+:bc1df466150a
 \section{Details of Closed Forms and Bounds}
 In this section we introduce in detail
 how the closed forms are obtained for regular expressions'
 derivatives and how they are bounded.
-We start by proving some basic identities
+We start by proving some basic identities and inequalities
 involving the simplification functions for r-regular expressions.
 After that we use these identities to establish the
 closed forms we need.
 Finally, we prove the functions such as $\flts$
 will keep the size non-increasing.
 the closed forms.
 %$r_1\cdot r_2$, $r^*$ and $\sum rs$.
-\subsection{Some Basic Identities}
+\subsection{Some Basic Identities and Inequalities}
+In this subsection, we introduce lemmas
-\subsubsection{$\textit{rdistinct}$'s Deduplicates Successfully}
+that are repeatedly used in later proofs.
+Note that for the $\textit{rdistinct}$ function there
+will be a lot of conversion from lists to sets.
+We use the name $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
 remove duplicates in an r-regular expression list.
 It will also correctly exclude any elements that
 is intially in the accumulator set.
 \begin{lemma}\label{rdistinctDoesTheJob}
 	By induction on $rs$ and using \ref{rdistinctDoesTheJob}.
 \end{proof}
 \noindent
 On the other hand, if an element $r$ does not appear in the input list waiting to be deduplicated,
 then expanding the accumulator to include that element will not cause the output list to change:
-\begin{lemma}
+\begin{lemma}\label{rdistinctOnDistinct}
 	The accumulator can be augmented to include elements not appearing in the input list,
 	and the output will not change.
 	\begin{itemize}
 		\item
-			If $r \notin rs$, then $\rdistinct{rs}{acc} = \rdistinct{rs}{\{r\} \cup acc}$.
+			If $r \notin rs$, then $\rdistinct{rs}{acc} = \rdistinct{rs}{(\{r\} \cup acc)}$.
 		\item
-			Particularly, when $acc = \varnothing$ and $rs$ de-duplicated, we have\\
+			Particularly, if $\;\;\textit{isDistinct} \; rs$, then we have\\
 			\[ \rdistinct{rs}{\varnothing} = rs \]
 	\end{itemize}
 \end{lemma}
 \begin{proof}
 	The first half is by induction on $rs$. The second half is a corollary of the first.
 \end{proof}
 \noindent
-The next property gives the condition for
+The function $\textit{rdistinct}$ removes duplicates from anywhere in a list.
-when $\rdistinct{\_}{\_}$ becomes an identical mapping
+Despite being seemingly obvious,
-for any prefix of an input list, in other words, when can
+the induction technique is not as straightforward.
-we ``push out" the arguments of $\rdistinct{\_}{\_}$:
-\begin{lemma}\label{distinctRdistinctAppend}
-	If $\textit{isDistinct} \; rs_1$, and $rs_1 \cap acc = \varnothing$,
-	then
-	\[\textit{rdistinct}\;  (rs_1 @ rsa)\;\, acc
-	= rs_1@(\textit{rdistinct} rsa \; (acc \cup rs_1))\]
-\end{lemma}
-\noindent
-In other words, it can be taken out and left untouched in the output.
-\begin{proof}
-	By an induction on $rs_1$, where $rsa$ and $acc$ are allowed to be arbitrary.
-\end{proof}
-\noindent
-$\rdistinct{}{}$ removes any element in anywhere of a list, if it
-had appeared previously:
 \begin{lemma}\label{distinctRemovesMiddle}
 	The two properties hold if $r \in rs$:
 	\begin{itemize}
 		\item
 			$\rdistinct{rs}{rset} = \rdistinct{(rs @ [r])}{rset}$\\
 	\end{itemize}
 \end{lemma}
 \noindent
 \begin{proof}
 	By induction on $rs$. All other variables are allowed to be arbitrary.
-	The second half of the lemma requires the first half.
+	The second part of the lemma requires the first.
-	Note that for each half's two sub-propositions need to be proven concurrently,
+	Note that for each part, the two sub-propositions need to be proven concurrently,
 	so that the induction goes through.
 \end{proof}
+\noindent
-\noindent
+This allows us to prove a few more equivalence relations involving
-This allows us to prove ``Idempotency" of $\rdistinct{}{}$ of some kind:
+$\textit{rdistinct}$ (it will be useful later):
 \begin{lemma}\label{rdistinctConcatGeneral}
-	The following equalities involving multiple applications  of $\rdistinct{}{}$ hold:
+	\mbox{}
 	\begin{itemize}
 		\item
 			$\rdistinct{(rs @ rs')}{\varnothing} = \rdistinct{((\rdistinct{rs}{\varnothing})@ rs')}{\varnothing}$
 		\item
 			$\rdistinct{(rs @ rs')}{\varnothing} = \rdistinct{(\rdistinct{rs}{\varnothing} @ rs')}{\varnothing}$
 	\end{itemize}
 \end{lemma}
 \begin{proof}
 	By \ref{rdistinctDoesTheJob} and \ref{distinctRemovesMiddle}.
 \end{proof}
+\noindent
-\subsubsection{The Properties of $\backslash_r$, $\backslash_{rsimp}$, $\textit{Rflts}$ and $\textit{Rsimp}_{ALTS}$}
+$\textit{rdistinct}$ is composable w.r.t list concatenation:
-We give in this subsection some properties of how $\backslash_r$, $\backslash_{rsimp}$, $\textit{Rflts}$ and $\textit{Rsimp}_{ALTS} $ interact with each other and with $@$, the concatenation operator.
+\begin{lemma}\label{distinctRdistinctAppend}
+			If $\;\; \textit{isDistinct} \; rs_1$,
+			and $(set \; rs_1) \cap acc = \varnothing$,
+			then applying $\textit{rdistinct}$ on $rs_1 @ rs_a$ does not
+			have an effect on $rs_1$:
+			\[\textit{rdistinct}\;  (rs_1 @ rsa)\;\, acc
+			= rs_1@(\textit{rdistinct} rsa \; (acc \cup rs_1))\]
+\end{lemma}
+\begin{proof}
+	By an induction on
+	$rs_1$, where $rsa$ and $acc$ are allowed to be arbitrary.
+\end{proof}
+\noindent
+$\textit{rdistinct}$ needs to be applied only once, and
+applying it multiple times does not cause any difference:
+\begin{corollary}\label{distinctOnceEnough}
+	$\textit{rdistinct} \; (rs @ rsa) {} = \textit{rdistinct} \; (rdistinct \;
+	rs \{ \} @ (\textit{rdistinct} \; rs_a \; (set \; rs)))$
+\end{corollary}
+\begin{proof}
+	By lemma \ref{distinctRdistinctAppend}.
+\end{proof}
+\subsubsection{The Properties of $\textit{Rflts}$}
+We give in this subsection some properties
+involving $\backslash_r$, $\backslash_{rsimp}$, $\textit{rflts}$ and
+$\textit{rsimp}_{ALTS} $, together with any non-trivial lemmas that lead to them.
 These will be helpful in later closed form proofs, when
-we want to transform the ways in which multiple functions involving
+we want to transform derivative terms which have
-those are composed together
+%the ways in which multiple functions involving
-in interleaving derivative and  simplification steps.
+%those are composed together
+interleaving derivatives and  simplifications applied to them.
-When the function $\textit{Rflts}$
-is applied to the concatenation of two lists, the output can be calculated by first applying the
+\noindent
-functions on two lists separately, and then concatenating them together.
+%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:\\
 	\begin{itemize}
 		\item
 			$\rflts \; (rs_1 @ rs_2) = \rflts \; rs_1 @ \rflts \; rs_2$
 \noindent
 \begin{proof}
 	By induction on $rs_1$ in the first sub-lemma, and induction on $r$ in the second part,
 	and induction on $rs$, $rs'$, $rs$, $rs'$, $rs_a$ in the third, fourth, fifth, sixth and
 	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
+the alternative regular expression:
+\begin{lemma}\label{rderRsimpAltsCommute}
+	$\rder{x}{(\rsimpalts \; rs)} = \rsimpalts \; (\map \; (\rder{x}{\_}) \; rs)$
+\end{lemma}
+\noindent
+\subsubsection{$\textit{rsimp}$ Does Not Increment the Size}
+Although it seems evident, we need a series
+of non-trivial lemmas to establish this property.
+\begin{lemma}\label{rsimpMonoLemmas}
+	\mbox{}
+	\begin{itemize}
+		\item
+			\[
+				\llbracket \rsimpalts \; rs \rrbracket_r \leq
+				\llbracket \sum \; rs \rrbracket_r
+			\]
+		\item
+			\[
+				\llbracket \rsimpseq \; r_1 \;  r_2 \rrbracket_r \leq
+				\llbracket r_1 \cdot r_2 \rrbracket_r
+			\]
+		\item
+			\[
+				\llbracket \rflts \; rs \rrbracket_r  \leq
+				\llbracket rs \rrbracket_r
+			\]
+		\item
+			\[
+				\llbracket \rDistinct \; rs \; ss \rrbracket_r  \leq
+				\llbracket rs \rrbracket_r
+			\]
+		\item
+			If all elements $a$ in the set $as$ satisfy the property
+			that $\llbracket \textit{rsimp} \; a \rrbracket_r \leq
+			\llbracket a \rrbracket_r$, then we have
+			\[
+				\llbracket \; \rsimpalts \; (\textit{rdistinct} \;
+				(\textit{rflts} \; (\textit{map}\;\textit{rsimp} as)) \{\})
+				\rrbracket \leq
+				\llbracket \; \sum \; (\rDistinct \; (\rflts \;(\map \;
+				\textit{rsimp} \; x))\; \{ \} ) \rrbracket_r
+			\]
+	\end{itemize}
+\end{lemma}
+\begin{proof}
+	Point 1, 3, 4 can be proven by an induction on $rs$.
+	Point 2 is by case analysis on $r_1$ and $r_2$.
+	The last part is a corollary of the previous ones.
+\end{proof}
+\noindent
+With the lemmas for each inductive case in place, we are ready to get
+the non-increasing property as a corollary:
+\begin{corollary}\label{rsimpMono}
+	$\llbracket \textit{rsimp} \; r \rrbracket_r$
+\end{corollary}
+\begin{proof}
+	By \ref{rsimpMonoLemmas}.
 \end{proof}
 \subsubsection{The $RL$ Function: Language Interpretation of $\textit{Rrexp}$s}
 Much like the definition of $L$ on plain regular expressions, one could also
 define the language interpretation of $\rrexp$s.
 of $\rsimp{}$ application:
 \begin{lemma}\label{test}
 	If $\good \;r$ then $\rsimp{r} = r$.
 \end{lemma}
 \begin{proof}
-	By an induction on the inductive cases of $\good$.
+	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}$,
-We are also
+We are also ready to prove that $\textit{rsimp}$ is idempotent.
-\subsection{$\rsimp$ is Idempotent}
+\subsubsection{$\rsimp$ is Idempotent}
 The idempotency of $\rsimp$ is very useful in
 manipulating regular expression terms into desired
 forms so that key steps allowing further rewriting to closed forms
 are possible.
 \begin{lemma}\label{rsimpIdem}
 		\item
 			$\rsimpalts \; (\rdistinct{\rflts \; [r]}{\varnothing}) = r$.
 	\end{itemize}
 \end{lemma}
 \begin{proof}
-	By application of \ref{rsimpIdem} and \ref{good1}.
+	By application of lemmas \ref{rsimpIdem} and \ref{good1}.
 \end{proof}
 \noindent
 With the idempotency of $\rsimp{}$ and its corollaries,
 we can start proving some key equalities leading to the
 		\inferrule[dB]{}{rs_a @ [a] @ rs_b @[a] @ rs_c \grewrite rs_a @ [a] @ rsb @ rsc}
 	\end{mathpar}
 \end{center}
 \noindent
-The reason why we take the trouble of defining
+We defined
-two separate list rewriting definitions $\frewrite$ and $\grewrite$
+two separate list rewriting definitions $\frewrite$ and $\grewrite$.
-is to separate the two stages of simplification: flattening and de-duplicating.
+The rewriting steps that take place during
+flattening is characterised by $\frewrite$.
+$\grewrite$ characterises both flattening and de-duplicating.
 Sometimes $\grewrites$ is slightly too powerful
-so we would rather use $\frewrites$ which makes certain rewriting steps
+so we would rather use $\frewrites$ because we only
-more straightforward to prove.
+need to prove about certain equivalence under the rewriting steps of $\frewrites$.
 For example, when proving the closed-form for the alternative regular expression,
 one of the rewriting steps would be:
 \begin{lemma}
 	$\sum (\rDistinct \;\; (\map \; (\_ \backslash x) \; (\rflts \; rs)) \;\; \varnothing) \sequal
 	\sum (\rDistinct \;\;  (\rflts \; (\map \; (\_ \backslash x) \; rs)) \;\; \varnothing)
 			(\rdistinct{rs}{\varnothing})) \sequal
 			\rsimpalts \; (\rDistinct \;
 			(\map \; (\_ \backslash_r x) rs) \;\varnothing  )$
 	\end{itemize}
 \end{lemma}
-\noindent
+\begin{proof}
+	Part 1 is by lemma \ref{insideSimpRemoval},
-Finally,
+	part 2 is by lemmas \ref{insideSimpRemoval} and \ref{distinctDer}.
-together with
+\end{proof}
-\begin{lemma}\label{rderRsimpAltsCommute}
+\noindent
-	$\rder{x}{(\rsimpalts \; rs)} = \rsimpalts \; (\map \; (\rder{x}{\_}) \; rs)$
+This leads to the first closed form--
-\end{lemma}
-\noindent
-this leads to the first closed form--
 \begin{lemma}\label{altsClosedForm}
 	\begin{center}
 		$\rderssimp{(\sum rs)}{s} \sequal
 		\sum \; (\map \; (\rderssimp{\_}{s}) \; rs)$
 	\end{center}
 %size change
 %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{center}
+\begin{figure}{H}
 	\begin{tabular}{@{}c@{\hspace{0mm}}c@{\hspace{0mm}}c@{}}
 		\begin{tikzpicture}
 			\begin{axis}[
-				xlabel={number of $a$'s},
+				xlabel={number of characters},
 				x label style={at={(1.05,-0.05)}},
 				ylabel={regex size},
 				enlargelimits=false,
 				xtick={0,5,...,30},
 				xmax=33,
-				ymax=1000,
+				%ymax=1000,
-				ytick={0,100,...,1000},
+				%ytick={0,100,...,1000},
 				scaled ticks=false,
 				axis lines=left,
 				width=5cm,
 				height=4cm,
 				legend entries={regex1},
 		  x label style={at={(1.05,-0.05)}},
 		  %ylabel={time in secs},
 		  enlargelimits=false,
 		  xtick={0,5,...,30},
 		  xmax=33,
-		  ymax=1000,
+		  %ymax=1000,
-		  ytick={0,100,...,1000},
+		  %ytick={0,100,...,1000},
 		  scaled ticks=false,
 		  axis lines=left,
 		  width=5cm,
 		  height=4cm,
 		  legend entries={regex2},
 		  x label style={at={(1.05,-0.05)}},
 		  %ylabel={time in secs},
 		  enlargelimits=false,
 		  xtick={0,5,...,30},
 		  xmax=33,
-		  ymax=1000,
+		  %ymax=1000,
-		  ytick={0,100,...,1000},
+		  %ytick={0,100,...,1000},
 		  scaled ticks=false,
 		  axis lines=left,
 		  width=5cm,
 		  height=4cm,
 		  legend entries={regex3},
 		  \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.}
 	\end{tabular}
-\end{center}
+\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 syntactic equivalence under simp
 %-----------------------------------
-\section{Syntactic Equivalence Under $\simp$}
-We prove that minor differences can be annhilated
-by $\simp$.
-For example,
-\begin{center}
-	$\simp \;(\simpALTs\; (\map \;(\_\backslash \; x)\; (\distinct \; \mathit{rs}\; \phi))) =
-	\simp \;(\simpALTs \;(\distinct \;(\map \;(\_ \backslash\; x) \; \mathit{rs}) \; \phi))$
-\end{center}
 %----------------------------------------------------------------------------------------
 %	SECTION ALTS CLOSED FORM
 %----------------------------------------------------------------------------------------

changeset 611	bc1df466150a
parent 610	d028c662a3df
child 613	b0f0d884a547