Forkable Regular Expressions
Martin Sulzmann1 and Peter Thiemann2

arXiv:1510.07293v2 [cs.FL] 8 Dec 2015

1

Faculty of Computer Science and Business Information Systems
Karlsruhe University of Applied Sciences
Moltkestrasse 30, 76133 Karlsruhe, Germany
martin.sulzmann@hs-karlsruhe.de
2
Faculty of Engineering, University of Freiburg
Georges-Köhler-Allee 079, 79110 Freiburg, Germany
thiemann@acm.org

Abstract. We consider forkable regular expressions, which enrich regular expressions with a fork operator, to establish a formal basis for static
and dynamic analysis of the communication behavior of concurrent programs. We define a novel compositional semantics for forkable expressions, establish their fundamental properties, and define derivatives for
them as a basis for the generation of automata, for matching, and for
language containment tests.
Forkable expressions may give rise to non-regular languages, in general,
but we identify sufficient conditions on expressions that guarantee finiteness of the automata construction via derivatives.
Keywords: automata and logic, forkable expressions, derivatives

1

Introduction

Languages like Concurrent ML and Go come with built-in support for finegrained concurrency, dynamic thread creation, and channel-based communication. Analyzing the communication behavior of programs in these languages
may be done by an effect system. Such a system computes an abstraction of the
sequences of events (i.e., the communication traces with events like communication actions or synchronizations) that a program may exhibit.
Effect systems for concurrent programs have been explored by the Nielsons [12], who proposed to model event traces with “behaviors” which are regular
expressions extended with a fork operator that encapsulates the behavior of a
newly created thread. While their work enables the analysis of finiteness properties of the communication topology, it stops short of providing a semantics of
behaviors in terms of effect traces. Subsequent work by the same authors [1,2,11]
concentrates on subtyping and automatic inference of effects.
We take up the Nielsons’ notion of behavior and tackle the problem of defining a compositional semantics for behaviors in terms of effect traces. Our novel
definition yields a semantic basis for the static and dynamic analysis of concurrent languages with dynamic thread creation and other communication effects.

2

Martin Sulzmann and Peter Thiemann

We show that, in general, a behavior may give rise to a non-regular trace language. This observation is in line with previous work on concurrent regular
expressions [4], flow expressions [13], and shuffle expressions [6] all of which augment regular expressions with (at least) shuffle and shuffle closure operators. The
shuffle closure is also referred to as the iterated shuffle [7].
We explore two application areas for forkable expressions. In a run-time verification setting (aka dynamic analysis), we are interested in matching traces
against behaviors, either at run time or post-mortem. To this end, we extend
Brzozowski derivatives to forkable expressions. Although Brzozowski’s construction no longer gives rise to a finite automaton, in general, derivatives can still
be used to solve instances of the word problem (which is hence decidable).
For static analysis, we are interested in approximation and testing language
containment in a specification. For this use case, we give a decidable criterium
that guarantees finiteness of (our extension of) Brzozowski’s automaton construction. This criterium essentially requires a finite communication topology, that is,
it forbids that new communicating threads are created in loops. We conjecture
that this property can be established with the Nielsons’ original analysis [12].
In summary our contributions are:
– In Section 3, we define a novel trace semantics of behaviors (i.e., regular
expressions with fork), and establish their fundamental properties.
– Section 4 extends Brzozowski’s derivative operation to behaviors.
– In Section 5, we characterize a class of behaviors with regular trace languages.
For these behaviors, Brzozowski’s construction yields finite automata.
Related work is discussed in Section 6.
The online version of this paper contains an appendix with all proofs.

2

3

Preliminaries

For a set X, we write ♯X for the cardinality of X and ℘(X) for its powerset. If
F : ℘(X) → ℘(X) is a monotone function (i.e., X ⊆ Y implies F (X) ⊆ F (Y )),
then we write µF for the least fixpoint of this function, which is uniquely defined
due to Tarski’s theorem. We write µX.e for the fixpoint µ(λX.e) where e is a
set-valued expression composed of monotone functions assuming that X is a set
with the same type of elements. (The scope of the µ operator extends as far to
the right as possible.) We will employ this operator to define the meaning of
forkable Kleene star behaviors [10].
Let Σ be a finite set, the alphabet of primitive events. We write Σ ∗ for the set
of finite words over Σ and denote with v·w the concatenation of words v, w ∈ Σ ∗ .
For languages L, M ⊆ ℘(Σ ∗ ), we write L · M = {v · w | v ∈ L, w ∈ M } for the set
of all pairwise concatenations. We write v · M as a shorthand for {v} · M . The
(asynchronous) shuffle operation vkw ⊆ Σ ∗ on words is the set of all interleavings
of words v and w. It is defined inductively by
εkw = {w}
3

vkε = {v}

http://arxiv.org/abs/1510.07293

xvkyw = {x} · (vkyw) ∪ {y} · (xvkw)

Forkable Regular Expressions

L(r) = L(r, {ε})

L(φ, K) = ∅
L(ε, K) = K
L(x, K) = {x} · K

L(r + s, K)
L(r · s, K)
L(r ∗ , K)
L(Fork (r ), K)

3

= L(r, K) ∪ L(s, K)
= L(r, L(s, K))
= µX.L(r, X) ∪ K
= L(r)kK

Fig. 1. Trace language of a behavior

S
The shuffle operation is lifted to languages by LkM = {vkw | v ∈ L, w ∈ M }.
We write L1 \L2 to denote the left quotient of L2 with L1 where L1 \L2 =
{w | ∃v ∈ L1 .v · w ∈ L2 }. We write x\L as a shorthand for {x}\L.

3

Behaviors

Recall that Σ is the alphabet of primitive events. Intuitively, a primitive event
x ∈ Σ is a globally visible side effect like sending or receiving a message. A
behavior is a regular expression over Σ extended with a new fork operator.
r, s, t ::= φ | ε | x | r + s | r · s | r∗ | Fork (r ) | (r)
As usual, we assume that · binds tighter than +.
The semantics of a behavior r is going to be a trace language L(r) ⊆ Σ ∗ .
However, due to the presence of the fork operator, its definition is not a simple
extension of the standard semantics J·K of a regular expression.
Definition 1. Figure 1 defines, for a behavior r, the trace languages L(r) ⊆ Σ ∗
and L(r, K) ⊆ Σ ∗ with respect to a continuation language K ⊆ Σ ∗ .
By induction on r, we can show that the mapping K 7→ L(r, K) in ℘(Σ ∗ ) →
℘(Σ ∗ ) is monotone, so that L is well-defined. For fork-free behaviors that do not
make use of the Fork (r ) operator, the trace language is regular and coincides
with the standard semantics JrK of a regular expression.
Theorem 2. If r is fork-free, then L(r) is regular and L(r) = JrK.
It is known that the regular languages are closed under the shuffle operation [5]. However, for forkable expressions the semantics of Fork (r ) is defined
by shuffling with the continuation language so that the language defined by a
behavior need not be regular as the following example shows.
∗

Example 3. Consider the behavior Fork (s) for a plain regular expression s
where s only consists of the standard regular expression operators. Its semantics
is the shuffle closure of JsK as demonstrated by the following calculation
∗

L(Fork (s) , {ε}) = µX.L(Fork (s), X) ∪ {ε} = µX.L(s)kX ∪ {ε}
= {ε} ∪ L(s) ∪ L(s)kL(s) ∪ . . .
where we assume that k binds tighter than ∪.

