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

abbreviation 

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

  STAR ("_\<^sup>*" [79] 78) and

of a mechanised correctness proof of Brzozowski's derivative-based matcher in HOL4 by

Also Ribeiro and Du Bois give one in Agda \cite{RibeiroAgda2017}.

However, there are two difficulties with derivative-based matchers:

First, Brzozowski's original matcher only generates a yes/no answer

for whether a regular expression matches a string or not.  This is too

little information in the context of lexing where separate tokens must

be identified and also classified (for example as keywords

or identifiers).  Sulzmann and Lu~\cite{Sulzmann2014} overcome this

difficulty by cleverly extending Brzozowski's matching

algorithm. Their extended version generates additional information on

\emph{how} a regular expression matches a string following the POSIX

rules for regular expression matching. They achieve this by adding a

second ``phase'' to Brzozowski's algorithm involving an injection

function.  In our own earlier work we provided the formal

specification of what POSIX matching means and proved in Isabelle/HOL

the correctness

of Sulzmann and Lu's extended algorithm accordingly

\cite{AusafDyckhoffUrban2016}.

The second difficulty is that Brzozowski's derivatives can 

& $\ll$ & \ldots \hspace{15mm}(regular expressions of sizes 98, 169, 283, 468, 767, \ldots)

typical computer (we shall define shortly the precise details of our

regular expressions and the derivative operation).  Clearly, the

notation involving $\ZERO$s and $\ONE$s already suggests

simplification rules that can be applied to regular regular

expressions, for example $\ZERO{}\,r \Rightarrow \ZERO$, $\ONE{}\,r

\Rightarrow r$, $\ZERO{} + r \Rightarrow r$ and $r + r \Rightarrow

r$. While such simple-minded simplifications have been proved in our

earlier work to preserve the correctness of Sulzmann and Lu's

algorithm \cite{AusafDyckhoffUrban2016}, they unfortunately do

\emph{not} help with limiting the growth of the derivatives shown

above: the growth is slowed, but the derivatives can still grow quickly

beyond any finite bound.

Sulzmann and Lu overcome this ``growth problem'' in a second algorithm

\cite{Sulzmann2014} where they introduce bitcoded

regular expressions. In this version, POSIX values are

represented as bitsequences and such sequences are incrementally generated

when derivatives are calculated. The compact representation

of bitsequences and regular expressions allows them to define a more

``aggressive'' simplification method that keeps the size of the

derivatives finite no matter what the length of the string is.

They make some informal claims about the correctness and linear behaviour

of this version, but do not provide any supporting proof arguments, not

even ``pencil-and-paper'' arguments. They write about their bitcoded

\emph{incremental parsing method} (that is the algorithm to be formalised

in this paper):

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

the derivative-based lexing algorithm of Sulzmann and Lu

\cite{Sulzmann2014} where regular expressions are annotated with

bitsequences. We define the crucial simplification function as a

recursive function, instead of a fix-point operation. One objective of

the simplification function is to remove duplicates of regular

expressions.  For this Sulzmann and Lu use in their paper the standard

@{text nub} function from Haskell's list library, but this function

does not achieve the intended objective with bitcoded regular expressions.  The

reason is that in the bitcoded setting, each copy generally has a

different bitcode annotation---so @{text nub} would never ``fire''.

Inspired by Scala's library for lists, we shall instead use a @{text

distinctBy} function that finds duplicates under an erasing function

that deletes bitcodes.

We shall also introduce our own argument and definitions for

establishing the correctness of the bitcoded algorithm when 

simplifications are included.\medskip

\noindent In this paper, we shall first briefly introduce the basic notions

of regular expressions and describe the basic definitions

of POSIX lexing from our earlier work \cite{AusafDyckhoffUrban2016}. This serves

as a reference point for what correctness means in our Isabelle/HOL proofs. We shall then prove

the correctness for the bitcoded algorithm without simplification, and

after that extend the proof to include simplification. 

*}

section {* Background *}

