Logical Methods in Computer ScienceVol. 3 (4:11) 2007, pp. 1–36
www.lmcs-online.org

Submitted
Published

Jul. 21, 2007
Nov. 19, 2007

GENERIC TRACE SEMANTICS VIA COINDUCTION ∗ICHIRO HASUO a , BART JACOBS b , AND ANA SOKOLOVA ca

Institute for Computing and Information Sciences, Radboud University Nijmegen, the Netherlands
and Research Institute for Mathematical Sciences, Kyoto University, Japan
URL: http://www.cs.ru.nl/~ichirobInstitute for Computing and Information Sciences, Radboud University Nijmegen, the Netherlands
URL: http://www.cs.ru.nl/~bartc

Department of Computer Sciences, University of Salzburg, Austria
e-mail address: anas@cs.uni-salzburg.at
Abstract. Trace semantics has been defined for various kinds of state-based systems,
notably with different forms of branching such as non-determinism vs. probability. In thispaper we claim to identify one underlying mathematical structure behind these “trace
semantics,” namely coinduction in a Kleisli category. This claim is based on our technicalresult that, under a suitably order-enriched setting, a final coalgebra in a Kleisli category
is given by an initial algebra in the category Sets. Formerly the theory of coalgebras
has been employed mostly in Sets where coinduction yields a finer process semantics ofbisimilarity. Therefore this paper extends the application field of coalgebras, providing a
new instance of the principle “process semantics via coinduction.”

1. Introduction
Trace semantics is a commonly used semantic relation for reasoning about state-based
systems. Trace semantics for labeled transition systems is found on the coarsest edge of thelinear time-branching time spectrum [57]. Moreover, trace semantics is defined for a variety
of systems, among which are probabilistic systems [49].
In this paper we claim that these various forms of “trace semantics” are instances ofa general construction, namely coinduction in a Kleisli category. Our point of view here iscategorical, coalgebraic in particular. Hence this paper demonstrates the abstraction power
1998 ACM Subject Classification: F.3.1, F.3.2, G.3.
Key words and phrases: coalgebra, category theory, trace semantics, monad, Kleisli category, process
semantics, non-determinism, probability.
∗
Earlier versions [16, 17] of this paper have been presented at the 1st International Conference on Algebra
and Coalgebra in Computer Science (CALCO 2005), Swansea, UK, September 2005, and at the 8th International Workshop on Coalgebraic Methods in Computer Science (CMCS 2006), Vienna, Austria, March2006.
aSupported by PRESTO research promotion program, Japan Science and Technology Agency.
b
Also part-time at Technical University Eindhoven, the Netherlands.
c
Supported by the Austrian Science Fund (FWF) project P18913-N15.

l

LOGICAL METHODSIN COMPUTER SCIENCEc
DOI:10.2168/LMCS-3 (4:11) 2007

CC

I. Hasuo, B. Jacobs, and A. Sokolova
Creative Commons

2

I. HASUO, B. JACOBS, AND A. SOKOLOVA

of categorical/coalgebraic methods in computer science, uncovering basic mathematicalstructures underlying various concrete examples.
1.1. “Trace semantics” in various contexts. First we motivate our contribution throughexamples of various forms of “trace semantics.” Think of the following three state-based,branching systems.
x

a

y

x′

b

a[ 31 ]

X

a[1]

z′

a[ 13 ]13y′a[ 12 ]
1
2

X

A context-free grammar(for Peano Arithmetic)
Terminal symbols:
0, s
Non-terminal symbol: T
Generation rules:
T→0
T → sT(1.1)• The first one is a non-deterministic system with a special state X denoting successful
termination. To its state x we can assign its trace set:
tr(x) = {a, ab, abb, . . . } = ab∗ ,(1.2)

that is, the set of the possible linear-time behavior (namely words) that can arise throughan execution of the system.1 In this case the trace set tr(x) is also called the accepted
language; formally it is defined (co)recursively by the following equations. For an arbitrarystate x,hi ∈ tr(x) ⇐⇒ x → X(1.3)
aa · σ ∈ tr(x) ⇐⇒ ∃y. ( x → y ∧ σ ∈ tr(y) )Here hi denotes the empty word; σ = a1 a2 . . . an is a word.
• The second system has a different type of branching, namely probabilistic branching.
a[1/3]

Here x′ −→ y ′ denotes: at the state x′ , a transition to y ′ outputting a occurs withprobability 1/3. Now, to the state x′ , we can assign its trace distribution:

hi 7→ 31 , a 7→ 13 · 21 , a2 7→ 13 · 12 · 12 , · · ·tr(x) =,
(1.4)
n
an 7→ 13 · 21 , · · ·that is, the probability distribution over the set of linear-time behavior.2 Its formal(corecursive) definition is as follows.
tr(x)(hi) = Pr(x → X) ,Patr(x)(a · σ) =y∈X Pr(x → y) · tr(y)(σ) ,(1.5)

where Pr(. . . ) denotes the probability of a transition.
• The third example can be thought of as a state-based system, with non-terminal symbols
as states. It is non-deterministic because a state T has two possible transitions. It isnatural to call the following set of parse-trees its “trace semantics.”


•
•

 •
s
•
s
•
0
·
·
·
tr(T) =0s•01The infinite trace abω is out of our scope here: we will elaborate this point later in Section 4.2.
2Here again, we do not consider the infinite trace aω 7→ 1/3.

GENERIC TRACE SEMANTICS VIA COINDUCTION

3

It is again a set of “linear-time behavior” as in the first example, although the notionof linear-time behavior is different here. Linear-time behavior—that is, what we observe
after we have resolved all the non-deterministic branchings in the system—is now a parsetree instead of a word.
1.2. Coalgebras and coinduction. In recent years the theory of coalgebras has emerged
as the “mathematics of state-based systems” [25,26,47]. In the categorical theory of coalgebras, an important definition/reasoning principle is coinduction: a system (identified witha coalgebra c : X → F X) is assigned a unique morphism behc into the final coalgebra.
F (behc )FXFZ∼= final

c

X

behc

Z

The success of coalgebras is largely due to the fact that, when Sets is taken as the basecategory, the final coalgebra semantics is fully abstract with respect to the conventionalcdnotion of bisimilarity: for states x and y of coalgebras X → F X and Y → F Y ,behc (x) = behd (y)⇐⇒x and y are bisimilar.

This is the case for a wide variety of systems (i.e. for a variety of functors F ), hence
coinduction in Sets captures bisimilarity.
However, there is not so much work so far that captures other behavioral equivalences(coarser than bisimilarity) by the categorical principle of coinduction. The current work—
capturing trace semantics by coinduction in a Kleisli category—therefore extends the application field of the theory of coalgebras.
1.3. Our contributions. Our technical contributions are summarized as follows. Assume
that T is a monad on Sets which has a suitable order structure; we shall denote its Kleisli
category by Kℓ(T ).
• Trace semantics via coinduction in a Kleisli category. Commutativity of the coinduction
diagram
FX

F (trc )X

FZ∼= finalc
trc

Z

in Kℓ(T ),the Kleisli category for T(1.6)

is shown to be equivalent to the conventional recursive definition of trace semantics suchas (1.3) and (1.5). This is true for both trace set semantics (for non-deterministic systems)
and trace distribution semantics (for probabilistic systems). The induced arrow trc thus
gives (conventional) trace semantics for a system c.
• Identification of the final coalgebra in a Kleisli category. We show thatan initial algebra in Sets
coincides witha final coalgebra in Kℓ(T ).

4

I. HASUO, B. JACOBS, AND A. SOKOLOVA

In particular, the final coalgebra in Rel is the initial algebra in Sets, because the category
Rel of sets and relations is a Kleisli category for a suitable monad. This coincidence
happens in the following two steps:- the initial algebra in Sets lifts to a Kleisli category, due to a suitable adjunction-lifting
result;- in a Kleisli category we have initial algebra-final coalgebra coincidence. Here we use theclassical result by Smyth and Plotkin [51], namely limit-colimit coincidence which isapplicable in a suitably order-enriched category.
Note the presence of two parameters in (1.6): a monad T and an endofunctor F , bothon Sets. The monad T specifies the branching type of systems. We have three leading
examples:3• the powerset monad P modeling non-deterministic or possibilistic branching;• the subdistribution monad D
X
DX = {d : X → [0, 1] |d(x) ≤ 1}x∈X

modeling probabilistic branching; and• the lift monad L = 1+( ) modeling system with exception (or deadlock, non-termination).
The functor F specifies the transition type of systems: our understanding of “transition
type” shall be clarified by the following examples.
• In labeled transition systems (LTSs) with explicit termination—no matter if they are
non-deterministic or even probabilistic—a state either- terminates (x → X), ora- outputs one symbol and moves to another state (x → x′ ),in one transition. This “transition type” is expressed by the functor F X = 1 + Σ × X,
where Σ is the output alphabet and 1 = {X}.
• In context-free grammars (CFGs) as state-based systems, a state evolves into a sequenceof terminal and non-terminal symbols in a transition. The functor
F X = (Σ + X)∗
with Σ being the set of terminal symbols, expresses this transition type.
Clear separation of branching and transition types is important in our generic treatment oftrace semantics. The transition type F determines the set of linear-time behavior (which isc
in fact given by the initial F -algebra in Sets). We model a system by a coalgebra X → F X
in the Kleisli category Kℓ(T )—see (1.6)—where F is a suitable lifting of F in Kℓ(T ). By
the definition of a Kleisli category we will easily see the following bijective correspondence.
Xc

F X in Kℓ(T )X

c

T F X in Sets

Hence our system—a function of the type X → T F X—first resolves a branching of type T
and then makes a transition of type F . Many branching systems allow such representation
so that our generic coalgebraic trace semantics applies to them.
3Other examples include the monad X 7→ (N ∪ {∞})X for multisets, the monad X 7→ [0, ∞]X for realvaluations, and the monad X 7→ P(M × ) with a monoid M for timed systems (cf. [29]). These monads
can be treated in a similar way as our leading examples. We leave out the details.

GENERIC TRACE SEMANTICS VIA COINDUCTION

5

1.4. Generic theory of traces and simulations. In the study of coalgebras as ‘categorical presentation of state-based systems’, there are three ingredients playing crucial roles:
coalgebras as systems; coinduction yielding process semantics; and morphisms of coalgebras
as behavior-preserving maps. In this paper we study the first two in a Kleisli category.
What about morphisms of coalgebras?
In [14] this question is answered by identifying lax/oplax morphisms of coalgebras ina Kleisli category as forward/backward simulations. Use of traces and simulations is acommon technique in formal verification of systems (see e.g. [41]): a desirable property
is expressed in terms of traces; and then a system is shown to satisfy the property byfinding a suitable simulation. Therefore this paper, together with [14], forms an essential
part of developing a “generic theory of traces and simulations” using coalgebras in a Kleisli
category. The categorical genericity—especially the fact that we can treat non-deterministic
and probabilistic branching in a uniform manner—is exploited in [19] to obtain a simulationbased proof method for a probabilistic notion of anonymity for network protocols. Currently
we are investigating how much more applicational impact can be brought about by ourgeneric theory of traces and simulations.
1.5. Testing and trace semantics. Since the emergence of the theory of coalgebras, thesignificance of modal logics as specification languages has been noticed by many authors.
This is exemplified by the slogan in [36]: ‘modal logic is to coalgebras what equational
logic is to algebras’. Inspired by coalgebras on Stone spaces and the corresponding modal
logic, recent developments [5, 6, 31, 32, 34, 37, 45] have identified the following situation as
the essential mathematical structure underlying modal logics for coalgebras.
P
F op

Cop

⊤

A

M

δ

together with M P =⇒ P F op

S op

In fact, it is noticed in [45] that such a situation not only hosts a modal logic but also a moregeneral notion of testing (in the sense of [53, 57], also called testing scenarios). Therefore
we shall call the above situation a testing situation.
In the last technical section of the paper we investigate coalgebraic trace semantics forthe special case T = P (modeling non-determinism) from this testing point of view. First,
we present some basic facts on testing situations, especially on the relationship between the
induced testing equivalence and the final coalgebra semantics. These two process equivalences are categorically presented as kernel pairs, which enables a fairly simple presentationof the theory of coalgebraic testing. In addition, we observe that the coinduction scheme
in the Kleisli category Kℓ(P) gives rise to a canonical testing situation, in which the set oftests is given by an initial F -algebra.
The material on testing in the last section has not been presented in the earlier versions [16, 17] of this paper.
1.6. Organization of the paper. In Section 2 we observe that a coalgebra in a Kleisli
category is an appropriate “denotation” of a branching system, when we focus on trace
semantics. In Section 3 we present our main technical result that an initial algebra in Sets
yields a final coalgebra in Kℓ(T ). The relationship to axiomatic domain theory—which
employs similar mathematical arguments—is also discussed here. Section 4 presents someexamples of the use of coinduction in Kℓ(T ) and argues that the coinduction principle is6

