arXiv:cs/0405097v1 [cs.LO] 26 May 2004

A Coalgebraic Approach to Kleene Algebra with Tests∗
Riccardo Pucella
Cornell University
Ithaca, NY 14853
riccardo@cs.cornell.edu

Hubie Chen
Cornell University
Ithaca, NY 14853
hubes@cs.cornell.edu

Abstract
Kleene algebra with tests is an extension of Kleene algebra, the algebra of regular expressions, which can be used to reason about programs. We develop a coalgebraic theory of Kleene
algebra with Tests, along the lines of the coalgebraic theory of regular expressions based on deterministic automata. Since the known automata-theoretic presentation of Kleene algebra with
tests does not lend itself to a coalgebraic theory, we define a new interpretation of Kleene algebra with tests expressions and a corresponding automata-theoretic presentation. One outcome
of the theory is a coinductive proof principle, that can be used to establish equivalence of our
Kleene algebra with tests expressions.

1 Introduction
Kleene algebra (KA) is the algebra of regular expressions [Conway 1971; Kleene 1956]. As is well
known, the theory of regular expressions enjoys a strong connection with the theory of finite-state
automata. This connection was used by Rutten [1998] to give a coalgebraic treatment of regular
expressions. One of the fruits of this coalgebraic treatment is coinduction, a proof technique for
demonstrating the equivalence of regular expressions [Rutten 2000]. Other methods for proving
the equality of regular expressions have previously been established—for instance, reasoning by
using a sound and complete axiomatization [Kozen 1994; Salomaa 1966], or by minimization of
automata representing the expressions [Hopcroft and Ullman 1979]. However, the coinduction
proof technique can give relatively short proofs, and is fairly simple to apply.
Recently, Kozen [1997] introduced Kleene algebra with tests (KAT), an extension of KA designed for the particular purpose of reasoning about programs and their properties. The regular
expressions of KAT allow one to intersperse boolean tests along with program actions, permitting
the convenient modelling of programming constructs such as conditionals and while loops. The utility of KAT is evidenced by the fact that it subsumes propositional Hoare logic, providing a complete
deductive system for Hoare-style inference rules for partial correctness assertions [Kozen 1999].
The goal of this paper is to develop a coalgebraic theory of KAT, paralleling the coalgebraic
treatment of KA. Our coalgebraic theory yields a coinductive proof principle for demonstrating the
equality of KAT expressions, in analogy to the coinductive proof principle for regular expressions.
∗

This paper is essentially the same as one that will appear in Theoretical Computer Science. A preliminary version appeared in the Proceedings of the Sixth International Workshop on Coalgebraic Methods in Computer Science, Electronic
Notes in Theoretical Computer Science, Volume 82.1, 2003.

1

The development of our coalgebraic theory proceeds as follows. We first introduce a form of deterministic automaton and define the language accepted by such an automaton. Next, we develop
the theory of such automata, showing that coinduction can be applied to the class of languages representable by our automata. We then give a class of expressions, which play the same role as the
regular expressions in classical automata theory, and fairly simple rules for computing derivatives
of these expressions.
The difficulty of our endeavor is that the known automata-theoretic presentation of KAT [Kozen
2003] does not lend itself to a coalgebraic theory. Moreover, the notion of derivative, essential to
the coinduction proof principle in this context, is not readily definable for KAT expressions as they
are defined by Kozen [1997]. Roughly, these difficulties arise from tests being commutative and
idempotent, and suggest that tests need to be handled in a special way. In order for the coalgebraic
theory to interact smoothly with tests, we introduce a type system along with new notions of strings,
languages, automata, and expressions, which we call mixed strings, mixed languages, mixed automata, and mixed expressions, respectively. (We note that none of these new notions coincide with
those already developed in the theory of KAT.) All well-formed instances of these notions can be
assigned types by our type system. Our type system is inspired by the type system devised by Kozen
[1998, 2002] for KA and KAT, but is designed to address different issues.
This paper is structured as follows. In the next section, we introduce mixed strings and mixed
languages, which will be used to interpret our mixed expressions. In Section 3, we define a notion of
mixed automaton that is used to accept mixed languages. We then impose a coalgebraic structure on
such automata. In Section 4, we introduce a sufficient condition for proving equivalence that is more
convenient than the condition that we derive in Section 3. In Section 5, we introduce our type system
for KAT, and connect typed KAT expressions with the mixed language they accept. In Section 6, we
give an example of how to use the coalgebraic theory, via the coinductive proof principle, to establish
equivalence of typed KAT expressions. In Section 7, we show that our technique is complete, that
is, it can establish the equivalence of any two typed KAT expressions that are in fact equivalent. We
conclude in Section 8 with considerations of future work.

2 Mixed Languages
In this section, we define the notions of mixed strings and mixed languages that we will use throughout the paper. Mixed strings are a variant of the guarded strings introduced by Kaplan [1969] as an
abstract interpretation for program schemes; sets of guarded strings were used by Kozen [2003] as
canonical models for Kleene algebra with tests. Roughly speaking, a guarded string can be understood as a computation where atomic actions are executed amidst the checking of conditions, in the
form of boolean tests. Mixed strings will be used as an interpretation for the mixed expressions we
introduce in Section 5.
Mixed strings are defined over two alphabets: a set of primitive programs (denoted P) and a
set of primitive tests (denoted B). We allow P to be infinite, but require that B be finite. (We will
see in Section 3 where this finiteness assumption comes in. Intuitively, this is because our automata
will process each primitive test individually.) Primitive tests can be put together to form more
complicated tests. A literal l is a primitive test b ∈ B or its negation b; the underlying primitive
test b is said to be the base of the literal, and is denoted by base(l). When A is a subset of B,
lit(A) denotes the set of all literals over A. A test is a nonempty set of literals with distinct bases.

2

Intuitively, a test can be understood as the conjunction of the literals it comprises. The base of a test
t, denoted by base(t), is defined to be the set {base(l) : l ∈ t}, in other words, the primitive tests
the test t is made up from. We extend the notion of base to primitive programs, by defining the base
of a primitive program p ∈ P as ∅.
Example 2.1: Let P = {p, q}, and B = {b, c, d}. The literals lit(B) of B are {b, b, c, c, d, d}. Tests
include {b, c, d} and {b, d}, but {b, b, c} is not a test, as b and b have the same base b. The base of
{b, c, d} is {b, c, d}.
Primitive programs and tests are used to create mixed strings. A mixed string is either the empty
string, denoted by ǫ, or a sequence σ = a1 . . . an (where n ≥ 1) with the following properties:
(1) each ai is either a test or primitive program,
(2) for i = 1, . . . , n − 1, if ai is a test, then ai+1 is a primitive program,
(3) for i = 1, . . . , n − 1, if ai is a primitive program, then ai+1 is a test, and
(4) for i = 2, . . . , n − 1, if ai is a test, then base(ai ) = B.
Hence, a mixed string is an alternating sequence of primitive programs and tests, where each test
in the sequence is a “complete” test, except possibly if it occurs as the first or the last element of
the sequence. This allows us to manipulate mixed strings on a finer level of granularity; we can
remove literals from the beginning of a mixed strings and still obtain a mixed string. The length of
the empty mixed string ǫ is 0, while the length of a mixed string a1 . . . an is n.
Example 2.2: Let P = {p, q}, and B = {b, c, d}. Mixed strings include ǫ (of length 0), {b} and
p (both of length 1), and {b}p{b, c, d}q{d} (of length 5). The sequence {b}p{b, d}q{d} is not a
mixed string, since base({b, d}) 6= B.
We define the concatenation of two mixed strings σ and σ ′ , denoted by σ · σ ′ , as follows. If one
of σ, σ ′ is the empty string, then their concatenation is the other string. If both σ = a1 . . . an and
σ ′ = b1 . . . bm have non-zero length, their concatenation is defined as:
(1) τ = a1 . . . an b1 . . . bm if exactly one of an , b1 is a primitive program and τ is a mixed string;
(2) τ = a1 . . . an−1 (an ∪ b1 )b2 . . . bm if an and b1 are tests such that base(an ) ∩ base(b1 ) = ∅
and τ is a mixed string; and is
(3) undefined otherwise.
Intuitively, concatenation of the two strings is obtained by concatenating the sequence of string
elements, possibly by combining the last test of the first string with the first test of the second string,
provided that the result is a valid mixed string. We note that concatenation of strings is an associative
operation.
Example 2.3: Let P = {p, q}, and B = {b, c, d}. The concatenation of the mixed strings p and
{b, c, d}q is p{b, c, d}q. Similarly, the concatenation of the mixed strings {b}p{b, c} and {d}q{d}
is the mixed string {b}p{b, c, d}q{d}. However, the concatenation of {b}p{b, c} and {b, d}q is not
defined, as {b, c} ∩ {b, d} =
6 ∅. The concatenation of {b}p{b, c} and q is also not defined, as
base({b, c}) 6= B, and thus {b}p{b, c}q is not a mixed string.
3

