# RE#: High Performance Derivative-Based Regex Matching with Intersection,
Complement and Lookarounds

Ian Erik Varatalu  0000-0003-1267-2712 Tallinn University of TechnologyEstonia
<EMAIL_ADDRESS>,  Margus Veanes  0009-0008-8427-7977 MicrosoftUSA
<EMAIL_ADDRESS>and  Juhan-Peep Ernits  0000-0002-4591-0425 Tallinn
University of TechnologyEstonia<EMAIL_ADDRESS>
###### Abstract.

We present a tool and theory $\mathbf{RE\\#}$ for regular expression matching
that is built on symbolic derivatives, does not use backtracking, and, in
addition to the classical operators, also supports complement, intersection
and lookarounds. We develop the theory formally and show that the main
matching algorithm has _input-linear_ complexity both in theory as well as
experimentally. We apply thorough evaluation on popular benchmarks that show
that $\mathbf{RE\\#}$ is _over 71% faster than the next fastest regex engine
in Rust_ on the baseline, and _outperforms all state-of-the-art engines on
extensions of the benchmarks often by several orders of magnitude._

##  1\. Introduction

In the seminal paper (Thompson, 1968) Thompson describes his regular
expression search algorithm for _standard_ regular expressions at the high
level as follows,

> “In the terms of Brzozowski, this algorithm continually takes the left
> derivative of the given regular expression with respect to the text to be
> searched.”

citing Brzozowski’s work (Brzozowski, 1964) from four years earlier.
Thompson’s algorithm compiles regular expressions into a very efficient form
of _automata_ and _has stood the test of time_ : its variants today constitute
the core of many state-of-the-art industrial _nonbacktracking_ regular
expression engines such as _RE2_ (Cox, 2010; Google, 2024) and the regex
engine of _Rust_ (Rust, 2024). Earlier automata based classical algorithms for
regular expression matching include (McNaughton and Yamada, 1960) and
(Glushkov, 1961) as a variant of the latter is used in _Hyperscan_ (Wang et
al., 2019).

Thompson’s algorithm as well as Glushkov’s construction have, by virtue of
their efficiency for the _standard_ or _classical_ subset, to some degree,
influenced how regular expression features have evolved over the past decades.
The standard fragment allows only _union_ (`|`) as a Boolean operator, and,
unfortunately, neither _intersection_ (`&`) nor _complement_ (`~`) ever made
it into the official notation, not even as reserved operators. In particular,
the standard fragment (with _anchors_), has been considered more-or-less as
the only feasible and safe fragment of regular expressions for which matching
can be performed reliably _without backtracking_ in _input-linear_ time.

> The broad goal of this paper is to break this decades long belief that
> nonbacktracking algorithms for matching are only viable for standard regular
> expressions.

_Backtracking_ based matching (Spencer, 1994), although much more general, is
considered to be unsafe in security critical applications because backtracking
may cause nonlinear search complexity that can expose catastrophic denial of
service vulnerabilities (OWASP, 2024; Davis et al., 2018; Davis, 2019). To
increase expressivity of the standard fragment, extensions such as unbounded
positive and negative _lookaheads_ have been added, but are currently only
supported by some backtracking based regex backends. A typical example of a
regex involving lookaheads is a _password filter_

(?=.*[a-z])(?=.*[A-Z])(?=.*\d)(?=.*[!-/])\S*

that checks the presence of at least one lowercase letter, one uppercase
letter, one digit, and one special character. If only the standard fragment is
allowed then the size of an equivalent regex grows _factorially_ as the number
of such individual constraints is increased, and becomes not only unreadable
and very difficult to formulate, but also infeasible. With intersection the
above regular expression takes the following equivalent form as a _filter_

(.*[a-z].*)&(.*[A-Z].*)&(.*\d.*)&(.*[!-/].*)&\S*

It was four decades after Thompson’s work when (Owens et al., 2009) recognized
that a key aspect of Brzozowski’s work had been forgotten:

> “It easily supports extending the regular-expression operators with boolean
> operations, such as intersection and complement. Unfortunately, this
> technique has been lost in the sands of time and few computer scientists are
> aware of it.”

Namely that derivatives provide an elegant algebraic framework to formulate
matching in functional programming, _not only for standard regular
expressions_ but also supporting _intersection_ and _complement_ , and can
moreover naturally support _large alphabets_. The first _industrial_
implementation of derivatives for standard regexes in an imperative language
(C#) materialized a decade later (Saarikivi et al., 2019) and was used for
_credential scanning_ (Microsoft, 2021a) while preserving input-linear
complexity of match search. This work was recently extended to support anchors
and to maintain PCRE (backtracking) match semantics (Moseley et al., 2023) and
is now part of the official release of .NET through the new NonBacktracking
regular expression option, where one of the key contributions is a new
formalization of derivatives that is based on _locations_ in words rather than
individual characters, which made it possible to support anchors using
derivatives.

Here we build on the theory (Moseley et al., 2023) and extend it to include
regular expressions that allow _all_ of the Boolean operators, including
_intersection_ and _complement_ , as well as any other Boolean operator that
is convenient to use for the matching task at hand, such as e.g. _symmetric
difference_ (_XOR_). The framework also supports _lookarounds_ as a
generalization of anchors.

To illustrate a combined use of many of the extended features, consider the
regex

$\underbrace{\texttt{(?<=author.*).*}}_{(1)}\,\&\,\underbrace{\texttt{\char
126\relax(.*and.*)}}_{(2)}\,\&\,\underbrace{\texttt{{\char 92\relax}b{\char
92\relax w}.*{\char 92\relax w}{\char 92\relax}b}}_{(3)}$

@a | rticle{ | ORT09,
---|---|---
| author |  = {Scott Owens and John H. Reppy and Aaron Turon},
| title | = {Regular-expression Derivatives Re-examined},
| journal | = {J. Funct. Program.},
| year | = {2009},
}

that matches all substrings in all _lines_ (. matches any character except \n)
that are: 1) preceded by "author" (via the lookbehind), 2) do not contain
"and", and 3) begin and end with _word letters_ (`\w`) surrounded by _word
boundaries_ (`\b`). This regex finds all the authors in a bibtex text, such as
the one shown above, where all the match results are highlighted.

