--- a/ChengsongTanPhdThesis/main.tex	Sat Nov 26 16:18:10 2022 +0000
+++ b/ChengsongTanPhdThesis/main.tex	Thu Dec 01 08:49:19 2022 +0000
@@ -250,7 +250,7 @@
 \noindent I, \authorname, declare that this thesis titled, \enquote{\ttitle} and the work presented in it are my own. I confirm that:
 
 \begin{itemize} 
-\item This work was done wholly or mainly while in candidature for a research degree at this University.
+\item This work was done wholly while in candidature for a research degree at this University.
 \item Where any part of this thesis has previously been submitted for a degree or any other qualification at this University or any other institution, this has been clearly stated.
 \item Where I have consulted the published work of others, this is always clearly attributed.
 \item Where I have quoted from the work of others, the source is always given. With the exception of such quotations, this thesis is entirely my own work.
@@ -291,18 +291,20 @@
 \addchaptertocentry{\abstractname} % Add the abstract to the table of contents
 %\addchap{Abstract} 
 This thesis is about regular expressions and derivatives. It combines functional algorithms and their formal verification in the Isabelle/HOL theorem prover. 
-Theoretical results say that regular expression matching should be 
-linear with respect to the input. 
+Classic results say that regular expression matching should be 
+linear with respect to the input. The size of the regular expressions
+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
-properties become appealing because the guarantee applies to all inputs, not a finite
+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. 
-
-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. 
+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.
+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. 
 
 
 

--- a/thys2/blexer2.sc	Sat Nov 26 16:18:10 2022 +0000
+++ b/thys2/blexer2.sc	Thu Dec 01 08:49:19 2022 +0000
@@ -917,9 +917,6 @@
 
     def turnIntoTerms(r: Rexp): List[Rexp] = r match {
       case SEQ(r1, r2)  => 
-    //   if(isOne1(r1)) 
-    //   turnIntoTerms(r2) 
-    // else 
         turnIntoTerms(r1).flatMap(r11 => furtherSEQ(r11, r2))
           case ALTS(r1, r2) => turnIntoTerms(r1) ::: turnIntoTerms(r2)
           case ZERO => Nil