% 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''

the functions and datatypes of our formalisation in Isabelle/HOL.

We also define what $\POSIX$ lexing means, 

followed by the first lexing algorithm by Sulzmanna and Lu \parencite{Sulzmann2014} 

that produces the output conforming

to the $\POSIX$ standard\footnote{In what follows 

we choose to use the Isabelle-style notation

for function applications, where

the parameters of a function are 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}

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

%\newcommand\notate[3]{%

%  \unskip\def\useanchorwidth{T}%

%  \setbox0=\hbox{#1}%

%  \def\stackalignment{c}\stackunder[-6pt]{%

%    \def\stackalignment{c}\stackunder[-1.5pt]{%

%      \stackunder[-2pt]{\strut #1}{\myupbracefill{\wd0}}}{%

%    \rule{\rlwd}{#2\baselineskip}}}{%

%  \strut\kern7pt$\hookrightarrow$\rlap{ \footnotesize#3}}\ignorespaces%

%}

%\Longstack{

%\notate{$\{ \ldots ,\;$ 

%	\notate{s}{1}{$(c_1 :: s_1)$} 

%	$, \; \ldots \}$ 

%}{1}{$S_{start}$} 

%}

%\Longstack{

%	$\stackrel{\backslash c_1}{\longrightarrow}$

%}

%\Longstack{

%	$\{ \ldots,\;$  \notate{$s_1$}{1}{$(c_2::s_2)$} 

%	$,\; \ldots \}$

%}

%\Longstack{

%	$\stackrel{\backslash c_2}{\longrightarrow}$ 

%}

%\Longstack{

%	$\{ \ldots,\;  s_2

%	,\; \ldots \}$

%}

%\Longstack{

%	$ \xdashrightarrow{\backslash c_3\ldots\ldots} $	

%}

%\Longstack{

%	\notate{$\{\ldots, [], \ldots\}$}{1}{$S_{end} = 

%	S_{start}\backslash s$}

%}

%\end{center}

%\begin{center}

%	$s \in S_{start} \iff [] \in S_{end}$

%\end{center}

%\noindent

Brzozowski noticed that $\Der$

can be ``mirrored'' on regular expressions which

he calls the derivative of a regular expression $r$

with respect to a character $c$, written

$r \backslash c$. This infix operator

takes regular expression $r$ as input

and a character as a right operand.

The derivative operation on regular expression

is defined such that the language of the derivative result 

coincides with the language of the original 

regular expression being taken 

derivative with respect to the same characters, namely

\begin{property}

\[

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

\]

\end{property}

\noindent

Pictorially, this looks as follows:\\

\vspace{3mm}

\parskip \baselineskip

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

\def\rlwd{.5pt}

\newcommand\notate[3]{%

  \unskip\def\useanchorwidth{T}%

  \setbox0=\hbox{#1}%

  \def\stackalignment{c}\stackunder[-6pt]{%

    \def\stackalignment{c}\stackunder[-1.5pt]{%

      \stackunder[-2pt]{\strut #1}{\myupbracefill{\wd0}}}{%

    \rule{\rlwd}{#2\baselineskip}}}{%

  \strut\kern8pt$\hookrightarrow$\rlap{ \footnotesize#3}}\ignorespaces%

}

\Longstack{

	\notate{$r$}{1}{$L \; r = \{\ldots, \;c::s_1, 

\;\ldots\}$}

}

\Longstack{

	$\stackrel{\backslash c}{\xrightarrow{\hspace*{8cm}}}$

}

\Longstack{

	\notate{$r\backslash c$}{1}{$L \; (r\backslash c)=

	\{\ldots,\;s_1,\;\ldots\}$}

}\\ 

\vspace{ 3mm }

The derivatives on regular expression can again be 

generalised to strings.

One could compute $r_{start} \backslash s$  and test membership of $s$

in $L \; r_{start}$ by checking

whether the empty string is in the language of 

$r_{end}$ (that is $r_{start}\backslash s$).\\

\vspace{2mm}

\Longstack{

	\notate{$r_{start}$}{4}{

		\Longstack{$L \; r_{start} = \{\ldots, \;$ 

			\notate{$s$}{1}{$c_1::s_1$} 

		$, \ldots\} $

		}

	} 

}

\Longstack{

	$\stackrel{\backslash c_1}{ \xrightarrow{\hspace*{1.8cm}} }$

}

\Longstack{

	\notate{$r_1$}{3}{

		$r_1 = r_{start}\backslash c_1$,

		$L \; r_1 = $

	\Longstack{

		$\{ \ldots,\;$  \notate{$s_1$}{1}{$c_2::s_2$} 

		$,\; \ldots \}$

	}

}

}

\Longstack{

	$\stackrel{\backslash c_2}{\xrightarrow{\hspace*{1.8cm}}}$ 

}

\Longstack{

	$r_2$	

}

\Longstack{

	$  \xdashrightarrow{\hspace*{0.3cm} \backslash c_3 \ldots \ldots \ldots \hspace*{0.3cm}} $	

}

\Longstack{

	\notate{$r_{end}$}{1}{

	$L \; r_{end} = \{\ldots, \; [], \ldots\}$}

}

We have the property that

\begin{property}

	$s \in L \; r_{start} \iff [] \in L \; r_{end}$

\end{property}

\noindent

Next, we give the recursive definition of derivative on

regular expressions so that it satisfies the properties above.

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

%takes a regular expression $r$ and character $c$, and

%returns a new regular expression representing

%the original regular expression's language $L \; r$

%being taken the language derivative with respect to $c$.

\begin{table}

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

\caption{Derivative on Regular Expressions}

\label{table:der}

\end{table}

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

\begin{center}

	\begin{tabular}{lcl}

		$(r_1 \cdot r_2 ) \backslash c$ & $\dn$ & 

		$\textit{if}\;\,([] \in L(r_1))\; 

		\textit{then} \; (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

Notice how this closely resembles

the language derivative operation $\Der$:

\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

The derivative of the star regular expression $r^*$ 

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:

\[

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

\]

Again,

the structure is the same as the language derivative of the Kleene star: 

\[

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

\]

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.  

\noindent

We have the following two correspondences between 

derivatives on regular expressions and

derivatives on a set of strings:

\begin{lemma}\label{derDer}