We assign one or more types to mixed strings in the following way. A type is of the form
A → B, where A and B are subsets of B. Intuitively, a mixed string has type A → B if the first
element of the string has base A, and it can be concatenated with an element with base B. It will be
the case that a mixed string of type A → B can be concatenated with a mixed string of type B → C
to obtain a mixed string of type A → C.
The mixed string ǫ has many types, namely it has type A → A, for all A ∈ ℘(B). A mixed
string of length 1 consisting of a single test t has type base(t) ∪ A → A, for any A ∈ ℘(B) such
that A ∩ base(t) = ∅. A mixed string of length 1 consisting of a single program p has type ∅ → B.
A mixed string a1 . . . an of length n > 1 has type base(a1 ) → B \ base(an ).
Example 2.4: Let P = {p, q}, and B = {b, c, d}. The mixed string p{b, c, d} has type ∅ → ∅.
The mixed string {d}p has type {d} → B. The mixed string {b}p{b, c, d}q{b, c} has type {b} →
{d}. The concatenation of {b}p{b, c, d}q{b, c} and {d}p, namely {b}p{b, c, d}q{b, c, d}p, has type
{b} → B.
A mixed language is a set of mixed strings, and is typeable, with type A → B, if all of the
mixed strings it contains have type A → B. In this paper, we will only be concerned with typeable
mixed languages.
We will be interested in different operations on mixed languages in the following sections. When
L1 ,L2 , and L are mixed languages, we use the notation L1 · L2 to denote the set {σ1 · σ2 : σ1 ∈
L1 , σ2 ∈ L2 }, L0 to denote the set {ǫ}, and for n ≥ 1, Ln to denote the set L · Ln−1 . The following
two operations will be useful in Section 5. The operator T , defined by
T (L) = {σ : σ ∈ L, |σ| = 1, σ is a test}
extracts from a language all the mixed strings made up of a single test. The operator ǫ, defined by
ǫ(L) = L ∩ {ǫ}
essentially checks if the empty mixed string ǫ is in L, since ǫ(L) is nonempty if and only if the
empty mixed string is in L.

3 Mixed Automata
Having introduced a notion of mixed strings, we now define a class of deterministic automata that
can accept mixed strings. Mixed strings enforce a strict alternation between programs and tests,
and this alternation is reflected in our automata. The transitions of the automata are labelled with
primitive programs and literals. Given a mixed string, mixed automaton can process the tests in the
string in many different orders; this reflects the fact that the tests that appear in mixed strings are
sets of literals.
A mixed automaton over the set of primitive programs P and set of primitive tests B is a 3-tuple
M = (hSA iA∈℘(B) , o, hδA iA∈℘(B) ), consisting of a set SA of states for each possible base A 6= ∅
of a test as well as a set S∅ of program states, an output function o : SS
∅ → {0, 1}, and transition
functions δ∅ : S∅ × P → SB and (for A 6= ∅) δA : SA × lit(A) → A∈℘(B) SA , subject to the
following two conditions:
A1. δA (s, l) ∈ SA\{base(l)} , and
4

A2. for every state s in SA , for every test t with base A, and for any two orderings hx1 , . . . , xm i,
y1
ym
x1
xm
hy1 , . . . , ym i of the literals in t, if s −→
. . . −→
s1 and s −→ . . . −→ s2 then s1 = s2 .
l

(For convenience, we write s −→ s′ if δA (s, l) = s′ for A the base of s.)
We give an example of a mixed automaton in Example 3.2. Intuitively, a state in SA can process
a mixed string of type A → B, for some B. Condition A1 enforces the invariant that, as a string is
being processed, the current state is in SA , for A the base of the first element of the string. Condition
A2 is a form of “path independence”: regardless of the order in which we process the literals of a
test, we end up in the same program state. Condition A2, and basing transitions on literals rather
than tests, allow the manipulation of mixed expressions at a finer level of granularity. This is related
to a similar choice we made when allowing mixed strings to start with a test that is not “complete”.
This flexibility will be useful when we analyze mixed expressions in Section 5.
The accepting states are defined via the output function o(s), viewed as a characteristic function.
Accepting states are in S∅.
As in the coalgebraic treatment of automata [Rutten 1998], and contrary to standard definitions,
we allow both the state spaces SA and the set P of primitive programs to be infinite. We also do not
force mixed automata to have initial states, for reasons that will become clear.
We now define the mixed language accepted by a state of a mixed automaton. Call a sequence
µ = e1 . . . em of primitive programs and literals a linearization of a mixed string σ = a1 . . . an if
µ can be obtained from σ by replacing each test ai in σ with a sequence of length |ai | containing
exactly the literals in ai .
Example 3.1: Let P = {p, q}, and B = {b, c}. The mixed string {b}p{b, c}q{b, c} (of type
{b} → ∅) has four linearizations: bpbcqbc, bpcbqbc, bpbcqcb, and bpcbqcb.
Intuitively, a mixed string σ is accepted by an automaton if a linearization of σ is accepted by
the automaton according to the usual definition. Formally, a mixed string σ is accepted by a state s
of an automaton M if either
(1) σ is ǫ and s is a program state with o(s) = 1 (i.e., s is an accepting program state), or
e

e

1
m
(2) there exists a linearization e1 . . . em of σ such that s −→
. . . −→
s′ , s′ is a program state,
′
and o(s ) = 1.

If σ is accepted (by a state s) in virtue of satisfying the second criterion, then every linearization is
a witness to this fact— in other words, the existential quantification in the second criterion could
be replaced with a universal quantification (over all linearizations of σ) without any change in the
actual definition. This is because of condition A2 in the definition of a mixed automaton.
We define the mixed language accepted by state s of automaton M , written LM (s), as the set
of mixed strings accepted by state s of M . It is easy to verify that all the strings accepted by a state
have the same type, namely, if s is in SA , then every string in LM (s) has type A → ∅, and hence
LM (s) has type A → ∅.
Example 3.2: Let P = {p, q}, and B = {b, c}. Consider the mixed automaton over P and B

5

b
s1,{b}

p
s1,ø

s2,{b,c}
c

b

s2,{b}

s2,{c}

b

c
s2,ø

Figure 1: A mixed automaton
pictured in Figure 1, given by M = (hSA iA∈℘(B) , o, hδA iA∈℘(B) ), where:
S{b,c} = {s2,{b,c} , ssink,{b,c} }
S{b} = {s1,{b} , s2,{b} , ssink,{b} }
S{c} = {s2,{c} , ssink,{c} }
S∅ = {s1,∅, s2,∅, ssink,∅}
and
o(s1,∅) = 1
o(s2,∅) = 1
o(ssink,∅) = 0.
The transition function δA can be read off from Figure 1; note that the sink states ssink,A as well as the
transitions to the sink states are not pictured. Intuitively, any transition not pictured in the automaton
can be understood as going to the appropriate sink state. For instance, we have δ{b,c} (s2,{b,c} , c) =
ssink,{b} . We can check that the two conditions A1 and A2 hold in M . The language accepted by
state s1,{b} is LM (s1,{b} ) = {{b}, {b}p{b, c}}. The language accepted by state s1,∅ is LM (s1,∅) =
{ǫ, p{b, c}}.
We define a homomorphism between mixed automata M and M ′ to be a family f = hfA iA∈℘(B)
′ such that:
of functions fA : SA → SA
6

