% Chapter Template

\chapter{Regular Expressions and POSIX Lexing} % Main chapter title

\label{Inj} % In chapter 2 \ref{Chapter2} we will introduce the concepts

%and notations we 

%use for describing the lexing algorithm by Sulzmann and Lu,

%and then give the algorithm and its variant, and discuss

%why more aggressive simplifications are needed. 

In this chapter, we define the basic notions 

for regular languages and regular expressions.

We also give the definition of what $\POSIX$ lexing means.

\section{Basic Concepts}

Usually in formal language theory there is 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:

\begin{center}

\begin{tabular}{lcl}

$\textit{string}$ & $\dn$ & $[] | c  :: cs$\\

& & $(c\; \text{has char type})$

\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 

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 \}$\\

\end{tabular}

\end{center}

We also call the above \emph{language concatenation}.

The power of a language is defined recursively, using the 

concatenation operator $@$:

\begin{center}

\begin{tabular}{lcl}

$A^0 $ & $\dn$ & $\{ [] \}$\\

$A^{n+1}$ & $\dn$ & $A^n @ A$

\end{tabular}

\end{center}

The union of all the natural number powers of a language   

is defined as the Kleene star operator:

\begin{center}

\begin{tabular}{lcl}

 $A*$ & $\dn$ & $\bigcup_{i \geq 0} A^i$ \\

\end{tabular}

\end{center}

\noindent

However, to obtain a convenient induction principle 

in Isabelle/HOL, 

we instead define the Kleene star

as an inductive set: 

\begin{center}

\begin{mathpar}

\inferrule{}{[] \in A*\\}

\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":

\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:

\begin{center}

\begin{tabular}{lcl}

$\textit{Ders} \;w \;A$ & $\dn$ & $\{ s \mid w@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\}$

in formal language theory.

For this dissertation the $\textit{Ders}$ definition with 

a single string suffices.

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 

sub-languages.

\begin{lemma}

\[

	\Der \; c \; (A @ B) =

	\begin{cases}

	((\Der \; c \; A) \, @ \, B ) \cup (\Der \; c\; B) , &  \text{if} \;  [] \in A  \\

	 (\Der \; c \; A) \,  @ \, B, & \text{otherwise}

	 \end{cases}	

\]

\end{lemma}

\noindent

This lemma states that if $A$ contains the empty string, $\Der$ can "pierce" through it

and get to $B$.

The language $A*$'s derivative can be described using the language derivative

of $A$:

\begin{lemma}

$\textit{Der} \;c \;(A*) = (\textit{Der}\; c A) @ (A*)$\\

\end{lemma}

\begin{proof}

\begin{itemize}

\item{$\subseteq$}

\noindent

The set 

\[ \{s \mid c :: s \in A*\} \]

is enclosed in the set

\[ \{s_1 @ s_2 \mid s_1 \, s_2. s_1 \in \{s \mid c :: s \in A\} \land s_2 \in A* \} \]

because whenever you have a string starting with a character 

in the language of a Kleene star $A*$, 

then that character together with some sub-string

immediately after it will form the first iteration, 

and the rest of the string will 

be still in $A*$.

\item{$\supseteq$}

Note that

\[ \Der \; c \; (A*) = \Der \; c \;  (\{ [] \} \cup (A @ A*) ) \]

and 

\[ \Der \; c \;  (\{ [] \} \cup (A @ A*) ) = \Der\; c \; (A @ A*) \]

where the $\textit{RHS}$ of the above equatioin can be rewritten

