# Derivative Based Extended Regular Expression Matching Supporting
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.

Regular expressions are widely used in software. Various regular expression
engines support different combinations of extensions to classical regular
constructs such as Kleene star, concatenation, nondeterministic choice (union
in terms of match semantics). The extensions include e.g. anchors,
lookarounds, counters, backreferences. The properties of combinations of such
extensions have been subject of active recent research.

In the current paper we present a symbolic derivatives based approach to
finding matches to regular expressions that, in addition to the classical
regular constructs, also support complement, intersection and lookarounds
(both negative and positive lookaheads and lookbacks). The theory of computing
symbolic derivatives and determining nullability given an input string is
presented that shows that such a combination of extensions yields a match
semantics that corresponds to an effective Boolean algebra, which in turn
opens up possibilities of applying various Boolean logic rewrite rules to
optimize the search for matches.

In addition to the theoretical framework we present an implementation of the
combination of extensions to demonstrate the efficacy of the approach
accompanied with practical examples.

##  1\. Introduction

Regular expressions are supported by standard libraries of all major
programming languages and software development kits. They are essential in
string manipulation, membership testing, text extraction tasks on strings,
etc. In recent years symbolic derivatives based regular expression matching
has seen rapid development as being performance wise more predictable than
backtracking engines and modern optimized regular expression engines such as
e.g. Hyperscan (Wang et al., 2019) and RE2 (Google, 2023), that are all, in
essence, relying on algorithms by (Glushkov, 1961) or (Thompson, 1968).

The extended regular expressions supported by backtracking engines often
involve support for combinations of extensions, e.g. backreferences,
lookarounds and balancing groups, yielding a family of languages that has been
shown by (Carle and Narendran, 2009) not to be closed under intersection.
Recent work by (Chida and Terauchi, 2023) has explored the expressive power of
the combination of regular expressions with backreferences and positive
lookaheads and devised a new flavor of memory automata to express their
behavior.

We present a derivative-based symbolic extended regular expression engine,
which supports _intersection_ (&), _complement_ ($\sim$) and _lookaround_
((?=), (?!), (?<=) and (?<!)) operations, i.e. both negative and positive
lookahead and lookback operations. To remind the reader, by example of a
positive lookahead, the regex a(?=c) will match a in the string “ac” but
nothing in “ab”, i.e. lookarounds do not match text but positions in strings
in a more general way than anchors (e.g. word boundary \b) (Friedl, 2006). We
show that the extended engine can be used to solve problems that are currently
unfeasible to solve with existing regular expression engines. We also show
that all context dependent regex anchors can be expressed using lookarounds.
We have implemented the extended engine as a library for the .NET platform,
which extends the existing .NET nonbacktracking engine (Moseley et al., 2023),
but without preserving backtracking semantics.

We demonstrate the usefulness of the extended engine by examples of precise
text extraction in a way that is to our knowledge not possible with standard
regexes or involves a factorial blowup of the regex pattern. We make the case
that intersection and complement are useful tools in concise definition of
regular expressions, showing examples of incremental specification of regexes
by use of complement, and exclusion of unwanted matches by use of negation.

Our work is motivated by the fact that the current state-of-the-art symbolic
regex engine (Moseley et al., 2023) does not support intersection because its
semantics is difficult to combine with all the other features in a meaningful
way while maintaining backtracking semantics. It is also a problem of
backwards compatibility to, for example, support & as a new operator.

### Contributions

This paper makes the following contributions:

  * •

We build on the .NET 7 nonbacktracking regular expression engine (Moseley et
al., 2023) to develop a theory for symbolic derivatives based regular
expression matching that, in addition to _Kleene star_ , _bounded loops_
(_counters_), _alternation_ (which in our case is synonymous to _union_) and
_concatenation_ , supports _intersection_ , _complement_ and _both positive
and negative lookaround operations_ in regexes. The result is a significant
increment over (Moseley et al., 2023) in terms of Theorem 1, Theorem 2 and
Theorem 3 accompanied by proofs.

  * •

The theoretical results are accompanied by an implementation (Varatalu, 2023)
of an extended regular expression engine that supports all Boolean operations
on regexes, including intersection and complement using a natural syntax
making it convenient to use.

  * •

Due to the match semantics of such a regular expression language corresponding
to an effective Boolean algebra, it is now possible to define and apply
numerous Boolean rewrites and optimizations that yield better runtime
performance. It is thus also possible to reason about the validity of such
optimizations in terms of Boolean algebra.

  * •

We show that the extended engine can be used to solve problems that are
currently either impossible or infeasible to solve with standard regular
expressions.

  * •

We show that all regex anchors can be expressed using lookarounds as
conjectured in (Moseley et al., 2023). We prove the conjecture together with
providing an implementation as mentioned above.

Before proceeding to introducing the theory, let us look at some practical
examples that illustrate how the proposed combination extensions can be used
to establish the existence of matches but also locate them in strings.

##  2\. Motivating examples

In this section we explain the intuition behind the intersection (conjunction)
and complement (negation) operators in regexes and give some motivating
examples of how they can be useful. The examples are also available in the
accompanying web application 111https://ieviev.github.io/sbre/. The following
examples are written in the syntax of the .NET regex engine, with the addition
of &, $\sim$, and the symbol $\top$, to denote a predicate that is true on any
character. The syntax is explained in more detail in Section 3.

###### Example 2.1 (Password extraction).

Consider the following regex

        ^(?=.*[a-z])(?=.*[A-Z])(?=.*\d)[a-zA-Z\d]{8,}$

that originates from a StackOverflow question
222http://stackoverflow.com/questions/19605150/regex-for-password-must-
contain-at-least-eight-characters-at-least-one-number-a asking for a regex for
validating a password. The regex in principle is an intersection of three
lookaheads, each of which checks for a certain condition and a loop that
checks for the length of the password.

  * •

`(?=.*[a-z])` checks for at least one lowercase letter

  * •

`(?=.*[A-Z])` checks for at least one uppercase letter

  * •

`(?=.*\d)` checks for at least one digit

  * •

`[a-zA-Z\d]{8,}` checks for at least 8 characters

The regex is a good example of emulating conjunctive conditions using
lookaheads for checking if there exists a match. However, the regex is not
suitable for extracting a password from an arbitrary string, even when
removing the anchors. The reason is that the regex engine will try to match
the lookaheads independently, and then backtrack to the beginning of the match
to try the next lookahead. This is an example of a limitation to what can be
expressed in traditional regular expressions. And note that due to the lack of
support for lookarounds in RE2 (Cox, 2010), Hyperscan (Wang et al., 2019) and
the nonbacktracking engine in .NET to name a few optimized open source regex
libraries, it cannot be expressed concisely using an engine that does not
support lookaheads.

Now consider the following regular expression, composed of intersections which
we denote by the & symbol:

        .*[a-z].*&.*[A-Z].*&.*\d.*&[a-zA-Z\d]{8,}

The regular expression has a number of differences from the previous one.

  * •

The proposed regex engine will check for all four conditions at the same time,
without any backtracking.

  * •

Upon meeting one of the conditions, the rest of the alternation is matched
with one less condition to check. For example, after matching the lowercase
letter a at the beginning, the set [a-z] is satisfied, and the regex engine
will match the rest of the input with the regex
.*[A-Z].*&.*\d.*&[a-zA-Z\d]{7,}, by effectively removing the first condition
from the regex, as the remaining .* will be subsumed by the other
intersections. In Sections 4.2 and 5.1 we show how it is achieved.

  * •

Because all checks are performed together at the same position, intersections
allow precise text extraction in a single pass, which is also highly amenable
to parallelization in the form of vectorization. Such optimizations could be
beneficial for tasks such as scanning for potential credential leaks.

  * •

The pattern does not currently check for the validity of the entire string,
but it can be done by appending the intersection ^.*$ to the regex, which uses
lookarounds to constrain the regex to match the entire line. Similarly, the
regex could be constrained to match text between word borders by appending the
intersection \b\S*\b to the regex.

Now consider modifying the regular expression to find potential password
substrings while excluding certain ones, such as those having 2 consecutive
digits or the word ”password” in it. Such conditions cannot be checked
effectively with positive lookaheads but can be achieved with negative ones.
For example, the following regular expression uses negative lookaheads to
match a password that does not have 2 consecutive digits:

        .*[a-z].*&.*[A-Z].*&.*\d.*&(?!\S*\d\d)[a-zA-Z\d]{8,}

An important detail to point out here, is that in such regular expressions,
the ranges of the lookaheads and the loop are not necessarily the same. For
example, if there was something like "@11" on the same line, after the
occurrence of the potential match - it would be falsely considered a non-
match, as \S* travels further than [a-zA-Z\d]{8,}, while the loop would stop
at @.

A better way of writing the pattern would be to convert the negative lookahead
(?!\S*\d\d) to (?![a-zA-Z\d]*\d\d), that is, adjust the loop in the negative
lookahead to the entire following regular expression body, to guarantee that
the constraints apply to the same range. This is where the use of complement
(‘~‘) can help.

        .*[a-z].*&.*[A-Z].*&.*\d.*&[a-zA-Z\d]{8,}&~(.*\d\d.*)

The regex above is equivalent to the previous one, but it is constrained to
_the exact range of the potential match_ , as $\sim$(.*\d\d.*) remains
nullable exactly until two sequential digits are found, after which it turns
the entire intersection of regexes into $\bot$. The negation operator is
explained in detail in Section 4.2.

###### Example 2.2 (Incremental specification of regexes through composition).

Consider the following regex:

        .*A.*&.*B.*&.*C.*

The regex matches any line that contains the substrings A, B and C in any
order.

Now consider creating an equivalent regular expression without using
intersections. The result would be similar to the following:

        .*A.*B.*C.*|.*A.*C.*B.*|.*B.*A.*C.*|.*B.*C.*A.*|.*C.*A.*B.*|.*C.*B.*A.*

The regex is equivalent to the previous one, but it is much more verbose, as
it requires enumerating all possible permutations of the substrings as
separate alternatives. In such scenarios the use of intersection (&) becomes
very6 helpful. The number of alternations required is equal to the factorial
of the number of substrings.

Matching substrings A,B,C,D,E,F this way would require 720 alternations, while
the equivalent regex with intersections would only require 6 intersections.
Note that positive lookaheads can be used for such examples strictly as long
as it is possible to define a clear lookup range for all the substrings, which
is not always the case.

Another important advantage of intersections is that they are not interlinked
with each other, and can be added or removed independently. For example, if we
wanted to add a fourth substring D, we would only need to add one more
intersection, instead of adding 18 alternations and modifying the existing 6.
And if we wanted to remove the substring C, we would only need to remove one
intersection, instead of reducing and modifying all alternations down to 4.

Similarly, if we wanted exclude strings containing the substring D, we would
only need append the negated intersection $\sim$(.*D.*), instead of modifying
all existing alternations to exclude the substring D.

Such incremental aspect can be significant when dealing with large regexes,
and can be useful for tasks such as machine learning based text extraction
with regular expressions, where the regex is incrementally built by adding and
removing positive or negative intersection terms. Such approach also improves
the readability of regular expressions, as the regexes are built in a modular
way.

###### Example 2.3 (Matching paragraphs of text containing multiple
substrings).

Another practical use case for the new features is matching paragraphs of text
that meet certain conditions, as both intersection and negation introduce new
ways of matching ranges of text with complex conditions. While it is possible
to envisage sequential use of e.g. grep for positively and negatively matching
lines of text on the input string when each paragraph is on a separate line,
we generalize the example to paragraphs spanning over multiple lines and
paragraphs being separated by double newlines, as is often done in texts, e.g.
in Project Gutenberg books in plain text format. The example generalizes to
any substring start and end condition and provides a mechanism to also extract
the match in addition to checking for the existence of it.

Note that, for the sake of improved readability, we use the $\top$ predicate
to denote the set of all characters, which can be thought of as a canonical
representation of [\s\S] or [\w\W].

For example, consider the following regular expression:

\n\n$\sim$($\top$*\n\n$\top$*),

which effectively splits the text into ranges not containing two sequential
newlines, as it becomes nullable with two newlines, and remains nullable until
two newlines are found again, after which it becomes $\bot$. As negation does
not match at the position of the final newline, an additional \n can be
appended to include that as well.

After defining the previous construct, we can extend it with intersections to
match paragraphs containing certain substrings. For example, the following
regex matches paragraphs containing the substrings "King", "Paris" and
"English" in any order:

\n\n$\sim$($\top$*\n\n$\top$*)&$\top\texttt{*}$King$\top\texttt{*}$&$\top\texttt{*}$Paris$\top\texttt{*}$&$\top\texttt{*}$English$\top\texttt{*}$

A key advantage of the approach is that it is very easy to infer the starting
predicate of such a regex and skip to it, we have all the necessary contextual
information to do so. A regex that starts with $\top\texttt{*}$ essentially
means that you can skip taking derivatives until the starting predicate of the
tail of the regex matches. In the case of
$\top\texttt{*}$King$\top\texttt{*}$, the only valid predicate that changes
the state of this regex is $\psi_{\texttt{$K$}}$, after which the regex
becomes ing$\top\texttt{*}$|$\top\texttt{*}$King$\top\texttt{*}$, and the next
predicate always changes state, as the alternation ing$\top\texttt{*}$ either
continues matching in the case of $\psi_{\texttt{$i$}}$, or turns to $\bot$,
making it an ”unskippable” state.

Using such information from all intersections, we can skip taking derivatives
until we reach a starting predicate that changes the state of the regex, which
allows us to perform a vectorized string search procedure on any skippable
state of the regex. Such starting predicate lookup and skipping is explained
in more detail in Section 5.3.

Another feature, that is exclusively available in the proposed regex engine,
is the ability to define a matching range based on non-matching constraints.
For example matching a range of text starting with "King" and ending with
"Paris", that must not contain two sequential digits between each other can be
concisely expressed with the following regex:
King$\sim$($\top$*\d\d$\top$*)Paris which finds a match in "The King in
Paris", but not "The King 11 Paris". Using a negative lookahead for regexes
such as this, for example King(?!$\top\texttt{*}$?\d\d)$\top\texttt{*}$?Paris,
is very difficult, as the $\top\texttt{*}$ inside the lookahead will leak far
past the occurrence of Paris, making it incorrect if any two sequential digits
occur inside the text after the match.

###### Example 2.4 (Conditional matching).

Extending the previous example, let us try to locate a paragraph containing
the word “charity” only in the case the paragraph does not contain the word
“honor”. Such properties can be represented in terms of Boolean combinations
of the implication operation, which we, for now, represent in terms of
complement, union and intersection.

