% 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 

% used 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.

This is essentially a description in ``English"

of our formalisation in Isabelle/HOL.

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

followed by an algorithm by Sulzmanna and Lu\parencite{Sulzmann2014} 

that produces the output conforming

to the $\POSIX$ standard.

It is also worth mentioning that

we choose to use the ML-style notation

for function applications, where

the parameters of a function is not enclosed

inside a pair of parentheses (e.g. $f \;x \;y$

instead of $f(x,\;y)$). This is mainly

to make the text visually more concise.

\section{Basic Concepts}

Usually, formal language theory starts with an alphabet 

denoting a set of characters.

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{s}$ & $\dn$ & $[] \; |\; c  :: s$

\end{tabular}

\end{center}

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 shall write as $s_1 @ s_2$.

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 \land 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 @ A^n$

\end{tabular}

\end{center}

The union of all powers of a language   

can be used to define 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 more convenient induction principle 

in Isabelle/HOL, 

we instead define the Kleene star

as an inductive set: 

\begin{center}

\begin{mathpar}

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

\inferrule{s_1 \in A \;\; s_2 \in A*}{s_1 @ s_2 \in A*}

\end{mathpar}

\end{center}

\noindent

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$, 

namely:

\begin{center}

\begin{tabular}{lcl}

$\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 with $L = \{w\}$

in formal language theory.

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 

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}

There are too inclusions to prove:

\begin{itemize}

\item{$\subseteq$}:\\

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*) ) \]

hold.

Also this holds:

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

where the $\textit{RHS}$ can be rewritten

as \[ (\Der \; c\; A) @ A* \cup (\Der \; c \; (A*)) \]

which of course contains $\Der \; c \; A @ A*$.

\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 \emph{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 will introduce

additional constructors in later chapters such as negation

and bounded repetitions.

We use $\ZERO$ for the regular expression that

matches no string, and $\ONE$ for the regular

expression that matches only the empty string\footnote{

some authors

also use $\phi$ and $\epsilon$ for $\ZERO$ and $\ONE$

but we prefer our notation}. 

The sequence regular expression is written $r_1\cdot r_2$

and sometimes we omit the dot if it is clear which

regular expression is meant; the alternative

is written $r_1 + r_2$.

The \emph{language} or meaning of 

a regular expression is defined recursively as

a set of strings:

%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 @ L \; r_2$\\

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

\end{tabular}

\end{center}

\noindent

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}

%Recall, the language derivative acts on a set of strings

%and essentially chops off a particular character from

%all strings in that set, Brzozowski defined 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)$:

can be ``mirrored" on regular expressions which

he calls the derivative of a regular expression $r$

with respect to a character $c$, written

\begin{center}

\[

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

\]

\end{center}

\noindent

For example in the sequence case we have 

\begin{center}

	\begin{tabular}{lcl}

		$\Der \; c \; (A @ B)$ & $\dn$ & 

		$ \textit{if} \;\,  [] \in A \; 

		\textit{then} \;\, ((\Der \; c \; A) @ B ) \cup 

		\Der \; c\; B$\\

		& & $\textit{else}\; (\Der \; c \; A) @ B$\\

	\end{tabular}

\end{center}

\noindent

This can be translated to  

regular expressions in the following 

manner:

\begin{center}

	\begin{tabular}{lcl}

		$(r_1 \cdot r_2 ) \backslash c$ & $\dn$ & $\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$

	\end{tabular}

\end{center}

\noindent

And similarly, the Kleene star's semantic derivative

can be expressed as

\[

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

\]

which translates to

\[

	(r^*) \backslash c \dn (r \backslash c)\cdot r^*.

\]

In the above definition of $(r_1\cdot r_2) \backslash c$,

the $\textit{if}$ clause's

boolean condition 

$[] \in L(r_1)$ needs to be 

somehow recursively computed.

We call such a function that checks

whether the empty string $[]$ is 

in the language of a regular expression $\nullable$:

\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 $\ZERO$ regular expression

does not contain any string and

therefore is not \emph{nullable}.

$\ONE$ is \emph{nullable} 

by definition. 

The character regular expression $c$

corresponds to the singleton set $\{c\}$, 

and therefore does not contain the empty string.

The alternative regular expression is nullable

if at least one of its children is nullable.

The sequence regular expression

would require both children to have the empty string

to compose an empty string, and the Kleene star

is always nullable because it naturally

contains the empty string. 

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

defines how a regular expression evolves into

a new one after all the string it contains is acted on: 

if it starts with $c$, then the character is chopped of,

if not, that string is removed.

\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 most involved cases are the sequence case

and the star case.

The sequence case says that if the first regular expression

contains an empty string, then the second component of the sequence

needs to be considered, as its derivative will contribute to the

result of this derivative.

The star regular expression $r^*$'s derivative 

unwraps one iteration of $r$, turns it into $r\backslash c$,

and attaches the original $r^*$

after $r\backslash c$, so that 

we can further unfold it as many times as needed.

We have the following correspondence between 

derivatives on regular expressions and

derivatives on a set of strings:

\begin{lemma}\label{derDer}

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

derivative-based matching)

is 

\begin{lemma}\label{derStepwise}

	$c\!::\!s \in L(r)$ \textit{iff} $s \in L(r\backslash c)$.

\end{lemma}

\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 

omit the subscript and use $\backslash$ instead

of $\backslash_r$ to denote

string derivatives for brevity.

Brzozowski's  regular-expression matcher algorithm can then be described as:

\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

 It can  be

relatively  easily shown that this matcher is correct:

\begin{lemma}

	$\textit{match} \; s\; r  = \textit{true} \; \textit{iff} \; s \in L(r)$

\end{lemma}

\begin{proof}

	By the stepwise property of derivatives (lemma \ref{derStepwise})

	and lemma \ref{derDer}. 

\end{proof}

\noindent

\begin{center}

	\begin{figure}

\begin{tikzpicture}

\begin{axis}[

    xlabel={$n$},

    ylabel={time in secs},

    ymode = log,

    legend entries={Naive Matcher},  

    legend pos=north west,

    legend cell align=left]

\addplot[red,mark=*, mark options={fill=white}] table {NaiveMatcher.data};