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

%and then give the algorithm and its variant and discuss

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.

Usually, formal language theory starts with an alphabet 

In what follows, we shall leave the information about the alphabet

way as we concatenate two lists, which we shall write as $s_1 @ s_2$.

The union of all powers of a language   

can be used to define the Kleene star operator:

However, to obtain a more convenient induction principle 

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

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

\noindent

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

With the sequencing, Kleene star, and $\textit{Der}$ operator on languages,

There are too inclusions to prove:

\item{$\subseteq$}:\\

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

\item{$\supseteq$}:\\

hold.

Also this holds:

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

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

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

The \emph{basic regular expressions} are defined inductively

We call them basic because we will introduce

additional constructors in later chapters such as negation

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:

$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)*$

%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 semantic derivative acts on a set of 

strings. Brzozowski noticed that this operation

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

He defined this operation such that the following property holds:

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}

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.

The most involved cases are the sequence case

and the star case.

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}

(that enables us to reason about the correctness of

derivative-based matching)

is 

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

When there is no ambiguity, we will 

omit the subscript and use $\backslash$ instead

of $\backslash_r$ to denote

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

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

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

	and lemma \ref{derDer}. 

\begin{center}

	\begin{figure}

\end{center} 

If we implement the above algorithm naively, however,

the algorithm can be excruciatingly slow, as shown in 

\ref{NaiveMatcher}.

Note that both axes are in logarithmic scale.

Around two dozens characters

would already explode the matcher on regular expression 

$(a^*)^*b$.

For this, we need to introduce certain 

One simpled-minded simplification function

that achieves these requirements is given below:

\begin{center}

	\begin{tabular}{lcl}

		$\simp \; r_1 \cdot r_2 $ & $ \dn$ & 

		$(\simp \; r_1,  \simp \; r_2) \; \textit{match}$\\

					  & & $\quad \case \; (\ZERO, \_) \Rightarrow \ZERO$\\

					  & & $\quad \case \; (\_, \ZERO) \Rightarrow \ZERO$\\

					  & & $\quad \case \; (\ONE, r_2') \Rightarrow r_2'$\\

					  & & $\quad \case \; (r_1', \ONE) \Rightarrow r_1'$\\

					  & & $\quad \case \; (r_1', r_2') \Rightarrow r_1'\cdot r_2'$\\

		$\simp \; r_1 + r_2$ & $\dn$ & $(\simp \; r_1, \simp \; r_2) \textit{match}$\\

				     & & $\quad \; \case \; (\ZERO, r_2') \Rightarrow r_2'$\\

				     & & $\quad \; \case \; (r_1', \ZERO) \Rightarrow r_1'$\\

				     & & $\quad \; \case \; (r_1', r_2') \Rightarrow r_1' + r_2'$\\

		$\simp \; r$ & $\dn$ & $r$

	\end{tabular}

\end{center}

If we repeatedly apply this simplification  

function during the matching algorithm, 

we have a matcher with simplification:

\begin{center}

	\begin{tabular}{lcl}

		$\derssimp \; [] \; r$ & $\dn$ & $r$\\

		$\derssimp \; c :: cs \; r$ & $\dn$ & $\derssimp \; cs \; (\simp \; (r \backslash c))$\\

		$\textit{matcher}_{simp}\; s \; r $ & $\dn$ & $\nullable \; (\derssimp \; s\;r)$

	\end{tabular}

\end{center}

\begin{figure}

    grid = both,

\end{tikzpicture} 

\caption{$(a^*)^*b$ 

against 

$\protect\underbrace{aa\ldots a}_\text{n \textit{a}s}$ Using $\textit{matcher}_{simp}$}\label{BetterMatcher}

\end{figure}

\noindent

The running time of $\textit{ders}\_\textit{simp}$

on the same example of \ref{NaiveMatcher}

is now very tame in terms of the length of inputs,

as shown in \ref{BetterMatcher}.

adding simplifications when necessary.

Sulzmanna and Lu \cite{Sulzmann2014} first came up with a nice and 

In this section, we present a two-phase regular expression lexing 

algorithm.

The first phase takes successive derivatives with 

respect to the input string,

and the second phase does the reverse, \emph{injecting} back

characters, in the meantime constructing a lexing result.

We will introduce the injection phase in detail slightly

later, but as a preliminary we have to first define 

the datatype for lexing results, 

called \emph{value} or

sometimes also \emph{lexical value}.  Values and regular