Let us first try to find all paragraphs that match the implication
$\mathtt{charity}\implies\mathtt{honor}$. When writing
`~(`$\top\texttt{*}$`\n\n`$\top\texttt{*}$`)&(~(`$\top\texttt{*}$charity$\top\texttt{*}$`)|(`$\top\texttt{*}$honor$\top\texttt{*}$`))`
the result is not yet precise enough, because the term
`~(`$\top\texttt{*}$`\n\n`$\top\texttt{*}$`)` stipulates that the match should
not contain two consecutive newlines, but there is no condition that tells
that the string _has_ to have double newlines before and after it. In the
Example 2.3 it worked because we did not use negative conditions, i.e. where
some word should not be contained in the match. Here we need to extend the
term for matching paragraphs by appropriate lookarounds as follows:

`(?<=\n\n|\A)~(`$\top\texttt{*}$`\n\n`$\top\texttt{*}$`)(?=\n\n|\Z)&(~(`$\top\texttt{*}$charity$\top\texttt{*}$`)|(`$\top\texttt{*}$honor$\top\texttt{*}$`))`

The result now matches all paragraphs where there is no word “charity” or
there exists a word “honor” (according to the definition of the standard
Boolean implication operation). To locate the paragraph where “charity” is
present, but “honor” is not, we need to take the complement of the implication
and write

`(?<=\n\n|\A)~(`$\top\texttt{*}$`\n\n`$\top\texttt{*}$`)(?=\n\n|\Z)&~(~(`$\top\texttt{*}$charity$\top\texttt{*}$`)|(`$\top\texttt{*}$honor$\top\texttt{*}$`))`

which in turn can be rewritten by applying de Morgan’s rule into

`(?<=\n\n|\A)~(`$\top\texttt{*}$`\n\n`$\top\texttt{*}$`)(?=\n\n|\Z)&(`$\top\texttt{*}$charity$\top\texttt{*}$`)&~(`$\top\texttt{*}$honor$\top\texttt{*}$`)`

The resulting regular expression matches the paragraph that contains the word
“charity” but does not contain “honor”.

It is possible to utilize the If-Then-Else conditionals
`(?(?=`$R_{1}$`)(`$R_{2}$`)|(`$R_{3}$`))` in traditional regex engines
supporting the construct. The explanation of If-Then-Else is nontrivial
(Friedl, 2006): $R_{1}$ acts as a test and if the test yields true then
$R_{2}$ gets applied, otherwise $R_{3}$. $R_{1}$ can either be a reference to
a capturing group and test if _the group participated in a match_ (which is
different from the actual match) or be a lookaround and yield a Boolean result
at a particular location. As mentioned before, there are differences in the
extent of the string in which lookarounds get evaluated and the extent of
loops, as was shown in the Example 2.1. As a result, writing a conditional
regular expression in terms of If-Then-Else corresponding to the above
requirements is error prone and requires a great deal of care. We argue that
the use of complement and intersection (and consequently a whole Boolean
algebra) together with lookarounds simplifies the task significantly.

We now proceed to establishing the theory for regular expressions extended
with lookarounds, complement and intersection.

##  3\. Preliminaries

Here we introduce the notation and main concepts used in the paper. The
general meta-notation, notation for denoting strings and locations is based on
the approach taken in (Moseley et al., 2023).

As a general meta-notation throughout the paper 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
$\Sigma$ be a domain of _characters_. $\langle{x,y}\rangle$ stands for pairs
of elements and let
$\pi_{1}(\langle{x,y}\rangle)\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}x$
and
$\pi_{2}(\langle{x,y}\rangle)\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}y$.

#### Strings.

Let $\epsilon$ or ”” denote the empty string and let $\Sigma^{*}$ denote the
set of all strings over $\Sigma$. Let $s\in\Sigma^{*}$. The length of $s$ is
denoted by $|s|$. Individual characters and strings of length 1 are not
distinguished. Let $i$ and $l$ be nonnegative integers such that $i+l\leq|s|$.
Then $s_{i,l}$ denotes the substring of $s$ that starts from index $i$ and has
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}$.
Let also
$s_{-1}=s_{|s|}\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}\epsilon$.
E.g.,
$\textrm{"}\texttt{abcde}\textrm{"}_{1,3}=\textrm{"}\texttt{bcd}\textrm{"}$
and $\textrm{"}\texttt{abcde}\textrm{"}_{5,0}=\epsilon$. $s^{r}\\!$ denotes
the _reverse_ of $s$, so that $s^{r}\\!_{i}=s_{|s|-1-i}$ for $0\leq i<|s|$.

#### Locations.

Let $s$ be a string. A _location in $s$_ is a pair $\langle{s,i}\rangle$,
where $-1\leq i\leq|s|$. We use $s\langle
i\rangle\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}\langle{s,i}\rangle$
as a dedicated notation for locations, where $s$ is the _string_ and $i$ the
_position_ of the location. Since $s\langle i\rangle$ is a pair, note also
that $\pi_{1}(s\langle i\rangle)=s$ and $\pi_{2}(s\langle i\rangle)=i$. If $x$
and $y$ are locations, then $x<y$ iff $\pi_{2}(x)<\pi_{2}(y)$. A location
$s\langle i\rangle$ is _valid_ if $0\leq i\leq|s|$. A location $s\langle
i\rangle$ is called _final_ if $i=|s|$ and _initial_ if $i=0$. Let
$\textit{Final}(s\langle
i\rangle)\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}i=|s|$
and $\textit{Initial}(s\langle
i\rangle)\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}i=0$.
We let
$\lightning\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}\epsilon\langle-1\rangle$
that is going to be used to represent _match failure_ and in general
$s\langle-1\rangle$ is used as a _pre-initial_ location. The _reverse_
$s\langle i\rangle^{r}\\!$ of a valid location $s\langle i\rangle$ in $s$ is
the valid location $s^{r}\\!\langle|s|{-}i\rangle$ in $s^{r}\\!$. For example,
the reverse of the final location in $s$ is the initial location in
$s^{r}\\!$. When working with sets $S$ of locations over the same string we
let $\max(S)$ ($\min(S)$) denote the maximum (minimum) location in the set
according to the location order above. In this context we also let
$\max(\emptyset)=\min(\emptyset)\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}\lightning$
and
$\lightning^{r}\\!\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}\lightning$.

Valid locations in a string $s$ can be illustrated by

$\begin{array}[]{ccccccccc}s\langle\\!0\\!\rangle&$\mbox{\Huge${s_{0}}$}$&s\langle\\!1\\!\rangle&$\mbox{\Huge${s_{1}}$}$&s\langle\\!2\\!\rangle&\cdots&s\langle\\!|s|\\!{-}\\!1\\!\rangle&$\mbox{\Huge${s_{|s|\\!-\\!1}}$}$&s\langle\\!|s|\\!\rangle\\\
\end{array}$

and should be interpreted as _border positions_ rather than character
positions. For example, $\epsilon$ has only one valid location
$\epsilon\langle 0\rangle$ that is both initial and final.

#### Boolean algebras as alphabet theories.

The tuple $\mathcal{A}=(\Sigma,\Psi,[[\\_]],\bot,\top,\vee,\wedge,\neg)$ is
called an _effective Boolean algebra over $\Sigma$_ 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_ or
$\textbf{SAT}(\varphi)$.

#### Character classes.

In all the examples below we let $\Sigma$ stand for the standard 16-bit
character set of Unicode333Also known as _Plane 0_ or the _Basic Multilingual
Plane_ of Unicode. and use the .NET syntax (Microsoft, 2021) of regular
expression character classes. For example, [A-Z] stands for all the Latin
capital letters, [0-9] for all the Latin numerals, \d for all the decimal
digits, \w for all the word-letters and dot (.) for all characters besides the
_newline character_ \n. (It is a standard convention that, by default, dot
does not match \n.). We also use the $\top$ predicate to denote the set of all
characters, which can be thought of as a canonical representation of [\s\S]
(or [\w\W]).

When we need to distinguish the concrete representation of character classes
from the corresponding abstract representation of predicates in $\mathcal{A}$
we map each character class $C$ to the corresponding predicate
$\psi_{\texttt{$C$}}$ in $\Psi$. For example $\psi_{\texttt{[\char 94\relax
0-9]}}\equiv\lnot\psi_{\texttt{[0-9]}}$, $\psi_{\texttt{{[{\char 92\relax
w}-[{\char 92\relax d}]]}}}\equiv\psi_{\texttt{{\char 92\relax
w}}}\land\lnot\psi_{\texttt{{\char 92\relax d}}}$, and $\psi_{\texttt{{\char
92\relax W}}}\equiv\lnot\psi_{\texttt{{\char 92\relax w}}}$. Observe also that
$[[\psi_{\texttt{[0-9]}}]]\subsetneq[[\psi_{\texttt{{\char 92\relax
d}}}]]\subsetneq[[\psi_{\texttt{{\char 92\relax w}}}]]$ and
$[[\psi_{\texttt{{\char 92\relax n}}}]]=\\{\texttt{\char 92\relax n}\\}$ and
$\texttt{\char 92\relax n}\notin[[\psi_{\texttt{{\char 92\relax w}}}]]$
because \n is not a word-letter. All predicates in $\Psi$ are represented in a
_canonical_ form in the implementation so that if $[[\varphi]]=[[\psi]]$ then
$\varphi=\psi$ by reusing the predicate algebra for Unicode Plane 0 that is
built-in into the .NET 7 runtime. In other words, character classes are only
used as the concrete notation, while, e.g., $\psi_{\texttt{{[{\char 92\relax
s}{\char 92\relax S}]}}}=\psi_{\texttt{{[{\char 92\relax w}{\char 92\relax
W}]}}}=\top$.

##  4\. Regexes with Lookarounds and Location Derivatives

Here we formally define regular expressions with _lookarounds_ and _loops_
supporting finite and infinite bounds. Regexes are defined modulo a character
theory $\mathcal{A}=(\Sigma,\Psi,[[\\_]],\bot,\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 irrelevant for the
purposes here where $\Sigma$ may even be infinite. After the definition of
regexes, we formally define a framework of _derivatives_ that leads to the key
notion of _derivation relation_ between locations that is used to prove
properties in this framework. We build on and extend definitions from (Moseley
et al., 2023) by incorporating _intersection_ , _complement_ , _loops_ , and
_lookarounds_ into a single unified theory of location derivatives and
matching.

###  4.1. Regexes

The class $\mathcal{R}$ of extended regular expressions with lookarounds, or
_regexes_ , is here defined by the following abstract grammar. Let
$\psi\in\Psi$, and $0\leq m\leq n\neq 0$, or $n=\infty$, and let $R$ range
over $\mathcal{R}$.

$\begin{array}[]{rcl}R&::=&\psi{\quad\mid\quad}\texttt{()}{\quad\mid\quad}R\mathbin{\texttt{|}}R^{\prime}{\quad\mid\quad}R\mathbin{\texttt{\&}}R^{\prime}{\quad\mid\quad}R\cdot
R^{\prime}{\quad\mid\quad}R\texttt{\\{}m{,n}\texttt{\\}}\quad{\mid}\quad\texttt{\char
126\relax}R\quad{\mid}\\\\[5.0pt]
&&\texttt{(?=}R\texttt{)}{\quad\mid\quad}\texttt{(?<=}R\texttt{)}{\quad\mid\quad}\texttt{(?!}R\texttt{)}{\quad\mid\quad}\texttt{(?<!}R\texttt{)}\end{array}$

where the operators in the first row appear in order of precedence, with
_union_ ($\mathbin{\texttt{|}}$) having lowest and _complement_ (~) having
highest precedence. The remaining operators in the first row are the _empty-
word regex_ (()), _intersection_ ($\mathbin{\texttt{\&}}$), _concatenation_
$(\cdot)$, and the _loop_ expression $R\texttt{\\{}m{,n}\texttt{\\}}$ where
$R$ is the _body_ , $m$ the _lower bound_ , and $n$ the _upper bound_ of the
loop. If $n=\infty$ then the loop is _infinite_ else _finite_. We let
$R\texttt{\\{}0{,0}\texttt{\\}}\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}\texttt{()}$
for convenience in recursive definitions. We use the common abbreviations
$R\texttt{*}$ for $R\texttt{\\{}0{,\infty}\texttt{\\}}$, $R\texttt{+}$ for
$R\texttt{\\{}1{,\infty}\texttt{\\}}$.

The regex denoting _nothing_ is just the predicate $\bot$. Concatenation
operator $\cdot$ is often implicit by using juxtaposition. The expressions in
the second row are called _lookarounds_ : $\texttt{(?=}R\texttt{)}$ is
_lookahead_ , $\texttt{(?<=}R\texttt{)}$ is _lookback_ ,
$\texttt{(?!}R\texttt{)}$ is _negative lookahead_ , and
$\texttt{(?<!}R\texttt{)}$ is _negative lookback_.

The _reverse_ $R^{r}\\!$ of $R\in\mathcal{R}$ is defined as follows:

$\begin{array}[]{rcl@{\quad}rcl}\psi^{r}\\!&\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}&\psi&\texttt{(?=}R\texttt{)}^{r}\\!&\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}&\texttt{(?<=}R^{r}\\!\texttt{)}\\\
\texttt{()}^{r}\\!&\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}&\texttt{()}&\texttt{(?<=}R\texttt{)}^{r}\\!&\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}&\texttt{(?=}R^{r}\\!\texttt{)}\\\
(R\mathbin{\texttt{|}}S)^{r}\\!&\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}&R^{r}\\!\mathbin{\texttt{|}}S^{r}\\!&\texttt{(?!}R\texttt{)}^{r}\\!&\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}&\texttt{(?<!}R^{r}\\!\texttt{)}\\\
(R\mathbin{\texttt{\&}}S)^{r}\\!&\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}&R^{r}\\!\mathbin{\texttt{\&}}S^{r}\\!&\texttt{(?<!}R\texttt{)}^{r}\\!&\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}&\texttt{(?!}R^{r}\\!\texttt{)}\\\
(R\cdot
S)^{r}\\!&\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}&S^{r}\\!\cdot
R^{r}\\!\\\
R\texttt{\\{}m{,n}\texttt{\\}}^{r}\\!&\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}&R^{r}\\!\texttt{\\{}m{,n}\texttt{\\}}\\\
(\texttt{\char
126\relax}R)^{r}\\!&\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}&\texttt{\char
126\relax}(R^{r}\\!)\end{array}$

Note that the reverse $R^{r}\\!$ of a regex $R$ has exactly the same size as
$R$. The size of a regex, $|R|$, is defined recursively as the number of
subexpressions, where each predicate $\psi\in\Psi$ is considered to have size
one, i.e., the actual representation size of predicates is irrelevant in this
context. It also follows by induction from the definition that
$(R^{r}\\!)^{r}\\!=R$.

###  4.2. Derivatives

In the following definition let $x=s\langle i\rangle$ be a valid nonfinal
location. For example, if $s=\textrm{"}\texttt{ab}\textrm{"}$ then the valid
nonfinal locations in $s$ are $s\langle 0\rangle$ and $s\langle 1\rangle$. In
the following let $\ell$ range over lookarounds. and let
$\infty{\stackrel{{{}_{\centerdot}}}{{-}}}1\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}\infty$,
$0{\stackrel{{{}_{\centerdot}}}{{-}}}1\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}0$,
and
$k{\stackrel{{{}_{\centerdot}}}{{-}}}1\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}k-1$
for $k>0$.

