% Chapter Template

\chapter{Regular Expressions and POSIX Lexing-Preliminaries} % 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. 

%We give a taste of what they 

%are like and why they are suitable for regular expression

%matching and lexing.

\section{Formal Specification of POSIX Matching 

and Brzozowski Derivatives}

%Now we start with the central topic of the thesis: Brzozowski derivatives.

Brzozowski \cite{Brzozowski1964} first introduced the 

concept of a \emph{derivative} of regular expression in 1964.

The derivative of a regular expression $r$

with respect to a character $c$, is written as $r \backslash c$.

This operation tells us what $r$ transforms into

if we ``chop'' off a particular character $c$ 

from all strings in the language of $r$ (defined

later as $L \; r$).

%To give a flavour of Brzozowski derivatives, we present

%two straightforward clauses from it:

%\begin{center}

%	\begin{tabular}{lcl}

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

%	\end{tabular}

%\end{center}

%\noindent

%The first clause says that for the regular expression

%denoting a singleton set consisting of a single-character string $\{ d \}$,

%we check the derivative character $c$ against $d$,

%returning a set containing only the empty string $\{ [] \}$

%if $c$ and $d$ are equal, and the empty set $\varnothing$ otherwise.

%The second clause states that to obtain the regular expression

%representing all strings' head character $c$ being chopped off

%from $r_1 + r_2$, one simply needs to recursively take derivative

%of $r_1$ and $r_2$ and then put them together.

Derivatives have the property

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

$c::s \in L \; r$ where $::$ stands for list prepending.

%This property can be used on regular expressions

%matching and lexing--to test whether a string $s$ is in $L \; r$,

%one simply takes derivatives of $r$ successively with

%respect to the characters (in the correct order) in $s$,

%and then test whether the empty string is in the last regular expression.

With this property, derivatives can give a simple solution

to the problem of matching a string $s$ with a regular

expression $r$: if the derivative of $r$ w.r.t.\ (in

succession) all the characters of the string matches the empty string,

then $r$ matches $s$ (and {\em vice versa}).  

%This makes formally reasoning about these properties such

%as correctness and complexity smooth and intuitive.

There are several mechanised proofs of this property in various theorem

provers,

for example one by Owens and Slind \cite{Owens2008} in HOL4,

another one by Krauss and Nipkow \cite{Nipkow98} in Isabelle/HOL, and

yet another in Coq by Coquand and Siles \cite{Coquand2012}.

In addition, one can extend derivatives to bounded repetitions

relatively straightforwardly. For example, the derivative for 

this can be defined as:

\begin{center}

	\begin{tabular}{lcl}

		$r^{\{n\}} \backslash c$     & $\dn$ & $r \backslash c \cdot

		r^{\{n-1\}} (\text{when} n > 0)$\\

	\end{tabular}

\end{center}

\noindent

Experimental results suggest that  unlike DFA-based solutions

for bounded regular expressions,

derivatives can cope

large counters

quite well.

There have also been 

extensions of derivatives to other regex constructs.

For example, Owens et al include the derivatives

for the \emph{NOT} regular expression, which is

able to concisely express C-style comments of the form

$/* \ldots */$ (see \cite{Owens2008}).

Another extension for derivatives is

regular expressions with look-aheads, done

by Miyazaki and Minamide

\cite{Takayuki2019}.

%We therefore use Brzozowski derivatives on regular expressions 

%lexing 

Given the above definitions and properties of

Brzozowski derivatives, one quickly realises their potential

in generating a formally verified algorithm for lexing: the clauses and property

can be easily expressed in a functional programming language 

or converted to theorem prover

code, with great ease.

Perhaps this is the reason why derivatives have sparked quite a bit of interest

in the functional programming and theorem prover communities in the last

fifteen or so years (

\cite{Almeidaetal10}, \cite{Berglund14}, \cite{Berglund18},

\cite{Chen12} and \cite{Coquand2012}

to name a few), despite being buried in the ``sands of time'' \cite{Owens2008}

after they were first published by Brzozowski.

However, there are two difficulties with derivative-based matchers:

First, Brzozowski's original matcher only generates a yes/no answer

for whether a regular expression matches a string or not.  This is too

little information in the context of lexing where separate tokens must

be identified and also classified (for example as keywords

or identifiers). 

Second, derivative-based matchers need to be more efficient in terms

of the sizes of derivatives.

Elegant and beautiful

as many implementations are,

they can be still quite slow. 

For example, Sulzmann and Lu

claim a linear running time of their proposed algorithm,