I. HASUO, B. JACOBS, AND A. SOKOLOVA

a general form of trace semantics. In Section 5 we review the preceding material from thetesting point of view.
2. Coalgebras in a Kleisli category
In the study of coalgebras as “categorical presentations of state-based systems,” thecategory Sets of sets and functions has been traditionally taken as a base category (seee.g. [25, 47]). An important fact in such a setting is that bisimilarity is often captured bycoinduction.4
However, bisimilarity is not the only process equivalence. In some applications one
would like coarser equivalences, for example in order to abstract away internal branching
structures. One of such coarser semantics, which has been extensively studied, is trace
equivalence. For example, the process algebra CSP [21] has trace semantics as its operationalmodel. Trace equivalence is coarser than bisimilarity, as the following classic example of“trace-equivalent but not bisimilar” systems illustrates.
y
a x a
•
b

a

•

•

•

b

c

•

c

•

•

It is first noticed in [46] that the Kleisli category for the powerset monad is an appropriate base category for trace semantics for non-deterministic systems. This observation ispursued further in [16, 17, 24]. In [15] it is recognized that the same is true for the subdistribution monad for probabilistic systems. The current paper provides a unified framework
which yields those preceding results, in terms of Cppo-enrichment of a Kleisli category; see
Section 2.3. In this section we first aim to justify the use of coalgebras in a Kleisli category.
2.1. Monads and Kleisli categories. Here we recall the relevant facts about monads
and Kleisli categories. For simplicity we exclusively consider monads on Sets.
A monad on Sets is a categorical construct. It consists of• an endofunctor T on Sets;
ηX• a unit natural transformation η : id ⇒ T , that is, a function X → T X for each set X
satisfying a suitable naturality condition; andµX• a multiplication natural transformation µ : T 2 ⇒ T , consisting of functions T 2 X →TX
with X ranging over sets.
The unit and multiplication are required to satisfy the following compatibility conditions.
TX

ηT X

id

T 2X
µX

TX

T ηX

id

TX

T 3X

T µX

µT X

T 2X

T 2X
µX

µX

TX

See [3, 42] for the details.
4Non-examples include LTSs with unbounded branching degree. They are modeled as coalgebras for
F X = P(Σ × X). Lambek’s Lemma readily shows that this choice of F does not have a final coalgebra in∼=
Sets, because it would imply an isomorphism Z →P(Σ × Z) which is impossible for cardinality reasons.

GENERIC TRACE SEMANTICS VIA COINDUCTION

7

The monad structures play a crucial role in modeling “branching.” Intuitively, theunit η embeds a non-branching behavior as a trivial branching (with only one possibility
to choose). The multiplication µ “flattens” two successive branchings into one branching,
abstracting away internal branchings:
x
x
•
µ
y
•
(2.1)
−
7
→
y
•
z
z
•
The following examples will illustrate how this flattening phenomenon is a crucial featureof trace semantics.
In this paper we concentrate on the three monads mentioned in the introduction: L, P
and D.
• The lift monad L = 1 + ( )—where we denote 1 = {⊥} with ⊥ meaning deadlock —hasa standard monad structure induced by a coproduct. For example, the multiplicationµL
X : 1 + 1 + X → 1 + X carries x ∈ X to itself and both ⊥’s to ⊥.
• The powerset monad P has a unit given by singletons and a multiplication given byunions. The monad P models non-deterministic branching: the “flattening” in (2.1)
corresponds to the following application of the multiplication of P.



µP
X

PPX
{x, y}, {z}PX{x, y, z}

The monad P’s action on arrows (as a functor) is given by direct images: for f : X → Y ,the function Pf : PX → PY carries a subset u ⊆ X to the subset {f (x) | x ∈ u} ⊆ Y .
• The subdistribution monad D has a unit given by the Dirac distributions.
D
ηX

X

DX


x

x 7→ 1x′ 7→ 0 (for x′ 6= x)



Its multiplication is given by multiplying the probabilities along the way. That is,
X
µD
(ξ)
=
λx.
ξ(d) · d(x) ,Xd∈DX

which models “flattening” of the following kind.
1/2
1/3

•

2/3

•

•

1/2
1

x
y
z

µ

•

7−→

1/6

x

1/6

y ,

2/3

z

that is, x 7→ 1/2
y 7→ 1/2[z 7→ 1]



7→ 1/3 
7→ 2/3

µ

7−→




x 7→ 1/6
 y 7→ 1/6  .
z 7→ 2/3

The monad D’s action on arrows (as a functor) is given as a suitable adaptation of“direct images.”
Namely, for f : X → Y , the function Df : DX → DY carries d ∈ DXP
to [y 7→ x∈f −1 (y) d(x)] ∈ DY .

8

I. HASUO, B. JACOBS, AND A. SOKOLOVA

Given any monad T , its Kleisli category Kℓ(T ) is defined as follows. Its objects are theobjects of the base category, hence sets in our consideration. An arrow X → Y in Kℓ(T ) is
the same thing as an arrow X → T Y in the base category, here Sets.
X

Y in Kℓ(T )X

T Y in Sets

Identities and composition of arrows are defined using the unit and the multiplication of T .
Moreover, there is a canonical adjunctionJ

Sets

Kℓ(T )

⊥
K

f

(2.2)

η ◦f

Y
such that J carries X −→ Y in Sets to X −→Y in Kℓ(T ). See [3, 42] for details.
The relevance in this paper is that a Kleisli category can be thought of as a category
where the branching is implicit. For example, an arrow X → Y in the Kleisli category
Kℓ(P) is a function X → PY hence a “non-deterministic function.” When T = D, thenby writing X → Y in the Kleisli category we mean a function with probabilistic branching.
Moreover, composition of arrows in Kℓ(T ) is given byfg

X −→ Y −→ Z

in Kℓ(T )

=

f

Tg

µ

Z
X −→ T Y −→ T 2 Z −→TZ

in Sets;

that is, making one transition (by g) after another (by f ), and then flattening (by µZ ). Forfgexample, this general definition instantiates as follows when T = D. For X → Y → Z,P(g ◦ f )(x)(z) = y∈Y f (x)(y) · g(y)(z) .

Remark 2.1. Our use of the sub-distribution monad instead of the distribution monadX
D=1 (X) = {d : X → [0, 1] |d(x) = 1}
x∈X

needs some justification. Looking at the trace distribution (1.4), one sees that the probabilities add up only to 2/3 and not to 1; this is because the infinite trace (namely aω 7→ 1/3)
are not present. Therefore in this example, although the state-based system can be modeled
as a coalgebra in the category Kℓ(D=1 ), its trace semantics can only be expressed as anarrow in Kℓ(D).
When a system is modeled as a coalgebra in Kℓ(D), a state may have a (sub)distribution
over possible transitions which adds up to less than 1. In that case the missing probability
can be understood as the probability for deadlock.
Technically, we use the monad D instead of D=1 because we need the minimum element(a bottom) so that the Kleisli category becomes Cppo-enriched (Theorem 3.3). A bottom
is available for D as the zero distribution [x 7→ 0], but not for D=1 .
2.2. Lifting functors by distributive laws. In this paper a state-based system is presented as a coalgebra X → F X in Kℓ(T ), where F : Kℓ(T ) → Kℓ(T ) is a lifting of
F : Sets → Sets. This lifting F 7→ F is equivalent to a distributive law F T ⇒ T F .
The rest of this section elaborates on this point.

GENERIC TRACE SEMANTICS VIA COINDUCTION

9

Various kinds of state-based, branching systems are expressed as a function of the formc
X → T F X with T a monad (for branching type) and F a functor (for transition type).
The following examples are already hinted at in the introduction.
c• For T = P and F = 1 + Σ × , a function X → T F X is an LTS with explicit termination.
For example, consider the following systemcXxP(1 + Σ × X)
{X, (a1 , x1 ), (a2 , x2 )}where X is the element of 1.5 Then the state x can make three possible transitions,aanamely: x → X (successful termination), x →1 x1 , and x →2 x2 , when written in aconventional way.
• By replacing T = P by D, but keeping F the same, we obtain a probabilistic system suchas the one in the middle of (1.1). For example,c

X

D(1 + Σ × X)
(a, y ′ ) 7→ 1/3
 (a, z ′ ) 7→ 1/3 .
X 7→ 1/3x′c• For T = P and F = (Σ + )∗ , a function X → T F X is a CFG with Σ the terminalalphabet (but without finiteness conditions e.g. on the state space). See [16] for moredetails.
cc
All these systems are modeled by a function X → T F X, hence an arrow X → F X inKℓ(T ). Our question here is: is c a coalgebra in Kℓ(T )? In other words: is the functor F
on Sets also a functor on Kℓ(T )?
Hence, to develop a generic theory of traces in Kℓ(T ), we need to lift F to a functor F
on Kℓ(T ). A functor F is said to be a lifting of F if the following diagram commutes. HereJ is the left adjoint in (2.2).
Kℓ(T )FJ

Sets

Kℓ(T )

(2.3)

J
F

Sets

The following fact is presented in [43]; see also [39, 40]. Its proof is straightforward.
Lemma 2.2. A lifting F of F is in bijective correspondence with a distributive law
λ : F T ⇒T F . A distributive law λ is a natural transformation which is compatible with T ’s
monad structure, in the following way.
FX

F ηX
ηF X

FTX
λX

TFX

F T 2XλT X

TFTX

5Note that the singleton 1 = {X} here in F = 1 + Σ ×

T 2F X
µF X

F µX

FTX

T λX

λX

TFX

has a different interpretation from 1 = {⊥} in
T = L = 1 + . The intuition is as follows. On the one hand, when an execution hits successful termination
X, it yields its history of observations as its trace. On the other hand, when an execution hits deadlock ⊥then it yields no trace no matter what is the history before hitting ⊥. This distinction will be made formal
in Example 4.3.

10

I. HASUO, B. JACOBS, AND A. SOKOLOVA

A distributive law λ induces a lifting F as follows. On objects: F X = F X. Given f :X → Y in Kℓ(T ), we need an arrow F f : F X → F Y in Kℓ(T ). Recall that f is a function
X → T Y in Sets; one takes F f to be the arrow which corresponds to the functionFfλY
F X −→ F T Y −→TFY

in Sets .

A distributive law specifies how a transition (of type F ) “distributes” over a branching(of type T ). Let us look at an example. For T = P and F = 1 + Σ × (the combination
for LTSs with explicit termination), we have the following distributive law.
1 + Σ × (PX)X
(a, S)For example,
x
λ
y −
7 → •
z

λX

P(1 + Σ × X){X}
(a, x) | x ∈ S

a

x
 λ 
that isa, {x, y, z} 7−→ (a, x), (a, y), (a, z) ,yazwhere waving arrows ; denote branchings.
Throughout the paper we need the global assumption that a functor F has a lifting F
on Kℓ(T ), or equivalently, that there is a distributive law λ : F T ⇒ T F . Now we present
some sufficient conditions for existence of λ. In most examples one of these conditions holds.
First, take T = P, in which case we have Kℓ(P) ∼= Rel, the category of sets and binary
relations. We can provide the following condition that uses relation liftings, whose definition
is found [24].
•aaLemma 2.3 (From [24]). Let F : Sets → Sets be a functor that preserves weak pullbacks.
Then there exists a distributive law λ : F P ⇒ PF given by
λX (u) = v ∈ F X | (v, u) ∈ RelF (∈X ) ,where u ∈ F PX and RelF (∈X ) ⊆ F X × F PX is the F -relation lifting of the membership
relation ∈X .

