Finiteness of Symbolic Derivatives in Lean

We develop a formalized proof in Lean¹¹1See [31] for the complete self-contained Lean formalization. of finiteness of the set of all iterated derivatives in the class ${\mathrm{𝐄𝐑𝐄}}_{\le }$ of regular expressions that allow intersection, complement and lookarounds, modulo any effective Boolean algebra (EBA) over characters. A key insight of the proof is that in the equivalence relation of regular expressions we can replace commutativity of alternation with deduplication, which maintains the order of alternations as required in the backtracking semantics.

We first lift the technique of transition regexes from [24] and formalize it in Lean through symbolic location derivatives where the symbolic location derivative of an expression is a transition tree. This way we abstract away from concrete locations and can take advantage of the symbolic representation as transition trees. In this context, the set of iterated (concrete) derivatives of $R$ is a subset of the set of leaves of (the transition trees of) all iterated symbolic location derivatives of $R$. This is because transition trees, due to their symbolic representation, may contain unreachable leaves. Our approach to proving finiteness is to first define an explicit procedure that, given a regular expression $R$, constructs a (finite) list of regular expressions. We then show that any leaf, reachable or unreachable, of an iterated symbolic location derivative of $R$ is contained in this list (modulo certain equations). We also show how this overapproximation can be used to include certain simplifications in the derivative operation while preserving finiteness.

We use the formalization of the core theory of location derivatives of ${\mathrm{𝐄𝐑𝐄}}_{\le }$ in [32] to show that symbolic location derivatives indeed preserve the match semantics. In doing so, we work with alternation up to associativity, deduplication and idempotence (ADI) and make use of several standard Lean libraries. Although our ultimate goal is practical efficiency, the finiteness proof presented in this paper prioritizes simplicity and ease of formalization while keeping the set of quotienting operations (relatively) minimal.

The remainder of the paper is structured as follows. Section 2 discusses related work. Section 3 provides the preliminaries used in the rest of the paper, including the key results and definitions needed from [32]. Section 4 introduces the Lean theory of symbolic location derivatives that builds on transition regexes from [24]. Section 5 develops the Lean formalization of the finiteness result including the main theorem, finiteness. Finally, Section 6 discusses future work.

Transition regexes are the underlying representation of symbolic derivatives. The abstract grammar of $f,g\in \mathrm{𝐓𝐑}$ is as follows, for $L,R\in {\mathrm{𝐄𝐑𝐄}}_{\le }$:

A transition regex is a binary classification tree: it is either a leaf $L$ or an ITE term $\text{(}R,f,g\text{)}$ with condition $R$, then-case $f$ and else-case $g$. The key idea is that the regular expression $R$ in the condition acts as a symbolic predicate: the ITE evaluates to $f$ if $R$ is nullable at the current location, and to $g$ otherwise.

All binary operations $\diamond :{\mathrm{𝐄𝐑𝐄}}_{\le }\times {\mathrm{𝐄𝐑𝐄}}_{\le }\to {\mathrm{𝐄𝐑𝐄}}_{\le }$ and unary operations $\mathrm{◆}:{\mathrm{𝐄𝐑𝐄}}_{\le }\to {\mathrm{𝐄𝐑𝐄}}_{\le }$ are lifted to $\mathrm{𝐓𝐑}$ as follows, let $f,g,h\in \mathrm{𝐓𝐑}$ and $L,R\in {\mathrm{𝐄𝐑𝐄}}_{\le }$:

The symbolic location derivative $\delta (R)$ of $R\in {\mathrm{𝐄𝐑𝐄}}_{\le }$ is defined as a transition regex in $\mathrm{𝐓𝐑}$ which, intuitively, represents a partial evaluation of $\mathrm{𝐝𝐞𝐫}(R,x)$ with respect to $R$ whose nullability tests have been postponed. Let $\mathrm{\ell }\in \mathrm{𝐋𝐀}$, $\psi \in 𝜶$:

where $⋓$, $⋒$, $\cdot$ and ˜ are lifted to $\mathrm{𝐓𝐑}$. We simplify $\delta (\perp )\stackrel{\text{def}}{=}\perp$.