text {*

  In our Isabelle/HOL formalisation strings are lists of characters with

  the empty string being represented by the empty list, written $[]$,

  and list-cons being written as $\_\!::\!\_\,$; string

  concatenation is $\_ \,@\, \_\,$. We often use the usual

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

  consisting of just a single character $c$ is written $[c]$.   

  Our 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 "CH 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 constructors $+$ and $\cdot$ represent alternatives and sequences, respectively.

  The

  \emph{language} of a regular expression, written $L$, is defined as usual

  and we omit giving the definition here (see for example \cite{AusafDyckhoffUrban2016}).

  Central to Brzozowski's regular expression matcher are two functions

  called @{text nullable} and \emph{derivative}. The latter is written

  $r\backslash c$ for the derivative of the regular expression $r$

  w.r.t.~the character $c$. Both functions are defined by recursion over

  regular expressions.  

  \noindent

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

  \begin{center}

  \begin{tabular}{cc}

  \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}

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

  \end{tabular}

  &

  \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}

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

  \end{tabular}

  \end{tabular}

  \end{center}

\noindent

Using @{text nullable} and the derivative operation, we can

define the following simple regular expression matcher:

%

\[

@{text "match s r"} \;\dn\; @{term nullable}(r\backslash s)

\]

\noindent This is essentially Brzozowski's algorithm from 1964. Its

main virtue is that the algorithm can be easily implemented as a

functional program (either in a functional programming language or in

a theorem prover). The correctness proof for @{text match} amounts to

establishing the property

%

\begin{proposition}\label{matchcorr} 

@{text "match s r"} \;\;\text{if and only if}\;\; $s \in L(r)$

\end{proposition}

\noindent

It is a fun exercise to formaly prove this property in a theorem prover.

The novel idea of Sulzmann and Lu is to extend this algorithm for 

lexing, where it is important to find out which part of the string

is matched by which part of the regular expression.