In fact, the functor F : Rel → Rel induced by this distributive law carries an arrow
R : X → Y in Kℓ(P)—which is a binary relation between X and Y —to its F -relation
lifting RelF (R). That is,
F R = RelF (R) : F X −→ F Y(2.4)∼
in Kℓ(P) = Rel.
Now let us consider a monad T which is not P. When a monad T is commutative and afunctor F is shapely, we can provide a canonical distributive law. The class of such monads
and functors is wide and all the examples in this paper are contained.
• A commutative monad [33] is intuitively a monad whose corresponding algebraic theory
has only commutative operators. We exploit the fact that a commutative monad isequipped with an arrow called double strength
dstX,Y : T X × T Y −→ T (X × Y )for any sets X and Y ; the double strength must be compatible with the monad structureof T in an obvious way.

GENERIC TRACE SEMANTICS VIA COINDUCTION

11

Our three examples of monads are all commutative, with the following double strengths.
(u, v) if u ∈ X and v ∈ Y,
L
dstX,Y (u, v) =⊥if u = ⊥ or v = ⊥,(2.5)
P
dstX,Y (u, v) = u × v ,dstD
X,Y (u, v) = λ(x, y). u(x) · v(y) .
• The family of shapely functors [27]6 on Sets is defined inductively by the following BNF
notation:`
F ::= id | Σ | F1 × F2 | i∈I Fi ,where Σ denotes the constant functor into an arbitrary set Σ. Notice that taking infinite
product is not allowed, nor exponentiation to the power of an infinite set. This is in orderto ensure that we find an initial F -algebra as a suitable ω-colimit—see Proposition A.1.
Lemma 2.4. Let T : Sets → Sets be a commutative monad, and F : Sets → Sets a shapely
functor. Then there is a distributive law λ : F T ⇒ T F .
Proof. The construction of a distributive law is done inductively on the construction ofshapely F .
• If F is the identity functor, then the λ is the identity natural transformation T ⇒ T .
• If F is a constant functor, say X 7→ Σ, then λ is the unit ηΣ : Σ → T Σ at Σ ∈ Sets.
• If F = F1 × F2 we use induction in the form of distributive laws λFi : Fi T ⇒ T Fi for
i ∈ {1, 2} to form the composite:
λF1 ×λF2

dst

T F1 X × T F2 X
T (F1 X × F2 X) .
F1 T X × F2 T X`• If F is a coproduct i∈I Fi then we use laws λFi : Fi T ⇒ T Fi for i ∈ I in:`[T (κi )◦λFi ]i∈Ii∈I Fi (T X)`
T ( i∈I Fi X) .

It is straightforward to check that such λ is natural and compatible with the monad structure.
We have provided some sufficient conditions for a distributive law to exist, that is,for a functor F to be lifted to Kℓ(T ). This does not mean the results in the sequel holdexclusively for commutative monads and shapely functors.
2.3. Order-enriched structures of Kleisli categories. The notion of branching naturally involves a partial order: one branching is bigger than another if the former offers“more possibilities” than the latter. Formally, this order appears as the Cppo-enriched
structure of a Kleisli category. It plays an important role in the initial algebra-final coalgebra coincidence in Section 3.1.
A Cppo-enriched category C is a category where:• Each homset C(X, Y ) carries a partial order ⊑ as in
⊑

g

X

Y

f
6Shapely functors here are called polynomial functors by some authors, although other authors allow

infinite powers or the powerset construction.

12

I. HASUO, B. JACOBS, AND A. SOKOLOVA

which makes C(X, Y ) an ω-cpo with a bottom. This means:- for an increasing ω-chain of arrows from X to Y ,f0 ⊑ f1 ⊑ . . .

X −→ Y ,:F

there exists its join n<ω fn : X → Y ;- for any X and Y there exists a bottom arrow ⊥X,Y : X → Y which is the minimum inC(X, Y ).
• Moreover, composition of arrows is continuous as a function C(X, Y )×C(Y, Z) → C(X, Z).
This means that the following joins are preserved:7


F
F
F
F
g◦
=
and
n<ω fnn<ω (g ◦ fn )n<ω fn ◦ h =n<ω (fn ◦ h) .

Note that composition need not preserve bottoms (i.e. it is not necessarily strict).
This is in fact an instance of a more general notion of V-enriched categories where V is thecategory Cppo of pointed (i.e. with ⊥) cpo’s and continuous (but not necessarily strict)functions. See [7, 28, 38] for more details on enriched category theory, and [1] on cpo’s anddomain theory.
Lemma 2.5. For our three examples L, P and D of a monad T , the Kleisli category Kℓ(T )is Cppo-enriched. Moreover, composition of arrows is left-strict: ⊥ ◦ f = ⊥.
The left-strictness of composition will be necessary later.
Proof. Notice first that a set T Y for T ∈ {L, P, D} carries a cpo structure with ⊥. The set
LY = {⊥} + Y carries the flat order with a bottom:
y

y′

y ′′

···

⊥
embodying the idea that ⊥ denotes non-termination or deadlock —in contrast to X forsuccessful termination. The set PY carries an inclusion order; in DY we define d ⊑ e if
d(y) ≤ e(y) for each y ∈ Y . The bottom element in DY is the zero distribution [y 7→ 0]:
this belongs to the set DY because D is the sub-distribution monad.
The cpo structure of a homset Kℓ(T )(X, Y ) comes from that of T Y in a pointwisemanner:⊑g

XY

if and only if∀x ∈ X. f (x) ⊑T Y g(x) .

f

It is laborious but straightforward to show that composition in Kℓ(T ) is continuous andleft-strict.
7This component-wise preservation of joins is equivalent to the continuity of the composition function.

See [1, Lemma 3.2.6].

GENERIC TRACE SEMANTICS VIA COINDUCTION

13

We are concerned with coalgebras X → F X in the category Kℓ(T ), which we assume is
Cppo-enriched. Hence it comes natural to require that functor F is somehow compatible
with the Cppo-enriched structure of Kℓ(T ). The obvious choice is to require that F isa Cppo-enriched functor (see e.g. [7]), i.e. F is locally continuous. It means that for an
increasing ω-chain fn : X → Y , we haveGGF(fn ) =(F fn ) .
n<ωn<ωThis is indeed the assumption chosen in axiomatic domain theory. We will come back tothis point later in Section 3.3. However, for our later purpose, we only need the weakercondition of local monotonicity: f ⊑ g implies F f ⊑ F g.
For a monad T = {L, P, D} and a shapely functor F (recall Lemma 2.4), the lifted F
is indeed locally continuous. We emphasize again that this does not mean our results in
Section 3 hold exclusively for shapely functors.
Lemma 2.6. Let F be a shapely functor and T ∈ {L, P, D}. The lifting F : Kℓ(T ) → Kℓ(T )induced by Lemma 2.4 is locally continuous.
Proof. By induction on the construction of shapely functors.
• F = id, the identity functor. Then F = id which satisfies the condition.
• F = Σ, a constant functor. Then F maps every arrow to the identity map on Σ in Kℓ(T ).
This is obviously locally continuous.
• F = F1 × F2 . First notice that, for f : X → Y in Kℓ(T ), we obtain F f as the following
composite in Sets.
F1 X × F2 X

F1 f ×F2 f

Ff

T F1 Y × T F2 Y
dstF1 Y,F2 Y