We develop our theory formally and show that our matching algorithm is _input-
linear_ on single match search despite all the extensions. We have implemented
the theory in a new tool $\mathbf{RE\\#}$ that is built on top of the open
source codebase of .NET regular expressions (Microsoft, 2022) where we have
made use of several recent features available in .NET9, such as e.g. further
SIMD vectorization of string matching functions and implementation of the
Teddy (Qiu et al., 2021) algorithm. We show through comprehensive evaluation,
using the _BurntSushi/rebar_ benchmarking tool (Gallant, 2024) evaluating
engines with respect to finding _all matches_ , that

(a) Monster benchmarks (Section 6.2.2).

(b) Sets and Unicode benchmarks (Section 6.2.5).

Figure 1. Two evaluations from Section 6. $\mathbf{RE\\#}$ is the baseline and
$y$-axis is relative slowdown in _log_ scale.

  1. $\checkmark$

Baseline: $\mathbf{RE\\#}$ is not only on par with state-of-the-art matching
engines on the benchmarks but places overall _first_ in the summarized
measurement (Section 6.1), _over 71% faster than the next fastest engine Rust_
as shown in Figure 5(a) ($2.54/1.48\approx 1.716$). We explain the key aspects
of each individual experiment.

  2. $\checkmark$

Extensions: We provide compelling experimental evidence on a new set of
benchmarks involving many of the extended features that are either very
difficult to express or fall outside the expressivity of existing tools. Here
we want to draw attention to Figure 1 where $\mathbf{RE\\#}$ _outperforms all
other engines and often by several orders of magnitude_.

To a large extent, most optimizations rely heavily on the algebraic treatment
of derivatives where regex based rewrite rules are available that would
otherwise be very difficult to detect solely at the level of automata. Several
of the optimizations that affect the baseline evaluation results in
$\mathbf{RE\\#}$ are applicable also to the NonBacktracking engine of .NET.

#### Contributions

In summary, we consider the following as the main contributions of this paper:

  * $\checkmark$

A new symbolic derivative based nonbacktracking matching algorithm for regular
expression matching that supports _intersection_ , _complement_ and
_lookarounds_ in regexes, with correctness theorem, while preserving _input
linear_ performance (Section 4).

  * $\checkmark$

Explanation of the key techniques used in the implementation of
$\mathbf{RE\\#}$ (Section 5).

  * $\checkmark$

Extensive evaluation using a popular benchmarking tool that ranks
$\mathbf{RE\\#}$ as fastest among all regex matchers today. All the evaluation
results are explained in detail. (Section 6).

We start with some motivating examples for the extended operators that
demonstrate how $\mathbf{RE\\#}$ can be used to match patterns that are
currently either very difficult or infeasible to express with standard regular
expressions.

##  2\. Motivating Examples

In this section we explain the intuition behind the _intersection_ (&) and
_complement_ (~) operators in $\mathbf{RE\\#}$ and illustrate their use
through some examples. The examples are also available in the accompanying web
application (Varatalu, 2024) and are written essentially in .NET regex syntax,
with the addition of & and ~, as well as the _wildcard_ _* that matches _all
strings_ , equivalently represented by (.|\n)*, where dot denotes all
characters _except_ the newline character (\n).

Table 1. Basic constructs and their meaning in the extended regex syntax in $\mathbf{RE\\#}$.  Lookarounds | Prefixes/Suffixes | Other
---|---|---
$\texttt{(?<=}R\texttt{)}\texttt{\\_{*}}$ : |  preceded by $R$ |  $R\texttt{\\_{*}}$ : |  starts with $R$ |  $\texttt{\\_{*}}R\texttt{\\_{*}}$ : |  contains $R$
$\texttt{(?<!}R\texttt{)}\texttt{\\_{*}}$ : |  not preceded by $R$ |  $\texttt{\char 126\relax}(R\texttt{\\_{*}})$ : |  does not start with $R$ |  $\texttt{\char 126\relax}(\texttt{\\_{*}}R\texttt{\\_{*}})$ : |  does not contain $R$
$\texttt{\\_{*}}\texttt{(?=}R\texttt{)}$ : |  followed by $R$ |  $\texttt{\\_{*}}R$ : | ends with R |  $R\texttt{|}S$ : |  either $R$ or $S$
$\texttt{\\_{*}}\texttt{(?!}R\texttt{)}$ : |  not followed by $R$ |  $\texttt{\char 126\relax}(\texttt{\\_{*}}R)$ : |  does not end with $R$ |  $R\texttt{\&}S$ : |  both $R$ and $S$
Table 2. Real-world constraints expressed as regexes in $\mathbf{RE\\#}$. Real-world constraint | Regex equivalent | Notes
---|---|---
a line with an email |<EMAIL_ADDRESS>|  $\texttt{\char 94\relax{}}\stackrel{{\scriptstyle\textsc{\raisebox{-0.94496pt}{\tiny{def}}}}}{{=}}\texttt{(?<=}\texttt{\char 92\relax A}\texttt{|}\texttt{\char 92\relax n}\texttt{)}$ and $\texttt{\char 36\relax{}}\stackrel{{\scriptstyle\textsc{\raisebox{-0.94496pt}{\tiny{def}}}}}{{=}}\texttt{(?=}\texttt{\char 92\relax z}\texttt{|}\texttt{\char 92\relax n}\texttt{)}$
in the Valid section |  (?<=Valid~(_*Invalid_*))_* |  see Example 2.1
without a subdomain | $.\texttt{*}{}@\texttt{\char 126\relax}\texttt{(}\texttt{(}\texttt{\\_{*}}\texttt{\char 92\relax}.\texttt{\\_{*}}\texttt{)}\texttt{\\{}2\texttt{\\}}\texttt{)}$ |  domain not containing two dots (\\.)
not from @other.com |<EMAIL_ADDRESS>|  match not ending with @other.com

The full syntax and semantics is explained in detail in Section 4. The overall
intuition is, first of all, that matching of a regex $R$ is relative to a
_substring_ of the input string. In particular, the wildcard _* matches all
substrings of any input. For example, if the string is " HelloWorld\n" then
the regex (?<=\s)_*(?=\s) matches only "HelloWorld" in it, because it is the
only substring surrounded by white space characters. The regex e_*(?=\s)
matches the substring "elloWorld", while _*e_*(?=\s) matches the substring "
HelloWorld".

For the upcoming examples, consult Table 1 for intuition on how to interpret
the various constructs.

###### Example 2.1 (Context-aware matching).

Consider the input text in the first column below

\--- Valid<EMAIL_ADDRESS><EMAIL_ADDRESS><EMAIL_ADDRESS>\--- Invalid<EMAIL_ADDRESS>email<EMAIL_ADDRESS>|  \--- Valid<EMAIL_ADDRESS><EMAIL_ADDRESS><EMAIL_ADDRESS>\--- Invalid<EMAIL_ADDRESS>email<EMAIL_ADDRESS>\--- Valid \--- Invalid |  \--- Valid<EMAIL_ADDRESS><EMAIL_ADDRESS><EMAIL_ADDRESS>\--- Invalid<EMAIL_ADDRESS>email<EMAIL_ADDRESS>\--- Valid \--- Invalid
---|---|---

which contains a list of valid email addresses and invalid email addresses.
Our goal is not to _validate_ the email addresses themselves, but to _extract_
all the email addresses from the Valid section.

Finding the email addresses is easy, it is all lines that contain @ which is
expressed by the regex<EMAIL_ADDRESS>and since name and domain parts must be non-
empty, we can refine the regex to<EMAIL_ADDRESS>
The Valid section requirement is more difficult, as we need a mechanism to
distinguish between the two sections. This is where lookarounds come in handy.
We can use a lookbehind to match the Valid section, and a lookahead to match
the Invalid section, this ensures that the matches are between the two
sections, using the regex (?<=Valid_*).+@.+(?=_*Invalid).

However, this regex has a problem. If the input contains multiple Valid
sections, the lookbehind will match the first Valid section and the lookahead
will match the last Invalid section, as highlighted in the middle column
above. But we want to match only the entries in Valid sections.

What we need is a way to define a window that starts with the Valid section
and ends with the Invalid section. This is where _complement_ comes in handy.
What we really want to match is expressed with the regex
<EMAIL_ADDRESS>– the lookbehind requires
$u{\cdot}$Valid${\cdot}v$ for some $u$ and $v$ to occur before the match while
prohibits Invalid from occurring in $v$.

We do not need the lookahead because the existence of the Valid section is
enough to ensure that the match is in the Valid section. The complement then
ensures that the Invalid section has not started yet, which works even if the
Invalid section does not exist, which is exactly what we want, as highlighted
by the matches of this regex in the third column above. $\boxtimes$

###### Example 2.2 (Separation of concerns).

What if we have more requirements for the email addresses? What if we want to
exclude email addresses that contain a subdomain. What if we want to exclude
emails from the other.com domain? In real-world applications, it is common to
have multiple requirements for a match, and it is important to be able to
express these requirements in a concise, maintainable way. All of these
requirements can be expressed as regex constraints, as shown in Table 2 where
^ and $ are called _line anchors_. The precise specification of what we want
to match in this example is the following intersection of individual
constraints:

$\underbrace{\texttt{(\char<EMAIL_ADDRESS>36\relax{})}}_{\textit{single
line}}\texttt{\&}\underbrace{\texttt{($\texttt{(?<=}\texttt{Valid}\texttt{\char
126\relax}\texttt{(}\texttt{\\_{*}}{}\texttt{Invalid}\texttt{\\_{*}}{}\texttt{)}\texttt{)}\texttt{\\_{*}}{}$)}}_{\textit{occurs
in the {Valid}
section}}\texttt{\&}\underbrace{\texttt{($.\texttt{*}{}@\texttt{\char
126\relax}\texttt{((}\texttt{\\_{*}}\texttt{\char
92\relax}.\texttt{\\_{*}}\texttt{)}\texttt{\\{2\\}}\texttt{)}$)}}_{\textit{without
a subdomain}}\texttt{\&}\underbrace{\texttt{($\texttt{\char
126\relax}\texttt{(}\texttt{\\_{*}}{}@\texttt{other.com}\texttt{)}$)}}_{\textit{not
from {other.com} domain}}$

This regex is easy to read and understand in individual components, and can be
easily modified to add or remove requirements. The only match for it in the
Example 2.1 text is<EMAIL_ADDRESS>$\boxtimes$

###### Example 2.3 (Extended expressivity but not at the cost of performance).

In industrial applications, regexes with unbounded lookarounds such as
<EMAIL_ADDRESS>do not exist for a reason. Unbounded lookbehinds are not
supported by many popular backtracking regex engines, such as PCRE and even
the ones that do support them, such as .NET, cannot match them with good
performance because the engine has to repeatedly backtrack for the context
conditions for every potential match. This reduces the impact of having such
features available, as the performance is too poor to make it feasible for use
in practice.

This is where $\mathbf{RE\\#}$ shines. It is able to match extended regexes
not only in linear time, but with performance that is comparable to industrial
automata based engines, such as RE2, Hyperscan, and Rust. This is due to the
fact that $\mathbf{RE\\#}$ is internally also automata based and does not
backtrack.

The addition of intersection and complement does not increase the complexity
of the matching algorithm relative to the input – the overall complexity of
the engine remains _input-linear_. This includes not only lookarounds but
allows also for more advanced constructs shown in Table 3.

Table 3. Advanced constructs in the extended regex syntax of $\mathbf{RE\\#}$. | Regex | Notes
---|---|---
Difference | $L\nrightarrow R$ |  $L$ but not $R$ (same as $L\texttt{\&}\texttt{\char 126\relax}{}R$)
Implies (Negated Difference) | $L\rightarrow{}R$ |  if $L$ then $R$ (same as $\texttt{\char 126\relax}{}L\texttt{|}R$)
XOR (Symmetric Difference) | $L\oplus R$ |  exactly one of $L$, $R$ (same as $L\texttt{\&}\texttt{\char 126\relax}{}R\texttt{|}\texttt{\char 126\relax}{}L\texttt{\&}R$)
XNOR (Neg. Symm. Diff.) | $L\odot R$ |  both or none of $L$, $R$ (same as $L\texttt{\&}R\texttt{|}\texttt{\char 126\relax}{}L\texttt{\&}\texttt{\char 126\relax}{}R$)
Window | $\texttt{(?<=}L\texttt{\char 126\relax}\texttt{(}\texttt{\\_{*}}{}R\texttt{\\_{*}}{}\texttt{)}\texttt{)}\texttt{\\_{*}}{}$ |  in a window starting with $L$ but not past $R$
Between | $\texttt{(?<=}L\texttt{)}\texttt{\char 126\relax}\texttt{(}\texttt{\\_{*}}{}\texttt{$L${|}$R$}\texttt{\\_{*}}{}\texttt{)}\texttt{(?=}R\texttt{)}$ |  between $L$ and $R$ without crossing boundaries

Furthermore, lookbehind assertions for context such as the ones shown in
Example 2.1 can be used to find not just the first match, but _all matches_ in
linear time, which is due to the fact that the engine is able to locate all
the matches in a single pass over the input string. Note that certain
combinations of regexes and inputs can still have an all-matches search
complexity of $O(n^{2})$ in regex engines that are otherwise guaranteed to be
linear for a single match. Scenarios illustrating this are shown in Sections
6.1.4 and 6.2.6.

Since other engines do not support lookbehinds with complement, we are using
the regex pattern<EMAIL_ADDRESS>to illustrate this scenario in Figure
2, where a new section is known to start with the dash (-) character, which is
not used anywhere else in the input.

The input is similar to the one used in Example 2.1, but here the $x$ axis
shows the number of lines with email addresses that the Valid and Invalid
sections contain, and the $y$ axis shows how many times the engine is slower
than $\mathbf{RE\\#}$ that has a constant throughput in all cases.

Figure 2. All matches in _linear_ time in resharp ($\mathbf{RE\\#}$). Both
axes are logarithmic.

$\boxtimes$

We now proceed to establish the theory for regular expressions extended with
lookarounds, complement and intersection. We first recall some background
material.

##  3\. Preliminaries

Here we introduce the notation and main concepts used in the paper. The
general meta-notation and notation for denoting strings and locations follows
(Moseley et al., 2023) but differs in some minor aspects. We write
$\textit{lhs}\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}\textit{rhs}$
to let lhs be _equal by definition_ to rhs. Let
$\mathbb{B}=\\{\mathbf{false},\mathbf{true}\\}$ denote Boolean values, let
$\langle{x,y}\rangle$ stand for pairs with
$\langle{x,y}\rangle_{1}\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}x$
and
$\langle{x,y}\rangle_{2}\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}y$.

Let $\Sigma$ be a domain of _characters_ and let $\Sigma^{*}$ denote the set
of all strings over $\Sigma$. We write $\epsilon$ for the empty string. The
length of $s\in\Sigma^{*}$ is denoted by $|s|$. Strings of length one are
treated as characters. Let $i$ and $l$ be nonnegative integers such that
$i+l\leq|s|$. Then $s_{i,l}$ denotes the substring of $s$ starting from index
$i$ having length $l$, where the first character has index 0. In particular
$s_{i,0}=\epsilon$. For $0\leq i<|s|$ let
$s_{i}\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}s_{i,1}$
and let
$s_{|s|}\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}\epsilon$.
E.g.,
$\textrm{"}\texttt{abcdef}\textrm{"}_{1,4}=\textrm{"}\texttt{bcde}\textrm{"}$
and $\textrm{"}\texttt{abcde}\textrm{"}_{5}=\epsilon$.

We let $s^{r}\\!$ denote the _reverse_ of $s$, i.e.,
$s^{r}\\!_{i}=s_{|s|-1-i}$ for $0\leq i<|s|$.

Let $s\in\Sigma^{*}$. A _location in $s$_ is a pair
$s{[}i{]}\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}\langle{s,i}\rangle$,
where $0\leq i\leq|s|$, where $s{[}0{]}$ is called _initial_ and $s{[}|s|{]}$
_final_. The set of all locations in $s$ is $\mathbf{Loc}_{s}$ and
$\mathbf{Loc}\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}\bigcup_{s\in\Sigma^{*}}\mathbf{Loc}_{s}$.
$\mathbf{Loc}^{+}$ stands for all the _nonfinal_ locations. For
$s{[}i{]}\in\mathbf{Loc}^{+}$ let
$s{[}i{]}+1\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}s{[}i+1{]}$.
Let also
$\mathit{hd}(s{[}i{]})\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}s_{i}$,
i.e., if $x$ is nonfinal then $\mathit{hd}(x)$ is the next(current) character
of the location.

The _reverse_ $s{[}i{]}^{r}\\!$ of a location $s{[}i{]}$ in $s$ is the
location $s^{r}\\!{[}|s|{-}i{]}$ in $s^{r}\\!$. For example, the reverse of
the final location in $s$ is the initial location in $s^{r}\\!$.

##### Effective Boolean Algebra

The tuple $\mathcal{A}=(\Sigma,\Psi,[[\\_]],\bot,\top,\vee,\wedge,\neg)$ is
called an _Effective Boolean Algebra over $\Sigma$_ or _EBA_ (D’Antoni and
Veanes, 2021) where $\Psi$ is a set of _predicates_ that is closed under the
Boolean connectives; $[[\\_]]:\Psi\rightarrow 2^{\Sigma}$ is a _denotation
function_ ; $\bot,\top\in\Psi$; $[[\bot]]=\emptyset$, $[[\top]]=\Sigma$, and
for all $\varphi,\psi\in\Psi$, $[[\varphi\vee\psi]]=[[\varphi]]\cup[[\psi]]$,
$[[\varphi\wedge\psi]]=[[\varphi]]\cap[[\psi]]$, and
$[[\neg\varphi]]=\Sigma\setminus[[\varphi]]$. Two predicates $\phi$ and $\psi$
are _equivalent_ when $[[\phi]]=[[\psi]]$, denoted by $\phi\equiv\psi$. If
$\varphi\nequiv\bot$ then $\varphi$ is _satisfiable_.

In examples $\Sigma$ stands for the standard 16-bit character set of Unicode
(also known as the _Basic Multilingual Plane_ or _Plane 0_) and use the .NET
syntax (Microsoft, 2021b) of regular expression character classes. E.g., \w
denotes all the _word-letters_ , $[[\texttt{\char 92\relax
W}]]=[[\lnot\texttt{\char 92\relax w}]]$, [0-9] denotes all the _Latin
numerals_ , \d denotes all the _decimal digits_ , and
$[[\texttt{.}]]=[[\lnot\texttt{\char 92\relax n}]]$ (i.e., all characters
other than the newline character).111Note that in .NET
$[[\texttt{[0-9]}]]\subsetneq[[\texttt{\char 92\relax d}]]$ while for example
in _JavaScript_ $[[\texttt{[0-9]}]]=[[\texttt{\char 92\relax d}]]$. $\top$
corresponds in $\mathbf{RE\\#}$ to [\s\S] and $\bot$ corresponds to [0-[0]].

##  4\. Regexes with Lookarounds and Location Derivatives

Here we formally define regexes supported in $\mathbf{RE\\#}$. Regexes are
defined modulo a character theory
$\mathcal{A}=(\Sigma,\Psi,[[\\_]],\bot,\texttt{$\top$},\vee,\wedge,\neg)$ that
we illustrate with standard (.NET Regex) character classes in examples while
the actual representation of character classes in $\Psi$ is immaterial and
$\Sigma$ may even be _infinite_. $\mathcal{A}$ that is used for character
classes in .NET is a _$K$ -bit bitvector algebra_ (Moseley et al., 2023,
Section 5.1) using _mintermization_ for compression. In most cases $K\leq 64$
and $\Psi$ represents predicates using unsigned 64-bit integers or UInt64
where all the Boolean operations are essentially $O(1)$ operations: bitwise-
AND, bitwise-OR, and bitwise-NOT, with $\bot=0$. Here
$\texttt{\\_{*}}\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}\texttt{$\top$}\texttt{*}$.

After the definition of $\mathbf{RE\\#}$ regexes we define their match
semantics, that is based on pairs of locations called _spans_ – the intuition
is that a span $\langle{s{[}i{]},s{[}j{]}}\rangle$, where $i\leq j$, provides
a match in $s$ where the matching substring is $s_{i,j-i}$. Thereafter we
formally define _derivatives_ for $\mathbf{RE\\#}$, develop the main matching
algorithm for $\mathbf{RE\\#}$ and prove its correctness and input linearity.
Some of the results use theorems in (Zhuchko et al., 2024) of the more general
theory $\mathbf{ERE_{\leq}}$ that we define first.

###  4.1. Full Class $\mathbf{ERE_{\leq}}$ of Regexes

The class $\mathbf{ERE_{\leq}}$ of regexes is defined as follows. Members of
$\mathbf{ERE_{\leq}}$ are denoted here by $\mathbf{R}$. _Concatenation_
(${\cdot}$) is often implicit by juxtaposition. All operators appear in order
of precedence where _union_ (|) binds weakest and _complement_ (~) binds
strongest. Let $\psi\in\Psi$ and let $m$ be a positive integer.

$\displaystyle\mathbf{R}$ $\displaystyle::=$
$\displaystyle\psi{\;\mid\;}\mbox{$\varepsilon$}{\;\mid\;}\mathbf{R}_{1}\texttt{|}\mathbf{R}_{2}{\;\mid\;}\mathbf{R}_{1}\texttt{\&}\mathbf{R}_{2}{\;\mid\;}\mathbf{R}_{1}{\cdot}\mathbf{R}_{2}{\;\mid\;}\mathbf{R}\texttt{\\{}m\texttt{\\}}{\;\mid\;}\mathbf{R}\texttt{*}{\;\mid\;}\texttt{\char
126\relax}\mathbf{R}{\;\mid\;}\texttt{(?<=}\mathbf{R}\texttt{)}{\;\mid\;}\texttt{(?<!}\mathbf{R}\texttt{)}{\;\mid\;}\texttt{(?=}\mathbf{R}\texttt{)}{\;\mid\;}\texttt{(?!}\mathbf{R}\texttt{)}$

We also write `()` for the _empty word_ regex $\varepsilon$. The regex
denoting _nothing_ is just the predicate $\bot$. We let
$\mathbf{R}\texttt{\\{}0\texttt{\\}}\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}\mbox{$\varepsilon$}$
for convenience. In reality also
$\mathbf{R}\texttt{\\{}1\texttt{\\}}\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}\mathbf{R}$.
We write $R\texttt{+}$ for $R{\cdot}R\texttt{*}$.

The regexes $\texttt{(?=}\mathbf{R}\texttt{)}$,
$\texttt{(?!}\mathbf{R}\texttt{)}$, $\texttt{(?<=}\mathbf{R}\texttt{)}$, and
$\texttt{(?<!}\mathbf{R}\texttt{)}$ are called _lookarounds_ ;
$\texttt{(?=}\mathbf{R}\texttt{)}$ is _(positive) lookahead_ ,
$\texttt{(?!}\mathbf{R}\texttt{)}$ is _negative lookahead_ ,
$\texttt{(?<=}\mathbf{R}\texttt{)}$ is _(positive) lookbehind_ , and
$\texttt{(?<!}\mathbf{R}\texttt{)}$ is _negative lookbehind_. In the context
of $\mathbf{ERE_{\leq}}$ let $\texttt{\char 92\relax
A}\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}\texttt{(?<!}\texttt{$\top$}\texttt{)}$
and $\texttt{\char 92\relax
z}\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}\texttt{(?!}\texttt{$\top$}\texttt{)}$.

###  4.2. Regexes Supported in $\mathbf{RE\\#}$

$\begin{array}[]{<EMAIL_ADDRESS>\includegraphics[scale={0.5}]{figs/RE.pdf}\\\\[-10.00002pt] \end{array}$

Figure 3. ${\mbox{$\mathbf{RE\\#}$}}\subsetneq{\mbox{$\mathbf{ERE_{\leq}}$}}$

Here we introduce the abstract syntax of regular expressions $R$ that are
supported by $\mathbf{RE\\#}$ that we also denote by $\mathbf{RE\\#}$. First,
regexes _without lookarounds_ are below denoted by $E$ and the corresponding
subclass is denoted by $\mathbf{ERE}$. Regexes $R$ then extend $E$ with
lookarounds and are closed under intersection. Let $\mathbf{RE}$ stand for the
_standard_ subset of $\mathbf{ERE}$ without ~ and &.

$\begin{array}[]{@{}c@{\;\;}c@{\;\;}l@{}}E&::=&\texttt{\char 92\relax
A}{\;\;\mid\;\;}\texttt{\char 92\relax
z}{\;\;\mid\;\;}\psi{\;\;\mid\;\;}\mbox{$\varepsilon$}{\;\;\mid\;\;}E_{1}\texttt{|}E_{2}{\;\;\mid\;\;}E_{1}\texttt{\&}E_{2}{\;\;\mid\;\;}E_{1}{\cdot}E_{2}{\;\;\mid\;\;}E\texttt{\\{}m\texttt{\\}}{\;\;\mid\;\;}E\texttt{*}{\;\;\mid\;\;}\texttt{\char
126\relax}E\\\\[1.99997pt]
R&::=&E{\;\;\mid\;\;}R_{1}\texttt{\&}R_{2}{\;\;\mid\;\;}\texttt{(?<=}E\texttt{)}{\cdot}R{\;\;\mid\;\;}\texttt{(?<!}E\texttt{)}{\cdot}R{\;\;\mid\;\;}R{\cdot}\texttt{(?=}E\texttt{)}{\;\;\mid\;\;}R{\cdot}\texttt{(?!}E\texttt{)}\end{array}$

The regex \A is called the _start anchor_ and \z is called the _end anchor_.
While all other standard anchors supported in .NET are also supported in the
concrete syntax of $\mathbf{RE\\#}$, they are defined via lookarounds and
(currently) disallowed in $\mathbf{ERE}$. For example, the _line anchors_ `^`
and `$` are defined in Table 2. The presence of \A and \z as _primitive_
regexes in $\mathbf{ERE}$ is used in the proof of Theorem 1.

Let also
$E\texttt{\\{}m{,n}\texttt{\\}}\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}E\texttt{\\{}m\texttt{\\}}{{\cdot}}(E{\texttt{|}}\mbox{$\varepsilon$})\texttt{\\{}n-m\texttt{\\}}$,
where $0\leq m\leq n$, as the _bounded loop_ with _lower bound_ $m$ and _upper
bound_ $n$. In fact, the implementation in $\mathbf{RE\\#}$ uses
$E\texttt{\\{}m{,n}\texttt{\\}}$ as the _core_ construct, where $m=0$ is an
important special case during rewrites, and
$E\texttt{\\{}m\texttt{\\}}\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}E\texttt{\\{}m{,m}\texttt{\\}}$
and
$E\texttt{*}\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}E\texttt{\\{}0{,\infty}\texttt{\\}}$.

The core intuition of the difference between $\mathbf{ERE_{\leq}}$ and
$\mathbf{RE\\#}$ lies in that in $\mathbf{RE\\#}$ lookbacks are only allowed
to match context _before_ the actual match and lookaheads _after_ it.
Intersection can be used to express behavior similar to lookarounds _within_ a
match. For example, the regex `(?=.*[a-z])\w*` turns into `.*[a-z].*&\w*` –
the _password filter_ example in the introduction is similar.

###  4.3. Match Semantics

The match semantics of regexes in $\mathbf{ERE_{\leq}}$ uses _spans_. A _span_
in a string $s$ is formally a pair of locations
$\theta=\langle{s{[}i{]},s{[}j{]}}\rangle$ where $i\leq j$; the _width_ of
$\theta$ is
$0pt{\theta}\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}j-i$.
We call $\theta_{1}$ the _start location of $\theta$_ and $\theta_{2}$ the
_end location of $\theta$_. If $0pt{\theta}=0$ then $\theta_{1}=\theta_{2}$ is
also called the _location of $\theta$_. The set of all spans in $s$ is denoted
by $\mathbf{Span}(s)$ and
$\mathbf{Span}\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}\bigcup_{s\in\Sigma^{*}}\mathbf{Span}(s)$.
For all $\theta\in\mathbf{Span}$ and $R\in\mbox{$\mathbf{ERE_{\leq}}$}$,
_$\theta$ is a match of $R$_ or _$\theta$ models $R$_ is denoted by
$\theta\models R$:

$\begin{array}[]{@{}r@{\,}c@{\,}l@{\;\;}c@{\;\;}l@{}}\theta&\models&\mbox{$\varepsilon$}&\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}&0pt{\theta}\,{=}\,0\\\
\theta&\models&\psi&\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}&0pt{\theta}\,{=}\,1\mathrel{\mathbf{and}}\mathit{hd}(\theta_{1})\in[[\psi]]\\\
\theta&\models&L\texttt{|}R&\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}&\theta\,{\models}\,L\mathrel{\mathbf{or}}\theta\,{\models}\,R\\\
\theta&\models&L\texttt{\&}R&\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}&\theta\,{\models}\,L\mathrel{\mathbf{and}}\theta\,{\models}\,R\\\
\theta&\models&\texttt{\char
126\relax}R&\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}&\theta\not\models
R\\\
\theta&\models&R\texttt{*}&\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}&\exists\,m\geq
0:\theta\,{\models}\,R\texttt{\\{}m\texttt{\\}}\end{array}\;\begin{array}[]{@{}r@{\,}c@{\,}l@{\;\;}c@{\;\;}l@{}}\theta&\models&L{\cdot}R&\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}&\exists\,x:\langle{\theta_{1},x}\rangle\,{\models}\,L\mathrel{\mathbf{and}}\langle{x,\theta_{2}}\rangle\,{\models}\,R\\\
\quad\theta&\models&R\texttt{\\{}m\texttt{\\}}&\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}&\exists\,x:\langle{\theta_{1},x}\rangle\,{\models}\,R\mathrel{\mathbf{and}}\langle{x,\theta_{2}}\rangle\,{\models}\,R\texttt{\\{}m{-}1\texttt{\\}}\\\
\theta&\models&{\texttt{(?=}R\texttt{)}}&\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}&0pt{\theta}\,{=}\,0\mathrel{\mathbf{and}}\exists\,x:\langle{\theta_{1},x}\rangle\,{\models}\,R\\\
\theta&\models&{\texttt{(?!}R\texttt{)}}&\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}&0pt{\theta}\,{=}\,0\mathrel{\mathbf{and}}\nexists\,x:\langle{\theta_{1},x}\rangle\,{\models}\,R\\\
\theta&\models&{\texttt{(?<=}R\texttt{)}}&\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}&0pt{\theta}\,{=}\,0\mathrel{\mathbf{and}}\exists\,x:\langle{x,\theta_{2}}\rangle\,{\models}\,R\\\
\theta&\models&{\texttt{(?<!}R\texttt{)}}&\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}&0pt{\theta}\,{=}\,0\mathrel{\mathbf{and}}\nexists\,x:\langle{x,\theta_{2}}\rangle\,{\models}\,R\end{array}$