′ (f (s), p),
(1) for all s ∈ S∅, o(s) = o′ (f∅(s)), and for all p ∈ P, fB (δ∅(s, p)) = δ∅
∅
′ (f (s), l).
(2) for all s ∈ SA (where A 6= ∅) and all l ∈ lit(A), fA\{base(l)} (δA (s, l)) = δA
A

A homomorphism preserves accepting states and transitions. We write f : M → M ′ when f is a
homomorphism between automata M and M ′ . For convenience, we often write f (s) for fA (s) when
the type A of s is understood. It is straightforward to verify that mixed automata form a category
(denoted MA), where the morphisms of the category are mixed automata homomorphisms.
We are interested in identifying states that have the same behaviour, that is, that accept the same
mixed language. A bisimulation between two mixed automata M = (hSA iA∈℘(B) , o, hδA iA∈℘(B) )
′ i
′
′
′
and M ′ = (hSA
A∈℘(B) , o , hδA iA∈℘(B) ) is a family of relations hRA iA∈℘(B) where RA ⊆ SA × SA
such that the following two conditions hold:
′ , if sR s′ , then o(s) = o′ (s′ ) and for all p ∈ P, δ (s, p)R δ ′ (s′ , p),
(1) for all s ∈ S∅ and s′ ∈ S∅
∅
∅
B ∅
and
′ (where A 6= ∅), if sR s′ , then for all l ∈ lit(A), δ (s, l)R
′
′
(2) for all s ∈ SA and s′ ∈ SA
A
A
A\{base (l)} δA (s , l).

A bisimulation between M and itself is called a bisimulation on M . Two states s and s′ of M
having the same type B are said to be bisimilar, denoted by s ∼M s′ , if there exists a bisimulation
hRA iA∈℘(B) such that sRB s′ . (We simply write s ∼ s′ when M is clear from the context.) For each
M , the relation ∼M is the union of all bisimulations on M , and in fact is the greatest bisimulation
on M .
Proposition 3.3: If s is a state of M and s′ is a state of M ′ with s ∼ s′ , then LM (s) = LM ′ (s′ ).
Proof: We show, by induction on the length of mixed strings that for all mixed strings σ, and for all
states s, s′ such that s ∼ s′ , then σ ∈ LM (s) if and only if σ ∈ LM ′ (s′ ). For the empty mixed string
ǫ, we have ǫ ∈ LM (s) if and only if o(s) = 1 if and only if o′ (s′ ) = 1 (by definition of bisimilarity)
if and only if ǫ ∈ LM ′ (s′ ). Assume inductively that the results holds for mixed strings of length n.
Let σ be a mixed string of length n + 1, of the form aσ ′ . Assume σ ∈ LM (s). By definition, there
e1
em
is a linearization e1 . . . em of a and a state s1 such that s −→
. . . −→
s1 and σ ′ ∈ LM (s1 ). By the
e1
em
′
′
′
definition of bisimilar states, we have s −→ . . . −→ s1 and s1 ∼ s1 . By the induction hypothesis,
σ ′ ∈ LM ′ (s′1 ). By the choice of s′1 , we have that σ ∈ LM ′ (s′ ), as desired.
Conditions (1) and (2) of the definition of a bisimulation are analogous to the conditions in the
definition of a homomorphism. Indeed, a homomorphism can be viewed as a bisimulation.
Proposition 3.4: If f : M → M ′ is a mixed automataon homomorphism, then hRA iA∈℘(B) , defined
by RA = {(s, fA (s)) : s ∈ SA } is a bisimulation.
Proof: First, for all s ∈ S∅, sR∅s′ implies s′ = f∅(s), and o(s) = o′ (f∅(s)) = o′ (s′ ). Moreover,
′ (s′ , p) = δ ′ (f (s), p) = f (δ (s, l)), so that δ (s, l)R δ ′ (s′ , l), as
for all p ∈ P, we have δ∅
B ∅
∅
B ∅
∅ ∅
required. Similarly, let s ∈ SA (where A 6= ∅); sRA s′ implies s′ = fA (s), and thus for all
′ (s′ , l) = δ ′ (f (s), l) = f
′
′
l ∈ lit(A), δA
A\{base(l)} (δA (s, l)), so that δA (s, l)RA\{base (l)} δA (s , l),
A A
as required, proving that hRA iA∈℘(B) is a bisimulation.
An immediate consequence of this relationship is that homomorphisms preserve accepted languages.
7

Proposition 3.5: If f : M → M ′ is a mixed automaton homomorphism, then LM (s) = LM ′ (f (s))
for all states s of M .
Proof: Immediate from Propositions 3.4 and 3.3.
It turns out that we can impose a mixed automaton structure on the set of all mixed languages
with type A → ∅. We take as states mixed languages of type A → ∅. A state is accepting if the
empty string ǫ is in the language. It remains to define the transitions between states; we adapt the
idea of Brzozowski derivatives [Brzozowski 1964]. Our definition of derivative depends on whether
we are taking the derivative with respect to a program element or a literal.
If the mixed language L has type ∅ → B and p ∈ P is a primitive program, define
Dp (L) = {σ : p · σ ∈ L}.
If the mixed language L has type A → B (for A 6= ∅) and l ∈ lit(A) is a literal, then
Dl (L) = {σ : {l} · σ ∈ L}.
Define LA to be the set of mixed languages of type A → ∅. Define L to be (hLA iA∈℘(B) , oL , hδA iA∈℘(B) ),
where oL (L) = 1 if ǫ ∈ L, and 0 otherwise; δ∅(L, p) = Dp (L); and δA (L, l) = Dl (L), for A 6= ∅
and l ∈ lit(A). It is easy to verify that L is indeed a mixed automaton. The following properties of
L are significant.
Proposition 3.6: For a mixed automaton M with states hSA iA∈℘(B) , the maps fA : SA → L
mapping a state s in SA to the language LM (s) form a mixed automaton homomorphism.
Proof: We check the two conditions for the family hfA iA∈℘(B) to be a homomorphism. First, given
s ∈ S∅, o(s) = 1 if and only if ǫ ∈ LM (s), which is equivalent to oL (f∅(s)) = 1. Moreover, given
p ∈ B, fB (δ∅(s, p)) = LM (δ∅(s, p)) = {σ : p · σ ∈ LM (s)} = Dp (LM (s)) = Dp (f∅(s)),
as required. Similarly, given s ∈ SA (where A 6= ∅), and l ∈ lit(A), fA\{base(l)} (δA (s, l)) =
LM (δA (s, l)) = {σ : {l} · σ ∈ LM (s)} = Dl (LM (s)) = Dl (fA (s)), as required.
Proposition 3.7: For any mixed language L in L, the mixed language accepted by state L in L is L
itself, that is, LL (L) = L.
Proof: We prove by induction on the length of linearizations of σ that for all mixed strings σ,
σ ∈ L if and only if σ ∈ LL (L). For the empty mixed string ǫ, we have ǫ ∈ L ⇔ oL (L) = 1 ⇔ ǫ ∈
LL (L). For σ of the form pσ ′ , we have σ = p·σ ′ , and thus we have p·σ ′ ∈ L ⇔ σ ′ ∈ Dp (L), which
by the induction hypothesis holds if and only if σ ′ ∈ LL (Dp (L)) ⇔ σ ′ ∈ Dp (LL (L)) (because
LL is a mixed automaton homomorphism from L to L), which is just equivalent to p · σ ′ ∈ LL (L).
For σ with a linearization le1 . . . em , letting σ ′ denote a string with linearization e1 . . . em , we have
σ = {l} · σ ′ , and we can derive in an exactly similar manner that {l} · σ ′ ∈ L ⇔ σ ′ ∈ Dl (L) ⇔
σ ′ ∈ LL (Dl (L)) ⇔ σ ′ ∈ Dl (LL (L)) ⇔ {l} · σ ′ ∈ LL (L) ⇔ σ ∈ LL (L).
These facts combine into the following fundamental property of L, namely, that L is a final
automaton.