T (F1 Y × F2 Y )Because the order in Kℓ(T )(F X, F Y ) is pointwise, it suffices to show the following: dst :T X × T Y → T (X × Y ) is a continuous map between cpo’s. It is easy to check that thisis indeed` the case. See (2.5).
• F = j∈J Fj . For f : X → Y in Kℓ(T ), we obtain the map F f as the composite`[T κj ]j∈J ◦ j∈J Kℓ(Fj )(f ) in Sets. Since the order on the homset is pointwise, it suffices`
to show that each T κj : T Fj Y → T ( j∈J Fj Y ) is continuous. This is easy.
3. Final coalgebra in a Kleisli category
In this section we shall prove our main technical result: the initial F -algebra in Sets
yields the final F -coalgebra in Kℓ(T ). It happens in the following two steps: first, theinitial algebra in Sets is lifted to the initial algebra in Kℓ(T ); second we have the initial
algebra-final coalgebra coincidence in Kℓ(T ). For the latter we use the classical result [51]of limit-colimit coincidence. This is where the Cppo-enriched structure of Kℓ(T ) plays arole.
In the proof we use two standard constructions: initial/final sequences [2] and limitcolimit coincidence [51]. The reader who is not familiar with these constructions is invited
to look at Appendices A.1 and A.2 where we briefly recall them.

14

I. HASUO, B. JACOBS, AND A. SOKOLOVA

Remark 3.1. The proof of our main theorem (Theorem 3.3) can be simplified if we suitably
strengthen the assumptions. First, if we assume local continuity of the lifted functor F(instead of local monotonicity that is assumed in our main theorem), then the initial algebrafinal coalgebra coincidence follows from a standard result in axiomatic domain theory; see
Section 3.3. Furthermore, for the special case T = P in which case Kℓ(P) ∼= Rel, the initial
algebra-final coalgebra coincidence is almost obvious due to the duality Rel ∼= Relop ; see
Section 3.2.
3.1. The initial algebra in Sets is the final coalgebra in Kℓ(T ). First, it is standard
that an initial algebra in Sets is lifted to an initial algebra in Kℓ(T ). Such a phenomenon is
studied for instance in [11,44] in the context of combining datatypes (modeled by an initial
algebra) and effectful computations (modeled by a Kleisli category). For this result we do
not need an order structure.
Proposition 3.2. Let T be a monad and F be a endofunctor, both on a category C. Assume
that we have a distributive law F T ⇒ T F —or equivalently, we have a lifting F on Kℓ(T ).
∼= A in C, then
If F has an initial algebra α : F A →Jα = ηA ◦ α :F A −→ Ain Kℓ(T )is an initial F -algebra. Here J is the canonical Kleisli left adjoint as in (2.2).
We will use an instance of this result for C = Sets.
Proof. It follows from [20, Theorem 2.14] that a distributive law lifts the canonical Kleisli
adjunction to an adjunction between the categories Alg(F ) and Alg(F ) of algebras.
J′

Alg(F )⊥C⊥
K

Alg(F )J

Kℓ(T )The left adjoint J ′ preserves the initial object (see e.g. [42]).
Second, we use the initial algebra-final coalgebra coincidence in Kℓ(T )—which holds ina suitable order-enriched setting—to identify the final coalgebra in Kℓ(T ). This is our main
theorem.
Theorem 3.3 (Main theorem). Assume the following:(1) A monad T on Sets is such that its Kleisli category Kℓ(T ) is Cppo-enriched andcomposition in Kℓ(T ) is left-strict.
(2) For an endofunctor F on Sets, we have a distributive law λ : F T ⇒ T F . Equivalently,
F has a lifting F on Kℓ(T ). Moreover, the lifting F is locally monotone.
(3) The functor F preserves ω-colimits in Sets, hence has an initial algebra via the initial
sequence (see Proposition A.1).
∼= A yields a final F -coalgebra in Kℓ(T ) by
Then the initial F -algebra α : F A →(Jα)−1 = J(α−1 ) = ηF A ◦ α−1 :A −→ F A

in Kℓ(T ) .

GENERIC TRACE SEMANTICS VIA COINDUCTION

15

We first present the main line of the proof. Some details are provided in the form ofsubsequent lemmas. Note that the assumptions are satisfied by T ∈ {L, P, D} and shapely
F ; see Lemmas 2.5 and 2.4.
Proof. By the assumption (3) we obtain the initial algebra via the initial sequence in Sets.
In Sets···αnF n−1 ¡

F n0

F n+1 0F αn−1

αn+1

···

A

(colimit)

α ∼
= α−1

F αn

FA

(3.1)

(colimit)

Here 0 = ∅ ∈ Sets is initial and ¡ : 0 → X is the unique arrow from 0 to an arbitrary X.
We apply the functor J : Sets → Kℓ(T ) to the whole diagram. Since J is a left adjoint it
preserves colimits: hence the two cocones in the following diagram are both colimits again.
In Kℓ(T )···JαnJF n−1 ¡

F n0

Jαn+1

···

F n+1 0JF αn−1A(colimit)Jα ∼= Jα−1

JF αn

FA

(3.2)

(colimit)

The ω-chain in this diagram is in fact the initial sequence for the functor F (Lemma 3.4)
because, for example, a left adjoint J preserves initial objects. Moreover the lower cone is
the image of the upper cone under F ; see the diagram (2.3). Hence the diagram (3.2) isequal to the following one. Recall that F X = F X on objects.
In Kℓ(T )
···

Jαn
F

n−1

¡

n

F 0

F

n+1

0

A
···

= Jα−1Jα ∼F Jαn
F Jαn−1∼(colimit)

Jαn+1

FA

(3.3)

(colimit)= A is an initial F -algebra. This can be seen as
Thus Proposition A.1 yields that Jα : F A →a more concrete proof of Proposition 3.2.
Now we show the initial algebra-final coalgebra coincidence in Kℓ(T ). This is done byreversing all the arrows in (3.3) and transforming the diagram into the one of the final
sequence and its limits.
n
We notice (Lemma 3.6) that each arrow F ¡ in the initial sequence is an embedding(Definition A.4). Hence the limit-colimit coincidence Theorem A.8 says that every arrowin the diagram is an embedding. Note that Jα and Jα−1 , inverse to each other, form anembedding-projection pair.
By taking the corresponding projections—they are uniquely determined (Lemma A.5)
and are denoted by ( )P —we obtain the next diagram. The limit-colimit coincidence
Theorem A.8 says that the two resulting cones are both limits. It is also obvious that the16

I. HASUO, B. JACOBS, AND A. SOKOLOVA

whole diagram commutes.
In Kℓ(T )···(Jαn )P

(F

n−1

¡ )P

n

F 0

F

n+1

A

(limit)(Jα)P∼= (Jα−1 )P(Jαn+1 )P

···

0

(3.4)

(F Jαn )P(F Jαn−1FA)P(limit)The ω op -chain here is indeed a final sequence: Lemma 3.5 shows—using the assumption(1) on left-strictness—that 0 is also final in Kℓ(T ), and according to Lemma 3.6 we havenn(F ¡ )P = F ! where ! : X → 0 is the unique arrow to the final object 0 in Kℓ(T ). As toP
the lower cone we have F Jαn = F (Jαn )P by Lemma 3.7.
Hence the diagram (3.4) is equal to the following one, showing the final sequence for
F , its limit (the upper one) and that limit mapped by F (the lower one) which is again alimit.
In Kℓ(T )···(Jαn )P
F

n−1

!

n

F 0

F

n+1

A

(Jαn+1 )P

···

0

Jα−1

(limit)
∼
= Jα

(3.5)

F (Jαn )PF (Jαn−1FA)P(limit)By Proposition A.2 we conclude that Jα−1 is a final F -coalgebra.
In the remainder of this section the lemmas used in the above proof are presented. We
rely on the same assumptions as in Theorem 3.3.
Lemma 3.4. The ω-chain in the diagram (3.2) is indeed the initial sequence for F . Thatis, we have for each n < ω,n
JF n ¡ Sets = F ¡ Kℓ(T ) : JF n 0 −→ JF n+1 0 in Kℓ(T ),where ¡ Sets : 0 → F 0 in Sets and ¡ Kℓ(T ) : 0 → F 0 in Kℓ(T ) denote the unique maps.

Proof. By induction on n. For n = 0 the two maps are equal due to the initiality of J0 = 0
in Kℓ(T ). For the step case we use the commutativity JF = F J of (2.3).
Lemma 3.5. The empty set 0 is both an initial and a final object in Kℓ(T ).
In particular, this implies that the object T 0 is final in Sets.
Proof. The functor J : Sets → Kℓ(T ) preserves initial objects since it is a left adjoint.
Therefore 0 = J0 is initial in Kℓ(T ). Finality follows essentially from the left-strictness
assumption: for each set X there exists at least one arrow X → 0 in Kℓ(T ), for example⊥X,0 . To show the uniqueness of such an arrow, take an arbitrary arrow f : X → 0 inKℓ(T ). Recalling that the bottom map ⊥0,0 : 0 → 0 is also the identity arrow in Kℓ(T )because of initiality, we obtain(∗)

f = id ◦ f = ⊥0,0 ◦ f = ⊥X,0 ,where the compositions are taken in Kℓ(T ) and the equality marked by (∗) holds by leftstrictness of composition.

GENERIC TRACE SEMANTICS VIA COINDUCTION

17nLemma 3.6. Each arrow F ¡ in the initial sequence for F , as in the diagram (3.3), is anembedding. Its corresponding projection is given by
n

F ¡

P

n

n

=F !

in

F

n

F

n

!

F n0

F n+1 0 .
¡n

Proof. We show that (F ¡ , F ! ) is an embedding-projection pair for all n < ω. We havenn
F ! ◦ F ¡ = id because ! ◦ ¡ = id. For the other half we havennnF ¡ ◦ F ! = F (¡ ◦ !)n

= F (⊥0,F 0 ◦ ! )initiality of 0 in Kℓ(T )n= F (⊥F 0,F 0 )composition is left-strictn

F is locally monotone.
⊑ F (id) = id
P
Lemma 3.7. We have F Jαn = F (Jαn )P . Hence the lower cone in the diagram (3.4)
is the image of the upper cone under F .
indeed form an embedding-projection
Proof. It is easy to check that F Jαn , F (Jαn )Ppair. Therein we use the monotonicity of F ’s action on arrows.
3.2. Simpler proof in Kℓ(P) ∼= Rel. When T = P we have the self-duality
Op

:

∼
=

Kℓ(P)op −→ Kℓ(P) .

This is because of the following bijective correspondence between functions
XYf

PY in Setsf∨

PX in Sets

given by f ∨ (y) = {x ∈ X | y ∈ f (x)}. Recalling Kℓ(P) ∼= Rel, this mapping f 7→ f ∨corresponds to taking the opposite relation.
Due to this “global” duality Kℓ(P) ∼= Kℓ(P)op , the proof of Theorem 3.3 is drasticallyopsimplified for T = P. It essentially relies on the lifted self duality Alg(F ) ∼= Alg(F ),where the latter is isomorphic to (Coalg(F ))op . We do not need here an order structure ofKℓ(P) nor local monotonicity of F .
Theorem 3.8. Let F : Sets → Sets be a functor which preserves weak pullbacks, andF : Kℓ(P) → Kℓ(P) be its lifting induced by relation lifting (Lemma 2.3). Then the initial
F -algebra in Sets yields the final F -coalgebra in Kℓ(P).
Proof. We have the following situation because of the self-duality of Kℓ(P).
J

Sets
F

⊥
K

Kℓ(P)
F

Op op
∼
=

Kℓ(P)opF

op

18

I. HASUO, B. JACOBS, AND A. SOKOLOVA∼=
The adjunction J ⊣ K and the isomorphism Op : Kℓ(P)op →Kℓ(P) lift to those between
the categories of algebras.
J′

Alg(F )

⊥

Sets

⊥
K

Alg(F )

(Op ′ )op
∼
=

Alg(F

Kℓ(P)

Op op
∼
=

Kℓ(P)op

J

op

)

∼
=

(Coalg(F ))op∼=
Indeed, J ⊣ K lifts due to Proposition 3.2; the lifted isomorphism Op ′ : Alg(F ) →Alg(Fis because of the following commutativity:

Kℓ(P)op
F

Op

)

Kℓ(P)

op

Kℓ(P)op

op

F

(3.6)

Kℓ(P)

Op

which is because: F R = RelF (R) (see (2.4)); and taking relation liftings is compatible withop
opposite relations (i.e. RelF (Rop ) = (RelF R)op , see [22]). Moreover the category Alg(F )is obviously isomorphic to (Coalg(F ))op .
Therefore the initial object in Alg(F ) is carried to that in (Coalg(F ))op , hence thefinal object in Coalg(F ).
For monads such as T = D a “global” self-duality Kℓ(T ) ∼= Kℓ(T )op is not available.
Instead, in the proof of Theorem 3.3, we exploit the “partial” duality which holds between
the colimit/limit of the initial/final sequence.
3.3. Related work: axiomatic domain theory. The initial algebra-final coalgebra coincidence is heavily exploited in the field of axiomatic domain theory, e.g. in [9, 12, 13, 50].
There, categories which have coinciding initial algebra and final coalgebra for each endofunctor are called algebraically compact categories. They draw special attention as suitable“categories of domains” for denotational semantics of datatype construction. The relevancecomes as follows.
Let C be a “category of domains.” We think of an object of the category C as a type.
A “recursive” datatype constructor—a prototypical example is (X, Y ) 7→ Y X —is presented
as a bifunctor G : Cop × C → C. Note the presence of both covariance and contravariance.
We expect that such a category C has a canonical fixed point Fix G such that∼= Fix G ,G(Fix G, Fix G) →which models the recursive type determined by the datatype constructor G. Freyd [12]showed that if C is algebraically compact, then we can construct such a fixed point as asuitable initial algebra; moreover this fixed point is shown by Fiore [9] to be a canonical
one in a suitable sense. The rough idea here is that the covariant part of G is taken care ofby an initial algebra; the contravariant part is by a final coalgebra; the initial algebra-final
coalgebra coincidence yields a fixed point of overall G.
Typical examples of algebraically compact categories are enriched over Cppo or one ofits variants. This conforms the traditional use of the word “domain” for certain cpo’s (e.g.
in [1]).

GENERIC TRACE SEMANTICS VIA COINDUCTION

19

Although we utilize the initial algebra-final coalgebra coincidence result in Kℓ(T ), we are
not so much interested in algebraic compactness of Kℓ(T ). This is because our motivation isdifferent from that of axiomatic domain theory. In studying trace semantics for coalgebras,
we need not deal with every endofunctor on Kℓ(T ), but only such an endofunctor F which
is a lifting of F : Sets → Sets.
In a different context of functional programming, the work [44] also studies initial
algebras and final coalgebras in a Kleisli category. The motivation there is to combine datatypes and effects. More specifically, an initial algebra and a final coalgebra support thefold and the unfold operators, respectively, used in recursive programs over datatypes. A
computational effect is presented as a monad, and its Kleisli category is the category ofeffectful computations.
The difference between [44] and the current work is as follows. In [44], the original
category of pure functions is already algebraically compact; the paper studies the conditions for the algebraic compactness to be carried over to Kleisli categories. In contrast, inthe current work, it is a monad—with a suitable order structure, embodying the essenceof “branching”—which yields the initial algebra-final coalgebra coincidence on a Kleisli
category; the coincidence is not present in the original category Sets.
3.3.1. Local continuity vs. local monotonicity. In axiomatic domain theory, Cppo-enrichedcategories are said to be algebraically compact because, “in a 2-category setting” [13], every
endofunctor has an initial algebra and a final coalgebra. Concretely this means: “every
locally continuous functor.”
In this spirit, we could have made a stronger assumption of F ’s local continuity in
Theorem 3.3 instead of local monotonicity. If we do so, in fact, the proof of Theorem 3.3
becomes much simpler: the following proposition (Lemma in [13, p.98]) immediately yields
the initial algebra-final coalgebra coincidence for a locally continuous F .
Proposition 3.9 ( [13]). Let D be a Cppo-enriched category whose composition is left∼= B,
strict, and G : D → D be a locally continuous endofunctor. An initial algebra β : GB →∼= GB.
if it exists, yields a final coalgebra β −1 : B →Proof. Given a coalgebra d : Y → GY , the function
Φ : D(Y, B) −→ D(Y, B) ,f 7−→ β ◦ Gf ◦ d

is continuous due to the local continuity of G. Hence it has the least fixed point
this proves existence of a morphism from d to β −1 .
GY

GB

d

∼
= β −1YBnn<ω Φ (⊥);

F

Now we shall show its uniqueness. Assume that g : Y → B is a morphism of coalgebras
as above, that is, Φ(g) = g. Similarly to Φ, we define a function Ψ : D(B, B) → D(B, B) as

20

I. HASUO, B. JACOBS, AND A. SOKOLOVA

the one which carries h : B → B to β ◦ Gh ◦ β −1 . We have
F n
F n
g
⊥
composition is left-strict, so ⊥ ◦ g = ⊥n Φ (⊥) =n Φ (B → B → Y )
F= n Ψn (⊥) ◦ Φn (g)Φn (⊥ ◦ g) = Ψn (⊥) ◦ Φn (g), by induction

F n
F n 
=
composition is continuousn Ψ (⊥) ◦n Φ (g)F n
F n= n Φ (g)n Ψ (⊥) = id, (∗)=g

Φ(g) = g by assumption.

Here (∗) holds because n Ψn (⊥), being a fixed point for Ψ, is the unique morphism ofalgebras from β to β. This shows that the morphism g must be the least fixed point of Φ.
F

For our main Theorem 3.3 we can do with only local monotonicity of the lifted functor
F , by taking a closer look at the initial/final sequences. However at this stage it is not clear
how much we gain from this generality: up to now we have not found an example where
the functor F is only locally monotone (and not locally continuous).
4. Finite trace semantics via coinduction
In this section we shall further illustrate the observation that the principle of coinduction, when employed in Kℓ(T ), captures trace semantics of state-based systems. As we haveshown in the previous section, an initial algebra in Sets constitutes the semantic domain,i.e. is a final coalgebra in Kℓ(T ). Viewing an initial algebra as the set of well-founded terms(such as finite words or finite-depth parse trees), this fact means that the “trace semantics”
induced by coinduction is inevitably finite, in the sense that it captures only finite behavior.
Here we will elaborate on this finiteness issue as well.
4.1. Trace semantics by coinduction. As we have seen in Section 2.2 various types ofstate-based systems allow their presentation as coalgebras X → F X in a Kleisli category
Kℓ(T ). For example,• LTSs with explicit termination, with T = P and F = 1 + Σ × ;• probabilistic LTSs (also called generative probabilistic transition systems in [52, 58]) with
explicit termination, with T = D and F = 1 + Σ × ;• context-free grammars with T = P and F = (Σ + )∗ .
The main observation underlying this work is the following. If we instantiate the parameters
T for branching type

andF for transition typein the coinduction diagram
FX

F (trc )X

FA∼= Jα−1c
trc

in Kℓ(T )

(4.1)

A

with one of the above choices, then the commutativity of the diagram is equivalent to thecorresponding (conventional) definition of trace semantics in Section 1.1. Therefore we claimthat the diagram (4.1) is the mathematical principle underlying various “trace semantics,”
no matter if it is “trace set” (non-deterministic) or “trace distribution” (probabilistic).

GENERIC TRACE SEMANTICS VIA COINDUCTION

21

Corollary 4.1 (Trace semantics for coalgebras). Assume that T and F are such as in∼= A is an initial F -algebra in Sets. Given a coalgebra c : X →Theorem 3.3, and α : F A →T F X in Sets, we can assign a function
trc : X −→ T A

in Sets

which is, as an arrow X → A in Kℓ(T ), the unique one making the diagram (4.1) commute.
We shall call this function trc the (finite) trace semantics for the coalgebra c.
Example 4.2. As further illustration we give details for the choice of parameters T = P
and F = 1 + Σ × . This is the suitable choice to deal with the first system in (1.1).
Now the coinduction diagram looks as follows. Recall that an initial F -algebra is carriedby the set Σ∗ of finite words.
1+Σ×X

1+Σ×trc∼= J([nil,cons])−1
Σ∗

c

X

1 + Σ × Σ∗trc

in Kℓ(P)(4.2)

It assigns, to a system c, a function trc : X → P(Σ∗ ) which carries a state x ∈ X to theset of finite words on Σ which can possibly arise as an execution “trace” of c starting fromx. The commutativity states equality of two arrows X ⇉ 1 + Σ × Σ∗ in Kℓ(P), that is,functions X ⇉ P(1 + Σ × Σ∗ ). Let us denote these functions by
u = (1 + Σ × trc ) ◦ c (up, then right),

v = J([nil, cons])−1 ◦ trc(right, then up).

For each x ∈ X, the following conditions—derived straightforwardly by definition of composition of Kℓ(P), lifting of the functor 1 + Σ × , etc.—specify u and v’s value at x, as asubset of 1 + Σ × Σ∗ .
X ∈ u(x) ⇐⇒ X ∈ c(x)(a, σ) ∈ u(x) ⇐⇒ ∃x′ ∈ X. (a, x′ ) ∈ c(x) ∧ σ ∈ trc (x′ )X ∈ v(x) ⇐⇒ hi ∈ trc (x)(a, σ) ∈ v(x) ⇐⇒ a · σ ∈ trc (x)Commutativity of (4.2) amounts to u = v; this gives the condition (1.3).
From a different point of view we can also express that as follows: finality of the∼= 1 + Σ × Σ∗ in (4.2) ensures that the conventional recursive definition (1.3)
coalgebra Σ∗ →uniquely determines a function trc : X → P(Σ∗ ). Hence trc is well-defined.
An easy consequence of the recursive definition (1.3) is
a1 . . . an ∈ trc (x)⇐⇒∃x1 , . . . , xn ∈ X.

aan
x →1 · · · →xn → X .

Therefore every trace a1 . . . an ∈ trc (x) has termination X implicit at its tail. In particular,
the set trc (x) is not necessarily prefix-closed: a1 . . . an an+1 . . . an+m ∈ trc (x) does not imply
a1 . . . an ∈ trc (x).
Example 4.3. Let us take T = L (the lift monad) and F = 1 + Σ ×ccoalgebra X → L(1 + Σ × X) in Sets is a system which can• get into a deadlock (c(x) = ⊥ where L = {⊥} + ),• successfully terminate (c(x) = X where F = {X} + Σ × ), or• output a letter from Σ and move to the next state (c(x) = (a, x′ )).

. In this case a22

I. HASUO, B. JACOBS, AND A. SOKOLOVA

By examining trace semantics for such systems, we shall formally put the difference between
the computational meanings of the two elements, ⊥ and X.
The coinduction diagram (4.1) instantiates to the same diagram as (4.2), but now in the
category Kℓ(L). Easy calculation shows that its commutativity amounts to the following
condition. The function
X

trc

L(Σ∗ ) = {⊥} + Σ∗

in Setssatisfies, for each x ∈ X,
trc (x) = hi⇐⇒ c(x) = X ,trc (x) = a · σ ⇐⇒ ∃x′ ∈ X. c(x) = (a, x′ ) ∧ trc (x′ ) = σ ,trc (x) = ⊥⇐⇒ c(x) = ⊥ or ∃x′ ∈ X. c(x) = (a, x′ ) ∧ trc (x′ ) = ⊥ .

(4.3)

Here σ ∈ Σ∗ is a word in Σ.
For the systems under consideration, we can think of three different kinds of possible
executions.
aan• An execution eventually hitting X, that is, x →1 · · · →xn → X. By the condition (4.3) ityields a word trc (x) = a1 . . . an as its trace.
aan• An execution eventually hitting ⊥, that is, x →1 · · · →xn → ⊥. By the third line of(4.3) we see that trc (xn ) = ⊥; moreover trc (xn−1 ) = · · · = trc (x) = ⊥. It properly reflects
our intuition that a state x that eventually goes into deadlock does not yield a finite (orterminating) trace.
aa• An execution not hitting X nor ⊥, that is, x →1 x1 →2 · · · . In this case, the only possible
solution of the “recursive equation” (4.3) is trc (x) = trc (x1 ) = · · · = ⊥. The intuition
here is: a state leading to livelock does not yield a finite trace.
4.2. Infinite traces. The trace semantics obtained via coinduction (Corollary 4.1) assigns,
to each state x ∈ X, “a set of” (if T = P) or “a distribution over” (if T = D) elements of
the initial algebra A. Elements of A are thought of as possible linear behavior of the systemdetermined by the transition type (i.e. the functor F ).
Now the intuition is that an initial F -algebra A consists of the well-founded (or finitedepth) terms and a final F -coalgebra Z consists of the possibly non-well-founded (or infinitedepth) terms. For example,• for F = 1 + Σ × , A = Σ∗ consists of all the finite words, and Z = Σ∞ = Σ∗ + Σω isaugmented with streams, i.e. infinite words;• for F = (Σ + )∗ , A is the set of finite-depth skeletal parse trees (see [16]), and Z
additionally contains infinite-depth ones;• for F = Σ × which models LTSs without explicit termination, A = 0 and Z = Σω .
Therefore our trace semantics X → T A only takes account of finite, well-founded lineartime behavior but not infinite ones. This is why the trace set (1.2) does not contain abω ;and also why we have been talking about LTSs with explicit termination—otherwise thefinite trace semantics is always empty.
Designing a coalgebraic framework to capture possibly infinite trace semantics is themain aim of [24]. The work is done exclusively in a non-deterministic setting and the main
result reads as follows.

GENERIC TRACE SEMANTICS VIA COINDUCTION

23

Theorem 4.4 (Possibly infinite trace semantics for coalgebras, [24]). Let F be a shapely∼= F Z be a final coalgebra in Sets. The coalgebra
functor on Sets, and ζ : Z →in Kℓ(P)Jζ : Z −→ F Z

is weakly final: that is, given a coalgebra c : X → F X, there is a morphism from c to Jζ
but the morphism is not necessarily unique.
FX

F (tr∞
c )

X

FZ

∼
= Jζ

c
tr∞
c

in Kℓ(P)(4.4)

Z

Still there is a canonical choice tr∞
c among such morphisms, namely the one which is
maximal with respect to the inclusion order. We shall call the function tr∞
c : X → PZ thepossibly-infinite trace semantics for c.
Note here that, when we take F = 1 + Σ × and T = P (the choice for LTSs withtermination), commutativity of (4.4) boils down to exactly the same conditions as (1.3):
hi ∈ tr∞c (x)a · σ ∈ tr∞
c (x)

a

∃y. ( x → y ∧ σ ∈ tr∞c (y) ).
(4.5)
∼
∼
=
=
∞
∞
Weak finality of Σ → 1+Σ×Σ (corresponding to Z → F Z in (4.4)) means the following.
The recursive definition (4.5)—although it looks valid at the first sight—does not uniquely∞∞determine the infinite trace map tr∞
c : X → P(Σ ). Instead, the map trc is the maximal
one among those which satisfy (4.5).
As an example take the first system in (1.1). We expect its possibly-infinite trace map
X → P(Σ∞ ) to be such that x 7→ ab∗ + abω and y 7→ b∗ + bω . Indeed this satisfies (4.5) andis moreover the maximal. However, the function x 7→ ab∗ and y 7→ b∗ —this is actually thefinite trace X → P(Σ∗ ) embedded along Σ∗ ֒→ Σ∞ —also satisfies (4.5). In fact, [16, Section
5] shows a general fact that such an embedding of the finite trace map is the minimal one
among those morphisms which make the diagram (4.4) commute.
The coalgebraic characterization (Theorem 4.4) of possibly-infinite trace semantics is
not yet fully developed. In particular the current proof of Theorem 4.4 (in [24]) is fairly
concrete and a categorical principle behind it is less clear than the one behind finite traces.
Consequently the result’s applicability is limited: we do not know whether the result holds
in a probabilistic setting; or whether it holds for any weak-pullback-preserving functor F .
⇐⇒x → X,⇐⇒

5. Trace semantics as testing equivalence
In this section we will observe that, in a non-deterministic setting, the coalgebraic finite
trace semantics (i.e. coinduction in Kℓ(P)) gives rise to a canonical testing situation inwhich a test is an element of the initial F -algebra A in Sets. Here F specifies the transition
type, just as before. The notion of testing situations (Definition 5.1) and its variants haveattracted many authors’ attention in the context of coalgebraic modal logic; our aim here isto demonstrate genericity and pervasiveness of the notion of testing situations by presenting
an example which is not much like modal logic (that is, propositional logic plus modality).
In Section 5.1 we introduce the notion of testing situations and investigate some of
their general properties. Our main concern there is the comparison between two processequivalences, namely testing equivalence and equivalence modulo final coalgebra semantics.

24

I. HASUO, B. JACOBS, AND A. SOKOLOVA

We present the equivalences categorically as suitable kernel pairs; this makes the arguments
simple and clean. In Section 5.2 we present the canonical testing situation for trace semantics. Moreover we show that it is expressive: the testing captures final coalgebra semantics,
which is now trace semantics.
5.1. Testing situations. Recent studies [5, 6, 32, 35, 37, 45] on coalgebra and modal logic
have identified (variants of) the following categorical situation as the essential underlying
structure. Following [45], we prefer using a more general term “testing”: it subsumes “modal
logic” in the following sense. We learn properties of a system through pass or failure oftests; modal logic constitutes a special case where tests are modal formulas.
Definition 5.1. A testing situation is the following situation of a contravariant adjunction
S op ⊣ P and two endofunctors F, M
P
F op

Cop

⊤

A

M

(5.1)

S op

plus a “denotation” natural transformation δ : M P ⇒ P F op : Cop → A, which consists ofδX
P F X in A.
arrows M P X −→Note that the denotation δ is a parameter: the same “syntax for tests” M : A → A canhave different interpretations with different δ.
The requirements in Definition 5.1 are the same as in [32, 45]. They are what we needto compare two process semantics, namely testing equivalence—which arises naturally fromthe concept of testing—and final coalgebra semantics.8 We shall explain each ingredient’srole, using the well-established terminology of modal logic.
• The endofunctor F : C → C makes Coalg(F ) the category of “systems,” or “Kripke
models” in modal logic.
• The category A—typical examples being Bool of Boolean algebras or Heyt of Heyting
algebras—is that of “propositional logic.” The functor M specifies “modality”: modal
operators and axioms. Then Alg(M ) is the category of “modal algebras”; the initial∼=
M -algebra M L →L is a “modal logic” consisting of modal formulas, modulo logicalequivalence.
• The denotation δ specifies how the modality M is interpreted via transitions of type
F . This allows to give “Kripke semantics” for the modal logic: given a coalgebra (or a“Kripke model”) c : X → F X, interpretation J Kc of modal formulas therein is given by
the following induction.
MPX
ML
δX
initial ∼
=

PFX

(5.2)

Pc

L

J Kc

PX

8In fact we can be even more liberal: existence of a denotation δ can be replaced by existence of alifting P̂ : Coalg(F )op → Alg(M ) of P . The results in this section nevertheless hold in that case. The
latter condition (there is a lifting P̂ ) is strictly weaker than the former (there is a natural transformation
δ): obviously δ induces P̂ but not the other way round. Let C = ω op , A = ω, P = id, F = (1 + )op and
M = 2 + . Then both Coalg(F ) and Alg(M ) are the empty category hence P has the trivial lifting.
However there is no natural transformation M P X → P F op X.

GENERIC TRACE SEMANTICS VIA COINDUCTION

25• Why a right adjoint S of P op ? It allows us, via transposition, to assign a modal “theory”
to each state of a Kripke model.
J Kc

L
X

thc

PX
SL

in A

(S op ⊣ P )

(5.3)

in C

The theory thc (x) associated with a state x contains precisely the modal formulas that
hold at x.
Following the above intuition, we define the categorical notion of testing equivalence—twostates are testing-equivalent if they have the same modal theory.
Definition 5.2. Assume that we have a testing situation (5.1), and that C has finite limits.
c
On a coalgebra X → F X, the testing equivalence TestEqc is the kernel pair of the theory
map thc defined by (5.2) and (5.3). Equivalently,
TestEqc

hp1 ,p2 i

thc ◦π1

X ×X

thc ◦π2SL(5.4)

is an equalizer.
Similarly, we introduce the categorical notion of “equivalence modulo final coalgebra
semantics”; we shall call it FCS-equivalence for short.
∼=
Definition 5.3. Assume that there is a final F -coalgebra ζ : Z →F Z, and that C hascfinite limits. On a coalgebra X → F X, the FCS-equivalence FCSEqc is the kernel pair of
the unique map behc : X → Z induced by finality. Equivalently,
hq1 ,q2 i

FCSEqcbehc ◦π1

X ×X

behc ◦π2Z(5.5)

is an equalizer.
It is easily seen that the two “relations” TestEqc and FCSEqc on X are equivalence
relations in the sense of [23, Section 1.3]. That is, they satisfy the reflexivity, symmetry,
and transitivity conditions when the conditions are suitably formulated in categorical terms.
Now our concern is the comparison between two process semantics TestEqc and FCSEqc ,as subobjects of X × X. The following lemma is crucial for our investigation; in fact it isimportant for coalgebraic modal logic in general and appears e.g. as [32, Theorem 3.3].
Lemma 5.4. A morphism of F -coalgebras preserves theory maps. That is,
FX

Ff

c

X

d
f

X

FY
Y

implies

f

Y

thc
thd

SL

.

26

I. HASUO, B. JACOBS, AND A. SOKOLOVA

Proof. The following induction diagram proves P f ◦ J Kd = J Kc . Naturality of δ plays animportant role there.
ML

Ff

MPY

MP f

MPX

δY
initial ∼
=

PFY
Pd

L

J Kd

PY

δX
PFf
Pf

PFX
Pc

PX

.

Then the claim follows from naturality of the transposition (5.3).
We show that in a testing situation like (5.1), tests respect final coalgebra semantics.
That is, testing does not distinguish two FCS-equivalent states.
Proposition 5.5. Consider such a testing situation and equivalence relations as in Definictions 5.2 and 5.3. For any coalgebra X → F X we have an inclusion
FCSEqc ≤ TestEqc
of subobjects of X × X.
Proof. It suffices to show that the arrow hq1 , q2 i in (5.5) equates the parallel arrows in (5.4);
then the claim follows from universality of an equalizer.
thc ◦ π1 ◦ hq1 , q2 i = thc ◦ q1
= thζ ◦ behc ◦ q1(∗)

= thζ ◦ behc ◦ q2

due to (5.5)= thc ◦ q2(∗)

= thc ◦ π2 ◦ hq1 , q2 i .
Here (∗) is an instance of Lemma 5.4: behc is a morphism of coalgebras from c to the finalζ.
The converse TestEqc ≤ FCSEqc does not hold in general. For a fixed type of systems(i.e. for fixed F : C → C), we can think of logics with varying degree of expressive power;
this results in process equivalences with varying granularity. This view is systematicallypresented by van Glabbeek in [57] as the linear time-branching time spectrum—a categoricalversion of which we consider as an important direction of future work.
∼= TestEq that a modal logic (considered as a testing
It is when we have FCSEqc →csituation) is said to be expressive. Recall that FCSEqc usually coincides with bisimilarity if
C is Sets: in this case an expressive logic captures bisimilarity.
The following proposition states a (rather trivial) equivalent condition for a testing
situation to be expressive. For more ingenious sufficient conditions—which essentially relyon the transpose of δ being monic—see e.g. [32].
Proposition 5.6. Consider a testing situation as in Definitions 5.2 and 5.3. The testingcis expressive, that is, for any coalgebra X → F X we have∼=
TestEqc →FCSEqcas subobjects of X × X, if and only if the theory map thζ : Z → SL for the final coalgebra
is a mono.

GENERIC TRACE SEMANTICS VIA COINDUCTION

27

Proof. We first prove the “if” direction. In view of Proposition 5.5, it suffices to show that
hp1 , p2 i in (5.4) equalizes behc ◦ π1 and behc ◦ π2 (which proves TestEqc ≤ FCSEqc ).
thζ ◦ behc ◦ p1 = thc ◦ p1

by Lemma 5.4= thc ◦ p2
= thζ ◦ behc ◦ p2

due to (5.4)
by Lemma 5.4

We have behc ◦ p1 = behc ◦ p2 since thζ is a mono.
To prove the “only if” direction, first we observe that the FCS-equivalence on the final∼=
coalgebra ζ : Z →F Z is the diagonal relation: that is,behζ ◦π1

FCSEqζ
∼
=

Z ×Z

Z

behζ ◦π2hid,idi.
Z
This is because behζ = id : Z → Z. Now assume that thζ ◦ k = thζ ◦ l for k, l : Y ⇉ Z.
Universality of an equalizer TestEqζ induces a mediating arrow m in the following diagram.
behζ ◦π1

hk,li

Y

Z ×Z

behζ ◦π2hid,idim

TestEqζ∼=FCSEqζ∼=Z

Z

The whole diagram commutes since TestEqζ ∼= FCSEqζ (by assumption) and FCSEqζ ∼=Z(by the above observation), both as subobjects of Z × Z. This proves k = l.
Remark 5.7. The literature [5, 6] considers more restricted settings than the testing situations in Definition 5.1. There an adjunction S op ⊣ P is replaced by a dual equivalence of
categories, and a denotation δ is required to be a natural isomorphism. These additional
restrictions allow one to say more about the situations: logics are always expressive; themain concern of [6] is how to present an abstract modal logic M : A → A by concrete syntax. However, for our purpose in Section 5.2 the greater generality of our notion of testing
situations is needed.
5.2. Canonical testing for trace semantics in Kℓ(P). In this section we shall present
a canonical testing situation for coalgebras in Kℓ(P). We shall also show that the testing is“expressive,” in the sense that the testing captures final coalgebra semantics. The intuitionis as follows.
Trace semantics for non-deterministic systems assigns to each system c its “(finite) traceset” map trc : X → PA, where A carries an initial algebra in Sets. This suggests a natural
testing framework where: an element t of A is a test; a state x ∈ X of a system passes a
test t if and only if the trace set of x includes t (i.e. x |= t ⇐⇒ t ∈ trc (x)). An important
point here is that A, carrying an initial algebra in Sets, usually gives a well-founded syntax
for tests.9
We focus on a non-deterministic setting (i.e. T = P) in this section and leave a probabilistic one as future work. Although the above intuition is true in probabilistic settings
9Recall the construction of an initial algebra in Sets via the initial sequence (Proposition A.1). The set
A is the colimit (union in Sets) of the initial sequence 0 → F 0 → F 2 0 → · · · . Each F n 0 can be thought ofas the set of terms with depth ≤ n.

28

I. HASUO, B. JACOBS, AND A. SOKOLOVA

as well—where the 2-valued (pass/failure) observation scheme is replaced by the refined[0, 1]-valued one—we do not know yet how to extend the current material to probabilistic
settings. The difficulty is that the category Kℓ(D) is not self-dual, as opposed to Kℓ(P); see(5.6) below.
The canonical testing situation which captures finite trace semantics is the followingone.
Op

Kℓ(P)op
F

∼
=
Op

op

F

K

Kℓ(P)

Sets

⊤

op

(5.6)

J
∼

=
Here J ⊣ K is the canonical Kleisli adjunction. Recall the self duality Op : Kℓ(P)op →Kℓ(P) from Section 3.2. The denotation is given by (the components of) the distributive
law λ : F P ⇒ PF . The following lemma establishes naturality of the denotation.

Lemma 5.8. Let F : Sets → Sets be a functor which preserves weak pullbacks, and F be
λX
its lifting induced by the relation lifting (Lemma 2.3). Then the components F PX →PF Xof the corresponding distributive law λ also form a natural transformation
F ◦ K ◦ Op =⇒ K ◦ Op ◦ F

op: Kℓ(P)op −→ Sets .

Proof. The desired natural transformation is obtained from another natural transformation
λ′ : F K =⇒ KF : Kℓ(P) −→ Sets
which we describe in a moment, by post-composing the functor Op. That is, the desired
one is the composite
λ′ ◦Op(∗)

F KOp =⇒ KF Op = KOpF
or equivalently, in a 2-categorical presentation,
Kℓ(P)opF

op

Kℓ(P)op

Op
(∗)
Op

Kℓ(P)

K

Kℓ(P)

,

Sets
λ′

F

op

K

F

Sets .

Here the equality (∗) is the one in (3.6).
Now we describe the natural transformation λ′ . Its components are given by those of
λ; naturality of λ′ is an easy consequence of λ’s being a distributive law. Indeed, given anarrow f : X → Y in Kℓ(P), the following shows that the naturality square commutes.
KF f ◦ λX = µP
F Y ◦ PF f ◦ λX

definition of K= µP
F Y ◦ PλY ◦ PF f ◦ λX

definition of F= µP
F Y ◦ PλY ◦ λPY ◦ F Pf
= λY ◦ F µ P
Y ◦ F Pf

naturality of λ= λY ◦ F Kf

λ is compatible with the multiplication µP of P
definition of K

The previous lemma establishes that the situation (5.6) is indeed a testing situation as
defined in Definition 5.1.
In the previous Section 5.1, the use of testing situations is demonstrated through comparing testing equivalence and final coalgebra semantics, both described as suitable kernel

GENERIC TRACE SEMANTICS VIA COINDUCTION

29

pairs. Unfortunately this argument is not valid in the current situation (5.6), since thecategory Kℓ(P) does not have kernel pairs.
Still, we shall claim that the situation (5.6) is “expressive,” in the sense that final
coalgebra semantics is captured by testing. This claim is supported by the following fact:
in the current situation the two arrows trc and thc simply coincide. Therefore their kernel
relations—in any reasonable formalization—should coincide as well.
c

Proposition 5.9. Let X → F X be a coalgebra in Kℓ(P). In the testing situation (5.6),
the following arrows in Kℓ(P) coincide.
• trc : X → A, giving the final coalgebra (trace) semantics for c.
• thc : X → A, giving the testing semantics, i.e. the set of passed tests.
Therefore the testing is “expressive”: tests from an initial F -algebra captures trace semantics(which is via a final F -coalgebra).
Here A is the carrier of an initial F -algebra, hence that of a final F -coalgebra. Note that,in the general setting in Section 5.1, the codomains of trc and thc need not coincide.
Proof. We shall show that the transposetr∨c : A −→ PX

in Setsof trc under the adjunction in (5.6) makes the diagram (5.2)—which defines J Kc —commute.
∨
This proves tr∨
c = J Kc , hence trc = J Kc = thc .
First note that the transpose tr∨
c : A → PX is given by the arrow Op(trc ) : A → X inKℓ(P) thought of as an arrow in Sets. In the sequel we shall write Op(trc ) for tr∨c.
Commutativity of the diagram (4.1)—defining trc —yields the following equality.
Op(trc ) ◦ Op(Jα−1 ) = Op(c) ◦ Op(F

op

trc )

in Kℓ(P).

By the definition of composition in Kℓ(P), it reads as follows in Sets.
µX ◦ P(Op(trc )) ◦ Op(Jα−1 ) = µX ◦ P(Op(c)) ◦ Op(F

op

trc )

We use this equality in showing that Op(trc ) makes the diagram (5.2) commute.
Op(trc ) ◦ α = µX ◦ ηX ◦ Op(trc ) ◦ αunit law= µX ◦ P(Op(trc )) ◦ ηA ◦ αnaturality of η−1

= µX ◦ P(Op(trc )) ◦ Op(Jα= µX ◦ P(Op(c)) ◦ Op(F

op

)

trc )

Op(Jα−1 ) = Jα = ηA ◦ αby (5.7)
op= µX ◦ P(Op(c)) ◦ F Op(trc )OpF= µX ◦ P(Op(c)) ◦ λX ◦ F Op(trc )definition of F

= F Op, (3.6)= KOp(c) ◦ λX ◦ F Op(trc ) .
Recall that M in (5.2) is now F ; P in (5.2) is now KOp. This concludes the proof.

(5.7)

30

I. HASUO, B. JACOBS, AND A. SOKOLOVA

The proposition establishes a connection between two semantics for F -coalgebras inKℓ(P), namely: trc via a final F -coalgebra, and thc via an initial F -algebra. One may
well say that it is a “degenerate” case because, as we have shown in Section 3, coinduction
in Kℓ(P) and induction in Sets are essentially the same principle. Our emphasis is moreon the fact that the coincidence of induction and coinduction yields a rather uncommon
example of testing situations. Testing situations are of interest in modal logic—where theunderlying contravariant adjunction S op ⊣ P : A → Cop in (5.1) is often the Stone duality
or one of its variants. Our example Kℓ(P)op ⇆ Sets here does not look like one of thosefamiliar examples.
6. Conclusions and future work
We have developed a mathematical principle underlying “trace semantics” for various
kinds of branching systems, namely coinduction in a Kleisli category. This general view is
supported by a technical result that a final coalgebra in a Kleisli category is induced by aninitial algebra in Sets.
The possible instantiations of our generic framework include non-deterministic systems
and probabilistic systems, but do not yet include systems with both non-deterministic andprobabilistic branching. The importance of having both of these branchings in system verification has been claimed by many authors e.g. [48, 60], with an intuition that probabilistic
branching models the choices “made by the system, i.e. on our side,” while (coarser) nondeterministic choices are “made by the (unknown) environment of the system, i.e. on theadversary’s side.” A typical example of such systems is given by probabilistic automata
introduced by Segala [48].
In fact this combination of non-deterministic and probabilistic branching is a notoriously
difficult one from a theoretical point of view [8, 54, 59]: many mathematical tools that are
useful in a purely non-deterministic or probabilistic setting cease to work in the presence ofboth. For our framework of generic trace semantics, the problem is that we could not finda suitable monad T with an order structure.
We have used the order-enriched structure of a Kleisli category (expressing “more possibilities”) to obtain the initial algebra-final coalgebra coincidence result. However, an order
structure is not the only one that can yield such coincidence: other examples include metric,
quasi-metric and quantale-enriched structures (in increasing generality). See e.g. [10,56] forthe potential use of such enriched structures in a coalgebraic setting. The relation of thecurrent work to such structures is yet to be investigated.
In the discipline of process algebra, a system is represented by an algebraic term (such asa.P k a.Q) and a structural operational semantics (SOS) rule determines its dynamics, thatis, its coalgebraic structure. This is where “algebra meets coalgebra” and the interaction is
studied e.g. in [4, 30, 55]. In our recent work [18] we claim the importance of the microcosm
principle in this context and provide a “general compositionality theorem”: under suitable
assumptions, the final coalgebra semantics is compatible with the algebraic structure. The
results of the current paper say that the final coalgebra semantics can be interpreted as
finite trace semantics, hence the result in [18] also yields a general compositionality result
for trace semantics.
In this paper we have included some material—on possibly-infinite traces and testing
situations—which, unfortunately, we have worked out only in a non-deterministic setting.
A fully general account on these topics is left as future work.

GENERIC TRACE SEMANTICS VIA COINDUCTION

31

Finally, there are so many different process semantics for branching systems, between
two edges of bisimilarity and trace equivalence in the linear time-branching time spectrum [57]. How to capture them in a coalgebraic setting is, we believe, an important andchallenging question.
Acknowledgment
Thanks are due to Jiřı́ Adámek, Chris Heunen, Stefan Milius, Tarmo Uustalu and theanonymous referees for helpful discussions and comments.
References[1] S. Abramsky and A. Jung. Domain theory. In S. Abramsky, D.M. Gabbai, and T.S.E. Maibaum, editors,
Handbook of Logic in Computer Science, volume 3, pages 1–168. Oxford Univ. Press, 1994.
[2] J. Adámek and V. Koubek. Least fixed point of a functor. Journ. Comp. Syst. Sci, 19(2):163–178, 1979.
[3] M. Barr and C. Wells. Toposes, Triples and Theories. Springer, Berlin, 1985. Available online.
[4] F. Bartels. On generalised coinduction and probabilistic specification formats. Distributive laws in coalgebraic modelling. PhD thesis, Free Univ. Amsterdam, 2004.
[5] M.M. Bonsangue and A. Kurz. Duality for logics of transition systems. In V. Sassone, editor, FoSSaCS,
volume 3441 of Lect. Notes Comp. Sci., pages 455–469. Springer, 2005.
[6] M.M. Bonsangue and A. Kurz. Presenting functors by operations and equations. In L. Aceto and
A. Ingólfsdóttir, editors, FoSSaCS, volume 3921 of Lect. Notes Comp. Sci., pages 172–186. Springer,
2006.
[7] F. Borceux. Handbook of Categorical Algebra, volume 50, 51 and 52 of Encyclopedia of Mathematics.
Cambridge Univ. Press, 1994.
[8] L. Cheung. Reconciling Nondeterministic and Probabilistic Choices. PhD thesis, Radboud Univ. Nijmegen, 2006.
[9] M.P. Fiore. Axiomatic Domain Theory in Categories of Partial Maps. Distinguished Dissertations in
Computer Science. Cambridge Univ. Press, 1996.
[10] M.P. Fiore. A coinduction principle for recursive data types based on bisimulation. Inf. & Comp.,
127(2):186–198, 1996.
[11] M.M. Fokkinga. Monadic maps and folds for arbitrary datatypes. Memoranda Informatica, Universityof Twente, 94–28, 1994.
[12] P.J. Freyd. Algebraically complete categories. In A. Carboni, M.C. Pedicchio, and G. Rosolini, editors,
Como Conference on Category Theory, number 1488 in Lect. Notes Math., pages 95–104. Springer,
Berlin, 1991.
[13] P.J. Freyd. Remarks on algebraically compact categories. In M.P. Fourman, P.T. Johnstone, and A.M.
Pitts, editors, Applications of Categories in Computer Science, number 177 in LMS, pages 95–106.
Cambridge Univ. Press, 1992.
[14] I. Hasuo. Generic forward and backward simulations. In C. Baier and H. Hermanns, editors, International Conference on Concurrency Theory (CONCUR 2006), volume 4137 of Lect. Notes Comp. Sci.,
pages 406–420. Springer, Berlin, 2006.
[15] I. Hasuo and B. Jacobs. Coalgebraic trace semantics for probabilistic systems. In P. Mosses, J. Power,and M. Seisenberger, editors, CALCO-jnr Workshop, 2005.
[16] I. Hasuo and B. Jacobs. Context-free languages via coalgebraic trace semantics. In J.L. Fiadeiro, N. Harman, M. Roggenbach, and J.J.M.M. Rutten, editors, International Conference on Algebra and Coalgebrain Computer Science (CALCO’05), volume 3629 of Lect. Notes Comp. Sci., pages 213–231. Springer,
Berlin, 2005.
[17] I. Hasuo, B. Jacobs, and A. Sokolova. Generic trace theory. In N. Ghani and A.J. Power, editors,
International Workshop on Coalgebraic Methods in Computer Science (CMCS 2006), volume 164 of
Elect. Notes in Theor. Comp. Sci., pages 47–65. Elsevier, Amsterdam, 2006.
[18] I. Hasuo, B. Jacobs, and A. Sokolova. The microcosm principle and concurrency in coalgebras, 2007.
Preprint, available from http://www.cs.ru.nl/~ichiro/papers.

32

I. HASUO, B. JACOBS, AND A. SOKOLOVA[19] I. Hasuo and Y. Kawabe. Probabilistic anonymity via coalgebraic simulations. In R. De Nicola, editor,
European Symposium on Programming (ESOP 2007), volume 4421 of Lect. Notes Comp. Sci., pages
379–394. Springer, 2007.
[20] C. Hermida and B. Jacobs. Structural induction and coinduction in a fibrational setting. Inf. & Comp.,
145:107–152, 1998.
[21] C.A.R. Hoare. Communicating Sequential Processes. Prentice Hall, 1985.
[22] J. Hughes and B. Jacobs. Simulations in coalgebra. Theor. Comp. Sci., 327(1-2):71–108, 2004.
[23] B. Jacobs. Categorical Logic and Type Theory. North Holland, Amsterdam, 1999.
[24] B. Jacobs. Trace semantics for coalgebras. In J. Adámek and S. Milius, editors, Coalgebraic Methods in
Computer Science, volume 106 of Elect. Notes in Theor. Comp. Sci. Elsevier, Amsterdam, 2004.
[25] B. Jacobs and J.J.M.M. Rutten. A tutorial on (co)algebras and (co)induction. EATCS Bulletin, 62:222–
259, 1997.
[26] B. Jacobs. Introduction to coalgebra. Towards mathematics of states and observations. Draft of a book,www.cs.ru.nl/B.Jacobs/PAPERS/index.html, 2005.
[27] C.B. Jay. A semantics for shape. Science of Comput. Progr., 25:251–283, 1995.
[28] G.M. Kelly. Basic Concepts of Enriched Category Theory. Number 64 in LMS. Cambridge Univ. Press,
1982.
[29] M. Kick, A.J. Power, and A. Simpson. Coalgebraic semantics for timed processes. Inf. & Comp.,
204(4):588–609, 2006.
[30] B. Klin. From bialgebraic semantics to congruence formats. In Workshop on Structural Operational
Semantics (SOS 2004), volume 128 of Elect. Notes in Theor. Comp. Sci., pages 3–37, 2005.
[31] B. Klin. Bialgebraic operational semantics and modal logic. In Logic in Computer Science, pages 336–
345. IEEE Computer Society, 2007.
[32] B. Klin. Coalgebraic modal logic beyond Sets. In MFPS XXIII, volume 173, pages 177–201. Elsevier,
Amsterdam, 2007.
[33] A. Kock. Monads on symmetric monoidal closed categories. Arch. Math., XXI:1–10, 1970.
[34] C. Kupke, A. Kurz, and Y. Venema. Stone coalgebras. Theor. Comp. Sci., 327(1-2):109–134, 2004.
[35] C. Kupke, A. Kurz, and D. Pattinson. Algebraic semantics for coalgebraic logics. Elect. Notes in Theor.
Comp. Sci., 106:219–241, 2004.
[36] A. Kurz. Logics for Coalgebras and Applications to Computer Science. PhD thesis, Universität München,
April 2000.
[37] A. Kurz. Coalgebras and their logics. SIGACT News, 37(2):57–77, 2006.
[38] F.W. Lawvere. Metric spaces, generalized logic, and closed categories. Seminario Matematico e Fisico.
Rendiconti di Milano, 43:135–166, 1973. Reprinted in Theory and Applications of Categories, 1:1–37,
2002.
[39] M. Lenisa, A.J. Power, and H. Watanabe. Distributivity for endofunctors, pointed and co-pointed
endofunctors, monads and comonads. In H. Reichel, editor, Coalgebraic Methods in Computer Science,
volume 33 of Elect. Notes in Theor. Comp. Sci. Elsevier, Amsterdam, 2000.
[40] M. Lenisa, J. Power, and H. Watanabe. Category theory for operational semantics. Theor. Comp. Sci.,
327(1–2):135–154, 2004.
[41] N. Lynch and F. Vaandrager. Forward and backward simulations. I. Untimed systems. Inf. & Comp.,
121(2):214–233, 1995.
[42] S. Mac Lane. Categories for the Working Mathematician. Springer, Berlin, 2nd edition, 1998.
[43] P.S. Mulry. Lifting theorems for Kleisli categories. In Mathematical Foundations of Programming Semantics (MFPS IX), pages 304–319, London, UK, 1994. Springer-Verlag.
[44] A. Pardo. Fusion of recursive programs with computational effects. Theor. Comp. Sci., 260(1–2):165–
207, 2001.
[45] D. Pavlović, M. Mislove, and J.B. Worrell. Testing semantics: connecting processes and process logics.
In M. Johnson and V. Vene, editors, Algebraic Methodology and Software Technology (AMAST 2006),
volume 4019 of Lect. Notes Comp. Sci. Springer, 2006.
[46] J. Power and D. Turi. A coalgebraic foundation for linear time semantics. In Category Theory andComputer Science, volume 29 of Elect. Notes in Theor. Comp. Sci. Elsevier, Amsterdam, 1999.
[47] J.J.M.M. Rutten. Universal coalgebra: a theory of systems. Theor. Comp. Sci., 249:3–80, 2000.
[48] R. Segala. Modeling and verification of randomized distributed real-time systems. PhD thesis, MIT, 1995.

GENERIC TRACE SEMANTICS VIA COINDUCTION

33[49] R. Segala. A compositional trace-based semantics for probabilistic automata. In International Conference on Concurrency Theory (CONCUR ’95), pages 234–248. Springer-Verlag, 1995.
[50] A.K. Simpson. Recursive types in Kleisli categories. Unpublished paper, available at
http://homepages.inf.ed.ac.uk/als/Research/, 1992.
[51] M.B. Smyth and G.D. Plotkin. The category theoretic solution of recursive domain equations. SIAM
Journ. Comput., 11:761–783, 1982.
[52] A. Sokolova. Coalgebraic Analysis of Probabilistic Systems. PhD thesis, Techn. Univ. Eindhoven, 2005.
[53] M. Stoelinga and F.W. Vaandrager. A testing scenario for probabilistic automata. In J.C.M. Baeten,
J.K. Lenstra, J. Parrow, and G.J. Woeginger, editors, ICALP, volume 2719 of Lect. Notes Comp. Sci.,
pages 464–477. Springer, 2003.
[54] R. Tix, K. Keimel, and G.D. Plotkin. Semantic domains for combining probability and non-determinism.
Elect. Notes in Theor. Comp. Sci., 129:1–104, 2005.
[55] D. Turi and G. Plotkin. Towards a mathematical operational semantics. In Logic in Computer Science,
pages 280–291. IEEE, Computer Science Press, 1997.
[56] D. Turi and J.J.M.M. Rutten. On the foundations of final semantics: non-standard sets, metric spaces
and partial orders. Math. Struct. in Comp. Sci., 8(5):481–540, 1998.
[57] R.J. van Glabbeek. The linear time–branching time spectrum I; the semantics of concrete, sequential
processes. In J.A. Bergstra, A. Ponse, and S.A. Smolka, editors, Handbook of Process Algebra, chapter 1,
pages 3–99. Elsevier, 2001. Available at http://boole.stanford.edu/pub/spectrum1.ps.gz.
[58] R.J. van Glabbeek, S.A. Smolka, and B. Steffen. Reactive, generative, and stratified models of probabilistic processes. Inf. & Comp., 121:59–80, 1995.
[59] D. Varacca and G. Winskel. Distributing probabililty over nondeterminism. Math. Struct. in Comp.
Sci., 16(1):87–113, 2006.
[60] M.Y. Vardi. Automatic verification of probabilistic concurrent finite-state programs. In FOCS ’85, pages
327–338, 1985.

Appendix A. Preliminaries
A.1. Initial/final sequences. Here we recall the standard construction [2] of the initial
algebra (or the final coalgebra) via the initial (or final) sequence. Notice that the basecategory need not be Sets.
Let C be a category with initial object 0, and F : C → C be an endofunctor. The initial
sequence 10 of F is a diagram
0

¡

F0

F ¡

F n−1 ¡

···

F n0

Fn ¡

···

where ¡ : 0 → X is the unique arrow.
Now assume that:αn• the initial sequence has an ω-colimit11 (F n 0 −→A)n<ω ;• the functor F preserves that ω-colimit.
Then we have two cocones (αn )n<ω and (F αn−1 )n<ω over the initial sequence. Moreover,the latter is again a colimit: hence we have mediating isomorphisms between these cones.
αn

···

F n0

Fn ¡

F n+1 0F αn−1

αn+1

···
F αn

10In this paper we consider only initial/final sequences of length ω.
11An ω-colimit is a colimit of a diagram whose shape is the ordinal ω.

A
α ∼
= α−1

FA

34

I. HASUO, B. JACOBS, AND A. SOKOLOVA∼=
Proposition A.1. The F -algebra α : F A →A is initial.

Proof. For future reference we prove the dual result: see Proposition A.2.
The dual of this construction yields a final F -coalgebra. Assume that the base category
C has a terminal object 1. The final sequence of F is
1

!

F1

F!

F n−1 !

···

Fn !

F n1

··· ,
ζn

where ! : X → 1 is the unique arrow. Assume that it has an ω op -limit (Z −→ F n 1)n<ω ,and also that F preserves that ω op -limit. We have the following situation.
ζn

···

F n1

Fn !

Z

ζn+1

···

F n+1 1

ζ −1 ∼= ζF ζnF ζn−1FZ∼=
Proposition A.2. The coalgebra ζ : Z →F Z is final.
βn

Proof. Any F -coalgebra c : X → F X induces a cone (X −→ F n 1)n<ω over the final
sequence in the following way.
β0 = ! : X −→ 1 ,βn+1 = F βn ◦ c .

Now we can prove the following: for an arrow f : X → Z, f is a morphism of coalgebras
from c to ζ if and only if f is a mediating arrow from the cone (βn )n<ω to the limit (ζn )n<ω .
Hence such a morphism of coalgebras uniquely exists.
It is easy to see that every shapely functor in Sets preserves ω-colimits and ω op -limits.
Hence we have the following.
Lemma A.3. A shapely functor F has both an initial algebra and a final coalgebra in Sets.

A.2. limit-colimit coincidence. We recall some relevant notions and results from [51].
The idea is that in a suitable order-enriched setting, (co)limits are equivalently described as
an order-theoretic notion of O-(co)limits. Due to the inherent coincidence between O-limits
and O-colimits, we also obtain the so-called limit-colimit coincidence.
limit
O-limitcolimitobvious coincidence

O-colimit

The notions of O-(co)limits are stated in terms of embedding-projection pairs which
we can define in an order-enriched category. In the sequel we assume the Cppo-enriched
structure.
Definition A.4 (Embedding-projection pairs). Let C be a Cppo-enriched category. A
pair of arrows
e

Y

X
p

GENERIC TRACE SEMANTICS VIA COINDUCTION

35

in C is said to be an embedding-projection pair if we have p ◦ e = id and e ◦ p ⊑ id.
Diagrammatically presented,
e

Y

id

p

id

X

⊑

X

Y.

e

By p ◦ e = id we automatically have that e is a mono and p is an epi. Both split.
Proposition A.5. Let (e, p), (e′ , p′ ) : X ⇄ Y be two embedding-projection pairs with thesame (co)domains. Then e ⊑ e′ holds if and only if p′ ⊑ p. As a consequence, one
component of an embedding-projection pair determines the other.
This proposition justifies the notation eP for the projection corresponding to a given embedding e, and pE for the embedding corresponding to a given projection p. It is easy tocheck that(e ◦ f )P = f P ◦ eP
and(p ◦ q)E = q E ◦ pE .
f0

f1

Definition A.6 (O-(co)limits). Let X0 → X1 → · · · be an ω-chain in a Cppo-enriched C.
σn
A cocone (Xn →C)n<ω over this chain is said to be an O-colimit if:• each σn is an embedding;• the sequence of arrows ( C
the cpo C(C, C) is idC .

P
σn

σn

Xn

C )n<ω is increasing. Moreover its join taken in
C

σ0
σ1

X0
γn

σ0P
f0

σ1P

X1

···

···

f1
g0

g1

Dually, a cone (C → Yn )n<ω over an ω op -chain Y0 ← Y1 ← · · · is an O-limit if: eachγn is a projection, and the sequence (γnE ◦ γn : C → C)n<ω is increasing and its join is idC .
The following proposition establishes the equivalence between (co)limits and O-(co)limits. For its full proof the reader is referred to [51].
e

e

0
1
Proposition A.7 (Propositions A, B, C, D in [51]). Let X0 →X1 →· · · be an ω-chain
where each en is an embedding.
σn(1) Let (Xn →C)n<ω be the colimit over the chain. Then each σn is also an embedding.
Moreover, (σn )n<ω is an O-colimit.
σn(2) Conversely, an O-colimit (Xn →C)n<ω over the chain is a colimit.

p0

p1

Dually, let X0 ← X1 ← · · · be an ω op -chain where each pn is a projection.
τn(3) Let (D →Xn )n<ω be a limit over the chain. Then each τn is also a projection.
Moreover (τn )n<ω is an O-limit.
τn(4) Conversely, an O-limit (D →Xn )n<ω over the chain is a limit.
βn

Proof. For later reference we present the proof of (4). Let (B → Xn )n<ω be an arbitraryp0
p1
cone over the chain X0 ← X1 ← · · · . First we prove the uniqueness of a mediating map

36

I. HASUO, B. JACOBS, AND A. SOKOLOVA

f : B → D.
En<ω (τn ◦ τn ) ◦ f
F= n<ω (τnE ◦ τn ◦ f )F= n<ω (τnE ◦ βn )f = idD ◦ f =F(τn )n<ω is an O-limit
composition is continuous
f is mediating .

We conclude the proof by showing that the sequence (τnE ◦ βn )n<ω is increasing, hence suchf indeed exists.
EE
τnE ◦ βn = τnE ◦ pn ◦ βn+1 = τn+1
◦ pE
n ◦ pn ◦ βn+1 ⊑ τn+1 ◦ βn+1

The last inequality holds because pEn ◦ pn ⊑ id from the definition of embedding-projection
pairs.
ee

0
1Theorem A.8 (Limit-colimit coincidence). Let X0 →X1 →· · · be an ω-chain where eachσnen is an embedding, and (Xn → C)n<ω be the colimit over the chain. Then each σn is an

eP

σP

eP

n
0
1
embedding, and the cone (C →Xn )n<ω is a limit over the ω op -chain X0 ←
X1 ←
···.

C

σ0

: colimit

σ1

X0

e0

X1

e1

···

C

σ0P

=⇒

σ1P

X0

eP
0

X1

eP
1

: limit···

Dually, the limit of an ω op -chain of projections consists of projections. By taking thecorresponding embeddings we obtain a colimit of an ω-chain of embeddings.
Proof. We prove the first statement. By Proposition A.7 each σn is an embedding, and
eP

eP

0
1
X1 ←
···.
moreover (σn )n<ω is an O-colimit. Now obviously (σnP )n<ω is a cone over X0 ←Here we use the inherent coincidence of O-(co)limits: namely, the condition that (σn )n<ω
is an O-colimit is exactly the same as that (σnP )n<ω is an O-limit. We use Proposition A.7
to conclude the proof.

This work is licensed under the Creative Commons Attribution-NoDerivs License. To viewa copy of this license, visit http://creativecommons.org/licenses/by-nd/2.0/ or send a
letter to Creative Commons, 559 Nathan Abbott Way, Stanford, California 94305, USA.