$\begin{array}[]{@{}rcl@{}}\partial_{x}(\texttt{()})&\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}&\bot\\\
\partial_{x}(\ell)&\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}&\bot\\\
\partial_{s\langle
i\rangle}(\psi)&\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}&\left\\{\begin{array}[]{@{}l@{\;}l}\texttt{()},&\mathbf{if}\,s_{i}\in[[\psi]];\\\
\bot,&\mathbf{otherwise}.\end{array}\right.\\\
\partial_{x}(R\mathbin{\texttt{|}}S)&\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}&\partial_{x}(R)\mathbin{\texttt{|}}\partial_{x}(S)\\\
\partial_{x}(R\mathbin{\texttt{\&}}S)&\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}&\partial_{x}(R)\mathbin{\texttt{\&}}\partial_{x}(S)\\\
\partial_{x}(\texttt{\char
126\relax}R)&\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}&\texttt{\char
126\relax}\partial_{x}(R)\\\
\partial_{x}(R{\cdot}S)&\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}&\left\\{\begin{array}[]{@{}l@{\;}l}\partial_{x}(R){\cdot}S{\mathbin{\texttt{|}}}\partial_{x}(S),&\mathbf{if}\,\mathit{Null}_{x}(R);\\\
\partial_{x}(R){\cdot}S,&\mathbf{otherwise}.\end{array}\right.\\\
\partial_{x}(R\texttt{\\{}m{,n}\texttt{\\}})&\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}&\left\\{\begin{array}[]{@{}l@{\;}l}\partial_{x}(R){\cdot}R\texttt{\\{}m{\stackrel{{{}_{\centerdot}}}{{-}}}1{,n{\stackrel{{{}_{\centerdot}}}{{-}}}1}\texttt{\\}},&\mathbf{if}\,m{=}0\mathrel{\mathbf{or}}\mathit{Null}_{\forall}(R){=}\mathbf{true}\mathrel{\mathbf{or}}\mathit{Null}_{x}(R){=}\mathbf{false};\\\
\partial_{x}(R{\cdot}R\texttt{\\{}m{\stackrel{{{}_{\centerdot}}}{{-}}}1{,n{\stackrel{{{}_{\centerdot}}}{{-}}}1}\texttt{\\}}),&\mathbf{otherwise}.\end{array}\right.\end{array}$

where
$\mathit{Null}_{\forall}(R)\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}\forall
x(\mathit{Null}_{x}(R)=\mathbf{true})$ intuitively means that $R$ is nullable
and nullability does not depend on lookarounds. Next we define nullability of
locations and what it means to find a match _end_ location from a valid
_start_ location $x$ in a string $s$ by a regex $R\in\mathcal{R}$.
$\textit{MatchEnd}(x,R)$ returns the _latest match end location_ from a valid
$x$ or $\lightning$ if none exists. Note that
$\max(x,\lightning)=\max(\lightning,x)=x$.

$\begin{array}[]{rcl}\textit{Null}^{\lightning}_{x}\\!(R)&\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}&\left\\{\begin{array}[]{@{}l@{\;}l}x,&\mathbf{if}\,\mathit{Null}_{x}(R);\\\
\lightning,&\mathbf{otherwise}.\end{array}\right.\\\
\textit{MatchEnd}(x,R)&\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}&\left\\{\begin{array}[]{@{}l@{\;}l}\textit{Null}^{\lightning}_{x}\\!(R),&\mathbf{if}\,\textit{Final}(x);\\\
\max(\textit{Null}^{\lightning}_{x}\\!(R),\textit{MatchEnd}(x{+}1,\partial_{x}(R))),&\mathbf{otherwise}.\end{array}\right.\\\
\textit{IsMatch}(x,R)&\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}&\textit{MatchEnd}(x,R)\neq\lightning\\\
\mathit{Null}_{x}(\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}\\\
\mathit{Null}_{x}(R\mathbin{\texttt{|}}R^{\prime})&\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}&\mathit{Null}_{x}(R)\mathrel{\mathbf{or}}\mathit{Null}_{x}(R^{\prime})\\\
\mathit{Null}_{x}(R\mathbin{\texttt{\&}}R^{\prime})&\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}&\mathit{Null}_{x}(R)\mathrel{\mathbf{and}}\mathit{Null}_{x}(R^{\prime})\\\
\mathit{Null}_{x}(R\cdot
R^{\prime})&\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}&\mathit{Null}_{x}(R)\mathrel{\mathbf{and}}\mathit{Null}_{x}(R^{\prime})\\\
\mathit{Null}_{x}(R\texttt{\\{}m{,n}\texttt{\\}})&\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}&m=0\mathrel{\mathbf{or}}\mathit{Null}_{x}(R)\\\
\mathit{Null}_{x}(\texttt{\char
126\relax}R)&\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}&\mathbf{not}\,\mathit{Null}_{x}(R)\\\
\mathit{Null}_{x}(\texttt{(?=}R\texttt{)})&\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}&\textit{IsMatch}(x,R)\\\
\mathit{Null}_{x}(\texttt{(?<=}R\texttt{)})&\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}&\textit{IsMatch}(x^{r}\\!,R^{r}\\!)\\\
\mathit{Null}_{x}(\texttt{(?!}R\texttt{)})&\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}&\mathbf{not}\,\textit{IsMatch}(x,R)\\\
\mathit{Null}_{x}(\texttt{(?<!}R\texttt{)})&\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}&\mathbf{not}\,\textit{IsMatch}(x^{r}\\!,R^{r}\\!)\end{array}$

Observe that the definition of $\textit{MatchEnd}(x,R)$ with $x=s\langle
i\rangle$ computes the transition from the source state (regex) $R$ to the
target state $S=\partial_{x}(R)$ for the character $s_{i}$ and then continues
matching from location $x+1$ and state $S$. The definition of derivatives and
IsMatch are mutually recursive, through nullability test of lookarounds. The
definition of $\mathit{Null}_{x}(\ell)$ of lookarounds $\ell$ is well-defined
because the regex $R$ in $\ell$ is a strictly smaller expression than $\ell$
and $R^{r}\\!$ has the same size as $R$.

The definition of $\textit{IsMatch}(x,R)$ terminates as soon as
$\mathit{Null}_{x}(R)=\mathbf{true}$. This is an obvious but important
optimization that is absent from the abstract definition above, along many
other common cases, to avoid redundant computation.

###  4.3. Derivation Relation

The key concept is the _derivation relation_
$x\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}y$ between locations, that is instrumental in reasoning about
properties of derivatives. Given a valid location $x$, the definition of _all
matches of $R$ from $x$_,
$({x}{\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}})$, is as follows.

$\begin{array}[]{r@{\;}c@{\;}l@{\quad}r@{\;}c@{\;}l}({x}{\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}})&\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}&\left\\{\begin{array}[]{@{}l@{\;}l}\textit{Null}^{\emptyset}_{x}(R),&\mathbf{if}\,\textit{Final}(x);\\\
\textit{Null}^{\emptyset}_{x}(R)\cup({x{+}1}{\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{@{}c@{}}\partial_{x}(R)\\\\[-2.79996pt]
\end{array}}$}}}),&\mathbf{otherwise}.\end{array}\right.&\textrm{where}\quad\textit{Null}^{\emptyset}_{x}(R)&\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}&\left\\{\begin{array}[]{@{}l@{\;}l}\\{x\\},&\mathbf{if}\,\mathit{Null}_{x}(R);\\\
\emptyset,&\mathbf{otherwise}.\end{array}\right.\\\
x\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}y&\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}&y\in({x}{\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}})\\\ \end{array}$

Two regexes $R$ and $S$ are _equivalent_ , denoted by $R\equiv S$, if, for all
locations $x$ and $y$,
$x\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}y\boldsymbol{\Leftrightarrow}x\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}y$. The following is the main derivation theorem that extends
(Moseley et al., 2023, Theorem 3.3). When $x$ is a final location we let
$({x{+}1}{\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}})\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}\emptyset$
for convenience in formal arguments. Note also that, for all $x$,
$({x}{\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}})=\emptyset$.

###### Theorem 1 (Derivation).

For all regexes and valid locations, let $\ell$ be a lookaround and
$\psi\in\Psi$:

  1. (1)

$x\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{@{}c@{}}\texttt{()}\\\\[-2.79996pt]
\end{array}}$}}y\boldsymbol{\Leftrightarrow}x=y$;

  2. (2)

$x\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}y\boldsymbol{\Leftrightarrow}\mathit{Null}_{x}(\ell)\mathrel{\mathbf{and}}x=y$;

  3. (3)

$s\langle
i\rangle\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}y\boldsymbol{\Leftrightarrow}s_{i}\in[[\psi]]\mathrel{\mathbf{and}}y=s\langle
i+1\rangle$;

  4. (4)

$x\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}y\boldsymbol{\Leftrightarrow}(x\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}y\mathrel{\mathbf{or}}x\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}y)$;

  5. (5)

$x\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}y\boldsymbol{\Leftrightarrow}(x\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}y\mathrel{\mathbf{and}}x\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}y)$;

  6. (6)

$x\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{@{}c@{}}\texttt{\char
126\relax}R\\\\[-2.79996pt]
\end{array}}$}}y\boldsymbol{\Leftrightarrow}\mathbf{not}\,(x\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}y)$;

  7. (7)

$x\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}y\boldsymbol{\Leftrightarrow}\exists
z(x\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}z\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}y)$;

  8. (8)

$\forall m>0:R\texttt{\\{}m{,n}\texttt{\\}}\equiv
R{\cdot}R\texttt{\\{}m-1{,n-1}\texttt{\\}}\equiv
R\texttt{\\{}m-1{,n-1}\texttt{\\}}{\cdot}R$;

  9. (9)

$R\texttt{\\{}0{,n}\texttt{\\}}\equiv
R\texttt{\\{}1{,n}\texttt{\\}}{\mathbin{\texttt{|}}}\texttt{()}$;

###### Proof.

1(1) follows from $\mathit{Null}_{x}(\texttt{()})=\mathbf{true}$,
$\partial_{x}(\texttt{()})=\bot$ and
$({x{+}1}{\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}})=\emptyset$.

#### Proof of 1(2)

We have that
$x\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}y$ iff
$y\in({x}{\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}})$ iff $y\in\textit{Null}^{\emptyset}_{x}(\ell)$ because
$\partial_{x}(\ell)=\bot$ and
$({x{+}1}{\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}})=\emptyset$. We also have that if $\mathit{Null}_{x}(\ell)$
then $\textit{Null}^{\emptyset}_{x}(\ell)=\\{x\\}$ else
$\textit{Null}^{\emptyset}_{x}(\ell)=\emptyset$.

#### Proof of 1(3)

Here $x=s\langle i\rangle$ is nonfinal. It follows that $s\langle
i\rangle\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}y$ iff
$y\in({x{+}1}{\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{@{}c@{}}\partial_{x}(\psi)\\\\[-2.79996pt]
\end{array}}$}}})$ iff $s_{i}\in[[\psi]]$ and
$y\in\textit{Null}^{\emptyset}_{x{+}1}(\texttt{()})$ iff $s_{i}\in[[\psi]]$
and $y=x{+}1=s\langle i{+}1\rangle$.

#### Proof of 1(4)

By induction over $\pi_{2}(y)-\pi_{2}(x)$ with $y$ fixed. If $x=y$ then

$\begin{array}[]{l}x\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}y\stackrel{{\scriptstyle(x=y)}}{{\boldsymbol{\Leftrightarrow}}}\mathit{Null}_{x}(R\mathbin{\texttt{|}}S)\boldsymbol{\Leftrightarrow}\mathit{Null}_{x}(R)\mathrel{\mathbf{or}}\mathit{Null}_{x}(S)\stackrel{{\scriptstyle(x=y)}}{{\boldsymbol{\Leftrightarrow}}}x\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}y\mathrel{\mathbf{or}}x\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}y\end{array}$

If $x<y$ then

$\begin{array}[]{rl}x\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}y\boldsymbol{\Leftrightarrow}x{+}1\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{@{}c@{}}\partial_{x}(R{\mathbin{\texttt{|}}}S)\\\\[-2.79996pt]
\end{array}}$}}y&\boldsymbol{\Leftrightarrow}x{+}1\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{@{}c@{}}\partial_{x}(R){\mathbin{\texttt{|}}}\partial_{x}(S)\\\\[-2.79996pt]
\end{array}}$}}y\\\
&\stackrel{{\scriptstyle\textsc{ih}}}{{\boldsymbol{\Leftrightarrow}}}x{+}1\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{@{}c@{}}\partial_{x}(R)\\\\[-2.79996pt]
\end{array}}$}}y\mathrel{\mathbf{or}}x{+}1\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{@{}c@{}}\partial_{x}(S)\\\\[-2.79996pt]
\end{array}}$}}y\boldsymbol{\Leftrightarrow}x\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}y\mathrel{\mathbf{or}}x\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}y\end{array}$

#### Proof of 1(5)

By induction over $\pi_{2}(y)-\pi_{2}(x)$ with $y$ fixed. For the base case
$x=y$ we get that

$\begin{array}[]{l}x\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}y\stackrel{{\scriptstyle(x=y)}}{{\boldsymbol{\Leftrightarrow}}}\mathit{Null}_{x}(R\mathbin{\texttt{\&}}S)\boldsymbol{\Leftrightarrow}\mathit{Null}_{x}(R)\mathrel{\mathbf{and}}\mathit{Null}_{x}(S)\stackrel{{\scriptstyle(x=y)}}{{\boldsymbol{\Leftrightarrow}}}x\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}y\mathrel{\mathbf{and}}x\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}y\end{array}$

For the induction case $x<y$ we get that

$\begin{array}[]{rl}x\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}y\stackrel{{\scriptstyle(x<y)}}{{\boldsymbol{\Leftrightarrow}}}x{+}1\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{@{}c@{}}\partial_{x}(R\mathbin{\texttt{\&}}S)\\\\[-2.79996pt]
\end{array}}$}}y&\boldsymbol{\Leftrightarrow}x{+}1\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{@{}c@{}}\partial_{x}(R)\mathbin{\texttt{\&}}\partial_{x}(S)\\\\[-2.79996pt]
\end{array}}$}}y\\\
&\stackrel{{\scriptstyle\textsc{(ih)}}}{{\boldsymbol{\Leftrightarrow}}}x{+}1\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{@{}c@{}}\partial_{x}(R)\\\\[-2.79996pt]
\end{array}}$}}y\mathrel{\mathbf{and}}x{+}1\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{@{}c@{}}\partial_{x}(S)\\\\[-2.79996pt]
\end{array}}$}}y\stackrel{{\scriptstyle(x<y)}}{{\boldsymbol{\Leftrightarrow}}}x\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}y\mathrel{\mathbf{and}}x\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}y\end{array}$

#### Proof of 1(6)