8

Theorem 3.8: L is final in the category MA, that is, for every mixed automaton M , there is a
unique homomorphism from M to L.
Proof: Let M be a mixed automaton. By Proposition 3.6, there exists a homomorphism f from M
to the final automaton L, mapping a state s to the language LM (s) accepted by that state. Let f ′ be
another homomorphism from M to L. To establish uniqueness, we need to show that for any state
s of M , we have f (s) = f ′ (s):
f (s) = LM (s)

(by definition of f )

′

= LL (f (s))(by Proposition 3.5)
= f ′ (s)

(by Proposition 3.7).

Hence, f is the required unique homomorphism.
The finality of L gives rise to the following coinduction proof principle for language equality,
in a way which is by now standard [Rutten 2000].
Corollary 3.9: For two mixed languages K and L of type A → ∅, if K ∼ L then K = L.
In other words, to establish the equality of two mixed languages, it is sufficient to exhibit a
bisimulation between the two languages when viewed as states of the final automaton L. In the
following sections, we will use this principle to analyze equality of languages described by a typed
form of KAT expressions.

4 Pseudo-Bisimulations
The “path independence” condition (A2) in the definition of a mixed automaton gives mixed automata a certain form of redundancy. It turns out that due to this redundancy, we can define a
simpler notion than bisimulation that still lets us establish the bisimilarity of states.
A pseudo-bisimulation (relative to the ordering b1 , . . . , b|B| of the primitive tests in B) between
′ i
′
′
two mixed automata M = (hSA iA∈℘(B) , o, hδA iA∈℘(B) ) and M ′ = (hSA
A∈℘(B) , o , hδA iA∈℘(B) )
′
is a family of relations hRi ii=0,... ,|B| where Ri ⊆ SAi × SAi (with Ai denoting {bj : j ≤ i, j ∈
{1, . . . , |B|}}) such that the following two conditions hold:
′ , if sR s′ , then o(s) = o′ (s′ ) and for all p ∈ P, δ (s, p)R δ ′ (s′ , p),
(1) for all s ∈ S∅ and s′ ∈ S∅
0
∅
|B| ∅
and
′ , if sR s′ , then for all l ∈ lit(b ),
(2) for all i = 1, . . . , |B|, for all s ∈ SAi and s′ ∈ SA
i
i
i
′ (s′ , l).
δAi (s, l)Ri−1 δA
i

The sense in which pseudo-bisimulation is weaker than a bisimulation is that there need not
be a relation for each element of ℘(B). As the following theorem shows, however, we can always
complete a pseudo-bisimulation to a bisimulation.
Theorem 4.1: If hRi ii=0,... ,|B| is a pseudo-bisimulation (relative to the ordering b1 , . . . , b|B| of the
′ i such that R′ = R for all i = 0, . . . , |B|
primitive tests in B), then there exists a bisimulation hRA
i
Ai
(with Ai denoting {bj : j ≤ i, j ∈ {1, . . . , |B|}}).

9

Proof: Let hRi ii=0,... ,|B| be a pseudo-bisimulation (relative to the ordering on primitive tests
′ ⊆ S × S ′ for each A ∈ ℘(B), and show
b1 , . . . , b|B| ). We define a family of relations RA
A
A
that it forms a bisimulation with the required property. The proof relies on the path independence
condition A2 of mixed automata in a fundamental way. Given A ∈ ℘(B), let i(A) be the largest i ∈
{1, . . . , |B|} such that {b1 , . . . , bi } ⊆ A, and let c(A) be the relative complement of {b1 , . . . , bi(A) }
defined by A \ {b1 , . . . , bi(A) }. We say that a sequence of literals l1 , . . . , lk is exhaustive over a set
′ as follows: sR′ s′ holds if and
of bases A if A = {base(l1 ), . . . , base(lk )} and |A| = k. Define RA
A
l

l

l

1
1
k
only if for all literal sequences l1 , . . . , lk exhaustive over c(A), we have s −→
. . . −→
s1 , s′ −→

l

k
′ =R
. . . −→
s′1 , and s1 Ri(A) s′1 . Clearly, if A = {b1 , . . . , bi(A) }, then RA
i(A) , as required. We now
′ s′ , then sR s′ , and hence
′
′
check that hRA iA∈℘(B) is a bisimulation. Clearly, since R∅ = R0 , if sR∅
0
o(s) = o′ (s′ ), and for all p ∈ P, it holds that δ∅(s, p)R|B| δ∅(s′ , p), implying δ∅(s, p)RB′ δ∅(s′ , p).
′ , l ∈ lit(A), and assume sR′ s′ . Consider the following cases:
Now, let A 6= ∅, s ∈ SA , s′ ∈ SA
A
′ s′ , then sR
′
Case A = {b1 , . . . , bi(A) }, base(l) = bi(A) : Since sRA
i(A) s , and by the properties
′
of pseudo-bisimulations, we have δA (s, l)Ri(A)−1 δA (s′ , l), which is exactly δA (s, l)RA\{base(l)}
δA (s′ , l).
′
′
′
Case A = {b1 , . . . , bi(A) }, base(l) = bj , j < i(A): Since sRA s , then sRi(A) s . let l1 , . . . , lk
′
′
be an arbitrary exhaustive sequence of literals over {bi(A) , . . . , bj+1 }. Let li(A)
, . . . , lj+1
be the
′
′
′
arrangement of l1 , . . . , lk such that base(lm ) = bm . Consider the states s1 , s2 , s1 , s2 such that
′
li(A)

′
lj+1

′
li(A)

l

′
lj+1

l

s −→ . . . −→ s1 −→ s2 , and s′ −→ . . . −→ s′1 −→ s′2 . By the definition of pseudo-bisimulation,
′
li(A)

l

we have that s2 Rj−1 s′2 . Now, by condition A2, we have states s3 , s′3 such that s −→ s3 −→
′
lj+1

′
li(A)

l

′
lj+1

l

l

1
k
. . . −→ s2 and s′ −→ s′3 −→ . . . −→ s′2 . By condition A2 again, we have that s3 −→
. . . −→
s2

l

l

k
1
and s′3 −→
s′2 . Since l1 , . . . , lk was arbitrary, s2 Rj−1 s′2 and i(A \ {base(l)}) = j − 1, we
. . . −→
′
′
′
have s3 RA\{base(l)} s′3 , that is, δA (s, l)RA\{base
(l)} δA (s , l).
Case A ⊃ {b1 , . . . , bi(A) }, base(l) ∈ c(A)): Pick an arbitrary sequence l1 , . . . , lk of literals

l

l

l

k
1
that is exhaustive over c(A \ {base(l)}), and states s1 , s2 , s′1 , s′2 such that s −→ s2 −→
s1 ,
. . . −→

l

l

l

1
k
′ , we have s R
′
. . . −→
s′1 . By definition of RA
and s′ −→ s′2 −→
1 i(A) s1 . Since the sequence of
′
literals l1 , . . . , lk was arbitrary, and since i(A) = i(A \ {base(l)}), we have that s2 RA\{base(l)}
s′2 ,
′
that is, δA (s, l)RA\{base(l)}
δA (s′ , l).
Case A ⊃ {b1 , . . . , bi(A) }, base(l) = bi(A) : Pick an arbitrary sequence l1 , . . . , lk of literals

