(*<*)

theory Paper

imports 

   "../Lexer"

   "../Simplifying" 

   "../Sulzmann" 

   "~~/src/HOL/Library/LaTeXsugar"

begin

declare [[show_question_marks = false]]

abbreviation 

 "der_syn r c \<equiv> der c r"

abbreviation 

 "ders_syn r s \<equiv> ders s r"

notation (latex output)

  If  ("(\<^raw:\textrm{>if\<^raw:}> (_)/ \<^raw:\textrm{>then\<^raw:}> (_)/ \<^raw:\textrm{>else\<^raw:}> (_))" 10) and

  Cons ("_\<^raw:\mbox{$\,$}>::\<^raw:\mbox{$\,$}>_" [75,73] 73) and  

  ZERO ("\<^bold>0" 78) and 

  ONE ("\<^bold>1" 78) and 

  CHAR ("_" [1000] 80) and

  ALT ("_ + _" [77,77] 78) and

  SEQ ("_ \<cdot> _" [77,77] 78) and

  STAR ("_\<^sup>\<star>" [1000] 78) and

  val.Void ("'(')" 1000) and

  val.Char ("Char _" [1000] 78) and

  val.Left ("Left _" [79] 78) and

  val.Right ("Right _" [1000] 78) and

  val.Seq ("Seq _ _" [79,79] 78) and

  val.Stars ("Stars _" [79] 78) and

  L ("L'(_')" [10] 78) and

  der_syn ("_\\_" [79, 1000] 76) and  

  ders_syn ("_\\_" [79, 1000] 76) and

  flat ("|_|" [75] 74) and

  Sequ ("_ @ _" [78,77] 63) and

  injval ("inj _ _ _" [79,77,79] 76) and 

  mkeps ("mkeps _" [79] 76) and 

  length ("len _" [73] 73) and

  Prf ("_ : _" [75,75] 75) and  

  Posix ("'(_, _') \<rightarrow> _" [63,75,75] 75) and

  lexer ("lexer _ _" [78,78] 77) and 

  F_RIGHT ("F\<^bsub>Right\<^esub> _") and

  F_LEFT ("F\<^bsub>Left\<^esub> _") and  

  F_ALT ("F\<^bsub>Alt\<^esub> _ _") and

  F_SEQ1 ("F\<^bsub>Seq1\<^esub> _ _") and

  F_SEQ2 ("F\<^bsub>Seq2\<^esub> _ _") and

  F_SEQ ("F\<^bsub>Seq\<^esub> _ _") and

  simp_SEQ ("simp\<^bsub>Seq\<^esub> _ _" [1000, 1000] 1) and

  simp_ALT ("simp\<^bsub>Alt\<^esub> _ _" [1000, 1000] 1) and

  slexer ("lexer\<^sup>+" 1000) and

  ValOrd ("_ >\<^bsub>_\<^esub> _" [77,77,77] 77) and

  ValOrdEq ("_ \<ge>\<^bsub>_\<^esub> _" [77,77,77] 77)

definition 

  "match r s \<equiv> nullable (ders s r)"

(*

comments not implemented

p9. The condtion "not exists s3 s4..." appears often enough (in particular in

the proof of Lemma 3) to warrant a definition.

*)

(*>*)

section {* Introduction *}

text {*

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

derivative} @{term "der c r"} of a regular expression @{text r} w.r.t.\ a

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

problem of matching a string @{term s} with a regular expression @{term r}:

if the derivative of @{term r} w.r.t.\ (in succession) all the characters of

the string matches the empty string, then @{term r} matches @{term s} (and

{\em vice versa}). The derivative has the property (which may almost be

regarded as its specification) that, for every string @{term s} and regular

expression @{term r} and character @{term c}, one has @{term "cs \<in> L(r)"} if

and only if \mbox{@{term "s \<in> L(der c r)"}}. 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{Kuklewicz,Sulzmann2014,Vansummeren2006}. For example consider

