1 (*<*)

     2 theory Paper

     3   imports

     4    "Posix.FBound" 

     5    "HOL-Library.LaTeXsugar"

     6 begin

     7 

     8 declare [[show_question_marks = false]]

     9 

    10 notation (latex output)

    11   If  ("(\<^latex>\<open>\\textrm{\<close>if\<^latex>\<open>}\<close> (_)/ \<^latex>\<open>\\textrm{\<close>then\<^latex>\<open>}\<close> (_)/ \<^latex>\<open>\\textrm{\<close>else\<^latex>\<open>}\<close> (_))" 10) and

    12   Cons ("_\<^latex>\<open>\\mbox{$\\,$}\<close>::\<^latex>\<open>\\mbox{$\\,$}\<close>_" [75,73] 73) 

    13 

    14 

    15 abbreviation 

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

    17 abbreviation 

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

    19 abbreviation 

    20   "bder_syn r c \<equiv> bder c r"  

    21 

    22 notation (latex output)

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

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

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

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

    27   bders_simp ("_\\\<^sub>b\<^sub>s\<^sub>i\<^sub>m\<^sub>p _" [79, 1000] 76) and

    28 

    29   ZERO ("\<^bold>0" 81) and 

    30   ONE ("\<^bold>1" 81) and 

    31   CH ("_" [1000] 80) and

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

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

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

    35 

    36   val.Void ("Empty" 78) and

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

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

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

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

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

    42 

    43   Prf ("\<turnstile> _ : _" [75,75] 75) and  

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

    45 

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

    47   flats ("|_|" [72] 74) and

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

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

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

    51   set ("_" [73] 73) and

    52 

    53   AZERO ("ZERO" 81) and 

    54   AONE ("ONE _" [79] 78) and 

    55   ACHAR ("CHAR _ _" [79, 79] 80) and

    56   AALTs ("ALTs _ _" [77,77] 78) and

    57   ASEQ ("SEQ _ _ _" [79, 79,79] 78) and

    58   ASTAR ("STAR _ _" [79, 79] 78) and

    59 

    60   code ("code _" [79] 74) and

    61   intern ("_\<^latex>\<open>\\mbox{$^\\uparrow$}\<close>" [900] 80) and

    62   erase ("_\<^latex>\<open>\\mbox{$^\\downarrow$}\<close>" [1000] 74) and

    63   bnullable ("bnullable _" [1000] 80) and

    64   bsimp_AALTs ("bsimpALT _ _" [10,1000] 80) and

    65   bsimp_ASEQ ("bsimpSEQ _ _ _" [10,1000,1000] 80) and

    66   bmkeps ("bmkeps _" [1000] 80) and

    67 

    68   eq1 ("_ \<approx> _" [77,77] 76) and 

    69 

    70   srewrite ("_\<^latex>\<open>\\mbox{$\\,\\stackrel{s}{\\leadsto}$}\<close> _" [71, 71] 80) and

    71   rrewrites ("_ \<^latex>\<open>\\mbox{$\\,\\leadsto^*$}\<close> _" [71, 71] 80) and

    72   srewrites ("_ \<^latex>\<open>\\mbox{$\\,\\stackrel{s}{\\leadsto}^*$}\<close> _" [71, 71] 80) and

    73   blexer_simp ("blexer\<^sup>+" 1000) 

    74 

    75 

    76 lemma better_retrieve:

    77    shows "rs \<noteq> Nil ==> retrieve (AALTs bs (r#rs)) (Left v) = bs @ retrieve r v"

    78    and   "rs \<noteq> Nil ==> retrieve (AALTs bs (r#rs)) (Right v) = bs @ retrieve (AALTs [] rs) v"

    79   apply (metis list.exhaust retrieve.simps(4))

    80   by (metis list.exhaust retrieve.simps(5))

    81 

    82 

    83 

    84 

    85 (*>*)

    86 

    87 section {* Introduction *}

    88 

    89 text {*

    90 

    91 In the last fifteen or so years, Brzozowski's derivatives of regular

    92 expressions have sparked quite a bit of interest in the functional

    93 programming and theorem prover communities.  The beauty of

    94 Brzozowski's derivatives \cite{Brzozowski1964} is that they are neatly

    95 expressible in any functional language, and easily definable and

    96 reasoned about in theorem provers---the definitions just consist of

    97 inductive datatypes and simple recursive functions.  Derivatives of a

    98 regular expression, written @{term "der c r"}, give a simple solution

    99 to the problem of matching a string @{term s} with a regular

   100 expression @{term r}: if the derivative of @{term r} w.r.t.\ (in

   101 succession) all the characters of the string matches the empty string,

   102 then @{term r} matches @{term s} (and {\em vice versa}).  We are aware

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

   104 Owens and Slind~\cite{Owens2008}. Another one in Isabelle/HOL is part

   105 of the work by Krauss and Nipkow~\cite{Krauss2011}.  And another one

   106 in Coq is given by Coquand and Siles \cite{Coquand2012}.

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

   108 

   109 

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

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

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

   113 little information in the context of lexing where separate tokens must

   114 be identified and also classified (for example as keywords

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

   116 difficulty by cleverly extending Brzozowski's matching

   117 algorithm. Their extended version generates additional information on

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

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

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

   121 function.  In our own earlier work we provided the formal

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

   123 the correctness

   124 of Sulzmann and Lu's extended algorithm accordingly

   125 \cite{AusafDyckhoffUrban2016}.

   126 

   127 The second difficulty is that Brzozowski's derivatives can 

   128 grow to arbitrarily big sizes. For example if we start with the

   129 regular expression \mbox{@{text "(a + aa)\<^sup>*"}} and take

   130 successive derivatives according to the character $a$, we end up with

   131 a sequence of ever-growing derivatives like 

   132 

   133 \def\ll{\stackrel{\_\backslash{} a}{\longrightarrow}}

   134 \begin{center}

   135 \begin{tabular}{rll}

   136 $(a + aa)^*$ & $\ll$ & $(\ONE + \ONE{}a) \cdot (a + aa)^*$\\

   137 & $\ll$ & $(\ZERO + \ZERO{}a + \ONE) \cdot (a + aa)^* \;+\; (\ONE + \ONE{}a) \cdot (a + aa)^*$\\

   138 & $\ll$ & $(\ZERO + \ZERO{}a + \ZERO) \cdot (a + aa)^* + (\ONE + \ONE{}a) \cdot (a + aa)^* \;+\; $\\

   139 & & $\qquad(\ZERO + \ZERO{}a + \ONE) \cdot (a + aa)^* + (\ONE + \ONE{}a) \cdot (a + aa)^*$\\

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

   141 \end{tabular}

   142 \end{center}

   143  

   144 \noindent where after around 35 steps we run out of memory on a

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

   146 regular expressions and the derivative operation).  Clearly, the

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

   148 simplification rules that can be applied to regular regular

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

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

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

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

   153 algorithm \cite{AusafDyckhoffUrban2016}, they unfortunately do

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

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

   156 quickly beyond any finite bound.

   157 

   158 

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

   160 \cite{Sulzmann2014} where they introduce bitcoded

   161 regular expressions. In this version, POSIX values are

   162 represented as bitsequences and such sequences are incrementally generated

   163 when derivatives are calculated. The compact representation

   164 of bitsequences and regular expressions allows them to define a more

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

   166 derivatives finitely bounded no matter what the length of the string is.

   167 They make some informal claims about the correctness and linear behaviour

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

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

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

   171 in this paper):

   172 %

   173 \begin{quote}\it

   174   ``Correctness Claim: We further claim that the incremental parsing

   175   method [..] in combination with the simplification steps [..]

   176   yields POSIX parse trees. We have tested this claim

   177   extensively [..] but yet

   178   have to work out all proof details.'' \cite[Page 14]{Sulzmann2014}

   179 \end{quote}  

   180 

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

   182 the derivative-based lexing algorithm of Sulzmann and Lu

   183 \cite{Sulzmann2014} where regular expressions are annotated with

   184 bitsequences. We define the crucial simplification function as a

   185 recursive function, without the need of a fix-point operation. One objective of

   186 the simplification function is to remove duplicates of regular

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

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

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

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

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

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

   193 distinctWith} function that finds duplicates under an ``erasing'' function

   194 which deletes bitcodes before comparing regular expressions.

   195 We shall also introduce our own argument and definitions for

   196 establishing the correctness of the bitcoded algorithm when 

   197 simplifications are included. Finally we

   198 establish that the size of derivatives can be finitely bounded.\medskip%\footnote{ In this paper, we shall first briefly introduce the basic notions

   199 %of regular expressions and describe the definition

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

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

   202 %the correctness for the bitcoded algorithm without simplification, and

   203 %after that extend the proof to include simplification.}\smallskip

   204 %\mbox{}\\[-10mm]

   205 

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

   207 of regular expressions and describe the definition

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

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

   210 the correctness for the bitcoded algorithm without simplification, and

   211 after that extend the proof to include simplification.\mbox{}\\[-6mm]

   212 

   213 *}

   214 

   215 section {* Background *}

   216 

   217 text {*

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

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

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

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

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

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

   224   Our regular expressions are defined as usual as the following inductive

   225   datatype:\\[-4mm]

   226   %

   227   \begin{center}

   228   @{text "r ::="} \;

   229   @{const "ZERO"} $\mid$

   230   @{const "ONE"} $\mid$

   231   @{term "CH c"} $\mid$

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

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

   234   @{term "STAR r"} 

   235   \end{center}

   236 

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

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

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

   240   The constructors $+$ and $\cdot$ represent alternatives and sequences, respectively.

   241   We sometimes omit the $\cdot$ in a sequence regular expression for brevity. 

   242   The

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

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

   245 

   246   Central to Brzozowski's regular expression matcher are two functions

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

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

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

   250   regular expressions.  

   251 %

   252 \begin{center}

   253 \begin{tabular}{cc}

   254   \begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}

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

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

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

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

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

   260   & & @{text "then"} @{term "ALT (SEQ (der c r\<^sub>1) r\<^sub>2) (der c r\<^sub>2)"}\\

   261   & & @{text "else"} @{term "SEQ (der c r\<^sub>1) r\<^sub>2"}\\

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

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

   264   \end{tabular}

   265   &

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

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

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

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

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

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

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

   273   \end{tabular}  

   274 \end{tabular}  

   275 \end{center}

   276 

   277   \noindent

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

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

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

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

   282 define a simple regular expression matcher, namely

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

   284 This is essentially Brzozowski's algorithm from 1964. Its

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

   286 functional program (either in a functional programming language or in

   287 a theorem prover). The correctness of @{text match} amounts to

   288 establishing the property:%\footnote{It is a fun exercise to formally prove this property in a theorem prover.}

   289 %

   290 \begin{proposition}\label{matchcorr} 

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

   292 \end{proposition}

   293 

   294 \noindent

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

   296 

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

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

   299 is matched by which part of the regular expression.

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

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

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

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

   304   matches a string. \emph{Values} are defined as the inductive datatype

   305   %

   306   \begin{center}

   307   @{text "v ::="}

   308   @{const "Void"} $\mid$

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

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

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

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

   313   @{term "Stars vs"} 

   314   \end{center}  

   315 

   316   \noindent where we use @{term vs} to stand for a list of values. The

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

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

   319   collects the characters contained in it \cite{AusafDyckhoffUrban2016}.

   320 

   321 

   322   Sulzmann and Lu also define inductively an

   323   inhabitation relation that associates values to regular expressions. This

   324   is defined by the following six rules for the values:

   325   %

   326   \begin{center}

   327   \begin{tabular}{@ {\hspace{-12mm}}c@ {}}

   328   \begin{tabular}{@ {}c@ {}}

   329   \\[-8mm]

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

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

   332   \end{tabular}

   333   \quad

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

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

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

   337   @{thm[mode=Rule] Prf.intros(6)[of "vs" "r"]}\mbox{}\hspace{-10mm}\mbox{}

   338   \end{tabular}

   339   \end{center}

   340 

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

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

   343   It is routine to establish how values ``inhabiting'' a regular

   344   expression correspond to the language of a regular expression, namely

   345   @{thm L_flat_Prf}.

   346 

   347   In general there is more than one value inhabited by a regular

   348   expression (meaning regular expressions can typically match more

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

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

   351   regular expression can match this string. POSIX lexing is about

   352   identifying the unique value for a given regular expression and a

   353   string that satisfies the informal POSIX rules (see

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

   355 	lexing acquired its name from the fact that the corresponding

   356 	rules were described as part of the POSIX specification for

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

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

   359   One contribution of our earlier paper is to give a convenient

   360  specification for what POSIX values are (the inductive rules are shown in

   361   Figure~\ref{POSIXrules}).

   362 

   363 \begin{figure}[t]

   364   \begin{center}

   365   \begin{tabular}{@ {}c@ {}}

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

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

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

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

   370   $\mprset{flushleft}

   371    \inferrule

   372    {@{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

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

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

   375    {@{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\\

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

   377   $\mprset{flushleft}

   378    \inferrule

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

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

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

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

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

   384   \end{tabular}

   385   \end{center}

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

   387   of given a string $s$ and a regular

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

   389   regular expression matching.}\label{POSIXrules}

   390   \end{figure}

   391 

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

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

   394   construction of the derivative on regular expressions. Essentially it

   395   injects back a character into a value.

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

   397  %

   398   \begin{center}

   399   \begin{tabular}{@ {}l@ {}}

   400   \begin{tabular}{@ {}lcl@ {}}

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

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

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

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

   405   \end{tabular}\smallskip\\

   406 

   407   \begin{tabular}{@ {}cc@ {}}

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

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

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

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

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

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

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

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

   416   \end{tabular}

   417   &

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

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

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

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

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

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

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

   425   \end{tabular}

   426   \end{tabular}

   427   \end{tabular}\smallskip

   428   \end{center}

   429 

   430   \noindent

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

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

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

   434   then calculates the corresponding value for each intermediate derivative until

   435   a value for the original regular expression is generated.

   436   Graphically the algorithm by

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

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

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

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

   441   left, the second phase.

   442 %

   443 \begin{center}

   444 \begin{tikzpicture}[scale=0.99,node distance=9mm,

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   463 \end{tikzpicture}

   464 \end{center}

   465 %

   466 \noindent

   467   The picture shows the steps required when a

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

   469   "[a,b,c]"}. The first lexing algorithm by Sulzmann and Lu can be defined as:\\[-8mm]

   470 

   471 %  \begin{figure}[t]

   472 %\begin{center}

   473 %\begin{tikzpicture}[scale=1,node distance=1cm,

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   492 %\end{tikzpicture}

   493 %\end{center}

   494 %\mbox{}\\[-13mm]

   495 %

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

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

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

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

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

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

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

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

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

   505 %the POSIX value for this string and

   506 %regular expression.

   507 %\label{Sulz}}

   508 %\end{figure} 

   509 

   510 

   511 

   512   \begin{center}

   513   \begin{tabular}{lcl}

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

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

   516                      @{term "None"}  @{text "\<Rightarrow>"} @{term None}\\

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

   518   \end{tabular}

   519   \end{center}

   520 

   521 

   522 We have shown in our earlier paper \cite{AusafDyckhoffUrban2016} that

   523 this algorithm is correct, that is it generates POSIX values. The

   524 central property we established relates the derivative operation to the

   525 injection function.

   526 

   527   \begin{proposition}\label{Posix2}

   528 	\textit{If} $(s,\; r\backslash c) \rightarrow v$ \textit{then} $(c :: s,\; r) \rightarrow$ \textit{inj} $r\; c\; v$. 

   529 \end{proposition}

   530 

   531   \noindent

   532   With this in place we were able to prove:

   533 

   534 

   535   \begin{proposition}\mbox{}\smallskip\\\label{lexercorrect}

   536   \begin{tabular}{ll}

   537   (1) & @{thm (lhs) lexer_correct_None} if and only if @{thm (rhs) lexer_correct_None}\\

   538   (2) & @{thm (lhs) lexer_correct_Some} if and only if @{thm (rhs) lexer_correct_Some}\\

   539   \end{tabular}

   540   \end{proposition}

   541 

   542   \noindent

   543   In fact we have shown that, in the success case, the generated POSIX value $v$ is

   544   unique and in the failure case that there is no POSIX value $v$ that satisfies

   545   $(s, r) \rightarrow v$. While the algorithm is correct, it is excruciatingly

   546   slow in cases where the derivatives grow arbitrarily (recall the example from the

   547   Introduction). However it can be used as a convenient reference point for the correctness

   548   proof of the second algorithm by Sulzmann and Lu, which we shall describe next.

   549   

   550 *}

   551 

   552 section {* Bitcoded Regular Expressions and Derivatives *}

   553 

   554 text {*

   555 

   556   In the second part of their paper \cite{Sulzmann2014},

   557   Sulzmann and Lu describe another algorithm that also generates POSIX

   558   values but dispenses with the second phase where characters are

   559   injected ``back'' into values. For this they annotate bitcodes to

   560   regular expressions, which we define in Isabelle/HOL as the datatype

   561 

   562   \begin{center}

   563   @{term breg} $\;::=\;$ @{term "AZERO"}

   564                $\;\mid\;$ @{term "AONE bs"}

   565                $\;\mid\;$ @{term "ACHAR bs c"}

   566                $\;\mid\;$ @{term "AALTs bs rs"}

   567                $\;\mid\;$ @{term "ASEQ bs r\<^sub>1 r\<^sub>2"}

   568                $\;\mid\;$ @{term "ASTAR bs r"}

   569   \end{center}

   570 

   571   \noindent where @{text bs} stands for bitsequences; @{text r},

   572   @{text "r\<^sub>1"} and @{text "r\<^sub>2"} for bitcoded regular

   573   expressions; and @{text rs} for lists of bitcoded regular

   574   expressions. The binary alternative @{text "ALT bs r\<^sub>1 r\<^sub>2"}

   575   is just an abbreviation for \mbox{@{text "ALTs bs [r\<^sub>1, r\<^sub>2]"}}. 

   576   For bitsequences we use lists made up of the

   577   constants @{text Z} and @{text S}.  The idea with bitcoded regular

   578   expressions is to incrementally generate the value information (for

   579   example @{text Left} and @{text Right}) as bitsequences. For this 

   580   Sulzmann and Lu define a coding

   581   function for how values can be coded into bitsequences.

   582 

   583   \begin{center}

   584   \begin{tabular}{cc}

   585   \begin{tabular}{lcl}

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

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

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

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

   590   \end{tabular}

   591   &

   592   \begin{tabular}{lcl}

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

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

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

   596   \mbox{\phantom{XX}}\\

   597   \end{tabular}

   598   \end{tabular}

   599   \end{center}

   600    

   601   \noindent

   602   As can be seen, this coding is ``lossy'' in the sense that we do not

   603   record explicitly character values and also not sequence values (for

   604   them we just append two bitsequences). However, the

   605   different alternatives for @{text Left}, respectively @{text Right}, are recorded as @{text Z} and

   606   @{text S} followed by some bitsequence. Similarly, we use @{text Z} to indicate

   607   if there is still a value coming in the list of @{text Stars}, whereas @{text S}

   608   indicates the end of the list. The lossiness makes the process of

   609   decoding a bit more involved, but the point is that if we have a

   610   regular expression \emph{and} a bitsequence of a corresponding value,

   611   then we can always decode the value accurately (see Fig.~\ref{decode}).

   612   The function \textit{decode} checks whether all of the bitsequence is

   613   consumed and returns the corresponding value as @{term "Some v"}; otherwise

   614   it fails with @{text "None"}. We can establish that for a value $v$

   615   inhabited by a regular expression $r$, the decoding of its

   616   bitsequence never fails.

   617 

   618   %The decoding can be

   619   %defined by using two functions called $\textit{decode}'$ and

   620   %\textit{decode}:

   621 

   622   \begin{figure}

   623   \begin{center}

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

   625   \multicolumn{3}{@ {}l}{$\textit{decode}'\,bs\,(\ONE)$ $\;\dn\;$ $(\Empty, bs)$ \quad\qquad

   626   $\textit{decode}'\,bs\,(c)$ $\;\dn\;$ $(\Char\,c, bs)$}\\

   627   $\textit{decode}'\,(\Z\!::\!bs)\;(r_1 + r_2)$ & $\dn$ &

   628      $\textit{let}\,(v, bs_1) = \textit{decode}'\,bs\,r_1\;\textit{in}\;

   629        (\Left\,v, bs_1)$\\

   630   $\textit{decode}'\,(\S\!::\!bs)\;(r_1 + r_2)$ & $\dn$ &

   631      $\textit{let}\,(v, bs_1) = \textit{decode}'\,bs\,r_2\;\textit{in}\;

   632        (\Right\,v, bs_1)$\\                           

   633   $\textit{decode}'\,bs\;(r_1\cdot r_2)$ & $\dn$ &

   634         $\textit{let}\,(v_1, bs_1) = \textit{decode}'\,bs\,r_1\;\textit{in}$\\

   635   & &   $\textit{let}\,(v_2, bs_2) = \textit{decode}'\,bs_1\,r_2$

   636         \hspace{2mm}$\textit{in}\;(\Seq\,v_1\,v_2, bs_2)$\\

   637   $\textit{decode}'\,(\Z\!::\!bs)\,(r^*)$ & $\dn$ & $(\Stars\,[], bs)$\\

   638   $\textit{decode}'\,(\S\!::\!bs)\,(r^*)$ & $\dn$ & 

   639          $\textit{let}\,(v, bs_1) = \textit{decode}'\,bs\,r\;\textit{in}$\\

   640   & &   $\textit{let}\,(\Stars\,vs, bs_2) = \textit{decode}'\,bs_1\,r^*$

   641         \hspace{2mm}$\textit{in}\;(\Stars\,v\!::\!vs, bs_2)$\medskip\\

   642   \multicolumn{3}{l}{$\textit{decode}\,bs\,r$ $\dn$ 

   643      $\textit{let}\,(v, bs') = \textit{decode}'\,bs\,r\;\textit{in}$

   644      $\;\,\textit{if}\;bs' = []\;\textit{then}\;\textit{Some}\,v\;

   645        \textit{else}\;\textit{None}$}\\[-4mm]   

   646   \end{tabular}    

   647   \end{center}

   648   \caption{Two functions, called $\textit{decode}'$ and \textit{decode}, for decoding a value from a bitsequence with the help of a regular expression.\\[-5mm]}\label{decode}

   649   \end{figure}

   650 

   651   %\noindent

   652   %The function \textit{decode} checks whether all of the bitsequence is

   653   %consumed and returns the corresponding value as @{term "Some v"}; otherwise

   654   %it fails with @{text "None"}. We can establish that for a value $v$

   655   %inhabited by a regular expression $r$, the decoding of its

   656   %bitsequence never fails.

   657 

   658 \begin{lemma}\label{codedecode}\it

   659   If $\;\vdash v : r$ then

   660   $\;\textit{decode}\,(\textit{code}\, v)\,r = \textit{Some}\, v$.

   661 \end{lemma}

   662 

   663 

   664 

   665   Sulzmann and Lu define the function \emph{internalise}

   666   in order to transform (standard) regular expressions into annotated

   667   regular expressions. We write this operation as $r^\uparrow$.

   668   This internalisation uses the following

   669   \emph{fuse} function.	     

   670   %

   671   \begin{center}

   672   \begin{tabular}{@ {}cc@ {}}

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

   674   $\textit{fuse}\,bs\,(\textit{ZERO})$ & $\dn$ & $\textit{ZERO}$\\

   675   $\textit{fuse}\,bs\,(\textit{ONE}\,bs')$ & $\dn$ &

   676      $\textit{ONE}\,(bs\,@\,bs')$\\

   677   $\textit{fuse}\,bs\,(\textit{CHAR}\,bs'\,c)$ & $\dn$ &

   678      $\textit{CHAR}\,(bs\,@\,bs')\,c$

   679   \end{tabular}

   680   &

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

   682   $\textit{fuse}\,bs\,(\textit{ALTs}\,bs'\,rs)$ & $\dn$ &

   683      $\textit{ALTs}\,(bs\,@\,bs')\,rs$\\

   684   $\textit{fuse}\,bs\,(\textit{SEQ}\,bs'\,r_1\,r_2)$ & $\dn$ &

   685      $\textit{SEQ}\,(bs\,@\,bs')\,r_1\,r_2$\\

   686   $\textit{fuse}\,bs\,(\textit{STAR}\,bs'\,r)$ & $\dn$ &

   687      $\textit{STAR}\,(bs\,@\,bs')\,r$

   688   \end{tabular}

   689   \end{tabular}

   690   \end{center}    

   691 

   692   \noindent

   693   A regular expression can then be \emph{internalised} into a bitcoded

   694   regular expression as follows:

   695   %

   696   \begin{center}

   697   \begin{tabular}{@ {}ccc@ {}}

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

   699   $(\ZERO)^\uparrow$ & $\dn$ & $\textit{ZERO}$\\

   700   $(\ONE)^\uparrow$ & $\dn$ & $\textit{ONE}\,[]$

   701   \end{tabular}

   702   &

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

   704   $(c)^\uparrow$ & $\dn$ & $\textit{CHAR}\,[]\,c$\\

   705   $(r^*)^\uparrow$ & $\dn$ & $\textit{STAR}\;[]\,r^\uparrow$

   706   \end{tabular}

   707   &

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

   709   $(r_1 + r_2)^\uparrow$ & $\dn$ &

   710          $\textit{ALT}\;[]\,(\textit{fuse}\,[\Z]\,r_1^\uparrow)\,

   711                             (\textit{fuse}\,[\S]\,r_2^\uparrow)$\\

   712   $(r_1\cdot r_2)^\uparrow$ & $\dn$ &

   713          $\textit{SEQ}\;[]\,r_1^\uparrow\,r_2^\uparrow$

   714   \end{tabular}

   715   \end{tabular}

   716   \end{center}    

   717 

   718   \noindent

   719   There is also an \emph{erase}-function, written $r^\downarrow$, which

   720   transforms a bitcoded regular expression into a (standard) regular

   721   expression by just erasing the annotated bitsequences. We omit the

   722   straightforward definition. For defining the algorithm, we also need

   723   the functions \textit{bnullable} and \textit{bmkeps}(\textit{s}), which are the

   724   ``lifted'' versions of \textit{nullable} and \textit{mkeps} acting on

   725   bitcoded regular expressions.

   726   %

   727   \begin{center}

   728   \begin{tabular}{@ {}c@ {\hspace{2mm}}c@ {}}

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

   730   $\textit{bnullable}\,(\textit{ZERO})$ & $\dn$ & $\textit{False}$\\

   731   $\textit{bnullable}\,(\textit{ONE}\,bs)$ & $\dn$ & $\textit{True}$\\

   732   $\textit{bnullable}\,(\textit{CHAR}\,bs\,c)$ & $\dn$ & $\textit{False}$\\

   733   $\textit{bnullable}\,(\textit{ALTs}\,bs\,\rs)$ & $\dn$ &

   734      $\exists\, r \in \rs. \,\textit{bnullable}\,r$\\

   735   $\textit{bnullable}\,(\textit{SEQ}\,bs\,r_1\,r_2)$ & $\dn$ &

   736      $\textit{bnullable}\,r_1\wedge \textit{bnullable}\,r_2$\\

   737   $\textit{bnullable}\,(\textit{STAR}\,bs\,r)$ & $\dn$ &

   738      $\textit{True}$

   739   \end{tabular}

   740   &

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

   742   $\textit{bmkeps}\,(\textit{ONE}\,bs)$ & $\dn$ & $bs$\\

   743   $\textit{bmkeps}\,(\textit{ALTs}\,bs\,\rs)$ & $\dn$ &

   744   $bs\,@\,\textit{bmkepss}\,\rs$\\

   745   $\textit{bmkeps}\,(\textit{SEQ}\,bs\,r_1\,r_2)$ & $\dn$ &\\

   746   \multicolumn{3}{r}{$bs \,@\,\textit{bmkeps}\,r_1\,@\, \textit{bmkeps}\,r_2$}\\

   747   $\textit{bmkeps}\,(\textit{STAR}\,bs\,r)$ & $\dn$ &

   748      $bs \,@\, [\S]$\\

   749   $\textit{bmkepss}\,(r\!::\!\rs)$ & $\dn$ &

   750      $\textit{if}\;\textit{bnullable}\,r$\\

   751   & &$\textit{then}\;\textit{bmkeps}\,r$\\

   752   & &$\textit{else}\;\textit{bmkepss}\,\rs$

   753   \end{tabular}

   754   \end{tabular}

   755   \end{center}    

   756  

   757 

   758   \noindent

   759   The key function in the bitcoded algorithm is the derivative of a

   760   bitcoded regular expression. This derivative function calculates the

   761   derivative but at the same time also the incremental part of the bitsequences

   762   that contribute to constructing a POSIX value.	

   763   % 

   764   \begin{center}

   765   \begin{tabular}{@ {}lcl@ {}}

   766   \multicolumn{3}{@ {}l}{$(\textit{ZERO})\backslash c$ $\;\dn\;$ $\textit{ZERO}$ \quad\qquad  

   767   $(\textit{ONE}\;bs)\backslash c$ $\;\dn\;$ $\textit{ZERO}$}\\  

   768   $(\textit{CHAR}\;bs\,d)\backslash c$ & $\dn$ &

   769         $\textit{if}\;c=d\; \;\textit{then}\;

   770          \textit{ONE}\;bs\;\textit{else}\;\textit{ZERO}$\\  

   771   $(\textit{ALTs}\;bs\,\rs)\backslash c$ & $\dn$ &

   772         $\textit{ALTs}\,bs\,(\mathit{map}\,(\_\backslash c)\,\rs)$\\

   773   $(\textit{SEQ}\;bs\,r_1\,r_2)\backslash c$ & $\dn$ &

   774      $\textit{if}\;\textit{bnullable}\,r_1$\\

   775   & &$\textit{then}\;\textit{ALT}\,bs\;(\textit{SEQ}\,[]\,(r_1\backslash c)\,r_2)$

   776   $\;(\textit{fuse}\,(\textit{bmkeps}\,r_1)\,(r_2\backslash c))$\\

   777   & &$\textit{else}\;\textit{SEQ}\,bs\,(r_1\backslash c)\,r_2$\\

   778   $(\textit{STAR}\,bs\,r)\backslash c$ & $\dn$ &

   779       $\textit{SEQ}\;bs\,(\textit{fuse}\, [\Z] (r\backslash c))\,

   780        (\textit{STAR}\,[]\,r)$

   781   \end{tabular}    

   782   \end{center}

   783 

   784 

   785   \noindent

   786   This function can also be extended to strings, written $r\backslash s$,

   787   just like the standard derivative.  We omit the details. Finally we

   788   can define Sulzmann and Lu's bitcoded lexer, which we call \textit{blexer}:

   789   %

   790   \begin{center}

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

   792   $\textit{blexer}\;r\,s$ & $\dn$ &

   793       $\textit{let}\;r_{der} = (r^\uparrow)\backslash s\;\textit{in}$                

   794   $\;\;\textit{if}\; \textit{bnullable}(r_{der}) \;\;\textit{then}\;\textit{decode}\,(\textit{bmkeps}\,r_{der})\,r

   795        \;\;\textit{else}\;\textit{None}$

   796 \end{tabular}

   797 \end{center}

   798 

   799   \noindent

   800 This bitcoded lexer first internalises the regular expression $r$ and then

   801 builds the bitcoded derivative according to $s$. If the derivative is

   802 (b)nullable the string is in the language of $r$ and it extracts the bitsequence using the

   803 $\textit{bmkeps}$ function. Finally it decodes the bitsequence into a value.  If

   804 the derivative is \emph{not} nullable, then $\textit{None}$ is

   805 returned. We can show that this way of calculating a value

   806 generates the same result as \textit{lexer}.

   807 

   808 Before we can proceed we need to define a helper function, called

   809 \textit{retrieve}, which Sulzmann and Lu introduced for the correctness proof.

   810 %

   811 \begin{center}

   812   \begin{tabular}{lcl}

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

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

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

   816   @{thm (lhs) better_retrieve(1)} & $\dn$ & @{thm (rhs) better_retrieve(1)}\\

   817   @{thm (lhs) better_retrieve(2)} & $\dn$ & @{thm (rhs) better_retrieve(2)}\\

   818   @{thm (lhs) retrieve.simps(6)[of _ "r\<^sub>1" "r\<^sub>2" "v\<^sub>1" "v\<^sub>2"]}

   819       & $\dn$ & @{thm (rhs) retrieve.simps(6)[of _ "r\<^sub>1" "r\<^sub>2" "v\<^sub>1" "v\<^sub>2"]}\\

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

   821   @{thm (lhs) retrieve.simps(8)} & $\dn$ & @{thm (rhs) retrieve.simps(8)}

   822   \end{tabular}

   823   \end{center}

   824 

   825 \noindent

   826 The idea behind this function is to retrieve a possibly partial

   827 bitsequence from a bitcoded regular expression, where the retrieval is

   828 guided by a value.  For example if the value is $\Left$ then we

   829 descend into the left-hand side of an alternative in order to

   830 assemble the bitcode. Similarly for

   831 $\Right$. The property we can show is that for a given $v$ and $r$

   832 with $\vdash v : r$, the retrieved bitsequence from the internalised

   833 regular expression is equal to the bitcoded version of $v$.

   834 

   835 \begin{lemma}\label{retrievecode}

   836 If $\vdash v : r$ then $\textit{code}\, v = \textit{retrieve}\,(r^\uparrow)\,v$.

   837 \end{lemma}

   838 

   839 \noindent

   840 We also need some auxiliary facts about how the bitcoded operations

   841 relate to the ``standard'' operations on regular expressions. For

   842 example if we build a bitcoded derivative and erase the result, this

   843 is the same as if we first erase the bitcoded regular expression and

   844 then perform the ``standard'' derivative operation.

   845 

   846 \begin{lemma}\label{bnullable}\mbox{}\smallskip\\

   847   \begin{tabular}{ll}

   848 \textit{(1)} & $(r\backslash s)^\downarrow = (r^\downarrow)\backslash s$\\    

   849 \textit{(2)} & $\textit{bnullable}(r)$ iff $\textit{nullable}(r^\downarrow)$\\

   850 \textit{(3)} & $\textit{bmkeps}(r) = \textit{retrieve}\,r\,(\textit{mkeps}\,(r^\downarrow))$ provided $\textit{nullable}(r^\downarrow)$.

   851 \end{tabular}  

   852 \end{lemma}

   853 

   854 %\begin{proof}

   855 %  All properties are by induction on annotated regular expressions.

   856 %  %There are no interesting cases.

   857 %\end{proof}

   858 

   859 \noindent

   860 The only difficulty left for the correctness proof is that the bitcoded algorithm

   861 has only a ``forward phase'' where POSIX values are generated incrementally.

   862 We can achieve the same effect with @{text lexer} (which has two phases) by stacking up injection

   863 functions during the forward phase. An auxiliary function, called $\textit{flex}$,

   864 allows us to recast the rules of $\lexer$ in terms of a single

   865 phase and stacked up injection functions.

   866 %

   867 \begin{center}

   868 \begin{tabular}{@ {}l@ {}c@ {}l@ {\hspace{10mm}}l@ {}c@ {}l@ {}}

   869   $\textit{flex}\;r\,f\,[]$ & $\dn$ & $f$ & 

   870   $\textit{flex}\;r\,f\,(c\!::\!s)$ & $\dn$ &

   871   $\textit{flex}\,(r\backslash c)\,(\lambda v.\,f\,(\inj\,r\,c\,v))\,s$

   872 \end{tabular}    

   873 \end{center}    

   874 

   875 \noindent

   876 The point of this function is that when

   877 reaching the end of the string, we just need to apply the stacked up

   878 injection functions to the value generated by @{text mkeps}.

   879 Using this function we can recast the success case in @{text lexer} 

   880 as follows:

   881 

   882 \begin{lemma}\label{flex}

   883 If @{text "lexer r s = Some v"} \;then\; @{text "v = "}$\,\textit{flex}\,r\,id\,s\,

   884       (\mkeps (r\backslash s))$.

   885 \end{lemma}

   886 

   887 \noindent

   888 Note we did not redefine \textit{lexer}, we just established that the

   889 value generated by \textit{lexer} can also be obtained by a different

   890 method. While this different method is not efficient (we essentially

   891 need to traverse the string $s$ twice, once for building the

   892 derivative $r\backslash s$ and another time for stacking up injection

   893 functions), it helps us with proving

   894 that incrementally building up values in @{text blexer} generates the same result.

   895 

   896 This brings us to our main lemma in this section: if we calculate a

   897 derivative, say $r\backslash s$, and have a value, say $v$, inhabited

   898 by this derivative, then we can produce the result @{text lexer} generates

   899 by applying this value to the stacked-up injection functions

   900 that $\textit{flex}$ assembles. The lemma establishes that this is the same

   901 value as if we build the annotated derivative $r^\uparrow\backslash s$

   902 and then retrieve the corresponding bitcoded version, followed by a

   903 decoding step.

   904 

   905 \begin{lemma}[Main Lemma]\label{mainlemma}\it

   906 If $\vdash v : r\backslash s$ then 

   907 $\textit{Some}\,(\textit{flex}\,r\,\textit{id}\,s\,v) =

   908   \textit{decode}(\textit{retrieve}\,(r^\uparrow \backslash s)\,v)\,r$

   909 \end{lemma}  

   910 

   911 

   912 

   913 \noindent

   914 %With this lemma in place,

   915 We can then prove the correctness of \textit{blexer}---it indeed

   916 produces the same result as \textit{lexer}.

   917 

   918 

   919 \begin{theorem}\label{thmone}

   920 $\textit{lexer}\,r\,s = \textit{blexer}\,r\,s$

   921 \end{theorem}  

   922 

   923 

   924 

   925 \noindent This establishes that the bitcoded algorithm \emph{without}

   926 simplification produces correct results. This was

   927 only conjectured by Sulzmann and Lu in their paper

   928 \cite{Sulzmann2014}. The next step is to add simplifications.

   929 

   930 *}

   931 

   932 

   933 section {* Simplification *}

   934 

   935 text {*

   936 

   937      Derivatives as calculated by Brzozowski’s method are usually more

   938      complex regular expressions than the initial one; the result is

   939      that derivative-based matching and lexing algorithms are

   940      often abysmally slow if the ``growth problem'' is not addressed. As Sulzmann and Lu wrote, various

   941      optimisations are possible, such as the simplifications

   942      $\ZERO{}\,r \Rightarrow \ZERO$, $\ONE{}\,r \Rightarrow r$,

   943      $\ZERO{} + r \Rightarrow r$ and $r + r \Rightarrow r$. While these

   944      simplifications can considerably speed up the two algorithms  in many

   945      cases, they do not solve fundamentally the growth problem with

   946      derivatives. To see this let us return to the example from the

   947      Introduction that shows the derivatives for \mbox{@{text "(a + aa)\<^sup>*"}}.

   948      If we delete in the 3rd step all $\ZERO{}s$ and $\ONE$s according to

   949      the simplification rules shown above we obtain

   950      %

   951      %%

   952      %

   953      \begin{equation}\def\xll{\xrightarrow{\_\backslash{} [a, a, a]}}\label{derivex}

   954      (a + aa)^* \quad\xll\quad

   955       \underbrace{\mbox{$(\ONE + a) \cdot (a + aa)^*$}}_{r} \;+\;

   956      ((a + aa)^* + \underbrace{\mbox{$(\ONE + a) \cdot (a + aa)^*$}}_{r})

   957      \end{equation}

   958 

   959      \noindent This is a simpler derivative, but unfortunately we

   960      cannot make any further simplifications. This is a problem because

   961      the outermost alternatives contains two copies of the same

   962      regular expression (underlined with $r$). These copies will

   963      spawn new copies in later derivative steps and they in turn even more copies. This

   964      destroys any hope of taming the size of the derivatives.  But the

   965      second copy of $r$ in \eqref{derivex} will never contribute to a

   966      value, because POSIX lexing will always prefer matching a string

   967      with the first copy. So it could be safely removed without affecting the correctness of the algorithm.

   968      The dilemma with the simple-minded

   969      simplification rules above is that the rule $r + r \Rightarrow r$

   970      will never be applicable because as can be seen in this example the

   971      regular expressions are not next to each other but separated by another regular expression.

   972 

   973      But here is where Sulzmann and Lu's representation of generalised

   974      alternatives in the bitcoded algorithm shines: in @{term

   975      "ALTs bs rs"} we can define a more aggressive simplification by

   976      recursively simplifying all regular expressions in @{text rs} and

   977      then analyse the resulting list and remove any duplicates.

   978      Another advantage with the bitsequences in  bitcoded regular

   979      expressions is that they can be easily modified such that simplification does not

   980      interfere with the value constructions. For example we can ``flatten'', or

   981      de-nest, or spill out, @{text ALTs} as follows

   982      %

   983      \[

   984      @{term "ALTs bs\<^sub>1 ((ALTs bs\<^sub>2 rs\<^sub>2) # rs\<^sub>1)"}

   985      \quad\xrightarrow{bsimp}\quad

   986      @{term "ALTs bs\<^sub>1 ((map (fuse bs\<^sub>2) rs\<^sub>2) # rs\<^sub>1)"}

   987      \]

   988 

   989      \noindent

   990      where we just need to fuse the bitsequence that has accumulated in @{text "bs\<^sub>2"}

   991      to the alternatives in @{text "rs\<^sub>2"}. As we shall show below this will

   992      ensure that the correct value corresponding to the original (unsimplified)

   993      regular expression can still be extracted. %In this way the value construction

   994      %is not affected by simplification. 

   995 

   996      However there is one problem with the definition for the more

   997      aggressive simplification rules described by Sulzmann and Lu. Recasting

   998      their definition with our syntax they define the step of removing

   999      duplicates as

  1000      %

  1001      \[ @{text "bsimp (ALTs bs rs)"} \dn @{text "ALTs

  1002      bs (nub (map bsimp rs))"}

  1003      \]

  1004    

  1005      \noindent where they first recursively simplify the regular

  1006      expressions in @{text rs} (using @{text map}) and then use

  1007      Haskell's @{text nub}-function to remove potential

  1008      duplicates. While this makes sense when considering the example

  1009      shown in \eqref{derivex}, @{text nub} is the inappropriate

  1010      function in the case of bitcoded regular expressions. The reason

  1011      is that in general the elements in @{text rs} will have a

  1012      different annotated bitsequence and in this way @{text nub}

  1013      will never find a duplicate to be removed. One correct way to

  1014      handle this situation is to first \emph{erase} the regular

  1015      expressions when comparing potential duplicates. This is inspired

  1016      by Scala's list functions of the form \mbox{@{text "distinctWith rs eq

  1017      acc"}} where @{text eq} is an user-defined equivalence relation that

  1018      compares two elements in @{text rs}. We define this function in

  1019      Isabelle/HOL as

  1020 

  1021      \begin{center}

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

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

  1024      @{thm (lhs) distinctWith.simps(2)} & $\dn$ &

  1025      @{text "if (\<exists> y \<in> acc. eq x y)"} & @{text "then distinctWith xs eq acc"}\\

  1026      & & & @{text "else x :: distinctWith xs eq ({x} \<union> acc)"}

  1027      \end{tabular}

  1028      \end{center}

  1029 

  1030      \noindent where we scan the list from left to right (because we

  1031      have to remove later copies). In @{text distinctWith}, @{text eq} is intended to be an

  1032      equivalence relation for annotated regular expressions and @{text acc} is an accumulator for annotated regular

  1033      expressions---essentially a set of regular expressions that we have already seen

  1034      while scanning the list. Therefore we delete an element, say @{text x},

  1035      from the list provided a @{text "y"} with @{text "y"} being equivalent to @{text x} is already in the accumulator;

  1036      otherwise we keep @{text x} and scan the rest of the list but 

  1037      add @{text "x"} as another ``seen'' element to @{text acc}. We will use

  1038      @{term distinctWith} where @{text eq} is an equivalence that deletes bitsequences from bitcoded regular expressions

  1039      before comparing the components. One way to define this in Isabelle/HOL is by the following recursive function from

  1040      annotated regular expressions to @{text bool}:

  1041      %

  1042      \begin{center}

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

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

  1045      @{thm (lhs) eq1.simps(2)[of DUMMY DUMMY]} & $\dn$ & @{thm (rhs) eq1.simps(2)[of DUMMY DUMMY]}\\

  1046      @{thm (lhs) eq1.simps(3)[of DUMMY "c" DUMMY "d"]} & $\dn$ & @{thm (rhs) eq1.simps(3)[of DUMMY "c" DUMMY "d"]}\\

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

  1048      @{thm (rhs) eq1.simps(4)[of DUMMY "r\<^sub>1\<^sub>1" "r\<^sub>1\<^sub>2" DUMMY "r\<^sub>2\<^sub>1" "r\<^sub>2\<^sub>2"]}\\

  1049      @{thm (lhs) eq1.simps(5)[of DUMMY DUMMY]} & $\dn$ & @{thm (rhs) eq1.simps(5)[of DUMMY DUMMY]}\\

  1050      @{thm (lhs) eq1.simps(6)[of DUMMY "r\<^sub>1" "rs\<^sub>1" DUMMY "r\<^sub>2" "rs\<^sub>2"]} & $\dn$ &

  1051      @{thm (rhs) eq1.simps(6)[of DUMMY "r\<^sub>1" "rs\<^sub>1" DUMMY "r\<^sub>2" "rs\<^sub>2"]}\\

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

  1053      \end{tabular}

  1054      \end{center}

  1055 

  1056      \noindent

  1057      where all other cases are set to @{text False}.

  1058      This equivalence is clearly a computationally more expensive operation than @{text nub},

  1059      but is needed in order to make the removal of unnecessary copies

  1060      to work properly.

  1061 

  1062      Our simplification function depends on three more helper functions, one is called

  1063      @{text flts} and analyses lists of regular expressions coming from alternatives.

  1064      It is defined as follows:

  1065 

  1066      \begin{center}

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

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

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

  1070      @{thm (lhs) flts.simps(3)[of "bs'" "rs'"]} & $\dn$ & @{thm (rhs) flts.simps(3)[of "bs'" "rs'"]}\\

  1071      \end{tabular}

  1072      \end{center}

  1073 

  1074      \noindent

  1075      The second clause of @{text flts} removes all instances of @{text ZERO} in alternatives and

  1076      the third ``de-nests'' alternatives (but retaining the

  1077      bitsequence @{text "bs'"} accumulated in the inner alternative). There are

  1078      some corner cases to be considered when the resulting list inside an alternative is

  1079      empty or a singleton list. We take care of those cases in the

  1080      @{text "bsimpALTs"} function; similarly we define a helper function that simplifies

  1081      sequences according to the usual rules about @{text ZERO}s and @{text ONE}s:

  1082 

  1083      \begin{center}

  1084      \begin{tabular}{c@ {\hspace{5mm}}c}

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

  1086      @{text "bsimpALTs bs []"}  & $\dn$ & @{text "ZERO"}\\

  1087      @{text "bsimpALTs bs [r]"} & $\dn$ & @{text "fuse bs r"}\\

  1088      @{text "bsimpALTs bs rs"}  & $\dn$ & @{text "ALTs bs rs"}\\

  1089      \mbox{}\\

  1090      \end{tabular}

  1091      &

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

  1093      @{text "bsimpSEQ bs _ ZERO"}  & $\dn$ & @{text "ZERO"}\\

  1094      @{text "bsimpSEQ bs ZERO _"} & $\dn$ & @{text "ZERO"}\\

  1095      @{text "bsimpSEQ bs\<^sub>1 (ONE bs\<^sub>2) r\<^sub>2"}

  1096          & $\dn$ & @{text "fuse (bs\<^sub>1 @ bs\<^sub>2) r\<^sub>2"}\\

  1097      @{text "bsimpSEQ bs r\<^sub>1 r\<^sub>2"} & $\dn$ &  @{text "SEQ bs r\<^sub>1 r\<^sub>2"}

  1098      \end{tabular}

  1099      \end{tabular}

  1100      \end{center}

  1101 

  1102      \noindent

  1103      With this in place we can define our simplification function as

  1104 

  1105      \begin{center}

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

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

  1108          @{thm (rhs) bsimp.simps(1)[of "bs" "r\<^sub>1" "r\<^sub>2"]}\\

  1109      @{thm (lhs) bsimp.simps(2)[of "bs" _]} & $\dn$ & @{text "bsimpALTs bs (distinctWith (flts (map bsimp rs)) \<approx> \<emptyset>)"}\\

  1110      @{text "bsimp r"} & $\dn$ & @{text r}

  1111      \end{tabular}

  1112      \end{center}

  1113 

  1114      \noindent

  1115      We believe our recursive function @{term bsimp} simplifies regular

  1116      expressions as intended by Sulzmann and Lu. There is no point in applying the

  1117      @{text bsimp} function repeatedly (like the simplification in their paper which needs to be

  1118      applied until a fixpoint is reached) because we can show that @{term bsimp} is idempotent,

  1119      that is

  1120 

  1121      \begin{proposition}

  1122      @{term "bsimp (bsimp r) = bsimp r"}

  1123      \end{proposition}

  1124 

  1125      \noindent

  1126      This can be proved by induction on @{text r} but requires a detailed analysis

  1127      that the de-nesting of alternatives always results in a flat list of regular

  1128      expressions. We omit the details since it does not concern the correctness proof.

  1129      

  1130      Next we can include simplification after each derivative step leading to the

  1131      following notion of bitcoded derivatives:

  1132      

  1133      \begin{center}

  1134       \begin{tabular}{cc}

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