l

l

l

l

1
1
k
k
. . . −→
s1 and s′ −→
. . . −→
s′1 .
that is exhaustive over c(A), and states s1 , s′1 such that s −→

l

′ , we have s R
′
By definition of RA
1 i(A) s1 . By definition of pseudo-bisimulation, if s1 −→ s2 and
l

l

s′1 −→ s′2 , then we have s2 Ri(A)−1 s′2 . By condition A2, we have that for states s3 , s′3 , s −→
l

l

l

l

l

1
k
1
k
. . . −→
s′2 . Thus, since l1 , . . . , lk was arbitrary, and
s3 −→
. . . −→
s2 and s′ −→ s′3 −→
′
′
δA (s′ , l).
i(A \ {base(l)}) = i(A) − 1, we have s3 RA\{base(l)}
s′3 , that is, δA (s, l)RA\{base(l)}
Case A ⊃ {b1 , . . . , bi(A) }, base(l) = bj , j < i(A): Pick an arbitrary sequence l1 , . . . , lk of
literals that is exhaustive over c(A)∪{bi(A) , . . . , bj+1 }. Let l1′ , . . . , lk′ ′ be the elements of l1 , . . . , lk
with bases in c(A). Let l1′′ , . . . , lk′′′′ be the elements of l1 , . . . , lk with bases in {bi(A) , . . . , bj+1 }. Let
′′′ , . . . , l′′′ be the arrangement of l′′ , . . . , l′′ such that base(l′′′ ) = b . Consider states s , s′
li(A)
m
1 1
m
1
j+1
k ′′

l′

l′ ′

l′

l′ ′

1
k
1
k
′ , we have s R
′
. . . −→
. . . −→
such that s −→
s1 and s′ −→
s′1 . By definition of RA
1 i(A) s1 . Now,

10

′′′
li(A)

′′′
lj+1

l

′′′
li(A)

′′′
lj+1

l

l

l

l

l

l

consider states s2 , s3 , s′2 , s′3 such that s1 −→ . . . −→ s2 −→ s3 and s′1 −→ . . . −→ s′2 −→ s′3 . By
the definition of pseudo-bisimulation, since s1 Ri(A) s′1 , we have that s3 Rj−1 s′3 . Now, by condition
l

1
k
1
k
. . . −→
s′3 .
. . . −→
s3 and s′ −→ s′4 −→
A2, we have states s4 , s′4 such that s −→ s4 −→
′
Since l1 , . . . , lk was arbitrary, and i(A \ {base(l)}) = j − 1, we have s4 RA\{base(l)}
s′4 , that is,
′
′
δA (s, l)RA\{base (l)} δA (s , l).

Let us say that two states s, s′ are pseudo-bisimilar if they are related by some Ri in a pseudobisimulation hRi i; it follows directly from Theorem 4.1 that pseudo-bisimilar states are bisimilar.

