The Microcosm Principle andConcurrency in Coalgebras
Ichiro Hasuo
Radboud University Nijmegen, the Netherlands
Kyoto University, Japan

Joint work with

Bart Jacobs
Radboud U. Nijmegen, NL

Ana Sokolova
U. Salzburg, Austria

1-slide review of coalgebra/coinduction
abstraction, genericity, (joy)Theory of coalgebras= “categorical theory of state-based systems”
categoricallysystemin Sets : bisimilarity
behaviorpreserving
mapin Kleisli : trace
semantics

coalgebra

morphism of coalgebras[Hasuo,Jacobs,Sokolova]

behavior

coinduction(via final coalgebra)

Concurrency{is about parallel composition C || Drunning C and D at the same timez with communication/synchronization between C and Dz{is everywhere
computer networks
Picture byBocchi, Fiadeiro, Lopesz multi-core processorsz modular, component-based design of complex systemsz{is hard to get rightze.g. so easy to get into deadlockszcf. Edward Lee. Making Concurrency Mainstream.
Invited talk at CONCUR 2006.
http://ptolemy.eecs.berkeley.edu/presentations/main.htm

Compositionality
Behavior of C || Dis determined bybehavior of C and behavior of D

Enables compositional verification of complex systems{ Conventional presentation:{C ~ C’,z

D ~ D’

ÎC || D ~ C’ || D’~ : process/observational/behavioral equivalence{ bisimilarity, trace equivalence, etc.

z“bisimilarity is a congruence”

Compositionality in coalgebras{ Final coalgebra semantics as“process semantics”.
{ “Coalgebraic compositionality”{ Two different || !

|| : CoalgF x CoalgF Æ CoalgF
on coalgebras
z || : Z x Z Æ Z
on statesz

Nested algebraic structures:the microcosm principle
with{The same “algebraic structure”
operations (binary ||)z equations(e.g. associativity of ||)z{is carried by
the category CoalgF andz its object Z ∈ CoalgF
in a nested manner!
z{“Microcosm principle” (Baez & Dolan)

Microcosm in macrocosm

XThe microcosm principle{ You may have seen itz“a monoid is in a monoidal category”z

Notice:{ The “inner” structure depends on the “outer” one{ We identify (probably) the first CS example

Formalizing the microcosm principle
What do we mean exactly by the “microcosm principle”?
{{{

When a category L presents an algebraic theory(Lawvere theory),Its (set-theoretic) model isa FP-preserving functor

How about a nested model as in the microcosm principle?
Î Our answer: a lax natural transformation

Outline{

Microcosm principle for concurrency (|| and ||)z|| and || essentially arise from“synchronization” natural transformationsync : FX ⊗ FY Æ F(X ⊗Y){

The microcosm principle syntactically
Algebraic structure is syntactically presented as (Σ, E)
z … (Ana can tell you more!)z{The microcosm principle 2-categorically(Common) alg. str. is presented by a Lawvere theory
z Applications:z{ generic compositionality theorem{ generic soundness theorem

Part I:
Parallel composition of coalg.
via sync nat. trans.

Parallel composition of coalgebras|| : bifunctor CoalgF x CoalgF Æ CoalgF
Î usually denoted by ⊗ (tensor){ Theorem If{

the base category C has associative tensor⊗:CxC Æ Cz and F : C Æ C comes with natural transformation
syncX,Y : FX ⊗ FY Æ F(X ⊗ Y)z then we have ⊗ : CoalgF x CoalgF Æ CoalgF
zParallel composition arises from sync

Parallel composition of coalgebras⊗ Y)
F (X??
syncX,YFX ⊗ FYc⊗dX⊗??Y⊗ on basecategory{ Different sync yield different ⊗Examples ofsync : FX ⊗ FY Æ F(X ⊗ Y)
C = Sets, F = Pfin(Σ x _)for LTS

Cartesian product as ⊗{ CSP-style (Hoare){ CCS-style (Milner)

Assuming

Compositionality result{Compositionality result{Theorem
Given that{

C has tensor ⊗{F has syncX,Y : FX ⊗ FY Æ F(X ⊗ Y){

there is a final coalgebra Z Æ FZ

we have compositionality“Compositionality for free”{ It follows:
C ~ C’, D ~ D’ Î C || D ~ C’ || D’{ Proof By finality{ We shall generalize this to an arbitrary (single-sorted)
algebraic theory{

Part II:2-categorical formulation of
the microcosm principle

Microcosm principle (Baez & Dolan){ The same algebraic theory{ interpreted both on C and on X ∈ Cz C : outer modelz X ∈ C : inner model{ Examples:z monoid in a monoidal categoryz final coalgebra in CoalgF with ⊗What is microcosm principle, mathematically?

Setting{ 2-categoricalz 2-categories: categories in categories
z suitable for microcosm structures, i.e.

algebras in algebras

Lawvere theory L{ Categorical presentation of an algebraic

specification/theory{ Definition

A Lawvere theory L is a small categorys.t.
z L’s objects are natural numbersz L has finite products

Lawvere theory
is a category L that has{ Arrows for operations

arityarity{ Commutativity for equations~ unit law{ Other arrows:

projectionsz (composed) terms
z~ assoc. law

Models for Lawvere theory{Cf. A (set-theoretic) model isa FP-preserving functor

A set with L-structurez “Functorial semantics”
z{How about the microcosm principle:
L-algebraic structures on
C : outer modelz X ∈ C : inner modelz

Outer model: L-category{ Outer model=a category with L-structure Î “L-category”{ L-category: an FP-preserving functorz

In fact, a pseudo-functor (equations are up-to-iso)Inner model: L-object
Definition
An L-object in an L-category
is a lax natural transformation

Outer model

Recall:compatible with products.

Components

Inner alg. structure
occurs from lax naturality
lax naturality

lax L-functor: lax natural trans.
L-functor: (strict) natural transformation

Facts lax naturality:
lax L-functor{ L-functorpreserves
L-objects.
= functorwith sync
{ C: L-categoryz

F: C Æ C, lax L-functor
Î CoalgF is an L-categoryz

F: C Æ C, oplax L-functor
Î AlgF is an L-categoryz

X ∈ C , L-object
Î C/X is an L-categoryzFinal object is an L-object

F : lax, G : oplax
Î Inserter Ins(F, G) isan L-category

Generic compositionality result{Theorem
Given that{

C is an L-category{F : C Æ C is a lax L-functor{

there is a final coalgebra Z Æ FZ

the functor

by coinduction

is a (strict) L-functor.
{This subsumes the previous compositionality result

Related work: bialgebras{ Related to the study of bialgebraic structures[Turi-Plotkin, Bartels, Klin, …]
z Algebraic structures on coalgebras{ In the current work:z Equations, not only operations, are also anintegral partz Algebraic structures are nested, higherdimensional

Conclusion{ Microcosm principle :same algebraic structure
on a category C andz on an object X ∈ Cz

{ 2-categorical formulation:

Inner model

Algebraic theory
Outer model{ Concurrency in coalgebras as a CS example{ Preprint available:

http://www.cs.ru.nl/~ichiro

Thank you for your attention!
Ichiro Hasuo, Kyoto U., Japan(At U. Nijmegen, NL, till 2008.3)
http://www.cs.ru.nl/~ichiroBehavior by coinduction: example
Take F = Pfin (Σ × _) in Sets.
{{System as coalgebra:

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

processgraph of xxzz

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

such asExamples ofsync : FX ⊗ FY Æ F(X ⊗ Y)
{ Note:Asynchronous/interleaving compositions
don’t fit in this frameworkz such asz We have to use, instead of F,

the cofree comonad on F

Lawvere theory{Presentation of an algebraic theory as a category:zz

objects: 0, 1, 2, 3, … “arities”
arrows: “terms (in a context)”
projections
operation
composed termz

commuting diagrams are understood as “equations”~ unit lawz~ assoc. law

arises from(single-sorted) algebraic specification (Σ, E) as the syntactic category{ FP-sketch{Outline{ In a coalgebraic study of concurrency,{ Nested algebraic structures

on a category C andz on an object X ∈ Cz

arise naturally (microcosm principle){ Our contributions:

Syntactic formalization of microcosm principle
z 2-categorical formalization with Lawvere theories
z Application to coalgebras:{ generic compositionality theoremz

Generic soundness result{ A Lawvere theory L is foroperations, andz equations (e.g. associativity, commutativity)z{ CoalgF is an L-categoryÎ Parallel composition ⊗ is automaticallyassociative (for example)zUltimately, this is due to the coherence condition on
the lax L-functor F{ Possible application :Study of syntactic formats that ensureassociativity/commutativity (future work)