(1)

4

Martin Sulzmann and Peter Thiemann
C(φ)
C(ε)
C(x)
C(r + s)
C(r · s)
C(r ∗ )
C(Fork (r ))

=
=
=
=
=
=
=

φ
ε
φ
C(r) + C(s)
C(r) · C(s)
C(r)∗
Fork (r )

S(φ)
S(ε)
S(x)
S(r + s)
S(r · s)
S(r ∗ )
S(Fork (r ))

=
=
=
=
=
=
=

φ
φ
x
S(r) + S(s)
S(r) · s + C(r) · S(s)
C(r)∗ · S(r) · r ∗
φ

Fig. 2. Concurrent and sequential part of a behavior

In general, the shuffle closure is not regular [7] as the following concrete in∗
stance shows. Consider the behavior r = Fork (x · y + y · x ) . By the calculation
in (1), L(r) is the shuffle closure of {x · y, y · x} which happens to be the contextfree language {w ∈ {x, y}∗ | ♯(x, w) = ♯(y, w)} of words that contain the same
number of xs and ys. This language is not regular.
Some of our proofs rely on semantic equivalence and employ identities from
Kleene algebra [9] that hold for standard regular expressions. Hence, we need to
establish that forkable expressions also form a Kleene algebra.
Definition 4 (Semantic equality and containment).
1. Behaviors r and s are equal, r ≡ s, if L(r, K) = L(s, K), for all K.
2. Behaviors r and s are contained, r ≦ s, if L(r, K) ⊆ L(s, K), for all K.
Theorem 5. The set of forkable expressions with semantic equality and containment is a Kleene algebra.
Each behavior r can be decomposed into a sequential part S(r) and a concurrent part C(r), which are defined by induction on r in Figure 2. The intuition
is that the sequential part of a behavior describes what must happen next, inevitably, whereas the concurrent part describes behavior that happens eventually
and concurrent to the sequential behavior. For example, in case of concatenation r · s, the sequential part must either start with S(r), or must end with S(s).
For Kleene star r∗ it is similar, we simply consider the possible unrolling of the
underlying expression r.
Our decomposition theorem proves that every behavior is semantically equivalent to the union of its concurrent part and its sequential part. Its proof requires
the Kleene identity r∗ ≡ ε + r · r∗ .4
Theorem 6. For all r, r ≡ C(r) + S(r).
The next lemma establishes some algebraic properties of the functions C()
and S() that we need in subsequent proofs.
Lemma 7. For all r: 1. C(C(r)) = C(r) (syntactic equality); 2. C(S(r)) ≡ φ;
3. S(C(r)) ≡ φ; 4. S(S(r)) ≡ S(r).
4

We generally write r = s for syntactic equality of expressions and use other symbols
like r ≡ s for equivalences where some additional reasoning may be involved.

Forkable Regular Expressions

5

Proof. The proof for part 1 is by trivial induction on r. See the online version
for the remaining parts; they are not needed in the rest of this paper.
⊓
⊔
Lemma 8. For all r, ε ∈ L(r) iff ε ≦ C(r).

4

Derivatives

We want to use Brzozowski’s derivative operation [3] to translate behaviors to
automata and to create algorithms for checking language containment and matching. To this end, we extend derivatives to forkable expressions. The derivative of
r w.r.t. some symbol x, written dx (r), yields the new behavior after consumption of the leading symbol x. The derivative operation for behaviors is defined by
structural induction. In addition to the regular operators, the derivative needs
to deal with Fork (r ) expressions and the case of concatenated expressions r · s
requires special attention.
Definition 9 (Derivatives). The derivative of behavior r w.r.t. some symbol
x is defined inductively as follows:
dx (φ) = φ
dx (ε) = φ

dx (y) =

ε if x = y
φ otherwise

dx (r + s) = dx (r) + dx (s)
dx (r · s)
= dx (r) · s + C(r) · dx (s)
dx (r∗ )
= dx (r) · r∗
dx (Fork (r )) = Fork (dx (r ))

We just explain the cases that differ from Brzozowski’s definition. The derivative
of a fork, Fork (r ), is simply pushed down to the underlying expression. The
derivative of r · s consists of two components. The first one, dx (r) · s, is identical
to the standard definition: it computes the derivative of r and continues with s.
The second one covers symbols that may reach s. In a fork-free regular expression,
a symbol in s can only be consumed if r is nullable, i.e. ε ∈ L(r). For forkable
behaviors, a symbol in s can also be consumed if r exhibits concurrent behavior.
Hence, we extract the concurrent behavior C(r) and concatenate it with the
derivative of s. The concurrent behavior generalizes nullability in the sense that
ε ∈ C(r) iff ε ∈ L(r). See Lemma 8.
Next, we verify that the derivative operation is correct in the sense that the
resulting expression dx (r) denotes the left quotient of r by x.
Theorem 10 (Left Quotients). Let r be a behavior and x be a symbol. Then,
we have that L(dx (r)) = x\L(r).
Proof. To obtain a viable inductive hypothesis for the proof, we need to expand
the definition of L(r) = L(r, {ε}) and to generalize the statement to an arbitrary
continuation language K ⊆ Σ ∗ . That is, we set out to prove, by induction on r:
∀r. ∀K. L(dx (r), K) ∪ L(C(r))k(x\K) = x\L(r, K)

(2)

6

Martin Sulzmann and Peter Thiemann

The original statement follows from the generalized hypothesis (2) by setting
K = {ε} (recall that Lk∅ = ∅):
L(dx (r)) = L(dx (r)) ∪ L(C(r))k∅
= L(dx (r), {ε}) ∪ L(C(r))k(x\{ε})
(2)

= x\L(r, {ε}) = x\L(r)

The proof of (2) proceeds by induction on r.

⊓
⊔

Like in the standard regular expression case, we can conclude (based on the
above result) that each behavior can be represented as a sum of its derivatives.
Theorem 11 (Representation).
For any behavior r, we have L(r) = (ε ∈
S
L(r) =⇒ {ε}) ∪ x∈Σ x · L(dx (r)).
Expression (ε ∈ L(r) =⇒ {ε}) denotes {} if ε ∈ L(r), otherwise, {}.
The representation theorem is the basis for solving the word problem with
derivatives. Here, we extend the derivative operation to words as usual by dε (r) =
r and daw (r) = dw (da (r)).
Corollary 12. For a behavior r and w ∈ Σ ∗ , w ∈ L(r) iff ε ∈ L(dw (r)).
This corollary implies decidability of the word problem for forkable expressions:
the derivative is computable and the nullability test ε ∈ L(dw (r)) is a syntactic
test as for standard regular expressions. Full details how to compute all dissimilar
derivatives can be found in the online version.
To construct an automaton from an expression r, Brzozowski repeatedly
takes the derivative with respect to all symbols x ∈ Σ. We call these derivatives
descendants.
Definition 13 (Descendants). A descendant s of a behavior r is either r itself,
a derivative of r, or the derivative of a descendant. We write s ⊏ r, if s is a
direct descendant of r, that is, if s = dx (r), for some x. The “is descendant
of ” relation is the reflexive, transitive closure of the direct descendant relation:
s  r = s ⊏∗ r. The “is a true descendant of ” relation is the transitive closure
of the direct descendant relation: s ≺ r = s ⊏+ r. We define d(r) = {s | s  r}
as the set of descendants of r.
For standard regular expressions, Brzozowski showed that the set of descendants of an expression is finite up to similarity. Two expressions are similar
if they are equal modulo associativity, commutativity, and idempotence. This
result no longer holds in our setting.
x
In the following, we write r −→ s if s = dx (r). Subterms on which the
derivation operation is applied are underlined.