5 Mixed Expressions and Derivatives
A mixed expression (over the set of primitive programs P and the set of primitive tests B) is any
expression built via the following grammar:
e ::= 0 | 1 | p | l | e1 + e2 | e1 · e2 | e∗
(with p ∈ P and l ∈ lit(B)). For simplicity, we often write e1 e2 for e1 · e2 . We also freely
use parentheses when appropriate. Intuitively, the constants 0 and 1 stand for failure and success,
respectively. The expression p represents a primitive program, while l represents a primitive test.
The operation + is used for choice, · for sequencing, and ∗ for iteration. These are a subclass
of the KAT expressions as defined by Kozen [1997]. (In addition to allowing negated primitive
tests, Kozen also allows negated tests.) We call them mixed expressions to emphasize the different
interpretation we have in mind.
In a way similar to regular expressions denoting regular languages, we define a mapping M
from mixed expressions to mixed languages inductively as follows:
M (0) = ∅
M (1) = {ǫ}
M (p) = {p}
M (l) = {{l}}
M (e1 + e2 ) = M (e1 ) ∪ M (e2 )
M (e1 · e2 ) = M (e1 ) · M (e2 )
[
M (e∗ ) =
M (e)n .
n≥0

The mapping M is a rather canonical homomorphism from mixed expressions to mixed languages. (It is worth noting that we have not defined any axioms for deriving the “equivalence” of
mixed expressions, and it is quite possible for distinct mixed expressions to give rise to the same
mixed language.)
Inspired by a type system devised by Kozen [1998, 2002] for KA and KAT expressions, we
impose a type system on mixed expressions. The types have the form A → B, where A, B ∈ ℘(B),
the same types we assigned to mixed strings in Section 2. We shall soon see that this is no accident.
We assign a type to a mixed expression via a type judgment written ⊢ e : A → B. The following

11

inference rules are used to derive the type of a mixed expression:
⊢0:A→B

⊢1:A→A

⊢p:∅→B

⊢ l : A ∪ {base(l)} → A \ {base(l)}

⊢ e1 : A → B ⊢ e2 : A → B
⊢ e1 + e2 : A → B

⊢ e1 : A → B ⊢ e2 : B → C
⊢ e1 · e2 : A → C

e:A→A
.
e∗ : A → A
It is clear from these rules that any subexpression of a mixed expression having a type judgment
also has a type judgment.
The typeable mixed expressions (which intuitively are the “well-formed” expressions) induce
typeable mixed languages via the mapping M , as formalized by the following proposition.
Proposition 5.1: If ⊢ e : A → B, then M (e) is a mixed language of type A → B.
Proof: A straightforward induction on the structure of mixed expressions.
Our goal is to manipulate mixed languages by manipulating the mixed expressions that represent
them via the mapping M . (Of course, not every mixed language is in the image of M .) In particular,
we are interested in the operations T (L) and ǫ(L), as defined in Section 2, as well as the language
derivatives Dp and Dl introduced in the last section.
We now define operators on mixed expressions that capture those operators on the languages
denoted by those mixed expressions. We define T̂ inductively on the structure of mixed expressions,
as follows:
T̂ (0) = 0
T̂ (1) = 1
T̂ (p) = 0
T̂ (l) = l
T̂ (e1 + e2 ) = T̂ (e1 ) + T̂ (e2 )
T̂ (e1 · e2 ) = T̂ (e1 ) · T̂ (e2 )
T̂ (e∗ ) = T̂ (e)∗
(where p ∈ P and l ∈ lit(B)). The operator T̂ “models” the operator T (L), as is made precise in
the following way.
Proposition 5.2: If ⊢ e : A → B, then T̂ (e) is a typeable mixed expression such that T (M (e)) =
M (T̂ (e)).

12

Proof: A straightforward induction on the structure of mixed expressions.
We define ǫ̂ inductively on the structure of mixed expressions, as follows:
ǫ̂(0) = 0
ǫ̂(1) = 1
ǫ̂(p) = 0
ǫ̂(l) = 0

0
ǫ̂(e1 + e2 ) =
1

1
ǫ̂(e1 · e2 ) =
0

if ǫ̂(e1 ) = ǫ̂(e2 ) = 0
otherwise
if ǫ̂(e1 ) = ǫ̂(e2 ) = 1
otherwise

ǫ̂(e∗ ) = 1
(where p ∈ P and l ∈ lit(B)). Note that ǫ̂(e) is always the mixed expression 0 or 1. In analogy to
Proposition 5.2, we have the following fact connecting the ǫ and ǫ̂ operators.
Proposition 5.3: If ⊢ e : A → B, then ǫ̂(e) is a typeable mixed expression such that ǫ(M (e)) =
M (ǫ̂(e)).
Proof: A straightforward induction on the structure of mixed expressions.
Finally, we define, by induction on the structure of mixed expressions, the derivative operator
D̂ for typeable mixed expressions. There are two forms of the derivative, corresponding to the two
forms of derivative for mixed languages: the derivative D̂l with respect to a literal l ∈ lit(B), and
the derivative D̂p with respect to a primitive program p ∈ P. The two forms of derivative are
defined similarly, except on the product of two expressions. (Strictly speaking, since the definition
of the derivative depends on the type of the expressions being differentiated, D̂ should take type
derivations as arguments rather than simply expressions. To lighten the notation, we write D̂ as
though it took mixed expressions as arguments, with the understanding that the appropriate types
are available.)
The derivative D̂p with respect to a primitive program p ∈ P is defined as follows:
D̂p (0) = 0
D̂p (1) = 0

1 if p = q
D̂p (q) =
0 otherwise
D̂p (l) = 0
D̂p (e1 + e2 ) = D̂p (e1 ) + D̂p (e2 )

D̂p (e1 ) · e2
if B 6= ∅
D̂p (e1 · e2 ) =
D̂p (e1 ) · e2 + ǫ̂(e1 ) · D̂p (e2 ) otherwise
where ⊢ e1 : A → B and ⊢ e2 : B → C
D̂p (e∗ ) = D̂p (e) · e∗ .
13

The derivative D̂l with respect to a literal l ∈ lit(B) is defined as follows:
D̂l (0) = 0
D̂l (1) = 0
D̂l (p) = 0

1 if l = l′
′
D̂l (l ) =
0 otherwise
D̂l (e1 + e2 ) = D̂l (e1 ) + D̂l (e2 )

D̂l (e1 ) · e2
if base(l) ∈
/B
D̂l (e1 · e2 ) =
D̂l (e1 ) · e2 + T̂ (e1 ) · D̂l (e2 ) otherwise
where ⊢ e1 : A → B and ⊢ e2 : B → C
∗

D̂l (e ) = D̂l (e) · e∗ .
We have the following proposition, similar to the previous two, connecting the derivative D̂ to
the previously defined derivative D on mixed languages.
Proposition 5.4: Suppose that ⊢ e : A → B.
If A = ∅, then for all p ∈ P, Dp (M (e)) = M (D̂p (e)).
If A 6= ∅, then for all l ∈ lit(A), Dl (M (e)) = M (D̂l (e)).
Proof: The proof is by induction on the structure of the mixed expression e. To illustrate the proof
technique, we give one case of the proof.
Suppose that ⊢ e1 : A → B and ⊢ e2 : B → C, and e = e1 · e2 . Suppose further that
l ∈ lit(B) is a literal such that base(l) ∈ A and base(l) ∈ B. We will show that the proposition
holds for the expression e, assuming (by the induction hypothesis) that the proposition holds for all
subexpressions of e.
We first establish three claims that will be needed.
Claim 1: If t is a test which (as a mixed string) can be judged to have type A → B, then {t} · {σ :
{l} · σ ∈ M (e2 )} = {σ ′ : {l} · σ ′ ∈ {t} · M (e2 )}.
First suppose that σ is a mixed string such that {l} · σ ∈ M (e2 ). Then σ can be judged to
have type B \ {base(l)} → C, and so {l} · {t} · σ = {t} · {l} · σ ∈ {t} · M (e2 ). It follows that
t · σ ∈ {σ ′ : {l} · σ ′ ∈ {t} · M (e2 )}. For the other direction, suppose that σ ′ is a mixed string such
that {l} · σ ′ ∈ {t} · M (e2 ). Then there exists a mixed string τ ∈ M (e2 ) such that {l} · σ ′ = {t} · τ .
Since t can be judged to have type A → B and base(l) ∈ A ∩ B, base(l) ∈
/ t and there exists a
mixed string σ such that {l} · σ ′ = {t} · τ = {l} · {t} · σ. Thus σ ′ = {t} · σ where {l} · σ ∈ M (e2 ).
Claim 2: If σ is a mixed string such that l · σ ∈ M (e1 ), then l · σ ∈ M (e1 ) \ T (M (e1 )).
This claim holds because {l} · σ ∈ M (e1 ) implies that σ has type A \ {base(l)} → B; since
B 6⊆ A′ , by the definition of the type of a mixed string, |σ| > 1 and so |{l} · σ| > 1.
Claim 3: {σ : {l}·σ ∈ M (e1 )\T (M (e1 ))}·M (e2 ) = {σ : {l}·σ ∈ (M (e1 )\T (M (e1 )))·M (e2 )}
The ⊆ direction is straightforward. For the ⊇ direction, let σ be a mixed string in the second
set; then, there exist strings τ1 ∈ M (e1 ) \ T (M (e1 )) and τ2 ∈ M (e2 ) such that {l} · σ = τ1 · τ2 .
All strings in M (e1 ) have type A → B; since base(l) ∈ B, there are no strings in M (e1 ) of length
one consisting of a primitive program, and so |τ1 | > 3. Hence σ = σ ′ · τ2 for some mixed string σ ′
such that {l} · σ ′ ∈ M (e1 ) \ T (M (e1 )).
14

Using these three claims, we show that Dl (M (e)) = M (D̂l (e)):
M (D̂l (e1 · e2 ))
= M (D̂l (e1 ) · e2 + T̂ (e1 ) · D̂l (e2 ))

(by definition of D̂l )

= M (D̂l (e1 )) · M (e2 ) ∪ M (T̂ (e1 )) · M (D̂l (e2 )) (by definition of M )
= Dl (M (e1 )) · M (e2 ) ∪ M (T̂ (e1 )) · D(M (e2 ))

(by induction hypothesis)

= Dl (M (e1 )) · M (e2 ) ∪ T (M (e1 )) · D(M (e2 ))

(by Proposition 5.2)

= {σ : {l} · σ ∈ M (e1 )} · M (e2 ) ∪
T (M (e1 )) · {σ : {l} · σ ∈ M (e2 ))}

(by definition of Dl )

= {σ : {l} · σ ∈ M (e1 )} · M (e2 ) ∪
{σ : {l} · σ ∈ T (M (e1 )) · M (e2 ))}

(by Claim 1)

= {σ : {l} · σ ∈ M (e1 ) \ T (M (e1 ))} · M (e2 ) ∪
{σ : {l} · σ ∈ T (M (e1 )) · M (e2 ))}

(by Claim 2)

= {σ : {l} · σ ∈ (M (e1 ) \ T (M (e1 ))) · M (e2 )} ∪
{σ : {l} · σ ∈ T (M (e1 )) · M (e2 ))}

(by Claim 3)

= {σ : {l} · σ ∈ M (e1 ) · M (e2 )}
= Dl (M (e1 ) · M (e2 ))

(by definition of Dl )

= Dl (M (e1 · e2 ))

(by definition of M ).

The other cases are similar.

6 Example
In this section, we use the notions of pseudo-bisimulation and the coinduction proof principle
(Corollary 3.9), along with the derivative operator D̂, to prove the equivalence of two mixed languages specified as mixed expressions.
Fix P to be the set of primitive programs {p, q}, and B to be the set of primitive tests {b, c}. Let
[b] be a shorthand for (b + b). Define α to be the mixed expression
(bp([b]cq)∗ c)∗ b
and β to be the mixed expression
bp([b]cq + bcp)∗ cb + b.
Our goal is to prove that α and β are equivalent, in the sense that they induce the same language
via the mapping M . In other words, we want to establish that M (α) = M (β). This example
demonstrates the equivalence of the program
while b do {
p;
while c do q
}
15