A transition regex encodes a function from locations (in the input string) to regular expressions. That is, given $f\in \mathrm{𝐓𝐑}$ and $x\in \mathrm{𝐋𝐨𝐜}$, we define $f[x]\in {\mathrm{𝐄𝐑𝐄}}_{\le }$ as the evaluation of $f$ at $x$. Let $L,R\in {\mathrm{𝐄𝐑𝐄}}_{\le }$ and $f,g\in \mathrm{𝐓𝐑}$:

While the evaluation function of transition regexes is well-defined for all locations, transition regexes are used to represent functions from nonfinal locations ${\mathrm{𝐋𝐨𝐜}}^{+}$ to ${\mathrm{𝐄𝐑𝐄}}_{\le }$. For example, the derivative $\delta (\psi )$ of a predicate $\psi$ is the transition regex $\text{(}\text{(?=}\psi \text{)},\epsilon ,\perp \text{)}$ using the lookahead of $\psi$ as its condition. Thus, for all nonfinal locations $x\in {\mathrm{𝐋𝐨𝐜}}^{+}$,

because, using that $x$ is nonfinal,

The following lifting lemma of transition regexes is used frequently in many contexts where $\diamond$ and $\mathrm{◆}$ are lifted binary and unary operations.

The above lemma justifies certain useful transformations. For example, we can propagate complement into the leaves of a transition regex without affecting its conditions. This is the justification for the last step in the following equations

where $\psi \in 𝜶$, $\delta (\text{˜}\epsilon )=\text{˜}\perp$ and $\delta (\text{˜}\perp )=\text{˜}\perp$. In this case the resulting transition terms can directly be viewed as the Symbolic Finite Automaton [10] given in Figure 1 where the states $\text{˜}\perp$ and $\text{˜}\psi$ are always nullable, hence unconditionally accepting, and $\text{˜}\epsilon$ is never nullable, hence unconditionally non-accepting.

The regex $\text{˜}\psi$ is, without using ˜, equivalent to the regex $\epsilon ⋓{\psi }^{𝐜}\cdot \top \text{*}⋓\psi \cdot \top \text{+}$ that is also clear from Figure 1. Propagation of ˜ into leaves is a superpower of transition regexes that enables lazy propagation of complement as in [24] by avoiding eager powerset constructions for determinization.

Finally, we prove that the symbolic derivative (evaluated at a location $x$) is the same as the classical derivative:

An immediate consequence of Theorem 1 is that the correctness of $\mathrm{𝐝𝐞𝐫}(R,x)$ in [32] carries over to the symbolic definition. Observe also that if the lookaround height of $L$ is 0 then nullability of $L$, $\mathrm{𝑁𝑢𝑙𝑙}(L)$, is independent of locations, and thus

Recall that the symbolic location derivative $\delta (R)$ is a transition regex (i.e., a tree). Note that Theorem 1 implies that it is enough in the finiteness proof to care about the leaves of $\delta (R)$ as an overapproximation of $\{\mathrm{𝐝𝐞𝐫}(R,x)\mid x\in {\mathrm{𝐋𝐨𝐜}}^{+}\}$ (i.e., the set of all states reachable in one derivative step from $R$). To reason about iterated applications of the derivative, we repeatedly collect the leaves from the transition regex tree and apply $\delta$ to each of them. This process captures all states reachable through successive derivations and forms the basis of our finiteness argument.

The following function collects all of the leaves of a transition regex:

We lift unary operations $\mathrm{◆}$ and binary operations $\diamond$ on regexes to lists of regexes $X,Y$.

Lifting satisfies the following properties for any $f,g\in \mathrm{𝐓𝐑}$:

The unary case is straightforward in Lean, but lifting binary operations requires the helper function productWith, which computes the Cartesian product of two lists and applies a given binary function to each pair. This function differs from zipWith which instead combines corresponding elements pointwise.