Forkable Regular Expressions

rhs

(Refl, Trans, Sym, Comp) r h r
(Assoc, Comm)
(Idem, Unit)

sht

rht

sht

sht

ths

E[s] h E[t]

r + (s + t) h (r + s) + t
r+r hr

r+s h s+r

r+φhr

φ+r h r

ε·r hr

r·εhr

ε∗ h ε

Fork (ε) h ε

(Empty Language)

φ·r hφ

r·φhφ

φ∗ h ε

Fork (φ) h φ

(Regular Contexts)

E ::= [] | E ∗ | E · s | r · E | E + s | r + E | Fork (E )

(Empty Word)

7

Fig. 3. Rules and axioms for similarity

Example 14. Let r = (Fork (x · y))∗ and take the derivative by x repeatedly.
(Fork (x · y))∗
−→ Fork (y) · r
x
−→ Fork (φ) · r + Fork (y) · Fork (y) · r
x
−→ · · · + Fork (φ) · Fork (y) · r + Fork (y) · (Fork (φ) · r + Fork (y) · Fork (y) · r)
x
−→ . . .
x

Here we omit parentheses (assuming associativity) and apply equivalences such
as C(C(r)) = C(r) (Lemma 7). Clearly, we obtain an increasing sequence of
behaviors of the form Fork (y)·...·Fork (y) ·r. Hence, the set of descendants of r is
infinite even if we consider behaviors equal modulo associativity, commutativity,
and idempotence of alternatives.
This observation is no surprise, given that behaviors may give rise to nonregular languages (cf. Example 3). In general, there is no hope to retain Brzozowski’s result, but it turns out that we can find a well-behavedness condition
for behaviors that is sufficient to retain finiteness of descendants.

5

Well-Behaved Behaviors

In this section, we develop a criterion to guarantee that a forkable expression
only gives rise to a finite set of dissimilar descendants. To start with, we adapt
Brzozowski’s notion of similarity to our setting. In addition to associativity, commutativity, and idempotence we introduce simplification rules that implement
further Kleene identities and that deal with forks.
Definition 15 (Similarity). Behaviors r and s are similar, if r h s is derivable
using the rules and axioms in Figure 3.

8

Martin Sulzmann and Peter Thiemann

The compatibility rule (Comp) uses regular contexts E, which are regular expressions with a single hole []. In the rule, we write E[t] to denote the expression
with the hole replaced by t.
We establish some basic results for similar behaviors, all with straightforward inductive proofs: Similarity implies semantic equivalence, it is complete
for recognizing ε and φ, and it is compatible with derivatives and extraction of
concurrent parts.
Lemma 16. If r h s, then r ≡ s.
Lemma 17. 1. If L(r) = {ε} then r h ε. 2. If L(r) = {} then r h φ.
Lemma 18. 1. If r h r′ , then dx (r) h dx (r′ ), for all x ∈ Σ.
2. If r h r′ , then C(r) h C(r′ ).
Similarity is an equivalence relation. We write [s] = {t | t h s} to denote the
equivalence class of all expressions similar to s. If R is a set of behaviors, we
write R/h = {[r] | r ∈ R} for the set of equivalence classes of elements of R.
To identify the set of well-behaved behaviors, we need to characterize the set
of dissimilar descendants. First, we establish that each composition of derivatives
and applications of C() that finishes in some C(r) may be compressed to the
composition of the derivatives applied to the remaining C(r).
Lemma 19. For a behavior r and symbol x, C(dx (C(r))) = dx (C(r)), syntactically.
The above result makes it easier to classify the forms of dissimilar descendants.
The Kleene star case is clearly highly relevant. The following statement confirms the observation in Example 14.
Lemma 20. For w ∈ Σ + , dw (r∗ ) h dw (r) · r∗ + t where t is a possibly empty
sum of terms of the form s1 · . . . · sn · r′ · r∗ where r′ ≺ r, n ≥ 1, and for each
si , si  C(s) for some descendant s ≺ r.
Proof. Induction on w.
Case x: dx (r∗ ) = dx (r) · r∗ h dx (r) · r∗ + φ.
Case wx: dwx (r∗ ) = dx (dw (r∗ )). By induction for w, dw (r∗ ) h dw (r) · r∗ + t
where each summand of t has the form s1 · . . . · sn · r′ · r∗ . First, observe that
dx (dw (r) · r∗ + t) = dwx (r) · r∗ + C(dw (r)) · dx (r) · r∗ + dx (t). We show by auxiliary
induction on n that the derivative of t is a sum of terms of the desired form.
Case 0:
dx (r′ · r∗ ) = dx (r′ ) · r∗ + C(r′ ) · dx (r∗ )
= dx (r′ ) · r∗ + C(r′ ) · dx (r) · r∗
which has the desired format.
Case n > 0: dx (s1 · . . . · sn · r′ · r∗ )
= dx (s1 ) · s2 · . . . · sn · r′ · r∗ + C(s1 ) · dx (s2 · . . . · sn · r′ · r∗ )
The first summand has the desired form. By induction (on n), each summand
of dx (s2 · . . . · sn · r′ · r∗ ) has the desired form and multiplying with C(s1 ) from
the left retains this form: By Lemma 19, C(s1 ) is still a descendant of C(s) for
some descendant s of r.
⊓
⊔

Forkable Regular Expressions

9

To obtain finiteness it appears that a sufficient condition is to ensure that
the subterms si are trivial (either ε or φ). Via similarity, the explosion of terms
derived from Kleene star can then be avoided. To verify this claim we also
characterize the descendants of concatenated behaviors.
Lemma 21. For w ∈ Σ + , dw (r · s) has the form
dw (r · s) h dw (r) · s + C(r) · dw (s) + t
where t is a sum of terms of the form r′ · s′ where s′ is a descendant of s and r′
is a descendant of C(r′′ ) and r′′ is a descendant of r.
Proof. By induction on w.
Case x: Immediate from the definition of dx (r · s) with t = φ.
Case wx: By induction
dx (dw (r · s)) h dx (dw (r) · s + C(r) · dw (s) + t)
h dwx (r) · s + C(dw (r)) · dx (s)
+ dx (C(r)) · dw (s) + C(r) · dwx (s)
+ dx (t)
The underlined summands have the expected forms. The newly created summands have a form corresponding to r′ · s′ . It remains to observe that the derivative of a summand in t has the expected form by Lemma 19 and Lemma 7.
dx (r′ · s′ ) = dx (r′ ) · s′ + C(r′ ) · dx (s′ )

⊓
⊔

