Healthiness fromDuality
Wataru Hino, Hiroki Kobayashi, Ichiro Hasuo
The University of Tokyo

Bart Jacobs
Radboud University1

Today’s goal••

Categorical predicate transformer semantics•

unifying [Hasuo 2014] and [Jacobs CALCO 2015]
with relative algebra•

enabling formulation of healthiness condition

Extension to the alternating cases

Wataru Hino (Tokyo)

2

Predicate Transformer
Semantics
Interpreting a computation (= a Kleisli arrow)as a backward predicate transformer
predicate transformer

nondet. program

mustXf! PY

Wataru Hino (Tokyo)

2X{x 2 X | 8y 2 f (x). y 2 S}3Y2[S✓YRemark: There might be multiple choices ofPT semantics for a single type of branching.
must{x 2 X | 8y 2 f (x). y 2 S}[S✓Yf

X ! PYmay{x 2 X | 9y 2 f (x). y 2 S}[S✓YWataru Hino (Tokyo)

4Probabilistic Example
prob. program

predicate transformer

0.7
0.3
1.0
0.4
0.6

⇢

probability
distributions on Y

Wataru Hino (Tokyo)

001

weighted
0.7
sumf

X ! DY

0.3

( x.

X

[0, 1]

0.5

X

p(y)f (x, y))y2Y589< x1 7! 0.3 =x2 7! 0:;x3 7! 0.7

[0, 1]Y[ (p : Y ! [0, 1])

8
9< y1 7! 0 =y2 7! 1[:;
y3 7! 0.5

Healthiness condition
Healthiness condition: what kind of predicate
transformer comes from a Kleisli arrow?
e.g.

Thm. for ' : 2Y ! 2X ,' = P⌃ (f ) for some f : X ! PY () ' is join-preserving

In other words,⌃

P : K`(P)

op! CLW(X ! P Y ) 7! (2X
Wataru Hino (Tokyo)

2Y )

6

is well-defined & full.

Categorical understandingsof PT semanticsWataru Hino (Tokyo)

7

Recipe 1: adjunction recipe[Jacobs CALCO 2015]

Observation: we have a decomposition:2(P⇠=[2,2]WSetk8

PX ! [2 , 2]W_S 7! ( 7!

(x))

()

X

x2S

Wataru Hino (Tokyo)

8?

)[ ,2]W,op
CLW

then we have
(X 7! PY ) 7P⌃K`( )K`(P) ⇠ / K` [2( ) , 2]W=eY

X! (2 ! 2 )Ka$

Set r/5 (CLW )opaop
W! (CL )and the resulting functor K`(P)
is fully faithful (since so is comparison functor K),→ healthiness condition!

Wataru Hino (Tokyo)

9Summary of adjunction recipe
Key: decomposing a monad into a dual adjunction✓ healthiness condition for free✗ decomposition is hard to find✗ hiding the use of modality (e.g. may vs. must)

Wataru Hino (Tokyo)

10

Recipe 2: modality recipe
Observation: modality = Eilenberg-Moore algebra[Moggi 1991, Hasuo 2014]

e.g. May-modality(for powerset)
W= P2 ! 2 (join-semilattice structure)
Using this “modality”, we can define PT semantics as⌃

P : K`(P) ! Setf(X ! P Y ) 7! (2Wataru Hino (Tokyo)

X11

opYY2 )

PYOfXP!2/ P2W✏/2

Summary of modality recipe
Key: Use of modality = EM-algebra over truth values✓ concrete description of PT semantics✓ able to distinguishW“must vs. may”
V
(as choice of P2 ! 2 or P2 ! 2 )✗ domain of interpretation is restricted to Set✗ too loose to acquire healthiness result

Wataru Hino (Tokyo)

12

Problem•

How to unify these 2 approaches?
••

adjunction recipe & modality recipe

we want to get•precise healthiness result•concrete description of semantics by modality

Wataru Hino (Tokyo)

13

Key observation⌧A modality T ⌦ ! ⌦ defines Set-valued semantics
K`(T ) ! Setsince ⌦ is a set.

op

X 7 ! ⌦X

X-fold product of Ω

Wataru Hino (Tokyo)

14

To acquireKl(P) ! DopD
we want T-algebra whose underlying space is in D.

How to formalize it?

Wataru Hino (Tokyo)

15

Equivalent formulation ofEilenberg-Moore algebra
Thm (Kelly?). T : monad on Set, A : set, then↵ : T A ! A : EM-alg]↵ : T ! Set(A( ), A) : monad map

A(Set(A(),A)

Setk816,?
A(Wataru Hino (Tokyo)))Setop

Universal algebraic perspective
The monad map can be understood as:]↵X : T X

t7! Set(AX , A)]
! ↵X (t)its interpretation

term over X

Wataru Hino (Tokyo)

17

Relative algebra
Def. (D : complete cat.)a D-relative T -algebra is a pair (A, ↵) where• A2D• ↵ : T ! D(A( ) , A) : monad map
A(D(A(),A)

Setk8)?
D( ,A)

Wataru Hino (Tokyo)

18+DopRelative algebra recipe
Ingredient: D : complete category (for predicates)(⌦, ⌧ ): relative T-algbera (modality)
T ! D(⌦( ) , ⌦)then we can define PT-semantics asK`(T )
P⌧D✏

op

Wataru Hino (Tokyo)

X ! T Y in Set
YX ! T Y ! D(⌦ , ⌦)⌦

Y!⌦

19X

in D

Healthiness result
Recall we have P⌧ : K`(T ) ! Dop for relative T -alg (⌦, ⌧ ).
Thm (Healthiness result).
P⌧X,Y : K`(T )(X, Y ) ! D(⌦Y , ⌦X ) is surjective (injective)
if ⌧Y : T Y ! D(⌦Y , ⌦) is surjective (injective)

Wataru Hino (Tokyo)

20

Problem of relative algebra(A : D-object, ⌧ : T ! D(A•, A))

Too abstract, difficult to construct explicitly••( )to define a relative algebra, we need a naturaltransformation = large amount of datacf.) a T-algebra = an object & a morphism

Wataru Hino (Tokyo)

21

Construct a relative algebra
Assume UD : D ! Set : faithful and continuousThm. there is a bijective correspondence
a D-relative T -algebraaAD 2 D and T A ! A subject to• UD (AD ) = A• satisfies the following lifting condition:
TX
Wataru Hino (Tokyo)

229a] Xa]XD(AX, AD )D9UD✏
/ Set(AX , A)

ExamplesW• ⌧⌃ : P2 ! 2 induces CLW -relative algebra,]with ⌧⌃ : P ! [2( ) , 2]W an isomorphism.
! P⌧⌃ = P⌃ is fully faithful.
R• ⌧ = : D[0, 1] ! [0, 1] induces EMod-relative algebra,
and ⌧ ] : DX ! EMod([0, 1]X , [0, 1]) is bijective when X finite.
! healthiness for finite states holds.