By induction over $\pi_{2}(y)-\pi_{2}(x)$. For the base case $x=y$ we get that

$\begin{array}[]{l}x\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{@{}c@{}}\texttt{\char
126\relax}R\\\\[-2.79996pt]
\end{array}}$}}y\stackrel{{\scriptstyle(x=y)}}{{\boldsymbol{\Leftrightarrow}}}\mathit{Null}_{x}(\texttt{\char
126\relax}R)\boldsymbol{\Leftrightarrow}\mathbf{not}(\mathit{Null}_{x}(R))\stackrel{{\scriptstyle(x=y)}}{{\boldsymbol{\Leftrightarrow}}}\mathbf{not}(x\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}y)\end{array}$

For the induction case $x<y$ we get that

$\begin{array}[]{l}x\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{@{}c@{}}\texttt{\char
126\relax}R\\\\[-2.79996pt]
\end{array}}$}}y\stackrel{{\scriptstyle(x<y)}}{{\boldsymbol{\Leftrightarrow}}}x+1\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{@{}c@{}}\partial_{x}(\texttt{\char
126\relax}R)\\\\[-2.79996pt]
\end{array}}$}}y\boldsymbol{\Leftrightarrow}x+1\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{@{}c@{}}\texttt{\char
126\relax}\partial_{x}(R)\\\\[-2.79996pt]
\end{array}}$}}y\stackrel{{\scriptstyle\textsc{(ih)}}}{{\boldsymbol{\Leftrightarrow}}}\mathbf{not}(x+1\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{@{}c@{}}\partial_{x}(R)\\\\[-2.79996pt]
\end{array}}$}}y)\stackrel{{\scriptstyle(x<y)}}{{\boldsymbol{\Leftrightarrow}}}\mathbf{not}(x\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}y)\end{array}$

#### Proof of 1(7)

by induction over $\pi_{2}(y)-\pi_{2}(x)$ with $y$ fixed. If $x=y$ then

$x\\!\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}\\!y\boldsymbol{\Leftrightarrow}y\in\textit{Null}^{\emptyset}_{x}(R{\cdot}S)\boldsymbol{\Leftrightarrow}(y\in\textit{Null}^{\emptyset}_{x}(R)\mathrel{\mathbf{and}}y\in\textit{Null}^{\emptyset}_{x}(S))\boldsymbol{\Leftrightarrow}(x\\!\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}\\!y\\!\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}\\!y)\boldsymbol{\Leftrightarrow}\exists
z(x\\!\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}\\!z\\!\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}\\!y)$

Observe that $z$ in the last ‘$\boldsymbol{\Leftrightarrow}$’ must be $x$
because
$x\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}z\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}x$ implies that $x\leq z\leq x$. If $x<y$ then, by case
analysis over $\mathit{Null}_{x}(R)$, if $\mathit{Null}_{x}(R)=\mathbf{false}$
then

$\displaystyle
x\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}y\boldsymbol{\Leftrightarrow}x{+}1\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{@{}c@{}}\partial_{x}(R{\cdot}S)\\\\[-2.79996pt]
\end{array}}$}}y\boldsymbol{\Leftrightarrow}x{+}1\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{@{}c@{}}\partial_{x}(R){\cdot}S\\\\[-2.79996pt]
\end{array}}$}}y\stackrel{{\scriptstyle\textsc{ih}}}{{\boldsymbol{\Leftrightarrow}}}\exists
z(x{+}1\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{@{}c@{}}\partial_{x}(R)\\\\[-2.79996pt]
\end{array}}$}}z\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}y)\boldsymbol{\Leftrightarrow}\exists
z(x\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}z\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}y)$

In the last ‘$\boldsymbol{\Leftrightarrow}$’ above
$\mathit{Null}_{x}(R)=\mathbf{false}$ so $x{+}1\leq z$. If
$\mathit{Null}_{x}(R)=\mathbf{true}$ then

$\begin{array}[]{rcl}x\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}y&\boldsymbol{\Leftrightarrow}&x{+}1\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{@{}c@{}}\partial_{x}(R){\cdot}S{\mathbin{\texttt{|}}}\partial_{x}(S)\\\\[-2.79996pt]
\end{array}}$}}y\\\ &\stackrel{{\scriptstyle\textrm{by
\ref{thm:DERS}(\ref{thm:DERS:d})}}}{{\boldsymbol{\Leftrightarrow}}}&x{+}1\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{@{}c@{}}\partial_{x}(R){\cdot}S\\\\[-2.79996pt]
\end{array}}$}}y\mathrel{\mathbf{or}}x{+}1\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{@{}c@{}}\partial_{x}(S)\\\\[-2.79996pt]
\end{array}}$}}y\\\
&\stackrel{{\scriptstyle\textsc{ih}}}{{\boldsymbol{\Leftrightarrow}}}&\exists
z(x{+}1\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{@{}c@{}}\partial_{x}(R)\\\\[-2.79996pt]
\end{array}}$}}z\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}y)\mathrel{\mathbf{or}}x{+}1\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{@{}c@{}}\partial_{x}(S)\\\\[-2.79996pt]
\end{array}}$}}y\\\
&\stackrel{{\scriptstyle(x<y)}}{{\boldsymbol{\Leftrightarrow}}}&\exists
z(x{+}1\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{@{}c@{}}\partial_{x}(R)\\\\[-2.79996pt]
\end{array}}$}}z\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}y)\mathrel{\mathbf{or}}x\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}y\\\ &\boldsymbol{\Leftrightarrow}&\exists
z{>}x(x\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}z\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}y)\mathrel{\mathbf{or}}x\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}y\\\
&\stackrel{{\scriptstyle\mathit{Null}_{x}(R)=\mathbf{true}}}{{\boldsymbol{\Leftrightarrow}}}&\exists
z(x\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}z\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}y)\end{array}$

#### Proof of 1(8).

Let $L=R\texttt{\\{}m{,n}\texttt{\\}}$ where $m>0$. We prove the statement by
proving (for all $m$ and $n$)

$x\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}y\boldsymbol{\Leftrightarrow}x\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{@{}c@{}}R{\cdot}(L-1)\\\\[-2.79996pt]
\end{array}}$}}y$

The statement holds trivially when $m=n=1$. Assume $n>1$.

We prove the statement by induction over $\pi_{2}(y)-\pi_{2}(x)$. In each
induction step we also get, by using the IH, that $R(L-1)\equiv
R((L-2)R)\equiv(R(L-2))R\equiv(L-1)R$, where $(L-2)$ is well-defined because
$n>1$.

The case $\mathit{Null}_{\forall}(R)=\mathbf{false}$ but
$\mathit{Null}_{x}(R)=\mathbf{true}$ then
$\partial_{x}(L)=\partial_{x}(R{\cdot}(L-1))$ by definition. If
$\mathit{Null}_{x}(R)=\mathbf{false}$ then
$\partial_{x}(L)=\partial_{x}(R){\cdot}(L-1)$ but then also
$\partial_{x}(R{\cdot}(L-1))=\partial_{x}(R){\cdot}(L-1)$. So, in either case
it follows that $L\equiv R{\cdot}(L-1)$ without induction.

The remaining case is $\mathit{Null}_{\forall}(R)=\mathbf{true}$. The base
case of $x=y$ follows directly because $x=y$ iff
$\mathit{Null}_{x}(R)=\mathbf{true}$ iff $\mathit{Null}_{x}(L)$ iff
$\mathit{Null}_{x}(R{\cdot}(L-1))$.

For the induction case Let $x<y$. If $m>1$ then let $L^{\prime}=(L-1)$ else if
$m=1$, using that $R\texttt{\\{}0{,k}\texttt{\\}}\equiv
R\texttt{\\{}1{,k}\texttt{\\}}$ when
$\mathit{Null}_{\forall}(R)=\mathbf{true}$, let
$L^{\prime}=R\texttt{\\{}1{,n-1}\texttt{\\}}$ in order to maintain that the
lower bound remains positive. Observe that the induction is over
$\pi_{2}(y)-\pi_{2}(x)$ and in the induction steps there exists $z\geq x+1$
such that
$z\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}y$ where $\pi_{2}(y)-\pi_{2}(z)<\pi_{2}(y)-\pi_{2}(x)$.

$\begin{array}[]{rcl}x\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{@{}c@{}}R{\cdot}(L-1)\\\\[-2.79996pt]
\end{array}}$}}y&\boldsymbol{\Leftrightarrow}&x{+}1\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{@{}c@{}}\partial_{x}(R{\cdot}{L^{\prime}})\\\\[-2.79996pt]
\end{array}}$}}y\\\
&\boldsymbol{\Leftrightarrow}&x{+}1\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{@{}c@{}}\partial_{x}(R){\cdot}{L^{\prime}}\mathbin{\texttt{|}}\partial_{x}(L^{\prime})\\\\[-2.79996pt]
\end{array}}$}}y\\\
&\boldsymbol{\Leftrightarrow}&x{+}1\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{@{}c@{}}\partial_{x}(R){\cdot}{L^{\prime}}\\\\[-2.79996pt]
\end{array}}$}}y\mathrel{\mathbf{or}}x{+}1\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{@{}c@{}}\partial_{x}(L^{\prime})\\\\[-2.79996pt]
\end{array}}$}}y\\\
&\stackrel{{\scriptstyle\textsc{(ih)}}}{{\boldsymbol{\Leftrightarrow}}}&x{+}1\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{@{}c@{}}\partial_{x}(R){\cdot}(L-2){\cdot}R\\\\[-2.79996pt]
\end{array}}$}}y\mathrel{\mathbf{or}}x{+}1\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{@{}c@{}}\partial_{x}(L^{\prime})\\\\[-2.79996pt]
\end{array}}$}}y\\\
&\boldsymbol{\Leftrightarrow}&x{+}1\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{@{}c@{}}\partial_{x}(L^{\prime}){\cdot}R\\\\[-2.79996pt]
\end{array}}$}}y\mathrel{\mathbf{or}}x{+}1\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{@{}c@{}}\partial_{x}(L^{\prime})\\\\[-2.79996pt]
\end{array}}$}}y\\\
&\stackrel{{\scriptstyle\mathit{Null}_{\forall}(R)}}{{\boldsymbol{\Leftrightarrow}}}&x{+}1\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{@{}c@{}}\partial_{x}(L^{\prime}){\cdot}R\\\\[-2.79996pt]
\end{array}}$}}y\\\
&\boldsymbol{\Leftrightarrow}&x{+}1\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{@{}c@{}}\partial_{x}(R){\cdot}(L-2){\cdot}R\\\\[-2.79996pt]
\end{array}}$}}y\\\
&\stackrel{{\scriptstyle\textsc{(ih)}}}{{\boldsymbol{\Leftrightarrow}}}&x{+}1\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{@{}c@{}}\partial_{x}(R){\cdot}(L^{\prime})\\\\[-2.79996pt]
\end{array}}$}}y\\\
&\boldsymbol{\Leftrightarrow}&x\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}y\end{array}$

#### Proof of 1(9)

for the case of $\mathit{Null}_{\forall}(R)=\mathbf{true}$ is similar to the
proof of 1(8) and observe that in this case $R\equiv
R{\mathbin{\texttt{|}}}\texttt{()}$. Assume
$\mathit{Null}_{\forall}(R)=\mathbf{false}$. Then for
$\mathit{Null}_{x}(R)=\mathbf{true}$ or $\mathit{Null}_{x}(R)=\mathbf{false}$
the proof follows directly because in either case
$\partial_{x}(R\texttt{\\{}0{,n}\texttt{\\}})=\partial_{x}(R{\cdot}R\texttt{\\{}0{,n-1}\texttt{\\}})$:

$x\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{@{}c@{}}R\texttt{\\{}0{,n}\texttt{\\}}\\\\[-2.79996pt]
\end{array}}$}}y\boldsymbol{\Leftrightarrow}x+1\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{@{}c@{}}\partial_{x}(R{\cdot}R\texttt{\\{}0{,n-1}\texttt{\\}})\\\\[-2.79996pt]
\end{array}}$}}y\mathrel{\mathbf{or}}x\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{@{}c@{}}\texttt{()}\\\\[-2.79996pt]
\end{array}}$}}y\boldsymbol{\Leftrightarrow}x\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{@{}c@{}}R{\cdot}R\texttt{\\{}0{,n-1}\texttt{\\}}\mathbin{\texttt{|}}\texttt{()}\\\\[-2.79996pt]
\end{array}}$}}y$

where $R{\cdot}R\texttt{\\{}0{,n-1}\texttt{\\}}\equiv
R\texttt{\\{}1{,n}\texttt{\\}}$ by 1(8). The theorem follows by the induction
principle over long distances. ∎ It is possible to prove Theorem 1 by
induction over $R$ but the proof becomes much more involved, while using
induction over location distances takes full advantage of the definition of
location derivatives. We get the following key characterization of
$\mathcal{R}$ as a corollary of Theorem 1. Let

$\begin{array}[]{rcl}\mathcal{U}&\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}&\\{\langle{s\langle
i\rangle,s\langle j\rangle}\rangle\mid s\in\Sigma^{*},0\leq i\leq
j\leq|s|\\}\\\ \langle{x,y}\rangle\models
R&\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}&x\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}y\quad\textrm{for}\;\langle{x,y}\rangle\in\mathcal{U}\\\
\mathcal{M}(R)&\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}&\\{M\in\mathcal{U}\mid
M\models R\\}\end{array}$

We say that $M\in\mathcal{U}$ is a _match_ of $R$ if $M\models R$, and
$\mathcal{M}(R)$ is called the _match set_ or _match sematics_ of $R$. Observe
that $R\equiv S\boldsymbol{\Leftrightarrow}\mathcal{M}(R)=\mathcal{M}(S)$.

###### Corollary 1.

$\mathfrak{M}=(\mathcal{U},\mathcal{R},\mathcal{M},\bot,\top\texttt{*},\mathbin{\texttt{|}},\mathbin{\texttt{\&}},\texttt{\char
126\relax})$ is an effective Boolean algebra over $\mathcal{U}$.

###### Proof.

Recall that _complement_ of $X\subseteq\mathcal{U}$ in $\mathfrak{M}$ is
$\complement(X)\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}\mathcal{U}\setminus
X$. It holds that $\mathcal{M}(\bot)=\emptyset$ and
$\mathcal{M}(\top\texttt{*})=\mathcal{U}$. Theorem 1(4) implies that
$\mathcal{M}(R\mathbin{\texttt{|}}S)=\mathcal{M}(R)\cup\mathcal{M}(S)$.
Theorem 1(5) implies that
$\mathcal{M}(R\mathbin{\texttt{\&}}S)=\mathcal{M}(R)\cap\mathcal{M}(S)$.
Theorem 1(6) implies that $\mathcal{M}(\texttt{\char
126\relax}R)=\complement(\mathcal{M}(R))$. ∎