Definition 22 (Well-behaved Behaviors). A behavior t is well-behaved if
all subterms of the form r∗ have the property that C(dw (r)) ≦ ε, for all w ∈ Σ ∗ .
The intuition for this definition is simple: Well-behaved behaviors do not fork
processes with non-trivial communication behavior in a loop (i.e., under a star).
Indeed, we have a simple decidable sufficient condition for well-behavedness.
Lemma 23. If r h r′ and r′ is fork-free, then C(dw (r)) ≦ ε, for all w ∈ Σ ∗ .
Thus, a behavior is also well-behaved if, for all subterms of the form r∗ , r is
similar to a fork-free expression.
Recall that d(r) is the set of all descendants of r and d(r)/(h) denotes the set
of equivalence classes of descendants of r. If we pick a representative from each of
these equivalence classes, we obtain the dissimilar descendants of r. In a practical
implementation, we may want to compute the canonical representative of each
equivalence class. See the online version for further details. For the purpose of
this paper, an arbitrary representative is sufficient.
Definition 24 (Dissimilar Descendants). We define the set of dissimilar
descendants of r, dh (r), as a complete set of arbitrarily chosen representative
behaviors for the equivalence classes d(r)/(h).

10

Martin Sulzmann and Peter Thiemann

We extend the function C() on behaviors pointwise to sets of behaviors and
relation h to sets of behaviors by
R h S iff (∀r ∈ R.∃s ∈ S.r h s) ∧ (∀s ∈ S.∃r ∈ R.r h s)
Lemma 25. For any behavior r, C(dh (C(dh (r)))) h dh (C(dh (r))).
⊓
⊔

Proof. Follows from Lemma 19 and Lemma 18.
Lemma 26. For any behavior r, d(r) h dh (r).

Proof. We need to verify that for each t1 ∈ d(r) there exists t2 ∈ dh (r) such
that t1 h t2 . We prove this property by induction on the number of derivative
steps.
Case w = ε: Then, t1 = r. Clearly, there exists t2 ∈ dh (r) such that t1 h t2 .
Case w = x · w′ : Then, t1 = dx (dw′ (r)). By the IH, dw′ (r) h t2 where
t2 ∈ dh (r). By Lemma 18, t1 ≡ dx (t2 ) where dx (t2 ) h t3 for some t3 ∈ dh (r).
Thus, we are done.
⊓
⊔
The next result can be verified via similar reasoning.
Lemma 27. For any behavior r, d(dh (r)) h dh (r).
Theorem 28 (Finiteness of Well-Behaved Dissimilar Descendants).
Let t be a well-behaved behavior. Then, ♯dh (t) < ∞.
Proof. We need to generalize the statement to obtain the result: If t is wellbehaved then ♯dit < ∞ for all i ≥ 0 where d0t = dh (t) and dn+1
= dh (C(dnt )).
t
n+1
n
Based on Lemmas 27 and 25 we find that dt
= dt for n ≥ 1. That is, in
the induction step it is sufficient to establish that d0t and d1t are finite.
We proceed by induction on t. For brevity, we only consider the case of
concatenation.
Case r · s: By the IH, dir and dis are finite for any i ≥ 0. We first show that d0r·s
is finite.
1. By Lemma 21, the elements of d(r · s) are drawn from the set
X
d(r) · s + C(r) · d(s) +
d(C(d(r))) · d(s)

2. By Lemma 26 the above is similar to

dh (r) · s + C(r) · dh (s) +

X

dh (C(dh (r))) · dh (s)

3. Immediately, we can conclude that d0r·s is finite.
Next, we consider d1r·s .
1. From above, the (dissimilar) descendants of r · s are drawn from
X
d(C(d(r))) · dh (s)
d(r) · s + C(r) · d(s) +
|
{z
}
| {z } | {z }
t1

t2

t3

For each ti we will show that d1ti is finite and thus follows the desired result.

Forkable Regular Expressions

11

2. By Lemma 21, descendants of C(t1 ) are of the form
X
d(C(d(r))) · C(s) + C(d(r)) · d(C(s)) +
d(C(d(C(d(r))))) · d(C(s))

3. As we know by the IH, dir and dis are finite for any i ≥ 0. Hence, via similar
reasoning as above we can conclude that the above is similar to expressions
of the form
P
d1r · C(s) + C(d0r ) · d1s + d2r · d1s

As all sub-components are finite, we conclude that d1t1 is finite.
4. We consider the descendants of C(t2 ) which are of the following form
P
d(C(r)) · C(d(s)) + C(r) · d(C(d(s))) + d(C(d(C(r)))) · d(C(d(s)))

5. The above is similar to

d1r · C(d0s ) + C(r) · d1r +

P

d2r · d1s

Thus, we find that d1t2 is finite.
6. Finally, we observe that shape of descendants of C(t3 )
d(C(d(C(d(r)))))
· C(d(s)) + C(d(C(d(r)))) · d(C(d(s)))
P
+ d(C(d(C(d(C(d(r))))))) · d(C(d(s)))

7. The above is similar to

d2r · C(d0s ) + C(d1r ) · d1s +

P

d3r · d1s

8. Then, d1t3 is finite which concludes the proof for this case.
⊓
⊔
The result no longer holds if we replace the assumption C(dw (r)) ≦ ε, for
w ∈ Σ ∗ by a simpler assumption like C(r) ≦ ε. For example, consider the
behavior (x · Fork (y))∗ where C(x · Fork (y)) = φ ≦ ε. However, the set of
dissimilar descendants of (x · Fork (y))∗ is infinite as shown by the calculation
(x · Fork (y))∗
→ (ε · Fork (y)) · (x · Fork (y))∗
h Fork (y) · (x · Fork (y))∗
x
→ Fork (φ) · (x · Fork (y))∗ + Fork (y) · Fork (y) · (x · Fork (y))∗
h Fork (y) · Fork (y) · (x · Fork (y))∗
...
x

The example also shows that the assumption C(dw (r)) ≦ ε, for w ∈ Σ ∗ is
necessary and cannot be weakened to words w of a fixed length.
As an example, consider the behavior t = (x1 · ... · xn · xn+1 Fork (y))∗ where
for all w ∈ Σ ∗ with length less or equal n we find that C(dw (x1 · ... · xn ·
xn+1 Fork (y))) ≦ ε. Via a similar calculation as above, we can show that the
set of dissimilar descendants of t is infinite.

12

6

Martin Sulzmann and Peter Thiemann

Related Work

Shuffle expressions are regular expressions with operators for shuffle and shuffle closure. Shaw [13] proposes to describe the behavior of software using flow
expressions, which extend shuffle expressions with further operators. Gischer [6]
shows that shuffle expression generate context-sensitive languages and proposes
a connection to Petri net languages.
The latter connection is made precise by Garg and Ragunath [4], who study
concurrent regular expressions (CRE), which are shuffle expressions extended
with synchronous composition. They show that the class of CRE languages is
equal to the class of Petri net languages. The proof requires the presence of synchronous composition. Forkable expressions do not support synchronous composition, but they are equivalent to unit expressions, which are also defined by
Garg and Ragunath and shown to be strictly less powerful than CREs.
Warmuth and Haussler [14] present more refined complexity results for the
languages generated by shuffle expressions. Jedrzejowicz [8] shows that the nesting of iterated closure operators matters.

Acknowledgments
We thank the reviewers for their comments.

