Generic Weakest Precondition Semantics
from Monads Enriched with Order
Ichiro Hasuo
University of Tokyo, Japan

Abstract. We devise a generic framework where a weakest precondition semantics, in the form of indexed posets, is derived from a monadwhose Kleisli category is enriched by posets. It is inspired by Jacobs’
recent identification of a categorical structure that is common in various
predicate transformers, but adds generality in the following aspects: 1)
different notions of modality (such as “may” vs. “must”) are captured
by Eilenberg-Moore algebras; 2) nested branching—like in games and inprobabilistic systems with nondeterministic environments—is modularly
modeled by a monad on the Eilenberg-Moore category of another.

1

Introduction

Among various styles of program semantics, the one by predicate transformers [5] is arguably the most intuitive. Its presentation is inherently logical, representing a program’s behaviors by what properties (or predicates) hold before
and after its execution. Predicate transformer semantics therefore form a basisof program verification, where specifications are given in the form of pre- andpost-conditions [14]. It has also been used for refinement of specifications into
programs (see e.g. [30]). Its success has driven extensions of the original nondeterministic framework, e.g. to the probabilistic one [18, 24] and to the settingwith both nondeterministic and probabilistic branching [31].
A Categorical Picture More recently, Jacobs in his series of papers [16, 17] haspushed forward a categorical view on predicate transformers. It starts with amonad T that models a notion of branching. Then a program—henceforth calleda (branching) computation—is a Kleisli arrow X → T Y ; and the the weakest
precondition semantics is given as a contravariant functor PK` : K`(T )op → A,from the Kleisli category to the category A of suitable ordered algebras.
For example, in the basic nondeterministic setting, T is the powerset
monadVP on Sets and A is the category CLV of complete lattices and -preserving
maps. The weakest precondition functor PK` : K`(T )op → CLV then carries afunction f : X → PY towpre(f ) : PY −→ PX ,Q 7−→ {x ∈ X | f (x) ⊆ Q} .

(1)

Moreover it can be seen that: 1) the functor PK` factors through the comparison
functor K : K`(P) → EM(P) to the Eilenberg-Moore category EM(P); and 2)

2

the extended functor PEM has a dual adjoint S. The situation is as follows.
CLV l\PK` = PEM ◦K op

S, (CLW )op ∼= EM(P)op
9

⊥
PEM
op

K

K`(P)

(2)

op

S
Here the functor K carries f : X → T Y to f † : PX → PY, P 7→ x∈P f (x)and is naturally thought of as a strongest postcondition semantics. Therefore
the picture (2)—understood as the one below—identifies a categorical structurethat underlies predicate transformer semantics. The adjunction here—it is in fact
an isomorphism in the specific instance of (2)—indicates a “duality” between
forward and backward predicate transformers.
S( backward predicate transformers ) oiweakest precondition
semantics⊥/( forward predicate transformers )6(computations)(3)strongest postcondition
semantics

Jacobs has identified other instances of (3) for: discrete probabilistic branching [16]; quantum logic [16]; and continuous probabilistic branching [17]. In allthese instances the notion of effect module—originally from the study of quantum probability [6]—plays an essential role as algebras of “quantitative logics.”
Towards Generic Weakest Precondition Semantics In [16, 17] the picture (3)is presented through examples and no categorical axiomatics—that induce thepicture—have been explicitly introduced. Finding such is the current paper’s
aim. In doing so, moreover, we acquire additional generality in two aspects:
different modalities and nested branching.
To motivate the first aspect, observe that the weakest precondition semantics
in (1) is the must semantics. The may variant looks as interesting; it would carrya postcondition Q ⊆ Y to {x ∈ X | f (x) ∩ Q 6= ∅}. The difference between thetwo semantics is much like the one between the modal operators 2 and 3.
On the second aspect, situations are abound in computer science where acomputation involves two layers of branching. Typically these layers correspondto two distinct players with conflicting interests. Examples are games, a twoplayer version of automata which are essential tools in various topics including
model-checking; and probabilistic systems where it is common to include nondeterministic branching too for modeling the environment’s choices. Further details
will be discussed later in §3.
Predicates and Modalities from Monads In this paper we present two categoricalsetups that are inspired by [4, 23]—specifically by their use of T 1 as a domainof truth values or quantities.
The first “one-player” setup is when we have only one layer of branching.
Much like in [16, 17] we start from a monad T . Assuming that T is orderenriched —in the sense that its Kleisli category K`(T ) is Posets-enriched—weobserve that:

3– a natural notion of truth value arises from an object T Ω (typically Ω = 1);– and a modality (like “may” and “must”) corresponds to a choice of an
Eilenberg-Moore algebra τ : T (T Ω) → T Ω.
The required data set (T, Ω, τ ) shall be called a predicate transformer situation.
We prove that it induces a weakest precondition semantics functor K`(T )op →Posets, and that it factors through K : K`(T ) → EM(T ), much like in (2).
The general setup addresses common instances like the original nondeterministic
one [5] and the probabilistic predicate transformers in [18,24]. Moreover it allows
us to systematically search for different modalities, leading e.g. to a probabilistic
notion of partial correctness guarantee (which does not seem well-known).
The other setup is the “two-player” one. It is much like a one-player setup
built on another, with two monads T and R and two “modalities” τ and ρ. A
potential novelty here is that R is a monad on EM(T ); this way we manage someknown complications in nested branching, such as the difficulty of combining
probability and nondeterminism. We prove that the data set (T, Ω, τ, R, ρ) gives
rise to a weakest precondition semantics, as before. Its examples include: a logic
of forced predicates in games; and the probabilistic predicate transformers in [31].
In this paper we focus on one side of predicate transformers, namely weakest
precondition semantics. Many components in the picture of [16,17] are therefore
left out. They include the adjoint S in (3), and the role of effect modules. Indeed,on the top-left corner of (3) we always have Posets which is less rich a structure
than complete lattices or effect modules. Incorporating these is future work.
Organization of the Paper In §2 we introduce our first “one-player” setup, andexhibit its examples. Our second “two-player” setup is first motivated in §3
through the examples of games and probabilistic systems, and is formally introduced in §4. Its examples are described in §5 in detail. In §6 we conclude.
ηX/ TX
Notations and Terminologies For a monad T , a T X
aalgebra T X → X shall always mean an Eilenberg( aidXMoore algebra for T , making the diagrams on the right(4)
Ta /
T (T X)
TX
commute. For categorical backgrounds see e.g. [1, 28].
µX 
aGiven a monad T on C, an arrow in the Kleisli cat/XTX
ap Y ; an identity arrow isegory K`(T ) is denoted by X →K`(T )
by idX ; and composition of arrows is by g f . These are to be distinguishedfrom X → Y , idX and g ◦ f in the base category C.

2Generic Weakest Preconditions, One-Player Setting

2.1

Order-Enriched Monad

We use monads for representing various notions of “branching.” These monads
are assumed to have order-enrichment (v for, roughly speaking, “more options”);
and this will be used for an entailment relation, an important element of logic.
The category Posets is that of posets and monotone functions.

4

Definition 2.1 An order-enriched monad T on a category C is a monad together with a Posets-enriched structure of the Kleisli category K`(T ).
The latter means specifically: 1) each homset K`(T )(X, Y ) = C(X, T Y ) carries aprescribed poset structure; and 2) composition in K`(T ) is monotone in eachargument. Such order-enrichment typically arises from the poset structure of T Y
in the pointwise manner. In the specific setting of C = Sets such enrichment canbe characterized by substitutivity and congruence of orders on T X; see [21].
Below are some examples of order-enriched monads. Our intuition about
an order-enriched monad T is that it represents one possible branching type,where ηX : X → T X represents the trivial branching with a unique option andµX : T (T X) → T X represents flattening ‘branching twice’ into ‘branching once’(see [13]). In fact each of the examples below has the Kleisli category K`(T )enriched by the category Cppo of pointed cpo’s and continuous maps—not justby Posets—and hence is suited for generic coalgebraic trace semantics [13].
Example 2.2 1. The lift monad L = 1 + ( )—where the element of 1 isdenoted by ⊥—has a standard monad structure induced by coproducts. For
example, the multiplication µL : 1 + 1 + X → 1 + X carries x ∈ X to itself
and both ⊥’s to ⊥. The set LX is a pointed dcpo with the flat order (⊥ v x
for each x ∈ X).
The lift monad L models the “branching type” of potential nontermination.
2. The powerset monad P models (possibilistic) nondeterminism. Its action
on arrows takes direct images: (Pf )U = {f (x) | x ∈ U }. Its unit is givenPby singletons:
ηX= { } : X → PX, and its multiplication is by unions:SPµX = : P(PX) → PX.
3. The subdistribution monad D models probabilistic branching. It carries a set
X to the set of (probability) subdistributions over X:P
DX := d : X → [0, 1];
x∈X d(x) ≤ 1
such d is called a subdistribution since the values need not add to 1. Givenan:=
P arrow f : X → Y in Sets, Df : DX → DY is defined by (Df )(d)(y)
D
(x)
=
d(x).
Its
unit
is
the
Dirac
(or
pointmass)
distribution:η−1x∈f ({y})P X
00D[ x 7→ 1; x 7→ 0 (for x 6= x)]; its multiplication is µX (a) = [x 7→ d∈DX a(d)·d(x)] for a ∈ D(DX).
Besides, the quantum branching monad Q is introduced in [12] for the purposeof modeling a quantum programming language that obeys the design principleof “quantum data, classical control.” It comes with an order-enrichment, too,
derived from the Löwner partial order between positive operators. Yet anotherexample is the continuous variant of D, namely the Giry monad on the category
Meas of measurable spaces [7].
2.2

PT Situation and Generic Weakest Precondition Semantics

We introduce our first basic setup for our generic weakest precondition semantics.
In our main examples we take C = Sets and Ω = 1 (a singleton).

5

Definition 2.3 (PT situation) A predicate transformer situation (a PT situation for short) over a category C is a triple (T, Ω, τ ) of
– an order-enriched monad T on C;– an object Ω ∈ C; and– an (Eilenberg-Moore) algebra τ : T (T Ω) → T Ω that satisfies the following
monotonicity condition: for each X ∈ C, the correspondence(Φτ )X : C(X, T Ω) −→ C(T X, T Ω) , i.e. K`(T )(X, Ω) −→ K`(T )(T X, Ω) ,


p
Tp
τ
given by X → T Ω 7−→ T X → T (T Ω) → T Ω
is monotone with respect to the order-enrichment of the Kleisli category
K`(T ) (Def. 2.1). Note here that Φτ : C( , T Ω) ⇒ C(T , T Ω) is nothing but
the natural transformation induced by the arrow τ via the Yoneda lemma.
The data τ is called a modality; see the introduction (§1) and also §2.3 below.
The following lemma gives a canonical (but not unique) modality for T .
Lemma 2.4 If T is an order-enriched monad, (T, Ω, µΩ ) is a PT situation.
Proof. We have only to check the monotonicity condition of µΩ in Def. 2.3. Itis easy to see that (ΦµΩ )X = µΩ ◦ T ( ) : C(X, T Ω) → C(T X, T Ω) is equal top X is the( ) (idT X )∧ : K`(T )(X, Ω) → K`(T )(T X, Ω). Here (idT X )∧ : T X →arrow that corresponds to the identity idT X in C. The claim follows from themonotonicity of .
tu
We shall derive a weakest precondition semantics from a given PT situation(T, Ω, τ ). The goal would consist of:– a (po)set PK` (τ )(X) of predicates for each object X ∈ C, whose order v
represents an entailment relation between predicates; and– an assignment, to each (branching) computation f : X → T Y in C, a predicate transformer
wpre(f ) : PK` (τ )(Y ) −→ PK` (τ )(X)

(5)

that is a monotone function.
p Y in K`(T ), we are aiming at a functor
Since a computation is an arrow f : X →PK` (τ ) : K`(T )op −→ Posets .

