--- a/ChengsongTanPhdThesis/main.tex	Sat Dec 24 11:55:04 2022 +0000
+++ b/ChengsongTanPhdThesis/main.tex	Fri Dec 30 01:52:32 2022 +0000
@@ -296,12 +296,17 @@
 are often treated as a constant factor.
 However with some regular expressions and inputs, existing implementations 
 often suffer from non-linear or even exponential running time, 
-giving to for example ReDoS (regular expression denial-of-service ) attacks. 
-To avoid these attacks, lexers with formalised correctness and running time related
+giving rise to ReDoS (regular expression denial-of-service ) attacks. 
+To avoid these attacks, regular expression matchers and lexers with 
+formalised correctness and running time related
 properties are of interest because the guarantees apply to all inputs, not just a finite
 number of empirical test cases.
 
-Sulzmann and Lu describe a lexing algorithm that calculates Brzozowski derivatives using bitcodes annotated to regular expressions. Their algorithm generates POSIX values which encode the information of how a regular expression matches a string—that is, which part of the string is matched by which part of the regular expression. This information is needed in the context of lexing in order to extract and to classify tokens. The purpose of the bitcodes is to generate POSIX values incrementally while derivatives are calculated. They also help with designing an “aggressive” simplification function that keeps the size of derivatives finitely bounded. Without simplification the size of some derivatives can grow arbitrarily big resulting in an extremely slow lexing algorithm.
+Sulzmann and Lu describe a lexing algorithm that calculates Brzozowski derivatives using bitcodes annotated to regular expressions. Their algorithm generates POSIX values which encode the information of how a regular expression matches a string—that is, which part of the string is matched by which part of the regular expression. This information is needed in the context of lexing in order to extract and to classify tokens. The purpose of the bitcodes is to generate POSIX values incrementally while derivatives are calculated. They also help with designing an “aggressive” simplification function that keeps the size of derivatives finitely bounded. 
+Our simplification function is more aggressive than the one by Sulzmann and Lu.
+We also fix a problem in Sulzmann and Lu's simplification to do with their use of
+the $\textit{nub}$ function which does not remove non-trivial duplicates.
+Without simplification the size of some derivatives can grow arbitrarily big resulting in an extremely slow lexing algorithm.
 In this thesis we describe a variant of Sulzmann and Lu’s algorithm: Our variant is a recursive functional program, whereas Sulzmann and Lu’s version involves a fixpoint construction. We (i) prove in Isabelle/HOL that our algorithm is correct and generates unique POSIX values; we also (ii) establish a finite bound for the size of the derivatives for every input string; we also
 (iii) give a program and a conjecture that the finite 
 bound can be improved to be cubic if stronger simplification rules are applied. 
@@ -329,9 +334,10 @@
 I want to thank Doctor Kathrin Stark, my SIGPLAN mentor, for offering brilliant advice
 at the late stage of my PhD. My transition from a PhD student to a postdoc researcher
 could not have been so smooth without Kathrin's mentoring.
-I want to thank Jeanna Wheeler, my UMO mentor, for helping me regulate my mental health
-and productivity, by being always encouraging
-and compassionate in her sessions.
+%I want to thank Jeanna Wheeler, my UMO mentor, for helping me regulate my mental health
+%and productivity, by being always encouraging
+%and compassionate in her sessions.
+I want to thank Jeanna Wheeler for helping me with keeping sane during my time during the PhD and COVID times when an encouraging and compassionate person was very appreciated.
 
 I want to thank my father Haiyan Tan and my mother Yunan Cheng,
 for their unconditional love, and who I have not seen