References
1. Amtoft, T., Nielson, F., Nielson, H.R.: Type and behaviour reconstruction for
higher-order concurrent programs. Journal of Functional Programming 7(3), 321–
347 (May 1997)
2. Amtoft, T., Nielson, H.R., Nielson, F.: Behavior analysis for validating communication patterns. STTT 2(1), 13–28 (1998)
3. Brzozowski, J.A.: Derivatives of regular expressions. J. ACM 11(4), 481–494 (1964)
4. Garg, V.K., Ragunath, M.T.: Concurrent regular expressions and their relationship
to Petri nets. Theor. Comput. Sci. 96(2), 285–304 (Apr 1992)
5. Ginsburg, S.: The Mathematical Theory of Context-Free Languages. McGraw-Hill,
Inc., New York, NY, USA (1966)
6. Gischer, J.: Shuffle languages, Petri nets, and context-sensitive grammars. Commun. ACM 24(9), 597–605 (Sep 1981)
7. Jantzen, M.: Extending regular expressions with iterated shuffle. Theor. Comput.
Sci. 38, 223–247 (1985)
8. Jedrzejowicz, J.: Nesting of shuffle closure is important. Inf. Process. Lett. 25(6),
363–368 (1987)
9. Kozen, D.: On Kleene algebras and closed semirings. In: Proceedings of the Mathematical Foundations of Computer Science 1990. pp. 26–47. MFCS ’90, SpringerVerlag, London, UK, UK (1990)
10. Leiß, H.: Towards Kleene algebra with recursion. In: Proc. of CSL’91. LNCS, vol.
626, pp. 242–256. Springer (1992)
11. Nielson, H.R., Amtoft, T., Nielson, F.: Behaviour analysis and safety conditions:
A case study in CML. In: FASE. pp. 255–269 (1998)

Forkable Regular Expressions

13

12. Nielson, H.R., Nielson, F.: Higher-order concurrent programs with finite communication topology. In: Proc. of POPL’94. pp. 84–97. ACM Press (Jan 1994)
13. Shaw, A.C.: Software descriptions with flow expressions. IEEE Trans. Software
Eng. 4(3), 242–254 (1978)
14. Warmuth, M.K., Haussler, D.: On the complexity of iterated shuffle. J. Comput.
Syst. Sci. 28(3), 345–358 (1984)

14

Martin Sulzmann and Peter Thiemann

A

Supplementary Material

A.1

Well-definedness of L

For each r, the mapping K 7→ L(r, K) is a monotone mapping in ℘(Σ ∗ ) → ℘(Σ ∗ ).
The proof is by induction on r.
Case φ: K 7→ L(φ, K) = ∅ is monotone.
Case ε: K 7→ L(ε, K) = K is monotone.
Case x: K 7→ L(x, K) = x · K is monotone.
Case r + s: K 7→ L(r + s, K) = L(r, K) ∪ L(s, K) is monotone by induction.
Case r · s: K 7→ L(r · s, K) = L(r, L(s, K)) is monotone by induction.
Case r∗ : K 7→ L(r∗ , K) = µX.L(r, X) ∪ K. By induction, f = X 7→ L(r, X)
is monotone. Hence, gK = X 7→ L(r, X)∪K is monotone, for all K. Furthermore,
f ≤ gK and gK ≤ gL in the pointwise ordering of set-valued functions, whenever
K ⊆ L. It follows that µgK ≤ µgL , which proves that K 7→ L(r∗ , K) is monotone.
Case Fork (r ): K 7→ L(Fork (r ), K) = L(r)kK. Immediate by induction and
because k is monotone.
A.2

Proof of Theorem 6

Proof. By induction on r.
Case φ, ε, x, Fork (r ): immediate.
Case r + s: immediate by induction.
Case r · s: C(r · s) + S(r · s) = C(r) · C(s) + C(r) · S(s) + S(r) · s
≡ C(r) · (C(s) + S(s)) + S(r) · s
IH

≡ C(r) · s + S(r) · s
≡ (C(r) + S(r)) · s
IH

≡ r·s

Case r∗ : C(r∗ ) + S(r∗ ) = C(r)∗ + C(r)∗ · S(r) · r∗
IH

≡ C(r)∗ + C(r)∗ · S(r) · (C(r) + S(r))∗
≡ (C(r) + S(r))∗
IH

≡ r∗
⊓
⊔

A.3

Proof of Theorem 2

Proof. Induction on r where we generalize the statement to L(r, K) = JrK · K,
for all K ⊆ Σ ∗ , and use Arden’s lemma for the case r∗ . The theorem follows by
setting K = {ε}.
Cases φ, ε, x: immediate.
Case r + s: immediate by IH.

Forkable Regular Expressions

15

Case r · s: L(r · s, K) = L(r, L(s, K)) = JrK · (JsK · K) = Jr · sK · K.
Case r∗ :
L(r∗ , K)
= (by definition)
µX.L(r, X) ∪ K
= (by IH, X must be in Σ ∗ )
= µX.JrK · X ∪ K
(by Arden’s lemma)
= Jr∗ K · K
⊓
⊔
A.4

Proof of Theorem 5

Proof. Following [9] a Kleene algebra satisfies the axioms of an idempotent semiring and the following axioms:
1.
2.
3.
4.

ε + r · r∗ ≦ r∗
ε + r∗ · r ≦ r∗
If r · s ≦ s then r∗ · s ≦ s
If s · r ≦ s then s · r∗ ≦ s

It is straightforward to verify that behaviors form on idempotent semiring.
Axioms (1) and (2) follow by calculation from the semantics.
Consider (3). Suppose r · s ≦ s. We will show that by induction for any n we
have that rn ·s ≦ s where r0 = ε and rn+1 = r·rn . Case n = 0 holds immediately.
For case n + 1 we perform the following calculations.
rn+1 · s
= r · rn · s
(IH)
≦r·s
≦s
Thus, we find that r∗ · s ≦ s. Case (4) can be verified similarly.
A.5

⊓
⊔

Proof of Lemma 7

Proof. 1. Trivial induction.
2. Induction on r. The cases for φ, ε, l, r + s, Fork (r ) are trivial or immediate
by the inductive hypothesis.
C(S(r · s)) = C(S(r) · s + C(r) · S(s))
= C(S(r) · s) + C(C(r) · S(s))
= C(S(r)) · C(s) + C(C(r)) · C(S(s))
≡ φ · C(s) + C(r) · φ
≡φ

16

Martin Sulzmann and Peter Thiemann

C(S(r∗ )) = C(C(r)∗ · S(r) · r∗ )
= C(C(r)∗ ) · C(S(r)) · C(r∗ )
≡ C(C(r))∗ · φ · C(r)∗
≡φ
3. Induction on r. The cases for φ, ε, l, r + s, Fork (r ) are trivial or immediate
by inductive hypothesis.
S(C(r · s)) = S(C(r) · C(s))
= S(C(r)) · C(s) + C(C(r)) · S(C(s))
≡ φ · C(s) + C(r) · φ
≡φ
S(C(r∗ )) = S(C(r)∗ )
= C(C(r))∗ · S(C(r)) · C(r)∗
≡ C(r)∗ · φ · C(r)∗
≡φ
4. Induction on r. The cases for φ, ε, l, r + s, Fork (r ) are trivial or immediate
by inductive hypothesis.
S(S(r · s)) = S(S(r) · s + C(r) · S(s))
= S(S(r) · s) + S(C(r) · S(s))
= S(S(r)) · s + C(S(r)) · S(s) + S(C(r)) · S(s) + C(C(r)) · S(S(s))
{by 1., 2., 3., and the inductive hypothesis}
≡ S(r) · s + C(r) · S(s)
S(S(r∗ )) = S(C(r)∗ · S(r) · r∗ )
= S(C(r)∗ ) · S(r) · r∗ + C(C(r)∗ ) · S(S(r) · r∗ )
∗