Next, we define a function that computes an overapproximation of the (immediate) derivatives of a regular expression $R$ as $\mathrm{𝐬𝐭𝐞𝐩}(R)\stackrel{\text{def}}{=}\mathrm{𝐥𝐯𝐬}(\delta (R))$. The following lemmas describe how the step function is well-behaved with respect to the extended regular expression operations.

To reason about the set of all derivatives of an expression we need a way to iterate the symbolic location derivative. We define the function steps that systematically explores all possible derivatives of the initial regular expression by using a symbolic approach which at each step expands the current leaves.

Thus steps r n is an overapproximation of derivatives of r wrt. words of length n. Here |> is (reverse) function application and flatten merges nested lists.

Recall that the symbolic location derivative δ can introduce unreachable leaves when constructing the ITE trees. The consequence of these unreachable leaves is that the step function does not respect idempotence.

The following is a concrete example where the idempotence property is violated. Consider the predicate representing the character $a$, denoted by

Taking a single step with a and a ⋓ a produces the following lists of expressions:

Observe that the expressions a and a ⋓ a are similar but the lists of expressions that we get are not. In Figure 2, which is the transition regex δ (a ⋓ a), one can clearly see that evaluating it with a concrete location can never reach the leaves ε ⋓ ⊥ and ⊥ ⋓ ε as the nullability conditions on those paths are contradictory. Consider the path from the leaf ε ⋓ ⊥ to the root: it contains one dashed line which represents the false branch of the nullability test and also one solid line which represents the true branch of the nullability test of the same expression so we reach a contradiction. We see that the unreachable leaves of symbolic location derivatives may be expressions that are not reachable even up to similarity. In a similar manner, the deduplication property is also violated.

For the finiteness proof it is sufficient to consider all possible states without actually pruning unreachable ones.

Let us first review the main idea of Brzozowski’s proof of finiteness [6]. As main finiteness statement [6, Theorem 5.2], Brzozowski proves that any regular expression $R$ has a finite number of dissimilar derivatives. The notion of similarity refers to the associativity, commutativity and idempotence of the union operator. Interestingly, the original proof by Brzozowski does not work without the additional equations $\epsilon \cdot R\cong R$ and $\perp \cdot R\cong \perp$, as first pointed out by Salomaa [23]. Both Salomaa [23] and Aanderaa [1] relied on Brzozowski’s proof of finiteness to establish the completeness of their systems. Later, Antimirov [2] proposed a modification to the original definition of derivatives, ensuring the finiteness result by Brzozowski holds just with the three original equations. This modified approach was subsequently widely adopted as the canonical definition [9, 18, 22].

Brzozowski first proves that every expression $R$ has a finite number $d_R$ of “types” of derivatives, where types are equivalence classes of expressions under language equivalence [6, Theorem 4.3(a)]. The proof is by induction and relies on arguments about the shapes of the resulting derivatives. He also gives a method [6, Theorem 4.3(b)] to construct the set of all $d_R$ types of derivatives of $R$ by lexicographically enumerating words and iteratively computing their derivatives until a fixpoint is reached under language equivalence. Brzozowski then proves that the number of dissimilar derivatives is also finite [6, Theorem 5.2] by showing that the process of constructing the set of all dissimilar derivatives must terminate. This argument relies on a careful analysis of the proof of [6, Theorem 4.3(a)].

As a comparison, we first note that Brzozowski’s proof technique relies on the finiteness of the underlying alphabet, our strategy does not. The other key difference is that Brzozowski proves the existence of a bound on the number of derivatives whereas our proof simply constructs an overapproximation of the set of derivatives. However, the underlying analysis when constructing the set of pieces of $R$ is somewhat similar to the arguments in Brzozowski’s proof of finiteness.

The set of iterated derivatives is clearly not finite in general; to achieve finiteness, we define a relation which we call similarity, which contains the following cases for $L,R,S\in {\mathrm{𝐄𝐑𝐄}}_{\le }$:

In the Lean formalization, we define the similarity relation Sim as an inductive predicate that is almost a congruence relation; we do not require a congruence rule for lookarounds and Kleene star, as derivatives do not occur under lookarounds or star. Moreover, the congruence rule for concatenation keeps the second argument fixed, i.e., if $L\cong R$ then $L\cdot S\cong R\cdot S$.

