Kyoto University, Japan
PRESTO Promotion Program, Japan

Radboud Univ. Nijmegen, NL
Technical Univ. Eindhoven, NL

Univ. Salzburg, Austria

Categorical theory of state‐based systems
in Sets : bisimilarity
i KlinKleisli:
i li trace semanticsi[Hasuo,Jacobs,Sokolova LMCS´07]

systembehavior‐
behavior‐
preserving
mapb h ibehavior

coalgebra
morphism ofcoalgebras

coinduction(via final coalgebra)

is everywhere• computerpnetworks• multi‐core processors• modular, component‐based design of complex systems

is hard to get right• so easy to get into deadlocks• exponentially growing complexity• cf. Edward Lee. Making Concurrency Mainstream.
• Invited talk at CONCUR 2006.

aids compositionalverificationo bisimilarity
o trace equivalenceo ...

„bisimilarity is acongruence“operation
pon

NFAs
` Final coalgebra
semantics
as|| : Coalg
xCoalgÆCoalgFFF

p coalgebras/systems
semantics”.
“processo composing` “Coalgebraic compositionality”

operation on

regularlanguages|| : Z x Z Æ Z
o composing behavior

withX ∈&o operations

binary ||o equations

e.g. assoc. of ||We name this principle themicrocosm principle, after thetheory,y, common in p
pre‐modern
correlative cosmologies, thatevery feature of the microcosm(e.g. the human soul)corresponds to some feature ofthe macrocosm.
thJohn Baez & James Dolan
Higher‐Dimensional Algebra III:n‐Categories and the Algebra of Opetopes
Adv. Math. 1998

` You may have seen it◦ “a monoid is in a monoidal category”
g y

inner depends on outerAnswer

concurrency/
compositionality

for arbitrary
algebraicl b itheory

microcosm forconcurrency( || and ||||))parallel composition
via sync nat. trans.

2‐categorical formulation

mathematics

Parallel composition of coalgebras
viasyncX,Y : FX ⊗ FY Æ F(X ⊗ Y)

bifunctor CoalgF x CoalgF Æ CoalgF
usually denoted by ⊗ (tensor)

Theorem If⊗ : CoalgF x CoalgF Æ CoalgF

 the base categoryg y C has a tensor⊗:CxC Æ C

 and F : C Æ C comes with naturaltransformationfisyncX,Y : FX ⊗ FY Æ F(X ⊗ Y)
 thenth we haveh⊗ : CoalgF x CoalgF Æ CoalgFlifting⊗ : CxCÆCF (X??
⊗ Y)
syncX,YXYFX ⊗ FYc⊗dX ??
⊗Y⊗ on basebcategory

different
sync

different⊗x : Sets x Sets Æ Sets
` CSP‐style (Hoare)` CCS‐styley ((Milner))

Assuming

C = Sets,S
F = Pfin(Σ x _))F‐coalgebra = LTS` ||“compositionpof states/behavior”/arises by coinduction