(These results are already known)
Wataru Hino (Tokyo)

23

Summary ofrelative algebra recipe•

introduced new categorical formulation of PT
semantics, unifying our two works✓ fine enough to explain helathiness condition fromcategorical point of view✓concrete description using “modality”

Wataru Hino (Tokyo)

24

Missing Link•

We have defined a functor:⌧
op
P : K`(T ) ! D(X ! T Y ) 7! (⌦•XY⌦ )It only involves Kleisli category,with Eilenberg-Moore category missing.

Wataru Hino (Tokyo)

25

In fact, it is a part of larger picture (if DD is complete)
opD [ lP⌧

[ ,⌦]D>[ ,⌦]TK`(T ),EM(T )_K

State-and-effect triangle[Jacobs]

Wataru Hino (Tokyo)

26

More details
D : complete and concrete,Setting:⌦ = (⌦, ⌧ ) : D-relative T -algebrathen we have[ ,⌦]D,op• We have dual adjunction D>
EM(T )l[ ,⌦]T••“over” Hom-functors (into “⌦” )⌧Factors through P : K`(P) ! Di.e. the following commutes.
op

D [P⌧

Wataru Hino (Tokyo)[ ,⌦]DK`(T ),EM(T )
_K

27op

op

D [ lP⌧[ ,⌦]D>[ ,⌦]TK`(T ),EM(T )_K

Why is this important?

We will use it for alternating branching case!

Wataru Hino (Tokyo)

28

Alternating branching•mixing 2 types of branching•nondet. & nondet. (player vs. opponent)•

nondet. & prob. (opponent vs. environment)[Morgan, McIver, Seidel 1996]•

formulated in [Hasuo 2014] assecond move

TR?T =U RF

Set
8F

Set
l8?

Ualternating branching
Wataru Hino (Tokyo)

29,

first move

EM(T ) R

Modalities for alternation
Non-alternating

AlternatingFBranching

Set8TSet
k8R?T =U RF

DG op

ModalityA()? D( ,A)

SetZ⌧ : T !D(A(Wataru Hino (Tokyo)

DG[ ,⌦]T?

U? [ ,⌦]DDop[ l⇢ : R![[ ,⌦]T ,⌦]D,A)
30

EM(T ) Rop

EM(T )W)-P⌧[ ,⌦]D>[ ,⌦]TK`(T ),EM(T )
_K

Results•Using these two modalities,

2nd branching

we have a PT-semantics:P•⌧,⇢: K`(R ? T ) ! D

modalities for⌧ : T ! D(A, A)

1st branchingop⇢ : R ! [[ , ⌦]T , ⌦]D

Its healthiness result is in the paper.

Wataru Hino (Tokyo)( )31

Summary ofthe alternting cases•

A dual adjunction between D and EM(T )••a part of a state-and-effect triangle

Our result naturally extends to the alternating cases•

using the dual adjunction above

Wataru Hino (Tokyo)

32

Future works•

Investigate relative algebra••

especially its connection to Lawvere theory

Extend result to enriched settings (cf. [Keimel 2015])

Wataru Hino (Tokyo)

33