
diff -r 3e19073e91f4 -r 4aabb0629e4b ChengsongTanPhdThesis/Chapters/Inj.tex
--- a/ChengsongTanPhdThesis/Chapters/Inj.tex	Mon Aug 22 17:58:29 2022 +0100
+++ b/ChengsongTanPhdThesis/Chapters/Inj.tex	Tue Aug 23 14:21:13 2022 +0100
@@ -10,19 +10,19 @@
 
 In this chapter, we define the basic notions 
 for regular languages and regular expressions.
-This is essentially a description in ``English"
+This is essentially a description in ``English''
 of our formalisation in Isabelle/HOL.
 We also give the definition of what $\POSIX$ lexing means, 
-followed by an algorithm by Sulzmanna and Lu\parencite{Sulzmann2014} 
+followed by a lexing algorithm by Sulzmanna and Lu\parencite{Sulzmann2014} 
 that produces the output conforming
 to the $\POSIX$ standard.
-It is also worth mentioning that
-we choose to use the ML-style notation
+\footnote{In what follows 
+we choose to use the Isabelle-style notation
 for function applications, where
-the parameters of a function is not enclosed
+the parameters of a function are not enclosed
 inside a pair of parentheses (e.g. $f \;x \;y$
 instead of $f(x,\;y)$). This is mainly
-to make the text visually more concise.
+to make the text visually more concise.}
 
 \section{Basic Concepts}
 Usually, formal language theory starts with an alphabet 
@@ -38,7 +38,7 @@
 $\textit{s}$ & $\dn$ & $[] \; |\; c  :: s$
 \end{tabular}
 \end{center}
-Where $c$ is a variable ranging over characters.
+where $c$ is a variable ranging over characters.
 Strings can be concatenated to form longer strings in the same
 way as we concatenate two lists, which we shall write as $s_1 @ s_2$.
 We omit the precise 
@@ -88,7 +88,8 @@
 \end{tabular}
 \end{center}
 \noindent
-This can be generalised to "chopping off" a string from all strings within set $A$, 
+This can be generalised to ``chopping off'' a string 
+from all strings within a set $A$, 
 namely:
 \begin{center}
 \begin{tabular}{lcl}
@@ -97,7 +98,7 @@
 \end{center}
 \noindent
 which is essentially the left quotient $A \backslash L$ of $A$ against 
-the singleton language with $L = \{w\}$
+the singleton language with $L = \{s\}$
 in formal language theory.
 However, for the purposes here, the $\textit{Ders}$ definition with 
 a single string is sufficient.
@@ -145,13 +146,13 @@
 \noindent
 This lemma states that if $A$ contains the empty string, $\Der$ can "pierce" through it
 and get to $B$.
-The language $A*$'s derivative can be described using the language derivative
+The language derivative for $A*$ can be described using the language derivative
 of $A$:
 \begin{lemma}
 $\textit{Der} \;c \;(A*) = (\textit{Der}\; c A) @ (A*)$\\
 \end{lemma}
 \begin{proof}
-There are too inclusions to prove:
+There are two inclusions to prove:
 \begin{itemize}
 \item{$\subseteq$}:\\
 The set 
@@ -167,8 +168,8 @@
 \item{$\supseteq$}:\\
 Note that
 \[ \Der \; c \; (A*) = \Der \; c \;  (\{ [] \} \cup (A @ A*) ) \]
-hold.
-Also this holds:
+holds.
+Also the following holds:
 \[ \Der \; c \;  (\{ [] \} \cup (A @ A*) ) = \Der\; c \; (A @ A*) \]
 where the $\textit{RHS}$ can be rewritten
 as \[ (\Der \; c\; A) @ A* \cup (\Der \; c \; (A*)) \]
@@ -218,15 +219,15 @@
 \end{tabular}
 \end{center}
 \noindent
