--- a/ChengsongTanPhdThesis/Chapters/Chapter1.tex Fri May 06 13:22:20 2022 +0100
+++ b/ChengsongTanPhdThesis/Chapters/Chapter1.tex Sat May 07 13:38:44 2022 +0100
@@ -25,11 +25,16 @@
\newcommand{\ZERO}{\mbox{\bf 0}}
\newcommand{\ONE}{\mbox{\bf 1}}
\newcommand{\AALTS}[2]{\oplus {\scriptstyle #1}\, #2}
+\newcommand{\rdistinct}[2]{\textit{distinct} \; \textit{#1} \; #2}
+\newcommand\hflat[1]{\llparenthesis #1 \rrparenthesis_*}
+\newcommand\hflataux[1]{\llparenthesis #1 \rrparenthesis_*'}
+\newcommand\createdByStar[1]{\textit{\textit{createdByStar}(#1)}}
\newcommand\myequiv{\mathrel{\stackrel{\makebox[0pt]{\mbox{\normalfont\tiny equiv}}}{=}}}
\def\lexer{\mathit{lexer}}
\def\mkeps{\mathit{mkeps}}
+\newcommand{\rder}[2]{#2 \backslash #1}
\def\AZERO{\textit{AZERO}}
\def\AONE{\textit{AONE}}
@@ -85,6 +90,7 @@
\newcommand\RALTS[1]{\oplus #1}
\newcommand\RSTAR[1]{#1^*}
\newcommand\vsuf[2]{\textit{vsuf} \;#1\;#2}
+
%----------------------------------------------------------------------------------------
%This part is about regular expressions, Brzozowski derivatives,
%and a bit-coded lexing algorithm with proven correctness and time bounds.
@@ -878,7 +884,8 @@
With the formally-specified rules for what a POSIX matching is,
they proved in Isabelle/HOL that the algorithm gives correct results.
-But having a correct result is still not enough, we want $\mathbf{efficiency}$.
+But having a correct result is still not enough,
+we want at least some degree of $\mathbf{efficiency}$.