Both deduplication and idempotence are used to ensure duplicate-free expressions. We conjecture that the finiteness proof would still hold without idempotence, at the cost of a larger state space. Instead of assuming commutativity, we adopt a right-biased deduplication rule: when eliminating duplicates in expressions like $L⋓(R⋓L)$, we retain the leftmost occurrence of $L$. This choice aligns with PCRE-style greedy semantics [19], where the first matching alternative has priority. Removing the earlier occurrence would break this behavior, hence the asymmetry. For the same reason, we cannot allow commutativity in the equivalence relation. Ignoring order – e.g., by treating alternation as a set operation – would further reduce the state space, but our finiteness result would still hold. While additional quotienting rules could coarsen the equivalence relation, they are not necessary for proving finiteness.

Since we work modulo an equivalence relation, it is natural for the theorems about regular expressions in this setting not to hold strictly, but up to equivalence under similarity. We therefore begin by setting up essential infrastructure for reasoning about lists of regular expressions modulo an equivalence relation. We define weaker “up to” definitions of membership of an element inside a list, inclusion, and equality (of lists as sets, i.e., mutual inclusions) w.r.t. any given relation R:

• $\mathrm{■}$

  The notation x ∈[ R ] ys expresses that there is an element in ys which is related to x by R;

• $\mathrm{■}$

  The notation xs ⊆[ R ] ys expresses that every element of xs is an element of ys up to equivalence under R (i.e., for all x ∈ xs, x ∈[ R ] ys);

• $\mathrm{■}$

  Finally, xs =[ R ] ys expresses that xs and ys are equal up to equivalence under R.

In this section we define the function pieces which, given a regular expression $R$, computes a list of regular expressions. The expressions in this list can then be combined together with the union operator to reconstruct any derivative of $R$, as discussed in the beginning of Section 5.

To illustrate the underlying idea, we begin with the so-called partial derivatives which were introduced by Antimirov [2]. The main difference with Brzozowski derivatives is that, given an input regular expression and a character, a Brzozowski derivative is simply a single regular expression (naturally leading to a DFA construction) while there is a set of Antimirov derivatives (naturally leading to an NFA construction). An advantage of Antimirov’s approach is that the finiteness of partial derivatives is significantly easier to prove than the finiteness of Brzozowski derivatives.

Interestingly, Mirkin [16] and Antimirov [2] independently proposed a similar method for constructing an NFA from a regular expression. Later, Champarnaud and Ziadi [8] proved that these constructions are equivalent, unifying the idea and presenting the notion of a support of a regular expression. It is defined as the following function where $c\in \mathrm{\Sigma }$, for some alphabet $\mathrm{\Sigma }$ and $\perp$ denotes the empty language:

In the definition above, the $⨀$ operation is simply concatenation lifted to set of regular expressions on the left and a single expression on the right.

It can be shown that all iterated Antimirov derivatives of $R$ are contained in the following set: $\{R\}\cup \mathrm{𝑠𝑢𝑝𝑝𝑜𝑟𝑡}(R)$. It is easy to see that Antimirov derivatives are not of the form $e⋓f$. In order to show finiteness of the set of Antimirov derivatives of $R$, it is sufficient to show that the $\mathrm{𝑠𝑢𝑝𝑝𝑜𝑟𝑡}(R)$ is finite. Note that it is not necessary to consider any similarity relation for this, as the set representation inherently accounts for ACI. The proof is by induction on $R$.

Our proof of finiteness follows a similar strategy, where we approximate the set of all iterated derivatives in a similar fashion to the support function above. Note that Brzozowski derivatives (and their finiteness) are not directly related to Antimirov derivatives, because additional equations would be needed to relate the two. In particular, one needs to include distributivity of concatenation over union in the similarity relation. For example, the Brzozowski derivative of an expression of the form $(e⋓f)\cdot g$ leads to expressions of the form $(e^{\prime }⋓f^{\prime })\cdot g⋓g^{\prime }$ (assuming that $e$ or $f$ is nullable), where $e^{\prime }$, $f^{\prime }$ and $g^{\prime }$ represent the derivatives of $e$, $f$ and $g$ respectively. For Antimirov derivatives, this leads to a set of expressions of the form $e^{\prime }\cdot g$, $f^{\prime }\cdot g$ or $g^{\prime }$ (again assuming that $e$ or $f$ is nullable).