Corollary 1 is a powerful tool that allows us to apply laws of distributivity
and de Morgan’s laws in order to rewrite regexes into various normal forms and
to simplify regexes based on other general laws of Boolean algebras as well as
specific laws of $\mathfrak{M}$ in combination with the laws of Kleene-star
and concatenation. For example, it follows from Theorem 1 that $\texttt{\char
126\relax}\bot\equiv\top\texttt{*}$, $\texttt{\char
126\relax}\texttt{()}\equiv\top\texttt{+}$,
$\top\texttt{*}\mathbin{\texttt{\&}}R\equiv R$, and thus for example that
$\partial_{x}(\texttt{\char
126\relax}\texttt{()}\mathbin{\texttt{\&}}R)\equiv\partial_{x}(\top\texttt{+})\mathbin{\texttt{\&}}\partial_{x}(R)=\top\texttt{*}\mathbin{\texttt{\&}}\partial_{x}(R)\equiv\partial_{x}(R)$.

###  4.4. Reversal Theorem

Reversal of regexes plays a key role in the top-level matching algorithm,
where it is used to locate the start location of a match backwards from the
end location (provided that the end location exists). Here our focus is on
reversal itself and we extend (Moseley et al., 2023, Theorem 3.8). We make use
of the following basic semantic fact of lookbacks.

###### Lemma 1.

Let $R\in\mathcal{R}$ and $x$ be a valid location. Then
$\mathit{Null}_{x}(\texttt{(?<=}R\texttt{)})\boldsymbol{\Leftrightarrow}\exists
z:z\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}x$.

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

For all $R\in\mathcal{R}$ and valid locations $x$ and $y$:

  1. (1)

$\mathit{Null}_{x}(R)\boldsymbol{\Leftrightarrow}\mathit{Null}_{x^{r}\\!}(R^{r}\\!)$

  2. (2)

$x\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}y\boldsymbol{\Leftrightarrow}y^{r}\\!\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{@{}c@{}}R^{r}\\!\\\\[-2.79996pt]
\end{array}}$}}x^{r}\\!$.

###### Proof.

The proof uses Theorem 1 and is by induction over
$(|R|,\pi_{2}(y)-\pi_{2}(x))$ where $(|S|,d)<(|R|,e)$ if either $|S|<|R|$ or
$|S|=|R|$ and $d<e$. For loops
$|X\texttt{\\{}m{,n}\texttt{\\}}|<|X\texttt{\\{}m^{\prime}{,n^{\prime}}\texttt{\\}}|$
when either $m<m^{\prime}$ or else $m=m^{\prime}$ and $n<n^{\prime}$.
Induction uses $\pi_{2}(y)-\pi_{2}(x)$ only when $R=X\texttt{*}$. (Recall also
that
$R\texttt{\\{}0{,0}\texttt{\\}}\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}\texttt{()}$.)
Let $x=s\langle i\rangle$ be a valid location.

The proof of (1) follows from (2) in all induction cases except when $R$ is a
lookaround where (1) is proved by using the IH of (2).

#### Base case $R=\texttt{()}$

Follows from $\texttt{()}^{r}\\!=\texttt{()}$.

#### Base case $R=\psi$

Here $x$ is _nonfinal_ so $x+1$ is valid. We get that
$x\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}y\boldsymbol{\Leftrightarrow}y^{r}\\!\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{@{}c@{}}\psi^{r}\\!\\\\[-2.79996pt]
\end{array}}$}}x^{r}\\!$ by Thm 1(3) because $x+1=y$ iff $y^{r}\\!+1=x^{r}\\!$
and $\psi^{r}\\!=\psi$, where $y^{r}\\!=s\langle
i+1\rangle^{r}\\!=s^{r}\\!\langle|s|-i-1\rangle$ and
$s^{r}\\!_{|s|-i-1}=s_{i}$, so $s_{i}\in[[\psi]]$ iff
$s^{r}\\!_{|s|-i-1}\in[[\psi^{r}\\!]]$. Note also that
$\mathit{Null}_{x}(\psi)=\mathit{Null}_{x^{r}\\!}(\psi^{r}\\!)=\mathit{Null}_{x^{r}\\!}(\psi)=\mathbf{false}$.

#### Induction case $R$ is a lookback

Let $R=\texttt{(?<=}S\texttt{)}$.

$\mathit{Null}_{x}(R)\stackrel{{\scriptstyle\textsc{(Lma~{}\ref{lma:lb})}}}{{\boldsymbol{\Leftrightarrow}}}\exists
z:z\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}x\stackrel{{\scriptstyle\textsc{(ih)}}}{{\boldsymbol{\Leftrightarrow}}}\exists
z:x^{r}\\!\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{@{}c@{}}S^{r}\\!\\\\[-2.79996pt]
\end{array}}$}}z^{r}\\!\boldsymbol{\Leftrightarrow}\textit{IsMatch}(x^{r}\\!,S^{r}\\!)\boldsymbol{\Leftrightarrow}\mathit{Null}_{x^{r}\\!}(\texttt{(?=}S^{r}\\!\texttt{)})\boldsymbol{\Leftrightarrow}\mathit{Null}_{x^{r}\\!}(R^{r}\\!)$

It follows also that
$x\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}y\boldsymbol{\Leftrightarrow}y^{r}\\!\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{@{}c@{}}R^{r}\\!\\\\[-2.79996pt]
\end{array}}$}}x^{r}\\!$ because
$x\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}y\boldsymbol{\Leftrightarrow}(\mathit{Null}_{x}(R)\mathrel{\mathbf{and}}x=y)$.
The proof of the negative lookback is similar because
$\mathit{Null}_{x}(\texttt{(?<!}S\texttt{)})\boldsymbol{\Leftrightarrow}\mathbf{not}\,\mathit{Null}_{x}(\texttt{(?<=}S\texttt{)})$.

#### Induction case $R$ is a lookahead

Let $R=\texttt{(?=}S\texttt{)}$.

$\mathit{Null}_{x}(R)\boldsymbol{\Leftrightarrow}\textit{IsMatch}(x,S)\boldsymbol{\Leftrightarrow}\exists
z:x\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}z\stackrel{{\scriptstyle\textsc{(ih)}}}{{\boldsymbol{\Leftrightarrow}}}\exists
z:z^{r}\\!\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{@{}c@{}}S^{r}\\!\\\\[-2.79996pt]
\end{array}}$}}x^{r}\\!\stackrel{{\scriptstyle\textsc{(Lma~{}\ref{lma:lb})}}}{{\boldsymbol{\Leftrightarrow}}}\mathit{Null}_{x^{r}\\!}(\texttt{(?<=}S^{r}\\!\texttt{)})\boldsymbol{\Leftrightarrow}\mathit{Null}_{x^{r}\\!}(R^{r}\\!)$

It follows also that
$x\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}y\boldsymbol{\Leftrightarrow}y^{r}\\!\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{@{}c@{}}R^{r}\\!\\\\[-2.79996pt]
\end{array}}$}}x^{r}\\!$. The proof of the negative lookahead is similar
because
$\mathit{Null}_{x}(\texttt{(?!}S\texttt{)})\boldsymbol{\Leftrightarrow}\mathbf{not}\,\mathit{Null}_{x}(\texttt{(?=}S\texttt{)})$.

#### Induction case $R=X\\!{\mathbin{\texttt{|}}}\\!Y$

Then

$x\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}y\stackrel{{\scriptstyle\textsc{Thm~{}\ref{thm:DERS}(\ref{thm:DERS:d})}}}{{\boldsymbol{\Leftrightarrow}}}x\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}y\mathrel{\mathbf{or}}x\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}y\stackrel{{\scriptstyle\textsc{(ih)}}}{{\boldsymbol{\Leftrightarrow}}}y^{r}\\!\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{@{}c@{}}X^{r}\\!\\\\[-2.79996pt]
\end{array}}$}}x^{r}\\!\mathrel{\mathbf{or}}y^{r}\\!\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{@{}c@{}}Y^{r}\\!\\\\[-2.79996pt]
\end{array}}$}}x^{r}\\!\stackrel{{\scriptstyle\textsc{Thm~{}\ref{thm:DERS}(\ref{thm:DERS:d})}}}{{\boldsymbol{\Leftrightarrow}}}y^{r}\\!\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{@{}c@{}}X^{r}\\!{\mathbin{\texttt{|}}}Y^{r}\\!\\\\[-2.79996pt]
\end{array}}$}}x^{r}\\!\boldsymbol{\Leftrightarrow}y^{r}\\!\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{@{}c@{}}R^{r}\\!\\\\[-2.79996pt]
\end{array}}$}}x^{r}\\!$

#### Induction case $R=X{\mathbin{\texttt{\&}}}Y$

Then

$x\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}y\stackrel{{\scriptstyle\textsc{Thm~{}\ref{thm:DERS}(\ref{thm:DERS:i})}}}{{\boldsymbol{\Leftrightarrow}}}x\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}y\mathrel{\mathbf{and}}x\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}y\stackrel{{\scriptstyle\textsc{(ih)}}}{{\boldsymbol{\Leftrightarrow}}}y^{r}\\!\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{@{}c@{}}X^{r}\\!\\\\[-2.79996pt]
\end{array}}$}}x^{r}\\!\mathrel{\mathbf{and}}y^{r}\\!\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{@{}c@{}}Y^{r}\\!\\\\[-2.79996pt]
\end{array}}$}}x^{r}\\!\stackrel{{\scriptstyle\textsc{Thm~{}\ref{thm:DERS}(\ref{thm:DERS:i})}}}{{\boldsymbol{\Leftrightarrow}}}y^{r}\\!\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{@{}c@{}}X^{r}\\!\mathbin{\texttt{\&}}Y^{r}\\!\\\\[-2.79996pt]
\end{array}}$}}x^{r}\\!\boldsymbol{\Leftrightarrow}y^{r}\\!\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{@{}c@{}}R^{r}\\!\\\\[-2.79996pt]
\end{array}}$}}x^{r}\\!$

#### Induction case $R=\texttt{\char 126\relax}X$

Then

$x\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}y\stackrel{{\scriptstyle\textsc{Thm~{}\ref{thm:DERS}(\ref{thm:DERS:n})}}}{{\boldsymbol{\Leftrightarrow}}}\mathbf{not}(x\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}y)\stackrel{{\scriptstyle\textsc{(ih)}}}{{\boldsymbol{\Leftrightarrow}}}\mathbf{not}(y^{r}\\!\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{@{}c@{}}X^{r}\\!\\\\[-2.79996pt]
\end{array}}$}}x^{r}\\!)\stackrel{{\scriptstyle\textsc{Thm~{}\ref{thm:DERS}(\ref{thm:DERS:n})}}}{{\boldsymbol{\Leftrightarrow}}}y^{r}\\!\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{@{}c@{}}\texttt{\char
126\relax}(X^{r}\\!)\\\\[-2.79996pt]
\end{array}}$}}x^{r}\\!\boldsymbol{\Leftrightarrow}y^{r}\\!\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{@{}c@{}}R^{r}\\!\\\\[-2.79996pt]
\end{array}}$}}x^{r}\\!$

#### Induction case $R=X{\cdot}Y$

Then

$x\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}y\stackrel{{\scriptstyle\textsc{Thm~{}\ref{thm:DERS}(\ref{thm:DERS:c})}}}{{\boldsymbol{\Leftrightarrow}}}\exists
z(x\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}z\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}y)\stackrel{{\scriptstyle\textsc{(ih)}}}{{\boldsymbol{\Leftrightarrow}}}\exists
z(y^{r}\\!\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{@{}c@{}}Y^{r}\\!\\\\[-2.79996pt]
\end{array}}$}}z^{r}\\!\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{@{}c@{}}X^{r}\\!\\\\[-2.79996pt]
\end{array}}$}}x^{r}\\!)\stackrel{{\scriptstyle\textsc{Thm~{}\ref{thm:DERS}(\ref{thm:DERS:c})}}}{{\boldsymbol{\Leftrightarrow}}}y^{r}\\!\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{@{}c@{}}Y^{r}\\!{\cdot}X^{r}\\!\\\\[-2.79996pt]
\end{array}}$}}x^{r}\\!\boldsymbol{\Leftrightarrow}y^{r}\\!\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{@{}c@{}}R^{r}\\!\\\\[-2.79996pt]
\end{array}}$}}x^{r}\\!$

#### Induction case $R=X\texttt{\\{}m{,n}\texttt{\\}}$ ($m>0$)

Then

$x\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}y\stackrel{{\scriptstyle\textsc{Thm~{}\ref{thm:DERS}(\ref{thm:DERS:c},\ref{thm:DERS:g})}}}{{\boldsymbol{\Leftrightarrow}}}\exists
z(x\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}z\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}y)\stackrel{{\scriptstyle\textsc{(ih)}}}{{\boldsymbol{\Leftrightarrow}}}\exists
z(y^{r}\\!\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{@{}c@{}}R^{r}\\!-1\\\\[-2.79996pt]
\end{array}}$}}z^{r}\\!\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{@{}c@{}}X^{r}\\!\\\\[-2.79996pt]
\end{array}}$}}x^{r}\\!)\stackrel{{\scriptstyle\textsc{Thm~{}\ref{thm:DERS}(\ref{thm:DERS:c},\ref{thm:DERS:g})}}}{{\boldsymbol{\Leftrightarrow}}}y^{r}\\!\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{@{}c@{}}R^{r}\\!\\\\[-2.79996pt]
\end{array}}$}}x^{r}\\!$

#### Induction case $R=X\texttt{\\{}0{,n}\texttt{\\}}$

Then, by using Thm 1(8,9,7,2),

$\begin{array}[]{rcl}x\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}y&\boldsymbol{\Leftrightarrow}&\exists
z(x\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}z\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}y)\mathrel{\mathbf{or}}x\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{@{}c@{}}\texttt{()}\\\\[-2.79996pt]
\end{array}}$}}y\\\
&\stackrel{{\scriptstyle\textsc{(ih)}}}{{\boldsymbol{\Leftrightarrow}}}&\exists
z(y^{r}\\!\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{@{}c@{}}R^{r}\\!-1\\\\[-2.79996pt]
\end{array}}$}}z^{r}\\!\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{@{}c@{}}X^{r}\\!\\\\[-2.79996pt]
\end{array}}$}}x^{r}\\!)\mathrel{\mathbf{or}}y^{r}\\!\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{@{}c@{}}\texttt{()}\\\\[-2.79996pt]
\end{array}}$}}x^{r}\\!\\\
&\boldsymbol{\Leftrightarrow}&y^{r}\\!\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{@{}c@{}}(R^{r}\\!-1){\cdot}X^{r}\\!\mathbin{\texttt{|}}\texttt{()}\\\\[-2.79996pt]
\end{array}}$}}x^{r}\\!\\\
&\boldsymbol{\Leftrightarrow}&y^{r}\\!\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{@{}c@{}}X^{r}\\!\texttt{\\{}1{,n}\texttt{\\}}\mathbin{\texttt{|}}\texttt{()}\\\\[-2.79996pt]
\end{array}}$}}x^{r}\\!\\\
&\boldsymbol{\Leftrightarrow}&y^{r}\\!\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{@{}c@{}}R^{r}\\!\\\\[-2.79996pt]
\end{array}}$}}x^{r}\\!\end{array}$

