%

\begin{isabellebody}%

\setisabellecontext{Paper}%

%

\isadelimtheory

%

\endisadelimtheory

%

\isatagtheory

%

\endisatagtheory

{\isafoldtheory}%

%

\isadelimtheory

%

\endisadelimtheory

%

\isadelimproof

%

\endisadelimproof

%

\isatagproof

%

\endisatagproof

{\isafoldproof}%

%

\isadelimproof

%

\endisadelimproof

%

\isadelimproof

%

\endisadelimproof

%

\isatagproof

%

\endisatagproof

{\isafoldproof}%

%

\isadelimproof

%

\endisadelimproof

%

\isadelimdocument

%

\endisadelimdocument

%

\isatagdocument

%

\isamarkupsection{Introduction%

}

\isamarkuptrue%

%

\endisatagdocument

{\isafolddocument}%

%

\isadelimdocument

%

\endisadelimdocument

%

\begin{isamarkuptext}%

This works builds on previous work by Ausaf and Urban using 

regular expression'd bit-coded derivatives to do lexing that 

is both fast and satisfied the POSIX specification.

In their work, a bit-coded algorithm introduced by Sulzmann and Lu

was formally verified in Isabelle, by a very clever use of

flex function and retrieve to carefully mimic the way a value is 

built up by the injection funciton.

In the previous work, Ausaf and Urban established the below equality:

\begin{lemma}

\isa{{\normalsize{}If\,}\ v\ {\isacharcolon}{\kern0pt}\ {\isacharparenleft}{\kern0pt}r\mbox{$^\downarrow$}{\isacharparenright}{\kern0pt}{\isacharbackslash}{\kern0pt}c\ {\normalsize \,then\,}\ retrieve\ {\isacharparenleft}{\kern0pt}r\mbox{$\bbslash$}c{\isacharparenright}{\kern0pt}\ v\ {\isacharequal}{\kern0pt}\ retrieve\ r\ {\isacharparenleft}{\kern0pt}inj\ {\isacharparenleft}{\kern0pt}r\mbox{$^\downarrow$}{\isacharparenright}{\kern0pt}\ c\ v{\isacharparenright}{\kern0pt}{\isachardot}{\kern0pt}}

\end{lemma}

This lemma links the derivative of a bit-coded regular expression with

the regular expression itself before the derivative. 

Brzozowski \cite{Brzozowski1964} introduced the notion of the {\em

derivative} \isa{r{\isacharbackslash}{\kern0pt}c} of a regular expression \isa{r} w.r.t.\

a character~\isa{c}, and showed that it gave a simple solution to the

problem of matching a string \isa{s} with a regular expression \isa{r}: if the derivative of \isa{r} w.r.t.\ (in succession) all the

characters of the string matches the empty string, then \isa{r}

matches \isa{s} (and {\em vice versa}). The derivative has the

property (which may almost be regarded as its specification) that, for

every string \isa{s} and regular expression \isa{r} and character

\isa{c}, one has \isa{cs\ {\isasymin}\ L{\isacharparenleft}{\kern0pt}r{\isacharparenright}{\kern0pt}} if and only if \mbox{\isa{s\ {\isasymin}\ L{\isacharparenleft}{\kern0pt}r{\isacharbackslash}{\kern0pt}c{\isacharparenright}{\kern0pt}}}. 

The beauty of Brzozowski's derivatives is that

they are neatly expressible in any functional language, and easily

definable and reasoned about in theorem provers---the definitions just

consist of inductive datatypes and simple recursive functions. A

mechanised correctness proof of Brzozowski's matcher in for example HOL4

has been mentioned by Owens and Slind~\cite{Owens2008}. Another one in

Isabelle/HOL is part of the work by Krauss and Nipkow \cite{Krauss2011}.

And another one in Coq is given by Coquand and Siles \cite{Coquand2012}.

If a regular expression matches a string, then in general there is more

than one way of how the string is matched. There are two commonly used

disambiguation strategies to generate a unique answer: one is called

GREEDY matching \cite{Frisch2004} and the other is POSIX

matching~\cite{POSIX,Kuklewicz,OkuiSuzuki2010,Sulzmann2014,Vansummeren2006}.

For example consider the string \isa{xy} and the regular expression

\mbox{\isa{{\isacharparenleft}{\kern0pt}x\ {\isacharplus}{\kern0pt}\ y\ {\isacharplus}{\kern0pt}\ xy{\isacharparenright}{\kern0pt}\isactrlsup {\isasymstar}}}. Either the string can be