-Now with semantic derivatives of a language and regular expressions and
-their language interpretations in place, we are ready to define derivatives on regexes.
+Now with language derivatives of a language and regular expressions and
+their language interpretations in place, we are ready to define derivatives on regular expressions.
 \subsection{Brzozowski Derivatives and a Regular Expression Matcher}
 %Recall, the language derivative acts on a set of strings
 %and essentially chops off a particular character from
 %all strings in that set, Brzozowski defined a derivative operation on regular expressions
 %so that after derivative $L(r\backslash c)$ 
 %will look as if it was obtained by doing a language derivative on $L(r)$:
-Recall that the semantic derivative acts on a 
+Recall that the language derivative acts on a 
 language (set of strings).
 One can decide whether a string $s$ belongs
 to a language $S$ by taking derivative with respect to
@@ -375,10 +376,10 @@
 Now we give the recursive definition of derivative on
 regular expressions, so that it satisfies the properties above.
 The derivative function, written $r\backslash c$, 
-defines how a regular expression evolves into
-a new one after all the string it contains is acted on: 
-if it starts with $c$, then the character is chopped of,
-if not, that string is removed.
+takes a regular expression $r$ and character $c$, and
+returns a new regular expression representing
+the original regular expression's language $L \; r$
+being taken the language derivative with respect to $c$.
 \begin{center}
 \begin{tabular}{lcl}
 		$\ZERO \backslash c$ & $\dn$ & $\ZERO$\\  
@@ -401,7 +402,9 @@
 result of this derivative:
 \begin{center}
 	\begin{tabular}{lcl}
-		$(r_1 \cdot r_2 ) \backslash c$ & $\dn$ & $\textit{if}\;\,([] \in L(r_1))\; r_1 \backslash c \cdot r_2 + r_2 \backslash c$ \\
+		$(r_1 \cdot r_2 ) \backslash c$ & $\dn$ & 
+		$\textit{if}\;\,([] \in L(r_1))\; 
+		\textit{then} \; r_1 \backslash c \cdot r_2 + r_2 \backslash c$ \\
 		& & $\textit{else} \; (r_1 \backslash c) \cdot r_2$
 	\end{tabular}
 \end{center}
@@ -418,7 +421,7 @@
 	\end{tabular}
 \end{center}
 \noindent
-The star regular expression $r^*$'s derivative 
+The derivative of the star regular expression $r^*$ 
 unwraps one iteration of $r$, turns it into $r\backslash c$,
 and attaches the original $r^*$
 after $r\backslash c$, so that 
@@ -427,7 +430,7 @@
 	(r^*) \backslash c \dn (r \backslash c)\cdot r^*.
 \]
 Again,
-the structure is the same as the semantic derivative of Kleene star: 
+the structure is the same as the language derivative of Kleene star: 
 \[
 	\textit{Der} \;c \;(A*) \dn (\textit{Der}\; c A) @ (A*)
 \]
@@ -494,16 +497,16 @@
 \begin{center}
 \begin{tabular}{lcl}
 $r \backslash_s (c\!::\!s) $ & $\dn$ & $(r \backslash c) \backslash_s s$ \\
-$r \backslash [\,] $ & $\dn$ & $r$
+$r \backslash_s [\,] $ & $\dn$ & $r$
 \end{tabular}
 \end{center}
 
 \noindent
 When there is no ambiguity, we will 
 omit the subscript and use $\backslash$ instead
-of $\backslash_r$ to denote
+of $\backslash_s$ to denote
 string derivatives for brevity.
-Brzozowski's  regular-expression matcher algorithm can then be described as:
+Brzozowski's  regular-expression matching algorithm can then be described as:
 
 \begin{definition}
 $\textit{match}\;s\;r \;\dn\; \nullable \; (r\backslash s)$
@@ -515,7 +518,9 @@
 
 \begin{equation}\label{graph:successive_ders}
 \begin{tikzcd}
-r_0 \arrow[r, "\backslash c_0"]  & r_1 \arrow[r, "\backslash c_1"] & r_2 \arrow[r, dashed]  & r_n  \arrow[r,"\textit{nullable}?"] & \;\textrm{YES}/\textrm{NO}
+r_0 \arrow[r, "\backslash c_0"]  & r_1 \arrow[r, "\backslash c_1"] & 
+r_2 \arrow[r, dashed]  & r_n  \arrow[r,"\textit{nullable}?"] & 
+\;\textrm{true}/\textrm{false}
 \end{tikzcd}
 \end{equation}
 