as \[ (\Der \; c\; A) @ A* \cup A' \], $A'$ being a possibly empty set.

\end{itemize}

\end{proof}

\noindent

Before we define the $\textit{Der}$ and $\textit{Ders}$ counterpart

for regular languages, we need to first give definitions for regular expressions.

\subsection{Regular Expressions and Their Meaning}

The basic regular expressions  are defined inductively

 by the following grammar:

\[			r ::=   \ZERO \mid  \ONE

			 \mid  c  

			 \mid  r_1 \cdot r_2

			 \mid  r_1 + r_2   

			 \mid r^*         

\]

\noindent

We call them basic because we might introduce

more constructs later such as negation

and bounded repetitions.

We defined the regular expression containing

nothing as $\ZERO$, note that some authors

also use $\phi$ for that.

Similarly, the regular expression denoting the 

singleton set with only $[]$ is sometimes 

denoted by $\epsilon$, but we use $\ONE$ here.

The language or set of strings denoted 

by regular expressions are defined as

%TODO: FILL in the other defs

\begin{center}

\begin{tabular}{lcl}

$L \; (\ZERO)$ & $\dn$ & $\phi$\\

$L \; (\ONE)$ & $\dn$ & $\{[]\}$\\

$L \; (c)$ & $\dn$ & $\{[c]\}$\\

$L \; (r_1 + r_2)$ & $\dn$ & $ L \; (r_1) \cup L \; ( r_2)$\\

$L \; (r_1 \cdot r_2)$ & $\dn$ & $ L \; (r_1) \cap L \; (r_2)$\\

$L \; (r^*)$ & $\dn$ & $ (L(r))^*$

\end{tabular}

\end{center}

\noindent

Which is also called the "language interpretation" of

a regular expression.

Now with semantic derivatives of a language and regular expressions and

their language interpretations in place, we are ready to define derivatives on regexes.

\subsection{Brzozowski Derivatives and a Regular Expression Matcher}

\ChristianComment{Hi this part I want to keep the ordering as is, so that it keeps the 

readers engaged with a story how we got to the definition of $\backslash$, rather 

than first "overwhelming" them with the definition of $\nullable$.}

The language derivative acts on a string set and chops off a character from

all strings in that set, we want to define a derivative operation on regular expressions

so that after derivative $L(r\backslash c)$ 

will look as if it was obtained by doing a language derivative on $L(r)$:

\begin{center}

\[

r\backslash c \dn ?

\]

so that

\[

L(r \backslash c) = \Der \; c \; L(r) ?

\]

\end{center}

So we mimic the equalities we have for $\Der$ on language concatenation

\[

\Der \; c \; (A @ B) = \textit{if} \;  [] \in A \; \textit{then} ((\Der \; c \; A) @ B ) \cup \Der \; c\; B \quad \textit{else}\; (\Der \; c \; A) @ B\\

\]

to get the derivative for sequence regular expressions:

\[

(r_1 \cdot r_2 ) \backslash c = \textit{if}\,([] \in L(r_1)) r_1 \backslash c \cdot r_2 + r_2 \backslash c \textit{else} (r_1 \backslash c) \cdot r_2

\]

\noindent

and language Kleene star:

\[

\textit{Der} \;c \;A* = (\textit{Der}\; c A) @ (A*)

\]

to get derivative of the Kleene star regular expression:

\[

r^* \backslash c = (r \backslash c)\cdot r^*

\]

Note that although we can formalise the boolean predicate

$[] \in L(r_1)$ without problems, if we want a function that works

computationally, then we would have to define a function that tests

whether an empty string is in the language of a regular expression.

We call such a function $\nullable$:

\begin{center}

\begin{tabular}{lcl}

		$\ZERO \backslash c$ & $\dn$ & $\ZERO$\\  

		$\ONE \backslash c$  & $\dn$ & $\ZERO$\\

		$d \backslash c$     & $\dn$ & 

		$\mathit{if} \;c = d\;\mathit{then}\;\ONE\;\mathit{else}\;\ZERO$\\

$(r_1 + r_2)\backslash c$     & $\dn$ & $r_1 \backslash c \,+\, r_2 \backslash c$\\

$(r_1 \cdot r_2)\backslash c$ & $\dn$ & $\mathit{if} \, [] \in L(r_1)$\\

	&   & $\mathit{then}\;(r_1\backslash c) \cdot r_2 \,+\, r_2\backslash c$\\

	&   & $\mathit{else}\;(r_1\backslash c) \cdot r_2$\\

	$(r^*)\backslash c$           & $\dn$ & $(r\backslash c) \cdot r^*$\\

\end{tabular}

\end{center}

\noindent

The function derivative, written $r\backslash c$, 

defines how a regular expression evolves into

a new regular expression after all the string it contains

is chopped off a certain head character $c$.

The most involved cases are the sequence 

and star case.

The sequence case says that if the first regular expression

contains an empty string then the second component of the sequence

might be chosen as the target regular expression to be chopped

off its head character.

The star regular expression's derivative unwraps the iteration of

regular expression and attaches the star regular expression

to the sequence's second element to make sure a copy is retained

for possible more iterations in later phases of lexing.

To test whether $[] \in L(r_1)$, we need the $\nullable$ function,

which tests whether the empty string $""$ 

is in the language of $r$:

\begin{center}

		\begin{tabular}{lcl}

			$\nullable(\ZERO)$     & $\dn$ & $\mathit{false}$ \\  

			$\nullable(\ONE)$      & $\dn$ & $\mathit{true}$ \\

			$\nullable(c)$ 	       & $\dn$ & $\mathit{false}$ \\

			$\nullable(r_1 + r_2)$ & $\dn$ & $\nullable(r_1) \vee \nullable(r_2)$ \\

			$\nullable(r_1\cdot r_2)$  & $\dn$ & $\nullable(r_1) \wedge \nullable(r_2)$ \\

			$\nullable(r^*)$       & $\dn$ & $\mathit{true}$ \\

		\end{tabular}

\end{center}

\noindent

The empty set does not contain any string and

therefore not the empty string, the empty string 

regular expression contains the empty string

by definition, the character regular expression

is the singleton that contains character only,

and therefore does not contain the empty string,

the alternative regular expression (or "or" expression)

might have one of its children regular expressions

being nullable and any one of its children being nullable

would suffice. The sequence regular expression

would require both children to have the empty string

to compose an empty string and the Kleene star

operation naturally introduced the empty string. 

We have the following property where the derivative on regular 

expressions coincides with the derivative on a set of strings:

\begin{lemma}

$\textit{Der} \; c \; L(r) = L (r\backslash c)$

\end{lemma}

\noindent

The main property of the derivative operation

that enables us to reason about the correctness of

an algorithm using derivatives is 

$c\!::\!s \in L(r)$ holds

if and only if $s \in L(r\backslash c)$.

\noindent

We can generalise the derivative operation shown above for single characters

to strings as follows:

\begin{center}

\begin{tabular}{lcl}

$r \backslash_s (c\!::\!s) $ & $\dn$ & $(r \backslash c) \backslash_s s$ \\

$r \backslash [\,] $ & $\dn$ & $r$

\end{tabular}

\end{center}

\noindent

When there is no ambiguity we will use  $\backslash$ to denote

string derivatives for brevity.

\begin{definition}

$\textit{match}\;s\;r \;\dn\; \nullable(r\backslash s)$

\end{definition}

\noindent

Assuming the string is given as a sequence of characters, say $c_0c_1..c_n$, 

this algorithm presented graphically is as follows:

\begin{equation}\label{graph:successive_ders}

\begin{tikzcd}

r_0 \arrow[r, "\backslash c_0"]  & r_1 \arrow[r, "\backslash c_1"] & r_2 \arrow[r, dashed]  & r_n  \arrow[r,"\textit{nullable}?"] & \;\textrm{YES}/\textrm{NO}

\end{tikzcd}

\end{equation}

\noindent

Building derivatives and then testing the existence

So far, so good. But what if we want to 

do lexing instead of just getting a YES/NO answer?

elegant (arguably as beautiful as the definition of the original derivative) solution for this.

Here we present the hybrid phases of a regular expression lexing 

algorithm using the function $\inj$, as given by Sulzmann and Lu.

They first defined the datatypes for storing the 

lexing information called a \emph{value} or

sometimes also \emph{lexical value}.  These values and regular

expressions correspond to each other as illustrated in the following

table:

\begin{center}

	\begin{tabular}{c@{\hspace{20mm}}c}

		\begin{tabular}{@{}rrl@{}}

			\multicolumn{3}{@{}l}{\textbf{Regular Expressions}}\medskip\\

			$r$ & $::=$  & $\ZERO$\\

			& $\mid$ & $\ONE$   \\

			& $\mid$ & $c$          \\

			& $\mid$ & $r_1 \cdot r_2$\\

			& $\mid$ & $r_1 + r_2$   \\

			\\

			& $\mid$ & $r^*$         \\

		\end{tabular}

		&

		\begin{tabular}{@{\hspace{0mm}}rrl@{}}

			\multicolumn{3}{@{}l}{\textbf{Values}}\medskip\\

			$v$ & $::=$  & \\

			&        & $\Empty$   \\

			& $\mid$ & $\Char(c)$          \\

			& $\mid$ & $\Seq\,v_1\, v_2$\\

			& $\mid$ & $\Left(v)$   \\

			& $\mid$ & $\Right(v)$  \\

			& $\mid$ & $\Stars\,[v_1,\ldots\,v_n]$ \\

		\end{tabular}

	\end{tabular}

\end{center}

\noindent

We have a formal binary relation for telling whether the structure

of a regular expression agrees with the value.

\begin{mathpar}

\inferrule{}{\vdash \Char(c) : \mathbf{c}} \hspace{2em}

\inferrule{}{\vdash \Empty :  \ONE} \hspace{2em}

\inferrule{\vdash v_1 : r_1 \\ \vdash v_2 : r_2 }{\vdash \Seq(v_1, v_2) : (r_1 \cdot r_2)}

\end{mathpar}

Building on top of Sulzmann and Lu's attempt to formalise the 

notion of POSIX lexing rules \parencite{Sulzmann2014}, 

Ausaf and Urban\parencite{AusafDyckhoffUrban2016} modelled

POSIX matching as a ternary relation recursively defined in a

natural deduction style.

The formal definition of a $\POSIX$ value $v$ for a regular expression

$r$ and string $s$, denoted as $(s, r) \rightarrow v$, can be specified 

in the following set of rules:

\ChristianComment{Will complete later}

\newcommand*{\inference}[3][t]{%

   \begingroup

   \def\and{\\}%

   \begin{tabular}[#1]{@{\enspace}c@{\enspace}}

   #2 \\

   \hline

   #3

   \end{tabular}%

   \endgroup

}

\begin{center}

\inference{$s_1 @ s_2 = s$ \and $(\nexists s_3 s_4 s_5. s_1 @ s_5 = s_3 \land s_5 \neq [] \land s_3 @ s_4 = s \land (s_3, r_1) \rightarrow v_3 \land (s_4, r_2) \rightarrow v_4)$ \and $(s_1, r_1) \rightarrow v_1$ \and $(s_2, r_2) \rightarrow v_2$  }{$(s, r_1 \cdot r_2) \rightarrow \Seq(v_1, v_2)$ }

\end{center}

\noindent

The above $\POSIX$ rules could be explained intuitionally as

\begin{itemize}

\item

match the leftmost regular expression when multiple options of matching

are available  

\item 

always match a subpart as much as possible before proceeding