1 \documentclass[a4paper,UKenglish]{lipics}

     2 \usepackage{graphic}

     3 \usepackage{data}

     4 

     5 %\usepackage{algorithm}

     6 \usepackage{amsmath}

     7 \usepackage[noend]{algpseudocode}

     8 \usepackage{enumitem}

     9 \usepackage{nccmath}

    10 \usepackage{tikz-cd}

    11 \usetikzlibrary{positioning}

    12 

    13 \definecolor{darkblue}{rgb}{0,0,0.6}

    14 \hypersetup{colorlinks=true,allcolors=darkblue}

    15 \newcommand{\comment}[1]%

    16 {{\color{red}$\Rightarrow$}\marginpar{\raggedright\small{\bf\color{red}#1}}}

    17 

    18 % \documentclass{article}

    19 %\usepackage[utf8]{inputenc}

    20 %\usepackage[english]{babel}

    21 %\usepackage{listings}

    22 % \usepackage{amsthm}

    23 %\usepackage{hyperref}

    24 % \usepackage[margin=0.5in]{geometry}

    25 %\usepackage{pmboxdraw}

    26  

    27 \title{POSIX Regular Expression Matching and Lexing}

    28 \author{Chengsong Tan}

    29 \affil{King's College London\\

    30 London, UK\\

    31 \texttt{chengsong.tan@kcl.ac.uk}}

    32 \authorrunning{Chengsong Tan}

    33 \Copyright{Chengsong Tan}

    34 

    35 \newcommand{\dn}{\stackrel{\mbox{\scriptsize def}}{=}}%

    36 \newcommand{\ZERO}{\mbox{\bf 0}}

    37 \newcommand{\ONE}{\mbox{\bf 1}}

    38 \def\lexer{\mathit{lexer}}

    39 \def\mkeps{\mathit{mkeps}}

    40 

    41 \def\DFA{\textit{DFA}}

    42 \def\bmkeps{\textit{bmkeps}}

    43 \def\retrieve{\textit{retrieve}}

    44 \def\blexer{\textit{blexer}}

    45 \def\flex{\textit{flex}}

    46 \def\inj{\mathit{inj}}

    47 \def\Empty{\mathit{Empty}}

    48 \def\Left{\mathit{Left}}

    49 \def\Right{\mathit{Right}}

    50 \def\Stars{\mathit{Stars}}

    51 \def\Char{\mathit{Char}}

    52 \def\Seq{\mathit{Seq}}

    53 \def\Der{\mathit{Der}}

    54 \def\nullable{\mathit{nullable}}

    55 \def\Z{\mathit{Z}}

    56 \def\S{\mathit{S}}

    57 \def\rup{r^\uparrow}

    58 

    59 \newcommand{\PDER}{\textit{PDER}}

    60 \newcommand{\flts}{\textit{flts}}

    61 \newcommand{\distinctBy}{\textit{distinctBy}}

    62 \newcommand{\map}{\textit{map}}

    63 \newcommand{\size}{\textit{size}}

    64 \def\awidth{\mathit{awidth}}

    65 \def\pder{\mathit{pder}}

    66 \def\maxterms{\mathit{maxterms}}

    67 \def\bsimp{\mathit{bsimp}}

    68 

    69 %\theoremstyle{theorem}

    70 %\newtheorem{theorem}{Theorem}

    71 %\theoremstyle{lemma}

    72 %\newtheorem{lemma}{Lemma}

    73 %\newcommand{\lemmaautorefname}{Lemma}

    74 %\theoremstyle{definition}

    75 %\newtheorem{definition}{Definition}

    76 \algnewcommand\algorithmicswitch{\textbf{switch}}

    77 \algnewcommand\algorithmiccase{\textbf{case}}

    78 \algnewcommand\algorithmicassert{\texttt{assert}}

    79 \algnewcommand\Assert[1]{\State \algorithmicassert(#1)}%

    80 % New "environments"

    81 \algdef{SE}[SWITCH]{Switch}{EndSwitch}[1]{\algorithmicswitch\ #1\ \algorithmicdo}{\algorithmicend\ \algorithmicswitch}%

    82 \algdef{SE}[CASE]{Case}{EndCase}[1]{\algorithmiccase\ #1}{\algorithmicend\ \algorithmiccase}%

    83 \algtext*{EndSwitch}%

    84 \algtext*{EndCase}%

    85 

    86 

    87 \begin{document}

    88 

    89 \maketitle

    90 

    91 \begin{abstract}

    92   Brzozowski introduced in 1964 a beautifully simple algorithm for

    93   regular expression matching based on the notion of derivatives of

    94   regular expressions. In 2014, Sulzmann and Lu extended this

    95   algorithm to not just give a YES/NO answer for whether or not a

    96   regular expression matches a string, but in case it does also

    97   answers with \emph{how} it matches the string.  This is important for

    98   applications such as lexing (tokenising a string). The problem is to

    99   make the algorithm by Sulzmann and Lu fast on all inputs without

   100   breaking its correctness. We have already developed some

   101   simplification rules for this, but have not yet proved that they

   102   preserve the correctness of the algorithm. We also have not yet

   103   looked at extended regular expressions, such as bounded repetitions,

   104   negation and back-references.

   105 \end{abstract}

   106 

   107 \section{Introduction}

   108 \subsection{Basic Regex Introduction}

   109 

   110 Suppose (basic) regular expressions are given by the following grammar:

   111 \[			r ::=   \ZERO \mid  \ONE

   112 			 \mid  c  

   113 			 \mid  r_1 \cdot r_2

   114 			 \mid  r_1 + r_2   

   115 			 \mid r^*         

   116 \]

   117 

   118 Problem of matching:

   119 

   120 \begin{center}

   121 \begin{tabular}{lcr}

   122 $\textit{Match}(r, s)$ & $ =  $ & $\textit{if}\; s \in L(r)\; \textit{output} \; \textit{YES}$\\

   123 &				& $\textit{else} \; \textit{output} \; \textit{NO}$

   124 \end{tabular}

   125 \end{center}

   126 Omnipresent use of regexes in modern 

   127 software. 

   128 Examples: Snort, Bro, etc?

   129 \subsubsection{The rules for network intrusion analysis tools }

   130 TODO: read rules libraries such as Snort and the explanation for some of the rules

   131 TODO: pcre/pcre2?

   132 TODO: any other libraries?

   133 

   134 

   135 There has been many widely used libraries such as 

   136 Henry Spencer's regexp(3), RE2, etc.

   137 They are fast and successful, but ugly corner cases

   138 allowing the $\textit{ReDoS}$ attack exist, and

   139 is a non-negligible protion.

   140 \subsection{The practical problem}

   141 These corner cases either

   142 \begin{itemize}

   143 \item

   144 go unnoticed until they

   145 cause considerable grief in real life

   146 \item

   147 or force the regex library writers to pose

   148 restrictions on the input, limiting the 

   149 choice a programmer has when using regexes.

   150 \end{itemize}

   151 

   152 Motivation:

   153 We want some library that supports as many constructs as possible,

   154 but still gives formal guarantees on the correctness and running

   155 time.

   156 

   157 \subsection{Regexes that brought down CloudFlare}

   158 

   159 

   160 matching some string $s$ with a regex

   161 

   162 \begin{verbatim}

   163 (?:(?:\"|'|\]|\}|\\|\d|

   164 (?:nan|infinity|true|false|null|undefined|symbol|math)

   165 |\`|\-|\+)+[)]*;?((?:\s|-|~|!|{}|\|\||\+)*.*(?:.*=.*))) 

   166 \end{verbatim}

   167 

   168 

   169 %Could be from a network intrusion detection algorithm.

   170 %Checking whether there is some malicious code 

   171 %in the network data blocks being routed.

   172 %If so, discard the data and identify the sender for future alert.

   173 \section{Existing approaches}

   174 \subsection{Shortcomings of different methods}

   175 

   176 

   177 \subsubsection{ NFA's}

   178 $\bold{Problems With This:}$

   179 \begin{itemize}

   180 \item

   181 Can be slow especially when many states are active.

   182 \item

   183 Want Lexing Results: Can have  Exponential different matching results.

   184 \end{itemize}

   185 

   186 

   187 One regular expression can have multiple lexical values. For example

   188 for the regular expression $(a+b)^*$, it has a infinite list of

   189 values corresponding to it: $\Stars\,[]$, $\Stars\,[\Left(Char(a))]$,

   190 $\Stars\,[\Right(Char(b))]$, $\Stars\,[\Left(Char(a),\,\Right(Char(b))]$,

   191 $\ldots$, and vice versa.

   192 Even for the regular expression matching a certain string, there could 

   193 still be more than one value corresponding to it.

   194 Take the example where $r= (a^*\cdot a^*)^*$ and the string 

   195 $s=\underbrace{aa\ldots a}_\text{n \textit{a}s}$.

   196 The number of different ways of matching 

   197 without allowing any value under a star to be flattened

   198 to an empty string can be given by the following formula:

   199 \begin{center}

   200 	$C_n = (n+1)+n C_1+\ldots + 2 C_{n-1}$

   201 \end{center}

   202 and a closed form formula can be calculated to be

   203 \begin{equation}

   204 	C_n =\frac{(2+\sqrt{2})^n - (2-\sqrt{2})^n}{4\sqrt{2}}

   205 \end{equation}

   206 which is clearly in exponential order.

   207 A lexer aimed at getting all the possible values has an exponential

   208 worst case runtime. Therefore it is impractical to try to generate

   209 all possible matches in a run. In practice, we are usually 

   210 interested about POSIX values, which by intuition always

   211 match the leftmost regular expression when there is a choice

   212 and always match a sub part as much as possible before proceeding

   213 to the next token. For example, the above example has the POSIX value

   214 $ \Stars\,[\Seq(Stars\,[\underbrace{\Char(a),\ldots,\Char(a)}_\text{n iterations}], Stars\,[])]$.

   215 The output of an algorithm we want would be a POSIX matching

   216 encoded as a value.\\

   217 $\mathbf{TODO:}$

   218 \begin{itemize}

   219 \item

   220 Illustrate graphically how you can match $a*a**$ with $aaa$ in different ways. 

   221 \item

   222 Give a backtracking algorithm, and explain briefly why this can be exponentially slow.

   223 (When there is a matching, it finds straight away; where there is not one, this fails to 

   224 recognize immediately that a match cannot be possibly found, and tries out all remaining 

   225 possibilities, etc.)

   226 \item

   227 From the above point, are there statical analysis tools that single out those malicious 

   228 patterns and tell before a lexer is even run?

   229 Have a more thorough survey of the Birmingham paper.

   230 Give out the suitable scenarios for such static analysis algorithms.

   231 

   232 \end{itemize}

   233 

   234 \subsubsection{DFAs}

   235 The tool JFLEX uses it.

   236 Advantages: super fast on most regexes \\

   237 TODO: show it being fast on a lot of inputs\\

   238 Disavantages:

   239 state explosion for bounded repetitions due to 

   240 theoretic bottleneck of having to remember exactly what the

   241 suffix up to length $n$ of input string is.

   242 "Countdown States activation problem":

   243 $.*a.{100}$ requires $2^100$ + DFA states.

   244 Example:

   245 Converting $((a|b )*b.{10}){3}$ to a $\DFA$

   246 gives the error:

   247 \begin{verbatim}

   248 147972 states before minimization, 79107 states in minimized DFA

   249 Old file "search.java" saved as "search.java~"

   250 Writing code to "search.java"

   251 

   252 Unexpected exception encountered. This indicates a bug in JFlex.

   253 Please consider filing an issue at http://github.com/jflex-de/jflex/issues/new

   254 

   255 

   256 character value expected

   257 java.lang.IllegalArgumentException: character value expected

   258         at jflex.generator.PackEmitter.emitUC(PackEmitter.java:105)

   259         at jflex.generator.CountEmitter.emit(CountEmitter.java:116)

   260         at jflex.generator.Emitter.emitDynamicInit(Emitter.java:530)

   261         at jflex.generator.Emitter.emit(Emitter.java:1369)

   262         at jflex.generator.LexGenerator.generate(LexGenerator.java:115)

   263         at jflex.Main.generate(Main.java:320)

   264         at jflex.Main.main(Main.java:336)

   265 \end{verbatim}

   266 

   267 \subsubsection{variant of DFA's}

   268 counting set automata 

   269 \\

   270 TODO: microsoft 2020 oopsla CsA work, need to add bibli entry, and read, understand key novelty, learn to benchmark like it

   271 \\

   272 TODO: find weakness of such counting set automata?

   273 \\

   274 Other variants?

   275 

   276 \subsubsection{NFA and Regex: isomorphic structure}

   277 TODO: define mathematically an isomorphism?\\

   278 

   279 

   280 

   281 \subsubsection{variants of NFA's}

   282 How about acting on regular expressions themselves? Certain copies represent verbose info--that they will always match the same string--prune away!

   283 

   284 \subsection{Brzozowski's derivatives}

   285 

   286 \subsection{Sulzmann and Lu's algorithm}

   287 

   288 \subsection{Bit-coded algorithm}

   289 +bitcodes!

   290 Built on top of derivatives, but with auxiliary bits

   291 \subsection{Correctness Proof}

   292 

   293 Not proven by Sulzmann  and Lu

   294 

   295 Proven by Ausaf and Urban!!

   296 

   297 

   298 For this we have started with looking at the proof of

   299 \begin{equation}\label{lexer}

   300 \blexer \; (r^\uparrow)  s = \lexer \;r \;s,

   301 \end{equation}

   302 

   303 %\noindent

   304 %might provide us insight into proving 

   305 %\begin{center}

   306 %$\blexer \; r^\uparrow \;s = \blexers \; r^\uparrow \;s$

   307 %\end{center}

   308 

   309 \noindent

   310 which established that the bit-sequence algorithm produces the same

   311 result as the original algorithm, which does not use 

   312 bit-sequences.

   313 The proof uses two ``tricks''. One is that it uses a \flex-function

   314 

   315 \begin{center}

   316 \begin{tabular}{lcl}

   317 $\textit{flex} \;r\; f\; (c\!::\!s) $ & $\dn$ & $\textit{flex} \;  (r\backslash c) \;(\lambda v. f (inj \; r \; c \; v)) \;s$ \\

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

   319 \end{tabular}

   320 \end{center}

   321 

   322 \noindent

   323 

   324 The intuition behind the $\flex$ function is that

   325  it  accumulates a series of $\inj$ function applications when doing derivatives

   326  in a $\mathit{LIFO}$ manner. The arguments of the $\inj$ functions are kept by

   327   remembering which character

   328  was chopped off and what the regular expression looks like before

   329  chopping off that character.

   330  The $\mathit{LIFO}$ order was achieved by putting the newest $\inj$ application

   331  always before the application of $f$, the previously accumulated function applications.\\

   332 Therefore, the function $\flex$, when acted on a string $s@[c]$ where the last

   333 character is $c$, by nature can have its last injection function revealed already: 

   334 \begin{equation}\label{flex}

   335 \flex \; r \; id \; (s@[c]) \; v = \flex \;  r \; id \; s \; (inj \; (r\backslash s) \; c\; v).

   336 \end{equation}

   337 that the last character can be taken off, and the injection it causes be applied to 

   338 the argument value $v$.

   339 

   340 Ausaf and Urban proved that the Sulzmann and Lu's lexers

   341 can be charactarized by the $\flex$ function:

   342 \begin{center}

   343 $\lexer \;r\; s = \flex \;\textit{id} \; r\;s \;(\mkeps \; (r\backslash s))$.

   344 \end{center}

   345 

   346 \noindent

   347 This property says that the Sulzmann and Lu's $\lexer$ does lexing by

   348 stacking up injection functions while doing derivatives,

   349 explicitly showing the order of characters being

   350 injected back in each step.

   351 

   352 \noindent

   353 The other trick, which is the crux in the existing proof, 

   354 is the use of the $\retrieve$-function:

   355 \begin{center}

   356 \begin{tabular}{@{}l@{\hspace{2mm}}c@{\hspace{2mm}}l@{}}

   357   $\textit{retrieve}\,(_{bs}\ONE)\,\Empty$ & $\dn$ & $bs$\\

   358   $\textit{retrieve}\,(_{bs}{\bf c})\,(\Char\,d)$ & $\dn$ & $bs$\\

   359   $\textit{retrieve}\,(_{bs}\sum a::as)\,(\Left\,v)$ & $\dn$ &

   360      $bs \,@\, \textit{retrieve}\,a\,v$\\

   361   $\textit{retrieve}\,(_{bs}\sum a::as)\,(\Right\,v)$ & $\dn$ &

   362   $\textit{bs} \,@\, \textit{retrieve}\,(_{[]}\sum as)\,v$\\

   363   $\textit{retrieve}\,(_{bs}a_1\cdot a_2)\,(\Seq\,v_1\,v_2)$ & $\dn$ &

   364      $bs \,@\,\textit{retrieve}\,a_1\,v_1\,@\, \textit{retrieve}\,a_2\,v_2$\\

   365   $\textit{retrieve}\,(_{bs}a^*)\,(\Stars\,[])$ & $\dn$ &

   366      $bs \,@\, [0]$\\

   367   $\textit{retrieve}\,(_{bs}a^*)\,(\Stars\,(v\!::\!vs))$ & $\dn$ &\\

   368   \multicolumn{3}{l}{

   369      \hspace{3cm}$bs \,@\, [1] \,@\, \textit{retrieve}\,a\,v\,@\,

   370                     \textit{retrieve}\,(_{[]}a^*)\,(\Stars\,vs)$}\\

   371 \end{tabular}

   372 \end{center}

   373 

   374 \noindent

   375 Sulzmann and Lu proposed this function, but did not prove

   376 anything about it. Ausaf and Urban made use of the

   377 fact about $\retrieve$ in their proof:

   378  \begin{equation}\label{retrieve_reversible}

   379  \retrieve\; \rup \backslash c \; v = \retrieve \;  \rup (\inj \;r \;c \; v)

   380  \end{equation} 

   381 This says that $\retrieve$ will always pick up 

   382 partial information about a lexing value value and transform it into suitable bitcodes.

   383 If the information is in the regular expression (stored as bitcodes), it will keep those

   384 bitcodes with the guidance of the value,

   385 if the information is in the value, which has been injected back to the value,

   386 it will "digest" and transform that part of the value to bitcodes.

   387 

   388 \noindent

   389 

   390 Using this together with ~\eqref{flex}, we can prove that the bitcoded version of

   391 lexer is the same as Sulzmann and Lu's lexer:

   392 \begin{center} 

   393 $\lexer \; r \; s =  \flex \; r\; id\; s\; v = \textit{decode} \;( \textit{bmkeps}\; (\rup \backslash s) ) r = \blexer \; r \; s$

   394 \end{center}

   395 \noindent

   396 \begin{proof}

   397 We express $\bmkeps$ using $\retrieve$, and the theorem to prove becomes:

   398 \begin{center} 

   399 $ \flex \; r\; id\; s\; v = \textit{decode} \;( \textit{retrieve}\; (\rup \backslash s) \; v \;) r$

   400 \end{center}

   401 \noindent

   402 We prove the above by reverse induction on string $s$(meaning that the inductive step is on 

   403 $s @ [c]$ rather than $c :: s$).

   404 $v$ takes arbitrary values.\\

   405 The base case goes through trivially.\\

   406 For the inductive step, assuming

   407 $ \flex \; r\; id\; s\; v = \textit{decode} \;( \textit{retrieve}\; (\rup \backslash s) \; v \;) r$

   408 holds for all values $v$. Now we need to show that

   409 $ \flex \; r\; id\; s@[c]\; v = \textit{decode} \;( \textit{retrieve}\; (\rup \backslash (s@[c])) \; v \;) r$.\\

   410 ~\eqref{flex} allows us to do the following rewrite:

   411 \begin{center} 

   412 $ \flex \; r\; id\; (s@[c])\; v = \flex \; r \; id\; s\; (\inj \; (r \backslash s) \; c\; v)=  \textit{decode} \;( \textit{retrieve}\; (\rup \backslash s) \; (\inj \; (r\backslash s) \;c\;v)\;) r$

   413 \end{center}

   414 ~\eqref{retrieve_reversible} allows us  to further rewrite the $\mathit{RHS}$ of the above to

   415 \begin{center}

   416 $\textit{decode} \; (\textit{retrieve}\; (\rup \backslash (s @ [c])) \; v\;)  \;r$

   417 \end{center}

   418 

   419 

   420 \end{proof}

   421 

   422 

   423 

   424 \section{My Work}

   425 

   426 \subsection{an improved version of bit-coded algorithm: with simp!}

   427 

   428 \subsection{a correctness proof for bitcoded algorithm}

   429 

   430 \subsection{finiteness proof }

   431 \subsubsection{closed form}

   432 We can give the derivative of regular expressions

   433 with respect to string a closed form with respect to simplification:

   434 \begin{itemize}

   435 \item

   436 closed form for sequences:

   437 \begin{verbatim}

   438 lemma seq_closed_form: shows 

   439 "rsimp (rders_simp (RSEQ r1 r2) s) = 

   440 rsimp ( RALTS ( (RSEQ (rders_simp r1 s) r2) # 

   441                 (map (rders r2) (vsuf s r1)) 

   442               )  

   443       )"

   444 \end{verbatim}

   445 where the recursive function $\textit{vsuf}$ is defined as

   446 \begin{verbatim}

   447 fun vsuf :: "char list -> rrexp -> char list list" where

   448 "vsuf [] _ = []"

   449 |"vsuf (c#cs) r1 = (if (rnullable r1) then  (vsuf cs (rder c r1)) @ [c # cs]

   450                                       else  (vsuf cs (rder c r1))

   451                    ) "

   452 

   453 \end{verbatim}

   454 \item

   455 closed form for stars:

   456 \begin{verbatim}

   457 lemma star_closed_form:

   458   shows "rders_simp (RSTAR r0) (c#s) = 

   459 rsimp ( RALTS ( 

   460 (map (\lambda s1. RSEQ (rders_simp r0 s1) (RSTAR r0) ) 

   461 (star_updates s r [[c]]) ) ))"

   462 \end{verbatim}

   463 where the recursive function $\textit{star}\_\textit{updates}$ is defined as

   464 \begin{verbatim}

   465 fun star_update :: "char -> rrexp -> char list list -> char list list" where

   466 "star_update c r [] = []"

   467 |"star_update c r (s # Ss) = (if (rnullable (rders_simp r s)) 

   468                                 then (s@[c]) # [c] # (star_update c r Ss) 

   469                                else   (s@[c]) # (star_update c r Ss) )"

   470 

   471 fun star_updates :: "char list -> rrexp -> char list list -> char list list"

   472   where

   473 "star_updates [] r Ss = Ss"

   474 | "star_updates (c # cs) r Ss = star_updates cs r (star_update c r Ss)"

   475 

   476 \end{verbatim}

   477 

   478 

   479 \end{itemize}

   480 These closed form is a formalization of the intuition 

   481  that we can push in the derivatives

   482 of compound regular expressions to its sub-expressions, and the resulting

   483 expression is a linear combination of those sub-expressions' derivatives.

   484 \subsubsection{Estimation of closed forms' size}

   485 And thanks to $\textit{distinctBy}$ helping with deduplication,

   486 the linear combination can be  bounded by the set enumerating all 

   487 regular expressions up to a certain size :

   488 \begin{verbatim}

   489 

   490 lemma star_closed_form_bounded_by_rdistinct_list_estimate:

   491   shows "rsize (rsimp ( RALTS ( (map (\lambda s1. RSEQ (rders_simp r0 s1) (RSTAR r0) )

   492          (star_updates s r [[c]]) ) ))) <=

   493         Suc (sum_list (map rsize (rdistinct (map (\lambda s1. RSEQ (rders_simp r0 s1) (RSTAR r0) )

   494          (star_updates s r [[c]]) ) {})  ) )"

   495          

   496          lemma distinct_list_rexp_up_to_certain_size_bouded_by_set_enumerating_up_to_that_size:

   497   shows "\forallr\in set rs. (rsize r ) <= N ==> sum_list (map rsize (rdistinct rs {})) <=

   498          (card (rexp_enum N))* N"

   499          

   500          lemma ind_hypo_on_ders_leads_to_stars_bounded:

   501   shows "\foralls. rsize (rders_simp r0 s) <= N ==>        

   502       (sum_list (map rsize (rdistinct (map (\lambda s1. RSEQ (rders_simp r0 s1) (RSTAR r0) )

   503          (star_updates s r [[c]]) ) {})  ) ) <= 

   504 (card (rexp_enum (Suc (N + rsize (RSTAR r0))))) * (Suc (N + rsize (RSTAR r0)))

   505 "

   506 \end{verbatim}

   507 

   508 With the above 3 lemmas, we can argue that the inductive hypothesis

   509 $r_0$'s derivatives is bounded above  leads to $r_0^*$'s

   510 derivatives being bounded above.

   511 \begin{verbatim}

   512 

   513 lemma r0_bounded_star_bounded:

   514   shows "\foralls. rsize (rders_simp r0 s) <= N ==>

   515              \foralls. rsize (rders_simp (RSTAR r0) s) <= 

   516 (card (rexp_enum (Suc (N + rsize (RSTAR r0))))) * (Suc (N + rsize (RSTAR r0)))"

   517 \end{verbatim}

   518 

   519 

   520 And we have a similar argument for the sequence case.

   521 \subsection{stronger simplification needed}

   522 

   523 \subsubsection{Bounded List of Terms}

   524 We have seen that without simplification the size of $(a+aa)^*$

   525 grows exponentially and unbounded(where we omit certain nested

   526 parentheses among the four terms in the last explicitly written out regex):

   527 

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

   529 \begin{center}

   530 \begin{tabular}{rll}

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

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

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

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

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

   536 \end{tabular}

   537 \end{center}

   538 

   539 But if we look closely at the regex

   540 \begin{center}

   541 \begin{tabular}{rll}

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

   543 \end{tabular}

   544 \end{center}

   545 we realize that:

   546 \begin{itemize}

   547 \item

   548 The regex is  equivalent to an alternative taking a long-flattened list, 

   549 where each list is a sequence, and the second child of that sequence

   550 is always $(a+aa)^*$. In other words, the regex is a "linear combination"

   551 of terms of the form $(a+aa)\backslash s \cdot (a+aa)^*$ ($s$ is any string).

   552 \item

   553 The number of different terms of the shape $(a+aa) \backslash s \cdot (a+aa)^*$ is 

   554 bounded because the first child $(a+aa) \backslash s$ can only be one of

   555 $(\ZERO + \ZERO{}a + \ZERO)$, $(\ZERO + \ZERO{}a + \ONE)$, 

   556 $(\ONE + \ONE{}a)$ and $(\ZERO + \ZERO{}a)$.

   557 \item

   558 With simplification we have that the regex is additionally reduced to,

   559 

   560 where each term $\bsimp((a+aa)\backslash s )  $

   561 is further reduced to only

   562 $\ONE$, $\ONE + a$ and $\ZERO$.

   563 

   564 

   565 \end{itemize}

   566 Generalizing this to any regular expression of the form 

   567 $\sum_{s\in L(r)} \bsimp(r\backslash s ) \cdot r^*$,

   568 we have the closed-form for star regex's string derivative as below:

   569 $\forall r \;s.\; \exists sl. \; s.t.\;\bsimp(r^* \backslash s) = \bsimp(\sum_{s'\in sl}(r\backslash s') \cdot r^* )$.

   570 

   571 The regex $\bsimp(\sum_{s' \in sl}(r\backslash s') \cdot r^*)$ is bounded by

   572 $\distinctBy(\flts(\sum_{s'\in sl}(\bsimp(r \backslash s')) \cdot r^*))$,

   573 which again is bounded by $\distinctBy(\sum_{s'\in sl}(\bsimp(r\backslash s')) \cdot r^*)$.

   574 This might give us a polynomial bound on the length of the list

   575 $\distinctBy[(\bsimp(r\backslash s')) \cdot r^* | {s'\in sl} ]$, if the terms in 

   576 $\distinctBy[(\bsimp (r\backslash s')) | {s' \in sl}]$ has a polynomial bound.

   577 This is unfortunately not true under our current $\distinctBy$ function:

   578 If we let $r_n = ( (aa)^* + (aaa)^* + \ldots + \underline{(a\ldots a)^*}{n \,a's}) $,

   579 then we have that $\textit{maxterms} r_n = \textit{sup} (\textit{length} [\bsimp(r_n\backslash s') | s' \in sl]) = 

   580 L.C.M(1,\ldots, n)$. According to \href{http://oeis.org/A003418}{OEISA003418}

   581 this grows exponentially quickly. So we have found a regex $r_n$ where

   582 $\textit{maxterms} (r_n ^* \backslash s) \geq 2^{(n-1)}$.

   583 

   584 

   585 \subsubsection{stronger version of \distinctBy}

   586 \href{https://www.researchgate.net/publication/340874991_Partial_derivatives_of_regular_expressions_and_finite_automaton_constructions}{Antimirove}

   587 has proven a linear bound on the number of terms in the "partial derivatives" of a regular expression:

   588 \begin{center}

   589 $\size (\PDER(r))  \leq \awidth (r)$.

   590 \end{center}

   591 

   592 The proof is by structural induction on the regular expression r.

   593 The hard cases are the sequence case $r_1\cdot r_2$ and star case $r^*$.

   594 The central idea that allows the induction to go through for this bound is on the inclusion:

   595 \begin{center}

   596 $\pder_{s@[c]} (a\cdot b) \subseteq (\pder_{s@[c]} a ) \cdot b \cup (\bigcup_{s' \in Suf(s@[c])} (\pder_{s'} \; b))$

   597 \end{center} 

   598 

   599 This way, 

   600 

   601 \begin{center}

   602 \begin{tabular}{lcl}

   603 $| \pder_{s@[c]} (a\cdot b) |$ & $ \leq$ & $ | (\pder_{s@[c]} a ) \cdot b \cup (\bigcup_{s' \in Suf(s@[c])} (\pder_{s'} \; b))|$\\

   604 & $\leq$ & $| (\pder_{s@[c]} a ) \cdot b|  + | (\bigcup_{s' \in Suf(s@[c])} (\pder_{s'} \; b))|$\\

   605 & $=$ & $\awidth(a) + \awidth(b)$ \\

   606 & $=$ & $\awidth(a+b)$

   607 \end{tabular}

   608 \end{center} 

   609 

   610 we have that a compound regular expression $a\cdot b$'s subterms

   611  is bounded by its sub-expression's derivatives terms.

   612  

   613 This argument can be modified to bound the terms in 

   614 our  version of regex with strong simplification:

   615 \begin{center}

   616 \begin{tabular}{lcl}

   617 $| \maxterms (\bsimp  (a\cdot b) \backslash s)|$ & $=$ & $ |maxterms(\bsimp( (a\backslash s \cdot b) + \sum_{s'\in sl}(b\backslash s') ))|$\\

   618 & $\leq$ & $| (\pder_{s@[c]} a ) \cdot b|  + | (\bigcup_{s' \in Suf(s@[c])} (\pder_{s'} \; b))|$\\

   619 & $=$ & $\awidth(a) + \awidth(b)$ \\

   620 & $=$ & $\awidth(a+b)$

   621 \end{tabular}

   622 \end{center} 

   623 

   624 

   625 

   626 

   627 \subsection{cubic bound}

   628 Bounding the regex's subterms by

   629 its alphabetic width.

   630 

   631 The entire expression's size can be bounded by

   632 number of subterms times each subterms' size.

   633 

   634 

   635 

   636 

   637 

   638 \section{Support for bounded repetitions and other constructs}

   639 Example: 

   640 $.*a.\{100\}$ after translation to $\DFA$ and minimization will 

   641 always take over $2^{100}$ states.

   642 

   643 \section{Towards a library with fast running time practically}

   644 

   645 registers and cache-related optimizations?

   646 JVM related optimizations?

   647 

   648 \section{Past Report materials}

   649 

   650 Deciding whether a string is in the language of the regex

   651 can be intuitively done by constructing an NFA\cite{Thompson_1968}:

   652 and simulate the running of it.

   653 

   654 Which should be simple enough that modern programmers

   655 have no problems with it at all?

   656 Not really:

   657 

   658 Take $(a^*)^*\,b$ and ask whether

   659 strings of the form $aa..a$ match this regular

   660 expression. Obviously this is not the case---the expected $b$ in the last

   661 position is missing. One would expect that modern regular expression

   662 matching engines can find this out very quickly. Alas, if one tries

   663 this example in JavaScript, Python or Java 8 with strings like 28

   664 $a$'s, one discovers that this decision takes around 30 seconds and

   665 takes considerably longer when adding a few more $a$'s, as the graphs

   666 below show:

   667 

   668 \begin{center}

   669 \begin{tabular}{@{}c@{\hspace{0mm}}c@{\hspace{0mm}}c@{}}

   670 \begin{tikzpicture}

   671 \begin{axis}[

   672     xlabel={$n$},

   673     x label style={at={(1.05,-0.05)}},

   674     ylabel={time in secs},

   675     enlargelimits=false,

   676     xtick={0,5,...,30},

   677     xmax=33,

   678     ymax=35,

   679     ytick={0,5,...,30},

   680     scaled ticks=false,

   681     axis lines=left,

   682     width=5cm,

   683     height=4cm, 

   684     legend entries={JavaScript},  

   685     legend pos=north west,

   686     legend cell align=left]

   687 \addplot[red,mark=*, mark options={fill=white}] table {re-js.data};

   688 \end{axis}

   689 \end{tikzpicture}

   690   &

   691 \begin{tikzpicture}

   692 \begin{axis}[

   693     xlabel={$n$},

   694     x label style={at={(1.05,-0.05)}},

   695     %ylabel={time in secs},

   696     enlargelimits=false,

   697     xtick={0,5,...,30},

   698     xmax=33,

   699     ymax=35,

   700     ytick={0,5,...,30},

   701     scaled ticks=false,

   702     axis lines=left,

   703     width=5cm,

   704     height=4cm, 

   705     legend entries={Python},  

   706     legend pos=north west,

   707     legend cell align=left]

   708 \addplot[blue,mark=*, mark options={fill=white}] table {re-python2.data};

   709 \end{axis}

   710 \end{tikzpicture}

   711   &

   712 \begin{tikzpicture}

   713 \begin{axis}[

   714     xlabel={$n$},

   715     x label style={at={(1.05,-0.05)}},

   716     %ylabel={time in secs},

   717     enlargelimits=false,

   718     xtick={0,5,...,30},

   719     xmax=33,

   720     ymax=35,

   721     ytick={0,5,...,30},

   722     scaled ticks=false,

   723     axis lines=left,

   724     width=5cm,

   725     height=4cm, 

   726     legend entries={Java 8},  

   727     legend pos=north west,

   728     legend cell align=left]

   729 \addplot[cyan,mark=*, mark options={fill=white}] table {re-java.data};

   730 \end{axis}

   731 \end{tikzpicture}\\

   732 \multicolumn{3}{c}{Graphs: Runtime for matching $(a^*)^*\,b$ with strings 

   733            of the form $\underbrace{aa..a}_{n}$.}

   734 \end{tabular}    

   735 \end{center}  

   736 

   737 Why?

   738 Using $\textit{NFA}$'s that can backtrack.

   739 %TODO: what does it mean to do DFS BFS on NFA's

   740 	

   741 

   742 Then how about determinization?

   743 \begin{itemize}

   744 \item

   745  Turning NFA's to DFA's can cause the size of the automata

   746 to blow up exponentially.

   747 \item

   748 Want to extract submatch information.

   749 For example, 

   750 $r_1 \cdot r_2$ matches $s$,

   751 want to know $s = s_1@s_2$ where $s_i$ 

   752 corresponds to $r_i$. Where $s_i$ might be the

   753 attacker's ip address.

   754 \item

   755 Variants such as counting automaton exist.

   756 But usually made super fast on a certain class

   757 of regexes like bounded repetitions:

   758 \begin{verbatim}

   759 .*a.{100}

   760 \end{verbatim}

   761 On a lot of inputs this works very well.

   762 On average good practical performance.

   763 ~10MiB per second.

   764 But cannot be super fast on all inputs of regexes and strings,

   765 can be imprecise (incorrect) when it comes to more complex regexes.

   766 

   767 \end{itemize}

   768 %TODO: real world example?

   769 

   770 

   771 

   772 \subsection{derivatives}

   773 Q:

   774 Is there an efficient lexing algorithm with provable guarantees on 

   775 correctness and running time?

   776 Brzozowski Derivatives\cite{Brzozowski1964}!

   777 

   778 \begin{center}

   779 		\begin{tabular}{lcl}

   780 			$\nullable(\ZERO)$     & $\dn$ & $\mathit{false}$ \\  

   781 			$\nullable(\ONE)$      & $\dn$ & $\mathit{true}$ \\

   782 			$\nullable(c)$ 	       & $\dn$ & $\mathit{false}$ \\

   783 			$\nullable(r_1 + r_2)$ & $\dn$ & $\nullable(r_1) \vee \nullable(r_2)$ \\

   784 			$\nullable(r_1\cdot r_2)$  & $\dn$ & $\nullable(r_1) \wedge \nullable(r_2)$ \\

   785 			$\nullable(r^*)$       & $\dn$ & $\mathit{true}$ \\

   786 		\end{tabular}

   787 	\end{center}

   788 	

   789 	

   790 	

   791 This function simply tests whether the empty string is in $L(r)$.

   792 He then defined

   793 the following operation on regular expressions, written

   794 $r\backslash c$ (the derivative of $r$ w.r.t.~the character $c$):

   795 

   796 \begin{center}

   797 \begin{tabular}{lcl}

   798 		$\ZERO \backslash c$ & $\dn$ & $\ZERO$\\  

   799 		$\ONE \backslash c$  & $\dn$ & $\ZERO$\\

   800 		$d \backslash c$     & $\dn$ & 

   801 		$\mathit{if} \;c = d\;\mathit{then}\;\ONE\;\mathit{else}\;\ZERO$\\

   802 $(r_1 + r_2)\backslash c$     & $\dn$ & $r_1 \backslash c \,+\, r_2 \backslash c$\\

   803 $(r_1 \cdot r_2)\backslash c$ & $\dn$ & $\mathit{if} \, nullable(r_1)$\\

   804 	&   & $\mathit{then}\;(r_1\backslash c) \cdot r_2 \,+\, r_2\backslash c$\\

   805 	&   & $\mathit{else}\;(r_1\backslash c) \cdot r_2$\\

   806 	$(r^*)\backslash c$           & $\dn$ & $(r\backslash c) \cdot r^*$\\

   807 \end{tabular}

   808 \end{center}

   809 

   810 

   811 

   812 

   813 \begin{ceqn}

   814 \begin{equation}\label{graph:01}

   815 \begin{tikzcd}

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

   817 v_0           & v_1 \arrow[l,"inj_{r_0} c_0"]                & v_2 \arrow[l, "inj_{r_1} c_1"]              & v_n \arrow[l, dashed]         

   818 \end{tikzcd}

   819 \end{equation}

   820 \end{ceqn}

   821 Nicely functional, correctness easily provable, but suffers

   822 from large stack size with long strings, and 

   823 inability to perform even moderate simplification.

   824 

   825 

   826 

   827 The Sulzmann and Lu's bit-coded algorithm:

   828 \begin{figure}

   829 \centering

   830 \includegraphics[scale=0.3]{bitcoded_sulzmann.png}

   831 \end{figure}

   832 

   833 This one-phase algorithm is free from the burden of large stack usage:

   834 

   835 \begin{center}

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

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

   838 \node (r0)  {$r_0$};

   839 \node (r1) [right=of r0]{$r_1$};

   840 \draw[->,line width=0.2mm](r0)--(r1) node[above,midway] {$\backslash\,c_0$};

   841 \node (r2) [right=of r1]{$r_2$};

   842 \draw[->, line width = 0.2mm](r1)--(r2) node[above,midway] {$\backslash\,c_1$};

   843 \node (rn) [right=of r2]{$r_n$};

   844 \draw[dashed,->,line width=0.2mm](r2)--(rn) node[above,midway] {} ;

   845 \draw (rn) node[anchor=west] {\;\raisebox{3mm}{$\nullable$}};

   846 \node (bs) [below=of rn]{$bs$};

   847 \draw[->,line width=0.2mm](rn) -- (bs);

   848 \node (v0) [left=of bs] {$v_0$};

   849 \draw[->,line width=0.2mm](bs)--(v0) node[below,midway] {$\textit{decode}$};

   850 \draw (rn) node[anchor=north west] {\;\raisebox{-8mm}{$\textit{collect bits}$}};

   851 \draw[->, line width=0.2mm](v0)--(r0) node[below, midway] {};

   852 \end{tikzpicture}

   853 \end{center}

   854 

   855 

   856 

   857 This is functional code, and easily provable (proof by Urban and Ausaf).

   858 

   859 But it suffers from exponential blows even with the simplification steps:

   860 \begin{figure}

   861 \centering

   862 \includegraphics[scale= 0.3]{pics/nub_filter_simp.png}

   863 \end{figure}

   864 claim: Sulzmann and Lu claimed it linear $w.r.t$ input.

   865 

   866 example that blows it up:

   867 $(a+aa)^*$

   868 \section{Contributions}

   869 \subsection{Our contribution 1}

   870 an improved version of the above algorithm that solves most blow up 

   871 cases, including the above example.

   872 

   873 a formalized closed-form for string derivatives:

   874 \[ (\sum rs) \backslash_s s = simp(\sum_{r \in rs}(r \backslash_s s)) \]

   875 \[ (r1\cdot r2) \backslash_s s = simp(r_1 \backslash_s s  \cdot r_2 + \sum_{s' \in Suffix(s)} r_2 \backslash_s s' )\]

   876 \[r0^* \backslash_s s = simp(\sum_{s' \in substr(s)} (r0 \backslash_s s') \cdot r0^*) \]

   877 

   878 

   879 

   880 Also with a size guarantee that make sure the size of the derivatives 

   881 don't go up unbounded.

   882 

   883 

   884 \begin{theorem}

   885 Given a regular expression r, we have 

   886 \begin{center}

   887 $\exists N_r.\; s.t. \;\forall s. \; |r \backslash_s s| < N_r$

   888 \end{center}

   889 \end{theorem}

   890 

   891 The proof for this is using partial derivative's terms to bound it.

   892 \begin{center}

   893 \begin{tabular}{lcl}

   894 $| \maxterms (\bsimp  (a\cdot b) \backslash s)|$ & $=$ & $ |maxterms(\bsimp( (a\backslash s \cdot b) + \sum_{s'\in sl}(b\backslash s') ))|$\\

   895 & $\leq$ & $| (\pder_{s@[c]} a ) \cdot b|  + | (\bigcup_{s' \in Suf(s@[c])} (\pder_{s'} \; b))|$\\

   896 & $=$ & $\awidth(a) + \awidth(b)$ \\

   897 & $=$ & $\awidth(a+b)$

   898 \end{tabular}

   899 \end{center} 

   900 

   901 

   902 \subsection{Our Contribution 2}

   903 more aggressive simplification that prunes away sub-parts

   904 of a regex based on what terms has appeared before.

   905 Which gives us a truly linear bound on the input length.

   906 

   907 

   908 

   909 \section{To be completed}

   910 

   911 benchmarking our algorithm against JFLEX

   912 counting set automata, Silex, other main regex engines (incorporate their ideas such

   913 as zippers and other data structures reducing memory use).

   914 

   915 extend to back references.

   916 

   917 

   918 

   919 

   920 

   921 

   922 \noindent These are clearly abysmal and possibly surprising results. One

   923 would expect these systems to do  much better than that---after all,

   924 given a DFA and a string, deciding whether a string is matched by this

   925 DFA should be linear in terms of the size of the regular expression and

   926 the string?

   927 

   928 Admittedly, the regular expression $(a^*)^*\,b$ is carefully chosen to

   929 exhibit this super-linear behaviour.  But unfortunately, such regular

   930 expressions are not just a few outliers. They are actually 

   931 frequent enough to have a separate name created for

   932 them---\emph{evil regular expressions}. In empiric work, Davis et al

   933 report that they have found thousands of such evil regular expressions

   934 in the JavaScript and Python ecosystems \cite{Davis18}. Static analysis

   935 approach that is both sound and complete exists\cite{17Bir}, but the running 

   936 time on certain examples in the RegExLib and Snort regular expressions

   937 libraries is unacceptable. Therefore the problem of efficiency still remains.

   938 

   939 This superlinear blowup in matching algorithms sometimes causes

   940 considerable grief in real life: for example on 20 July 2016 one evil

   941 regular expression brought the webpage

   942 \href{http://stackexchange.com}{Stack Exchange} to its

   943 knees.\footnote{\url{https://stackstatus.net/post/147710624694/outage-postmortem-july-20-2016}}

   944 In this instance, a regular expression intended to just trim white

   945 spaces from the beginning and the end of a line actually consumed

   946 massive amounts of CPU-resources---causing web servers to grind to a

   947 halt. This happened when a post with 20,000 white spaces was submitted,

   948 but importantly the white spaces were neither at the beginning nor at

   949 the end. As a result, the regular expression matching engine needed to

   950 backtrack over many choices. In this example, the time needed to process

   951 the string was $O(n^2)$ with respect to the string length. This

   952 quadratic overhead was enough for the homepage of Stack Exchange to

   953 respond so slowly that the load balancer assumed there must be some

   954 attack and therefore stopped the servers from responding to any

   955 requests. This made the whole site become unavailable. Another very

   956 recent example is a global outage of all Cloudflare servers on 2 July

   957 2019. A poorly written regular expression exhibited exponential

   958 behaviour and exhausted CPUs that serve HTTP traffic. Although the

   959 outage had several causes, at the heart was a regular expression that

   960 was used to monitor network

   961 traffic.\footnote{\url{https://blog.cloudflare.com/details-of-the-cloudflare-outage-on-july-2-2019/}}

   962 

   963 The underlying problem is that many ``real life'' regular expression

   964 matching engines do not use DFAs for matching. This is because they

   965 support regular expressions that are not covered by the classical

   966 automata theory, and in this more general setting there are quite a few

   967 research questions still unanswered and fast algorithms still need to be

   968 developed (for example how to treat efficiently bounded repetitions, negation and

   969 back-references).

   970 %question: dfa can have exponential states. isn't this the actual reason why they do not use dfas?

   971 %how do they avoid dfas exponential states if they use them for fast matching?

   972 

   973 There is also another under-researched problem to do with regular

   974 expressions and lexing, i.e.~the process of breaking up strings into

   975 sequences of tokens according to some regular expressions. In this

   976 setting one is not just interested in whether or not a regular

   977 expression matches a string, but also in \emph{how}.  Consider for

   978 example a regular expression $r_{key}$ for recognising keywords such as

   979 \textit{if}, \textit{then} and so on; and a regular expression $r_{id}$

   980 for recognising identifiers (say, a single character followed by

   981 characters or numbers). One can then form the compound regular

   982 expression $(r_{key} + r_{id})^*$ and use it to tokenise strings.  But

   983 then how should the string \textit{iffoo} be tokenised?  It could be

   984 tokenised as a keyword followed by an identifier, or the entire string

   985 as a single identifier.  Similarly, how should the string \textit{if} be

   986 tokenised? Both regular expressions, $r_{key}$ and $r_{id}$, would

   987 ``fire''---so is it an identifier or a keyword?  While in applications

   988 there is a well-known strategy to decide these questions, called POSIX

   989 matching, only relatively recently precise definitions of what POSIX

   990 matching actually means have been formalised

   991 \cite{AusafDyckhoffUrban2016,OkuiSuzuki2010,Vansummeren2006}. Such a

   992 definition has also been given by Sulzmann and  Lu \cite{Sulzmann2014},

   993 but the corresponding correctness proof turned out to be  faulty

   994 \cite{AusafDyckhoffUrban2016}. Roughly, POSIX matching means matching

   995 the longest initial substring. In the case of a tie, the initial

   996 sub-match is chosen according to some priorities attached to the regular

   997 expressions (e.g.~keywords have a higher priority than identifiers).

   998 This sounds rather simple, but according to Grathwohl et al \cite[Page

   999 36]{CrashCourse2014} this is not the case. They wrote:

  1000 

  1001 \begin{quote}

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

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

  1004 various subexpressions.''

  1005 \end{quote}

  1006 

  1007 \noindent

  1008 This is also supported by evidence collected by Kuklewicz

  1009 \cite{Kuklewicz} who noticed that a number of POSIX regular expression

  1010 matchers calculate incorrect results.

  1011 

  1012 Our focus in this project is on an algorithm introduced by Sulzmann and

  1013 Lu in 2014 for regular expression matching according to the POSIX

  1014 strategy \cite{Sulzmann2014}. Their algorithm is based on an older

  1015 algorithm by Brzozowski from 1964 where he introduced the notion of

  1016 derivatives of regular expressions~\cite{Brzozowski1964}. We shall

  1017 briefly explain this algorithm next.

  1018 

  1019 \section{The Algorithm by Brzozowski based on Derivatives of Regular

  1020 Expressions}

  1021 

  1022 Suppose (basic) regular expressions are given by the following grammar:

  1023 \[			r ::=   \ZERO \mid  \ONE

  1024 			 \mid  c  

  1025 			 \mid  r_1 \cdot r_2

  1026 			 \mid  r_1 + r_2   

  1027 			 \mid r^*         

  1028 \]

  1029 

  1030 \noindent

  1031 The intended meaning of the constructors is as follows: $\ZERO$

  1032 cannot match any string, $\ONE$ can match the empty string, the

  1033 character regular expression $c$ can match the character $c$, and so

  1034 on.

  1035 

  1036 The ingenious contribution by Brzozowski is the notion of

  1037 \emph{derivatives} of regular expressions.  The idea behind this

  1038 notion is as follows: suppose a regular expression $r$ can match a

  1039 string of the form $c\!::\! s$ (that is a list of characters starting

  1040 with $c$), what does the regular expression look like that can match

  1041 just $s$? Brzozowski gave a neat answer to this question. He started

  1042 with the definition of $nullable$:

  1043 \begin{center}

  1044 		\begin{tabular}{lcl}

  1045 			$\nullable(\ZERO)$     & $\dn$ & $\mathit{false}$ \\  

  1046 			$\nullable(\ONE)$      & $\dn$ & $\mathit{true}$ \\

  1047 			$\nullable(c)$ 	       & $\dn$ & $\mathit{false}$ \\

  1048 			$\nullable(r_1 + r_2)$ & $\dn$ & $\nullable(r_1) \vee \nullable(r_2)$ \\

  1049 			$\nullable(r_1\cdot r_2)$  & $\dn$ & $\nullable(r_1) \wedge \nullable(r_2)$ \\

  1050 			$\nullable(r^*)$       & $\dn$ & $\mathit{true}$ \\

  1051 		\end{tabular}

  1052 	\end{center}

  1053 This function simply tests whether the empty string is in $L(r)$.

  1054 He then defined

  1055 the following operation on regular expressions, written

  1056 $r\backslash c$ (the derivative of $r$ w.r.t.~the character $c$):

  1057 

  1058 \begin{center}

  1059 \begin{tabular}{lcl}

  1060 		$\ZERO \backslash c$ & $\dn$ & $\ZERO$\\  

  1061 		$\ONE \backslash c$  & $\dn$ & $\ZERO$\\

  1062 		$d \backslash c$     & $\dn$ & 

  1063 		$\mathit{if} \;c = d\;\mathit{then}\;\ONE\;\mathit{else}\;\ZERO$\\

  1064 $(r_1 + r_2)\backslash c$     & $\dn$ & $r_1 \backslash c \,+\, r_2 \backslash c$\\

  1065 $(r_1 \cdot r_2)\backslash c$ & $\dn$ & $\mathit{if} \, nullable(r_1)$\\

  1066 	&   & $\mathit{then}\;(r_1\backslash c) \cdot r_2 \,+\, r_2\backslash c$\\

  1067 	&   & $\mathit{else}\;(r_1\backslash c) \cdot r_2$\\

  1068 	$(r^*)\backslash c$           & $\dn$ & $(r\backslash c) \cdot r^*$\\

  1069 \end{tabular}

  1070 \end{center}

  1071 

  1072 %Assuming the classic notion of a

  1073 %\emph{language} of a regular expression, written $L(\_)$, t

  1074 

  1075 \noindent

  1076 The main property of the derivative operation is that

  1077 

  1078 \begin{center}

  1079 $c\!::\!s \in L(r)$ holds

  1080 if and only if $s \in L(r\backslash c)$.

  1081 \end{center}

  1082 

  1083 \noindent

  1084 For us the main advantage is that derivatives can be

  1085 straightforwardly implemented in any functional programming language,

  1086 and are easily definable and reasoned about in theorem provers---the

  1087 definitions just consist of inductive datatypes and simple recursive

  1088 functions. Moreover, the notion of derivatives can be easily

  1089 generalised to cover extended regular expression constructors such as

  1090 the not-regular expression, written $\neg\,r$, or bounded repetitions

  1091 (for example $r^{\{n\}}$ and $r^{\{n..m\}}$), which cannot be so

  1092 straightforwardly realised within the classic automata approach.

  1093 For the moment however, we focus only on the usual basic regular expressions.

  1094 

  1095 

  1096 Now if we want to find out whether a string $s$ matches with a regular

  1097 expression $r$, we can build the derivatives of $r$ w.r.t.\ (in succession)

  1098 all the characters of the string $s$. Finally, test whether the

  1099 resulting regular expression can match the empty string.  If yes, then

  1100 $r$ matches $s$, and no in the negative case. To implement this idea

  1101 we can generalise the derivative operation to strings like this:

  1102 

  1103 \begin{center}

  1104 \begin{tabular}{lcl}

  1105 $r \backslash (c\!::\!s) $ & $\dn$ & $(r \backslash c) \backslash s$ \\

  1106 $r \backslash [\,] $ & $\dn$ & $r$

  1107 \end{tabular}

  1108 \end{center}

  1109 

  1110 \noindent

  1111 and then define as  regular-expression matching algorithm: 

  1112 \[

  1113 match\;s\;r \;\dn\; nullable(r\backslash s)

  1114 \]

  1115 

  1116 \noindent

  1117 This algorithm looks graphically as follows:

  1118 \begin{equation}\label{graph:*}

  1119 \begin{tikzcd}

  1120 r_0 \arrow[r, "\backslash c_0"]  & r_1 \arrow[r, "\backslash c_1"] & r_2 \arrow[r, dashed]  & r_n  \arrow[r,"\textit{nullable}?"] & \;\textrm{YES}/\textrm{NO}

  1121 \end{tikzcd}

  1122 \end{equation}

  1123 

  1124 \noindent

  1125 where we start with  a regular expression  $r_0$, build successive

  1126 derivatives until we exhaust the string and then use \textit{nullable}

  1127 to test whether the result can match the empty string. It can  be

  1128 relatively  easily shown that this matcher is correct  (that is given

  1129 an $s = c_0...c_{n-1}$ and an $r_0$, it generates YES if and only if $s \in L(r_0)$).

  1130 

  1131  

  1132 \section{Values and the Algorithm by Sulzmann and Lu}

  1133 

  1134 One limitation of Brzozowski's algorithm is that it only produces a

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