Since we are working with Brzozowski-style derivatives, which do not compute sets of expressions, we can take the definition of support only as an inspiration. We need to tailor the definition of pieces to our setting which has extended regular expressions, deterministic derivatives and similarity consisting of associativity, deduplication and idempotence.

From the previous section, we know that for every expression r there is a finite set ⊕(pieces r). Now we will show that every derivative of r is represented by an element in this set.

We first prove that every one-step derivative of f (given by the step function) is similar to a sum of pieces of f. The following theorem captures precisely this property:

It follows that the set of one-step derivatives is contained in the overapproximation. This fact is captured by the following theorem:

To show that all derivatives are contained in the overapproximation ⊕(pieces r), it suffices to prove that any n-step derivative is in the overapproximation (up-to similarity).

The proof proceeds by induction on the number of derivative steps n. The base case follows from toSumSubsets_pieces_refl. For the inductive step, let e be any (n - 1)-step derivative. By the inductive hypothesis, we have that e is in the overapproximation of r, ⊕(pieces r). Then, we have that any single-step derivative f (of e) is in the overapproximation of e, ⊕(pieces e), by lemma step_to_toSumSubsets_pieces. The theorem is concluded by applying toSumSubsets_pieces_trans to show that f is contained in the overapproximation of r.

The main theorem asserts the existence of a list of regular expressions that contains the set of all iterated derivatives of a given regular expression r up-to similarity. We choose ⊕(pieces r) as the overapproximation.

In our formalization, the state space captured by the steps function only accounts for the parts of the expression at lookaround depth $0$ (i.e., not under a lookaround). This is because the derivative of a lookaround is always $\perp$ and the actual complexity of lookarounds lies in the nullability check (which is only done at matching time). A transition regex $\delta (R)$ encodes all possible transitions from $R$ with respect to any location. For a location $x$, the concrete transition is into $\delta (R)[x]$ and the computation of this target state may involve nullability checks. If the nullability check is for a subexpression of $R$ that is a lookaround, then this spawns an automaton for the lookaround body at location $x$.

Let us now informally consider the finiteness of the global state space for $R$, which includes the states induced by nullability checks of lookarounds. Finiteness follows by induction on lookaround height. For the base case $\mathrm{𝑙𝑜𝑜𝑘𝐻𝑒𝑖𝑔ℎ𝑡}(R)=0$, i.e., when $R$ contains no lookarounds, the global state space is the set of derivatives that we approximate with ⊕(pieces r) (which is finite). For the inductive case $\mathrm{𝑙𝑜𝑜𝑘𝐻𝑒𝑖𝑔ℎ𝑡}(R)=n+1$, we assume that the global state space is finite at lookaround height $n$. The set of top-level derivatives of $R$ is finite by the finiteness theorem. If a top-level state is an expression that has a lookaround as a subexpression, then computing its successor may spawn an automaton for the body of that lookaround (which has lookaround height at most $n$). By inductive hypothesis, the automaton corresponding to an expression with lookaround height $n$ has a finite global state space.

An alternative perspective on pieces is to view it as a closure operator when lifted to lists (sets) of expressions. This lifted function, piecesS, satisfies the standard properties of a closure operator: it is extensive, monotonic, and idempotent. In Lean, we define it as follows, where ∘ denotes function composition:

In order to prove finiteness in this setting, we show that

This proceeds by induction on the number of steps n. The base case follows from extensivity, since steps e 0 is just the singleton [e]. For the inductive case, we assume that

From the theorem step_to_pieces, it follows that

By applying monotonicity and idempotence on the inductive hypothesis, we get that

Finally, by transitivity we can conclude that