For this Sulzmann and Lu presented two lexing algorithms in their paper

  \cite{Sulzmann2014}. This first algorithm consists of two phases: first a

  matching phase (which is Brzozowski's algorithm) and then a value

  construction phase. The values encode \emph{how} a regular expression

  matches a string. \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. The

  string underlying a value can be calculated by a @{const flat}

  function, written @{term "flat DUMMY"}. It traverses a value and

  collects the characters contained in it. 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"]} \qquad

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

  \end{tabular}

  \end{center}

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

  @{term ZERO}, since it cannot match any string.

  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 inhabited by a regular

  expression (meaning regular expressions can typically match more

  than one string). But even when fixing a string from the language of the

  regular expression, there are generally more than one way of how the

  regular expression can match this string. POSIX lexing is about

  identifying the unique value for a given regular expression and a

  string that satisfies the informal POSIX rules (see

  \cite{POSIX,Kuklewicz,OkuiSuzuki2010,Sulzmann2014,Vansummeren2006}).\footnote{POSIX

	lexing acquired its name from the fact that the corresponding

	rules were described as part of the POSIX specification for

	Unix-like operating systems \cite{POSIX}.} Sometimes these

  informal rules are called \emph{maximal much rule} and \emph{rule priority}.

  One contribution of our earlier paper is to give a convenient

 specification for what a POSIX value is (the inductive rules are shown in

  Figure~\ref{POSIXrules}).

  \begin{center}

  \begin{tabular}{c}

  @{thm[mode=Axiom] Posix.intros(1)}\<open>P\<close>@{term "ONE"} \qquad

  @{thm[mode=Axiom] Posix.intros(2)}\<open>P\<close>@{term "c"}\medskip\\

  @{thm[mode=Rule] Posix.intros(3)[of "s" "r\<^sub>1" "v" "r\<^sub>2"]}\<open>P+L\<close>\qquad

  @{thm[mode=Rule] Posix.intros(4)[of "s" "r\<^sub>2" "v" "r\<^sub>1"]}\<open>P+R\<close>\medskip\\

  $\mprset{flushleft}

   \inferrule

   {@{thm (prem 1) Posix.intros(5)[of "s\<^sub>1" "r\<^sub>1" "v\<^sub>1" "s\<^sub>2" "r\<^sub>2" "v\<^sub>2"]} \qquad

    @{thm (prem 2) Posix.intros(5)[of "s\<^sub>1" "r\<^sub>1" "v\<^sub>1" "s\<^sub>2" "r\<^sub>2" "v\<^sub>2"]} \\\\

    @{thm (prem 3) Posix.intros(5)[of "s\<^sub>1" "r\<^sub>1" "v\<^sub>1" "s\<^sub>2" "r\<^sub>2" "v\<^sub>2"]}}

   {@{thm (concl) Posix.intros(5)[of "s\<^sub>1" "r\<^sub>1" "v\<^sub>1" "s\<^sub>2" "r\<^sub>2" "v\<^sub>2"]}}$\<open>PS\<close>\medskip\smallskip\\

  @{thm[mode=Axiom] Posix.intros(7)}\<open>P[]\<close>\qquad

  $\mprset{flushleft}

   \inferrule

   {@{thm (prem 1) Posix.intros(6)[of "s\<^sub>1" "r" "v" "s\<^sub>2" "vs"]} \qquad

    @{thm (prem 2) Posix.intros(6)[of "s\<^sub>1" "r" "v" "s\<^sub>2" "vs"]} \qquad

    @{thm (prem 3) Posix.intros(6)[of "s\<^sub>1" "r" "v" "s\<^sub>2" "vs"]} \\\\

    @{thm (prem 4) Posix.intros(6)[of "s\<^sub>1" "r" "v" "s\<^sub>2" "vs"]}}

   {@{thm (concl) Posix.intros(6)[of "s\<^sub>1" "r" "v" "s\<^sub>2" "vs"]}}$\<open>P\<star>\<close>\\[-4mm]

  \end{tabular}

  \end{center}

  \caption{The inductive definition of POSIX values taken from our earlier paper \cite{AusafDyckhoffUrban2016}. The ternary relation, written $(s, r) \rightarrow v$, formalises the notion

  of given a string $s$ and a regular

  expression $r$ what is the unique value $v$ that satisfies the informal POSIX constraints for

  regular expression matching.}\label{POSIXrules}

  \end{figure}

  The clever idea by Sulzmann and Lu \cite{Sulzmann2014} in their first algorithm is to define

  an injection function on values that mirrors (but inverts) the

  construction of the derivative on regular expressions. Essentially it

  injects back a character into a value.

  For this they define two functions called @{text mkeps} and @{text inj}:

  \begin{center}

  \begin{tabular}{l}

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

  \begin{tabular}{lcl}

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

  @{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"]}\\

  @{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"]}\\

  @{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"]}\\

  @{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"]}\\

  @{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"]}\\

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

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

  \end{tabular}

  \end{tabular}

  \end{center}

  \noindent

  The function @{text mkeps} is called when the last derivative is nullable, that is

  the string to be matched is in the language of the regular expression. It generates

  a value for how the last derivative can match the empty string. The injection function

  then calculates the corresponding value for each intermediate derivative until

  a value for the original regular expression is generated.

  Graphically the 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]"}. The lexing algorithm by Sulzmann and Lu can be defined as:

  \begin{figure}[t]

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

the values. The value @{term "v\<^sub>1"} is the result of the algorithm representing

the POSIX value for this string and

regular expression.

  \begin{tabular}{lcl}

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

  @{thm (lhs) lexer.simps(2)} & $\dn$ & @{text "case"} @{term "lexer (der c r) s"} @{text of}\\

                     & & \phantom{$|$} @{term "None"}  @{text "\<Rightarrow>"} @{term None}\\

                     & & $|$ @{term "Some v"} @{text "\<Rightarrow>"} @{term "Some (injval r c v)"}                          

We have shown in our earlier paper \cite{AusafDyckhoffUrban2016} that the algorithm by Sulzmann and Lu

is correct. The cenral property we established relates the derivative operation to the injection function.