Intuitively, $\theta\models\texttt{(?=}R\texttt{)}$ means that there exists a
match of $R$ _starting_ from the location of $\theta$, and
$\theta\models\texttt{(?<=}R\texttt{)}$ means that there exists a match of $R$
_ending_ in the location of $\theta$. For any _location_ $x$, we write
$x\models R$ for $\langle{x,x}\rangle\models R$. For the $\mathbf{ERE}$
anchors \A and \z above we have thus that

$x\models\texttt{\char 92\relax
A}\boldsymbol{\Leftrightarrow}\textit{Initial}(x)\qquad x\models\texttt{\char
92\relax z}\boldsymbol{\Leftrightarrow}\textit{Final}(x)$

Let $B$ be a (positive) lookbehind and let $A$ be a (positive) lookahead. Then
it follows via the match semantics of concatenation that

$\theta\models B{\cdot}R\boldsymbol{\Leftrightarrow}\theta_{1}\models
B\mathrel{\mathbf{and}}\theta\models R\qquad\theta\models
R{\cdot}A\boldsymbol{\Leftrightarrow}\theta_{2}\models
A\mathrel{\mathbf{and}}\theta\models R$

###### Example 4.1.

Consider the first part (?<=author.*).* of the author search regex from the
introduction. Then $\theta\models\texttt{(?<=author.*).*}$ implies that
$\theta_{1}\models{\texttt{(?<=author.*)}}$ and $\theta\models{\texttt{.*}}$.
So the _start_ location $\theta_{1}$ of the match must be after the string
"author" and the matched substring itself must be on a single line (recall
that $[[\texttt{.}]]=\Sigma\setminus\\{\texttt{\char 92\relax n}\\}$).
$\boxtimes$

###### Example 4.2.

As a simple but nontrivial example of various negations, we compare the regex
(?<!\w) with the regex $\texttt{(?<=}\lnot\texttt{\char 92\relax w}\texttt{)}$
(or (?<=\W)). Let $s=\texttt{"a@b"}$. Then
$s{[}0{]}\models\texttt{(?<!}\texttt{\char 92\relax w}\texttt{)}$ because no
word-letter precedes the initial location, but
$s{[}0{]}\not\models\texttt{(?<=}\lnot\texttt{\char 92\relax w}\texttt{)}$
because no non-word-letter precedes the initial location. On the other hand
both $s{[}2{]}\models\texttt{(?<!}\texttt{\char 92\relax w}\texttt{)}$ and
$s{[}2{]}\models\texttt{(?<=}\lnot\texttt{\char 92\relax w}\texttt{)}$.
$\boxtimes$

For $R\in\mbox{$\mathbf{ERE_{\leq}}$}$ let
$\mathcal{M}(R)\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}\\{\theta\in\mathbf{Span}\mid\theta\models
R\\}$ and for $R,S\in\mbox{$\mathbf{ERE_{\leq}}$}$, $R\equiv
S\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}\mathcal{M}(R)=\mathcal{M}(S)$.
The implementation in $\mathbf{RE\\#}$ uses the following key property for
normalisation of regexes in $\mathbf{RE\\#}$. It also shows the key role that
the start and end anchors play. We call the below normal form of
$R\in\mbox{$\mathbf{RE\\#}$}$ the _Lookaround Normal Form_ of $R$ and denote
it by $\mathbf{LNF}(R)$ and the LNF of $\mathbf{RE\\#}$ by
$\mathbf{LNF}(\mbox{$\mathbf{RE\\#}$})$. Construction of $\mathbf{LNF}(R)$ is
itself linear in the size of $R$.

###### Theorem 1 (LNF).

For all $R\in\mbox{$\mathbf{RE\\#}$}$ there exist
$A,B,E\in\mbox{$\mathbf{ERE}$}$ such that
$R\equiv\texttt{(?<=}B\texttt{)}{\cdot}E{\cdot}\texttt{(?=}A\texttt{)}$.

###### Proof.

First, by using (Zhuchko et al., 2024, Theorem 5), for all
$S\in\mbox{$\mathbf{ERE_{\leq}}$}$,
$\texttt{(?!}S\texttt{)}\equiv\texttt{(?=}\texttt{\char
126\relax}\texttt{(}S{\cdot}\texttt{\\_{*}}\texttt{)}{\cdot}\texttt{\char
92\relax z}\texttt{)}$ and
$\texttt{(?<!}S\texttt{)}\equiv\texttt{(?<=}\texttt{\char 92\relax
A}{\cdot}\texttt{\char
126\relax}\texttt{(}\texttt{\\_{*}}{\cdot}S\texttt{)}\texttt{)}$. If $S$ is in
$\mathbf{ERE}$ then so are $\texttt{\char
126\relax}\texttt{(}S{\cdot}\texttt{\\_{*}}\texttt{)}{\cdot}\texttt{\char
92\relax z}$ and $\texttt{\char 92\relax A}{\cdot}\texttt{\char
126\relax}\texttt{(}\texttt{\\_{*}}{\cdot}S\texttt{)}$. _We thus replace all
the negative lookarounds by positive ones in $R$._

Any concatenation of two lookaheads
$\texttt{(?=}A_{1}\texttt{)}{\cdot}\texttt{(?=}A_{2}\texttt{)}$ is in
$\mathbf{ERE_{\leq}}$ equivalent to the single lookahead
$\texttt{(?=}(A_{1}{\cdot}\texttt{\\_{*}})\texttt{\&}(A_{2}{\cdot}\texttt{\\_{*}})\texttt{)}$
where if $A_{1},A_{2}\in\mbox{$\mathbf{ERE}$}$ then so is
$(A_{1}{\cdot}\texttt{\\_{*}})\texttt{\&}(A_{2}{\cdot}\texttt{\\_{*}})$.
Analogously, for the case of lookbehinds,
$\texttt{(?<=}B_{1}\texttt{)}{\cdot}\texttt{(?<=}B_{2}\texttt{)}\equiv\texttt{(?<=}(\texttt{\\_{*}}{\cdot}B_{1})\texttt{\&}(\texttt{\\_{*}}{\cdot}B_{2})\texttt{)}$.

Any intersection
$\texttt{(?<=}B_{1}\texttt{)}{\cdot}E_{1}{\cdot}\texttt{(?=}A_{1}\texttt{)}\texttt{\&}\texttt{(?<=}B_{2}\texttt{)}{\cdot}E_{2}{\cdot}\texttt{(?=}A_{2}\texttt{)}$
is in $\mathbf{ERE_{\leq}}$ equivalent to the intersection
$\texttt{(?<=}B_{1}\texttt{)}{\cdot}\texttt{(?<=}B_{2}\texttt{)}{\cdot}(E_{1}\texttt{\&}E_{2}){\cdot}\texttt{(?=}A_{1}\texttt{)}{\cdot}\texttt{(?=}A_{2}\texttt{)}$
because, according to the formal semantics,

$\displaystyle\langle{x,y}\rangle\models\texttt{(?<=}B_{1}\texttt{)}{\cdot}E_{1}{\cdot}\texttt{(?=}A_{1}\texttt{)}\texttt{\&}\texttt{(?<=}B_{2}\texttt{)}{\cdot}E_{2}{\cdot}\texttt{(?=}A_{2}\texttt{)}$
$\displaystyle\boldsymbol{\Leftrightarrow}\langle{x,y}\rangle{\models}\texttt{(?<=}B_{1}\texttt{)}{\cdot}E_{1}{\cdot}\texttt{(?=}A_{1}\texttt{)}\mathrel{\mathbf{and}}\langle{x,y}\rangle{\models}\texttt{(?<=}B_{2}\texttt{)}{\cdot}E_{2}{\cdot}\texttt{(?=}A_{2}\texttt{)}$
$\displaystyle\boldsymbol{\Leftrightarrow}x{\models}\texttt{(?<=}B_{1}\texttt{)}\mathrel{\mathbf{and}}\langle{x,y}\rangle{\models}E_{1}\mathrel{\mathbf{and}}y{\models}\texttt{(?=}A_{1}\texttt{)}\mathrel{\mathbf{and}}x{\models}\texttt{(?<=}B_{2}\texttt{)}\mathrel{\mathbf{and}}\langle{x,y}\rangle{\models}E_{2}\mathrel{\mathbf{and}}y{\models}\texttt{(?=}A_{2}\texttt{)}$
$\displaystyle\boldsymbol{\Leftrightarrow}x{\models}\texttt{(?<=}B_{1}\texttt{)}{{\cdot}}\texttt{(?<=}B_{2}\texttt{)}\mathrel{\mathbf{and}}\langle{x,y}\rangle{\models}E_{1}\texttt{\&}E_{2}\mathrel{\mathbf{and}}y{\models}\texttt{(?=}A_{1}\texttt{)}{{\cdot}}\texttt{(?=}A_{2}\texttt{)}$

We thus arrive at the lookaround normal form, by applying these rewrites. ∎

###### Example 4.3.

Consider the author search regex from the introduction where the word border
\b _before_ \w corresponds to the negative lookback (?<!\w) and \b _after_ \w
corresponds to the negative lookahead (?!\w). After normalization the negative
lookarounds have been replaced by the equivalent positive ones:

$\underbrace{\texttt{(?<=}\texttt{\\_{*}}\texttt{author.*}\texttt{\&}\texttt{\\_{*}}\texttt{{\char
92\relax A}\char 126\relax($\texttt{$\top$}${*}{\char 92\relax
w})}\texttt{)}}_{\textit{lookbehind}}{\cdot}\underbrace{\texttt{(}\texttt{.*}\texttt{\&}\texttt{\char
126\relax(.*and.*)}\texttt{\&}\texttt{\char 92\relax
w}\texttt{.*}\texttt{\char 92\relax w}\texttt{)}}_{\textit{main
pattern}}{\cdot}\underbrace{\texttt{(?=\char 126\relax({\char 92\relax
w}$\texttt{\\_{*}}$){\char 92\relax z})}}_{\textit{lookahead}}$

This regex is pretty much humanly unreadable and is only intended for internal
processing by the matcher. Among several other simplifications, an immediate
simplification that is applied here is that $\texttt{(?=\char
126\relax($\psi\texttt{\\_{*}}$){\char 92\relax
z})}\equiv\texttt{(?=$\lnot\psi${|}{\char 92\relax z})}$ for all $\psi\in\Psi$
that gets rid of ~ and _*. $\boxtimes$

###  4.4. Reversal

Reversal of $R\in\mbox{$\mathbf{ERE_{\leq}}$}$, denoted by $R^{r}\\!$, is
defined as follows:

$\begin{array}[]{r@{\;}c@{\;}l}\psi^{r}\\!&\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}&\psi\\\
\mbox{$\varepsilon$}^{r}\\!&\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}&\mbox{$\varepsilon$}\\\
R\texttt{*}^{r}\\!&\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}&R^{r}\\!\texttt{*}\end{array}\quad\begin{array}[]{r@{\;}c@{\;}l}(R\texttt{|}S)^{r}\\!&\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}&R^{r}\\!\texttt{|}S^{r}\\!\\\
(R\texttt{\&}S)^{r}\\!&\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}&R^{r}\\!\texttt{\&}S^{r}\\!\\\
(\texttt{\char
126\relax}R)^{r}\\!&\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}&\texttt{\char
126\relax}(R^{r}\\!)\end{array}\quad\begin{array}[]{r@{\;}c@{\;}l}(R{\cdot}S)^{r}\\!&\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}&S^{r}\\!{\cdot}R^{r}\\!\\\
R\texttt{\\{}m\texttt{\\}}^{r}\\!&\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}&R^{r}\\!\texttt{\\{}m\texttt{\\}}\\\
\texttt{(?=}R\texttt{)}^{r}\\!&\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}&\texttt{(?<=}R^{r}\\!\texttt{)}\end{array}\quad\begin{array}[]{r@{\;}c@{\;}l}\texttt{(?<=}R\texttt{)}^{r}\\!&\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}&\texttt{(?=}R^{r}\\!\texttt{)}\\\
\texttt{(?!}R\texttt{)}^{r}\\!&\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}&\texttt{(?<!}R^{r}\\!\texttt{)}\\\
\texttt{(?<!}R\texttt{)}^{r}\\!&\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}&\texttt{(?!}R^{r}\\!\texttt{)}\end{array}$

Reversal is used in the definition of the top-level matching algorithm, and is
therefore a critical operation of the overall framework. It follows by
induction over regexes that reversal is both size-preserving and involutive:
$(R^{r}\\!)^{r}\\!=R$.

The reverse of a span $\theta\in\mathbf{Span}$ is defined as the span
$\theta^{r}\\!\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}\langle{(\theta_{2})^{r}\\!,(\theta_{1})^{r}\\!}\rangle$,
that is also an involutive and width-preserving operation. It follows also
that
$\theta\in\mathbf{Span}(s)\boldsymbol{\Leftrightarrow}\theta^{r}\\!\in\mathbf{Span}(s^{r}\\!)$.
We make use of the following theorem that has also been formally proved
correct (Zhuchko et al., 2024, Theorem 1) in the _Lean_ proof assistant.
Observe also that $\mathbf{RE\\#}$ is _closed under reversal_.

###### Theorem 2 (Reversal).

$\forall\,R\in\mbox{$\mathbf{ERE_{\leq}}$},\theta\in\mathbf{Span}:\theta\models
R\boldsymbol{\Leftrightarrow}\theta^{r}\\!\models R^{r}\\!$.

###  4.5. Nullability

Here we define _nullability_ of regexes $R\in{\mbox{$\mathbf{ERE}$}}$. The
definition is more-or-less standard with one key difference concering the two
anchors. In terms of the span based match semantics, $R$ being _always_
nullable means that $R$ is equivalent to $R|\mbox{$\varepsilon$}$ and thus
$x\models R$ for all locations $x$, i.e., that $R$ matches the empty word in
any context. Let $x$ be any location and let $\psi\in\Psi$.

$\begin{array}[]{r@{\;\;}c@{\;\;}l}\mathit{Null}_{x}(R\texttt{|}S)&\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}&\mathit{Null}_{x}(R)\mathrel{\mathbf{or}}\mathit{Null}_{x}(S)\\\
\mathit{Null}_{x}(R\texttt{\&}S)&\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}&\mathit{Null}_{x}(R)\mathrel{\mathbf{and}}\mathit{Null}_{x}(S)\\\
\mathit{Null}_{x}(R{\cdot}S)&\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}&\mathit{Null}_{x}(R)\mathrel{\mathbf{and}}\mathit{Null}_{x}(S)\\\
\mathit{Null}_{x}(R\texttt{\\{}m\texttt{\\}})&\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}&\mathit{Null}_{x}(R)\\\
\mathit{Null}_{x}(\texttt{\char
126\relax}R)&\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}&\mathrel{\mathbf{not}}\,\mathit{Null}_{x}(R)\end{array}\quad\begin{array}[]{r@{\;\;}c@{\;\;}l}\mathit{Null}_{x}(\texttt{\char
92\relax
A})&\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}&\textit{Initial}(x)\\\
\mathit{Null}_{x}(\texttt{\char 92\relax
z})&\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}&\textit{Final}(x)\\\
\mathit{Null}_{x}(\mbox{$\varepsilon$})&\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}&\mathbf{true}\\\
\mathit{Null}_{x}(R\texttt{*})&\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}&\mathbf{true}\\\
\mathit{Null}_{x}(\psi)&\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}&\mathbf{false}\end{array}$