and the program
if b then {
p;
while b + c do
if c then q else p
}
This equivalence is a component of the proof of the classical result that every while program can be
simulated by a while program with at most one while loop, as presented by Kozen [1997]. We refer
the reader there for more details.
There are a few ways to establish this equivalence. One is to rely on a sound and complete axiomatization of the equational theory of KAT, and derive the equivalence of α and β algebraically
[Kozen and Smith 1996]. Another approach is to first construct for each expression an automaton
that accepts the language it denotes, and then minimize both automata [Kozen 2003]. Two expressions are then equal if the two resulting automata are isomorphic.
In this paper, we describe a third approach, using the coinductive proof principle for mixed
languages embodied by Corollary 3.9. Since the theory we developed in Section 3 applies only to
mixed languages of type A → ∅, we verify that indeed we have ⊢ α : {b} → ∅ and ⊢ β : {b} → ∅,
so that, by Proposition 5.1, M (α) and M (β) are languages of type {b} → ∅.
We prove the equivalence of α and β by showing that the mixed languages M (α) and M (β)
are pseudo-bisimilar, that is, they are related by some pseudo-bisimulation. More specifically, we
exhibit a pseudo-bisimulation, relative to the ordering b1 = b, b2 = c, on the final automaton
L, such that M (α) and M (β) are pseudo-bisimilar. This is sufficient for proving equivalence,
since by Theorem 4.1, the languages M (α) and M (β) are then bisimilar, and by Corollary 3.9,
M (α) = M (β).
Define α′ to be the mixed expression
([b]cq)∗ cα
and define β ′ to be the mixed expression
([b]cq + bcp)∗ cb.
Notice that β = bpβ ′ + b.
We note that (using the notation of the definition of pseudo-bisimulation), A0 = ∅, A1 = {b},
and A2 = {b, c}. We claim that the following three relations form a pseudo-bisimulation:
R2 = {(M (α′ ), M (β ′ )),
(M (0), M (0))}

R1 = {(M ([b]qα′ ), M ([b]qβ ′ )),
(M (α), M (β))}

R0 = {(M (pα′ ), M (pβ ′ )),
(M (qα′ ), M (qβ ′ )),
(M (1), M (1)),
(M (0), M (0))}.

16

It is straightforward to verify that hR0 , R1 , R2 i is a pseudo-bisimulation on L, using the operators defined in the previous section. For instance, consider Db (M (α)), which is equal to M (D̂b (α))
by Proposition 5.4. We compute D̂b (α) here:
D̂b (α) = D̂b ((bp([b]cq)∗ c)∗ )b + T̂ ((bp([b]cq)∗ c)∗ )D̂b (b)
= D̂b (bp([b]cq)∗ c)(bp([b]cq)∗ c)∗ b + T̂ ((bp([b]cq)∗ c)∗ )0
= p([b]cq)∗ c(bp([b]cq)∗ c)∗ b
= pα′ .
Hence, Db (M (α)) = M (D̂b (α)) = M (pα′ ). The other cases are similar.
As we shall see shortly, there is a way to mechanically construct such a bisimulation to establish
the equivalence of two mixed expressions.
We remark that an alternative approach to establish equivalence of while programs based on
coalgebras is described by Rutten [1999]. This approach uses the operational semantics of the
programs instead of an algebraic framework.

7 Completeness
Thus far, we have established a coinductive proof technique for establishing the equality of mixed
languages (Section 3), and illustrated its use by showing the equality of two particular mixed languages specified by mixed expressions (Section 6), making use of the derivative calculus developed
in Section 5. A natural question about this proof technique is whether or not it can establish the
equivalence of any two mixed expressions that are equivalent (in that they specify the same mixed
language). In this section, we answer this question in the affirmative by formalizing and proving
a completeness theorem for our proof technique. In particular, we show that given two equivalent
mixed expressions, a finite bisimulation relating them can be effectively constructed, by performing only simple syntactic manipulations. In fact, we exhibit a deterministic procedure for deciding
whether or not two mixed expressions are equivalent.
In order to state our completeness theorem, we need a few definitions. We say that two mixed
ACI
expressions e1 and e2 are equal up to ACI properties, written e1 = e2 , if e1 and e2 are syntactically
equal, up to the associativity, commutativity, and idempotence of +. That is, e1 and e2 are equal
up to ACI properties if the following three rewriting rules can be applied to subexpressions of e1 to
obtain e2 :
e + (f + g) = (e + f ) + g
e+f =f +e
e + e = e.
Given a relation R̂ between mixed expressions, we define an induced relation R̂ACI as follows:
ACI
ACI
e1 R̂ACI e2 if and only if there exists e′1 , e′2 such that e1 = e′1 , e2 = e′2 , and e′1 R̂e′2 .
We define a syntactic bisimulation between two mixed expressions e1 and e2 having the same
type B → ∅ (for some B ⊆ B) to be a family R̂ = hR̂A iA∈℘(B) of relations such that
(1) for all mixed expressions e, e′ , if eR̂A e′ , then ⊢ e : A → ∅ and ⊢ e′ : A → ∅,
17

(2) eR̂B e′ ,
(3) for all mixed expressions e, e′ , if eR̂∅e′ , then ǫ̂(e) = ǫ̂(e′ ), and for all p ∈ P, D̂p (e)R̂BACI D̂p (e′ ),
and
ACI
′
(4) for all mixed expressions e, e′ , if eR̂A e′ (for A 6= ∅), then for all l ∈ lit(A), D̂l (e)R̂A\{base
(l)} D̂l (e ).

A syntactic bisimulation resembles a bisimulation, but is defined over mixed expressions, rather
than over mixed languages. The next theorem shows that any two equivalent mixed expressions are
related by a finite syntactic bisimulation, that is, a syntactic bisimulation R̂ where the number of
pairs in each relation R̂A is finite.
Theorem 7.1: For all mixed expressions e1 , e2 , of type A → ∅, M (e1 ) = M (e2 ) if and only if
there exists a finite syntactic bisimulation between e1 and e2 .
Proof: (⇐) It is easy to check that a syntactic bisimulation R̂ induces a bisimulation R such that
e1 R̂A e2 if and only if M (e1 )RA M (e2 ). The result then follows by Corollary 3.9.
(⇒) We first show how to construct, for every mixed expression e with ⊢ e : Ae → Be , a finitestate automaton M = (hSA iA∈℘(B)S, hδA iA∈℘(B) ) with transition functions δ∅ : S∅ × P → SB and
(for A 6= ∅) δA : SA × lit(A) → A∈℘(B) SA , satisfying the conditions
(1) δA (s, l) ∈ SA\{base(l)} ,

(2) the states of SA are mixed expressions having type A → Be ,
(3) e is a state of SAe ,
ACI

(4) if δ∅(s1 , p) = s2 , then D̂p (s1 ) = s2 , and
ACI

(5) if δA (s1 , l) = s2 , then D̂l (s1 ) = s2 .
We define the automaton by induction on the structure of e. The cases for 0, 1, p, l are straightforward. We focus on the remaining cases:
Case e = e1 + e2 : Assume by induction that we have automata M1 , M2 for e1 and e2 . Define:
SA = {f1 + f2 : f1 ∈ S1,A , f2 ∈ S2,A }
δ∅(f1 + f2 , p) = δ∅(f1 , p) + δ∅(f2 , p)
δA (f1 + f2 , l) = δ1,A (f1 , l) + δ2,A (f2 , l), for A 6= ∅, l ∈ lit(A).
Case e = e1 · e2 : Let ⊢ e1 : A1 → B1 . Assume by induction that we have automata M1 ,M2 for

18

e1 and e2 . Define:
P

SA = {f · e2 +

P

t·g+

δ∅(f






g :

g∈G

(t,g)∈E

f ∈ S1,A , E ⊆ Tests(A → B1 ) × S2,B1 , G ⊆ S2,A }
P
g, p) =
· e2 +
g∈G
P
δ2,∅(g, p) if B = ∅, ǫ̂(f ) = 1
δ1,∅(f, p) · e2 + δ2,∅(e2 , p) +
g∈G
P
δ2,∅(g, p)
otherwise
δ1,∅(f, p) · e2 +
g∈G