(6)Such a functor is known as an indexed poset, a special case of indexed categories.
These “indexed” structures are known to correspond to “fibered” structures(poset fibrations and (split) fibrations, respectively), and all these have beenused as basic constructs in categorical logic (see e.g. [15]). An indexed poset
like (6) therefore puts us on a firm footing.

6

Proposition 2.5 (the indexed poset PK` (τ )) Given a PT situation (T, Ω, τ ),the following defines an indexed poset PK` (τ ) : K`(T )op → Posets.1– On an object X ∈ K`(T ), PK` (τ )(X) := K`(T )(X, Ω) = C(X, T Ω).
p Y , PK` (τ )(f ) : C(Y, T Ω) → C(X, T Ω) is defined by– On an arrow f : X →q

Y → TΩ



7−→

f

Tq

τ

X → T Y → T (T Ω) → T Ω.

Proof. We need to check: the monotonicity of PK` (τ )(f ); and that the functor PK` (τ ) indeed preserves identities and composition of arrows. These will be
proved later, altogether in the proof of Thm. 2.10.
tu
A consequence of the proposition—specifically the functoriality of PK` (τ )—iscompositionality of the weakest precondition semantics: given two computations
f : X → T Y , g : Y → T U and a postcondition r : U → T 1, we havePK` (τ )(g

f )(r) = PK` (τ )(f ) PK` (τ )(g)(r)That is, the semantics of a sequential composition gby step.

2.3



.

f can be computed step

Examples of PT Situations

For each of T = L, P, D in Example 2.2, we take Ω = 1 and the set T 1 isnaturally understood as a set of “truth values” (an observation in [4, 23]):(ff := ⊥) (tt := 1) 
,

P1 =

v

v

 (tt := ∗) 
L1 =,and D1 =[0, 1], ≤.

(ff := ∅)Here ∗ is the element of the argument 1 in L1. Both L1 and P1 represent theBoolean truth values. In the D case a truth value is r ∈ [0, 1]; a predicate, beinga function X → [0, 1], is hence a random variable that tells the certainty withwhich the predicate holds at each x ∈ X.
We shall introduce modalities for these monads T and Ω = 1. The following
observation (easy by diagram chasing) will be used.
Lemma 2.6 The category EM(T ) of Eilenberg-Moore algebra is iso-closed in
the category of functor T -algebras. That is, given an Eilenberg-Moore algebra∼=a : T X → X, an arrow b : T Y → Y , and an isomorphism f : X →Y such thatf ◦ a = b ◦ T f , the arrow b is also an Eilenberg-Moore algebra.
tu
1

For brevity we favor the notation PK` (τ ) over more appropriate PK` (T, Ω, τ ).

7

The Lift Monad L: τtotal and τpartial We have the following two modalities(and none other, as is easily seen).
τtotal , τpartial : {⊥} + {tt, ff} = L(L1) −→ L1 = {tt, ff} ,τtotal : ⊥ 7→ ff , tt 7→ tt , ff 7→ ff ,τpartial : ⊥ 7→ tt , tt 7→ tt , ff 7→ ff .
The one we obtain from multiplication µL
1 is τtotal ; the other τpartial is nonethelessimportant in program verification. Given q : Y → L1 and f : X → LY where f
is understood as a possibly diverging computation from X to Y , the predicate
PK` (τpartial )(f )(q) = τpartial ◦ Lq ◦ f:

X −→ L1

carries x ∈ X to tt in case f (x) = ⊥, i.e., if the computation is diverging. Thisis therefore a partial correctness specification that is common in Floyd-Hoare
logic (see e.g. [37]). In contrast, using τtotal , the logic is about total correctness.
The Powerset Monad P: τ3 and τ2 The monad multiplication µP
1 yields a
modality which shall be denoted by τ3 . The other modality τ2 is given via the∼=swapping σ : P1 →
P1:
P(P1)
τ2 
P1 o

Pσ
∼
=

/ P(P1)

∼
=
σ

P1 ;

 τ3

explicitly,τ3 {} = ff, τ3 {tt} = tt, τ3 {ff} = ff, τ3 {tt, ff} = tt;
τ2 {} = tt, τ2 {tt} = tt, τ2 {ff} = ff, τ2 {tt, ff} = ff.

(7)
In view of Lem. 2.6, we have only to check that the map τ2 satisfies the monotonicity condition in Def. 2.3. We first observe that, for h : X → P1 and U ∈ PX,(τ2 ◦ Ph)(U ) = ff⇐⇒

ff ∈ (Ph)(U )⇐⇒∃x ∈ U. h(x) = ff ,p 1 and
where the first equivalence is by (7). Now assume that f v g : X →(τ2 ◦ Pg)(U ) = ff. For showing τ2 ◦ Pf v τ2 ◦ Pg it suffices to show that(τ2 ◦ Pf )(U ) = ff; this follows from the above observation.
The modalities τ3 and τ2 capture the may and must weakest preconditions,
respectively. Indeed, given q : Y → P1 and f : X → PY , we have PK` (τ3 )(f )(q)(x) =tt if and only if there exists y ∈ Y such that y ∈ f (x) and q(y) = tt; andPK` (τ2 )(f )(q)(x) = tt if and only if y ∈ f (x) implies q(y) = tt.
Moreover, we can show that τ3 and τ2 are the only modalities (in the senseof Def. 2.3) for T = P and Ω = 1. Since the unit law in (4) forces τ {tt} = tt
and τ {ff} = ff, the only possible variations are the following τ1 and τ2 (cf. (7)):τ1 {} = tt , τ1 {tt, ff} = tt ;

τ2 {} = ff , τ2 {tt, ff} = ff .

Both of these, however, fail to satisfy the multiplication law in (4).
 Pτ1 / {tt, ff}{{}, {ff}}
_
S _
P1 
 τ1

/
=
6
{ff} τ1 ff
tt/ {tt, ff}{{}, {tt}} 
_
S _
P1 
 τ2

/
=
6
{tt} τ2 tt
ff
Pτ2

8

The monotonicity condition in Def. 2.3, in the case of T ∈ {L, P} (henceTΩ ∼= 2), coincides with monotonicity of a predicate lifting 2( ) ⇒ 2T ( ) . The
latter is a condition commonly adopted in coalgebraic modal logic (see e.g. [25]).
The Subdistribution Monad D: τtotal and τpartial The modality τtotal : D[0, 1] →[0, 1] that arises from the multiplication µDsuch that: given q : Y → D1 and1 is Pf : X → DY , we have PK` (τtotal )(f )(q)(x) = y∈Y q(y) · f (x)(y). This is precisely the expected value of the random variable q under the distribution f (x);thus τtotal yields the probabilistic predicate transformer of [18, 24].
∼=
In parallel to the powerset monad case, we have an isomorphism σ : D1 →D1, p 7→ 1−p. Another modality τpartial : D[0, 1] → [0, 1] then arises by τpartial :=σ ◦ τtotal ◦ Dσ like in (7), for which we have PPτpartial (d) = 1 − r∈[0,1] d(r) + r∈[0,1] r · d(r) and P
PPK` (τpartial )(f )(q)(x) = 1 − y∈Y f (x)(y) + y∈Y q(y) · f (x)(y) .
PIn the second line, the value 1− y∈Y f (x)(y)—the probability of f ’s divergence—is added to the τtotal case. Therefore the modalities τpartial and τtotal , much likein the case of T = L, carry the flavor of partial and total correctness guarantee.
To see that τpartial is indeed a modality is easy: we use Lem. 2.6; and themonotonicity can be deduced from the following explicit presentation of τpartial ◦Dp for p : X → D1 = [0, 1]. For each d ∈ DX,hiP(τpartial ◦ Dp)(d) = τpartial r 7→ x∈p−1 ({r}) d(x)r∈[0,1] P
PPP= 1 − r∈[0,1] x∈p−1 ({r}) d(x) + r∈[0,1] r x∈p−1 ({r}) d(x) PP
= 1 − x∈X d(x) + x∈X p(x) · d(x) .
We do not yet know if τtotal and τpartial are the only modalities for D and Ω = 1.
Remark 2.7 We note the difference between a subdistribution d ∈ DX and a
predicate (i.e. a random variable) p : X → D1. An example of the latter is p>that is everywhere 1—this is the truth predicate.
PIn contrast, the former d ∈ DX
is subject to the (sub)normalization condition x d(x) ≤ 1. We understand it as
one single “current state” whose whereabouts are known only probabilistically.
2.4

Factorization via the Eilenberg-Moore Category

The indexed poset PK` (τ ) : K`(T )op → Posets in Prop. 2.5 is shown here to
factor through the comparison functor K : K`(T ) → EM(T ), much like in (2). In
fact it is possible to see K as a strongest postcondition semantics; see Rem. 2.11.
We will be using the following result.
Lemma 2.8 Let T be an order-enriched monad on C, X, Y, U ∈ C and f : X →Y be an arrow in C. Then ( ) ◦ f : C(Y, T U ) → C(X, T U ) is monotone.

9

Proof. Given g : Y → T U in C,g ◦ f = µU ◦ ηT U ◦ g ◦ f = µU ◦ T g ◦ T f ◦ ηX = µU ◦ T g ◦ T f ◦ µX ◦ ηT X ◦ ηX
Tf
g
JηX

p TX →p Y →p U ,= µU ◦ T g ◦ µY ◦ T (T f ) ◦ ηT X ◦ ηX = X →where J : Sets → K`(T ) is the Kleisli inclusion that sends the arrow ηX : X →p T X. In the calculation we used the monad laws as well
T X to ηT X ◦ ηX : X →as the naturality of η and µ. The correspondence ( ) (T f JηX ) is monotone
by assumption (Def. 2.1); this proves the claim.
tu
Proposition 2.9 (the indexed poset PEM (τ )) A PT situation (T, Ω, τ ) induces an indexed poset PEM (τ ) : EM(T )op → Posets in the following way.
– On objects,
PEM (τ )TX 
T X T (T Ω) ↓a:= EM(T ) ↓a , ↓τX
XTΩ

where the order v on the set EM(T )(a, τ ) is inherited from C(X, T Ω) via
the forgetful functor U T : EM(T ) → C.
ab
– On an arrow f : (T X → X) → (T Y → Y ),PEM (τ )(f ) : EM(T )T Y T (T Ω) 
T X T (T Ω) ↓b ,↓τ−→ EM(T ) ↓a , ↓τ
,
Y
X
TΩ
TΩ

q 7−→ q ◦ f .

Proof. The monotonicity of PEM (τ )(f ) follows from the order-enrichment of T
via Lem. 2.8. The functoriality of PEM (τ ) is obvious.
tu
Theorem 2.10 For a PT situation (T, Ω, τ ), the following diagram commutes
up-to a natural isomorphism. Here K is the comparison functor.
PEM (τ )Posets cp
P

K`

(τ )

Ψ ⇑∼
=
op

K`(T )op

9 EM(T )

(8)

K op

Proof. (Also of Prop. 2.5) The natural isomorphism Ψ in question is of the type
ΨX :

∼
=

PK` (τ )(X) = C(X, T Ω) −→ EM(T )T (T X) T (T Ω) ↓µX ,↓τ
= PEM (τ )(KX)
TX
TΩ

and it is defined by the adjunction C(X, U T τ ) ∼= EM(T )(µX , τ ) where U T is the


p
Tp
τ
forgetful functor. Explicitly: ΨX X → T Ω = T X → T (T Ω) → T Ω ; and its


f
ηX
f
−1
inverse is ΨX
T X → T Ω = X → T X → T Ω . The function ΨX is monotonic−1by the monotonicity of τ , see Def. 2.3; so is its inverse ΨX
by Lem. 2.8.
p Y in K`(T ), it requires
Let us turn to naturality of Ψ . Given f : X →C(Y, T Ω)PK` (τ )(f ) = τ ◦T ( )◦f 
C(X, T Ω)

ΨY
∼
=
ΨX
∼
=

/ EM(T )(µY , τ ) PEM (τ )(Kf ) = ( )◦µY ◦T f
/ EM(T )(µX , τ ) .

(9)

10

Indeed, given q : Y → T Ω,PEM (τ )(Kf )(ΨY q) = PEM (τ )(Kf )(τ ◦ T q) = τ ◦ T q ◦ µY ◦ T f= τ ◦ µT Ω ◦ T (T q) ◦ T f = τ ◦ T τ ◦ T (T q) ◦ T f = ΨX ◦ PK` (τ )(f ) q ,where the third equality is naturality of µ and the fourth is the multiplication
law of τ (see (4)). By this naturality, in particular, we have that PK` (τ )(f ) ismonotone (since the other three arrows are monotone). This is one property
needed in Prop. 2.5; the other—functoriality of PK` (τ )—also follows from naturality of Ψ , via the functoriality of K and PEM (τ ).
tuRemark 2.11 The comparison functor K : K`(T ) → EM(T ) can be seen as astrongest postcondition semantics. Given a (branching) computation f : X →T Y , we obtainspost(f ) := µY ◦ T f : T X −→ T Y
that is an algebra morphism Kf between free algebras. When T = P this indeed
yields a natural notion: concretely it is given by spostP (f )(S) = {y | ∃x ∈ S. y ∈f x}; here we think of subsets as predicates. Some remarks are in order.
Firstly, note that the notion of predicate here diverges in general from theone in the weakest precondition semantics. This is manifest when T = D: theformer is a subdistribution d ∈ DX (“partial information on the current state’s
whereabouts”, see Rem. 2.7), while the latter is a random variable p : X → [0, 1].
Secondly, there is no notion of modality involved here. This is unsatisfactory because, besides the above strongest postcondition semantics spostP (f ) for
T = P that carries the “may” flavor, the “must” variant spostP
must (f ) is also
conceivable such that spostP
must (f )(S) = {y | ∀x ∈ S. y ∈ f x}. This does notarise from the comparison functor K.

3

The Two-Player Setting: Introduction

We extend the basic framework in the previous section by adding another layerof branching. This corresponds to adding another “player” in computations or
systems. The additional player typically has an interest that conflicts with theoriginal player’s: the former shall be called Opponent and denoted by O, while
the latter (the original player) is called Player P.2
The need for two players with conflicting interests is pervasive)x1
in computer science. One example is the (nowadays heavy) use of x0 i
games in the automata-theoretic approach to model checking (see) 
x3e.g. [8]). Games here can be understood as a two-player version of x2 i
automata, where it is predetermined which player makes a move in each state.
An example is above on the right, where P-states are x0 , x3 and O-states are
x1 , x2 . Typical questions asked here are about what Player P can force: can P
force that x3 be reached? (yes); can P force that x0 be visited infinitely often?
2

Note that (capitalized) Player and Opponent are altogether called players.

11(no). In model checking, the dualities between ∧ and ∨, ν and µ, etc. in themodal µ-calculus are conveniently expressed as the duality between P and O;
and many algorithms and proofs rely on suitably formulated games and resultson them (such as the algorithm in [19] that decides the winner of a parity game).
Games have also been used in the coalgebraic study of fixed-point logics [26].
Another example of nested two-player branching is found in the processtheoretic study of probabilistic systems; see e.g. [3, 33]. There it is common to
include nondeterministic branching too: while probabilistic branching models
the behavior of a system (such as a stochastic algorithm) that flips an internalcoin, nondeterministic branching models the environment’s behavior (such as
requests from users) on which no statistical information is available. In thiscontext, probabilistic branching is often called angelic while nondeterministic
one is demonic; and a common verification goal would be to ensure a property—
with a certain minimal likelihood—whatever demonic choices are to be made.
3.1

Leading Example: Nondeterministic P and Nondeterministic O

Let us first focus on the simple setting where: P moves first and O moves second,in each round; and both P and O make nondeterministic choices. This is a setting
suited e.g. for bipartite games where P plays first. A computation with suchbranching is modeled by a function
f : X −→ PP (PO Y ) ,(10)

where the occurrences of the powerset functor P are annotated to indicate whichof the players it belongs to (hence PP = PO = P). We are interested in what
P can force; in this logic of forced predicates, the following notion of (pre)order
seems suitable.
a v b in PP (PO Y )

def.

⇐⇒

∀S ∈ a. ∃S 0 ∈ b. S 0 ⊆PO Y S(11)That is: if a can force Opponent to S ⊆ Y , then b—that has a greater power—
can force Opponent to better (i.e. smaller) S 0 ⊆ Y .
In fact, we shall now introduce a modeling alternative to (10) which uses
up-closed families of subsets, and argue for its superiority, mathematical andconceptual. It paves the way to our general setup in §4.
For a set Y , we define UPY to be the collection of up-closed families ofsubsets of Y , that is,
UPY :=

a ⊆ PY∀S, S 0 ⊆ Y. (S ∈ a ∧ S ⊆ S 0 ⇒ S 0 ∈ a)

.

(12)

On UPY we define a relation v by: a v b if a ⊆ b. It is obviously a partial order.
Lemma 3.1 1. For each set Y , the relation v in (11) on PP (PO Y ) is a preorder. It is not a partial order.

12

2. For a ∈ PP (PO Y ), let ↑ a := {S | ∃S 0 ∈ a. S 0 ⊆ S} be its upward closure. Then the following is an equivalence of (preorders considered to be)
categories; here ι is the obvious inclusion map.
UPY u

↑( )

4 PP (PO Y )'ιProof. For 1., reflexivity and transitivity of v is obvious. To see it is not antisymmetric consider {∅, Y } and {∅}.
For 2., ι is obviously monotone. If a v b in PP (PO Y ), for any S ∈ ↑ a there
exists S 0 ∈ b such that S 0 ⊆ S, hence S ∈ ↑ b. Therefore ↑( ) is monotone too.
Obviously ↑( ) ◦ ι = id.
It must be checked that ι(↑ a) ' a for a ∈ PP (PO Y ), where ' is the equivalence induced by v. The v direction is immediate from the definition of ↑ a; forthe other direction, observe that in general a ⊆ b implies a v b in PP (PO Y ). tu
Proposition 3.2 For each set Y , (UPY, v) is the poset induced by the preorder
PP (PO Y ), v . Moreover (UPY, v) is a complete lattice.
Proof. The first half is immediate from Lem. 3.1. For the latter, observe thatsupremums are given by unions.
tu
The constructions PP (PO ) and UP have been studied from a coalgebraic
perspective in the context of neighborhood frames [9, 10]. There a coalgebra for
the former is a model of non-normal modal logic (meaning that axioms like
2p ∧ 2q → 2(p ∧ q) and 2p → 2(p ∨ q) can fail); one for the latter is a modelof monotone modal logic (meaning that validity of 2p → 2(p ∨ q) is retained).
Prop. 3.2 shows that, as long as our interests are game-theoretic and are in the
logical reasoning with respect to the preorder v in (11), we may just as well use
UP which is mathematically better-behaved.
To argue further for the mathematical convenience of UP , we look at its
faction on arrows. For PP (PO ) there are two obvious choices (PPf and 22 ) ofaction on arrows, arising from the covariant and contravariant powerset functors,
respectively. Given f : X → Y in Sets,f

PPf, 22 : PP (PO X) −→ PP (PO Y ) ,(PPf )a := {qf S | S ∈ a} ,f

22 a := {T ⊆ Y | f −1 T ∈ a} .

Here qf S is the direct image of S by f .
These two choices are not equivalent with respect to v on PP (PO Y ). Inff
general we have 22 a v (PPf )a. To see that, assume U ∈ 22 a, i.e. f −1 U ∈ a.
−1
−1
Then qf (f U ) ⊆ U (a general fact) and qf (f U ) ∈ (PPf )a. However thefconverse 22 a w (PPf )a can fail: consider ! : 2 → 1 (where 2 = {0, 1}) andfa = {{0}}; then 22 a = ∅ while (PPf )a = {1}.

13This discrepancy is absent with UP . For a function f : X → Y , the “covariant” action UPf and the “contravariant” action UP 0 f are defied as follows.
UPXι 
PP (PO X)

UPf

/ UPY
O

↑( )

PPf

/ PP (PO Y )UPXPP (PO X)

UP 0 f

f

22

/ UPY

/ PP (PO Y )

(13)

f

On the left, ι and ↑( ) are as in Lem. 3.1. On the right 22 restricts to UPX →UPY (easy by the fact that f −1 is monotone); on the left such is not the case(consider f : 1 → 2, 0 7→ 0 and a = {1}) and we need explicit use of ↑( ).
Lemma 3.3 UPf = UP 0 f .
Proof. Let a ∈ UPX (hence up-closed). In view of Lem. 3.1, it suffices to showfthat 22 a ' (PPf )a; we have already proved the v direction. For the otherffdirection, let S ∈ a; proving qf S ∈ 22 a will prove (PPf )a ⊆ 22 a, hencef(PPf )a v 22 a. That S ⊆ f −1 (qf S) is standard; since a is up-closed we haveff −1 (qf S) ∈ a. Therefore qf S ∈ (22 )a.
tu
We therefore define UP : Sets → Sets by (12) on objects and either of theactions in (13) on arrows. Its functoriality is obvious from (13) on the right.
3.2

Nondeterministic O, then Probabilistic P: Search for Modularity

We have argued for the convenience of the functor UP, over PP (PO ), for modeling two-layer branching in games. A disadvantage, however, is that modularity islost. Unlike PP (PO ), the functor UP : Sets → Sets is not an obvious composite
of two functors, each of which modeling each player’s choice.
The same issue arises also in the systems with both probabilistic and nondeterministic branching (briefly discussed before). It is known (an observation
by Gordon Plotkin; see e.g. [35]) that there is no distributive law DP ⇒ PD of
the subdistribution monad D over the powerset monad P. This means we cannot compose them to obtain a new monad PD. Two principal fixes have been
proposed: one is to refine D into the indexed valuation monad that distinguishes
e.g. [x 7→ 1/2, x 7→ 1/2] from [x 7→ 1] (see [35]). The other way (see e.g. [34])replaces P by the convex powerset construction and usesPP
CDX := {a ⊆ DX | pi ∈ [0, 1], i pi = 1, di ∈ a ⇒ i pi di ∈ a}in place of PD, an alternative we favor due to our process-theoretic interests(see Rem. 5.8 later). However, much like with UP, it is not immediate how todecompose CD into Player and Opponent parts.
We now introduce a categorical setup that addresses this issue of separating
two players. It does so by identifying one layer of branching—like up-closed
powerset and convex powerset—as a monad on an Eilenberg-Moore category.

14

4

Generic Two-Player Weakest Precondition Semantics

Definition 4.1 (2-player PT situation) A 2-player predicate transformer situation over a category C is a quintuple (T, Ω, τ, R, ρ) where:– (T, Ω, τ ) is a PT situation (Def. 2.3), where in particular τ : T (T Ω) → T Ω
is an Eilenberg-Moore algebra;– R is a monad on the Eilenberg-Moore category EM(T ); andT (T Ω) T (T Ω) ↓τ↓τ→is an Eilenberg-Moore R-algebra, that is also– ρ: RTΩ
TΩ
called a modality. It is further subject to the monotonicity condition that ismuch like in Def. 2.3: the map
TX

EM(T )( ↓a ,X

T (T Ω)↓τ ) −→ EM(T )TΩR

T X  T (T Ω) 
↓a ,
↓τ
,
X
TΩ

f 7−→ ρ ◦ Rf

is monotone for each algebra a. Here the order of each homset is induced by
UT

the enrichment of K`(T ) via EM(T )(b, τ ) → C(U T b, T Ω) = K`(T )(U T b, Ω).
The situation is as in the following diagram.

U T U RF RF T
= U T RF T



T

t
9 CO

UT
>

 q
2 EM(T )
R

FT

UR
>
FR

1 EM(R)
O

(14)

K
T
T
/ K`(U RF )>The composite adjunction yields a new monad U T U R F R F T = U T RF T on C;
then from the Kleisli category K`(U T RF T ) for the new monad we obtain acomparison functor to EM(R). It is denoted by K.
We have a monad R on EM(T ) and an algebra (modality) ρ for it. This ismuch like in the original notion of PT situation, where τ : T (T Ω) → T Ω is amodality from which we derived a weakest precondition semantics. Indeed, thefollowing construction is parallel to Prop. 2.9.
Proposition 4.2 (the indexed poset PEM (τ, ρ)) A 2-player PT situation(T, Ω, τ, R, ρ) induces an indexed poset PEM (τ, ρ) : EM(R)op → Posets over
EM(T ) by:– on an object α ∈ EM(R),
a

EM

P

(τ, ρ)

 R(T X →X) ↓αa(T X →X)a:= EM(R)τ

R(T X →X) R(T (T Ω)→T Ω)

↓α
↓ρ
,
a
τ
(T X →X)(T (T Ω)→T Ω)

where the order v on the set EM(R)(α, ρ) is inherited from C(X, T Ω) via
the forgetful functors EM(R) → EM(T ) → C; and15– on an arrow f :

Ra 
↓α →
a

Rb 
↓β ,
b

Rb
Rτ 
↓β , ↓ρ −→ EM(R)
Rτ
b

Ra
Rτ 
↓α , ↓ρ,aτ

q 7−→ q ◦ f .

Proof. The same as the proof of Prop. 2.9, relying on Lem. 2.8.

tu

PEM (τ, ρ)(f ) : EM(R)

Much like in Thm. 2.10, composition of the indexed poset PEM (τ, ρ) : EM(R)op →Posets and the comparison functor K : K`(U T RF T ) → EM(R) will yield theweakest precondition calculus. The branching computations of our interest are
therefore of the type X → U T RF T Y . We will later see, through examples, that
this is indeed what models the scenarios in §3.
Note that in what follows we rely heavily on the adjunction F T a U T .
Proposition 4.3 (the indexed poset PK` (τ, ρ)) A 2-player PT situation(T, Ω, τ, R, ρ) induces an indexed poset PK` (τ, ρ) : K`(U T RF T )op → Posets by:– on an object X ∈ K`(U T RF T ), PK` (τ, ρ)(X) := K`(T )(X, Ω) = C(X, T Ω);
p Y in K`(U T RF T ), it induces an arrow f ∧ : F T X →– given an arrow f : X →T
R(F Y ) in EM(T ); this is used in
EM(T )(F T Y, τ ) → EM(T )(F T X, τ ) ,


f∧
Rq
ρ
q 7−→ F T X → R(F T Y ) → Rτ → τ .

The last map defines an arrow PK` (τ, ρ)(f ) : PK` (τ, ρ)(Y ) → PK` (τ, ρ)(X)
since we have PK` (τ, ρ)(U ) = C(U, T Ω) ∼= EM(T )(F T U, τ ).
We have the following natural isomorphism, where K is the comparison in (14).
PEM (τ,ρ)Posets fp
PK` (τ,ρ)Ξ•Ψ ⇑∼=T
T op

K`(U RF )op

7 EM(R)

(15)

K op

Proof. Note here that the comparison functor K is concretely described as follows: KX = F R (F T X) on objects, and use the correspondence∼ EM(T )(F T X, U R F R F T Y )K`(U T RF T )(X, Y ) = C(X, U T U R F R F T Y ) =∼= EM(R)(F R F T X, F R F T Y ) = EM(R)(KX, KY )for its action on arrows. We claim that the desired natural isomorphism Ξ • Ψis the (vertical) compositeΨXPK` (τ, ρ)(X) = C(X, T Ω) −→EM(T )(F T X, τ )ΞX−→
EM(R)(F R F T X, ρ) = PEM (τ, ρ)(KX)

where Ψ and Ξ are isomorphisms induced by adjunctions.
We have to check that ΨX and ΞX are order isomorphisms. The map ΨX−1
is monotone due to the monotonicity condition on τ (Def. 2.3); so is ΨX

16

by Lem. 2.8. Similarly, ΞX is monotone by the monotonicity condition on ρ
−1(Def. 4.1); so is ΞX
by Lem. 2.8.
We turn to the naturality: the following diagram must be shown to commute,p Y in K`(U T RF T ).
for each f : X →C(Y, T Ω)PK` (τ,ρ)(f ) C(X, T Ω)

ΨY
∼
=
ΨX
∼
=

/ EM(T )(F T Y, τ )ΞY∼=/ EM(R)(F R (F T Y ), ρ) ρ◦R( )◦f PEM (τ,ρ)(Kf ) = ( )◦Kf
/ EM(T )(F T X, τ ) ΞX / EM(R)(F R (F T Y ), ρ) .
∧

∼
=

(16)
The square on the left commutes by the definition of PK` (τ, ρ)(f ) (Prop. 4.3);
the one on the right is much like the one in (9) and its commutativity can be∧proved in the same way. Note here that Kf = µR
F T Y ◦ R(f ).
Since the diagram (16) commutes, and since Ψ and Ξ are order isomorphisms
and PEM (τ, ρ)(Kf ) is monotone (Prop. 4.2), we have that PK` (τ, ρ)f is monotone.
The functoriality of PK` (τ, ρ) is easy, too. This concludes the proof.
tu5

Examples of 2-Player PT Situations

5.1

Nondeterministic Player and then Nondeterministic Opponent

We continue §3 and locate the monad UP—and the logic of forced predicates—in
the general setup of §4. We identify a suitable 2-player PT situation(P, 1, τ2 , RG , ρP ), in which T = P, Ω = 1 and τ = τ2 that is from §2.3. The
choice of τ2 corresponds to the demonic nature of Opponent’s choices: Player
can force those properties that hold whatever choices Opponent makes.
To introduce the monad RG on EM(P)—corresponding to the up-closed powerset construction—we go via the following standard isomorphism.
PX 
Lemma 5.1 Let C : EM(P) → CLV be the functor such that C ↓a := (X, va
X), where the order is defined by x va y if x = a{x, y}. Conversely, let D : CLV →PX
V
↓EM(P) be such that D(X, v) :=. Both act on arrows as identities.
X∼=
Then C and D constitute an isomorphism EM(P) →
CLV .

t
u

The monad RG is then defined to be the composite RG := D ◦ Dw ◦ C, using
the down-closed powerset monad Dw on CLV .

RG

9 EM(P)

q

D
∼
=

2 CL

V

y

Dw

(17)

C

The switch between up-closed subsets in UP and down-closed subsets Dw may
seem confusing. Later in Prop. 5.3 it is shown that everything is in harmony; and∼=after all it is a matter of presentation since there is an isomorphism CLV →CLWthat reverses the order in each complete lattice. The switch here between up-

17

and down-closed is essentially because: the bigger the set of Opponent’s options
is, the smaller the power of Player (to force Opponent to somewhere) is.
Concretely, the monad Dw : CLV → CLV carries a complete lattice (X, v)
to the set DwX := {S ⊆ X | x v x0 , x0 ∈ S ⇒ x ∈ S}. We equip DwX
with the inclusion order; this makes DwX a complete lattice, with sups and infs
given by unions and intersections, respectively. An arrow f : X → Y is carried to
Dwf : DwX → DwY defined by S 7→ ↓(qf S). Here ↓( ) denotes
V the downward
closure and it is needed to ensure down-closedness (consider a -preserving map
f : 1 → 2, 0 7→ 1 where 0 v 1 in 2). The monad structure of DwSis given by:
DwηX: X → DwX, x 7→V↓{x}; and µDw
a. Note in
X : Dw(DwX) → DwX, a 7→
Dw
particular that ηX
is -preserving. As in (17) we define RG := D ◦ Dw ◦ C.
Finally, let us define the data ρP : RG (τ2 ) → τ2 in the 2-player PT situation.
Via the isomorphism (17) we shall think of it as an Dw-algebra, where the Palgebra τ2 is identified with the 2-element complete latticeV[ff v tt] (the order
is because τ2 {tt, ff} = ff). Therefore we are looking for a -preserving map
Dw[ff v tt] =

∅ v {ff} v {ff, tt}

 CρP−→ [ff v tt]

subject to the conditions of an Eilenberg-Moore algebra in (4). In fact such C(ρP )is uniquely determined: preservation of > forces (CρP ){ff, tt} = tt; the unit law
forces (CρP ){ff} = ff and monotonicity of CρP then forces (CρP )∅ = ff.
Lemma 5.2 (P, 1, τ2 , RG , ρP ) thus obtained is a 2-player PT situation.
Proof. It remains to check the monotonicity condition(Def. 4.1) for ρP . We
Vshall again think in terms of complete lattices and -preserving maps; then thefρP ◦Dwf
requirement is that the map X → [ff v tt] 7→ DwX → [ff v tt] ismonotone. Assume g v f , S ∈ DwX and (ρP ◦ Dwf )(S) = ff. It suffices to showthat (ρP ◦ Dwg)(S) = ff; this follows from the observation that, for h = f or g,(ρP ◦ Dwh)(S) = ff ⇐⇒ (Dwh)S ⊆ {ff} ⇐⇒ ∀x ∈ S. hx = ff .

tu

Let us check that the logic PK` (τ2 , ρP ) associated with this 2-player PT situation is indeed the logic of forced predicates in §3.1. For instance, we want“computations” X → U P RG F P Y to coincide with “computations” X → UPY .
Proposition 5.3 For any set X we have U P RG F P = UPX. In fact they are
isomorphic as complete lattices, that is, Dw ◦ C ◦ F P = UP : Sets → CLV
where the functor UP is equipped with the inclusion order.
Proof. Given X ∈ Sets, the definition of C dictates that C(F P X) = (PX, ⊇)and its order be given by the reverse inclusion order. Hence Dw(C(F P X)) is thecollection of families a ⊆ PX that are ⊇-down-closed, i.e. ⊆-up-closed. It is easily
checked that the two functors coincide on arrows, too, using the characterizationon the left in (13).
t
u

18

Next we describe the logic PK` (τ2 , ρP ) (Prop. 4.3) in concrete terms. We baseourselves again in CLV via the isomorphism EM(P) ∼= CLV in (17). Consider
a postcondition q : Y → P1 and a branching computation f : X → UPY . These
are in one-to-one correspondences with the following arrows in CLV :q ∧ : C(F P Y ) = (PY, ⊇) −→ [ff v tt] = C(τ2 ) ,f ∧ : C(F P X) = (PX, ⊇) −→ Dw(PY, ⊇) = C(RG (F P Y )) ,V
where we used Prop. 5.3. Since q ∧ are f ∧ are -preserving, we haveS
VVVq ∧ W = q ∧ ( y∈W {y}) = q ∧ ( y∈W {y}) = y∈W q ∧ {y} = y∈W qy ;Tand similarly f ∧ S = x∈S f x. Recall that Dw(PY, ⊇) has the inclusion order.
Now Prop. 4.3 states that the weakest precondition PK` (τ2 , ρP )(f )(q) is thearrow X → P1 that corresponds, via the adjunction C ◦ F P a U P ◦ D, toDw(q ∧ )f∧

ρP(PX, ⊇) −→ Dw(PY, ⊇) −→ Dw[ff v tt] −→ [ff v tt]

in CLV .

Unweaving definitions it is straightforward to see that, for S ⊆ X,ρP ◦ Dw(q ∧ ) ◦ f ∧ S = tt ⇐⇒ ∃W ⊆ Y. ∀x ∈ S. W ∈ f x ∧ ∀y ∈ W. qy = tt ;therefore PK` (τ2 , ρP )(f )(q)(x) = tt ⇐⇒ ∃W ⊆ Y. W ∈ f x ∧ ∀y ∈ W. qy = tt .
(18)
The last condition reads: among the set f x of possible moves of Player, there
exists a move W , from which q holds no matter what Opponent’s move y is.
Therefore PK` (τ2 , ρP )(f )(q)(x) = tt if Player can force the predicate q from x
after the (two-layer branching) computation f .
5.2

Nondeterministic Opponent and then Nondeterministic Player

We change the order of Player and Opponent: O moves first and then P moves.
The general setup in §4 successfully models this situation too, with a choice ofa 2-player PT situation (P, 1, τ3 , RG , ρO ) that is dual to the previous one.
The modality τ3 is from §2.3. Although the monad RG is the same as in §5.1,
we now prefer to present it in terms of EM(P) ∼= CLW instead of CLV . The
reason is that this way the algebra τ3 gets identified with [ff v tt], which is
intuitive. The situation is as follows.
D 0 :=D◦D 00

RGq
9 EM(P)

D
∼
=

Dw

2



r
CLV

C

D 00
∼
=
C

00

2 CL O

W

y

Up

(19)

C 0 :=C 00 ◦C

The functors C 00 and D00 carries a complete lattice (X, v) to (X, w), reversing
the order. The monad Up is defined by Up := C 00 ◦ Dw ◦ D00 ; concretely it carries

19(X, v) to the set of its up-closed subsets, equipped with the reverse inclusion
order ⊇. That is,Up(X, v) := {S ⊆ X | S 3 x v x0 ⇒ x0 ∈ S} , ⊇ .
We have RG = D ◦ Dw ◦ C = D0 ◦ Up ◦ C 0 .
The modality ρO : RG (τ3 ) → τ3 is identified, W
via the isomorphism C 0 in (19),with an Up-algebra on [ff v tt]. The latter is a -preserving map
 C 0 ρO
Up[ff v tt] = {ff, tt} v {tt} v ∅ −→ [ff v tt] ;note here that the order in Up(X, v) is the reverse inclusion ⊇. Such C 0 ρO is
uniquely determined (as before): the unit law forces (C 0 ρO ){tt} = tt; preservation of ⊥ forces (C 0 ρO ){tt, ff} = ff; and then by monotonicity (C 0 ρO )∅ = tt.
It is straightforward to see that (P, 1, τ3 , RG , ρO ) is indeed a 2-player PT
situation; the proof is symmetric to the one in §5.1. Also symmetrically, theweakest precondition semantics PK` (τ3 , ρO ) is concretely described as follows:
given a postcondition q : Y → P1 and a branching computation f : X → UPY ,
PK` (τ3 , ρO )(f )(q)(x) = tt ⇐⇒ ∀W ⊆ Y. W ∈ f x ⇒ ∃y ∈ W. qy = tt .

This is dual to (18) and reads: whatever move W Opponent takes, there exists
Player’s move y ∈ W so that q holds afterwards.
We note that the analogue of Prop. 5.3 becomes: Up ◦ C 0 ◦ F P = UP : Sets →CLW , where each UPX is equipped with the reverse inclusion order. This order(a v b in UPX if a ⊇ b) is intuitive if we think of v as the power of Player.
Remark 5.4 The constructions have been described in concrete terms; this isfor intuition. An abstract view is possible too: the modality τ3 is the dual of τ2
via the swapping σ (see (7)); and the other modality ρO is also the dual of ρP

ρP
RG σ
σ
by ρO = RG (τ3 ) →RG (τ2 ) → τ2 → τ3 .
5.3

Nondeterministic Opponent and then Probabilistic Player

In our last example Opponent O moves nondeterministically first, and thenPlayer P moves probabilistically. Such nested branching is in many processtheoretic models of probabilistic systems (see §3, in particular §3.2), most notably in Segala’s probabilistic automata [27]. We identify a 2-player PT situation(D, 1, τtotal , Cv, ρinf ) for this situation; then the associated logic PK` (τtotal , ρinf )is that of the probabilistic predicate transformers in [31]. The modality τtotal
is from §2.3. The other components (Cv, ρinf ) are to be described in terms of
convex cones and their convex subsets.
In what
P follows a D-algebra is referred to as a convex cone, adopting thenotation i∈I wi xi to denote a [xi 7→ wi ]i∈I ∈ X in P
a convex cone a : DX →X. Here I is a countable index set,3 wi ∈ [0, 1], and i∈I wi ≤ 1. Note that,
3

The countability requirement is superfluous since, if
ably many pi ’s are nonzero.

Pi∈I pi = 1, then only count-20

since D is the subdistribution monad, the zero distribution 0 is allowed in DX
and therefore a convex cone a : DX → X has its apex a0 ∈ X. Similarly, amorphism of D-algebras is referred to as a convex linear map.
Definition 5.5 (convex subset) A subset S ⊆ X of a convex
cone a : DX →P
X is said to be convex if, for any
p
∈
[0,
1]
such
that
p
= 1 and any
i
i
i∈I
P
xi ∈ S, the convex combination i∈I pi xi belongs to S.
P
We emphasizethat in the last definition i pi is required to be = 1. This isPunlike i wi ≤ 1 in the definition of convex cone. Therefore a convex subset S
need not include the apex a0; one can think of the base of a 3-dimensional coneas an example. This variation P
in the definitions is also found in [34, §2.1.2]; one
reason is technical: if we allow i pi ≤ 1 then it is hard to find the monad unit of
Cv (see below). Another process-theoretic reason is described later in Rem. 5.8.
Definition 5.6 (the monad Cv) The functor Cv : EM(D) → EM(D) carries a
convex cone a : DX → X to CvX := {S ⊆ X | S is convex}; the latter is aconvex cone byPP
i wi Si := {i wi xi | xi ∈ Si } .
P
It is easy to see that i wi Si is indeed a convex subset of X. Given a convex
linear map f : X → Y , Cvf : CvX → CvY is defined by (Cvf )S := qf S, which is
obviously convex in Y , too.
Cv:= { } : X → CvX;
The monad structure of Cv is as follows. Its unit is ηX
note that a singletonS{x} is a convex subset of X (Def. 5.5). The monad mulCv
and µCv: Cv(CvX) → CvX. It is easy to see that ηX
tiplication is µCv
X are
X :=
convex linear maps, and that they satisfy the monad axioms.
We introduce the last component, namely the modality ρinf : Cv(τtotal ) →τtotal . A convex subset S of the carrier D1 = [0, 1] of τtotal is nothing but aninterval (its endpoints may or may not be included); ρinf then carries such S
to its infimum inf S ∈ [0, 1]. That ρinf is convex linear, and that it satisfies theEilenberg-Moore axioms, are obvious.
Much like in Lem. 5.2, we obtain:
Lemma 5.7 (D, 1, τtotal , Cv, ρinf ) thus obtained is a 2-player PT situation.

tu

The resulting logic PK` (τtotal , ρinf ) is as follows. Given a postcondition q : Y →D1 and a computation f : X → U D CvF D Y , the weakest precondition isPPK` (τtotal , ρinf )(f )(q)(x) = inf.
(20)y∈Y d(y) · q(y) d ∈ f (x)P
Here d is a subdistribution chosen by Opponent; and the value y∈Y d(y)·q(y) isthe expected value of the random variable q under the distribution d. Therefore
the weakest precondition computed above is the least expected value of q when
Opponent picks a distribution in harm’s way. This is the same as in [31].

21Remark 5.8 The use of the convex powerset construction, instead of (plain)powersets, was motivated in §3.2 through the technical difficulty in getting amonad. Convex powersets are commonly used in the process-theoretic study ofprobabilistic systems, also because they model a probabilistic scheduler : Opponent (called a scheduler in this context) can not only pick one distribution but
also use randomization in doing so. See e.g. [2].
P
The definition of convex subset (Def. 5.5)—where we insist on i pi = 1
instead of ≤ 1—is natural in view of the logic PK` (τtotal , ρinf ) described above.
Relaxing this definition entails that the zero distribution 0 is always included ina “convex subset,” and hence always in Opponent’s options. This way, however,
the weakest precondition in (20) can always be forced to 0 and the logic getstrivial.
We can also model the situation where the roles of Player and Opponent areswapped: we can follow the same path as in Rem. 5.4 and obtain a 2-player PT
situation (D, 1, τpartial , Cv, ρsup ); the resulting modality ρsup carries an interval
to its supremum.

6

Conclusions and Future Work

Inspired by Jacobs’ recent work [16, 17] we pursued a foundation of predicate
transformers (more specifically weakest precondition semantics) based on anorder-enriched monad. There different notions of modality (such as “may” vs.
“must”) are captured by Eilenberg-Moore algebras. Nested branching with two
conflicting players can be modeled in a modular way, too, by a monad R on an
Eilenberg-Moore category EM(T ). Instances of this generic framework include
probabilistic weakest preconditions, those augmented with nondeterminism, andthe logic of forced predicates in games.
As future work we wish to address the components in the picture (2–3) thatare missing in the current framework. A generic weakest precondition calculus
presented in a syntactic form is another direction. Most probably relationships
between monads and algebraic theories (see e.g. [32]) will be exploited there. Socalled healthiness conditions—i.e. characterization of the image of PK` (τ ) in (8),to be precise its action on arrows—are yet another topic, generalizing [5, 31].
The current work is hopefully a step forward towards a coalgebraic theoryof automata (on infinite trees), games and fixed-point logics. For example, we
suspect that our categorical formulation of the logic of forced predicates be
useful in putting game (bi)simulation (studied e.g. in [22, 36]) in coalgebraic
terms. Possibly related, we plan to work on the relationship to the coalgebraic
theory of traces and simulations formulated in a Kleisli category [11, 13] since
all the monads in Example 2.2 fit in this trace framework.
In this paper we relied on an order-enrichment of a monad to obtain theentailment order. We are nevertheless interested in what our current framework
brings for other monads, like the ones that model computational effects [29](global state, I/O, continuation, etc.). Also interesting is a higher-order extension

22of the current work, where the logic will probably take the form of dependent
types. Related work in this direction is [20].
Acknowledgments Thanks are due to Kazuyuki Asada, Kenta Cho, Corina Cı̂rstea
and Tetsuri Moriya for useful discussions. The author is supported by Grantsin-Aid for Young Scientists (A) No. 24680001, JSPS, and by Aihara Innovative
Mathematical Modelling Project, FIRST Program, JSPS/CSTP.

References
1. Barr, M., Wells, C.: Toposes, Triples and Theories. Springer, Berlin (1985), available online.
2. Cattani, S., Segala, R.: Decision algorithms for probabilistic bisimulation. In: Brim,
L., Jancar, P., Kretı́nský, M., Kucera, A. (eds.) CONCUR. Lecture Notes in Computer Science, vol. 2421, pp. 371–385. Springer (2002)
3. Cheung, L.: Reconciling Nondeterministic and Probabilistic Choices. Ph.D. thesis,
Radboud Univ. Nijmegen (2006)
4. Cı̂rstea, C.: A coalgebraic approach to linear-time logics. In: FoSSaCS (2014), toappear
5. Dijkstra, E.W.: A Discipline of Programming. Prentice Hall (1976)
6. Foulis, D.J., Bennett, M.K.: Effect algebras and unsharp quantum logics. Found.
Physics 24(10), 1331–1352 (1994)
7. Giry, M.: A categorical approach to probability theory. In: Proc. Categorical Aspects of Topology and Analysis. Lect. Notes Math., vol. 915, pp. 68–85 (1982)
8. Grädel, E., Thomas, W., Wilke, T. (eds.): Automata, Logics, and Infinite Games:
A Guide to Current Research 2001], Lecture Notes in Computer Science, vol. 2500.
Springer (2002)
9. Hansen, H.H., Kupke, C.: A coalgebraic perspective on monotone modal logic.
Electr. Notes Theor. Comput. Sci. 106, 121–143 (2004)
10. Hansen, H.H., Kupke, C., Pacuit, E.: Neighbourhood structures: Bisimilarity andbasic model theory. Logical Methods in Computer Science 5(2) (2009)
11. Hasuo, I.: Generic forward and backward simulations II: Probabilistic simulation.
In: Gastin, P., Laroussinie, F. (eds.) CONCUR. Lect. Notes Comp. Sci., vol. 6269,
pp. 447–461. Springer (2010)
12. Hasuo, I., Hoshino, N.: Semantics of higher-order quantum computation via geometry of interaction. In: LICS. pp. 237–246. IEEE Computer Society (2011)13. Hasuo, I., Jacobs, B., Sokolova, A.: Generic trace semantics via coinduction. Logical
Methods in Comp. Sci. 3(4:11) (2007)
14. Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM
12, 576–580, 583 (1969)
15. Jacobs, B.: Categorical Logic and Type Theory. North Holland, Amsterdam (1999)
16. Jacobs, B.: New directions in categorical logic, for classical, probabilistic and quantum logic. Logical Methods in Comp. Sci. (2013), to appear
17. Jacobs, B.: Measurable spaces and their effect logic. In: LICS. pp. 83–92. IEEE
Computer Society (2013)
18. Jones, C.: Probabilistic Non-Determinism. Ph.D. thesis, Univ. Edinburgh (1990)
19. Jurdzinski, M.: Small progress measures for solving parity games. In: Reichel, H.,
Tison, S. (eds.) STACS. Lecture Notes in Computer Science, vol. 1770, pp. 290–301.
Springer (2000)

23
20. Katsumata, S.: Relating computational effects by >>-lifting. Inf. Comput. 222,
228–246 (2013)
21. Katsumata, S., Sato, T.: Preorders on monads and coalgebraic simulations. In:
Pfenning, F. (ed.) FoSSaCS. Lecture Notes in Computer Science, vol. 7794, pp.
145–160. Springer (2013)
22. Kissig, C., Venema, Y.: Complementation of coalgebra automata. In: Kurz, A.,
Lenisa, M., Tarlecki, A. (eds.) CALCO. Lect. Notes Comp. Sci., vol. 5728, pp.
81–96. Springer (2009)
23. Kock, A.: Monads and extensive quantities (2011), arXiv:1103.6009
24. Kozen, D.: Semantics of probabilistic programs. J. Comput. Syst. Sci. 22(3), 328–
350 (1981)
25. Kupke, C., Pattinson, D.: Coalgebraic semantics of modal logics: An overview.
Theor. Comput. Sci. 412(38), 5070–5094 (2011)
26. Kupke, C., Venema, Y.: Coalgebraic automata theory: Basic results. Logical Methods in Computer Science 4(4) (2008)
27. Lynch, N.A., Segala, R., Vaandrager, F.W.: Compositionality for probabilistic automata. In: Amadio, R.M., Lugiez, D. (eds.) CONCUR 2003. Lect. Notes Comp.
Sci., vol. 2761, pp. 204–222. Springer (2003)
28. Mac Lane, S.: Categories for the Working Mathematician. Springer, Berlin, 2ndedn. (1998)
29. Moggi, E.: Notions of computation and monads. Inf. & Comp. 93(1), 55–92 (1991)
30. Morgan, C.: Programming from Specifications. Prentice-Hall (1990)
31. Morgan, C., McIver, A., Seidel, K.: Probabilistic predicate transformers. ACM
Trans. Program. Lang. Syst. 18(3), 325–353 (1996)
32. Plotkin, G.D., Power, J.: Adequacy for algebraic effects. In: Honsell, F., Miculan, M. (eds.) FoSSaCS. Lecture Notes in Computer Science, vol. 2030, pp. 1–24.
Springer (2001)
33. Sokolova, A.: Coalgebraic Analysis of Probabilistic Systems. Ph.D. thesis, Techn.
Univ. Eindhoven (2005)
34. Tix, R., Keimel, K., Plotkin, G.D.: Semantic domains for combining probability
and non-determinism. Elect. Notes in Theor. Comp. Sci. 129, 1–104 (2005)
35. Varacca, D., Winskel, G.: Distributing probabililty over nondeterminism. Math.
Struct. in Comp. Sci. 16(1), 87–113 (2006)
36. Venema, Y., Kissig, C.: Game bisimulations between basic positions. Talk at Highlights of Logic, Games and Automata, Paris (2013)
37. Winskel, G.: The Formal Semantics of Programming Languages. MIT Press (1993)