matched in two `iterations' by the single letter-regular expressions

\isa{x} and \isa{y}, or directly in one iteration by \isa{xy}. The

first case corresponds to GREEDY matching, which first matches with the

left-most symbol and only matches the next symbol in case of a mismatch

(this is greedy in the sense of preferring instant gratification to

delayed repletion). The second case is POSIX matching, which prefers the

longest match.

In the context of lexing, where an input string needs to be split up

into a sequence of tokens, POSIX is the more natural disambiguation

strategy for what programmers consider basic syntactic building blocks

in their programs.  These building blocks are often specified by some

regular expressions, say \isa{r\isactrlbsub key\isactrlesub } and \isa{r\isactrlbsub id\isactrlesub } for recognising keywords and identifiers,

respectively. There are a few underlying (informal) rules behind

tokenising a string in a POSIX \cite{POSIX} fashion:

\begin{itemize} 

\item[$\bullet$] \emph{The Longest Match Rule} (or \emph{``{M}aximal {M}unch {R}ule''}):

The longest initial substring matched by any regular expression is taken as

next token.\smallskip

\item[$\bullet$] \emph{Priority Rule:}

For a particular longest initial substring, the first (leftmost) regular expression

that can match determines the token.\smallskip

\item[$\bullet$] \emph{Star Rule:} A subexpression repeated by ${}^\star$ shall 

not match an empty string unless this is the only match for the repetition.\smallskip

\item[$\bullet$] \emph{Empty String Rule:} An empty string shall be considered to 

be longer than no match at all.

\end{itemize}

\noindent Consider for example a regular expression \isa{r\isactrlbsub key\isactrlesub } for recognising keywords such as \isa{if},

\isa{then} and so on; and \isa{r\isactrlbsub id\isactrlesub }

recognising identifiers (say, a single character followed by

characters or numbers).  Then we can form the regular expression

\isa{{\isacharparenleft}{\kern0pt}r\isactrlbsub key\isactrlesub \ {\isacharplus}{\kern0pt}\ r\isactrlbsub id\isactrlesub {\isacharparenright}{\kern0pt}\isactrlsup {\isasymstar}}

and use POSIX matching to tokenise strings, say \isa{iffoo} and

\isa{if}.  For \isa{iffoo} we obtain by the Longest Match Rule

a single identifier token, not a keyword followed by an

identifier. For \isa{if} we obtain by the Priority Rule a keyword

token, not an identifier token---even if \isa{r\isactrlbsub id\isactrlesub }

matches also. By the Star Rule we know \isa{{\isacharparenleft}{\kern0pt}r\isactrlbsub key\isactrlesub \ {\isacharplus}{\kern0pt}\ r\isactrlbsub id\isactrlesub {\isacharparenright}{\kern0pt}\isactrlsup {\isasymstar}} matches \isa{iffoo},

respectively \isa{if}, in exactly one `iteration' of the star. The

Empty String Rule is for cases where, for example, the regular expression 

\isa{{\isacharparenleft}{\kern0pt}a\isactrlsup {\isasymstar}{\isacharparenright}{\kern0pt}\isactrlsup {\isasymstar}} matches against the

string \isa{bc}. Then the longest initial matched substring is the

empty string, which is matched by both the whole regular expression

and the parenthesised subexpression.

One limitation of Brzozowski's matcher is that it only generates a

YES/NO answer for whether a string is being matched by a regular

expression.  Sulzmann and Lu~\cite{Sulzmann2014} extended this matcher

to allow generation not just of a YES/NO answer but of an actual

matching, called a [lexical] {\em value}. Assuming a regular

expression matches a string, values encode the information of

\emph{how} the string is matched by the regular expression---that is,

which part of the string is matched by which part of the regular

expression. For this consider again the string \isa{xy} and

the regular expression \mbox{\isa{{\isacharparenleft}{\kern0pt}x\ {\isacharplus}{\kern0pt}\ {\isacharparenleft}{\kern0pt}y\ {\isacharplus}{\kern0pt}\ xy{\isacharparenright}{\kern0pt}{\isacharparenright}{\kern0pt}\isactrlsup {\isasymstar}}}

(this time fully parenthesised). We can view this regular expression

as tree and if the string \isa{xy} is matched by two Star

`iterations', then the \isa{x} is matched by the left-most

alternative in this tree and the \isa{y} by the right-left alternative. This

suggests to record this matching as

\begin{center}

\isa{Stars\ {\isacharbrackleft}{\kern0pt}Left\ {\isacharparenleft}{\kern0pt}Char\ x{\isacharparenright}{\kern0pt}{\isacharcomma}{\kern0pt}\ Right\ {\isacharparenleft}{\kern0pt}Left\ {\isacharparenleft}{\kern0pt}Char\ y{\isacharparenright}{\kern0pt}{\isacharparenright}{\kern0pt}{\isacharbrackright}{\kern0pt}}

\end{center}

\noindent where \isa{Stars}, \isa{Left}, \isa{Right} and \isa{Char} are constructors for values. \isa{Stars} records how many

iterations were used; \isa{Left}, respectively \isa{Right}, which

alternative is used. This `tree view' leads naturally to the idea that

regular expressions act as types and values as inhabiting those types

(see, for example, \cite{HosoyaVouillonPierce2005}).  The value for