@@ -526,12 +531,12 @@
 	$\textit{match} \; s\; r  = \textit{true} \; \textit{iff} \; s \in L(r)$
 \end{lemma}
 \begin{proof}
-	By the stepwise property of derivatives 
-	(lemma \ref{derDer}).
+	By induction on $s$ using property of derivatives:
+	lemma \ref{derDer}.
 \end{proof}
 \noindent
 \begin{center}
-	\begin{figure}
+\begin{figure}
 \begin{tikzpicture}
 \begin{axis}[
     xlabel={$n$},
@@ -543,7 +548,9 @@
 \addplot[red,mark=*, mark options={fill=white}] table {NaiveMatcher.data};
 \end{axis}
 \end{tikzpicture} 
-\caption{Matching $(a^*)^*b$ against $\protect\underbrace{aa\ldots a}_\text{n \textit{a}s}$}\label{NaiveMatcher}
+\caption{Matching the regular expression $(a^*)^*b$ against strings of the form
+$\protect\underbrace{aa\ldots a}_\text{n \textit{a}s}
+$ using Brzozowski's original algorithm}\label{NaiveMatcher}
 \end{figure}
 \end{center} 
 \noindent
@@ -552,9 +559,9 @@
 \ref{NaiveMatcher}.
 Note that both axes are in logarithmic scale.
 Around two dozens characters
-would already explode the matcher on regular expression 
+would already explode the matcher on the regular expression 
 $(a^*)^*b$.
-For this, we need to introduce certain 
+Too improve this situation, we need to introduce simplification
 rewrite rules for the intermediate results,
 such as $r + r \rightarrow r$,
 and make sure those rules do not change the 
@@ -574,7 +581,7 @@
 				     & & $\quad \; \case \; (\ZERO, r_2') \Rightarrow r_2'$\\
 				     & & $\quad \; \case \; (r_1', \ZERO) \Rightarrow r_1'$\\
 				     & & $\quad \; \case \; (r_1', r_2') \Rightarrow r_1' + r_2'$\\
-		$\simp \; r$ & $\dn$ & $r$
+		$\simp \; r$ & $\dn$ & $r\quad\quad (otherwise)$
 				   
 	\end{tabular}
 \end{center}
@@ -608,15 +615,15 @@
 \end{figure}
 \noindent
 The running time of $\textit{ders}\_\textit{simp}$
-on the same example of \ref{NaiveMatcher}
-is now very tame in terms of the length of inputs,
-as shown in \ref{BetterMatcher}.
+on the same example of Figure \ref{NaiveMatcher}
+is now ``tame''  in terms of the length of inputs,
+as shown in Figure \ref{BetterMatcher}.
 
-Building derivatives and then testing the existence
-of empty string in the resulting regular expression's language,
-adding simplifications when necessary.
-So far, so good. But what if we want to 
-do lexing instead of just getting a YES/NO answer?
+So far the story is use Brzozowski derivatives,
+simplifying where possible and at the end test
+whether the empty string is recognised by the final derivative.
+But what if we want to 
+do lexing instead of just getting a true/false answer?
 Sulzmanna and Lu \cite{Sulzmann2014} first came up with a nice and 
 elegant (arguably as beautiful as the definition of the original derivative) solution for this.
 
@@ -1152,12 +1159,12 @@
 \end{proof}
 \noindent
 As we did earlier in this chapter on the matcher, one can 
-introduce simplification on the regex.
+introduce simplification on the regular expression.
 However, now one needs to do a backward phase and make sure
 the values align with the regular expressions.
 Therefore one has to
 be careful not to break the correctness, as the injection 
-function heavily relies on the structure of the regexes and values
+function heavily relies on the structure of the regular expressions and values
 being correct and matching each other.
 It can be achieved by recording some extra rectification functions
 during the derivatives step, and applying these rectifications in 