P
g, l) =
t·g+
δA (f · e2 +
g∈G
(t,g)∈E

P
P

δ2,A (g, l)
if base(l) ∈ A \ B1
δ1,A (f, l) · e2 +
Dl (t) · g +



g∈G
(t,g)∈E

P
P


 δ1,A (f, l) · e2 +
δ2,A (g, l) if base(l) 6∈ A ∪ B1
t · δ2,B1 (g, l) +
P

g∈G

(t,g)∈E

if base(l) ∈ B1



δ1,A (f,


P l) · e2 + T̂ (f ) · δ2,B
P1 (e2 , l)+


δ2,A (g, l)
t
·
δ
(g,
l)
+

2,B
1

g∈G

(t,g)∈E

for A 6= ∅, l ∈ lit(A).

Case e = e∗1 : Let ⊢ e1 : A1 → A1 . Assume by induction that we have an automaton M1 for e1 .
Define:

P
∗

f · e∗1 : γ ∈ {0, 1}, F ⊆ S1,A1 } if A = A1
 {γ · e1 +
f
∈F
P
SA =
otherwise
f · e∗1 : F ⊆ S1,A }

 {
f ∈F
P
f · e∗1 , p) =
δ∅(γ · e∗1 +
f ∈F
P
P
ǫ̂(f ) · δ1,∅(e, p) · e∗1 ,
δ1,∅(f, p) · e∗1 +
γ · δ1,∅(e1 , p) · e∗1 +
f ∈F

f ∈F

for A = A1
X
X
δ∅(
f · e∗1 , p) =
δ1,∅(f, p) · e∗1 , for A 6= A1 ,
f ∈F

f ∈F

f · e∗1 , l) =
f ∈F
P
P
ǫ̂(f ) · δ1,A (e, l) · e∗1 ,
δ1,A (f, l) · e∗1 +
γ · δ1,A (e1 , l) · e∗1 +

δA (γ ·

e∗1

+

P

f ∈F

f ∈F

for A 6= ∅, A = A1 , l ∈ lit(A)
X
X
δA (
f · e∗1 , l) =
δ1,A (f, l) · e∗1 , for A 6= ∅, A 6= A1 , l ∈ lit(A).
f ∈F

f ∈F

It is straightforward (if tedious) to verify that the resulting automaton satisfies properties (1)-(5)
given above.
This completes the construction of the finite state mixed automaton corresponding to e.
Given equivalent mixed expressions e1 and e2 of type A → ∅, a finite syntactic bisimulation
R̂ can be constructed as follows. First, construct the automata M1 and M2 corresponding to e1 and
19

e2 . Then, initialize R̂ to contain the pair (e1 , e2 ), and iterate the following process: for every (e, e′ )
in R̂, add the pairs (δ1,B (e, x), δ2,B (e′ , x)) (where e, e′ have type B → ∅), for all x. Perform this
iteration until no new pairs are added to R̂. This must terminate, because there are finitely many
pairs of states (e, e′ ) with e in M1 and e′ in M2 . It is straightforward to check that R̂ is a syntactic
bisimulation, under the assumption that M (e1 ) = M (e2 ).
The procedure described in the proof of Theorem 7.1 can in fact be easily turned into a procedure
for deciding if two mixed expressions are equivalent. To perform this decision, construct R̂, and
verify that at all pairs of states (e, e′ ) in R̂, ǫ̂(e) = ǫ̂(e′ ). If this verification fails, then the two mixed
expressions are not equivalent; otherwise, they are equivalent.
The bisimulation in Section 6 is indeed a bisimulation induced by a syntactic bisimulation on
the mixed expressions α and β.

8 Conclusions and Future Work
We believe that proofs of equivalence between mixed expressions such as α and β via bisimulation
are in general more easily derived than ones obtained through a sound and complete axiomatization
of KAT. Given two equivalent mixed expressions, we can exhibit a bisimulation using the purely
mechanical procedure underlying Theorem 7.1: use the derivative operators to construct a finite
bisimulation in which the two expressions are paired. In contrast, equational reasoning typically
requires creativity.
The “path independence” of a mixed automaton (condition A2) gives any mixed automaton
a certain form of redundancy. This redundancy persists in the definition of bisimulation, and is
the reason why a pseudo-bisimulation, a seemingly weaker notion of bisimulation, gives rise to
a bisimulation. An open question is to cleanly eliminate this redundancy; a particular motivation
for doing this would be to make proofs of expression equivalence as simple as possible. Along
these lines, it would be of interest to develop other weaker notions of bisimulation that give rise to
bisimulations; pseudo-bisimulations require a sort of “fixed variable ordering” that does not seem
absolutely necessary.
Another issue for future work would be to give a class of expressions wider than our mixed expressions for which there are readily understandable and applicable rules for computing derivatives.
In particular, a methodology for computing derivatives of the KAT expressions defined by Kozen
[1997] would be nice to see. Intuitively, there seems to be a tradeoff between the expressiveness
of the regular expression language and the simplicity of computing derivatives (in the context of
KAT). Formal work towards understanding this tradeoff could potentially be quite useful.

Acknowledgments
The authors wish to thank Dexter Kozen for helpful comments on a draft of this paper, as well
as the anonymous referees who helped improve the presentation of the results. The second author was supported by NSF under grant CTC-0208535, by ONR under grants N00014-00-1-03-41
and N00014-01-10-511, and by the DoD Multidisciplinary University Research Initiative (MURI)
program administered by the ONR under grant N00014-01-1-0795.

20

References
Brzozowski, J. A. (1964). Derivatives of regular expressions. Journal of the ACM 11(4), 481–
494.
Conway, J. H. (1971). Regular Algebra and Finite Machines. London, UK: Chapman and Hall.
Hopcroft, J. E. and J. D. Ullman (1979). Introduction to Automata Theory, Languages, and Computation. Addison Wesley.
Kaplan, D. (1969). Regular expressions and the equivalence of programs. Journal of Computer
and Systems Sciences 3, 361–386.
Kleene, S. C. (1956). Representation of events in nerve nets and finite automata. In C. E. Shannon
and J. McCarthy (Eds.), Automata Studies, pp. 3–41. Princeton, NJ: Princeton University
Press.
Kozen, D. (1994). A completeness theorem for Kleene algebras and the algebra of regular events.
Information and Computation 110, 366–390.
Kozen, D. (1997). Kleene algebra with tests. Transactions on Programming Languages and Systems 19(3), 427–443.
Kozen, D. (1998). Typed Kleene algebra. Technical Report 98-1669, Computer Science Department, Cornell University.
Kozen, D. (1999). On Hoare logic and Kleene algebra with tests. In Proceedings of the Conference on Logic in Computer Science (LICS’99), pp. 167–172. IEEE Computer Society Press.
Kozen, D. (2002). On Hoare logic, Kleene algebra, and types. In Scope of Logic, Methodology,
and Philosophy of Science: Volume 1 of the 11th Int. Congress Logic, Methodology and
Philosophy of Science, Cracow, August 1999, Volume 315 of Studies in Epistemology, Logic,
Methodology, and Philosophy of Science, pp. 119–133. Kluwer.
Kozen, D. (2003). Automata on guarded strings and applications. Matématica Contemporânea 24, 117–139.
Kozen, D. and F. Smith (1996). Kleene algebra with tests: Completeness and decidability. In
Proceedings of the 10th Workshop on Computer Science Logic (CSL’96), Volume 1258 of
Lecture Notes in Computer Science, pp. 244–259. Springer-Verlag.
Rutten, J. J. M. M. (1998). Automata and coinduction (an exercise in coalgebra). In Proceedings
of CONCUR’98, Volume 1466 of Lecture Notes in Computer Science, pp. 193–217.
Rutten, J. J. M. M. (1999). A note on coinduction and weak bisimilarity for while programs.
Theoretical Informatics and Applications (RAIRO) 33, 393–400.
Rutten, J. J. M. M. (2000). Universal coalgebra: a theory of systems. Theoretical Computer
Science 249(1), 3–80.
Salomaa, A. (1966). Two complete axiom systems for the algebra of regular events. Journal of
the ACM 13(1), 158–169.

21