AssumeC has tensor ⊗{ F has syncX,Y : FX ⊗ FY Æ F(X ⊗ Y)
{ there is a final coalgebragZ Æ FZ{⊗ byyxxby finality
yields:|| byy` When is⊗ : CoalgF x CoalgF Æ CoalgF
associative?
` Answer When◦ ⊗ : C x CÆ C is associative, and◦ sync
y is “associative”

2‐categorical2
categorical formulation of
the microcosm principle

examplesomonoid inmonoidalcategory

ofinal coalg.
g in
CoalgF with ⊗oreg lang.
lang vs.
vsreg.
NFAs

A Lawvere theory. is a small category s.t.

o L’s objects are natural numberso L has finite productsother arrows:
o projections
o composed terms

operations

as arrowsm (binary)e (nullary)equationsassoc. of munit law

as commuting diagrams

o a set with .‐structure Î.‐set(product‐preserving)what aboutnested models?

X ∈&o a category with .‐structure Î.‐category(product‐preserving)

NB. our focus is on
strict alg. structures

Given an .‐category % an .‐object X in it
is a lax natural transformationcompatible with products.
products

X carrier
X:i obj.
bj

lax L‐functor?

` % : .‐category. t` F: % Æ % , lax .‐functor

Î CoalgF is an .‐category` % : .‐category` Z ∈ % , final object

Î Z is an .‐object

lax natur.
trans..

Generalizes
lax naturality?

Generalizes...

AssumeC is an L‐category{ F : C Æ C is a lax L‐functor{ there is a final coalgebragZ Æ FZ
{CoalgF is an .‐categoryZ Æ FZ is an .‐object

the behavior functor
by coinduction

is a (strict) .
.‐functor
functorsubsumesassociativei ti⊗ : CoalgF x CoalgF Æ CoalgF

lifting

associative⊗ : CxCÆC` equations are built
built‐inin in L

◦ asL‐structuret t
on CoalgF` how about „assoc
assoc“ of sync?

lifting◦ automaticvia
i “coherence“coherencehcondition“
di i “L‐structure
on C` Related
R l t d tto theth studyt d off bialgebraic structures
str ct res[Turi‐Plotkin, Bartels, Klin, …]◦ Algebraic
l b
structures on coalgebrasl b` In the current work:◦ Equations,q, not onlyy operations,p, are also an integral
gpart◦ Algebraic structures are nested, higher
higher‐dimensional` “Pseudo”
Pseudo algebraic structures◦ monoidal category (cf. strictly monoidal category)◦ equations hold up‐to‐isomorphism◦ L Æ CAT, product‐preserving pseudo‐functor?
` Microcosm principle for full GSOSΣBÎBΣcurrent workΣ (B x id) Î B TΣ??

(for full GSOS)

concurrency/
compositionality

for arbitrary
algebraicl b itheory

microcosm forconcurrency( || and ||||))
parallel composition
via sync nat. trans.
Thanks for your attention!
Ichiro Hasuo (Kyoto, Japan)
http://www.cs.ru.nl/~ichiro

2‐categorical formulation

mathematics

` Microcosm principle :same algebraic structure◦ on a category C and◦ on an object X ∈ C` 2‐categorical2 categorical formulation:` Concurrency in coalgebras as a CSexample

Thank you for your attention!
Ichiro Hasuo, Kyoto U., Japan
http://www.cs.ru.nl/~ichiro

Take F = Pfin (Σ × _)) in Sets.
Sets``

System as coalgebra:

the set ofz finitely branchingz edges labeled with Σz infinite-depth
ptrees,Behavior by coinduction:x

process
graph of x

◦ in Sets: bisimilarity◦ in certain Kleisli categories: trace equivalence[Hasuo,Jacobs,Sokolova,CMCS’06]

such as` Note:Asynchronous/interleaving compositions don’t fit inthis framework◦ such as◦ We have to use,use instead of F,F
the cofree comonad on F

`Presentation of an algebraic theory as a category:◦ objects: 0, 1, 2, 3, … “arities”◦ arrows: “terms ((in a context)”)

projections
operation
composed term
◦ commuting diagrams are understood as “equations”~ unit law~ assoc. law◦ arises fromx (single‐sorted) algebraic specification (Σ, E) as the syntactic category
x FP‐sketch` In a coalgebraic study of concurrency,` Nested algebraic structures◦ on a category C and◦ on an object
bj t X ∈ Carise naturally (microcosm principle)` Our contributions:◦ Syntactic formalization of microcosm principle◦ 2‐categorical formalization with Lawvere theories◦ Application to coalgebras:x generic compositionality theorem` A Lawvere theory L is for◦ operations, and◦ equationsti((e.g.
associativity,i ti it commutativity)t ti it )` CoalgF is an L‐categoryÎ Parallel composition ⊗ is automaticallyassociative (for example)◦ Ultimately, this is due to the coherence condition on the lax
L‐functor F` Possible application :Study of syntactic formats that ensureassociativity/commutativity (future work)