In the reasoning above, exactly the three properties of piecesS being a closure operator are needed. We can now prove the main finiteness theorem with piecesS [e] as the overapproximation since piecesS [e] contains all derivatives of e.

We briefly comment on the complexity aspects of our approximation for the derivatives of a regular expression. First of all, in no way is pieces r meant to be a (reasonably) precise approximation of the set of derivatives of r. It is just an upper bound of this set. The main feature is that pieces is a total function and thus pieces r is finite for any r.

Our definition for the overapproximation focuses on being easy to conceptualize, and is defined in terms of the composition of simpler components in order to make it more amenable to formal verification. In particular, the overapproximation is given in terms of the ⊕ function, which computes all non-empty subsets of permutations of a list, and the pieces function to actually traverse the regular expression. It can be shown that the computational complexity of ⊕ is already $𝒪(n!)$ in the size of the input list. The worst case of the pieces function materializes in the case for intersection, where one takes Cartesian products of the approximations of the two subexpressions.

We have shown that, for every n, every n-step derivative r’ of r is made of pieces of r. By this we mean that every element r’ of steps n r is ADI-equivalent to an element of ⊕(pieces r) (recall that ⊕(pieces r) contains every permutation of every subset of pieces r as a sum). Finiteness of the set of derivatives of r (modulo ADI) follows from the fact that the set pieces r is finite. We now describe how to integrate simplifications into the derivative computation without sacrificing finiteness. The key idea is to ensure that simplifications do not introduce any new pieces.

Our first observation is that ⊕ is monotone: if xs ⊆ ys, then ⊕xs ⊆ ⊕ys. More specifically, if an expression p’ is ADI-equivalent to an element of ⊕(pieces p), then it is also ADI-equivalent to an element of ⊕(pieces r) provided that pieces p ⊆ pieces r. This is the condition that determines allowed simplifications: r can be simplified to p if p does not introduce any new pieces (which is necessary for preserving finiteness). For us, a simplification is a function RE α → RE α that is applied after every derivative step.

We incorporate such a simplification f by defining a modified step function which applies f to every element in the result of the original step.

We define allowed simplifications f to be those that satisfy the following predicate.

Finally, we prove the following property which suffices to keep the rest of the finiteness proof almost the same as it was with just the function step. Every one-step derivative of r, after simplifications with a suitable f, is ADI-equivalent to an element of ⊕(pieces r).

Here we write r ⇝ s to say that r simplifies to s. For example, it is easy to see from the definition of pieces that the simplification rule r ⋓ s ⇝ r is nonincreasing since pieces r ⊆ pieces (r ⋓ s). It is not a valid simplification rule in the sense that it does not preserve the language. However, we can restrict ourselves to the cases where it does: r ⋓ ⊥ ⇝ r and r ⋓ ˜⊥ ⇝ ˜⊥. It is also easy to see that associativity, deduplication and idempotence can also be made into allowed simplification rules.

The simplification rule r ☀ s ⇝ s is also nonincreasing and thus is allowed. Again, this is not a valid rule but we can restrict to the cases where it is: ε ☀ s ⇝ s and r ☀ ⊥ ⇝ ⊥. Note, however, that we are not allowed to simplify r ☀ s to r as that would not be nonincreasing. The following simplification rules are allowed.

We can also compose any sequence of nonincreasing simplifications: the identity function is nonincreasing; if $f$ and $g$ are nonincreasing, then so is $g\circ f$. Also, nonincreasing simplifications satisfy certain congruences. If f is nonincreasing, then so are the following rules:

Note how the last rule keeps s fixed.

Furthermore, as the allowed simplifications are determined by pieces, we could allow more simplifications by extending the set of pieces of an expression. For example, if every expression had ⊥ as a piece, then ⊥ ☀ s ⇝ ⊥ would be allowed (or, we could ensure that pieces r is a subset of pieces (r ☀ s) which would also allow r ☀ ε ⇝ r). Similarly, more simplifications would be allowed if pieces r and pieces s were subsets of pieces (r ⋒ s). We suspect it would be relatively easy to extend pieces in this way so that the following simplifications are also allowed: