--- a/ChengsongTanPhdThesis/Chapters/Inj.tex Thu Jun 09 22:08:06 2022 +0100
+++ b/ChengsongTanPhdThesis/Chapters/Inj.tex Sun Jun 12 17:03:09 2022 +0100
@@ -10,29 +10,33 @@
In this chapter, we define the basic notions
for regular languages and regular expressions.
+This is essentially a description in "English"
+of your formalisation in Isabelle/HOL.
We also give the definition of what $\POSIX$ lexing means.
\section{Basic Concepts}
-Usually in formal language theory there is an alphabet
+Usually formal language theory starts with an alphabet
denoting a set of characters.
-Here we only use the datatype of characters from Isabelle,
-which roughly corresponds to the ASCII character.
-Then using the usual $[]$ notation for lists,
-we can define strings using chars:
+Here we just use the datatype of characters from Isabelle,
+which roughly corresponds to the ASCII characters.
+In what follows we shall leave the information about the alphabet
+implicit.
+Then using the usual bracket notation for lists,
+we can define strings made up of characters:
\begin{center}
\begin{tabular}{lcl}
-$\textit{string}$ & $\dn$ & $[] | c :: cs$\\
-& & $(c\; \text{has char type})$
+$\textit{s}$ & $\dn$ & $[] \; |\; c :: s$
\end{tabular}
\end{center}
-And strings can be concatenated to form longer strings,
-in the same way as we concatenate two lists,
-which we denote as $@$. We omit the precise
+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 write as @.
+We omit the precise
recursive definition here.
We overload this concatenation operator for two sets of strings:
\begin{center}
\begin{tabular}{lcl}
-$A @ B $ & $\dn$ & $\{s_A @ s_B \mid s_A \in A; s_B \in B \}$\\
+$A @ B $ & $\dn$ & $\{s_A @ s_B \mid s_A \in A \land s_B \in B \}$\\
\end{tabular}
\end{center}
We also call the above \emph{language concatenation}.
@@ -41,11 +45,11 @@
\begin{center}
\begin{tabular}{lcl}
$A^0 $ & $\dn$ & $\{ [] \}$\\
-$A^{n+1}$ & $\dn$ & $A^n @ A$
+$A^{n+1}$ & $\dn$ & $A @ A^n$
\end{tabular}
\end{center}
The union of all the natural number powers of a language
-is defined as the Kleene star operator:
+is usually defined as the Kleene star operator:
\begin{center}
\begin{tabular}{lcl}
$A*$ & $\dn$ & $\bigcup_{i \geq 0} A^i$ \\
@@ -65,28 +69,28 @@
\inferrule{\\s_1 \in A \land \; s_2 \in A*}{s_1 @ s_2 \in A*}
\end{mathpar}
\end{center}
-
-We also define an operation of "chopping of" a character from
-a language, which we call $\Der$, meaning "Derivative for a language":
+\ChristianComment{Yes, used the inferrule command in mathpar}
+We also define an operation of "chopping off" a character from
+a language, which we call $\Der$, meaning \emph{Derivative} (for a language):
\begin{center}
\begin{tabular}{lcl}
$\textit{Der} \;c \;A$ & $\dn$ & $\{ s \mid c :: s \in A \}$\\
\end{tabular}
\end{center}
\noindent
-This can be generalised to "chopping off" a string from all strings within set $A$,
-with the help of the concatenation operator:
+This can be generalised to "chopping off" a string from all strings within set $A$,
+namely:
\begin{center}
\begin{tabular}{lcl}
-$\textit{Ders} \;w \;A$ & $\dn$ & $\{ s \mid w@s \in A \}$\\
+$\textit{Ders} \;s \;A$ & $\dn$ & $\{ s' \mid s@s' \in A \}$\\
\end{tabular}
\end{center}
\noindent
-which is essentially the left quotient $A \backslash L'$ of $A$ against
-the singleton language $L' = \{w\}$
+which is essentially the left quotient $A \backslash L$ of $A$ against
+the singleton language with $L = \{w\}$
in formal language theory.
-For this dissertation the $\textit{Ders}$ definition with
-a single string suffices.
+However for the purposes here, the $\textit{Ders}$ definition with
+a single string is sufficient.
With the sequencing, Kleene star, and $\textit{Der}$ operator on languages,
we have a few properties of how the language derivative can be defined using
@@ -510,7 +514,12 @@
For instance, when lexing a code snippet
$\textit{iffoo} = 3$ with the regular expression $\textit{keyword} + \textit{identifier}$, we want $\textit{iffoo}$ to be recognized
as an identifier rather than a keyword.
-
+\ChristianComment{Do I also introduce lexical values $LV$ here?}
+We know that $\POSIX$ values are also part of the normal values:
+\begin{lemma}
+$(r, s) \rightarrow v \implies \vdash v: r$
+\end{lemma}
+\noindent
The good property about a $\POSIX$ value is that
given the same regular expression $r$ and string $s$,
one can always uniquely determine the $\POSIX$ value for it:
@@ -659,12 +668,12 @@
\noindent
The central property of the $\lexer$ is that it gives the correct result by
$\POSIX$ standards:
- \begin{lemma}
+ \begin{theorem}
\begin{tabular}{l}
- $s \in L(r) \Longleftrightarrow (\exists v. \; r \; s = \Some(v) \land (r, \; s) \rightarrow v)$\\
- $s \notin L(r) \Longleftrightarrow (\lexer \; r\; s = \None)$
+ $\lexer \; r \; s = \Some(v) \Longleftrightarrow (r, \; s) \rightarrow v$\\
+ $\lexer \;r \; s = \None \Longleftrightarrow \neg(\exists v. (r, s) \rightarrow v)$
\end{tabular}
- \end{lemma}
+ \end{theorem}
\begin{proof}
@@ -674,7 +683,7 @@
\end{proof}
-Pictorially, the algorithm is as follows (
+We now give a pictorial view of the algorithm (
For convenience, we employ the following notations: the regular
expression we start with is $r_0$, and the given string $s$ is composed
of characters $c_0 c_1 \ldots c_{n-1}$. The
@@ -735,7 +744,7 @@
\end{figure}\label{fig:BetterWaterloo}
That is because our lexing algorithm currently keeps a lot of
-"useless values that will never not be used.
+"useless" values that will not be used.
These different ways of matching will grow exponentially with the string length.
For $r= (a^*\cdot a^*)^*$ and
@@ -744,10 +753,10 @@
there will be $n - 1$ "splitting points" on $s$ we can independently choose to
split or not so that each sub-string
segmented by those chosen splitting points will form different iterations.
-For example when $n=4$,
+For example when $n=4$, we give out a few of the many possibilities of splitting:
\begin{center}
\begin{tabular}{lcr}
-$aaaa $ & $\rightarrow$ & $\Stars\, [v_{iteration \,aaaa}]$ (1 iteration, this iteration will be divided between the inner sequence $a^*\cdot a^*$)\\
+$aaaa $ & $\rightarrow$ & $\Stars\, [v_{iteration \,aaaa}]$ (1 iteration)\\
$a \mid aaa $ & $\rightarrow$ & $\Stars\, [v_{iteration \,a},\, v_{iteration \,aaa}]$ (two iterations)\\
$aa \mid aa $ & $\rightarrow$ & $\Stars\, [v_{iteration \, aa},\, v_{iteration \, aa}]$ (two iterations)\\
$a \mid aa\mid a $ & $\rightarrow$ & $\Stars\, [v_{iteration \, a},\, v_{iteration \, aa}, \, v_{iteration \, a}]$ (three iterations)\\