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:

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:

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

is defined as the Kleene star operator:

\noindent

However, to obtain a convenient induction principle 

in Isabelle/HOL, 

\begin{mathpar}

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

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

\end{mathpar}

We also define an operation of "chopping of" a character from

a language, which we call $\Der$, meaning "Derivative for a language":

\noindent

This can be generalised to "chopping off" a string from all strings within set $A$,

with the help of the concatenation operator:

\noindent

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

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

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

\noindent

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 

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

\noindent

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

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

\begin{center}

r\backslash c \dn ?

so that

\[

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

\]

\end{center}

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

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

which tests whether the empty string $""$ 

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

Building derivatives and then testing the existence

of empty string in the resulting regular expression's language.

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

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

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

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

\subsection*{Values and the Lexing Algorithm by Sulzmann and Lu}

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

to the next token.

\end{itemize}

The reason why we are interested in $\POSIX$ values is that they can

be practically used in the lexing phase of a compiler front end.

For instance, when lexing a code snippet 

$\textit{iffoo} = 3$ with the regular expression $\textit{keyword} + \textit{identifier}$, we want $\textit{iffoo}$ to be recognized

as an identifier rather than a keyword.

The good property about a $\POSIX$ value is that 

given the same regular expression $r$ and string $s$,

one can always uniquely determine the $\POSIX$ value for it:

\begin{lemma}

$\textit{if} \,(s, r) \rightarrow v_1 \land (s, r) \rightarrow v_2\quad  \textit{then} \; v_1 = v_2$

\end{lemma}

Now we know what a $\POSIX$ value is, the problem is how do we achieve 

such a value in a lexing algorithm, using derivatives?

\subsection{Sulzmann and Lu's Injection-based Lexing Algorithm}

The contribution of Sulzmann and Lu is an extension of Brzozowski's

algorithm by a second phase (the first phase being building successive

derivatives---see \eqref{graph:successive_ders}). In this second phase, a POSIX value 

is generated if the regular expression matches the string.

Two functions are involved: $\inj$ and $\mkeps$.

The function $\mkeps$ constructs a value from the last

one of all the successive derivatives:

\begin{ceqn}

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

\begin{tikzcd}

r_0 \arrow[r, "\backslash c_0"]  & r_1 \arrow[r, "\backslash c_1"] & r_2 \arrow[r, dashed] & r_n \arrow[d, "mkeps" description] \\

	        & 	              & 	            & v_n       

\end{tikzcd}

\end{equation}

\end{ceqn}

It tells us how can an empty string be matched by a 

regular expression, in a $\POSIX$ way:

	\begin{center}

		\begin{tabular}{lcl}

			$\mkeps(\ONE)$ 		& $\dn$ & $\Empty$ \\

			$\mkeps(r_{1}+r_{2})$	& $\dn$ 

			& \textit{if} $\nullable(r_{1})$\\ 

			& & \textit{then} $\Left(\mkeps(r_{1}))$\\ 

			& & \textit{else} $\Right(\mkeps(r_{2}))$\\

			$\mkeps(r_1\cdot r_2)$ 	& $\dn$ & $\Seq\,(\mkeps\,r_1)\,(\mkeps\,r_2)$\\

			$mkeps(r^*)$	        & $\dn$ & $\Stars\,[]$

		\end{tabular}

	\end{center}

\noindent 

We favour the left to match an empty string if there is a choice.

When there is a star for us to match the empty string,

we give the $\Stars$ constructor an empty list, meaning

no iterations are taken.

The result of a call to $\mkeps$ on a $\nullable$ $r$ would

be a $\POSIX$ value corresponding to $r$:

\begin{lemma}

$\nullable(r) \implies (r, []) \rightarrow (\mkeps\; v)$

\end{lemma}\label{mePosix}

After the $\mkeps$-call, we inject back the characters one by one in order to build

the lexical value $v_i$ for how the regex $r_i$ matches the string $s_i$

($s_i = c_i \ldots c_{n-1}$ ) from the previous lexical value $v_{i+1}$.

After injecting back $n$ characters, we get the lexical value for how $r_0$

matches $s$. 

To do this, Sulzmann and Lu defined a function that reverses

the ``chopping off'' of characters during the derivative phase. The

corresponding function is called \emph{injection}, written

$\textit{inj}$; it takes three arguments: the first one is a regular

expression ${r_{i-1}}$, before the character is chopped off, the second

is a character ${c_{i-1}}$, the character we want to inject and the

third argument is the value ${v_i}$, into which one wants to inject the

character (it corresponds to the regular expression after the character

has been chopped off). The result of this function is a new value. 

\begin{ceqn}

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

\begin{tikzcd}

r_1 \arrow[r, dashed] \arrow[d]& r_i \arrow[r, "\backslash c_i"]  \arrow[d]  & r_{i+1}  \arrow[r, dashed] \arrow[d]        & r_n \arrow[d, "mkeps" description] \\

v_1           \arrow[u]                 & v_i  \arrow[l, dashed]                              & v_{i+1} \arrow[l,"inj_{r_i} c_i"]                 & v_n \arrow[l, dashed]         

\end{tikzcd}

\end{equation}

\end{ceqn}