ChengsongTanPhdThesis/Chapters/Chapter1.tex
changeset 505 5ce3bd8e5696
parent 503 35b80e37dfe7
child 506 69ad05398894
--- 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}$.