but that was falsified by our experiments. The running time 

is actually $\Omega(2^n)$ in the worst case.

A similar claim about a theoretical runtime of $O(n^2)$ 

is made for the Verbatim \cite{Verbatim}

%TODO: give references

lexer, which calculates POSIX matches and is based on derivatives.

They formalized the correctness of the lexer, but not their complexity result.

In the performance evaluation section, they analyzed the run time

of matching $a$ with the string 

\begin{center}

	$\underbrace{a \ldots a}_{\text{n a's}}$.

\end{center}

\noindent

They concluded that the algorithm is quadratic in terms of 

the length of the input string.

When we tried out their extracted OCaml code with the example $(a+aa)^*$,

the time it took to match a string of 40 $a$'s was approximately 5 minutes.

\subsection{Sulzmann and Lu's Algorithm}

Sulzmann and Lu~\cite{Sulzmann2014} overcame the first 

problem with the yes/no answer 

by cleverly extending Brzozowski's matching

algorithm. Their extended version generates additional information on

\emph{how} a regular expression matches a string following the POSIX

rules for regular expression matching. They achieve this by adding a

second ``phase'' to Brzozowski's algorithm involving an injection

function. This injection function in a sense undoes the ``damage''

of the derivatives chopping off characters.

In earlier work, Ausaf et al provided the formal

specification of what POSIX matching means and proved in Isabelle/HOL

the correctness

of this extended algorithm accordingly

\cite{AusafDyckhoffUrban2016}.

The version of the algorithm proven correct

suffers however heavily from a 

second difficulty, where derivatives can

grow to arbitrarily big sizes. 

For example if we start with the

regular expression $(a+aa)^*$ and take

successive derivatives according to the character $a$, we end up with

a sequence of ever-growing derivatives like 

\def\ll{\stackrel{\_\backslash{} a}{\longrightarrow}}

\begin{center}

\begin{tabular}{rll}

$(a + aa)^*$ & $\ll$ & $(\ONE + \ONE{}a) \cdot (a + aa)^*$\\

& $\ll$ & $(\ZERO + \ZERO{}a + \ONE) \cdot (a + aa)^* \;+\; (\ONE + \ONE{}a) \cdot (a + aa)^*$\\

& $\ll$ & $(\ZERO + \ZERO{}a + \ZERO) \cdot (a + aa)^* + (\ONE + \ONE{}a) \cdot (a + aa)^* \;+\; $\\

& & $\qquad(\ZERO + \ZERO{}a + \ONE) \cdot (a + aa)^* + (\ONE + \ONE{}a) \cdot (a + aa)^*$\\

& $\ll$ & \ldots \hspace{15mm}(regular expressions of sizes 98, 169, 283, 468, 767, \ldots)

\end{tabular}

\end{center}

\noindent where after around 35 steps we usually run out of memory on a

typical computer.  Clearly, the

notation involving $\ZERO$s and $\ONE$s already suggests

simplification rules that can be applied to regular regular

expressions, for example $\ZERO{}\,r \Rightarrow \ZERO$, $\ONE{}\,r

\Rightarrow r$, $\ZERO{} + r \Rightarrow r$ and $r + r \Rightarrow

r$. While such simple-minded simplifications have been proved in 

the work by Ausaf et al. to preserve the correctness of Sulzmann and Lu's

algorithm \cite{AusafDyckhoffUrban2016}, they unfortunately do

\emph{not} help with limiting the growth of the derivatives shown

above: the growth is slowed, but the derivatives can still grow rather

quickly beyond any finite bound.

Therefore we want to look in this thesis at a second

algorithm by Sulzmann and Lu where they

overcame this ``growth problem'' \cite{Sulzmann2014}.

In this version, POSIX values are 

represented as bit sequences and such sequences are incrementally generated

when derivatives are calculated. The compact representation

of bit sequences and regular expressions allows them to define a more

``aggressive'' simplification method that keeps the size of the

derivatives finite no matter what the length of the string is.

They make some informal claims about the correctness and linear behaviour

of this version, but do not provide any supporting proof arguments, not

even ``pencil-and-paper'' arguments. They write about their bit-coded

\emph{incremental parsing method} (that is the algorithm to be formalised

in this dissertation)

  \begin{quote}\it

  ``Correctness Claim: We further claim that the incremental parsing

  method [..] in combination with the simplification steps [..]

  yields POSIX parse trees. We have tested this claim

  extensively [..] but yet

  have to work out all proof details.'' \cite[Page 14]{Sulzmann2014}

\end{quote}  

Ausaf and Urban made some initial progress towards the 

full correctness proof but still had to leave out the optimisation

Sulzmann and Lu proposed.

Ausaf  wrote \cite{Ausaf},

  \begin{quote}\it

``The next step would be to implement a more aggressive simplification procedure on annotated regular expressions and then prove the corresponding algorithm generates the same values as blexer. Alas due to time constraints we are unable to do so here.''

\end{quote}  

This thesis implements the aggressive simplifications envisioned

by Ausaf and Urban,

together with a formal proof of the correctness of those simplifications.

One of the most recent work in the context of lexing

%with this issue

is the Verbatim lexer by Egolf, Lasser and Fisher~\cite{Verbatim}.

This is relevant work for us and we will compare it later with 

our derivative-based matcher we are going to present.

There is also some newer work called

Verbatim++~\cite{Verbatimpp}, which does not use derivatives, 

but deterministic finite automaton instead.

We will also study this work in a later section.

%An example that gives problem to automaton approaches would be

%the regular expression $(a|b)^*a(a|b)^{\{n\}}$.

%It requires at least $2^{n+1}$ states to represent

%as a DFA.

\section{Basic Concepts}

Formal language theory usually starts with an alphabet 

denoting a set of characters.

Here we 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 as: 

\begin{center}

\begin{tabular}{lcl}

$\textit{s}$ & $\dn$ & $[] \; |\; c  :: s$

\end{tabular}

\end{center}

where $c$ is a variable ranging over characters.

The $::$ stands for list cons and $[]$ for the empty

list.

For brevity, a singleton list is sometimes written as $[c]$.

Strings can be concatenated to form longer strings in the same

way 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 a 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 = \{s\}$.

However, for our purposes here, the $\textit{Ders}$ definition with 

a single string is sufficient.

The reason for defining derivatives

is that they provide another approach

to test membership of a string in 

a set of strings. 

For example, to test whether the string

$bar$ is contained in the set $\{foo, bar, brak\}$, one can take derivative of the set with

respect to the string $bar$:

\begin{center}

\begin{tabular}{lll}

	$S = \{foo, bar, brak\}$ & $ \stackrel{\backslash b}{\rightarrow }$ & 

	$\{ar, rak\}$ \\

				 & $\stackrel{\backslash a}{\rightarrow}$ & $\{r \}$\\

				 & $\stackrel{\backslash r}{\rightarrow}$ & $\{[]\}$\\

				 %& $\stackrel{[] \in S \backslash bar}{\longrightarrow}$ & $bar \in S$\\

\end{tabular}	

\end{center}

\noindent

and in the end, test whether the set

contains the empty string.\footnote{We use the infix notation $A\backslash c$

	instead of $\Der \; c \; A$ for brevity, as it will always be

	clear from the context that we are operating

on languages rather than regular expressions.}

In general, if we have a language $S$,

then we can test whether $s$ is in $S$

by testing whether $[] \in S \backslash s$.

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.

For example, for the sequence operator, we have

something similar to a ``chain rule'':

\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 derivative for $A*$ 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 two inclusions to prove:

\begin{itemize}

\item{$\subseteq$}:\\

The set 

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

is enclosed in the set

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

This is because for any string $c::s$ satisfying $c::s \in A*$,

%whenever you have a string starting with a character 

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

%then that

the character $c$, together with a prefix of $s$

%immediately after $c$ 

forms the first iteration of $A*$, 

and the rest of the $s$ is also $A*$.

This coincides with the definition of $S_2$.

\item{$\supseteq$}:\\

Note that

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

holds.

Also the following 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

The clever idea of Brzozowski was to find counterparts of $\Der$ and $\Ders$

for regular expressions.

To introduce them, we need to first give definitions for regular expressions,

which we shall do next.

\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 this 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$ & $\varnothing$\\

$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 language derivatives of a language and regular expressions and

%their language interpretations in place, we are ready to define derivatives on regular expressions.

With $L$, we are ready to introduce Brzozowski derivatives on regular expressions.

We do so by first introducing what properties they should satisfy.

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

%Recall that the language derivative acts on a 

%language (set of strings).

%One can decide whether a string $s$ belongs

%to a language $S$ by taking derivative with respect to

%that string and then checking whether the empty 

%string is in the derivative:

%\begin{center}

%\parskip \baselineskip

%\def\myupbracefill#1{\rotatebox{90}{\stretchto{\{}{#1}}}

%\def\rlwd{.5pt}