= S(C(r)∗ ) · S(r) · r∗ + C(r) · (S(S(r)) · r∗ + C(S(r)) · S(r∗ ))
∗
= S(C(r)∗ ) · S(r) · r∗ + C(r) · (S(r) · r∗ + φ · S(r∗ ))
∗

= S(C(r)∗ ) · S(r) · r∗ + C(r) · (S(r) · r∗ )
∗
= C(C(r))∗ · S(C(r)) · C(r)∗ · S(r) · r∗ + C(r) · (S(r) · r∗ )
∗

∗

≡ C(r) · φ · C(r)∗ · S(r) · r∗ + C(r) · (S(r) · r∗ )
≡ C(r)∗ · (S(r) · r∗ )
⊓
⊔
A.6

Proof of Lemma 8

Proof. If ε ≦ C(r) and by decomposition r ≡ S(r) + C(r) we find that ε ∈ L(r).

Forkable Regular Expressions

17

The other direction requires induction on r. For brevity, we only consider
some cases.
ε ∈ L(r · s)
=⇒ ε ∈ L(r) ∧ ε ∈ L(s)
IH
=⇒ ε ≦ C(r) ∧ ε ≦ C(s)
=⇒ ε ≦ C(r) · C(s) = C(r · s)
For Kleene star, by definition C(r∗ ) = C(r)∗ and ε ≦ C(r)∗ is a derived
property in a Kleene algebra. Thus, ε ≦ C(r∗ ) follows immediately.
⊓
⊔
A.7

Auxiliary Statements

Lemma 29. Let r, s be behaviors. Then L(C(r))kL(C(s)) = L(C(r · s)).
Proof.
L(C(r))kL(C(s)) = L(C(r), L(C(s)))
= L(C(r), L(C(s), {ε}))
= L(C(r · s), {ε})
= L(C(r · s))
⊓
⊔
Lemma 30. Let r be a behavior and K a language. Then L(C(r), K) = L(C(r))kK
Proof. Induction on f .
Case φ.
Trivial as C(φ) = φ, L(φ, K) = ∅ = ∅kK.
Case ε.
C(ε) = ε. L(ε, K) = K = {ε}kK.
Case x.
C(x) = φ. L(φ, K) = ∅ = ∅kK.
Case r + s.
L(C(r + s), K) = L(C(r), K) ∪ L(C(s), K)
= L(C(r))kK ∪ L(C(s))kK
= L(C(r + s))kK

Case r · s. (requires Lemma 29)
L(C(r · s), K) = L(C(r) · C(s), K)
= L(C(r), L(C(s), K))
= L(C(r))kL(C(s))kK
= L(C(r · s))kK

18

Martin Sulzmann and Peter Thiemann

Case r∗ .
L(C(r∗ ), K) = L(C(r)∗ , K)
= µX.(L(C(r), X) ∪ K)
{IH}
= µX.(L(C(r))kX ∪ K)
= L(C(r))♯ kK
= (µX.L(C(r))kX ∪ {ε})kK
{IH}
= (µX.L(C(r), X) ∪ {ε})kK
= L(C(r)∗ , {ε})kK
= L(C(r∗ ))kK

Case Fork (r ).
L(C(Fork (r )), K) = L(Fork (r ), K)
= L(r)kK
= L(r)k{ε}kK
= L(Fork (r ), {ε})kK
= L(C(Fork (r )))kK

⊓
⊔
A.8

Remaining cases of Theorem 10

Proof. Case Fork (r ).
L(dx (Fork (r )), K) ∪ L(C(Fork (r )))kx\K
= L(Fork (dx (r )), K) ∪ L(Fork (r ))kx\K
= L(dx (r))kK ∪ L(r)kx\K
{IH}
= x\L(r)kK ∪ L(r)kx\K
= x\(L(r)kK)
= x\(L(Fork (r ), K))
Case φ. C(φ) = φ.
L(dx (φ), K) = L(φ, K) = ∅ = x\L(φ, K)
Case ε. C(ε) = ε.
L(dx (ε), K) ∪ L(C(ε))k(x\K) = L(φ, K) ∪ x\K = x\K = x\L(ε, K)

Forkable Regular Expressions

Case x. C(x) = φ.
L(dx (x), K) = L(ε, K) = K = x\L(x, K)
Case y 6= x.
L(dx (y), K) = L(φ, K) = ∅ = x\L(y, K)
Case r + s. C(r + s) = C(r) + C(s).
L(dx (r + x), K) ∪ L(C(r + s))k(x\K)
= L(dx (r), K) ∪ L(C(r))k(x\K) ∪ L(dx (s), K) ∪ L(C(s))k(x\K)
{IH}
= x\L(r, K) ∪ x\L(s, K)
= x\L(r + s, K)
Case r · s. C(r · s) = C(r) · C(s).
L(dx (r · s), K) ∪ L(C(r · s))k(x\K)
= L(dx (r) · s, K) ∪ L(C(r) · dx (s), K) ∪ L(C(s))kL(C(s))k(x\K)
= L(dx (r), L(s, K)) ∪ L(C(r), L(dx (s), K)) ∪ L(C(r))kL(C(s))k(x\K)
= L(dx (r), L(s, K)) ∪ L(C(r))kL(dx (s), K) ∪ L(C(r))kL(C(s))k(x\K)