where $\pi_{2}(y)-\pi_{2}(z)<\pi_{2}(y)-\pi_{2}(x)$ when
$\mathit{Null}_{x}(X)=\mathbf{false}$ and $n=\infty$, so the IH applies. If
$R=X\texttt{*}$ and $\mathit{Null}_{x}(X)=\mathbf{true}$ then the case $x=y$
is immediate. Otherwise $x<y$ and we may assume that any “stuttering” steps
$x\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}x$ are omitted from the derivation because they do not
contribute to completing the derivation that is finite and bounded by
$\pi_{2}(y)-\pi_{2}(x)$. Then the IH applies because then $z\geq x+1$. ∎

###  4.5. Anchors as Lookarounds

All anchors can be defined by lookarounds as was conjectured in (Moseley et
al., 2023, Section 3.7). In our implementation all the standard anchors are
defined by using lookarounds. Many other custom anchors can be defined with
lookarounds, e.g., to support different line separators besides \n such as
\r\n for different file formats, or to support anchors for detecting enclosing
parentheses.

Table 1. Standard anchors in regexes and their definitions by lookarounds relative to a valid location $s\langle i\rangle$. | Name | Definition | Effective meaning
---|---|---|---
\A | start | $\texttt{(?<!}\top\texttt{)}$ |  _initial_ location of input ($i=0$)
\z | end | $\texttt{(?!}\top\texttt{)}$ |  _final_ location of input ($i=|s|$)
^ | start-of-line | (\A|(?<=\n)) |  $i=0$ or $s_{i-1}=\texttt{\char 92\relax n}$
$ | end-of-line | (\z|(?=\n)) |  $i=|s|$ or $s_{i}=\texttt{\char 92\relax n}$
\Z | end-or-last-$ | (\z|(?=\n${\cdot}$\z)) |  $i=|s|$ or $i=|s|{-}1$ and $s_{i}=\texttt{\char 92\relax n}$
\b | word-border | $\texttt{(?<=}\texttt{\char 92\relax w}\texttt{)}{\cdot}\texttt{(?!}\texttt{\char 92\relax w}\texttt{)}{\mathbin{\texttt{|}}}\texttt{(?<!}\texttt{\char 92\relax w}\texttt{)}{\cdot}\texttt{(?=}\texttt{\char 92\relax w}\texttt{)}$ | $s_{i-1}\in[[\psi_{\texttt{{\char 92\relax w}}}]]\Leftrightarrow s_{i}\notin[[\psi_{\texttt{{\char 92\relax w}}}]]$
\B | non-word-border | $\texttt{(?<=}\texttt{\char 92\relax w}\texttt{)}{\cdot}\texttt{(?=}\texttt{\char 92\relax w}\texttt{)}{\mathbin{\texttt{|}}}\texttt{(?<!}\texttt{\char 92\relax w}\texttt{)}{\cdot}\texttt{(?!}\texttt{\char 92\relax w}\texttt{)}$ | $s_{i-1}\in[[\psi_{\texttt{{\char 92\relax w}}}]]\Leftrightarrow s_{i}\in[[\psi_{\texttt{{\char 92\relax w}}}]]$

Table 1 gives a summary of all anchors typically supported by regular
expression engines (Friedl, 2006) represented in terms of lookarounds. Recall
that $s_{-1}=s_{|s|}=\epsilon$ and thus, for all $\psi\in\Psi$,
$s_{-1}=s_{|s|}\notin[[\psi]]$. Therefore, e.g., the definition of \B as
$\texttt{(?<=}\texttt{\char 92\relax w}\texttt{)}\texttt{(?=}\texttt{\char
92\relax w}\texttt{)}{\mathbin{\texttt{|}}}\texttt{(?<=}\texttt{\char 92\relax
W}\texttt{)}\texttt{(?=}\texttt{\char 92\relax W}\texttt{)}$ would be
_incorrect_ where $[[\psi_{\texttt{{\char 92\relax
W}}}]]=[[\lnot\psi_{\texttt{{\char 92\relax w}}}]]$, because for example \B is
nullable in _all locations_ of "#" instead of in _no locations_ if one would
use $\texttt{(?<=}\texttt{\char 92\relax w}\texttt{)}\texttt{(?=}\texttt{\char
92\relax w}\texttt{)}{\mathbin{\texttt{|}}}\texttt{(?<=}\texttt{\char 92\relax
W}\texttt{)}\texttt{(?=}\texttt{\char 92\relax W}\texttt{)}$.

In other words, $\texttt{(?!}\texttt{\char 92\relax
w}\texttt{)}\nequiv\texttt{(?=}\texttt{\char 92\relax W}\texttt{)}$. In
general, negative lookarounds of predicates _cannot be converted_ into
positive lookarounds by delegating negation to the underlying character
algebra $\mathcal{A}$ by using $\lnot$ of $\mathcal{A}$.

It is also important to note that _complement_ $(\texttt{\char 126\relax})$ of
positive lookahead does not correspond to a negative lookahead (and vice
versa). Below we show that $\texttt{\char 126\relax}\texttt{\char 92\relax
b}\nequiv\texttt{\char 92\relax B}$, i.e. they are not complements of each
other in match semantics. Thus, negations of combinations of lookarounds must
be used with caution as their semantics needs careful analysis. In fact,
$\texttt{\char 126\relax}\texttt{\char 92\relax b}\equiv\texttt{\char 92\relax
B}{\mathbin{\texttt{|}}}\top\texttt{+}$, as shown below.

While it follows from definitions, for all valid locations $x$, that
$\mathit{Null}_{x}(\texttt{(?!}R\texttt{)})\boldsymbol{\Leftrightarrow}\mathbf{not}\,\mathit{Null}_{x}(\texttt{(?=}R\texttt{)})$
their _derivatives_ are fundamentally different: they are _complements_ of
each other. In particular,

$\begin{array}[]{rcl}\partial_{x}(\texttt{(?!}R\texttt{)})&=&\bot\\\
\partial_{x}(\texttt{\char
126\relax}{\texttt{(?=}R\texttt{)}})&=&\texttt{\char
126\relax}\partial_{x}(\texttt{(?=}R\texttt{)})=\texttt{\char
126\relax}\bot\equiv\top\texttt{*}\end{array}$

The same applies to lookbacks. The derivative of a lookaround is always $\bot$
because lookarounds are context conditions for locations with no forward
progress on their own, and essentially operate as blocking conditions inside
concatenations. It follows from the definition of derivatives of
concatenations that, if $\ell$ is a lookaround then

$\partial_{x}(\ell{\cdot}R)\equiv\left\\{\begin{array}[]{@{}l@{\;}l}\partial_{x}(R),&\mathbf{if}\,\mathit{Null}_{x}(\ell);\\\
\bot,&\mathbf{otherwise}.\end{array}\right.$

which is how derivatives are implemented for this case, i.e., the
simplification rewrite rules are directly embedded into the abstract
definition itself, rather than being applied afterwards in a separate step.
The same applies to all similar situations involving simplification rules for
example for (), $\bot$, and $\top\texttt{*}$, in intersections, unions, and
concatenations. Many of those rules are _mandatory_ in order to maintain
finiteness of the state space of regexes that arise during matching, and all
rewrite rules are applied as early as possible.

In order to understand the interaction of anchors with newly added extensions
better, let us take the word-border anchor \b and derive what the complement
of it $(\texttt{\char 126\relax}\texttt{{\textbackslash}b})$ would look like.
Here we make use of de Morgan’s laws via Corollary 1 and the property that
concatenation of two lookarounds has the same semantics as the intersection
(conjunction) of those lookarounds. Moreover, to simplify, we use laws of
distributivity and the properties that

$\begin{array}[]{rcl}\texttt{\char
126\relax}\texttt{(?!}R\texttt{)}\mathbin{\texttt{\&}}\texttt{\char
126\relax}\texttt{(?=}R\texttt{)}&\equiv&\top\texttt{+}\\\ \texttt{\char
126\relax}\texttt{(?<!}R\texttt{)}\mathbin{\texttt{\&}}\texttt{\char
126\relax}\texttt{(?<=}R\texttt{)}&\equiv&\top\texttt{+}\end{array}$

where $\partial_{x}(\texttt{\char
126\relax}\ell\mathbin{\texttt{\&}}\texttt{\char
126\relax}\ell^{\prime})\equiv\top\texttt{*}$ and the combined nullability
conditions become trivially false, e.g.,

$\mathit{Null}_{x}(\texttt{\char
126\relax}\texttt{(?!}R\texttt{)}\mathbin{\texttt{\&}}\texttt{\char
126\relax}\texttt{(?=}R\texttt{)})\boldsymbol{\Leftrightarrow}\mathit{Null}_{x}(\texttt{(?=}R\texttt{)})\mathrel{\mathbf{and}}\mathbf{not}\,\mathit{Null}_{x}(\texttt{(?=}R\texttt{)})$

Then

$\begin{array}[]{@{}r@{\;}c@{\;}l@{}}\texttt{\char 126\relax}\texttt{\char
92\relax b}&\equiv&\texttt{\char 126\relax}(\texttt{(?<=}\texttt{\char
92\relax w}\texttt{)}{\mathbin{\texttt{\&}}}\texttt{(?!}\texttt{\char 92\relax
w}\texttt{)}{\mathbin{\texttt{|}}}\texttt{(?<!}\texttt{\char 92\relax
w}\texttt{)}{\mathbin{\texttt{\&}}}\texttt{(?=}\texttt{\char 92\relax
w}\texttt{)})\\\ &\equiv&(\texttt{\char 126\relax}\texttt{(?<=}\texttt{\char
92\relax w}\texttt{)}{\mathbin{\texttt{|}}}\texttt{\char
126\relax}\texttt{(?!}\texttt{\char 92\relax
w}\texttt{)}){\mathbin{\texttt{\&}}}(\texttt{\char
126\relax}\texttt{(?<!}\texttt{\char 92\relax
w}\texttt{)}{\mathbin{\texttt{|}}}\texttt{\char
126\relax}\texttt{(?=}\texttt{\char 92\relax w}\texttt{)})\\\
&\equiv&\texttt{\char 126\relax}\texttt{(?<=}\texttt{\char 92\relax
w}\texttt{)}{\mathbin{\texttt{\&}}}\texttt{\char
126\relax}\texttt{(?<!}\texttt{\char 92\relax
w}\texttt{)}\mathbin{\texttt{|}}\texttt{\char
126\relax}\texttt{(?<=}\texttt{\char 92\relax
w}\texttt{)}{\mathbin{\texttt{\&}}}\texttt{\char
126\relax}\texttt{(?=}\texttt{\char 92\relax
w}\texttt{)}\mathbin{\texttt{|}}\texttt{\char
126\relax}\texttt{(?!}\texttt{\char 92\relax
w}\texttt{)}{\mathbin{\texttt{\&}}}\texttt{\char
126\relax}\texttt{(?<!}\texttt{\char 92\relax
w}\texttt{)}\mathbin{\texttt{|}}\texttt{\char
126\relax}\texttt{(?!}\texttt{\char 92\relax
w}\texttt{)}{\mathbin{\texttt{\&}}}\texttt{\char
126\relax}\texttt{(?=}\texttt{\char 92\relax w}\texttt{)}\\\
&\equiv&\texttt{\char 126\relax}\texttt{(?<=}\texttt{\char 92\relax
w}\texttt{)}{\mathbin{\texttt{\&}}}\texttt{\char
126\relax}\texttt{(?=}\texttt{\char 92\relax
w}\texttt{)}\mathbin{\texttt{|}}\texttt{\char
126\relax}\texttt{(?!}\texttt{\char 92\relax
w}\texttt{)}{\mathbin{\texttt{\&}}}\texttt{\char
126\relax}\texttt{(?<!}\texttt{\char 92\relax
w}\texttt{)}\mathbin{\texttt{|}}\top\texttt{+}\\\ &\equiv&\texttt{\char
92\relax B}\mathbin{\texttt{|}}\top\texttt{+}\end{array}$

where the last equivalence holds because, for any valid location $x$,

$\mathit{Null}_{x}(\texttt{\char 126\relax}\texttt{(?<=}\texttt{\char 92\relax
w}\texttt{)}{\mathbin{\texttt{\&}}}\texttt{\char
126\relax}\texttt{(?=}\texttt{\char 92\relax
w}\texttt{)}\mathbin{\texttt{|}}\texttt{\char
126\relax}\texttt{(?!}\texttt{\char 92\relax
w}\texttt{)}{\mathbin{\texttt{\&}}}\texttt{\char
126\relax}\texttt{(?<!}\texttt{\char 92\relax
w}\texttt{)})\Leftrightarrow\mathit{Null}_{x}(\texttt{(?<!}\texttt{\char
92\relax w}\texttt{)}{\mathbin{\texttt{\&}}}\texttt{(?!}\texttt{\char 92\relax
w}\texttt{)}\mathbin{\texttt{|}}\texttt{(?=}\texttt{\char 92\relax
w}\texttt{)}{\mathbin{\texttt{\&}}}\texttt{(?<=}\texttt{\char 92\relax
w}\texttt{)})$

that is equivalent to $\mathit{Null}_{x}(\texttt{\char 92\relax B})$. One can
also show that $\texttt{\char 126\relax}\texttt{\char 92\relax
B}\equiv\texttt{\char 92\relax b}\mathbin{\texttt{|}}\top\texttt{+}$. Observe
therefore that

$\texttt{\char 126\relax}(\texttt{\char 92\relax
B}\mathbin{\texttt{|}}\top\texttt{+})\equiv\texttt{\char
126\relax}\texttt{\char 92\relax B}\mathbin{\texttt{\&}}\texttt{\char
126\relax}(\top\texttt{+})\equiv(\texttt{\char 92\relax
b}\mathbin{\texttt{|}}\top\texttt{+})\mathbin{\texttt{\&}}\texttt{()}\equiv\texttt{\char
92\relax b}\mathbin{\texttt{\&}}\texttt{()}\equiv\texttt{\char 92\relax b}$

A natural question that arises, that we are investigating, is if there exists
a general way to encode any negative lookaround $\texttt{(?!}R\texttt{)}$ (or
$\texttt{(?<!}R\texttt{)}$) by an equivalent positive lookaround
$\texttt{(?=}R^{\prime}\texttt{)}$ (or $\texttt{(?<=}R^{\prime}\texttt{)}$),
by converting $R\in\mathcal{R}$ into a regex $R^{\prime}\in\mathcal{R}$ by
using ~ in some manner. A possible algorithmic advantage is that this
transformation may enable further transformations. For example,
$\texttt{(?!}R\texttt{)}{\cdot}\texttt{(?=}S\texttt{)}$ could then be
transformed into
$\texttt{(?=}R^{\prime}{\cdot}\top\texttt{*}\mathbin{\texttt{\&}}S{\cdot}\top\texttt{*}\texttt{)}$.

The anchor denoting the end of previous match \G (Friedl, 2006) is a non-
traditional anchor as it uses metadata instead of regular expressions. While
it can be supported by adding implementation details, we have decided to omit
it as we have not observed it being pervasively used in real life
applications. The anchor \a in (Moseley et al., 2023) that is needed
internally for reversal, can be defined here as $(\texttt{\char 92\relax
Z})^{r}\\!$; \a is not supported in the concrete syntax of .NET regular
expressions.

###  4.6. Top-Level Match Algorithm

The top-level match algorithm $\textrm{$\mathit{llMatch}$}{}(s,R)$ takes a
string $s\in\Sigma^{*}$ and a regex $R\in\mathcal{R}$, and either returns
$\lightning$ if $\mathcal{M}(R)=\emptyset$, or else returns a match
$\langle{s\langle i\rangle,s\langle j\rangle}\rangle\in\mathcal{M}(R)$ such
that $i$ is minimal (leftmost) and then $j$ is maximal for the given $i$ (in
particular all loops are eager). Semantically the implementation corresponds
to the following algorithm, which therefore provides the leftmost and longest
match, also known as POSIX semantics,

$\begin{array}[]{rcl}\textrm{$\mathit{llMatch}$}{}(s,R)&\stackrel{{\scriptstyle\textsc{\raisebox{-1.04996pt}{\tiny{def}}}}}{{=}}&\textbf{let}\,x=\textit{MatchEnd}{}(s^{r}\\!\langle
0\rangle,\top\texttt{*}{\cdot}R^{r}\\!)\,\textbf{in}\left\\{\begin{array}[]{@{}l@{\;}l}\lightning,&\mathbf{if}\,x=\lightning;\\\
\langle{x^{r}\\!,\textit{MatchEnd}{}(x^{r}\\!,R)}\rangle,&\mathbf{otherwise}.\end{array}\right.\end{array}$

In the actual implementation the first phase initially locates the end
location $s\langle j\rangle$ by simulating a PCRE “lazy” loop
$\top\texttt{*}\texttt{?}$ concatenated with $R$, and subsequently locates the
start location backwards from $s\langle j\rangle$ by using $R^{r}\\!$. It is
typically more economical to start the search from the start of the string
rather than backwards from the end of the string, although both variants are
possible.

###### Example 4.1.

Consider $s=\texttt{"\\#\\#\\#abacarabacaraba\\#\\#"}$ and
$R=\texttt{abacaraba}$. So $R^{r}\\!=\texttt{abaracaba}$ and
$s^{r}\\!=\texttt{"\\#\\#abaracabaracaba\\#\\#\\#"}$. Then
$\textit{MatchEnd}{}(s^{r}\\!\langle
0\rangle,\top\texttt{*}{\cdot}R^{r}\\!)=s^{r}\\!\langle
17\rangle=s\langle|s|-17\rangle^{r}\\!=s\langle 3\rangle^{r}\\!$ and
$\textit{MatchEnd}{}(s\langle 3\rangle,R)=s\langle 12\rangle$. So
$\textrm{$\mathit{llMatch}$}{}(s,R)=\langle{s\langle 3\rangle,s\langle
12\rangle}\rangle$. Observe that
$\textit{MatchEnd}{}(s,\top\texttt{*}{\cdot}R)=s\langle 18\rangle$ would be
the end location of the _second_ match. Therefore, when starting with the end
location search, the initial *-loop must be treated or simulated as a lazy
loop.

If we instead let $R=\texttt{abacaraba{\char 92\relax b}}$ so that the match
must end a word then in $R^{r}\\!=\texttt{{\char 92\relax b}abaracaba}$ the
match must start a word. In that case $\textit{MatchEnd}{}(s^{r}\\!\langle
0\rangle,\top\texttt{*}{\cdot}R^{r}\\!)=s^{r}\\!\langle 11\rangle=s\langle
9\rangle^{r}\\!$ because # is not a word-letter, and then
$\textrm{$\mathit{llMatch}$}{}(s,R)=\langle{s\langle 9\rangle,s\langle
18\rangle}\rangle$.

The _POSIX match for $R$ in $s$_, if a match exists, is a pair
$\langle{s\langle i\rangle,s\langle j\rangle}\rangle$ where $s\langle
i\rangle$ is the minimal location in $s$ such that $\exists y:s\langle
i\rangle\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}y$ and $s\langle j\rangle$ is the maximal location in $s$ such
that $s\langle
i\rangle\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}s\langle j\rangle$. The following is the correctness theorem of
$\mathit{llMatch}$.