If a regex $R$ in a lookaround $\texttt{(?=}R\texttt{)}$ or
$\texttt{(?<=}R\texttt{)}$ is always nullable then the lookaround is
simplified to $\varepsilon$. Such nullability status is maintained with each
regex AST node at construction time. For example, the regex `\n\z|\z` is only
nullable in a _final_ location. The lookahead `(?=\n\z|\z)` corresponds to the
\Z anchor in .NET and is also supported in the concrete syntax of
$\mathbf{RE\\#}$.

###  4.6. Derivatives in $\mathbf{ERE}$

Here we first define _derivatives_ of regexes in $\mathbf{ERE}$. This
definition is also more-or-less standard. Let $x\in\mathbf{Loc}^{+}$ be a
_nonfinal_ location, in which case we know that $\mathit{hd}(x)\in\Sigma$. For
example, if $s=\textrm{"}\texttt{ab}\textrm{"}$ then the nonfinal locations in
$s$ are $s{[}0{]}$ and $s{[}1{]}$. Let $\psi\in\Psi$, let
$\diamond\in\\{\texttt{\&},\texttt{|}\\}$, and let
$\textrm{\scriptsize\faAnchor}\in\\{\texttt{\char 92\relax A},\texttt{\char
92\relax z}\\}$.

$\begin{array}[]{@{}rcl@{}}\boldsymbol{\delta}_{x}(\textrm{\scriptsize\faAnchor})&\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}&\bot\\\
\boldsymbol{\delta}_{x}(\mbox{$\varepsilon$})&\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}&\bot\\\
\boldsymbol{\delta}_{x}(R\diamond
S)&\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}&\boldsymbol{\delta}_{x}(R)\diamond\boldsymbol{\delta}_{x}(S)\\\
\boldsymbol{\delta}_{x}(\texttt{\char
126\relax}R)&\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}&\texttt{\char
126\relax}\boldsymbol{\delta}_{x}(R)\\\
\boldsymbol{\delta}_{x}(R\texttt{*})&\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}&\boldsymbol{\delta}_{x}(R){\cdot}R\texttt{*}\\\
\end{array}\quad\begin{array}[]{@{}rcl@{}}\boldsymbol{\delta}_{x}(R\texttt{\\{}m\texttt{\\}})&\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}&\boldsymbol{\delta}_{x}(R){\cdot}R\texttt{\\{}m-1\texttt{\\}}\\\\[1.99997pt]
\boldsymbol{\delta}_{x}(\psi)&\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}&\left\\{\begin{array}[]{@{}l@{\;}l}\mbox{$\varepsilon$},&\textbf{if}\,\mathit{hd}(x)\in[[\psi]];\\\
\bot,&\mathbf{otherwise}.\end{array}\right.\\\\[10.00002pt]
\boldsymbol{\delta}_{x}(R{\cdot}S)&\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}&\left\\{\begin{array}[]{@{}l@{\;}l}\boldsymbol{\delta}_{x}(R){\cdot}S\texttt{|}\boldsymbol{\delta}_{x}(S),&\textbf{if}\,\mathit{Null}_{x}(R)=\mathbf{true};\\\
\boldsymbol{\delta}_{x}(R){\cdot}S,&\mathbf{otherwise}.\end{array}\right.\end{array}$

There is one aspect of this definition that deserves attention as it differs
from derivatives of bounded loops in (Moseley et al., 2023) where
$\boldsymbol{\delta}_{x}(R{\cdot}R)$ is not always equivalent to
$\boldsymbol{\delta}_{x}(R){\cdot}R$ when $R$ is not always nullable. One
culprit is the _word border_ anchor \b that is (currently) not allowed in
$\mathbf{ERE}$ but is in $\mathbf{RE\\#}$ defined via lookarounds. In general,
$\boldsymbol{\delta}_{x}(R{\cdot}R)$ and $\boldsymbol{\delta}_{x}(R){\cdot}R$
are always equivalent in $\mathbf{RE\\#}$.

##### Derivation Relation

The _derivation relation_
$x\,{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}\,y$ between locations $x,y\in\mathbf{Loc}$ and regexes
$R\in\mbox{$\mathbf{ERE}$}$ is used to reason about consequitive derivative
steps. The derivation relation combines steps so that, e.g.,
$x\,{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}\,x$ and
$x\,{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}\,x{+}2$ means that
$\boldsymbol{\delta}_{x+1}(\boldsymbol{\delta}_{x}(R))$ is nullable in
location $x{+}2$.

$x\,{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}\,y\quad\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}\quad\mathit{Null}_{x}(R)\mathrel{\mathbf{and}}x=y\;\;\mathrel{\mathbf{or}}\;\;\textit{Nonfinal}(x)\mathrel{\mathbf{and}}x{+}1\,{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{@{}c@{}}\boldsymbol{\delta}_{x}(R)\\\\[-2.79996pt]
\end{array}}$}}\,y$

###  4.7. Adding Lookarounds

Here we consider $\mathbf{LNF}(\mbox{$\mathbf{RE\\#}$})$. Let
$R=\texttt{(?<=}B\texttt{)}{\cdot}E{\cdot}\texttt{(?=}A\texttt{)}$ where
$A,B,E\in\mbox{$\mathbf{ERE}$}$. We are first interested in finding the
_latest_ end location of a match of $R$, we replace $\texttt{(?<=}B\texttt{)}$
with $\texttt{\\_{*}}{\cdot}B$. Say $D=\texttt{\\_{*}}{\cdot}B{\cdot}E$.

The general derivative rule for concatenation in Section 4.6 remains unchanged
for concatenation in $D{{\cdot}}\texttt{(?=}A\texttt{)}$ where it uses the
derivative rule for lookaheads as defined below. The basic insight for
lookaheads is the fact that if $\texttt{(?=}A\texttt{)}$ was reached there was
a nullable location after matching the regex $D$ before it. In order to recall
the _offsets_ to those locations, lookaheads are _annotated_ as
$\texttt{(?=}A\texttt{)}_{I}$ where $I$ is a set of offsets and
$\texttt{(?=}A\texttt{)}=\texttt{(?=}A\texttt{)}_{\\{0\\}}$ where $0$ is the
immediate offset.

The derivative rule for lookahead is as follows, where $A$ is treated as
$\varepsilon$ when nullable, and recall that
$\boldsymbol{\delta}_{x}(\mbox{$\varepsilon$})=\bot$. We also let
$\texttt{(?=}\bot\texttt{)}_{I}\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}\bot$
and
$\texttt{(?=}A\texttt{)}_{I}\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}\mbox{$\varepsilon_{I}$}$
when $A$ is nullable, where $\varepsilon_{I}$ is $\varepsilon$ annotated with
$I$. Let
$I+1\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}\\{i+1\mid
i\in I\\}$.

$\boldsymbol{\delta}_{x}(\texttt{(?=}A\texttt{)}_{I})\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}\left\\{\begin{array}[]{@{}l@{\;}l}\bot,&\textbf{if}\,\mathit{Null}_{x}(A);\\\
\texttt{(?=}\boldsymbol{\delta}_{x}(A)\texttt{)}_{I+1},&\mathbf{otherwise}.\end{array}\right.$

Then $\texttt{(?=}A\texttt{)}_{I}\texttt{|}\texttt{(?=}A\texttt{)}_{J}$ is
always rewritten to $\texttt{(?=}A\texttt{)}_{I\cup J}$. So
$\mbox{$\varepsilon_{I}$}\texttt{|}\mbox{$\varepsilon_{J}$}=\mbox{$\varepsilon_{I\cup
J}$}$. Also
$\mbox{$\varepsilon_{I}$}{\cdot}\mbox{$\varepsilon_{J}$}=\mbox{$\varepsilon_{I\cup
J}$}$.

###### Example 4.4.

Consider the regex \d+(?=:-) that looks for a price in a text and let
$s=\texttt{"50:- "}$. Then $\boldsymbol{\delta}_{s{[}0{]}}(\texttt{\char
92\relax d}\texttt{+}\texttt{(?=}\texttt{:-}\texttt{)})=\texttt{\char 92\relax
d}\texttt{*}\texttt{(?=}\texttt{:-}\texttt{)}$ and
$\boldsymbol{\delta}_{s{[}1{]}}(\texttt{\char 92\relax
d}\texttt{*}\texttt{(?=}\texttt{:-}\texttt{)})=\texttt{\char 92\relax
d}\texttt{*}\texttt{(?=}\texttt{:-}\texttt{)}$ since the lookahead did not
kick in yet. Then we get $\boldsymbol{\delta}_{s{[}2{]}}(\texttt{\char
92\relax
d}\texttt{*}\texttt{(?=}\texttt{:-}\texttt{)})=\texttt{(?=}\boldsymbol{\delta}_{s{[}2{]}}(\texttt{:-})\texttt{)}_{\\{1\\}}=\texttt{(?=}\texttt{-}\texttt{)}_{\\{1\\}}$
and finally that
$\boldsymbol{\delta}_{s{[}3{]}}(\texttt{(?=}\texttt{-}\texttt{)}_{\\{1\\}})=\texttt{(?=}\mbox{$\varepsilon$}\texttt{)}_{\\{2\\}}=\mbox{$\varepsilon_{\\{2\\}}$}$
in location $s{[}4{]}$, so the match end is $s{[}4-2{]}$. $\boxtimes$

####  4.7.1. Implementation of Lookahead Annotations

The set $I$ above is represented by a pair $\langle{k,X}\rangle$ containing a
_relative offset_ $k$ and an index set $X$ so that $I$ denotes $\\{k+i\mid
i\in X\\}$ and
$I+1\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}\langle{k+1,X}\rangle$;
a specialized union $I\cup J$ is also implemented that adjusts the result to
the lowest relative offset.

For purposes of DFA state caching, the sets $I$ are only ever compared with
pointer equality and there is a builder to keep track of unique set instances.
This makes several orders of magnitude difference in the memory footprint and
construction time. In practice, the sets $I$ are usually sparse which allows
the lookahead context to be hundreds or even thousands of characters long
without contributing significantly to state space.

The complete set $I$ is needed in the generalized algorithm for finding _all_
matches. In the case when only the _first_ match is searched, $I$ is only ever
needed to maintain the _minimal_ offset in it and in this case becomes just
that offset. Then, e.g.,
$\texttt{(?=}A\texttt{)}_{I}\texttt{|}\texttt{(?=}A\texttt{)}_{J}$ rewrites to
$\texttt{(?=}A\texttt{)}_{\min(I,J)}$.

###  4.8. Latest Match End

We consider again regexes in $\mathbf{RE\\#}$ in the normal form described
earlier and focus on the simplified and transformed case
$R=\texttt{\\_{*}}{\cdot}B{\cdot}E\texttt{(?=}A\texttt{)}$ where
$A,B,E\in\mbox{$\mathbf{ERE}$}$. We search for $j$ such that

$s{[}0{]}\,{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}\,s{[}j{]}\,{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}\,s{[}|s|{]}$

and want to find the _maximal_ $j$ if it exists. To this end we use the
function $\mathit{MaxEnd}(s{[}i{]},R,m)$ below where $s{[}i{]}$ is the
_current location_ and $m$ is the _maximal match end so far_. We let
$\mbox{$\varepsilon_{I}$}\in R$ denote the epsilon with the annotations that
exists (implicitly) in $R$, e.g.,
$\mbox{$\varepsilon_{\\{0,5\\}}$}\in\texttt{a}\texttt{*}\texttt{|}\mbox{$\varepsilon_{\\{5\\}}$}$
because a* contains $\varepsilon$ implicitly. Initially $m=-1$ and the search
starts from the initial location. We first consider any _nonfinal_ location
$s{[}i{]}$, i.e., $i<|s|$.

$\mathit{MaxEnd}(s{[}i{]},R,m)\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}\left\\{\begin{array}[]{ll}m,&\textbf{if}\,R=\bot;\\\
\mathit{MaxEnd}(s{[}i+1{]},\boldsymbol{\delta}_{s{[}i{]}}(R),\max(m,i-\min(I))),&\textbf{else}\,\textbf{if}\,\mbox{$\varepsilon_{I}$}\in
R;\\\
\mathit{MaxEnd}(s{[}i+1{]},\boldsymbol{\delta}_{s{[}i{]}}(R),m),&\mathbf{otherwise}.\end{array}\right.$

The latest match end so far becomes $\max(m,i-k)$ where $k=\min(I)$ is the
minimal offset from the current index $i$ to where a valid match of $E$ ended
when
$s{[}i-k{]}\,{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}\,s{[}i{]}$. In particular if $m=-1$ then $i-k$ is the _first_
match end that was found. Later search may reveal other match ends (including
both earlier and later ones) but only the latest one is remembered here.

We now consider the case of the final location in $s$. In the following let
$R^{\texttt{\char 92\relax z}\mapsto\mbox{$\varepsilon$}}$ stand for $R$ where
\z is replaced by $\varepsilon$. In particular, any lookahead
$\texttt{(?=}A\texttt{)}_{I}$ such that $A^{\texttt{\char 92\relax
z}\mapsto\mbox{$\varepsilon$}}$ is nullable is now automatically rewritten to
$\texttt{(?=}\mbox{$\varepsilon$}\texttt{)}_{I}\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}\mbox{$\varepsilon_{I}$}$.