the string @{term xy} and the regular expression \mbox{@{term "STAR (ALT

(ALT x y) xy)"}}. Either the string can be matched in two `iterations' by

the single letter-regular expressions @{term x} and @{term y}, or directly

in one iteration by @{term 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

@{text "r\<^bsub>key\<^esub>"} and @{text "r\<^bsub>id\<^esub>"} for recognising keywords and

identifiers, respectively. There are two underlying (informal) rules behind

tokenising a string in a POSIX fashion according to a collection of regular

expressions:

\begin{itemize} 

\item[$\bullet$] \emph{The Longest Match Rule} (or \emph{``maximal munch rule''}):

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 regular expression

that can match determines the token.

\end{itemize}

\noindent Consider for example a regular expression @{text "r\<^bsub>key\<^esub>"} for recognising keywords

such as @{text "if"}, @{text "then"} and so on; and @{text "r\<^bsub>id\<^esub>"}

recognising identifiers (say, a single character followed by

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

@{text "(r\<^bsub>key\<^esub> + r\<^bsub>id\<^esub>)\<^sup>\<star>"} and use POSIX matching to tokenise strings,

say @{text "iffoo"} and @{text "if"}.  For @{text "iffoo"} we obtain

by the Longest Match Rule a single identifier token, not a keyword

followed by an identifier. For @{text "if"} we obtain by the Priority

Rule a keyword token, not an identifier token---even if @{text "r\<^bsub>id\<^esub>"}

matches also.

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}. They 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 @{term

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. In Section

\ref{argu} we identify some inherent problems with their approach (of

which some of the proofs are not published in \cite{Sulzmann2014});

perhaps more importantly, we give a simple inductive (and

algorithm-independent) definition of what we call being a {\em POSIX

value} for a regular expression @{term r} and a string @{term s}; we

show that the algorithm 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}

%\footnote{The relation @{text "\<ge>\<^bsub>r\<^esub>"} defined by Sulzmann and Lu \cite{Sulzmann2014} 

%is a relation on the

%values for the regular expression @{term r}; but it only holds between

%@{term "v\<^sub>1"} and @{term "v\<^sub>2"} in cases where @{term "v\<^sub>1"} and @{term "v\<^sub>2"} have

%the same flattening (underlying string). So a counterexample to totality is

%given by taking two values @{term "v\<^sub>1"} and @{term "v\<^sub>2"} for @{term r} that

%have different flattenings (see Section~\ref{posixsec}). A different

%relation @{text "\<ge>\<^bsub>r,s\<^esub>"} on the set of values for @{term r}

%with flattening @{term s} is definable by the same approach, and is indeed

%total; but that is not what Proposition 1 of \cite{Sulzmann2014} does.}

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

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 @{term "ALT ZERO

r"}, @{term "ALT r ZERO"}, @{term "SEQ ONE r"} and @{term "SEQ r ONE"} to

@{term r} are applied.

*}

section {* Preliminaries *}

text {* \noindent Strings in Isabelle/HOL are lists of characters with the

empty string being represented by the empty list, written @{term "[]"}, and

list-cons being written as @{term "DUMMY # DUMMY"}. Often we use the usual

bracket notation for lists also for strings; for example a string consisting

of just a single character @{term c} is written @{term "[c]"}. By using the

type @{type 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}

  @{text "r :="}

  @{const "ZERO"} $\mid$

  @{const "ONE"} $\mid$

  @{term "CHAR c"} $\mid$

  @{term "ALT r\<^sub>1 r\<^sub>2"} $\mid$

  @{term "SEQ r\<^sub>1 r\<^sub>2"} $\mid$

  @{term "STAR r"} 

  \end{center}

  \noindent where @{const ZERO} stands for the regular expression that does

  not match any string, @{const ONE} for the regular expression that matches

  only the empty string and @{term c} for matching a character literal. The

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

  recursive function @{term L} with the six clauses:

  \begin{center}

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

  (1) & @{thm (lhs) L.simps(1)} & $\dn$ & @{thm (rhs) L.simps(1)}\\

  (2) & @{thm (lhs) L.simps(2)} & $\dn$ & @{thm (rhs) L.simps(2)}\\

  (3) & @{thm (lhs) L.simps(3)} & $\dn$ & @{thm (rhs) L.simps(3)}\\

  \end{tabular}

  \hspace{14mm}

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

  (4) & @{thm (lhs) L.simps(4)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) L.simps(4)[of "r\<^sub>1" "r\<^sub>2"]}\\

  (5) & @{thm (lhs) L.simps(5)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) L.simps(5)[of "r\<^sub>1" "r\<^sub>2"]}\\

  (6) & @{thm (lhs) L.simps(6)} & $\dn$ & @{thm (rhs) L.simps(6)}\\

  \end{tabular}

  \end{center}

  \noindent In clause (4) we use the operation @{term "DUMMY ;;

  DUMMY"} 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: @{text "(i)"} the empty string being in

  the star of a language and @{text "(ii)"} if @{term "s\<^sub>1"} is in a

  language and @{term "s\<^sub>2"} in the star of this language, then also @{term

  "s\<^sub>1 @ s\<^sub>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}

  @{thm Der_def}\;.

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

  @{thm (lhs) Der_null}  & \dn & @{thm (rhs) Der_null}\\

  @{thm (lhs) Der_empty}  & \dn & @{thm (rhs) Der_empty}\\

  @{thm (lhs) Der_char}  & \dn & @{thm (rhs) Der_char}\\

  @{thm (lhs) Der_union}  & \dn & @{thm (rhs) Der_union}\\

  @{thm (lhs) Der_Sequ}  & \dn & @{thm (rhs) Der_Sequ}\\

  @{thm (lhs) Der_star}  & \dn & @{thm (rhs) Der_star}

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

  @{thm (lhs) nullable.simps(1)} & $\dn$ & @{thm (rhs) nullable.simps(1)}\\

  @{thm (lhs) nullable.simps(2)} & $\dn$ & @{thm (rhs) nullable.simps(2)}\\

  @{thm (lhs) nullable.simps(3)} & $\dn$ & @{thm (rhs) nullable.simps(3)}\\

  @{thm (lhs) nullable.simps(4)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) nullable.simps(4)[of "r\<^sub>1" "r\<^sub>2"]}\\

  @{thm (lhs) nullable.simps(5)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) nullable.simps(5)[of "r\<^sub>1" "r\<^sub>2"]}\\

  @{thm (lhs) nullable.simps(6)} & $\dn$ & @{thm (rhs) nullable.simps(6)}\medskip\\

  %\end{tabular}

  %\end{center}

  %\begin{center}

  %\begin{tabular}{lcl}

  @{thm (lhs) der.simps(1)} & $\dn$ & @{thm (rhs) der.simps(1)}\\

  @{thm (lhs) der.simps(2)} & $\dn$ & @{thm (rhs) der.simps(2)}\\

  @{thm (lhs) der.simps(3)} & $\dn$ & @{thm (rhs) der.simps(3)}\\

  @{thm (lhs) der.simps(4)[of c "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) der.simps(4)[of c "r\<^sub>1" "r\<^sub>2"]}\\

  @{thm (lhs) der.simps(5)[of c "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) der.simps(5)[of c "r\<^sub>1" "r\<^sub>2"]}\\

  @{thm (lhs) der.simps(6)} & $\dn$ & @{thm (rhs) der.simps(6)}

  \end{tabular}

  \end{center}

  \noindent

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

  \begin{center}

  \begin{tabular}{lcl}

  @{thm (lhs) ders.simps(1)} & $\dn$ & @{thm (rhs) ders.simps(1)}\\

  @{thm (lhs) ders.simps(2)} & $\dn$ & @{thm (rhs) ders.simps(2)}\\

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

  @{text "(1)"} & @{thm (lhs) nullable_correctness} if and only if

  @{thm (rhs) nullable_correctness}, and \\ 

  @{text "(2)"} & @{thm[mode=IfThen] der_correctness}.

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

  @{thm match_def}

  \end{center}

  \noindent gives a positive answer if and only if @{term "s \<in> L r"}.

  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.

*}

section {* POSIX Regular Expression Matching\label{posixsec} *}

text {* 

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

  values for encoding \emph{how} a regular expression matches a string

  and then 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}

  @{text "v :="}

  @{const "Void"} $\mid$

  @{term "val.Char c"} $\mid$

  @{term "Left v"} $\mid$

  @{term "Right v"} $\mid$

  @{term "Seq v\<^sub>1 v\<^sub>2"} $\mid$ 

  @{term "Stars vs"} 

  \end{center}  

  \noindent where we use @{term 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 @{const flat} function, written

  @{term "flat DUMMY"} and defined as:

  \begin{center}

  \begin{tabular}[t]{lcl}

  @{thm (lhs) flat.simps(1)} & $\dn$ & @{thm (rhs) flat.simps(1)}\\

  @{thm (lhs) flat.simps(2)} & $\dn$ & @{thm (rhs) flat.simps(2)}\\

  @{thm (lhs) flat.simps(3)} & $\dn$ & @{thm (rhs) flat.simps(3)}\\

  @{thm (lhs) flat.simps(4)} & $\dn$ & @{thm (rhs) flat.simps(4)}

  \end{tabular}\hspace{14mm}

  \begin{tabular}[t]{lcl}

  @{thm (lhs) flat.simps(5)[of "v\<^sub>1" "v\<^sub>2"]} & $\dn$ & @{thm (rhs) flat.simps(5)[of "v\<^sub>1" "v\<^sub>2"]}\\

  @{thm (lhs) flat.simps(6)} & $\dn$ & @{thm (rhs) flat.simps(6)}\\

  @{thm (lhs) flat.simps(7)} & $\dn$ & @{thm (rhs) flat.simps(7)}\\

  \end{tabular}

  \end{center}

  \noindent Sulzmann and Lu also define inductively an inhabitation relation

  that associates values to regular expressions:

  \begin{center}

  \begin{tabular}{c}

  \\[-8mm]

  @{thm[mode=Axiom] Prf.intros(4)} \qquad

  @{thm[mode=Axiom] Prf.intros(5)[of "c"]}\\[4mm]

  @{thm[mode=Rule] Prf.intros(2)[of "v\<^sub>1" "r\<^sub>1" "r\<^sub>2"]} \qquad 

  @{thm[mode=Rule] Prf.intros(3)[of "v\<^sub>2" "r\<^sub>1" "r\<^sub>2"]}\\[4mm]

  @{thm[mode=Rule] Prf.intros(1)[of "v\<^sub>1" "r\<^sub>1" "v\<^sub>2" "r\<^sub>2"]}\\[4mm]

  @{thm[mode=Axiom] Prf.intros(6)[of "r"]} \qquad  

  @{thm[mode=Rule] Prf.intros(7)[of "v" "r" "vs"]}

  \end{tabular}

  \end{center}

  \noindent Note that no values are associated with the regular expression

  @{term ZERO}, and that the only value associated with the regular

  expression @{term ONE} is @{term Void}, pronounced (if one must) as @{text

  "Void"}. It is routine to establish how values ``inhabiting'' a regular

  expression correspond to the language of a regular expression, namely

  \begin{proposition}

  @{thm L_flat_Prf}

  \end{proposition}

  In general there is more than one value associated with a regular

  expression. In case of POSIX matching the problem is to calculate the

  unique value that satisfies the (informal) POSIX rules from the

  Introduction. Graphically the POSIX value calculation algorithm by

  Sulzmann and Lu can be illustrated by the picture in Figure~\ref{Sulz}

  where the path from the left to the right involving @{term derivatives}/@{const

  nullable} is the first phase of the algorithm (calculating successive

  \Brz's derivatives) and @{const mkeps}/@{text inj}, the path from right to

  left, the second phase. This picture shows the steps required when a

  regular expression, say @{text "r\<^sub>1"}, matches the string @{term

  "[a,b,c]"}. We first build the three derivatives (according to @{term a},

  @{term b} and @{term c}). We then use @{const nullable} to find out

  whether the resulting derivative regular expression @{term "r\<^sub>4"}

  can match the empty string. If yes, we call the function @{const mkeps}

  that produces a value @{term "v\<^sub>4"} for how @{term "r\<^sub>4"} can

  match the empty string (taking into account the POSIX constraints in case

  there are several ways). This function is defined by the clauses:

\begin{figure}[t]

\begin{center}

\begin{tikzpicture}[scale=2,node distance=1.3cm,

                    every node/.style={minimum size=6mm}]

\node (r1)  {@{term "r\<^sub>1"}};

\node (r2) [right=of r1]{@{term "r\<^sub>2"}};

\draw[->,line width=1mm](r1)--(r2) node[above,midway] {@{term "der a DUMMY"}};

\node (r3) [right=of r2]{@{term "r\<^sub>3"}};

\draw[->,line width=1mm](r2)--(r3) node[above,midway] {@{term "der b DUMMY"}};

\node (r4) [right=of r3]{@{term "r\<^sub>4"}};

\draw[->,line width=1mm](r3)--(r4) node[above,midway] {@{term "der c DUMMY"}};

\draw (r4) node[anchor=west] {\;\raisebox{3mm}{@{term nullable}}};

\node (v4) [below=of r4]{@{term "v\<^sub>4"}};

\draw[->,line width=1mm](r4) -- (v4);

\node (v3) [left=of v4] {@{term "v\<^sub>3"}};

\draw[->,line width=1mm](v4)--(v3) node[below,midway] {@{text "inj r\<^sub>3 c"}};

\node (v2) [left=of v3]{@{term "v\<^sub>2"}};

\draw[->,line width=1mm](v3)--(v2) node[below,midway] {@{text "inj r\<^sub>2 b"}};

\node (v1) [left=of v2] {@{term "v\<^sub>1"}};

\draw[->,line width=1mm](v2)--(v1) node[below,midway] {@{text "inj r\<^sub>1 a"}};

\draw (r4) node[anchor=north west] {\;\raisebox{-8mm}{@{term "mkeps"}}};

\end{tikzpicture}

\end{center}

\mbox{}\\[-13mm]

\caption{The two phases of the algorithm by Sulzmann \& Lu \cite{Sulzmann2014},

matching the string @{term "[a,b,c]"}. The first phase (the arrows from 

left to right) is \Brz's matcher building successive derivatives. If the 

last regular expression is @{term nullable}, then the functions of the 

second phase are called (the top-down and right-to-left arrows): first 

@{term mkeps} calculates a value @{term "v\<^sub>4"} witnessing

how the empty string has been recognised by @{term "r\<^sub>4"}. After

that the function @{term inj} ``injects back'' the characters of the string into

the values.

\label{Sulz}}

\end{figure} 

  \begin{center}

  \begin{tabular}{lcl}

  @{thm (lhs) mkeps.simps(1)} & $\dn$ & @{thm (rhs) mkeps.simps(1)}\\

  @{thm (lhs) mkeps.simps(2)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) mkeps.simps(2)[of "r\<^sub>1" "r\<^sub>2"]}\\

  @{thm (lhs) mkeps.simps(3)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) mkeps.simps(3)[of "r\<^sub>1" "r\<^sub>2"]}\\

  @{thm (lhs) mkeps.simps(4)} & $\dn$ & @{thm (rhs) mkeps.simps(4)}\\

  \end{tabular}

  \end{center}

  \noindent Note that this function needs only to be partially defined,

  namely only for regular expressions that are nullable. In case @{const

  nullable} fails, the string @{term "[a,b,c]"} cannot be matched by @{term

  "r\<^sub>1"} and the null value @{term "None"} is returned. Note also how this function

  makes some subtle choices leading to a POSIX value: for example if an

  alternative regular expression, say @{term "ALT r\<^sub>1 r\<^sub>2"}, can

  match the empty string and furthermore @{term "r\<^sub>1"} can match the

  empty string, then we return a @{text Left}-value. The @{text

  Right}-value will only be returned if @{term "r\<^sub>1"} cannot match the empty

  string.

  The most interesting idea from Sulzmann and Lu \cite{Sulzmann2014} is

  the construction of a value for how @{term "r\<^sub>1"} can match the

  string @{term "[a,b,c]"} from the value how the last derivative, @{term

  "r\<^sub>4"} in Fig.~\ref{Sulz}, can match the empty string. Sulzmann and

  Lu achieve this by stepwise ``injecting back'' the characters into the

  values thus inverting the operation of building derivatives, but on the level

  of values. The corresponding function, called @{term inj}, takes three

  arguments, a regular expression, a character and a value. For example in

  the first (or right-most) @{term inj}-step in Fig.~\ref{Sulz} the regular

  expression @{term "r\<^sub>3"}, the character @{term c} from the last

  derivative step and @{term "v\<^sub>4"}, which is the value corresponding

  to the derivative regular expression @{term "r\<^sub>4"}. The result is

  the new value @{term "v\<^sub>3"}. The final result of the algorithm is

  the value @{term "v\<^sub>1"}. The @{term inj} function is defined by recursion on regular

  expressions and by analysing the shape of values (corresponding to 

  the derivative regular expressions).

  %

  \begin{center}

  \begin{tabular}{l@ {\hspace{5mm}}lcl}

  (1) & @{thm (lhs) injval.simps(1)} & $\dn$ & @{thm (rhs) injval.simps(1)}\\

  (2) & @{thm (lhs) injval.simps(2)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1"]} & $\dn$ & 

      @{thm (rhs) injval.simps(2)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1"]}\\

  (3) & @{thm (lhs) injval.simps(3)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]} & $\dn$ & 

      @{thm (rhs) injval.simps(3)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]}\\

  (4) & @{thm (lhs) injval.simps(4)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]} & $\dn$ 

      & @{thm (rhs) injval.simps(4)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]}\\

  (5) & @{thm (lhs) injval.simps(5)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]} & $\dn$ 

      & @{thm (rhs) injval.simps(5)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]}\\

  (6) & @{thm (lhs) injval.simps(6)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]} & $\dn$ 

      & @{thm (rhs) injval.simps(6)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]}\\

  (7) & @{thm (lhs) injval.simps(7)[of "r" "c" "v" "vs"]} & $\dn$ 

      & @{thm (rhs) injval.simps(7)[of "r" "c" "v" "vs"]}\\

  \end{tabular}