###### Theorem 3 (Match).

For all $s\in\Sigma^{*}$ and $R\in\mathcal{R}$ the following statements hold:

  1. (1)

$\textrm{$\mathit{llMatch}$}{}(s,R)=\lightning\boldsymbol{\Leftrightarrow}\nexists
i,j:s\langle
i\rangle\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}s\langle j\rangle$;

  2. (2)

if $\textrm{$\mathit{llMatch}$}{}(s,R)\neq\lightning$ then
$\textrm{$\mathit{llMatch}$}{}(s,R)$ is the POSIX match for $R$ in $s$.

###### Proof.

By using Theorems 1 and 2, and that for all $x$ and $S\in\mathcal{R}$,
$\textit{MatchEnd}{}(x,S)=\max({x}{\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}})$. The proof also uses the fact that if $s\langle
i\rangle^{r}\\!=\max({s^{r}\\!\langle
0\rangle}{\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{@{}c@{}}\top\texttt{*}{\cdot}R^{r}\\!\\\\[-2.79996pt]
\end{array}}$}}})$ then $s\langle i\rangle$ is the _minimal_ location in $s$
such that $s\langle
i\rangle\mathrel{\raisebox{-1.00006pt}{\scriptsize$\xrightarrow{\begin{array}[]{<EMAIL_ADDRESS>\end{array}}$}}s\langle|s|\rangle$. ∎

##  5\. Implementation

Here we give a high level overview of how the engine was implemented, what
parts are shared with the rest of .NET and the nonbacktracking engine, and
some key differences and implementation details.

The core parser was taken directly from the .NET runtime, but was modified to
read the symbols & and $\sim$ as intersection and negation respectively.
Fortunately the escaped variants ‘\&’ and ‘\$\sim$’ were not assigned to any
regex construct, and all existing regex patterns can be used by escaping these
two characters.

Another important component we directly took from the .NET runtime is the
alphabet compression of the nonbacktracking engine that builds the minimal
number of predicates on the underlying character set by applying appropriate
Boolean combinations. For example, all input characters in the the regex ab
can be represented with just 3 predicates: $a$, $b$ and $[{\char
94\relax}ab]$. It is an essential preprocessing step for such a large alphabet
(16-bit Unicode Basic Multilingual Plane in our case), which allows us to
represent the input predicates as bits, and then use bitwise operations to
check if a character is in the set of characters represented by a predicate.

The engine itself is implemented in mostly high-level F#, without caching any
derivatives, which does not give it the optimal performance characteristics as
of at the time of writing. The aim is rather to provide a working prototype
that, despite having much higher number of memory allocations than, e.g., the
nonbacktracking or backtracking alternatives of .NET 7, is still capable of
solving problems that neither the backtracking nor nonbacktracking variant can
currently solve.

To make the modifications possible, the System.Text.RegularExpressions library
was copied to another namespace and the visibility of the library was changed
from internal to public. The only other meaningful modification to the library
is the extension of the parser to parse negation and intersection symbols
appropriately, as described above.

The concatenation and $\epsilon$-nodes were implemented as just a single-
linked list of other regex nodes, as it allows to traverse to next one using
just a tail pointer, without needing any other steps. There is never any need
to traverse the concatenation backwards, thus allowing to take advantage of
what the concatenation fundamentally is – a single linked list. And () is just
an empty concatenation, i.e. empty list.

###  5.1. Rewrite Rules and Subsumption

Our system implements a number of regex rewrite rules, which are essential for
the efficiency of the implementation. Figure 1 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.

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 1 that rewrites
$\psi\texttt{\\{}0{,\infty}\texttt{\\}}{\mathbin{\texttt{|}}}\psi\texttt{\\{}1{,1}\texttt{\\}}$
to $\psi\texttt{\\{}0{,\infty}\texttt{\\}}$.

A further simplification rule 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{*}\mathbin{\texttt{|}}.\texttt{*}$) to just
$.\texttt{*}$ (recall that $.\equiv\texttt{[\char 94\relax{\char 92\relax
n}]}$), which significantly reduces the number of alternations in total. Such
rewrite could potentially be extended even further, e.g., rewriting
($.\texttt{*}\texttt{ab}.\texttt{*}\mathbin{\texttt{|}}.\texttt{*}\texttt{b}.\texttt{*}$)
to $.\texttt{*}\texttt{b}.\texttt{*}$, but the detection overhead is more
complex for rewrites like this and has not been evaluated yet.

$\inferrule{\texttt{\char
126\relax}(\top\texttt{*})}{\bot}\quad\inferrule{\texttt{\char
126\relax}\bot}{\top\texttt{*}}\quad\inferrule{\texttt{\char
126\relax}\texttt{\char 126\relax}R}{R}\quad\inferrule{\texttt{\char
126\relax}\texttt{()}}{\top\texttt{+}}\quad\inferrule{\texttt{\char
126\relax}(\top\texttt{+})}{\texttt{()}}\quad\inferrule{\bot{\cdot}R}{\bot}\quad\inferrule{R{\cdot}\bot}{\bot}\quad\inferrule{\texttt{()}{\cdot}R}{R}\quad\inferrule{R{\cdot}\texttt{()}}{R}\quad\inferrule{\bot\texttt{*}}{\texttt{()}}$

$\quad\inferrule*{\top\texttt{*}\mathbin{\texttt{|}}R}{\top\texttt{*}}\quad\inferrule*{\top\texttt{*}\mathbin{\texttt{\&}}R}{R}\quad\inferrule*{\bot\mathbin{\texttt{|}}R}{R}\quad\inferrule*{\bot\mathbin{\texttt{\&}}R}{\bot}\quad\inferrule*{R\texttt{\\{}1{,1}\texttt{\\}}}{R}\quad\inferrule*{R\texttt{\\{}0{,0}\texttt{\\}}}{\texttt{()}}$

$\inferrule*[right={(\mathit{Null}_{x}(R))}]{\texttt{()}\mathbin{\texttt{\&}}R}{R}\quad\inferrule*[right={(\mathbf{not}\,\mathit{Null}_{x}(R))}]{\texttt{()}\mathbin{\texttt{\&}}R}{\bot}\quad\inferrule*[right={(l\leq
k\leq
m)}]{R\texttt{\\{}l{,m}\texttt{\\}}\mathbin{\texttt{|}}R\texttt{\\{}k{,n}\texttt{\\}}}{R\texttt{\\{}l{,\max(m,n)}\texttt{\\}}}$

Figure 1. Basic rewrite rules.

###  5.2. POSIX Semantics

One key difference from the .NET 7 nonbacktracking engine, is that we treat
both alternations and intersections as sets, which makes the semantics
different from the backtracking one. For example, matching the regular
expression (a|ab)* on the string “abab” with the current .NET engines results
in the prefix “a”, as the leftmost alternation finds a successful match. Our
engine will match the whole string “abab”, as all the alternations are
explored in parallel, and the longest match is in the right alternation. The
behavior of $\textit{IsMatch}(x,R)$ is identical in both engines.

In the nonbacktracking engine, PCRE semantics is achieved by prepending
$\top\texttt{*}\texttt{?}$ to the regex pattern, which is always nullable and
has only two potential derivatives. For example, in the case of the pattern
$\top\texttt{*}\texttt{?}\texttt{ab}$, the derivative can be either
$\texttt{b}{\mathbin{\texttt{|}}}\top\texttt{*}\texttt{?}\texttt{ab}$, when
the character matches $\psi_{\texttt{a}}$ (the initial pattern creates a new
alternation) , or $\top\texttt{*}\texttt{?}\texttt{ab}$, (i.e. just the
initial pattern) when it does not.

In our case we meet POSIX semantics by keeping the initial pattern as is, but
starting a potential match on every input position, that has a valid starting
predicate. Then we keep track of the nullability of all alternations the
initial pattern produced separately. This is done by having a set of ”top-
level alternation” data structures, each of which consist of a regex and the
maximum nullable position of the alternation. Once an alternation turns into
$\bot$, we check if the alternation has a nullable position, and if it does,
we return the match. If the alternation does not have a nullable position, we
remove it from the set and continue matching the remaining alternations.

###  5.3. Conjunctive Startset Lookup and Skipping

One very important optimization that allows to avoid doing a lot of
unnecessary work on average, depending on the input string and regular
expression, is the startset optimization, which enables search for characters
belonging to the set of initial characters of a regex denoted by the startset
predicate by using dedicated string traversal constructs which can be several
orders of magnitude faster than checking characters one-by-one.

The result of evaluating the predicate startset is captured in the state of
the regex node. Startset optimization is often comprised of checking if the
first character of the regex pattern is present in the input string. As
mentioned in Section 2.3, we make use of the fact that determining the
startset of a regex with derivatives is a relatively cheap operation, and we
can use it to incorporate efficient vectorized string-search procedures into
the matching algorithm.

A key difference from other regex engines is that we don’t just skip until the
initial startset of the regex, but perform intermediate startset computations
and appropriate skipping in the inner loop as well. To take advantage of the
fast startset check, we first need to determine if a regex is “skippable” or
not, where we determine if taking the derivative changes the node on only a
subset of the input alphabet. Such regexes start with a *-loop.

A skippable regex is defined as a regex that starts with a *-loop, or one in
which all child regexes recursively start with a *-loop, such as an
alternation, lookahead, intersection or negation of regexes starting only with
*-loops. Lookbacks are more complex and do not currently take advantage of
this optimization. The key insight of this skippable check is that *-loops
keep producing the same regex derivative until either the loop terminator or
tail of one of the *-loops matches.

For example, all regexes starting with $\top\texttt{*}$ are skippable, as
according to the derivation rules in Section 4.2: the derivative of the regex
does not change unless the tail of the concatenation produces a non-$\bot$
derivative. The same is true for all regexes starting with $.\texttt{*}$, as
the only two predicates that produce a non-initial derivative are
$\psi_{\texttt{{\char 92\relax n}}}$, that is the loop termination predicate
for .*, and the starting predicate of the concatenation tail. For example, the
regex .*ab has two predicates that change the state: $\psi_{\texttt{{\char
92\relax}n}}$, in which case the regex becomes $\bot$, and
$\psi_{\texttt{a}}$, in which case the regex becomes b|.*ab. All other
predicates produce the initial regex.

