Partial derivatives of regular expressions, introduced by Antimirov, define an elegant algorithm for generating equivalent non-deterministic finite automata (NFA) with a limited number of states. Here we focus on runtime verification (RV) of simple properties expressible with regular expressions. In this case, words are finite traces of monitorable events forming the language's alphabet, and the generated NFA may have an intractable number of states. This typically occurs when sub-traces of mutually independent events are allowed to interleave. To address this issue, regular expressions used for RV are extended with the shufle operator to make specifications more compact and easier to read. Exploiting partial derivatives enables a rewriting-based approach to RV, where only one derivative is stored at each step, avoiding the construction of an intractably large automaton. This raises the question of the space complexity of the largest generated partial derivative. While the total number of generated partial derivatives is known to be linear in the size of the initial regular expression, no results can be found in the literature regarding the size of the largest partial derivative. We study this problem w. r. t. two metrics (height and size of regular expressions), and show that the former increases by at most one, while the latter is quadratic in the size of the regular expression. Surprisingly, these results also hold with shufle.
Derivatives of regular expressions were introduced by Brzozowski [
Inspired by Brzozowski’s work, Antimirov [
While Antimirov’s work addresses the classical problem of word recognition in regular languages,
here we focus on runtime verification (RV) [
RV is a technique used to check the trace of events generated during a single execution of the System Under Scrutiny (SUS). This is done with monitors automatically generated from specifications that describe the correct behavior of the SUS (suitably instrumented to produce the trace to be analyzed).
RV is complementary to both formal verification and testing: like formal methods, it is based on
specification languages, although it is not exhaustive; like testing, it is scalable and suitable for real-world
systems and complex properties. Diferently from testing, RV can detect errors even in non-deterministic
systems [
When properties to be verified can be defined with regular expressions, words are finite traces of monitorable events, which define the alphabet of the language, and the monitor is the finite automaton generated from the regular expression defining the correct traces. However, this approach may be unfeasible because of the intractable number of states of the generated automaton, even for NFAs.
This typically happens when the properties to be verified consist of sub-traces of mutually independent
events, which are allowed to interleave during the execution of the SUS. Consider, for instance, the
challenge of verifying that files are properly opened and closed, in a system able to handle multiple
ifles independently. In such cases, extending regular expressions with the shufle operator [
This raises the question of the space complexity of the largest partial derivative that can be generated from an initial regular expression. Indeed, while the total number of generated partial derivatives is known to be linear in the size of the initial regular expression, no results can be found in the literature regarding the size of the largest partial derivative.
In this paper, we investigate this problem with respect to two diferent metrics for regular expressions: their height and their total number of nodes when viewed as trees. In particular, we show that the height of the largest partial derivative can increase by at most one, while the number of nodes in the largest partial derivative is bounded by 2, where is the number of nodes of the initial regular expression. Surprisingly, these results still hold when regular expressions are extended with shufle.
To this aim, we propose a proof methodology based on the definition of a function that, given a regular expression, returns an upper bound of the increment w.r.t. a specific metric for all its partial derivatives. In this way, an invariant can be established on single rewriting steps and directly extended to multiple steps, to derive the expected space complexity results. This proof methodology allows us to keep the same proof structure for all main results, and reuse parts of the proofs.
The paper is structured as follows: Section 2 introduces the basic notion of derivatives of regular
expressions. Section 3 defines partial derivatives and proves the space complexity results w. r. t. the
height and the size of expressions. Section 4 extends regular expressions with the shufle operator, and
show that the property proved in section 3 still hold. Finally, section 5 draws conclusions and some
directions for future work. All major proofs can be found in the companion technical report [
This section provides the basic notions on derivatives, by assuming familiarity with regular expressions.
Let Σ denote a given non-empty finite set of symbols, called alphabet. We call word an element of Σ* , and denote with the empty word. Furthermore, a : w denotes the word where a is the first symbol, and w the rest of the word, while w · w ′ denotes word concatenation. The set RE of regular expressions over Σ is inductively defined by the following grammar: e :: = 0 | | a | e0e1 | e0 + e1 | e * with a ∈ Σ We use the standard precedence rules: the Kleene star operator e * has higher precedence than concatenation e0e1, which in turn has higher precedence than union e0 + e1.
Definition 2.1 introduces the standard operators on regular languages, and definition 2.2 the standard semantics of regular expressions.
Definition 2.1. For all L, L0, L1 ⊆ Σ* Definition 2.2.
L1 · L2 = {w1 · w2 | w1 ∈ L1, w2 ∈ L2}
L0 = { }, L+1 = L · Lfor all ≥ 0
L * = ⋃︀≥ 0 L 0 = ∅ J K = { } J K a = {a} J K
Je0e1K = Je0K · Je1K
Je0 + e1K = Je0K ∪ Je1K
Je0 * K = Je0K *
Note the diference between (a constant in the syntax of regular expressions) and (the empty word).
The derivative [
Directly from definition 2.3 one can derive w ∈ L if ∈ w − 1(L) (1)
While the notion of derivative applies to any formal language, regular languages enjoy the following closure property: if L is regular, then w − 1(L) is regular as well, for any word w . In other words, the derivative of a regular expression can be defined by another regular expression.
This property allows an operational and succinct definition for the derivatives of regular expressions. First, the derivative w. r. t. a single symbol is defined (see fig. 1), then the more general notion of derivative w. r. t. a word is derived by reflexive transitive closure (see definition 2.4).
Here we deliberately follow the style of a labelled transition system, defined by means of inference
rules, to highlight two interesting related aspects:1
• derivatives provide an intuitive way to define a small-step semantics for regular expressions;
• a reduction step e→− a e′ corresponds to a transition step from the state represented by e to a state
represented by e′ with symbol a, for an automaton which recognizes the language defined by e.
By using the notation of Antimirov [
The definition of (e) in fig. 1 deserves some comments: the intended meaning is that (e) = if e , and, dually, (e) = 0 if ̸∈ JeK. The base cases of the definition are straightforward; thanks ∈ J K to the auxiliary functions and, or defined on and 0 in the corresponding tables, we can deduce that, as expected, e0e1 recognizes if both e0 and e1 recognize , while e0 + e1 recognizes if e0 or e1 recognizes .
The fact that (e) does not return a Boolean value was a deliberate choice of Brzozowski to define rule (cat) in a more compact way: if (e0) = , then e0e→1− a e0′ + e1′, since in this case e1 contributes to the derivative. Otherwise, e0e→1− a e0′ + 0e1′, since e1 does not contribute to the derivative.
Note that by definition of the rules, for all e and a, there always exists a unique derivative of e w. r. t. a. For instance, if a ̸= b, a ̸= c, then ab+ac→− a ( b+00)+( c+00) and ab+ac→− b (0b+0 )+(0c+00).
Definition 2.4 introduces the general notion of derivative w. r. t. a word w , by computing the reflexive transitive closure of the one-step relation defined in fig. 1. As expected, the definition is by induction 2 on the length of w . The multiple-steps rewriting relation provides also the operational semantics of regular expressions w. r. t. derivatives, driven by eq. (1). In the view above, which considers the labelled transition system as a deterministic automaton, the definition corresponds to that of accepted language, 1To the best of our knowledge, no previous work has used this style to define the (partial) derivatives of regular expressions. 2It is worth noting that the computation of a derivative always “terminates” in a finite number of steps, because words have ifnite length.
(cat) (empty) 0→− a 0 (eps)
→− a 0 e→0− a e′ e→1− a e′
0 1 e0e→1− a e0′e1 + (e0)e1′ (sym-eq) a→− a
(sym-neq) a→− b 0 (or) e→0− a e′ e→1− a e′
0 1 e0 + e→1− a e0′ + e1′ a ̸= b e→− a e′ e *→− a e′e * (star) or 0 0 0 ( ) = (e0 * ) = (0) = (a) = 0 (e0e1) = (e0) and (e1) (e0 + e1) = (e0) or (e1) and 0 0 0 0 0 that the set of all syntactically distinct derivatives of a regular expression e is generally unbounded, and so is their size. Hence, the underlying automaton is infinite, unless some finite quotient algebra of states modulo a suitable congruence is considered.
Definition 2.4. For all e, e0, e1 ∈ RE , a ∈ Σ, w ∈ Σ*
e→− e J →K− e e→0−− a:w e1 if e→0−
a e and e→− w e1 = {w ∈ Σ* | there exists e′ ∈ RE s.t. e→− w e′ and (e′) = }
are sound w. r. t. their intended semantics, and the operational semantics of regular expressions is equivalent to the standard one.
Theorem 2.5. For all e, e′ ∈ RE , w ∈ Σ* (e) = if ∈ JeK e→− w e′ implies w − 1( e ) = e′
J K
J K e
3This is for eficiency reasons, though the obtained states are still used by Antimirov to generate an NFA.
Rules (cat) and (or) in fig. 1 are split in fig. 2 in the two possibly overlapping
and (l-or), (r-or), respectively. For instance, according to Antimirov’s definition 5, the partial derivative of ab+ac w. r. t. symbol a returns the set of regular expressions { b, c} (that is, a(ab+ac) = { b, c} with Antimirov’s notation). This corresponds to the fact that there exist two possible transition steps from ab + ac labeled with a, namely, ab + ac − ⇀a b and ab + ac − ⇀a c.
Another diference with derivatives is that in fig. 2 there are no rules returning the empty derivative. Therefore, there are cases where the partial derivative of a regular expression w. r. t. a symbol (or word) does not exist. This is useful when partial derivatives are used for RV, because in this way errors can be detected with no further checks on the partial derivative: if no moves can be taken, then the partial derivative is empty and the trace of events (that is, the word) considered so far cannot be the prefix of any correct trace, therefore a violation of the specification can be reported.
Finally, a major diference between derivatives and partial derivatives lies in the fact that the set of all syntactically distinct partial derivatives of a given regular expression e is bounded by the size of e. This means that, after a single partial derivative is generated at each rewriting step, there is no need to simplify it in order to keep the size of partial derivatives bounded.
Definition 3.1 is dual to Definition 2.4.
Definition 3.1. For all e, e0, e1 ∈ RE , a ∈ Σ, w ∈ Σ*
e −⇀ e e0− −
a:⇀w e1 if e0 − ⇀a e and e − ⇀w e1
JeK−⇀ = {w ∈ Σ* | there exists e′ ∈ RE s.t. e − ⇀w e′ and (e′) = }
The claims below are dual to theorem 2.5, and directly follow from the results of Antimirov [
e′∈ w (e) Je′K and JeK−⇀ = e
J →K− .
Theorem 3.2. For all e ∈ RE , w − 1( e ) = ⋃︀
J K Corollary 3.3. For all e ∈ RE , JeK−⇀ = JeK.
Theorem 3.4. For all e ∈ RE , w (e) is bounded. 3.1. Height of partial derivatives In this section we investigate the upper bound on the height of the partial derivatives of a given regular expression, defined in a standard way as follows: | | = |a| = 0 |e0e1| = |e0 + e1| = max(|e0|, |e1|) + 1 |e *| = |e| + 1 Since the height of the partial derivative of an expression e w. r. t. a word w both depends on the shape of e and on w , we need to reason on any possible e and w . Moreover, we aim at providing a general proof methodology which can be followed to prove results when considering also shufle and the size of expressions.
To show a couple of examples let us consider the following reduction steps which compute the partial derivatives of a * b * w. r. t. ab and bb: a * b * − |a * b *| = 2 ⇀a ( a * )b * − b ⇀ b * |( a * )b *| = 3 b
b a * b * −
⇀ b * −⇀ b * | b *| = 2 4In the sense that for some regular expressions and symbols, both are applicable.
The following theorem is based as well on the results proved by Antimirov [
by one; increase; |e′| ≤ | e| + 1.
In the first example the height increases by one after the first step and decreases by one after the second, while in the second example the height of the expressions is unchanged.
What we are going to prove are the following main properties: 1. the height of the partial derivative of a regular expression w. r. t. a symbol can increase at most 2. the height of the partial derivative of a partial derivative w. r. t. a non-empty word, cannot
Although these properties can be proved in a direct way, they must be adapted when the size of expressions is considered. Furthermore, they do not hold in this stronger form, when shufle is added. Therefore we provide a more general proof methodology which works for both metrics on expressions, and can be adapted to the case of shufle, where weaker claims hold. e′, e′ ∈ RE , w ∈ Σ* }.
In order to do that, we define the function
Δmax(e) which returns an upper bound for |e′| − | e|, where e − ⇀w e′, with e′ ∈ RE , w ∈ Σ* . That is, if e = def. max{|e′| − | e| | e − ⇀w e′, e′ ∈ RE , w ∈ Σ* }, then a sound definition of provides an upper bound for the height of all partial derivatives of e: |e| + Δmax(e) ≥ max{|e′| | e − ⇀ Δmax(e) has to satisfy the constraint Δmax(e) ≥ e . Hence, |e| + Δmax(we) Definition 3.5. The function Δmax(e) is recursively defined as follows: Δmax(a) = Δmax( ) = 0 Δmax(e0 + e1) = 0 Δmax(e * ) = 1 Δmax(e0e1) = geq (e0, e1) · Δmax(e0) where geq (e0, e1) = {︃1, if |e0| ≥ | e1|
0, if |e0| < |e1|
Before commenting the definition of Δmax(e), we introduce the following straightforward lemma. Lemma 3.6. For all e ∈ RE , 0 ≤
Δmax(e) ≤ 1.
Proof. Directly by induction on the definition of Δmax(e). Δmax(e) = 0. by |e| + 1.
Because e −⇀ e, 0 ∈ {|e′| − | e| | e − ⇀w e′, e′ ∈ RE , w ∈ Σ* } and the constraint 0 ≤ Δmax(e) must always be met. The constraint Δmax(e) ≤
1 corresponds to what we want to prove in item 3 above.
The definition of
Δmax(e) is driven by the reduction rules in fig. 2 and by the property in item 3.
We comment only the non-trivial cases: if e = e0 + e1, then we expect |e′| ≤ | e| + 1, = 0, 1, hence |e′| ≤ | e| and Δmax(e) = 0; if e = e0 * , then we expect |e0′| ≤ | e0| + 1, hence |e0′e0 *| ≤ | and Δmax(e) = 1. Finally, the definition for e = e0e1 requires more care: if rule (l-cat) is applied, e| + 1 then |e0′e1| = |e| + 1, but only when |e0′| = |e0| + 1 and |e0| ≥ | e1|, otherwise |e0′e1| ≤ | e|; if rule (r-cat) is applied, then |e1′| ≤ | e|, as happens for rule (r-or). Therefore Δmax(e) = 1 if Δmax(e0) = 1 and |e0| ≥ | e1|, that is, geq (e0, e1) = 1. In all other cases, that is Δmax(e0) = 0 or geq (e0, e1) = 0,
The following theorem proves the soundness of the definition of Δmax w. r. t. its intended meaning. As a consequence, the height of the derivative of an expression e w. r. t. a symbol is always bounded Theorem 3.7. For all e, e′ ∈ RE , a ∈ Σ, if e − ⇀a e′, then |e′| ≤ | e| + Δmax(e).
The following corollary can be directly derived from theorem 3.7 and lemma 3.6.
Corollary 3.8. For all e, e′ ∈ RE , and a ∈ Σ, if e − ⇀a e′, then |e′| ≤ | e| + 1.
Theorem 3.7 shows that the height of the derivative of an expression e w. r. t. a symbol is bounded by |e| + 1. The following results prove a strong property: the height of the partial derivative of a partial derivative cannot increase; that is, after the first reduction step, the height of the derivative of an expression e w. r. t. a symbol is bounded by |e|. Therefore, one can conclude that the height of the derivative of an expression e w. r. t. an arbitrary word (not just a symbol) is bounded by |e| + 1. Lemma 3.9. For all e, e′ ∈ RE , and a ∈ Σ, if e − ⇀a e′, then Δmax(e′) = 0.
Given lemma 3.9, the following corollary may look useless, but it provides a general form of invariant which can be proved also for all other considered cases, where the strong claim of lemma 3.9 no longer holds.
Corollary 3.10. For all e, e′ ∈ RE , a ∈ Σ, if e − ⇀a e′, then |e′| ≤ | e| + Δmax(e) − Δmax(e′). Proof. A direct consequence of theorem 3.7 and lemma 3.9.
To provide intuition for the invariant of corollary 3.10, let us consider the following equivalent form: |e′| + Δmax(e′) ≤ | e| + Δmax(e) (2)
As noted in the previous page, |e′| + Δmax(e′) and |e| + Δmax(e) define the upper bound of the height of all partial derivatives of e′ and e, respectively. But e′ is a partial derivative of e because e − ⇀a e′, hence, by transitivity, the set ′ of all partial derivatives of e′ is a subset of all partial derivatives of e.
The following theorem shows that the invariant property of corollary 3.10 can be extended to derivatives w. r. t. any words.
Theorem 3.11. For all e, e′ ∈ RE , and w ∈ Σ* , if e − ⇀w e′, then |e′| ≤ | e| + Δmax(e) − Δmax(e′). Proof. By induction on the length of w . base case: if w = , then by definition e′ = e, hence |e′| = |e| and Δmax(e) = Δmax(e′), therefore |e′| = |e| ≤ | e| + Δmax(e) − Δmax(e′). inductive step: if w = a : w ′ for some a ∈ Σ, w ′ ∈ Σ* , then by definition there exists e′′ ∈ RE s.t. e − ⇀a e′′ and e′′ − w⇀′ e′. By corollary 3.10 |e′′| ≤ | e| + Δmax(e) − Δmax(e′′) and by inductive hypothesis |e′| ≤ | e′′|+Δmax(e′′)− Δmax(e′). Therefore by transitivity, |e′| ≤ | e′′|+Δmax(e′′)− Δmax(e′) ≤ | e| + Δmax(e) − Δmax(e′′) + Δmax(e′′) − Δmax(e′) = |e| + Δmax(e) − Δmax(e′).
The proof of theorem 3.11 is independent from the definition of Δmax, providing that the invariant of corollary 3.10 holds. Therefore, the crucial point is the definition of the function returning the upper bound of the increment of a partial derivation.
The result on the space complexity of derivatives can be directly derived from theorem 3.11 and lemma 3.6.
Corollary 3.12. For all e, e′ ∈ RE , and w ∈ Σ* , if e − ⇀w e′, then |e′| ≤ | e| + 1.
Proof. By theorem 3.11 |e′| ≤ | e| + Δmax(e) − hence |e′| ≤ | e| + 1.
Δmax(e′). By lemma 3.6 Δmax(e) − Δmax(e′) ≤ 1, 3.2. Size of partial derivatives In this section we investigate the upper bound on the size of the partial derivatives of a given regular expression, defined in a standard way as follows: || || = ||a|| = 1 ||e0e1|| = ||e0 + e1|| = ||e0|| + ||e1|| + 1 ||e *|| = ||e|| + 1
The results of section 3.1 must be adapted to the less trivial case of the size of expressions. Indeed, while for the height the upper bound of the increment is the constant 1, for the size this value depends on the square of the initial regular expression.
For instance, let us consider the following reduction steps which compute the partial derivative of a * * * w. r. t. aa: a * * * ||a * * *|| − ⇀a (( a * )a * * )a * * * − ⇀a (( a * )a * * )a * * *
= 4 ||(( a * )a * * )a * * *|| = 13 After the first step the size increases by 9 and remains unchanged after the second step. For expressions of the general shape e = a * . . . * it can be proved by induction on = ||e|| ≥ 2 that if e − ⇀a e′, then ||e′|| = ||e|| + 22+ − 1.
As another example, let us consider the following reduction steps which compute the partial derivative of (a * b * )c * w. r. t. abc: ab * * − ⇀a b * * − ⇀b ( b * )b * * ||ab * *|| = 5 || b * *|| = 5 ||( b * )b * *|| After the first step the size does not change, while increases by 3 after the second step. This example shows that the strong claim of lemma 3.9 cannot hold for || ||.
We follow the same methodology as in section 3.1 and define the function max(e), analogous to Δmax(e), for the size of e.
Definition 3.13. The function max(e) is recursively defined as follows: max(a) = max( ) = 0 max(e0e1) = max( max(e0), max(e1) − || e0|| − 1) max(e0 + e1) = max( max(e0) − || e1|| − 1, max(e1) − || e0|| − 1, 0) max(e * ) = ||e|| + max(e) + 1
The following lemma is analogous to lemma 3.6.
Lemma 3.14. For all e ∈ RE , 0 ≤ max(e) ≤ || e||2.
As for Δmax(e), the definition of max(e) is driven by the reduction rules in fig. 2, and by the definition of size. We comment only the non-trivial cases: if e = e0 + e1, then the partial derivative can be obtained by applying either rule (l-or) or (r-or). For the former rule, the partial derivative of e0 can increase of at most max(e0), but all the nodes of e1 and the + operator are removed, which corresponds to max(e0) − || e1|| − 1. The reasoning for the latter rule is symmetric. Then the maximum between these two values has to be considered to return a valid upper bound; furthermore, the bound must be non-negative for the same reason explained for Δmax. If e = e0 * , then the new term e′ needs to be considered, whose size is bounded by ||e|| + max(e). Furthermore, the concatenation operator is added, hence the function returns ||e|| + max(e) + 1. Finally, in the definition for e = e0e1 rule (r-cat) is managed as rule (r-or) (or (l-or)). In rule (l-cat) e0 is replaced by e0′, while e1 and concatenation are kept, hence the upper bound of the increment is max(e0). As for e0 + e1 the maximum needs to be considered.
Although the analogous of lemma 3.9 cannot be proved for max, the invariant of corollary 3.10 holds, and can be proved directly.
Theorem 3.15. For all e, e′ ∈ RE , a ∈ Σ, if e − ⇀a e′, then ||e′|| ≤ || e|| + max(e) − max(e′).
Having proved the invariant of theorem 3.15, we can derive the main result analogously as done in section 3.1.
Theorem 3.16. For all e, e′ ∈ RE , and w ∈ Σ* , if e − ⇀w e′, then ||e′|| ≤ || e|| + max(e) − max(e′). Proof. See theorem 3.11
The result on the space complexity of derivatives directly follows from theorem 3.16 and lemma 3.14. Corollary 3.17. For all e, e′ ∈ RE , and w ∈ Σ* , if e − ⇀w e′, then ||e′|| ≤ || e|| + ||e||2. Hence ||e′|| is (||e||2).
Proof. By theorem 3.16 ||e′|| ≤ || e||+ max(e)− max(e′). By lemma 3.6 max(e)− max(e′) ≤ max(e) ≤ ||e||2, hence ||e′|| ≤ || e|| + ||e||2.
4.1. Basic definitions In this section we extend the syntax of regular expressions by adding the shufle operator 6 e0 || e1 whose semantics is defined as follows by extending definition 2.1 and definition 2.2: || w = w || = {w } L1 || L2 = ⋃︀w1∈L1,w2∈L2 (w1 || w2) (a1w1) || (a2w2) = {a1} · (w1 || (a2w2)) ∪ {a2} · ((a1w1) || w2)
Je0 || e1K = Je0K || Je1K We denote with RE + the set of regular expressions extended with the shufle operator.
Although it is well-known that the shufle operator does not increase the abstract expressive power
of regular expressions, in practice it is still very useful in RV to write much more compact and clear
specifications when correct system behaviors can be described as independently interleaved event
traces. Indeed, it has been proved [
Let us consider for instance the distinct events , , and , with the meaning “file has been opened”, “accessed”, and “closed”, respectively, where = 1, 2 is the corresponding file descriptor. If the SUS is allowed to manage the two files independently, then a specification for the correct use of them can be defined quite concisely by the regular expression 11 * 1 || 22 * 2.
If, for simplicity, we assume that files can be accessed only once, and we generalize over the number of files, then the specification becomes the regular expression 111 || . . . || over the alphabet of 3 distinct symbols {1, 1, 1, . . . , , , }. For such an expression, an equivalent NFA must have at least 4 states.
(shf) e→0− a e0′ e→1− a e′
1 e0 || e→1− a (e0′ || e1) + (e0 || e1′)
(e0 || e1) = (e0) and (e1) (l-shf)
e0 − ⇀a e0′ e0 || e1 − ⇀a e0′ || e1 (r-shf)
e1 − ⇀a e1′ e0 || e1 − ⇀a e0 || e1′
The transition rules defining the derivative and the partial derivatives for the shufle operator can be found in fig. 3. They all correspond to the intuition that events can be interleaved; moreover, the empty trace is contained in e0 || e1 if it is contained in e0 and e1. 6In the examples we assume that the shufle has lower precedence than the concatenation and union operator.
As happens for the other operators, also with the shufle the derivative is always defined, while this is not the case for partial derivatives. For instance, if we assume a2 ̸= a0 and a2 ̸= a1, then a0 || a1 →−a2 (0 || a1) + (a0 || 0), and ((0 || a1) + (a0 || 0)) = 0, but there exists no e s.t. a0 || a1 − a⇀2 e.
Theorems 2.5 and 3.2 still hold along with corollary 3.3, when RE + is considered. 4.2. Height of partial derivatives with the shufle operator We extend the result of theorem 3.11 and corollary 3.12 to the case of the shufle operators.
Unfortunately the proofs are more challenging because the claim of lemma 3.9 no longer holds: There exist partial derivatives e s. t. Δmax(e) > 0. As a counter example, let us consider the following reduction steps computing the partial derivatives of ( || a * )(b || a * ) w. r. t. aba: e0 − ⇀a e1 − ⇀b e2 − ⇀a e3 e0 = ( || a * )(b || a * ) e1 = ( || a * )(b || a * ) e2 = || a * e3 = || a * We have |e1| = |e0| + 1 (first reduction step), but also |e3| = |e2| + 1 (third reduction step). Therefore, necessarily Δmax(e2) > 0, to ensure that eq. (2) holds.
To prove the extended versions of the results of section 3 we first extend the definition of Δmax given in definition 3.5 with the case for the shufle.
Δmax(e0 || e1) = max(geq (e0, e1) · Δmax(e0), geq (e1, e0) · Δmax(e1)) Before explaining the definition of Δmax above, we note that the claim of lemma 3.6 holds also for RE + and can still be proved by induction on the definition of Δmax: 0 ≤ Δmax(e) ≤ 1. Consequently, if the height of one sub-expression e is strictly greater than the other e1− , then only the partial derivative of e can contribute to the increment of the height of the partial derivative of e0 || e1, because increments are always bounded by 1. Note that max(Δmax(e), 0) = Δmax(e), since Δmax(e) ≥ 0, therefore Δmax(e0 || e1) = Δmax(e), if |e| > |e1− | for = 0, 1.
If |e0| = |e1|, then both the derivatives of e0 and e1 can contribute to the increment of the height of the partial derivative of e0 || e1. Since (l-shf) or (r-shf) can be non-deterministically applied, the maximum increment max(Δmax(e0), Δmax(e1)) needs to be considered.
The correctness of the definition of Δmax(e0 || e1) is still ensured by the claim of theorem 3.7 extended to RE +.
Proof of theorem 3.7 extended to RE + For all e, e′ ∈ RE +, a ∈ Σ, if e − ⇀a e′, then |e′| ≤ | e| + Δmax(e).
Proof. The structure of the proof is the same, but the two new rules for the shufle operator need to be considered.
• rule (l-shf): By inductive hypothesis |e0′| ≤ | e0| + Δmax(e0). We distinguish two cases: – |e0| ≥ | e1|: |e0′ || e1| d=ef max(|e0′|, |e1|) + 1 ≤ max(|e0| + Δmax(e0), |e1|) + 1 ≤ max(|e0|, |e1|) + 1 + Δmax(e0) ≤ max(|e0|, |e1|) + 1 + Δmax(e0 || e1) = |e0 || e1| + Δmax(e0 || e1), where inequalities are derived from the inductive hypothesis, the definition of max, | |, Δmax, and geq , the assumption |e0| ≥ | e1|, and lemma 3.6. – |e0| < |e1| (that is, |e0| + Δmax(e0) ≤ | e1| by lemma 3.6): |e0′ || e1| d=ef max(|e0′|, |e1|) + 1 ≤ max(|e0| + Δmax(e0), |e1|) + 1 = |e0 || e1| ≤ | e0 || e1| + Δmax(e0 || e1), where inequalities are derived from the inductive hypothesis, the definition of max, | |, Δmax, and geq , the assumption |e0| < |e1|, and lemma 3.6.
• rule (r-shf) is symmetric to rule (l-shf).
Since both lemma 3.6 and theorem 3.7 hold for RE +, corollary 3.8 holds for RE + as well.
To prove for RE + the invariant defined by eq. (2), we modularize the proof by introducing two lemmas.
The first lemma is a weaker version of lemma 3.9.
Lemma 4.1. For all e, e′ ∈ RE +, and a ∈ Σ, if e − ⇀a e′ and |e′| = |e| + 1, then Δmax(e′) = 0.
The second lemma establishes an invariant on Δmax when the height of the derivatives does not change.
Lemma 4.2. For all e, e′ ∈ RE +, and a ∈ Σ, if e − ⇀a e′ and |e′| = |e|, then Δmax(e′) ≤ Δmax(e).
Theorem 4.3. For all e, e′ ∈ RE +, a ∈ Σ, if e − ⇀a e′, then |e′| ≤ | e| + Δmax(e) − Δmax(e′).
From theorem 4.3 and lemma 3.6 (extended to RE +) we can extend for free theorem 3.11 and corollary 3.12 to RE +.
Theorem 4.4. For all e, e′ ∈ RE +, and w ∈ Σ* , if e − ⇀w e′, then |e′| ≤ | e| + Δmax(e) − Δmax(e′).
Corollary 4.5. For all e, e′ ∈ RE +, and w ∈ Σ* , if e − ⇀w e′, then |e′| ≤ | e| + 1. 4.3. Size of partial derivatives with the shufle operator Similar as done in the previous section, we extend the result of theorem 3.16 and corollary 3.17 to the case of the shufle operator in the case of the size ||e|| of a regular expression e.
Also for the size, the introduction of shufle does not afect the space complexity of partial derivatives. However, in this case the proofs can be extended in an easier way, although the definition of max(e0 || e1) requires some care.
Indeed, one would be tempted to consider the following (incorrect) definition: max(e0 || e1) = max( max(e0), max(e1)) (incorrect definition) Unfortunately, this definition verifies only the weaker inequality e0 || e1 − ⇀a e, but not ||e|| ≤ || e0 || e1|| + max(e0 || e1) − max(e).
To show this, let us consider the following reduction step computing the partial derivative of a * || b * w. r. t. a: ||e|| ≤ || e0 || e1|| + max(e0 || e1), if a a * || b * −⇀ a * || b * ||a * || b *|| = 5 max(a * || b * ) = 2 || a * || b *|| = 7 max( a * || b * ) = 2 We have || a * || b *|| = 7 ≤ 5 + 2 = ||a * || b *|| + max(a * || b * ), but || a * || b *|| = 7 ̸≤ 5 + 2 − 2 = ||a * || b *|| + max(a * || b * ) − max( a * || b * ).
To guarantee the invariant ||e′|| ≤ || e|| + max(e) − max(e′), the following definition has to be considered: max(e0 || e1) = max(e0) + max(e1) (correct definition) This new definition takes into account increments due to multiple reduction steps. In this way, we obtain || a * || b *|| = 7 ≤ 5 + 4 − 2 = ||a * || b *|| + max(a * || b * ) − max( a * || b * ).
The correctness of the definition of max(e0 || e1) is ensured by the claim of theorem 3.15 extended to RE +. For all e, e′ ∈ RE +, a ∈ Σ, if e − ⇀a e′, then ||e′|| ≤ | e| + max(e) − max(e′).
Proof. The structure of the proof is the same, but the two new rules for the shufle operator need to be considered.
• rule (l-shf): By inductive hypothesis ||e0′|| ≤ || e0|| + max(e0) − max(e0′).
We have ||e0′ || e1|| = ||e0′|| + ||e1|| + 1 ≤ || e0|| + max(e0) − max(e0′) + ||e1|| + 1 = ||e0 || e1|| + max(e0 || e1)− max(e1)− max(e0′ || e1)+ max(e1) = ||e0 || e1||+ max(e0 || e1)− max(e0′ || e1), by the inductive hypothesis, the definition of || ||, and max.
• rule (r-shf) is symmetric to rule (l-shf).
From theorem 3.15 and lemma 3.14 (extended to RE +) we can extend for free theorem 3.16 and corollary 3.17 to RE +.
Theorem 4.6. For all e, e′ ∈ RE +, and w ∈ Σ* , if e − ⇀w e′, then ||e′|| ≤ || e|| + max(e) − max(e′). Corollary 4.7. For all e, e′ ∈ RE +, and w ∈ Σ* , if e − ⇀w e′, then ||e′|| ≤ || e|| + ||e||2. Hence ||e′|| is (||e||2).
We have explored the space complexity of partial derivatives of regular expressions in the context of RV with regular expressions extended with the shufle operator. While the size of the set of syntactically distinct partial derivatives of a regular expression e is known to be linear in the size of e, no bounds on the size of the largest derivative had been previously investigated. We fill this gap by analyzing the height and size of partial derivatives and establishing upper bounds for both metrics.
We have shown that the height of any partial derivative of a regular expression increases by at most one, and that this property still holds when the shufle operator is considered. Furthermore, we proved that the size of the largest partial derivative is bounded quadratically in the size of the original expression. This quadratic bound also holds in the presence of shufle, despite with this operator there exist regular expressions whose equivalent NFAs exhibit an exponential explosion of the number of states.
Our approach is based on a general proof methodology that defines functions to compute upper bounds on the increase in height and size of the partial derivatives. These functions allows us to establish an invariant that can be generalized to multiple rewriting steps, enabling a modular and reusable proof structure. This methodology allowed us to seamlessly extend our results to a more complex operator like shufle.
Our results support the practical use of partial derivatives in rewriting-based RV, ensuring that the memory usage remains manageable even in the worst case. Moreover, they show that the shufle operator is useful for writing short and readable specifications without incurring high computational costs.
Short-term future work includes the extension of our analysis to other improvements of the expressive power of regular expressions, for instance with the use of additional operators or parameterized specifications.
During the preparation of this work, the authors used ChatGPT in order to: Grammar and spelling check, Paraphrase and reword. After using this tool/service, the authors reviewed and edited the content as needed and take full responsibility for the publication’s content.