Coalgebraic Trace Semantics
for Probabilistic Systems
Ichiro Hasuo and Bart Jacobs
Institute for Computing and Information Sciences, Radboud University Nijmegen
P.O. Box 9010, 6500 GL Nijmegen, The Netherlands
E-mail: {ichiro, B.Jacobs}@cs.ru.nl
URL: http://www.cs.ru.nl/{~ichiro, B.Jacobs}

Introduction The authors introduced in [1] the technique of coalgebraic trace∼=semantics for the powerset monad P. There the initial F -algebra α : F A →Ain Sets gives rise to the final coalgebra in the category Rel of sets and relations.
The category Rel is also described as the Kleisli category SetsP for thepowerset monad P. In this work we show that the analogous result holds forwhat we call the distribution
P monad D, instead of P. The monad D is definedas DX = {d : X → [0, 1] | x∈X d(x) ≤ 1}. It has the same monad structure as
the (standard) distribution monad.
The proof for D does not follow trivially from the one for P. However wenotice similar constructions they have in common. Hopefully the current work
will cast a light over the essence underlying these two different settings, and leadto a result with more generality (e.g. for monads other than P, D).
Technical result and example The endofunctors
F that we consider are`
constructed inductively by: F ::= id | Σ | F × F | i∈I Fi , where Σ is a constantfunctor. This family of functors is large enoughto contain many interesting`
examples, including the list functor X ∗ = n<ω X n . Notice that a functor F
thus constructed preserves ω-colimits: hence the initial F -algebra is obtained asthe colimit {αn : F n 0 → A} of the initial sequence.
∼=Theorem 1 Let α : F A →A be the initial F -algebra, and c : X → DF X be acoalgebra (both in Sets). Then there exists a unique arrow tracec that makes thefollowing diagram in SetsD commute.

FXcXF tracecFAηF A ◦ α−1tracec(1)

AWe sketch the construction of the map tracec . In the first place, to lift afunctor F in Sets to a functor in SetsD , we use a distributive law λ : F D ⇒ DF .
This is constructed inductively on F .1 With λ we can define the n-th composition
1In fact, for a functor F under consideration we can construct a distributive law
F T ⇒ T F for any commutative monad T (D is commutative). Most notably, for
F = F1 × F2 we use the double strength [2] of T .

cn : X → DF n X of a coalgebra c, whose one step corresponds to n successive
steps of c.
We use a construction which might be called the “contravariant distributionfunctor”: for a mono m : X ½ Y , the map Dm : DY → DX is defined by[(Dm)(d)](x) = (d ◦ m)(x). The n-th trace tracenc : X → DA is defined as thefollowing composite, where ?X : 0 → X is the unique arrow.
XcnDF n X

DF n ?XDF n 0DαnDA

The n-th trace gives the distribution over the behavior which terminate withinn steps. Now the trace tracec : X → DA is defined as the limit of the n-th trace,that is, for a ∈ Im αn , [tracec (x)](a) = [tracenc (x)](a). We have shown that tracec
is indeed well-defined, and that it is the unique arrow which makes the diagram(1) commute.
Example 2 (Lists) Consider the functor F = 1 + Σ × −. The initial F -algebra∼=[nil, cons] : 1 + Σ × Σ ∗ →Σ ∗ consists of the lists over Σ. The following is anexample of a coalgebra c : X → DF X.
x(a, 13 )(a, 1)

z(a, 13 )2
9y(a, 12 )12

X

The behavior of the state x is: it transits to y outputting a with the probability of
1/3, the same to z, and it terminates with the probability of 2/9. The remaining
1/9 is best understood as the probability x gets into deadlock.
By Theorem 1 we obtain tracec : X → DΣ ∗ via finality. The distribution
tracec (x) is such that: hi 7→ 2/9 and an 7→ 1/(3 · 2n ). Out of the remaining 4/9,
1/9 is the probability that x gets into deadlock at the first transition, and 1/3
is the probability that x goes to z and keep outputting a without termination(livelock ). The n-th trace tracenc is the restriction of tracec to the lists of at mostlength n.

References
1. I. Hasuo and B. Jacobs. Context-free languages via coalgebraic trace semantics.
In Conference on Algebra and Coalgebra in Computer Science (CALCO 2005), toappear.
2. B. Jacobs. Semantics of weakening and contraction. Ann. Pure & Appl. Logic,
69(1):73–106, 1994.