= L(dx (r), L(s, K)) ∪ L(C(r))k L(dx (s), K) ∪ L(C(s))k(x\K)
{IH}
= L(dx (r), L(s, K)) ∪ L(C(r))k(x\L(s, K))
{IH}
= x\L(r, L(s, K))
= x\L(r · s, K)
Case r∗ .
We verify for all n ≤ 0 that
x\L(rn , K) = L(dx (rn ), K) ∪ L(C(rn ))k(x\K)
where r0 = ε and rn+1 = r · rn .
Case n = 0: Straightforward
Case n =⇒ n + 1:
L(dx (rn+1 ), K) ∪ L(C(rn+1 ))k(x\K)
= L(dx (r) · rn + C(r) · dx (rn ), K) ∪ L(C(rn+1 ))k(x\K)
= L(dx (r), L(rn , K)) ∪ L(C(r), L(dx (rn ), K)) ∪ L(C(rn+1 ))k(x\K)
= L(dx (r), L(rn , K)) ∪ L(C(r), L(dx (rn ), K)) ∪ L(C(r), L(C(rn )))k(x\K)
(Lemma 30)
= L(dx (r), L(rn , K)) ∪ L(C(r))kL(dx (rn ), K) ∪ L(C(r)kL(C(rn ))k(x\K)
= L(dx (r), L(rn , K)) ∪ L(C(r))k(L(dx (rn ), K) ∪ L(C(rn ))k(x\K))
(IH)
= L(dx (r), L(rn , K)) ∪ L(C(r))k(x\(L(rn , K)))
(IH)
= x\L(r, L(rn , K))
= x\L(rn+1 , K)

19

20

Martin Sulzmann and Peter Thiemann

Then, the actual statement
l\L(r∗ , K) = L(dx (r∗ ), K) ∪ L(C(r∗ ))k(x\K)
follows from the fact that
(x\L(rn , K)) ≤ (x\L(b∗ , K))
L(dx (rn ), K) ∪ L(C(rn ))k(x\K) ≤ L(dx (r∗ ), K) ∪ L(C(r∗ ))k(x\K)
and by showing that for all finite words w ∈ Σ ∗ we have that w ∈ (x\L(r∗ , K))
iff w ∈ L(dx (r∗ ), K) ∪ L(C(r∗ ))k(x\K).
If w ∈ (x\L(r∗ , K)) then w ∈ (x\L(bn , K)) for some n ≤ 0. From above, we
conclude that w ∈ L(dx (rn ), K)∪L(C(rn ))k(x\K) ≤ L(dx (r∗ ), K)∪L(C(r∗ ))k(x\K).
The argument is similar for the other direction.
⊓
⊔
A.9

Proof of Lemma 17

Proof. By induction on r. Consider L(r) = {ε}.
Cases x and φ do not apply. Case ε is straightforward.
Case r + s: L(r + s) = {ε} implies that L(r) ⊆ {ε} and L(s) ⊆ {ε}. There
are four subcases to consider. Suppose L(r) = {ε} and L(s) = {}. By IH, r h ε
and either s h φ. Then, r + s h ε, by (Unit). Other cases are similar.
Case r·s: L(r·s) = L(r)·L(s) = {ε} implies that L(r) = {ε} and L(s) = {ε}.
By IH, r h ε and s h ε. Hence, r · s h ε, by (Empty Word).
Case r∗ : L(r∗ ) = {ε} implies that L(r) = {ε}. By IH, r h ε from which we
can conclude that r∗ h ε.
Case Fork (r ): Similar to the above.
Consider L(r) = {}. Cases x, ε and r∗ do not apply. Case φ is straightforward.
Case r·s: L(r·s) = {} implies that L(r) = {}∨L(s) = {}. Suppose L(r) = {}.
By IH, r h φ and therefore r · s h φ. The other case is similar.
Case r + s: Similar to the above.
Case Fork (r ): L(Fork (r )) = {} implies L(r) = {}. Via similar arguments as
above we find that Fork (r ) h φ.
⊓
⊔
A.10

Proof of Lemma 19

Proof. Case r = φ, ε, x: trivial as C(r) = φ.
Case r + s: immediate from the IH.
Case r · s:
dx (C(r · r))
= dx (C(r) · C(x))
= dx (C(r)) · C(s) + C(C(r)) · dx (C(x))
{IH, Lemma 7 part 1}
= C(dx (C(r))) · C(C(s)) + C(C(C(r))) · C(dx (C(s)))
= C(dx (C(r · s)))

Forkable Regular Expressions

21

Case r∗ :
dl (C(r∗ ))
= dx (C(r)∗ )
= dx (C(r)) · C(r)∗
{IH, Lemma 7 part 1}
= C(dx (C(r))) · C(C(r))∗
= C(dx (C(r∗ )))
Case Fork (r ):
dx (C(Fork (r )))
= dx (Fork (r ))
= Fork (dx (r ))
= C(Fork (dx (r )))
= C(dx (C(Fork (r ))))
⊓
⊔
A.11

Proof of Theorem 28

Proof. We need to generalize the statement to obtain the result: If t is wellbehaved then ♯dit < ∞ for all i ≥ 0 where d0t = dh (t) and dn+1
= dh (C(dnt )).
t
n+1
n
Based on Lemmas 27 and 25 we find that dt
= dt for n ≥ 1. That is, in the
induction step it is sufficient to establish that d0t and d1t are finite. We proceed
by induction on t.
Cases ε, x, φ: Straightforward.
Case r + s: By the IH, dir , dis are finite for any i ≥ 0. We know that d(r + s) =
d(r) + d(s). The above can be represented by dh (r) + dh (s). Immediately, we
find d0r+s is finite.
Via similar reasoning, we can show that the d(C(d(r +s))) can be represented
by dh (C(dh (r))) + dh (C(dh (s))). Hence, d1r+s which concludes the proof for this
case.
Case Fork (r ) : By the IH, dir are finite for any i ≥ 0.
From d(Fork (r )) = Fork (d(r )) and the above we can conclude that d0Fork (r )
is finite.
To establish d1Fork (r ) is finite, we apply the following reasoning.
dh (C(dh (Fork (r ))))
h dh (C(Fork (dh (r ))))
h dh (Fork (dh (r )))
h Fork (dh (dh (r )))
h Fork (dh (r ))
The set dh (r) is finite. Hence, d1Fork (r ) is finite.
Case r∗ : By the IH, dir are finite for any i ≥ 0. We show that d0r∗ is finite.

22

Martin Sulzmann and Peter Thiemann

1. By Lemma 20, descendants of r∗ are of the form
s1 · ... · sn · d(r) · r∗
where si ∈ d(C(dw (r))) for some w ∈ Σ + .
2. From Lemma 17 and the assumption that all subterms of the form r∗ have
the property that C(dw (r)) ≤ ε, for w ∈ Σ ∗ , we conclude that the above is
either similar to φ or d0r · r∗ .
3. Hence, d0r∗ is finite.
Next, we show that d1r∗ is finite.
1. We observe the possible forms of (dissimilar) descendants of r∗ .
2. For case φ we immediately find that dh (C(φ)) is finite.
3. For case d0r · r∗ , we consider the possible descendants of C(d0r · r∗ ) = C(d0r ) ·
C(r∗ ).
4. By Lemma 21, the shape of such terms is of the form
P
d(C(d0r )) · C(r∗ ) + C(d0r ) · d(C(r∗ )) + d(C(d(C(d0r )))) · d(C(r∗ ))

5. By Lemma 26 the above is similar to

d1r · C(r∗ ) + C(d0r ) · d(C(r∗ )) +

P

d2r · d(C(r∗ ))

6. We know that dir are finite. What remains is to show that dh (C(r∗ )) is finite.
7. Via similar reasoning as above we can argue that the descendants of C(r∗ ) =
C(r)∗ are of the form
t1 · ... · tm · d(C(r)) · C(r)∗
where ti ∈ d(C(dw (C(r)))) for some w ∈ Σ + .
8. Each ti is either φ or ε based on the following approximation. First, we
find that C(dw (C(r))) ≤ C(dw (C(r) + S(r))) = C(dw (r)). As we know that
C(dw (r)) ≤ ε for w ∈ Σ + , we can conclude that ti ≤ ε.
9. Hence, descendants of C(r)∗ are either similar to φ or terms of the form
d(C(r)) · C(r)∗ .
10. As we know d1r is finite and subsumes d(C(r)) we can conclude that dh (C(r∗ ))
is finite. Thus, we are done.
Case r · s: By the IH, dir and dis are finite for any i ≥ 0. We show that d0r·s is
finite.
1. By Lemma 21, each derivative dw (r · s) has the form
X
d(r) · s + C(r) · d(s) +
d(C(d(r))) · d(s)

2. By Lemma 26 the above is similar to

dh (r) · s + C(r) · dh (s) +

X

dh (C(dh (r))) · dh (s)

Forkable Regular Expressions

23

3. Immediately, we can conclude that d0r·s is finite.
Next, we consider d1r·s .
1. From above, the form of (dissimilar) descendants of r · s is
X
d(C(d(r))) · dh (s)
d(r) · s + C(r) · d(s) +
|
| {z } | {z }
{z
}
t1

t2

t3

For each ti we will show that d1ti is finite and thus follows the desired result.
2. By Lemma 21, descendants of C(t1 ) are of the form
X
d(C(d(r))) · C(s) + C(d(r)) · d(C(s)) +
d(C(d(C(d(r))))) · d(C(s))
3. As we know by the IH, dir and dis are finite for any i ≥ 0. Hence, via similar
reasoning as above we can conclude that the above is similar to expressions
of the form
P
d1r · C(s) + C(d0r ) · d1s + d2r · d1s
As all sub-components are finite, we can immediately conclude that d1t1 is
finite.
4. We consider the descendants of C(t2 ) which are of the following form
P
d(C(r)) · C(d(s)) + C(r) · d(C(d(s))) + d(C(d(C(r)))) · d(C(d(s)))

5. The above is similar to

d1r · C(d0s ) + C(r) · d1r +

P

d2r · d1s

Thus, we find that d1t2 is finite.
6. Finally, we observe that shape of descendants of C(t3 )
d(C(d(C(d(r)))))
· C(d(s)) + C(d(C(d(r)))) · d(C(d(s)))
P
+ d(C(d(C(d(C(d(r))))))) · d(C(d(s)))

7. The above is similar to

d2r · C(d0s ) + C(d1r ) · d1s +

P

d3r · d1s

8. Then, d1t3 is finite which concludes the proof for this case.
⊓
⊔
A.12

Similarity is decidable

We turn similarity rules from Figure 3 into term rewriting rules. Roughly, the
right-hand side of h is replaced by the left-hand side. See Figure 4. Rules (EW)
and (EL) are straightforward. Alternatives are normalized into right-associative
normal form. See rule (Assoc2). To easily enforce idempotence (rule (Idemp)) we
sort terms in a sum according to their term size. See rules (Comm) and (Assoc1).
We assume that |r| denotes the size of r. We write r < s iff |r| < |s|. Finally,
rule (U) removes φ in a sum. We assume that the term size of behaviors is such
that |φ| ≤ |r| for any behavior r. Thus, the single rule (U) is sufficient.

24

Martin Sulzmann and Peter Thiemann

(Comm)

(Assoc1)

s<r
r+s→s+r
s<r

r + (s + t) → s + (r + t)

(Assoc2) (r + s) + t → r + (s + t)
(Idemp) r + r → r
ε·r →r

φ·r →φ

r·ε→r
(U) φ + r → r (EW)

r·φ →φ
(EL)

ε∗ → ε

φ∗ → ε

Fork (ε) → ε

Fork (φ) → φ

Fig. 4. Normalization

Lemma 31. The rewrite system in Figure 4 is terminating and confluent.
Proof. Termination is due to the fact that the he size of the left-hand side term
becomes smaller than the size of the right-hand side term. The exceptions are
rules (Comm) and (Assoc1-2). However, it is clear that there can only be a finite
number of applications of these terms. In case of (Comm) and (Assoc1) we shift
smaller terms to the ’left’. In case of (Assoc2), the left part of an alternative
becomes smaller.
We show confluence by establishing local confluence. That is, all critical pairs
are confluence. Given that the term rewrite system is terminating, we obtain
confluence by application of Newman’s Lemma.
It is a straightforward exercise to verify that all critical pairs are joinable.
For example, note the presence of rule (Assoc2). Thus, the critical pair among
(Comm) and (Assoc2) becomes joinable.
⊓
⊔
Based on the above result we can build canonical normal forms by exhaustive
rule application until we reach a fixpoint. We write r →∗ t to denote that t is term
on which no further rewrite rules are applicable. We refer to t as the canonical
form of r. It is clear that r h t.
Lemma 32. Let r and s be behaviors such that r h s. Then, we find r ֌∗ t1
and s ֌∗ t2 for some t1 and t2 where t1 and t2 are syntactically equivalent.
Proof. The result follows by induction over the derivation r h s. For brevity, we
only show some cases.
Suppose
s1 h s2
(Compatibility)
r[s1 ] h r[s2 ]

Forkable Regular Expressions

25

By the IH, we find s1 ֌∗ t, s2 ֌∗ t for some t. Hence, r[s1 ] ֌n r[t] and
r[s2 ] ֌m r[t]. That is, in finite number of rewrite steps (either n or m), we
rewrite r[s1 ] into r[t] and r[s2 ] into r[t]. As every term, e.g. r[t], must have a
canonical normal form, the result follows by combing the above rewrite steps
and from the fact that the rewrite system is confluent.
Suppose in the last derivation step, we apply
(Associativity) r1 + (r2 + r3 ) h (r1 + r2 ) + r3
Suppose r1 + (r2 + r3 ) ֌∗ t. Then, (r1 + r2 ) + r3 ֌Assoc2 r1 + (r2 + r3 ) and
by confluence we know that r1 + (r2 + r3 ) and (r1 + r2 ) + r3 share the same
canonical normal form.
⊓
⊔
Based on the above results we obtain a decidable method to test for similarity
for some behaviors r and s. We build the canonical normal forms of r and s. If
the canonical normal forms are syntactically equivalent, we find that that r and
s are similar. Otherwise, r and s are dissimilar.
A.13

Normal form

Define smart constructors for expressions that implement the similarity rules.
We assume a total ordering < on forkable expressions. We further assume that
arguments of constructors are already in normal form. That means, that the
monomials in every sum are sorted in ascending order and that monomials are
bracketed to the right.

r





s



′
′′


r ⊕ (r ⊕ s)
r ⊕ s = (r ⊕ s′ ) + s′′



s + (r ⊕ s′′ )




r + s



s+r


φ





r





s

r ⊙ s = r′ ⊙ (r′′ ⊙ s)


s · r





Fork (s ′ ) · (r ⊙ s′′ )



r·s
(
r⊛ =

r
r
r
r
r
r
r

=s∨s = φ
=φ
= r′ + r′′
6= r′ + r′′ , s = s′ + s′′ , r < min s′′
6= r′ + r′′ , s = s′ + s′′ , r ≥ min s′′
6= r′ + r′′ , s 6= s′ + s′′ , r < s
6= r′ + r′′ , s 6= s′ + s′′ , r > s
r =φ∨s=φ
s=ε
r=ε
r = r′ · r′′
r = Fork (r ′ ), s = Fork (s ′ ), s′ < r′
r = Fork (r ′ ), s = Fork (s ′ ) · s′′ , s′ < r′
r 6= r′ · r′′

ε
r∗

r =φ∨r =ε
otherwise

26

Martin Sulzmann and Peter Thiemann



φ
F (r) = ε


Fork (r )

r=φ
r=ε
otherwise

This normal form exploits the following lemma, which is straightforward to prove
from the semantics.
Lemma 33. Fork (r ) · Fork (s) ≡ Fork (s) · Fork (r ), for all r and s.

B

Nullable and Emptiness Test

Definition 34 (Nullable Test).
N (φ) = False
N (r + s) = N (r) ∨ N (s)

N (ε) = True
N (r · s) = N (r) ∧ N (s)

N (x) = True
N (r∗ ) = True

N (Fork (r )) = N (r)
Lemma 35. Let r be a behavior. Then, ε ∈ L(r) iff N (r).
Definition 36 (Emptiness Test).
Φ(φ) = True
Φ(r + s) = Φ(r) ∧ Φ(s)

Φ(ε) = False
Φ(r · s) = Φ(r) ∨ Φ(s)

Φ(x) = False
Φ(r∗ ) = False

Φ(Fork (r )) = Φ(r)
Lemma 37. Let r be a behavior. Then, L(r) = {} iff Φ(r).
Proof. Fact: L(r, {}) = {}. We verify L(r, K) 6= {} iff ¬Φ(r). The proof proceeds
by straightforward induction.
⊓
⊔