matching \isa{xy} in a single `iteration', i.e.~the POSIX value,

would look as follows

\begin{center}

\isa{Stars\ {\isacharbrackleft}{\kern0pt}Seq\ {\isacharparenleft}{\kern0pt}Char\ x{\isacharparenright}{\kern0pt}\ {\isacharparenleft}{\kern0pt}Char\ y{\isacharparenright}{\kern0pt}{\isacharbrackright}{\kern0pt}}

\end{center}

\noindent where \isa{Stars} has only a single-element list for the

single iteration and \isa{Seq} indicates that \isa{xy} is matched 

by a sequence regular expression.

%, which we will in what follows 

%write more formally as \isa{x\ {\isasymcdot}\ y}.

Sulzmann and Lu give a simple algorithm to calculate a value that

appears to be the value associated with POSIX matching.  The challenge

then is to specify that value, in an algorithm-independent fashion,

and to show that Sulzmann and Lu's derivative-based algorithm does

indeed calculate a value that is correct according to the

specification.  The answer given by Sulzmann and Lu

\cite{Sulzmann2014} is to define a relation (called an ``order

relation'') on the set of values of \isa{r}, and to show that (once

a string to be matched is chosen) there is a maximum element and that

it is computed by their derivative-based algorithm. This proof idea is

inspired by work of Frisch and Cardelli \cite{Frisch2004} on a GREEDY

regular expression matching algorithm. However, we were not able to

establish transitivity and totality for the ``order relation'' by

Sulzmann and Lu.  There are some inherent problems with their approach

(of which some of the proofs are not published in

\cite{Sulzmann2014}); perhaps more importantly, we give in this paper

a simple inductive (and algorithm-independent) definition of what we

call being a {\em POSIX value} for a regular expression \isa{r} and

a string \isa{s}; we show that the algorithm by Sulzmann and Lu

computes such a value and that such a value is unique. Our proofs are

both done by hand and checked in Isabelle/HOL.  The experience of

doing our proofs has been that this mechanical checking was absolutely

essential: this subject area has hidden snares. This was also noted by

Kuklewicz \cite{Kuklewicz} who found that nearly all POSIX matching

implementations are ``buggy'' \cite[Page 203]{Sulzmann2014} and by

Grathwohl et al \cite[Page 36]{CrashCourse2014} who wrote:

\begin{quote}

\it{}``The POSIX strategy is more complicated than the greedy because of 

the dependence on information about the length of matched strings in the 

various subexpressions.''

\end{quote}

\noindent {\bf Contributions:} We have implemented in Isabelle/HOL the

derivative-based regular expression matching algorithm of

Sulzmann and Lu \cite{Sulzmann2014}. We have proved the correctness of this

algorithm according to our specification of what a POSIX value is (inspired

by work of Vansummeren \cite{Vansummeren2006}). Sulzmann

and Lu sketch in \cite{Sulzmann2014} an informal correctness proof: but to

us it contains unfillable gaps.\footnote{An extended version of

\cite{Sulzmann2014} is available at the website of its first author; this

extended version already includes remarks in the appendix that their

informal proof contains gaps, and possible fixes are not fully worked out.}

Our specification of a POSIX value consists of a simple inductive definition

that given a string and a regular expression uniquely determines this value.

We also show that our definition is equivalent to an ordering 

of values based on positions by Okui and Suzuki \cite{OkuiSuzuki2010}.

%Derivatives as calculated by Brzozowski's method are usually more complex

%regular expressions than the initial one; various optimisations are

%possible. We prove the correctness when simplifications of \isa{\isactrlbold {\isadigit{0}}\ {\isacharplus}{\kern0pt}\ r}, 

%\isa{r\ {\isacharplus}{\kern0pt}\ \isactrlbold {\isadigit{0}}}, \isa{\isactrlbold {\isadigit{1}}\ {\isasymcdot}\ r} and \isa{r\ {\isasymcdot}\ \isactrlbold {\isadigit{1}}} to

%\isa{r} are applied. 

We extend our results to ??? Bitcoded version??%

\end{isamarkuptext}\isamarkuptrue%

%

\isadelimdocument

%

\endisadelimdocument

%

\isatagdocument

%

\isamarkupsection{Preliminaries%

}

\isamarkuptrue%

%

\endisatagdocument

{\isafolddocument}%

%

\isadelimdocument

%

\endisadelimdocument

%

\begin{isamarkuptext}%

\noindent Strings in Isabelle/HOL are lists of characters with

the empty string being represented by the empty list, written \isa{{\isacharbrackleft}{\kern0pt}{\isacharbrackright}{\kern0pt}}, and list-cons being written as \isa{\underline{\hspace{2mm}}\mbox{$\,$}{\isacharcolon}{\kern0pt}{\isacharcolon}{\kern0pt}\mbox{$\,$}\underline{\hspace{2mm}}}. Often

we use the usual bracket notation for lists also for strings; for

example a string consisting of just a single character \isa{c} is

written \isa{{\isacharbrackleft}{\kern0pt}c{\isacharbrackright}{\kern0pt}}. We use the usual definitions for 

\emph{prefixes} and \emph{strict prefixes} of strings.  By using the

type \isa{char} for characters we have a supply of finitely many

characters roughly corresponding to the ASCII character set. Regular

expressions are defined as usual as the elements of the following

inductive datatype:

  \begin{center}

  \isa{r\ {\isacharcolon}{\kern0pt}{\isacharequal}{\kern0pt}}

  \isa{\isactrlbold {\isadigit{0}}} $\mid$

  \isa{\isactrlbold {\isadigit{1}}} $\mid$

  \isa{c} $\mid$

  \isa{r\isactrlsub {\isadigit{1}}\ {\isacharplus}{\kern0pt}\ r\isactrlsub {\isadigit{2}}} $\mid$

  \isa{r\isactrlsub {\isadigit{1}}\ {\isasymcdot}\ r\isactrlsub {\isadigit{2}}} $\mid$

  \isa{r\isactrlsup {\isasymstar}} 

  \end{center}

  \noindent where \isa{\isactrlbold {\isadigit{0}}} stands for the regular expression that does

  not match any string, \isa{\isactrlbold {\isadigit{1}}} for the regular expression that matches

  only the empty string and \isa{c} for matching a character literal. The

  language of a regular expression is also defined as usual by the

  recursive function \isa{L} with the six clauses:

  \begin{center}

  \begin{tabular}{l@ {\hspace{4mm}}rcl}

  \textit{(1)} & \isa{L{\isacharparenleft}{\kern0pt}\isactrlbold {\isadigit{0}}{\isacharparenright}{\kern0pt}} & $\dn$ & \isa{{\isasymemptyset}}\\

  \textit{(2)} & \isa{L{\isacharparenleft}{\kern0pt}\isactrlbold {\isadigit{1}}{\isacharparenright}{\kern0pt}} & $\dn$ & \isa{{\isacharbraceleft}{\kern0pt}{\isacharbrackleft}{\kern0pt}{\isacharbrackright}{\kern0pt}{\isacharbraceright}{\kern0pt}}\\

  \textit{(3)} & \isa{L{\isacharparenleft}{\kern0pt}c{\isacharparenright}{\kern0pt}} & $\dn$ & \isa{{\isacharbraceleft}{\kern0pt}{\isacharbrackleft}{\kern0pt}c{\isacharbrackright}{\kern0pt}{\isacharbraceright}{\kern0pt}}\\

  \textit{(4)} & \isa{L{\isacharparenleft}{\kern0pt}r\isactrlsub {\isadigit{1}}\ {\isasymcdot}\ r\isactrlsub {\isadigit{2}}{\isacharparenright}{\kern0pt}} & $\dn$ & 

        \isa{L{\isacharparenleft}{\kern0pt}r\isactrlsub {\isadigit{1}}{\isacharparenright}{\kern0pt}\ {\isacharat}{\kern0pt}\ L{\isacharparenleft}{\kern0pt}r\isactrlsub {\isadigit{2}}{\isacharparenright}{\kern0pt}}\\

  \textit{(5)} & \isa{L{\isacharparenleft}{\kern0pt}r\isactrlsub {\isadigit{1}}\ {\isacharplus}{\kern0pt}\ r\isactrlsub {\isadigit{2}}{\isacharparenright}{\kern0pt}} & $\dn$ & 

        \isa{L{\isacharparenleft}{\kern0pt}r\isactrlsub {\isadigit{1}}{\isacharparenright}{\kern0pt}\ {\isasymunion}\ L{\isacharparenleft}{\kern0pt}r\isactrlsub {\isadigit{2}}{\isacharparenright}{\kern0pt}}\\

  \textit{(6)} & \isa{L{\isacharparenleft}{\kern0pt}r\isactrlsup {\isasymstar}{\isacharparenright}{\kern0pt}} & $\dn$ & \isa{{\isacharparenleft}{\kern0pt}L{\isacharparenleft}{\kern0pt}r{\isacharparenright}{\kern0pt}{\isacharparenright}{\kern0pt}{\isasymstar}}\\

  \end{tabular}

  \end{center}

  \noindent In clause \textit{(4)} we use the operation \isa{\underline{\hspace{2mm}}\ {\isacharat}{\kern0pt}\ \underline{\hspace{2mm}}} for the concatenation of two languages (it is also list-append for

  strings). We use the star-notation for regular expressions and for

  languages (in the last clause above). The star for languages is defined

  inductively by two clauses: \isa{{\isacharparenleft}{\kern0pt}i{\isacharparenright}{\kern0pt}} the empty string being in

  the star of a language and \isa{{\isacharparenleft}{\kern0pt}ii{\isacharparenright}{\kern0pt}} if \isa{s\isactrlsub {\isadigit{1}}} is in a

  language and \isa{s\isactrlsub {\isadigit{2}}} in the star of this language, then also \isa{s\isactrlsub {\isadigit{1}}\ {\isacharat}{\kern0pt}\ s\isactrlsub {\isadigit{2}}} is in the star of this language. It will also be convenient

  to use the following notion of a \emph{semantic derivative} (or \emph{left

  quotient}) of a language defined as

  %

  \begin{center}

  \isa{Der\ c\ A\ {\isasymequiv}\ {\isacharbraceleft}{\kern0pt}s\ \mbox{\boldmath$\mid$}\ c\mbox{$\,$}{\isacharcolon}{\kern0pt}{\isacharcolon}{\kern0pt}\mbox{$\,$}s\ {\isasymin}\ A{\isacharbraceright}{\kern0pt}}\;.

  \end{center}

  \noindent

  For semantic derivatives we have the following equations (for example

  mechanically proved in \cite{Krauss2011}):

  %

  \begin{equation}\label{SemDer}

  \begin{array}{lcl}

  \isa{Der\ c\ {\isasymemptyset}}  & \dn & \isa{{\isasymemptyset}}\\

  \isa{Der\ c\ {\isacharbraceleft}{\kern0pt}{\isacharbrackleft}{\kern0pt}{\isacharbrackright}{\kern0pt}{\isacharbraceright}{\kern0pt}}  & \dn & \isa{{\isasymemptyset}}\\

  \isa{Der\ c\ {\isacharbraceleft}{\kern0pt}{\isacharbrackleft}{\kern0pt}d{\isacharbrackright}{\kern0pt}{\isacharbraceright}{\kern0pt}}  & \dn & \isa{\textrm{if}\ c\ {\isacharequal}{\kern0pt}\ d\ \textrm{then}\ {\isacharbraceleft}{\kern0pt}{\isacharbrackleft}{\kern0pt}{\isacharbrackright}{\kern0pt}{\isacharbraceright}{\kern0pt}\ \textrm{else}\ {\isasymemptyset}}\\

  \isa{Der\ c\ {\isacharparenleft}{\kern0pt}A\ {\isasymunion}\ B{\isacharparenright}{\kern0pt}}  & \dn & \isa{Der\ c\ A\ {\isasymunion}\ Der\ c\ B}\\

  \isa{Der\ c\ {\isacharparenleft}{\kern0pt}A\ {\isacharat}{\kern0pt}\ B{\isacharparenright}{\kern0pt}}  & \dn & \isa{{\isacharparenleft}{\kern0pt}Der\ c\ A\ {\isacharat}{\kern0pt}\ B{\isacharparenright}{\kern0pt}\ {\isasymunion}\ {\isacharparenleft}{\kern0pt}\textrm{if}\ {\isacharbrackleft}{\kern0pt}{\isacharbrackright}{\kern0pt}\ {\isasymin}\ A\ \textrm{then}\ Der\ c\ B\ \textrm{else}\ {\isasymemptyset}{\isacharparenright}{\kern0pt}}\\

  \isa{Der\ c\ {\isacharparenleft}{\kern0pt}A{\isasymstar}{\isacharparenright}{\kern0pt}}  & \dn & \isa{Der\ c\ A\ {\isacharat}{\kern0pt}\ A{\isasymstar}}

  \end{array}

  \end{equation}

  \noindent \emph{\Brz's derivatives} of regular expressions

  \cite{Brzozowski1964} can be easily defined by two recursive functions:

  the first is from regular expressions to booleans (implementing a test

  when a regular expression can match the empty string), and the second

  takes a regular expression and a character to a (derivative) regular

  expression:

  \begin{center}

  \begin{tabular}{lcl}

  \isa{nullable\ {\isacharparenleft}{\kern0pt}\isactrlbold {\isadigit{0}}{\isacharparenright}{\kern0pt}} & $\dn$ & \isa{False}\\

  \isa{nullable\ {\isacharparenleft}{\kern0pt}\isactrlbold {\isadigit{1}}{\isacharparenright}{\kern0pt}} & $\dn$ & \isa{True}\\

  \isa{nullable\ {\isacharparenleft}{\kern0pt}c{\isacharparenright}{\kern0pt}} & $\dn$ & \isa{False}\\

  \isa{nullable\ {\isacharparenleft}{\kern0pt}r\isactrlsub {\isadigit{1}}\ {\isacharplus}{\kern0pt}\ r\isactrlsub {\isadigit{2}}{\isacharparenright}{\kern0pt}} & $\dn$ & \isa{nullable\ r\isactrlsub {\isadigit{1}}\ {\isasymor}\ nullable\ r\isactrlsub {\isadigit{2}}}\\

  \isa{nullable\ {\isacharparenleft}{\kern0pt}r\isactrlsub {\isadigit{1}}\ {\isasymcdot}\ r\isactrlsub {\isadigit{2}}{\isacharparenright}{\kern0pt}} & $\dn$ & \isa{nullable\ r\isactrlsub {\isadigit{1}}\ {\isasymand}\ nullable\ r\isactrlsub {\isadigit{2}}}\\

  \isa{nullable\ {\isacharparenleft}{\kern0pt}r\isactrlsup {\isasymstar}{\isacharparenright}{\kern0pt}} & $\dn$ & \isa{True}\medskip\\

%  \end{tabular}

%  \end{center}

%  \begin{center}

%  \begin{tabular}{lcl}

  \isa{\isactrlbold {\isadigit{0}}{\isacharbackslash}{\kern0pt}c} & $\dn$ & \isa{\isactrlbold {\isadigit{0}}}\\

  \isa{\isactrlbold {\isadigit{1}}{\isacharbackslash}{\kern0pt}c} & $\dn$ & \isa{\isactrlbold {\isadigit{0}}}\\

  \isa{d{\isacharbackslash}{\kern0pt}c} & $\dn$ & \isa{\textrm{if}\ c\ {\isacharequal}{\kern0pt}\ d\ \textrm{then}\ \isactrlbold {\isadigit{1}}\ \textrm{else}\ \isactrlbold {\isadigit{0}}}\\

  \isa{{\isacharparenleft}{\kern0pt}r\isactrlsub {\isadigit{1}}\ {\isacharplus}{\kern0pt}\ r\isactrlsub {\isadigit{2}}{\isacharparenright}{\kern0pt}{\isacharbackslash}{\kern0pt}c} & $\dn$ & \isa{{\isacharparenleft}{\kern0pt}r\isactrlsub {\isadigit{1}}{\isacharbackslash}{\kern0pt}c{\isacharparenright}{\kern0pt}\ {\isacharplus}{\kern0pt}\ {\isacharparenleft}{\kern0pt}r\isactrlsub {\isadigit{2}}{\isacharbackslash}{\kern0pt}c{\isacharparenright}{\kern0pt}}\\

  \isa{{\isacharparenleft}{\kern0pt}r\isactrlsub {\isadigit{1}}\ {\isasymcdot}\ r\isactrlsub {\isadigit{2}}{\isacharparenright}{\kern0pt}{\isacharbackslash}{\kern0pt}c} & $\dn$ & \isa{\textrm{if}\ nullable\ r\isactrlsub {\isadigit{1}}\ \textrm{then}\ {\isacharparenleft}{\kern0pt}r\isactrlsub {\isadigit{1}}{\isacharbackslash}{\kern0pt}c{\isacharparenright}{\kern0pt}\ {\isasymcdot}\ r\isactrlsub {\isadigit{2}}\ {\isacharplus}{\kern0pt}\ {\isacharparenleft}{\kern0pt}r\isactrlsub {\isadigit{2}}{\isacharbackslash}{\kern0pt}c{\isacharparenright}{\kern0pt}\ \textrm{else}\ {\isacharparenleft}{\kern0pt}r\isactrlsub {\isadigit{1}}{\isacharbackslash}{\kern0pt}c{\isacharparenright}{\kern0pt}\ {\isasymcdot}\ r\isactrlsub {\isadigit{2}}}\\

  \isa{{\isacharparenleft}{\kern0pt}r\isactrlsup {\isasymstar}{\isacharparenright}{\kern0pt}{\isacharbackslash}{\kern0pt}c} & $\dn$ & \isa{{\isacharparenleft}{\kern0pt}r{\isacharbackslash}{\kern0pt}c{\isacharparenright}{\kern0pt}\ {\isasymcdot}\ r\isactrlsup {\isasymstar}}

  \end{tabular}

  \end{center}

  \noindent

  We may extend this definition to give derivatives w.r.t.~strings:

  \begin{center}

  \begin{tabular}{lcl}

  \isa{r{\isacharbackslash}{\kern0pt}{\isacharbrackleft}{\kern0pt}{\isacharbrackright}{\kern0pt}} & $\dn$ & \isa{r}\\

  \isa{r{\isacharbackslash}{\kern0pt}{\isacharparenleft}{\kern0pt}c\mbox{$\,$}{\isacharcolon}{\kern0pt}{\isacharcolon}{\kern0pt}\mbox{$\,$}s{\isacharparenright}{\kern0pt}} & $\dn$ & \isa{{\isacharparenleft}{\kern0pt}r{\isacharbackslash}{\kern0pt}c{\isacharparenright}{\kern0pt}{\isacharbackslash}{\kern0pt}s}\\

  \end{tabular}

  \end{center}

  \noindent Given the equations in \eqref{SemDer}, it is a relatively easy

  exercise in mechanical reasoning to establish that

  \begin{proposition}\label{derprop}\mbox{}\\ 

  \begin{tabular}{ll}

  \textit{(1)} & \isa{nullable\ r} if and only if

  \isa{{\isacharbrackleft}{\kern0pt}{\isacharbrackright}{\kern0pt}\ {\isasymin}\ L{\isacharparenleft}{\kern0pt}r{\isacharparenright}{\kern0pt}}, and \\ 

  \textit{(2)} & \isa{L{\isacharparenleft}{\kern0pt}r{\isacharbackslash}{\kern0pt}c{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ Der\ c\ {\isacharparenleft}{\kern0pt}L{\isacharparenleft}{\kern0pt}r{\isacharparenright}{\kern0pt}{\isacharparenright}{\kern0pt}}.

  \end{tabular}

  \end{proposition}

  \noindent With this in place it is also very routine to prove that the

  regular expression matcher defined as

  %

  \begin{center}

  \isa{match\ r\ s\ {\isasymequiv}\ nullable\ {\isacharparenleft}{\kern0pt}r{\isacharbackslash}{\kern0pt}s{\isacharparenright}{\kern0pt}}

  \end{center}

  \noindent gives a positive answer if and only if \isa{s\ {\isasymin}\ L{\isacharparenleft}{\kern0pt}r{\isacharparenright}{\kern0pt}}.

  Consequently, this regular expression matching algorithm satisfies the

  usual specification for regular expression matching. While the matcher

  above calculates a provably correct YES/NO answer for whether a regular

  expression matches a string or not, the novel idea of Sulzmann and Lu

  \cite{Sulzmann2014} is to append another phase to this algorithm in order

  to calculate a [lexical] value. We will explain the details next.%

\end{isamarkuptext}\isamarkuptrue%

%

\isadelimdocument

%

\endisadelimdocument

%

\isatagdocument

%

\isamarkupsection{POSIX Regular Expression Matching\label{posixsec}%

}

\isamarkuptrue%

%

\endisatagdocument

{\isafolddocument}%

%

\isadelimdocument

%

\endisadelimdocument

%

\begin{isamarkuptext}%

There have been many previous works that use values for encoding 

  \emph{how} a regular expression matches a string.

  The clever idea by Sulzmann and Lu \cite{Sulzmann2014} is to 

  define a function on values that mirrors (but inverts) the

  construction of the derivative on regular expressions. \emph{Values}

  are defined as the inductive datatype

  \begin{center}

  \isa{v\ {\isacharcolon}{\kern0pt}{\isacharequal}{\kern0pt}}

  \isa{Empty} $\mid$

  \isa{Char\ c} $\mid$

  \isa{Left\ v} $\mid$

  \isa{Right\ v} $\mid$

  \isa{Seq\ v\isactrlsub {\isadigit{1}}\ v\isactrlsub {\isadigit{2}}} $\mid$ 

  \isa{Stars\ vs} 

  \end{center}  

  \noindent where we use \isa{vs} to stand for a list of

  values. (This is similar to the approach taken by Frisch and

  Cardelli for GREEDY matching \cite{Frisch2004}, and Sulzmann and Lu

  for POSIX matching \cite{Sulzmann2014}). The string underlying a

  value can be calculated by the \isa{flat} function, written

  \isa{{\isacharbar}{\kern0pt}\underline{\hspace{2mm}}{\isacharbar}{\kern0pt}} and defined as:

  \begin{center}

  \begin{tabular}[t]{lcl}

  \isa{{\isacharbar}{\kern0pt}Empty{\isacharbar}{\kern0pt}} & $\dn$ & \isa{{\isacharbrackleft}{\kern0pt}{\isacharbrackright}{\kern0pt}}\\

  \isa{{\isacharbar}{\kern0pt}Char\ c{\isacharbar}{\kern0pt}} & $\dn$ & \isa{{\isacharbrackleft}{\kern0pt}c{\isacharbrackright}{\kern0pt}}\\

  \isa{{\isacharbar}{\kern0pt}Left\ v{\isacharbar}{\kern0pt}} & $\dn$ & \isa{{\isacharbar}{\kern0pt}v{\isacharbar}{\kern0pt}}\\

  \isa{{\isacharbar}{\kern0pt}Right\ v{\isacharbar}{\kern0pt}} & $\dn$ & \isa{{\isacharbar}{\kern0pt}v{\isacharbar}{\kern0pt}}

  \end{tabular}\hspace{14mm}

  \begin{tabular}[t]{lcl}

  \isa{{\isacharbar}{\kern0pt}Seq\ v\isactrlsub {\isadigit{1}}\ v\isactrlsub {\isadigit{2}}{\isacharbar}{\kern0pt}} & $\dn$ & \isa{{\isacharbar}{\kern0pt}v\isactrlsub {\isadigit{1}}{\isacharbar}{\kern0pt}\ {\isacharat}{\kern0pt}\ {\isacharbar}{\kern0pt}v\isactrlsub {\isadigit{2}}{\isacharbar}{\kern0pt}}\\

  \isa{{\isacharbar}{\kern0pt}Stars\ {\isacharbrackleft}{\kern0pt}{\isacharbrackright}{\kern0pt}{\isacharbar}{\kern0pt}} & $\dn$ & \isa{{\isacharbrackleft}{\kern0pt}{\isacharbrackright}{\kern0pt}}\\

  \isa{{\isacharbar}{\kern0pt}Stars\ {\isacharparenleft}{\kern0pt}v\mbox{$\,$}{\isacharcolon}{\kern0pt}{\isacharcolon}{\kern0pt}\mbox{$\,$}vs{\isacharparenright}{\kern0pt}{\isacharbar}{\kern0pt}} & $\dn$ & \isa{{\isacharbar}{\kern0pt}v{\isacharbar}{\kern0pt}\ {\isacharat}{\kern0pt}\ {\isacharbar}{\kern0pt}Stars\ vs{\isacharbar}{\kern0pt}}\\

  \end{tabular}

  \end{center}

  \noindent We will sometimes refer to the underlying string of a

  value as \emph{flattened value}.  We will also overload our notation and 

  use \isa{{\isacharbar}{\kern0pt}vs{\isacharbar}{\kern0pt}} for flattening a list of values and concatenating

  the resulting strings.

  Sulzmann and Lu define

  inductively an \emph{inhabitation relation} that associates values to

  regular expressions. We define this relation as

  follows:\footnote{Note that the rule for \isa{Stars} differs from

  our earlier paper \cite{AusafDyckhoffUrban2016}. There we used the

  original definition by Sulzmann and Lu which does not require that

  the values \isa{v\ {\isasymin}\ vs} flatten to a non-empty

  string. The reason for introducing the more restricted version of

  lexical values is convenience later on when reasoning about an

  ordering relation for values.}

  \begin{center}

  \begin{tabular}{c@ {\hspace{12mm}}c}\label{prfintros}

  \\[-8mm]

  \isa{\mbox{}\inferrule{\mbox{}}{\mbox{Empty\ {\isacharcolon}{\kern0pt}\ \isactrlbold {\isadigit{1}}}}} & 

  \isa{\mbox{}\inferrule{\mbox{}}{\mbox{Char\ c\ {\isacharcolon}{\kern0pt}\ c}}}\\[4mm]

  \isa{\mbox{}\inferrule{\mbox{v\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\kern0pt}\ r\isactrlsub {\isadigit{1}}}}{\mbox{Left\ v\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\kern0pt}\ r\isactrlsub {\isadigit{1}}\ {\isacharplus}{\kern0pt}\ r\isactrlsub {\isadigit{2}}}}} &

  \isa{\mbox{}\inferrule{\mbox{v\isactrlsub {\isadigit{2}}\ {\isacharcolon}{\kern0pt}\ r\isactrlsub {\isadigit{1}}}}{\mbox{Right\ v\isactrlsub {\isadigit{2}}\ {\isacharcolon}{\kern0pt}\ r\isactrlsub {\isadigit{2}}\ {\isacharplus}{\kern0pt}\ r\isactrlsub {\isadigit{1}}}}}\\[4mm]

  \isa{\mbox{}\inferrule{\mbox{v\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\kern0pt}\ r\isactrlsub {\isadigit{1}}}\\\ \mbox{v\isactrlsub {\isadigit{2}}\ {\isacharcolon}{\kern0pt}\ r\isactrlsub {\isadigit{2}}}}{\mbox{Seq\ v\isactrlsub {\isadigit{1}}\ v\isactrlsub {\isadigit{2}}\ {\isacharcolon}{\kern0pt}\ r\isactrlsub {\isadigit{1}}\ {\isasymcdot}\ r\isactrlsub {\isadigit{2}}}}}  &

  \isa{\mbox{}\inferrule{\mbox{{\isasymforall}v{\isasymin}vs{\isachardot}{\kern0pt}\ v\ {\isacharcolon}{\kern0pt}\ r\ {\isasymand}\ {\isacharbar}{\kern0pt}v{\isacharbar}{\kern0pt}\ {\isasymnoteq}\ {\isacharbrackleft}{\kern0pt}{\isacharbrackright}{\kern0pt}}}{\mbox{Stars\ vs\ {\isacharcolon}{\kern0pt}\ r\isactrlsup {\isasymstar}}}}

  \end{tabular}

  \end{center}

  \noindent where in the clause for \isa{Stars} we use the

  notation \isa{v\ {\isasymin}\ vs} for indicating that \isa{v} is a

  member in the list \isa{vs}.  We require in this rule that every

  value in \isa{vs} flattens to a non-empty string. The idea is that

  \isa{Stars}-values satisfy the informal Star Rule (see Introduction)

  where the $^\star$ does not match the empty string unless this is

  the only match for the repetition.  Note also that no values are

  associated with the regular expression \isa{\isactrlbold {\isadigit{0}}}, and that the

  only value associated with the regular expression \isa{\isactrlbold {\isadigit{1}}} is

  \isa{Empty}.  It is routine to establish how values ``inhabiting''

  a regular expression correspond to the language of a regular

  expression, namely

  \begin{proposition}\label{inhabs}

  \isa{L{\isacharparenleft}{\kern0pt}r{\isacharparenright}{\kern0pt}\ {\isacharequal}{\kern0pt}\ {\isacharbraceleft}{\kern0pt}{\isacharbar}{\kern0pt}v{\isacharbar}{\kern0pt}\ \mbox{\boldmath$\mid$}\ v\ {\isacharcolon}{\kern0pt}\ r{\isacharbraceright}{\kern0pt}}

  \end{proposition}

  \noindent

  Given a regular expression \isa{r} and a string \isa{s}, we define the 

  set of all \emph{Lexical Values} inhabited by \isa{r} with the underlying string 

  being \isa{s}:\footnote{Okui and Suzuki refer to our lexical values 

  as \emph{canonical values} in \cite{OkuiSuzuki2010}. The notion of \emph{non-problematic

  values} by Cardelli and Frisch \cite{Frisch2004} is related, but not identical

  to our lexical values.}

  \begin{center}

  \isa{LV\ r\ s\ {\isasymequiv}\ {\isacharbraceleft}{\kern0pt}v\ \mbox{\boldmath$\mid$}\ v\ {\isacharcolon}{\kern0pt}\ r\ {\isasymand}\ {\isacharbar}{\kern0pt}v{\isacharbar}{\kern0pt}\ {\isacharequal}{\kern0pt}\ s{\isacharbraceright}{\kern0pt}}

  \end{center}

  \noindent The main property of \isa{LV\ r\ s} is that it is alway finite.

  \begin{proposition}

  \isa{finite\ {\isacharparenleft}{\kern0pt}LV\ r\ s{\isacharparenright}{\kern0pt}}

  \end{proposition}

  \noindent This finiteness property does not hold in general if we

  remove the side-condition about \isa{{\isacharbar}{\kern0pt}v{\isacharbar}{\kern0pt}\ {\isasymnoteq}\ {\isacharbrackleft}{\kern0pt}{\isacharbrackright}{\kern0pt}} in the

  \isa{Stars}-rule above. For example using Sulzmann and Lu's