$\mathit{MaxEnd}(s{[}|s|{]},R,m)\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}\left\\{\begin{array}[]{ll}{\max(m,|s|-\min(I))},&\textbf{if}\,\mbox{$\varepsilon_{I}$}\in
R^{\texttt{\char 92\relax z}\mapsto\mbox{$\varepsilon$}};\\\
m,&\mathbf{otherwise}.\end{array}\right.$

For example if $R=\texttt{\char 92\relax
z}\texttt{|}\texttt{(?=}\texttt{a}\texttt{*}\texttt{\char 92\relax
z}\texttt{)}_{\\{5\\}}$ then $R^{\texttt{\char 92\relax
z}\mapsto\mbox{$\varepsilon$}}=\mbox{$\varepsilon$}\texttt{|}\mbox{$\varepsilon_{\\{5\\}}$}=\mbox{$\varepsilon_{\\{0,5\\}}$}$
and thus $\max(m,|s|-0)=|s|$.

The following lemma is key in establishing the formal relationship between the
derivation relation for $\mathbf{RE\\#}$ and the formal match semantics. It
makes fundamental use of the theory of derivatives of $\mathbf{ERE_{\leq}}$
that has recently been fully formalized and proved correct (Zhuchko et al.,
2024) using the _Lean_ proof assistant. The general derivative theory
developed for $\mathbf{ERE_{\leq}}$ is highly _nonlinear_ for use in practice
but subsumes $\mathbf{RE\\#}$, which enables us to apply the main correctness
result of $\mathbf{ERE_{\leq}}$ relating the general theory of derivatives in
$\mathbf{ERE_{\leq}}$ with the formal match semantics.

###### Lemma 1.

Let $s{[}i_{0}{]}\in\mathbf{Loc}$ and
$R\in\mathbf{LNF}(\mbox{$\mathbf{RE\\#}$})$, and let
$\mathit{MaxEnd}(s{[}i_{0}{]},R,-1)=j$. Then

  1. (1)

$j=-1$ $\boldsymbol{\Leftrightarrow}$ $\nexists\,\imath\geq
i_{0},\jmath:\langle{s{[}\imath{]},s{[}\jmath{]}}\rangle\models R$.

  2. (2)

If $j\geq 0$ then $j$ is the maximal $\jmath$ such that $\exists\,\imath\geq
i_{0}:\langle{s{[}\imath{]},s{[}\jmath{]}}\rangle\models R$.

###### Proof Outline.

Consider $i_{0}=0$ and let
$R=\texttt{(?<=}B\texttt{)}E\texttt{(?=}A\texttt{)}$ where
$A,B,E\in\mbox{$\mathbf{ERE}$}$. First observe that when
$\boldsymbol{\delta}_{s{[}\jmath{]}}(\texttt{(?=}A\texttt{)})$ is invoked it
is when
$s{[}0{]}\,{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}\,s{[}\jmath{]}$. This follows because
$\texttt{(?<=}B\texttt{)}$ is replaced by $\texttt{\\_{*}}{\cdot}B$ and
$\mathit{MaxEnd}$ just iterates derivatives from one location to the next.
From this point forward the offsets after taking each derivative are
increased. For the current location $s{[}i{]}$ and
$\texttt{(?=}D\texttt{)}_{I}$ where $D$ has been derived from $A$ we know that
the latest _candidate_ match exists at index $i-\min(I)$. $\mathit{MaxEnd}$
then keeps track of the latest _valid_ match end index when $D$ is nullable.
So $\mathit{MaxEnd}(s{[}0{]},R,-1)$ returns the latest such index or -1 if
there is none. The final location is handled separately which is the only
location where \z is equivalent to $\varepsilon$.

We now use the fact that $\mathbf{RE\\#}$ is a fragment of
$\mathbf{ERE_{\leq}}$ and that the derivative rules for $\mathbf{ERE}$ are the
same as in $\mathbf{ERE_{\leq}}$. We use (Zhuchko et al., 2024, Theorem 2)
(say $\dagger$)

$\begin{array}[]{r@{\;}c@{\;}l}\exists\,\imath:\langle{s{[}\imath{]},s{[}\jmath{]}}\rangle\models
R&\boldsymbol{\Leftrightarrow}&\exists\,\imath:s{[}\imath{]}\models\texttt{(?<=}B\texttt{)}\mathrel{\mathbf{and}}\langle{s{[}\imath{]},s{[}\jmath{]}}\rangle\models
E\mathrel{\mathbf{and}}{s{[}\jmath{]}}\models\texttt{(?=}A\texttt{)}\\\
&\stackrel{{\scriptstyle\dagger}}{{\boldsymbol{\Leftrightarrow}}}&\exists\,\imath:s{[}0{]}\,{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}\,s{[}\imath{]}\,{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}\,s{[}\jmath{]}\,{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}\,s{[}|s|{]}\stackrel{{\scriptstyle\dagger}}{{\boldsymbol{\Leftrightarrow}}}s{[}0{]}\,{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}\,s{[}\jmath{]}\,{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}\,s{[}|s|{]}\end{array}$

This completes the proof because $\mathit{MaxEnd}$ returns the maximal such
$\jmath$ iff it exists or else $-1$. ∎

###  4.9. Leftmost-Longest Match Algorithm

We now describe the main match algorithm in $\mathbf{RE\\#}$. It uses reversal
and the $\mathit{MaxEnd}$ algorithm above in two directions to compute the
match such that the so called POSIX semantics holds. What is unique about this
algorithm is that _in the general case_ described below it traverses the input
string in _reverse_ in the first phase in order to find the earliest or
leftmost start index. We describe the algorithm for
$R=\texttt{(?<=}B\texttt{)}{\cdot}E{\cdot}\texttt{(?=}A\texttt{)}$ as follows.

$\begin{array}[]{l@{\;}c@{\;}l}\textrm{$\mathit{LLMatch}$}{}(s,R)&\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}&\textbf{let}\,k=\mathit{MaxEnd}(s^{r}\\!{[}0{]},R^{r}\\!,-1)\,\textbf{in}\\\
&&\quad\textbf{if}\;k=-1\;\textbf{then}\;\textbf{return}\,\lightning\;\textbf{else}\\\
&&\quad\quad\textbf{let}\,i=|s|-k;j=\mathit{MaxEnd}(s{[}i{]},E{\cdot}\texttt{(?=}A\texttt{)},-1)\,\textbf{in}\\\
&&\quad\quad\quad\textbf{return}\,\langle{s{[}i{]},s{[}j{]}}\rangle\end{array}$

###### Theorem 3 (LLMatch).

$\textrm{$\mathit{LLMatch}$}{}(s,R)$ returns $\lightning$ if there exists no
match of $R$ in $s$ else returns the match $\langle{s{[}i{]},s{[}j{]}}\rangle$
of $R$ where $i$ is minimal and $j$ is maximal for $i$.

###### Proof.

Let $R=\texttt{(?<=}B\texttt{)}{\cdot}E{\cdot}\texttt{(?=}A\texttt{)}$. Then
$R^{r}\\!=\texttt{(?<=}A^{r}\\!\texttt{)}{\cdot}E^{r}\\!{\cdot}\texttt{(?=}B^{r}\\!\texttt{)}$.
Let $k=\mathit{MaxEnd}(s^{r}\\!{[}0{]},R^{r}\\!,-1)$. If $k=-1$ then, by Lemma
1(1), $\nexists\theta\in\mathbf{Span}(s^{r}\\!):\theta\models R^{r}\\!$ and,
by Theorem 2, $\nexists\theta\in\mathbf{Span}(s):\theta\models R$.

Assume $k\geq 0$. Then, by Lemma 1(2), $k$ is the _maximal_ index such that
$\exists\,x:\langle{x,s^{r}\\!{[}k{]}}\rangle\models R^{r}\\!$. So, by Theorem
2, $i=|s|-k$ is the _minimal_ index such that
$\exists\,x:\langle{s{[}i{]},x}\rangle\models R$. (Recall that
$s^{r}\\!{[}k{]}^{r}\\!=s{[}|s|-k{]}$.) Thus, $i$ is the minimal index such
that

$\exists\,x:{s{[}i{]}}\models\texttt{(?<=}B\texttt{)}\mathrel{\mathbf{and}}\langle{s{[}i{]},x}\rangle\models
E\mathrel{\mathbf{and}}x\models\texttt{(?=}A\texttt{)}$

In particular, it follows that $\exists\,x:\langle{s{[}i{]},x}\rangle\models
E{\cdot}\texttt{(?=}A\texttt{)}$. Now, by using Lemma 1(2) again, it follows
that that $j=\mathit{MaxEnd}(s{[}i{]},E{\cdot}\texttt{(?=}A\texttt{)},-1)$ is
the maximal index such that $\langle{s{[}i{]},s{[}j{]}}\rangle\models R$. ∎

In the implementation of $\mathit{LLMatch}$ for a _single_ POSIX match search
as descibed above, the sets $I$ in $\texttt{(?=}A\texttt{)}_{I}$ are
implemented by only keeping their _minimal_ elements – then $I\cup
J=\min(I,J)$. This does not affect any of the statements above, because only
the minimal element is ever used above but the more general formulation is
needed in Section 4.9.1.

###### Theorem 4 (InputLinearity).

The complexity of $\textrm{$\mathit{LLMatch}$}{}(s,R)$ is linear in $|s|$.

###### Proof.

The main search algorithm runs twice over the input $s$. The regexes reached by reading the symbols from $s$ are internalized and cached as states in a DFA with $q_{0}=R$ as the initial state and $\boldsymbol{\delta}_{a}(q)$ as the transition function of the DFA, where the operators | and & are treated as associative, commutative and idempotent operators, which results in a finite state space whose size is independent of $|s|$. The offset annotation $I$ maintained in $\texttt{(?=}A\texttt{)}_{I}$ is incremented linearly up to the point when $A$ becomes nullable and where $\texttt{(?=}A\texttt{)}_{I}\texttt{|}\texttt{(?=}A\texttt{)}_{J}=\texttt{(?=}A\texttt{)}_{\min(I,J)}$. ∎

All nonbacktracking engines are in principle input linear for a single match
search and internally maintain some form of DFA. When the number of DFA states
grows too large they fall back in an NFA mode. Such a fallback mechanism is
currently not supported in $\mathbf{RE\\#}$ but can be implemented by working
with a generalized form of Antimirov derivatives (Antimirov, 1996).

The $\mathbf{RE\\#}$ engine capitalizes on the fact that the symbolic
derivative based automata construction is small and independent of the
alphabet size, but the state space can still grow exponentially with respect
to the size of the regex in the worst case. For the most critical use cases,
we provide the option to precompile the regex into a _complete DFA_ up front.
This allows for extremely fast matching at the cost of a potentially large
memory footprint, which can be known ahead of time.

####  4.9.1. Finding All Nonoverlapping Leftmost-Longest Matches

The key algorithm $\mathit{MaxEnd}$ above is generalized in $\mathbf{RE\\#}$
into an algorithm $\mathit{AllEnds}$ that produces _all_ match ends as
follows. We then discuss more informally how $\mathit{AllEnds}$ is used in the
general match algorithm in $\mathbf{RE\\#}$ to locate all nonoverlapping POSIX
matches. Similar to $\mathit{MaxEnd}$ the algorithm takes a regex
$R=\texttt{(?<=}B\texttt{)}{\cdot}E{\cdot}\texttt{(?=}A\texttt{)}\in\mathbf{LNF}(\mbox{$\mathbf{RE\\#}$})$
and a start location $s{[}i{]}$ but in this case a _set_ $M$ of _match end
indices found so far_. We consider only the case of $i<|s|$ with the case
$i=|s|$ being analogous to above.

$\mathit{AllEnds}(s{[}i{]},R,M)\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}\left\\{\begin{array}[]{ll}M,&\textbf{if}\,R=\bot;\\\
\mathit{AllEnds}(s{[}i+1{]},\boldsymbol{\delta}_{s{[}i{]}}(R),M\cup
i-J),&\textbf{else}\,\textbf{if}\,\mbox{$\varepsilon_{J}$}\in R;\\\
\mathit{AllEnds}(s{[}i+1{]},\boldsymbol{\delta}_{s{[}i{]}}(R),M),&\mathbf{otherwise}.\end{array}\right.$

where
$i-J\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}\\{i-\jmath\mid\jmath\in
J\\}$. Let
$\mathit{MaxEnd}(x,R)\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}\mathit{MaxEnd}(x,R,-1)$.
Thus
$\mathit{MaxEnd}(s{[}0{]},R)=\max(\mathit{AllEnds}(s{[}0{]},R,\emptyset))$,
provided that
$\max(\emptyset)\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}-1$
here, where _all_ match ends, including the maximal one, are collected in $M$.

If we now first compute
$I=|s|-\mathit{AllEnds}(s^{r}\\!{[}0{]},R^{r}\\!,\emptyset)$ then it holds,
similarly to case above, that $I$ contains _all the start indices_ $i$ such
that $s{[}i{]}\models\texttt{(?<=}B\texttt{)}$ and
$\exists\,j:\langle{s{[}i{]},s{[}j{]}}\rangle\models
E{\cdot}\texttt{(?=}A\texttt{)}$.

Starting with $i=\min(I)$ we compute
$j=\mathit{MaxEnd}(s{[}i{]},E{\cdot}\texttt{(?=}A\texttt{)})$. This gives us
the first POSIX match $\langle{s{[}i{]},s{[}j{]}}\rangle$. We now repeat the
same search from $I:=\\{\imath\in I\mid i<\imath,j\leq\imath\\}$ to ignore
overlapping matches. Observe that $i<\imath$ is necessary to make progress
when $j=i$.

This concludes our high-level overview of the main matching algorithm
$\mathit{LLMatches}(s,R)$ in $\mathbf{RE\\#}$. The implementation of
$\mathit{LLMatches}(s,R)$ is not linear, but may in the worst case be
quadratic in $|s|$. However, our extensive evaluation does consistently
indicate linear behavior, even for the _quadratic_ benchmark (see Section
6.1.4).

###### Example 4.5.

Let $R=\texttt{b+(?=c)}$ and $s=\texttt{"aaaaabcababbc"}$. Then initially

$I=|s|-\mathit{AllEnds}(\texttt{"cbbabacbaaaaa"}{[}0{]},\texttt{{(?<=}c{)}b+},\emptyset)=13-\\{2,3,8\\}=\\{5,10,11\\}$

The first match starts from $5$ and ends at
$\mathit{MaxEnd}(s{[}5{]},\texttt{b+(?=c)})=6$. This leaves $I:=\\{10,11\\}$.
The next match starts from $10$ and ends at
$\mathit{MaxEnd}(s{[}10{]},\texttt{b+(?=c)})=12$. This leaves $I:=\emptyset$
and concludes the search. Thus
$\mathit{LLMatches}(s,R)=\\{\langle{s{[}5{]},s{[}6{]}}\rangle,\langle{s{[}10{]},s{[}12{]}}\rangle\\}$.
$\boxtimes$

##  5\. Implementation

Here we give a brief overview of the implementation of the engine along with
some key optimizations and performance considerations. At the high level,
derivatives are computed lazily and cached in a DFA with regexes internalized
as states and use the transition function $\boldsymbol{\delta}_{a}(q)$ for
states $q$.

The core parser was taken directly from the .NET runtime, but was modified to
read the symbols & and ~ as intersection and complement respectively. The
parser was also extended to interpret the symbol _ as the set of all
characters, since it is very commonly used in our regexes. Fortunately the
escaped variants \&, \~ and \\_ were not assigned to any regex construct, and
existing regex patterns can be used by escaping these characters.

The parser also supports Unicode symbols for operators
$(\oplus,\odot,\rightarrow,\nrightarrow)$, as explained in Table 3, for more
advanced Boolean operations. Moreover, rather than implementing those
operators through the core Boolean operators, one can add specialized rules.
Derivatives rules for the extended operations are in fact _identical_ as for
$\diamond$ in Section 4.6. Nullability, for example for XOR, can be defined by
$\mathit{Null}_{x}(L\oplus
R)\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}(\mathit{Null}_{x}(L)\neq\mathit{Null}_{x}(R))$,
and analogously for the other operators.

The matching implementation of nearly all industrial regex engines consists of
two separate components: a prefilter and a matcher. The prefilter is essential
to be competitive with other engines, and is used to quickly eliminate non-
matching strings. Our derivative-based approach is used in both components,
which in some cases provides a significant advantage over other engines.

###  5.1. Prefilter

The prefilter is an input-parallel operation on the side that is applied
aggressively. For simple regexes, such as [abc], the prefilter can locate the
entire match in parallel, where the only real-world limitation is availability
of space per parallel operation. For more complex regexes, the prefilter is
used to locate the _prefix_ of the input string that is guaranteed to match
the regex, before the core engine kicks in. In $\mathbf{RE\\#}$ the prefilter
is using vectorized bitwise operations, which are very efficient on modern
CPUs. The speedup of processing 64 bytes at a time, e.g., using AVX512
instructions, is significant and immediately visible in the overall
performance.

It is important to note that, unlike in many other engines, the prefilter
optimizations in our engine are not limited to simple regexes, but are applied
to all regexes in a derivative-based manner, including lookarounds, which
makes the extensions very competitive in real-world scenarios. The impact of
this systematic approach to prefilters is shown in Sections 6.2.6 and 6.2.4.

####  5.1.1. Breadth-First Derivative Calculation

Derivatives are used to examine the optimizations available for the regex
pattern. One key optimization is to explore _all_ derivatives symbolically, or
in a _breadth-first_ manner, and bitwise-merge their conditions until reaching
the first successful match. This provides a way to optimize the matching
process with more specialized algorithms.

####  5.1.2. Prefix Search

Often, the entire regex pattern is a single string literal or a set of words.
In such cases, we optimize the matching process by using a dedicated string
matching algorithm. We first check if the regex pattern is a string literal or
a small set (up to 20) of string literals, and if so, we use the _Teddy_ (Qiu
et al., 2021) algorithm, recently supported in .NET9 to locate matches.

###  5.2. Combined Techniques and Inner Loop Vectorization

A key difference from other regex engines is that we do not just use
specialized search algorithms for locating the prefix, but the algoritms are
deeply integrated with the core engine. We combine the search algorithms with
automaton transitions that have been cached from derivatives, which allows us
to use specialized algorithms for the prefix in the input text, and transition
through multiple steps in the automaton right away.

One such example is the regex pattern abcd.*efg, which can be optimized to
match the string literal abcd in the input text and then immediately
transition to the automaton state representing .*efg for the rest of the
match.

We also use the derivatives to perform intermediate prefix computations and
appropriate skipping in inner loop of the match. The breadth-first calculation
of derivatives is used to compute the prefix of the remaining regex, which is
then used to skip over large parts of the input string in a single step, and
only perform the more expensive automaton transitions on the remaining
positions. This means that the rest of the aforementioned pattern .*efg makes
use of input-parallel algorithms as well.

All of the DFA states have pre-computed optimizations during construction,
which are used whenever possible to skip over parts of the input string. A
benchmark scenario illustrating the power of inner-loop optimizations is shown
in Section 6.2.4, where $\mathbf{RE\\#}$ is shown to be significantly faster
on long matching strings than other engines.

However, it is important to note that vectorization is not always beneficial.
For example, even though the AVX512 instruction set can process 64 bytes at a
time, the overhead of setting up the vectorized operations can be significant
for large common character sets, such as [a-zA-Z]. In such cases, the engine
falls back to automaton transitions. Even the Teddy algorithm is not always
beneficial, as it has a certain upper limit (roughly 20) on the number of
strings it can process efficiently, otherwise the engine falls back to
automaton transitions for large alternations as well.

###  5.3. Rewrite Rules and Subsumption

Our system implements a number of regex rewrite rules, which are essential for
the efficiency of the implementation. Figure 4 illustrates the basic rewrite
rules that are always applied when regular expressions are constructed.
Intersection and union are implemented as commutative, associative and
idempotent operators, so changing the order of their arguments does not change
the result.

Each $R\in\mbox{$\mathbf{ERE}$}$ comes with a predicate $\varphi_{R}\in\Psi$
that approximates its relevant characters. The definition is:
$\varphi_{\psi}\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}\psi$,
$\varphi_{\texttt{\char
126\relax}R}\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}\texttt{$\top$}$,
$\varphi_{L\texttt{|}R}=\varphi_{L{\cdot}R}\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}\varphi_{L}\lor\varphi_{R}$,
$\varphi_{L\texttt{\&}R}\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}\varphi_{L}\land\varphi_{R}$,
and
$\varphi_{R\texttt{\\{}m\texttt{\\}}}=\varphi_{R\texttt{*}}\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}\varphi_{R}$.
Also $\varphi_{\mbox{$\varepsilon$}}=\varphi_{\texttt{\char 92\relax
A}}=\varphi_{\texttt{\char 92\relax
z}}\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}\bot$.
All operations of $\mathcal{A}$ are $O(1)$ operations and if
$\varphi\equiv\psi$ then $\varphi=\psi$. For example, the test $\texttt{\char
92\relax n}\notin[[\varphi_{R}]]$ is $\varphi_{\texttt{\char 92\relax
n}}\land\varphi_{R}=\bot$ and the test $[[\phi]]\subseteq[[\psi]]$ is
$\phi\lor\psi=\psi$ in Figure 4.

There are many further derived rules that can be beneficial in reducing the
state space. Unions and intersections are both implemented by sets. If a union
contains a regex $S$, such as a predicate $\psi$, that is trivially subsumed
by another regex $R$, such as $\psi\texttt{*}$, then $S$ is removed from the
union. This is an instance of the loop rule in Figure 4 that rewrites
$\psi\texttt{*}{\texttt{|}}\psi\texttt{\\{}1\texttt{\\}}$ to $\psi\texttt{*}$
(where $\psi\texttt{*}=\psi\texttt{\\{}0{,\infty}\texttt{\\}}$).

A further simplification rule (using $\varphi_{R}$ in Figure 4) for unions is
that if a union contains a regex $\psi\texttt{*}$ and all the other
alternatives only refer to elements from $[[\psi]]$ then the union reduces to
$\psi\texttt{*}$. This rule rewrites any union such as
(${.\texttt{*}}\texttt{ab}.\texttt{*}\texttt{|}.\texttt{*}$) to just
$.\texttt{*}$ (recall that $.\equiv\texttt{[\char 94\relax{\char 92\relax
n}]}$), which significantly reduces the number of alternatives in unions.

$\inferrule{\texttt{\char
126\relax}(\texttt{\\_{*}})}{\bot}\quad\inferrule{\texttt{\char
126\relax}\bot}{\texttt{\\_{*}}}\quad\inferrule{\texttt{\char
126\relax}\texttt{\char 126\relax}R}{R}\quad\inferrule{\texttt{\char
126\relax}\mbox{$\varepsilon$}}{\texttt{$\top$}\texttt{+}}\quad\inferrule{\texttt{\char
126\relax}(\texttt{$\top$}\texttt{+})}{\mbox{$\varepsilon$}}\quad\inferrule{\bot{{\cdot}}R}{\bot}\quad\inferrule{R{{\cdot}}\bot}{\bot}\quad\inferrule{\mbox{$\varepsilon$}{{\cdot}}R}{R}\quad\inferrule{R{{\cdot}}\mbox{$\varepsilon$}}{R}\quad\inferrule{\bot\texttt{*}}{\mbox{$\varepsilon$}}\quad\inferrule{\texttt{\\_{*}}\texttt{|}R}{\texttt{\\_{*}}}\quad\inferrule{\texttt{\\_{*}}\texttt{\&}R}{R}\quad\inferrule{\texttt{(?=}\bot\texttt{)}_{I}}{\bot}$

$\inferrule*[left=loop,right={(l\leq k\leq
m,m\leq\infty)}]{R\texttt{\\{}l{,m}\texttt{\\}}\texttt{|}R\texttt{\\{}k{,n}\texttt{\\}}}{R\texttt{\\{}l{,\max(m,n)}\texttt{\\}}}\quad\inferrule*[right=\texttt{\char
92\relax
n}\notin[[\varphi_{R}]]]{.\texttt{*}\texttt{|}R}{.\texttt{*}}\quad\inferrule*[right=\texttt{\char
92\relax n}\notin[[\varphi_{R}]]]{.\texttt{*}\texttt{\&}R}{R}$

$\quad\inferrule*[left=sub1]{(R1\texttt{\&}R2)\texttt{|}R1}{R1}\quad\inferrule*[left=dedup]{R1\diamond
R2\diamond R1}{R1\diamond
R2}\quad\inferrule*[left=sub2]{(R1\texttt{\&}(R2|R3))\texttt{|}(R1\texttt{\&}R2)}{(R1\texttt{\&}(R2|R3))}$

$\quad\inferrule*{R1R2|R1R3}{R1(R2|R3)}\quad\inferrule*{R1R3|R2R3}{(R1|R2)R3}\quad\inferrule*[right=[[\phi]]\subseteq[[\psi]]]{\phi\texttt{\\{}0{,m}\texttt{\\}}\psi\texttt{*}}{\psi\texttt{*}{}}\quad\inferrule*[right=\mathit{Null}(R)]{\texttt{(?=}R\texttt{)}_{I}}{\mbox{$\varepsilon_{I}$}}$

Figure 4. Basic rewrite rules where $\diamond\in\\{\texttt{|},\texttt{\&}\\}$
and $\phi,\psi\in\Psi$.

###  5.4. Overhead Elimination

To make the engine competitive in scenarios with frequent matches, it is
important to keep the engine as lightweight as possible and to avoid
unnecessary operations. Many optimizations are cached into bit flags, which
are used to quickly determine if a certain operation is necessary. For
example, there is a bit flag for checking if a regex is always nullable, which
is immediately marked as true if the regex accepts the empty string
$\varepsilon$. There is also a specialized flag for anchor nullability, which
is used to quickly determine if an anchor was valid in the previous position.

There are also shortcuts for quickly return $\lightning$ if a dead state is
reached, and for checking if an automaton state has more specialized
algorithms available. We are also extensively using pointer comparisons for
equality checks, e.g. for checking if two regexes are the same, or if a regex
is a subset of another regex.

For match end lookups, as we know the position of the match start, we often
skip a number of transitions in the automaton, e.g. if the regex is abcd.*efg,
we can skip the transitions for abcd entirely and start the match 4 characters
ahead with the transitions for .*efg, which is a significant optimization for
many regexes.

The engine also supports using ASCII bytes as input, which effectively doubles
the speed of vectorized operations, as the engine can process double the
characters per parallel step. We do not use this optimization in any of the
benchmark comparisons, as the UTF-16 input is more mature in .NET and has more
algorithms readily available, but it is a significant optimization for many
real-world scenarios, especially when processing large amounts of data. We are
also planning to support UTF-8 input directly in the future.

When the engine detects no opportunities for more-specialized algorithms and
falls back to automaton transitions, it uses a highly optimized loop, which
does not store any intermediate results, and only uses the automaton
transitions to determine the match end. Additionally, the engine compiles very
small regexes directly into full DFAs, which eliminates a conditional branch
dead center in the hot-path, which would otherwise be used to lazily create
new states.

###  5.5. Pending Nullable Position Representation in Lookahead Annotations

The set of pending match positions is a key component of the engine, and is
used to keep track of context throughout the matches. As the set can grow very
large, it is important to keep the representation and operations on the set
lightweight in terms of memory and CPU usage.

The set is represented as a sorted list of ranges, which is minimized during
construction. One frequent operation is to increment all the positions in the
set, which is done by simply incrementing the start and end of each range.
Contiguous ranges are also merged during this operation, which often results
in a very small memory overhead. For example, a pending match set of 10000
sequential positions can be represented as a single range, which can take up
as little as 8 bytes of memory for int32 positions. This allows the context
length to be very large in practice, and the engine can handle complex regexes
with many lookarounds.

###  5.6. Validating Correctness of $\mathbf{RE\\#}$ Implementation Using
Formalized Lean Semantics

There are many low-level optimizations and rewrite rules in the
$\mathbf{RE\\#}$ engine. For example, for obvious reasons, no input string $s$
is ever actually reversed but $s^{r}\\!$ is an abstraction that hides
underlying index calculations. We use the Lean formalization of
$\mathbf{ERE_{\leq}}$ and its POSIX matching semantics (Zhuchko et al., 2024)
that is _executable_ because the membership test $a\in[[\psi]]$ in
$\mathcal{A}$ is executable. The _span_ universe $\mathbf{Span}$ is in Lean
defined as $\Sigma^{*}\times\Sigma^{*}\times\Sigma^{*}$ with
$\langle{u,v,w}\rangle$ representing $\langle{s{[}i{]},s{[}j{]}}\rangle$ where
$s=u^{r}\\!vw$, $i=|u|$ and $j=|uv|$. Although the semantics in Lean is highly
_nonlinear_ it does have the same semantics for $\mathbf{RE\\#}$ (as
${\mbox{$\mathbf{RE\\#}$}}\subsetneq{\mbox{$\mathbf{ERE_{\leq}}$}}$) and is
the only test oracle available.

The $\mathbf{RE\\#}$ engine was extensively tested with thousands of regexes,
and the results where compared with the expected results according to the Lean
specification. This helped to find numerous bugs throughout the development of
the engine, such as the handling of the edges of the input string and
detecting one-off errors in reversal. One such bug we found during
implementation in the regex ^\n+, which should have matched the full input
string "\n\n", but instead matched only the second \n, because the engine did
not handle the edge of the input string correctly.

##  6\. Evaluation

We have evaluated the performance of our engine on a number of regex
benchmarks, and compared it to other regex engines available in the
_BurntSushi/rebar_ benchmarking tool (Gallant, 2024). The benchmarks are split
into two categories: the baseline comparison (Section 6.1) consists of the
curated regex benchmark suite from the _BurntSushi/rebar_ tool; the extended
comparison (Section 6.2) consists of a set of regexes that are designed to
emphasize the strengths of our engine.

The benchmarks report the throughput of the engine in terms of the number of
bytes processed per second, and the geometric mean ($\mu_{g}$) ratio of the
throughput is used as the primary metric for comparison. Each of the
benchmarks is reported by the ratio of throughput compared to the best
performing engine in the benchmark, where 1x is the leader in each individual
benchmark. The overall $\mu_{g}$ ratio is displayed for each major category,
where the displayed ratio means, e.g., 3x is twice as fast as 6x. Any number
larger than 1x implies that the engine lost some benchmarks in the category.
The results are shown in Figure 5. Below we analyze the results in some
detail.

The measurements were performed on a machine running an Ubuntu 22.04 Docker
image with a AMD Ryzen Threadripper 3960X 24-Core Processor and 128 GB of
memory.

|  $\mu_{g}$ relative slowdown ratio
---|---
Engine |  | Sec
---
6.1
| Sec
---
6.1.1
| Sec
---
6.1.2
| Sec
---
6.1.3
| Sec
---
6.1.4
| Sec
---
6.1.5
resharp | 1.48 | 1.98 | 1.12 | 1.43 | 1.86 | 1
rust/regex | 2.54 | 1.49 | 3.69 | 1.38 | 21.9 | 1.2
hyperscan | 2.76 | 1.69 | 1.76 | 102 | 1 | 2.26
dotnet/comp | 5.29 | 2.7 | 3.71 | 3.77 | 4.52 | 208
pcre2/jit | 7.86 | 3.48 | 2.3 | 615 | 23.6 | 17.6
dotnet/nobt | 9.14 | 5.88 | 6.61 | 27.7 | 42.7 | 3.58
re2 | 12.3 | 11.7 | 5.05 | 16.7 | 39.1 | 25.6
javascript/v8 | 19.5 | 6.26 | 4.78 | 1503 | 25.4 | 140
regress | 50.5 | 23.4 | 5.34 | 3690 | 77.1 | 521
python/re | 65.2 | 40 | 11.6 | 900 | 149 | 599
python/regex | 66.1 | 21.7 | 17 | 4516 | 122 | 800
perl | 74.7 | 41.1 | 44.9 | 2572 | 146 | 20.8
java/hotspot | 77.4 | 86.5 | 9.13 | 3841 | 40.1 | 618
go/regexp | 166 | 237 | 29.5 | 189 | 423 | 997
pcre2 | 285 | 472 | 42.6 | 8519 | 161 | 651
(a) Baseline evaluation (Section 6.1).

|  $\mu_{g}$ relative slowdown ratio
---|---
Engine |  | Sec
---
6.2
| Sec
---
6.2.1
| Sec
---
6.2.2
| Sec
---
6.2.3
| Sec
---
6.2.4
| Sec
---
6.2.5
| Sec
---
6.2.6
resharp | 1.09 | 1 | 1 | 1.09 | 1.02 | 1 | 1.14
hyperscan | 3.77 | 1.08 | 2.14 | 1.79 | 5.85 | - | -
dotnet/nobt | 10.7 | 2.13 | 9.19 | - | 67.4 | 11.6 | -
pcre2/jit | 20 | 23.8 | - | 86.2 | 38.5 | 9.21 | 15.8
rust/regex | 29.5 | 4.16 | 2747 | 7.63 | 20.1 | 82.9 | -
dotnet/comp | 41.3 | 80.9 | 554 | 694 | 7.48 | 25.6 | 5.26
re2 | 48.9 | 175 | 1440 | 28 | 16.5 | - | -
python/regex | 141 | 139 | 1673 | 1196 | 50.7 | 48.3 | 79.6
javascript/v8 | 214 | 86.5 | 449 | 66.9 | - | - | 141
python/re | 233 | 93 | 2005 | 936 | 188 | 62.4 | 135
regress | 360 | 99.6 | 1264 | 749 | - | - | 188
pcre2 | 503 | 2399 | - | 599 | 1076 | 943 | 255
java/hotspot | 698 | 176 | 2597 | 769 | 423 | 56.3 | 718
go/regexp | 957 | 318 | 2733 | 1135 | 763 | - | -
perl | 1143 | 6.32 | 199 | 1310 | 7195 | 2863 | 1189
(b) Extended evaluation (Section 6.2).

Figure 5. Benchmark $\mu_{g}$ slowdown. Top three outcomes in each benchmark
category are indicated in bold.

###  6.1. Baseline Comparison

The baseline comparison is done on the popular curated regex benchmark suite
and using the publicly available _BurntSushi/rebar_ benchmarking tool, from
which we included all benchmarks that our engine supports. There are 27
benchmarks in total. Benchmarks requiring unsupported features, e.g., capture
groups, are excluded from the comparison. Since $\mathbf{RE\\#}$ (resharp)
uses _leftmost-longest_ matching semantics, the match results are carefully
compared with the other engines. The benchmarks also use _earliest_ matching
semantics in the case of Hyperscan. In 25 out of 27 benchmarks, the match
results are _identical_ to _leftmost-greedy_ engines.

The baseline benchmarks are ran “as is”, without any modifications to the
regexes or the input strings. Certain apples-to-apples benchmarks, when
appropriate, are included in the Section 6.2 to display the performance of the
engine in a more controlled environment. The baseline summary geometric mean
of speed ratios is shown in Figure 5(a) _with a separate column for each
benchmark category below as indicated by the column title_.

In the figures dotnet/comp is the Compiled option in .NET and dotnet/nobt is
the NonBacktracking option in .NET. We have omitted the engine version
numbers, but have used the most recent available stable versions in all cases.

####  6.1.1. Literal and Literal-Alternate Categories (10 benchmarks)

The literal category consists of regexes that are simple string literals, and
the literal-alternate category consists of regexes that are simple
alternations of string literals.

These categories are orthogonal to the engine itself, as the performance is
mostly determined by the string matching algorithms used in the engine, and
whether an how well the engine supports the literal optimizations, e.g., those
in Section 5.1.

$\mathbf{RE\\#}$ does not win in either of these categories, see Figure 5(a),
but it is consistently close to the top performer, with the worst performance
being in the literal-alternate ‘sherlock-ru’ benchmark, where the engine is 3x
slower than the best performing engine, rust/regex.

Having more highly optimized 8-bit string literal matching algorithms would be
beneficial to compete in the ASCII categories of this benchmark, but the
engine is still competitive here, and not far off from the top in both
categories. Rust and Hyperscan perform excellent in both of these categories
with their strong string literal optimizations and geometric mean performance
ratio. Hyperscan has a single outlier in the unicode literal ‘sherlock-ru’
benchmark, where it is 10x slower, which brings the geometric mean performance
down to 1.69x.

####  6.1.2. Words and Bounded-Repeat Categories (8 benchmarks)

The words and bounded repeat (or counters) categories consist mostly of
benchmarks that are simple with many short matches, such as \b\w+\b and
[A-Za-z]{8,13}. $\mathbf{RE\\#}$ performs very well in these categories, as do
other automata-based engines. What sets $\mathbf{RE\\#}$ apart is the ability
to efficiently handle _Unicode_ as discussed also later in Section 6.2. On
patterns such as \b\w{12,}\b, $\mathbf{RE\\#}$ is over 7x faster than the next
best engine, pcre2/jit, and over 10x faster than the rest of the competition.

The reason for this gap is that \w denotes a very large character set, and
other automata-based engines cannot handle it as efficiently, as \w may
contribute with tens of thousands of individual transitions. $\mathbf{RE\\#}$
also has a very efficient implementation of the word boundary \b – represented
via negative lookarounds in the engine and encoded directly into DFA
transitions – which causes the engine to have a very fast inner matching loop.
Another benchmark where $\mathbf{RE\\#}$ excels at is the ‘context’ benchmark,
which uses `[A-Za-z]{10}\s+[\s\S]{0,100}Result[\s\S]{0,100}\s+[A-Za-z]{10}`,
it is over 8x faster than other automata-based engines, which struggle with
the `[\s\S]{0,100}` part of the pattern, as it creates many transitions in the
automaton. This is where the algebraic approach to regex matching shines, as
the engine can easily detect redundant transitions through the loop rule in
Figure 4 and thereby minimize the automaton on the fly.

####  6.1.3. CloudFlare-ReDOS (3 benchmarks)

This category is designed to showcase worst-case performance of regex engines.
The regexes themselves are not very practical, but useful to distinguish
between the engines that have good worst-case performance and those that do
not.

The cloud-flare-redos category is a set of regexes that are designed to
trigger catastrophic backtracking in backtracking regex engines. The benchmark
comes in three variants: the ‘original’ variant is using the pattern that
caused the CloudFlare outage in 2019, while the ‘simplified-short’ and
‘simplified-long’ variants are matching the regex .*.*=.*, which on linear
complexity engines is essentially benchmarking “how fast can you find the
equals sign”, and on backtracking engines is a worst-case scenario, where
certain backtracking engines are hundreds of thousands, even millions of times
slower than the best performing engines. $\mathbf{RE\\#}$ is the top performer
in the ‘original’ variant of the benchmark, which does not really show
anything meaningful about the engine, apart from the fact that it does not
suffer from catastrophic backtracking.

####  6.1.4. Quadratic (3 benchmarks)

Figure 6. _Quadratic_ benchmark results for 1x=100, 2x=200, 10x=1000

The regexes here are intended to trigger quadratic behavior in all-match
scenarios. The benchmark comes in three variants: ‘1x’, ‘2x’, and ‘10x’, which
illustrate how the performance of the engines scales with the input length.
While the reason for Hyperscan’s excellent performance is _earliest_ match
semantics, which guarantees linearity, the reason for $\mathbf{RE\\#}$’s
close-to-linear performance is different. While Figure 5(a) shows the
$\mu_{g}$ relative slowdown ratios, Figure 6 illustrates the three variants
separately.

The reason for $\mathbf{RE\\#}$’s excellent performance in the quadratic
category is that the engine finds a match in a fixed number of input-parallel
steps, which it detects at the level of the algebraic representation of the
regex. The engine still suffers from the number of matches, which brings the
performance down to $O(pn)$, where $p$ is the number of parallel steps
required to process the input, and $n$ is the number of matches. The engine is
still significantly faster than other engines in the category apart from
Hyperscan, which has a linear time complexity by design.

####  6.1.5. Date and Dictionary (3 benchmarks)

These are large regexes with many alternations. The date benchmark is
described as a tokenizer for dates in various formats, which has numerous
short matches of ¡5 characters. The dictionary benchmark consists of
approximately 2500 words, which measures the speed of traversing a string with
many alternation.

While $\mathbf{RE\\#}$ wins here, see Figure 5(a), both of these categories
have flaws and should be taken with a grain of salt. Neither of the patterns
are sorted by descending length, which means that the pattern consists of many
alternations completely unreachable to PCRE engines, such as may|mayo, where
the engine will never match mayo at all.

Upon further inspection, this behavior seems to originate from a near decade
old semantic bug in a Python library for finding dates (Koumjian, 2024), that
gets millions of downloads per month, but has somehow gone unnoticed. And the
dictionary benchmark consists of many alternations ordered such as
(absentmindedness|absentmindedness’s), where the second alternation will never
be matched. Furthermore, the dictionary benchmark contains only _one match_ ,
which barely explores any of the state space of the automaton than can arise
from the regex.

Since $\mathbf{RE\\#}$ uses a larger regex in both of these benchmarks, it
also reports a slightly higher match length sum of 111832 instead of 111825 in
the two _date_ benchmarks, where certain matches are longer than their
_leftmost-greedy_ counterparts. For this reason, these benchmarks are
separately analyzed in the extended benchmark in Section 6.2, where the
patterns are sorted by length, and the performance of the engines is compared
in a more controlled environment.

###  6.2. Extended Comparison

The extended comparison consists of a set of regexes to emphasize the
strengths of our engine. The benchmarks have been split into several
categories. The first category consists of modified versions of the _date_ and
_dictionary_ benchmarks from the rebar benchmark suite. Hyperscan is included
in very few of these benchmarks as it does not support \b with Unicode
characters or lookarounds or patterns that exceed a certain length, but for
the sake of comparison, we include it in benchmarks using multi-pattern mode
and _earliest_ match semantics whenever possible.

The extended summary $\mu_{g}$ of speed ratios is shown in Figure 5(b) _with a
separate column for each benchmark category below as indicated by the column
title_. The actual $\mu_{g}$ of several engines is larger than shown, as many
of the benchmarks are designed to push the engines to their limits, and the
engine may not finish the benchmark in 1 minute that is the _cut-off_ time.

####  6.2.1. Date and Dictionary Amended (2 benchmarks)

The benchmarks are the same as in the baseline comparison apart from two
small, but significant, changes:

  * ✓

alternations (unions) are sorted in descending order by length

  * ✓

inputs contain not just one but over a thousand unique matches

The large amount of _unique_ matches is especially important, as it prevents
the lazy automata engines from creating a tiny purpose-built automaton for
matching the exact same string over and over. Adding more matches to the input
drops the performance of the lazy automata engines significantly, including
$\mathbf{RE\\#}$.

The throughput reported for $\mathbf{RE\\#}$ in the _dictionary_ benchmark is
564.5MB/s with 1 match, and 107.3MB/s with 2663 matches. But what is notable
here is that the performance of $\mathbf{RE\\#}$ does not fall with complexity
at the same rate as the other automata engines. Where the throughput of
rust/regex falls from 535.6MB/s to 8.9MB/s, and the throughput of re2 falls
from 3.6MB/s to 618KB/s. Even the throughput of Hyperscan falls from 5.4 GB/s
to 104.6MB/s by increasing the number of matches, which is just slightly below
the throughput of $\mathbf{RE\\#}$. $\mathbf{RE\\#}$ still maintains this
level of performance with even far more complex regexes, as show in the
_monster_ regex category in Section 6.2.2.

####  6.2.2. Monster Regexes (5 benchmarks)

This category comprises large regexes designed to stress the engines to their
limits. These regexes are challenging for both backtracking as well as
automata engines, where the former will suffer from redundant work and the
latter will suffer from large state space complexity. This category
illustrates one of the biggest strengths of $\mathbf{RE\\#}$, where it
dominates the competition in all of the benchmarks in this category, see
Figure 1(a), thanks to both its small symbolic automaton and algebraic
rewrites. Hyperscan is included in the first three benchmarks as these
patterns can be split into multiple individual patterns and run in multi-
pattern mode, but not in the last two benchmarks, as these consist of one
large pattern, which exceeds the maximum size supported by Hyperscan. All of
the patterns exceed the maximum size supported by pcre2/jit as well, which is
why it is not included.

The first benchmark in this category is the same dictionary regex as in the
previous benchmark, but with _case insensitivity_ enabled (IgnoreCase option
or (?i:$R$)). Ignoring case on the dictionary regex significantly increases
the state space complexity of the regex, and neither backtracking nor the
automata engines can handle it. Hyperscan with multi-pattern mode does well
here, albeit with an easier pattern than the others because of _earliest_
match semantics. Perl seems to have some interesting optimizations for ASCII
dictionaries specifically, being the only backtracking engine that can handle
it. But the interesting part in this benchmark is how, very
counterintuitively, the performance of $\mathbf{RE\\#}$ and dotnet/nobt
_increases_ when case is ignored.

The throughput of $\mathbf{RE\\#}$ with the case-insensitive dictionary regex
actually increases by $\approx$ 40% over the case-sensitive version, which is
due to the size of the automaton _decreasing_ when case is ignored, as the
engine can merge transitions together. This is a very interesting result, as
many others completely fall apart with case insensitivity enabled, with their
throughput falling hundreds of times compared to the case-sensitive version.

The second and third benchmarks are similar dictionary regexes, but with
unicode characters. This benchmark illustrates the performance of the engine
on unicode character classes, which are difficult to handle for most engines.
On the case-insensitive version of the unicode dictionary, most engines are
several orders of magnitude behind $\mathbf{RE\\#}$, apart from hyperscan and
dotnet/nobt, which are 5.2x and 5.5x slower than $\mathbf{RE\\#}$, which are
still very good results, as the fourth-fastest engine, perl, is 862x slower
than $\mathbf{RE\\#}$.

The last two benchmarks add a context of 50 characters in the form of .{0,50}
on either side of an already difficult case-insensitive dictionary regex,
which forces the engine to explore a significant amount of possibilities, as
the context can be anything. These benchmarks are a difficult scenario for
even dotnet/nobt, which otherwise manages to keep up in these difficult
scenarios, here even dotnet/nobt is 20x slower than $\mathbf{RE\\#}$.

####  6.2.3. Hidden Passwords (11 benchmarks)

This category illustrates something that is very difficult to express in
standard regex syntax, which causes the pattern to be very large and slow to
handle for most engines. $\mathbf{RE\\#}$ uses _intersection_ to demonstrate
how the performance does not degrade at the rate of other engines that use
_union_ to express an equivalent pattern but at a _factorial_ cost. The main
regex is an intersection of constraints, where the match must contain at least
one character in all of [0-9], [a-z], [A-Z], [!-/], and the password must have
a certain length that varies throughout the benchmark. To simplify, all of the
inputs here have been limited to ASCII.

This benchmark, see Figure 7, illustrates the same principle as the _monster_
regexes, where the performance of the engine does not degrade at the rate of
other engines. While re2 and rust/regex are able to handle the pattern up to 8
characters, both of the engines hit a wall at 9 characters, where the
performance of the engines drops significantly. The performance of Hyperscan
is also dropping at 9 characters, but it stops accepting the pattern at 10
characters. The search-time performance of $\mathbf{RE\\#}$ is still
reasonable at 15 characters and above, and the throughput of the engine is
still in the hundreds of MB/s. Without intersections, the performance of
$\mathbf{RE\\#}$ would also hit a wall soon after the others, as the state
space of the automaton grows at an exponential rate, but using intersections
allows to keep the automaton small and the performance of the engine high.

Figure 7. Searching for hidden passwords of increasing length.

####  6.2.4. Long Matches (7 benchmarks)

This category is designed to test the engines’ ability to accelerate long
matching patterns, see Figure 8(a). The input used in this category consists
of long lines, averaging around 3000 characters in length. The patterns used
in the category are designed so that the engine has to scan the entire line to
find a match, but the engine has many opportunities to skip characters during
the inner loop of matching.

An interesting observation from this category is that many of the engines have
one-off optimizations for long matches, where certain patterns with the exact
same language are significantly faster than others. For example the pattern
used in the _skip-5_ benchmark, (?m)^.*1.*1.*1.*1.*1.*$ is 120x faster than
the pattern in the _skip-5-loop_ benchmark (?m)^.*(1.*){5}$ for dotnet/comp,
as optimizations get detected and applied in the former, but not in the
latter. The same is true for python/re and pcre2/jit which both lose
performance noticeably with the loop variant of the pattern. $\mathbf{RE\\#}$
actually loses one benchmark in this category, the _skip-2_ benchmark with the
pattern (?m)^.*1.*1.*$, where dotnet/comp vectorizes the first part of the
pattern as well. The benchmarks _skip-3_ and _skip-5_ show that this behavior
does not apply to the remainder of the pattern, as the performance of
dotnet/comp drops significantly with the number of skips.

The reason why $\mathbf{RE\\#}$ is able to outperform the other engines in
this benchmark is that derivatives allow the engine to cheaply infer which
transitions are redundant, which lets the engine use input-parallelism to skip
over large parts of the input, which gives the engine an advantage of an order
of magnitude over most other engines in this category.

(a) Long matches (Section 6.2.4).

(b) Lookarounds (Section 6.2.6).

Figure 8. Long and Lookaround benchmarks. $y$-axis is relative slowdown in
_log_ scale.

####  6.2.5. Character Sets and Unicode (7 benchmarks)

This category shows the performance of symbolic character sets in
$\mathbf{RE\\#}$, i.e., the power of $\mathcal{A}$. The patterns used in this
category are to find words containing a certain character set, such as
\b\w*[abc]w*\b. To add a layer of complexity, both the input and character set
are unicode characters, which makes the pattern difficult to handle for most
engines, see Figure 1(b).

The first two benchmarks _word-vowels-1_ and _word-vowels-2_ , illustrate how
$\mathbf{RE\\#}$ is able to use the derivative-based framework to incorporate
vectorized character set matching into simple word patterns and be an order of
magnitude faster than the other engines.

The _word-vowels-3 and word-vowels-4_ benchmarks are more complex both in
terms of number of matches and the complexity of the pattern, where the
performance of $\mathbf{RE\\#}$ is still very good, but not as dominant as in
the first two benchmarks.

The _word-vowels-5-to-digits and word-digits-to-vowels-5_ benchmarks
illustrate that this character set efficiency works in both directions, where
certain engines (e.g., python/re and dotnet/comp) locate the digits-first
variant significantly faster than the vowels, but the throughput for
$\mathbf{RE\\#}$ is nearly identical for both. The _many-set-constraints_
benchmark illustrates a more complex scenario, where the engine has to find
many of these set constraints in a single match, which severely slows several
engines down, but $\mathbf{RE\\#}$ is still able to maintain a throughput of
757.7MB/s, where most other engines are in KB/s.

####  6.2.6. Lookarounds (8 benchmarks)

The lookarounds category illustrates that all the optimizations apply to
lookarounds in $\mathbf{RE\\#}$ as well. There are many benchmarks in this
category where the performance of the engine is several orders of magnitude
faster than in other engines, see Figure 8(b). Note that certain engines (e.g.
pcre2/jit) are omitted from the context-both benchmarks as they do not support
unbounded lookbehinds.

The _lookbehind-fixed_ and _lookahead-fixed_ benchmarks demonstrate the
efficacy of simple string literal prefilter optimizations, e.g. those in
Section 5.2, where the engine is able to vectorize the search for patterns
containing both prefix and suffix lookarounds, which makes $\mathbf{RE\\#}$
several orders of magnitude faster than the other engines.

While Figure 2 showed that the performance of lookbehinds is linear for all
matches, the same is not true for lookaheads. The only guarantee for
lookaheads is that a single match is input-linear, but the performance of the
engine degrades if there are multiple matches depending on the same lookahead
context, which is located far away from the match. The _context-ahead_
benchmarks illustrate this, where the performance of the engine is slightly
behind dotnet/comp, as both of the engines suffer from quadratic all-matches
behavior in this case.

Despite this, the performance of $\mathbf{RE\\#}$ is still very good in this
category compared to the rest of the engines, where there is a noticeable lack
of optimizations for lookarounds. How to eliminate quadratic all-matches
behavior for lookaheads is a topic for future work.

The _context-both_ benchmarks illustrate the scenario where each match is
dependent on both a lookbehind and a lookahead, where $\mathbf{RE\\#}$ has a
lead similar to Figure 2, as the linear time _all-matches_ complexity of
lookbehinds is not applicable to other engines.

##  7\. Related and Future Work

This work builds upon and uses the theory of location based derivatives introduced in (Moseley et al., 2023), and the implementation builds upon the open source .NET regular expression library (Microsoft, 2022). The match semantics supported in $\mathbf{RE\\#}$ is _leftmost-longest_ (POSIX) rather than _leftmost-greedy_ (a.k.a., _backtracking_ or PCRE) semantics. It is unclear how to support extended Boolean operators in backtracking in the first place and what their intended semantics would be – this is primarily related to that | is _non-commutative_ in the backtracking semantics and therefore some key distributivity laws such as $X(Y\texttt{|}Z)\equiv XY\texttt{|}XZ$ no longer preserve match semantics. For example, in PCRE (a|ab)(c|b) matches the prefix "ab" of "abc" but (a|ab)c|(a|ab)b matches the whole string "abc". Consequently, many rewrite rules based on derived Boolean laws, such as sub1 and loop in Figure 4, become invalid in PCRE.

In functional programming derivatives were studied in (Fischer et al., 2010;
Owens et al., 2009) for IsMatch. (Sulzmann and Lu, 2012; Ausaf et al., 2016)
study matching with Antimirov derivatives and POSIX semantics and also
Brzozowski derivatives in (Ausaf et al., 2016) with a formalization in
Isabelle/HOL. The algorithm of (Sulzmann and Lu, 2012) has been recently
further studied in (Tan and Urban, 2023; Urban, 2023). It is also mentioned in
(Urban, 2023, p.22) that _reversal_ , as used in (Moseley et al., 2023), is
not directly applicable in the context of the (Sulzmann and Lu, 2012)
algorithm. Partial derivatives of regular expressions extended with complement
and intersection have also been studied in (Caron et al., 2011). These works
do not support lookarounds (or anchors). The key difference with the work of
_transition regexes_ used in SMT (Stanford et al., 2021) is that the theory of
transition regexes does not support lookarounds. However, generalizing
transition regexes to location based derivatives is an interesting direction
for future work.

The conciseness of using intersection and complement in regular expressions is
demonstrated in (Gelade and Neven, 2012) where the authors show that using
intersection and complement in regular expressions can lead to a double
exponentially more succinct representation of regular expressions. Here we
have experimentally shown how the enriched expressivity can enable practical
scenarios for matching that are otherwise not possible.

Regular expressions have in practice many extensions, such as _backreferences_
and _balancing groups_ , that reach far beyond _regular_ languages in their
expressive power. Such extensions, see (Loring et al., 2019), fall outside the
scope of $\mathbf{RE\\#}$. Lookaheads do maintain regularity (Morihata, 2012)
and regular expressions with lookaheads can be converted to Boolean automata
(Berglund et al., 2021b). (Chida and Terauchi, 2023) consider extended regular
expressions in the context of backreferences and lookaheads. They build on
(Carle and Narendran, 2009) to show that extended regular expressions
involving backreferences and both positive and negative lookaheads leads to
_undecidable_ emptiness, but, when restricted to positive lookaheads only is
closed under complement and intersection. (Miyazaki and Minamide, 2019)
present an approach to finding match end with derivatives in regular
expressions with lookaheads using _Kleene algebras with lookahead_ as an
extension of Kleene algebras with tests (Kozen, 1997) where the underlying
semantic concatenation is _commutative_ and _idempotent_ – it is unclear how
lookbehinds and reversal fit in here. Derivatives combined with Kleene
algebras are also studied in (Pous, 2015).

Some aspects of our work here are related to SRM (Saarikivi et al., 2019) that
is the predecessor of the NonBacktracking regex backend of .NET (Moseley et
al., 2023), but SRM lacks support for lookarounds as well as anchors and is
neither POSIX nor PCRE compliant. Intersection was also included as an
experimental feature in the initial version of SRM by building directly on
derivatives in (Brzozowski, 1964), and used an encoding via regular expression
_conditionals_ that unfortunately conflicts with the intended semantics of
conditionals and therefore has, to the best of our knowledge, never been used
or evaluated.

State-of-the-art nonbacktracking regular expression matchers based on automata
such as RE2 (Cox, 2010) and grep (GNU, 2023) using variants of (Thompson,
1968), and Hyperscan (Wang et al., 2019) using a variant of (Glushkov, 1961),
as well as the derivative based NonBacktracking engine in .NET make heavy use
of _state graph memoization_. None of these engines currently support
lookarounds, intersection or complement. A general advantage of using
derivatives is that they often minimize the state graph (but do not guarantee
minimization), as was already shown in (Owens et al., 2009, Table 1) for DFAs.
Similar discussion apperas also in (Sulzmann and Lu, 2012, Section 5.4) where
NFA sizes are compared for Thompson’s and Glushkov’s, versus Antimirov’s
constructions, showing that Antimirov’s construction consistently yields a
smaller state graph. Further comparison with automata based engines appears in
(Moseley et al., 2023).

The two main standards for matching are PCRE (backtracking semantics) and
POSIX (Laurikari, 2000; Berglund et al., 2021a). _Greedy_ matching algorithm
for backtracking semantics was originally introduced in (Frisch and Cardelli,
2004), based on $\epsilon$-NFAs, while maintaining matches for eager loops. In
the current work we focused on the expressivity of a _single_ regular
expression. Compared to lookarounds, there are different approaches to
achieving contextual information, e.g. it can be done programmatically by
matching multiple regular expressions, or by the use of transducers, e.g.
Kleenex (Grathwohl et al., 2016), that can produce substrings in context at
high throughput rates.

The theory of derivatives based on locations that is developed here can
potentially be used to extend regular expressions with lookarounds in SMT
solvers that support derivative based lazy exploration of regular expressions
as part of the sequence theory, such solvers are CVC5 (Barbosa et al., 2022;
Liang et al., 2015) and Z3 (de Moura and Bjørner, 2008; Stanford et al.,
2021). A further extension is to lift the definition of location derivatives
to a fully _symbolic_ form as is done with _transition regexes_ in Z3
(Stanford et al., 2021). (Chen et al., 2022) mention that the OSTRICH string
constraint solver could be extended with backreferences and lookaheads by some
form of alternating variants of prioritized streaming string transducers
(PSSTs), but it has, to our knowledge, not been done. Such extensions would
widen the scope of analysis of string verification problems that arise from
applications that involve regexes using anchors and lookarounds. It would then
also be beneficial to extend the SMT-LIB (SMT-LIB, 2021) format to support
lookarounds.

Counters are a well-known Achilles heel of essentially all nonbacktracking
state-of-the-art regular expression matching engines as recently also
demonstrated in (Turoňová et al., 2022), which makes any algorithmic
improvements of handling counters highly valuable. In (Turoňová et al., 2020),
Antimirov-style derivatives (Antimirov, 1996) are used to extend NFAs with
counting to provide a more succinct symbolic representation of states by
grouping states that have similar behavior for different stages of counter
values together using a data-structure called a _counting-set_. It is an
intriguing open problem to investigate if this technique can be adapted to
work with location derivatives within our current framework. (Glaunec et al.,
2023) point out that it is important to optimize specific steps of regular
expression matching to address particular performance bottlenecks. The
specific BVA-Scan algorithm is aimed at finding matches with regular
expressions containing counters more efficient. (Holík et al., 2023) report on
a subset of regexes with counters called synchronizing regexes that allow for
fast matching.

Recently (Mamouras and Chattopadhyay, 2024) presented a new algorithm for
matching lookarounds with Oracle NFAs, which are essentially cached queries to
the oracle that can be used to match lookarounds. The semantics presented in
their paper is consistent with the semantics of $\mathbf{ERE_{\leq}}$ but
without support for $\texttt{\&}{},\texttt{\char 126\relax}$, as described in
(Moseley et al., 2023, Section 3.7) using derivation relations, for example,
$\langle{s{[}i{]},s{[}j{]}}\rangle\models\texttt{(?=}R\texttt{)}$ iff $i=j$
and
$s{[}i{]}\,{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}\,s{[}|s|{]}$. We could not find any implementation of the
algorithm, but it would be interesting to compare the lookaround approaches.

(Barrière and Pit-Claudel, 2024) present a new nonbacktracking algorithm for
matching JavaScript regular expressions with lookarounds in linear time. The
first steps of the algorithm construct an oracle similar to the one in
(Mamouras and Chattopadhyay, 2024), but leveraging JavaScript semantics for
the unique capability of matching capture groups both in the main regex and
lookarounds in linear time. The algorithm is implemented as an NFA engine,
whereas $\mathbf{RE\\#}$ is a lazy DFA engine. The fragment of regexes is also
orthogonal to the regexes in $\mathbf{RE\\#}$: while intersection and
complement are not allowed, at the same time lookarounds can be used freely in
any context. But there is a common subset on which it would be interesting to
see how the two approaches compare in practice. Supporting capture groups in
$\mathbf{RE\\#}$ is an interesting extension for future work, which could
potentially be done as in (Moseley et al., 2023) or using tagged-NFA’s as in
(Laurikari, 2000).

##  8\. Conclusion

We have presented both a theory and an implementation for extended regular
expressions including complement, intersection and positive and negative
lookarounds that have not previously been explored in depth in such a
combination. Prior work has analyzed different other sets of extensions and
their properties, but several such combinations veer out of the scope of
regular languages.

We have demonstrated the practicality of the class $\mathbf{RE\\#}$ and the
power of algebraic simplification rules through derivatives. We have included
extensive evaluation using popular benchmarks and compared to industrial
state-of-the-art engines that come with decades of expert level automata
optimizations, where $\mathbf{RE\\#}$ shows $71\%$ improvement over the
fastest industrial matcher today, already for the _baseline_ , while enabling
reliable support for features out of reach for all other engines. There are
also many interesting open problems and extensions remaining.

We expect that these new insights will change how regular expressions are
preceived and the landscape of their applications in the future. Potentially
enabling new applications in LLM prompt engineering frameworks, new
applications in medical research and bioinformatics, and new opportunities in
access and resource policy language design by web service providers, where
regexes are an integral part but today limited to _very restricted fragments
of $\mathbf{RE}$_ due to their application in security critical contexts with
high reliability requirements in policy engines.

## References

  * (1)
  * Antimirov (1996) Valentin Antimirov. 1996\.  Partial Derivatives of Regular Expressions and Finite Automata Constructions.  _Theoretical Computer Science_ 155 (1996), 291–319.  https://doi.org/10.1007/3-540-59042-0_96
  * Ausaf et al. (2016) Fahad Ausaf, Roy Dyckhoff, and Christian Urban. 2016\.  POSIX Lexing with Derivatives of Regular Expressions (Proof Pearl). In _Interactive Theorem Proving_ _(LNCS, Vol. 9807)_ , Jasmin Christian Blanchette and Stephan Merz (Eds.). Springer, 69–86.  https://doi.org/10.1007/978-3-319-43144-4_5
  * Barbosa et al. (2022) Haniel Barbosa, Clark W. Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli, and Yoni Zohar. 2022\.  cvc5: A Versatile and Industrial-Strength SMT Solver. In _Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part I_ _(Lecture Notes in Computer Science, Vol. 13243)_ , Dana Fisman and Grigore Rosu (Eds.). Springer, 415–442.  https://doi.org/10.1007/978-3-030-99524-9_24
  * Barrière and Pit-Claudel (2024) Aurèle Barrière and Clément Pit-Claudel. 2024\.  Linear Matching of JavaScript Regular Expressions.  _PLDI’2024_ 8 (2024), 201:1–201:25.  https://doi.org/10.1145/3656431
  * Berglund et al. (2021a) Martin Berglund, Willem Bester, and Brink van der Merwe. 2021a.  Formalising and implementing Boost POSIX regular expression matching.  _Theoretical Computer Science_ 857 (2021), 147–165.  https://doi.org/10.1016/j.tcs.2021.01.010
  * Berglund et al. (2021b) Martin Berglund, Brink van der Merwe, and Steyn van Litsenborgh. 2021b.  Regular Expressions with Lookahead.  _Journal of Universal Computer Science_ 27, 4 (2021), 324–340.  https://doi.org/10.3897/jucs.66330
  * Brzozowski (1964) Janusz A. Brzozowski. 1964\.  Derivatives of regular expressions.  _JACM_ 11 (1964), 481–494.  https://doi.org/10.1145/321239.321249
  * Carle and Narendran (2009) Benjamin Carle and Paliath Narendran. 2009.  On Extended Regular Expressions. In _Language and Automata Theory and Applications, Third International Conference, LATA 2009, Tarragona, Spain, April 2-8, 2009\. Proceedings_ _(Lecture Notes in Computer Science, Vol. 5457)_ , Adrian-Horia Dediu, Armand-Mihai Ionescu, and Carlos Martín-Vide (Eds.). Springer, 279–289.  https://doi.org/10.1007/978-3-642-00982-2_24
  * Caron et al. (2011) Pascal Caron, Jean-Marc Champarnaud, and Ludovic Mignot. 2011\.  Partial Derivatives of an Extended Regular Expression. In _Language and Automata Theory and Applications - 5th International Conference, LATA 2011, Tarragona, Spain, May 26-31, 2011. Proceedings_ _(Lecture Notes in Computer Science, Vol. 6638)_ , Adrian-Horia Dediu, Shunsuke Inenaga, and Carlos Martín-Vide (Eds.). Springer, 179–191.  https://doi.org/10.1007/978-3-642-21254-3_13
  * Chen et al. (2022) Taolue Chen, Alejandro Flores-Lamas, Matthew Hague, Zhilei Han, Denghang Hu, Shuanglong Kan, Anthony W. Lin, Philipp Rümmer, and Zhilin Wu. 2022.  Solving String Constraints with Regex-Dependent Functions through Transducers with Priorities and Variables.  _Proc. ACM Program. Lang._ 6, POPL, Article 45 (jan 2022), 31 pages.  https://doi.org/10.1145/3498707
  * Chida and Terauchi (2023) Nariyoshi Chida and Tachio Terauchi. 2023.  On Lookaheads in Regular Expressions with Backreferences.  _IEICE Trans. Inf. Syst._ 106, 5 (2023), 959–975.  https://doi.org/10.1587/transinf.2022edp7098
  * Cox (2010) Russ Cox. 2010.  Regular Expression Matching in the Wild.  https://swtch.com/r̃sc/regexp/regexp3.html
  * D’Antoni and Veanes (2021) Loris D’Antoni and Margus Veanes. 2021.  Automata Modulo Theories.  _Commun. ACM_ 64, 5 (May 2021), 86–95.
  * Davis (2019) James C. Davis. 2019\.  Rethinking Regex Engines to Address ReDoS. In _Proceedings of ESEC/FSE’19_ (Tallinn, Estonia) _(ESEC/FSE 2019)_. ACM, New York, NY, USA, 1256–1258.  https://doi.org/10.1145/3338906.3342509
  * Davis et al. (2018) James C. Davis, Christy A. Coghlan, Francisco Servant, and Dongyoon Lee. 2018.  The Impact of Regular Expression Denial of Service (ReDoS) in Practice: An Empirical Study at the Ecosystem Scale. In _Proceedings of ESEC/FSE’18_ (Lake Buena Vista, FL, USA) _(ESEC/FSE 2018)_. ACM, New York, NY, USA, 246–256.  https://doi.org/10.1145/3236024.3236027
  * de Moura and Bjørner (2008) Leonardo de Moura and Nikolaj Bjørner. 2008.  Z3: An Efficient SMT Solver. In _TACAS’08_ _(LNCS)_. Springer, 337–340.  https://doi.org/10.1007/978-3-540-78800-3_24
  * Fischer et al. (2010) Sebastian Fischer, Frank Huch, and Thomas Wilke. 2010\.  A Play on Regular Expressions: Functional Pearl.  _SIGPLAN Not._ 45, 9 (2010), 357–368.  https://doi.org/10.1145/1863543.1863594
  * Frisch and Cardelli (2004) Alain Frisch and Luca Cardelli. 2004.  Greedy Regular Expression Matching. In _Automata, Languages and Programming (ICALP’04)_ _(LNCS, Vol. 3142)_ , Josep Díaz, Juhani Karhumäki, Arto Lepistö, and Donald Sannella (Eds.). Springer, 618–629.  https://doi.org/10.1007/978-3-540-27836-8_53
  * Gallant (2024) Andrew Gallant. 2024\.  BurntSushi: rebar.  https://github.com/BurntSushi/rebar.
  * Gelade and Neven (2012) Wouter Gelade and Frank Neven. 2012.  Succinctness of the Complement and Intersection of Regular Expressions.  _ACM Trans. Comput. Log._ 13, 1 (2012), 4:1–4:19.  https://doi.org/10.1145/2071368.2071372
  * Glaunec et al. (2023) Alexis Le Glaunec, Lingkun Kong, and Konstantinos Mamouras. 2023\.  Regular Expression Matching using Bit Vector Automata.  _Proc. ACM Program. Lang._ 7, OOPSLA1 (2023), 492–521.  https://doi.org/10.1145/3586044
  * Glushkov (1961) V. M. Glushkov. 1961\.  The abstract theory of automata.  _Russian Math. Surveys_ 16 (1961), 1–53.  https://doi.org/10.1070/RM1961v016n05ABEH004112
  * GNU (2023) GNU. 2023.  grep.  https://www.gnu.org/software/grep/.
  * Google (2024) Google. 2024.  RE2.  https://github.com/google/re2.
  * Grathwohl et al. (2016) Niels Bjørn Bugge Grathwohl, Fritz Henglein, Ulrik Terp Rasmussen, Kristoffer Aalund Søholm, and Sebastian Paaske Tørholm. 2016\.  Kleenex: compiling nondeterministic transducers to deterministic streaming transducers. In _Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016_ , Rastislav Bodík and Rupak Majumdar (Eds.). ACM, 284–297.  https://doi.org/10.1145/2837614.2837647