Such skipping becomes useful when we want to match over input text with
multiple intersections or alternations. For example, consider the regex
(12.*)&(.*\d), which is strictly non-skippable, as the transition from 12.* to
$\bot$ or to 2.* is an important part of the matching process. However, the
regex (.*12.*)&(.*\d) is skippable, allowing us to look up the occurrence of a
character satisfying the predicate
$\psi_{\texttt{{[{\textbackslash}d{\textbackslash}n]}}}$ (the disjunction of
predicates 1, \d and the loop exit condition \n), and continue matching
directly at that position.

The in-match startset computation heuristic itself is very simple, and only
considers the first node of the regex, or the first node and the second node
recursively in the case of a star. In the case of a regex starting with a
predicate, we take the predicate itself. In the case of a predicate star loop,
we take the negation of the loop body predicate, and union it with the
concatenation tail predicate, as done in the previous example. In the case of
an intersection, alternation or complement, we take the union of the startsets
of the contained regex bodies. Notably, the startset of a complement is not
the complement of the startset of the contained regex, but the same startset,
as the derivation rules apply the same way inside negation.

After computing the joint startset of the regex, we use it in a vectorized
index-of lookup in the following input string. Currently, we perform this
lookup in an overestimated manner, by taking the union of all startsets, but
this can be improved upon by taking the intersection in some cases. For
example, if we have an intersection with the startsets $\psi_{\texttt{{\char
92\relax}d}}$ and $\psi_{\texttt{1}}$ strictly in the same position, then we
know ahead-of-time that the startset of the intersection is constrained to
only $\psi_{\texttt{1}}$ \- the conjunction of the two startsets.

The startset optimization is very powerful as it allows us to skip over large
parts of the input string in a single step, and only perform the more
expensive derivative computation on the remaining positions. A future
improvement would be to extend this to multi-character predicates and
intersections, which would allow us to skip over even more of the input
string.

##  6\. Evaluation

The evaluation of the engine is still in its early stages, and we have not yet
implemented all the optimizations that are possible, such as caching
transition regexes, or skipping over multi-character predicates. However,
despite being only a research prototype, we can already see that the engine is
capable of solving problems that neither of the available .NET regex engines
can currently solve.

An industrial implementation of the engine should reach performance characteristics comparable to (Moseley et al., 2023) over standard regexes, because the same .NET framework is used, with potential marginal gains in space/time due to commutative |, as non-commutativity of | disallows some useful rewrites in (Moseley et al., 2023). Moreover, all initial fixed-prefix/suffix-search optimizations are shared across all backends. For a more comprehensive evaluation on standard regexes outside .NET, see the evaluation of (Moseley et al., 2023) directly.

Note that we do not use the caching mechanism from the nonbacktracking engine
in our prototype, as it is not yet fully implemented, and would require a
significant amount of work to integrate in the presence of lookarounds. The
lack of caching is the main reason why our engine is not yet competitive with
the nonbacktracking engine on the benchmarks.

We have evaluated the performance of our engine against the .NET default
backtracking engine, and the symbolic automata based nonbacktracking version.
The benchmarks were run on a machine with an AMD Ryzen 7 5800X 8-Core CPU, and
32 GB of RAM. The benchmarks were run on .NET version 7.0.305.

We compare the performance of extracting paragraphs containing multiple
substrings from the collected works of Mark Twain (Herczeg, 2015), first we
compare the performance on a 9 kB string, containing 34 paragraphs, extracted
from the lines 188589 to 188771, and then on the entire 20 MB file, containing
379897 lines in total.

The paragraphs are extracted with three kinds of patterns: one that uses a
negative lookahead to match the end of the paragraph, one that uses a line
loop until the occurrence of two sequential newlines, and one that uses
negation to constrain the paragraph range and intersections to constrain the
paragraph contents.

Examples of the patterns used to match paragraphs containing the word ”King”:

  1. (1)

Negative lookahead: `\n\n((?!\n\n)[\s\S])*?(King)((?!\n\n)[\s\S])*?\n\n`

  2. (2)

Loop: `\n\n((.+\n)+?(.*King.*\n)(.+\n)+?)\n`

  3. (3)

Conjunction, negation: `\n\n~([\s\S]*\n\n[\s\S]*)\n&[\s\S]*King[\s\S]*`

Note that using a simpler pattern, such as `\n\n[\s\S]*?King[\s\S]*?\n\n`,
would not work, as any non-match inside the paragraph would cause `[\s\S]*?`
to leak outside the current paragraph, and match over multiple paragraphs.

The substrings we look for in the paragraph are ”King”, ”Paris”, ”English”,
”would”, ”rise”, ”struck”, ”council”, ”march”, ”war”, ”May”, ”Orleans” and
”work”, where we introduce the next substring, as the number of substrings
increases. In the case of 1 substring we use ”King”, for 2 substrings we look
for ”King” and ”Paris” in the same paragraph, etc.

Figure 2. Time taken to find a matching paragraph containing all required
substrings in any order in a 9kB sample text.

The results of an experiment run on a 9 kB string where the first paragraph
matching the number of substrings indicated on the x axis is given in Fig. 2.
As the y axis is logarithmic it can be seen how using the intersections
produces more efficient match as there is no blowup in match orderings
required in conventional regular expressions.

In the 9 kB sample text, our engine, SBRE (Varatalu, 2023) starts becoming
faster than the rest at 3 substrings, but due to lack of caching has 4 times
higher memory allocations than the nonbacktracking engine and about 9 times
higher allocations than the backtracking implementation.

After a certain number of substrings, the order of the matchings (Table 2)
becomes so large that both the backtracking and nonbacktracking engines stop
being able to find a match within 60 seconds, while our engine still manages
to complete the match with minor slowdowns.

Table 2. Paragraph extraction pattern lengths in characters n of substrings |  Neg. lookahead |  Loop |  & and $\sim$
---|---|---|---
1 |  50 |  34 |  46
2 |  101 |  77 |  66
3 |  363 |  295 |  88
4 |  1869 |  1513 |  108
5 |  11805 |  9385 |  127
6 |  87885 |  69145 |  148
7 |  740925 |  579625 |  170
8 |  6854445 |  5322265 |  190
9 |  69310125 |  53343385 |  208
10 |  769305645 |  587865625 |  226

In the full 20 MB text, our research prototype (SBRE) takes significantly more
unnecessary derivatives than the nonbacktracking variant, as it suffers from
the lack of caching, but after a certain number of substrings, it is still the
only engine that can complete the match within 60 seconds. The results are
shown in Fig. 3.

A notable observation in the full text is that the lookahead pattern of the
backtracking engine falls off significantly earlier than in the 9 kB text,
where it showed promising results up to 6 substrings. In the full text, the
nonbacktracking engine shows the best performance up to 6 substrings, but then
falls off completely, as the memory allocated blows up from 74.41 MB in 5
paragraphs to 3.39 GB in 6 paragraphs. The nonbacktracking engine was not able
to produce a result with 7 substrings within 10 minutes.

Figure 3. Time taken to find a matching paragraph containing all required
substrings in any order in the full 20MB sample text.

The results show that our engine is able to search for a large amount of
substrings in a paragraph efficiently, while the other engines suffer from the
exponential blowup in match orderings. In the full text, adding a substring to
the SBRE pattern after 2 substrings currently causes a constant memory
allocation growth of 800 MB, which is a significant amount of memory, but
still allows for the match to complete, while the other engines are not able
to complete the match at all. The memory usage of the SBRE engine could be
significantly reduced by caching the derivatives, which would make the engine
more competitive overall.

##  7\. Related Work

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 this paper. The focus on related work here is solely on automata and
derivative based matching algorithms, tools, and techniques, that in some form
or shape maintain, at least in principle, a finite state based view
corresponding to regular languages. In particular, _lookaheads_ 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 find match end with
derivatives in regular expressions with lookaheads. The semantics of
derivatives in (Miyazaki and Minamide, 2019) uses _Kleene algebras with
lookahead_ as an extension of Kleene algebras with tests (Kozen, 1997), and is
fundamentally different from our formulation in several aspects, where the
underlying semantic concatenation is _commutative_ and _idempotent_ and where
the difference to derivatives of concatenations in relation to (Brzozowski,
1964) is also pointed out, which also leaves unclear the question of
supporting lookbacks and reverse. Derivatives in combination of Kleene
algebras are also studied in (Pous, 2015). Our approach is a conservative
extension of the theory in (Moseley et al., 2023) with intersection and
complement, as well as positive and negative lookbacks and lookaheads, that
builds on (Brzozowski, 1964), leading to the core fundamental results of
Theorem 1 and Theorem 2.

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 MatchEnd 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) as a recursive functional program and
also formalized in Isabelle/HOL. The fundamental difference to the theory here
is that, because of lookarounds (that in particular enable the definition
anchors) imply that certain classical laws, such as several of the
_inhabitation relation rules_ in (Tan and Urban, 2023), become invalid. In
(Wingbrant, 2019) anchors are considered as special symbols in an extended
alphabet, using classical derivatives. This approach has the drawback that
anchors are intended as specialized lookarounds and treating them as special
symbols conflicts with match semantics in terms of locations. Some aspects of
our work here, such as support for intersection, 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. The top-level matcher of SRM is also different and more costly
because it uses three passes over the input to locate a match, instead of two.

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. An 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. Further
evidence of this is also provided 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. In automata-based engines an upfront DFA minimization is
undesirable because it is too costly, while derivatives allow DFA-minimizing
optimizations to be applied essentially on-the-fly. In general, the rewrite
rules applied in our framework are not feasible in automata-caching, because
the corresponding semantic language-level checks would require global
analysis, because in traditional automata based representations one has lost
the relationship between states and regular expressions. In our case we
preserve the relationship between regular expressions

The two phases of the top-level matching algorithm: to find the match end
location and to find the match start location are similar in RE2 (Cox, 2010)
as well as in .NET NonBacktracking which our implementation builds on top of.
It therefore also benefits from switching to NFA mode when a certain threshold
of DFA states is reached, having an overall effect similar to that of RE2
(Cox, 2010), but the derivatives can switch to Antimirov-style derivatives
without any prior bookkeeping. The top-level loop is in some sense oblivious
to the fact that intersection, complement, and lookarounds are being used
inside the regular expressions.

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. We
should point out that (Frisch and Cardelli, 2004, Proposition 2) assumes the
axiom $L(R{\cdot}S)=L(R){\cdot}L(S)$ that fails with anchors or lookarounds.
While backtracking semantics is needed in .NET for compatibility across all
the backends – including NonBacktracking (Moseley et al., 2023) – here we use
POSIX semantics that allows us to treat alternations and intersections as
commutative operations. The rationale behind using POSIX is that it is
semantically unclear as to what de Morgan’s laws and laws of distributivity
would mean in the context of backtracking semantics if intersection would be
treated as a noncommutative operation.

The results (Moseley et al., 2023, Theorem 3.3 and Theorem 3.8) form a _strict
subset_ of our Theorem 1 and Theorem 2 whose proofs are novel and nonobvious
because definitions of nullability and derivatives are mutually recursive. It
was far from obvious if regex complement and intersection could even be
combined in any meaningful way with lookarounds. It remains unclear to us, as
to if the main result (Moseley et al., 2023, Theorem 4.5) that builds on
formally linking the semantics of derivatives to _backtracking_ (PCRE)
semantics can be extended to cover the extended fragment of regexes defined
here by $\mathcal{R}$ due to noncommutativity of alternations in backtracking
semantics, the proof of (Moseley et al., 2023, Theorem 4.5) is much more
complicated than that of Theorem 3. Intersection was also included as an
experimental feature in the initial version of SRM (Saarikivi et al., 2019) by
building directly on derivatives in (Brzozowski, 1964), and used an encoding
via regular expression _conditionals_ (if-then-else) that unfortunately
conflicts with the intended semantics of conditionals and therefore has, to
the best of our knowledge, never been used or evaluated.

The conciseness of using intersection and complement in regular expressions is
also 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.

##  8\. Future Work

The theory of derivatives based on locations that is developed here can 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 CVC4 (CVC4, 2020; 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.

Further work of improved rewrite rules is also needed in our current
implementation to reduce the number of states that arise in the matching
engine, as well as enhancing caching techniques that record transitions that
have already been seen for lookarounds. Currently, no special handling of
transitions arising from lookarounds is taking place. And, as intersections
allow precise text extraction in a single pass, the approach can be optimized
further by application of vectorization.

One of the main drawbacks of lookarounds is that they are not cacheable in the
same way as other regexes, as they depend on the position of the matcher in
the string. This means that the regex engine cannot statically determine if a
lookaround will match at a given position and has to try the lookaround at
every position.

This is not a problem for the short context-lookups, like the anchor
lookarounds in Table 1, as they do not move around in the string, and retain
the linear time complexity of the regex. However, this is a problem for the
other lookarounds, such as the lookback (?<=a.*)b, where the occurrence of the
character a has to be re-checked at every occurrence of b. This leads to a
non-ideal quadratic time complexity.

However, these kinds of lookarounds could be cached by storing the predicate
$\psi_{\texttt{\\!\large{.}\\!}}=\psi_{\texttt{{[\char 94\relax{\char 92\relax
n}]}}}$ and passing it along with the derivative. This way, the regex engine
will only invalidate the cache upon finding an occurrence of a character that
does not match the loop predicate, i.e., in the case of (?<=a.*) this cached
predicate will be invalidated by \n, which is the only character not in
$[[\psi_{\texttt{\\!\large{.}\\!}}]]$. This caching technique could lead to a
linear time complexity for many lookarounds but needs more research.

One notable feature that is missing from our regexes is support for laziness.
However, this feature can often be emulated by using complement and negation
of character classes. For example, the regex a.*?b, which matches the shortest
string in the range of a and b, can be emulated by a[^b\n]*b, which has the
exact same semantics, but without using laziness. Another way to emulate
laziness is by using intersection and complement, as in (a.*)&(~(.*b.*)b),
which is also equivalent a.*?b. Note that ~(.*b.*), that means “does not
contain b”, matches _before_ b where the final match character must be b in
(~(.*b.*)b).

##  9\. Conclusion

We have presented both a theory and implementation for a combination of
extensions to 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. The work combines and extends the symbolic
derivatives based approaches presented in (Saarikivi et al., 2019) and
(Moseley et al., 2023) by showing how the carefully selected set of extensions
to regular expressions yield an effective Boolean algebra on the match set
semantics, producing a regular language with interesting new applications and
opening up a principled way to defining rewrite rules for optimizations that
play an important role in practical applications. In addition, we have
provided a precisely defined approach to finding matches using symbolic
derivatives.

When considering context-sensitive anchors, we showed how anchors can be
represented in terms of lookarounds and are thus supported by our approach.
Moreover, such generalization provides possibilities for defining custom
anchors.

The implementation reuses several components of the .NET 7 nonbacktracking
regular expression backend and adds support for newly introduced extensions.
To demonstrate the efficacy of the approach we showed that the task of
locating a substring containing a set of matches in arbitrary order can be
solved by the proposed engine while neither the nonbacktracking nor
backtracking engines of .NET 7 scaled due to the factorial blowup of the
possible orderings of the matches.

## 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
  * 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