2.1 Monads and Distributive Laws

We briefly recall here some definitions about monads. For a more detailed account see e.g. MacLane (Reference MacLane1998, Section VI). Let $\mathbb{C}$ be a category. A monad is a triple $(\mathsf{T},\eta,\mu)$ of a functor $\mathsf{T} \colon \mathbb{C} \to \mathbb{C}$ and two natural transformations $\eta\colon {\rm Id} \Rightarrow \mathsf{T}$ (the unit) and $\mu\colon \mathsf{T}^2 \Rightarrow \mathsf{T}$ (the multiplication) such that $\mu \mathbin{\star} \eta\mathsf{T} = {\rm id}_\mathsf{T} = \mu \mathbin{\star} \mathsf{T}\eta $ and $\mu \mathbin{\star} \mu\mathsf{T} = \mu \mathbin{\star} \mathsf{T}\mu$ .

The Kleisli lifting of $f: X\rightarrow \mathsf{T} Y$ is a morphism $f^{\#}\colon \mathsf{T} X \rightarrow \mathsf{T} Y$ defined as $f^{\#}\mathbin{\triangleq}\mu_ Y\circ \mathsf{T} f$ . A monad may be equivalently given by a triple $(\mathsf{T},\eta,(\_)^{\#})$ , replacing the multiplication with the Kleisli lifting $(\_)^{\#}:\mathbb{C}( X,\mathsf{T} Y)\to \mathbb{C}(\mathsf{T} X,\mathsf{T} Y)$ ; see Moggi (Reference Moggi1991).

The Kleisli category $\mathbb{C}_\mathsf{T}$ of a monad $(\mathsf{T},\eta,\mu)$ is a category whose objects are the objects of $\mathbb{C}$ and whose homsets are defined by $\mathbb{C}_\mathsf{T}( X, Y)\mathbin{\triangleq} \mathbb{C}( X,\mathsf{T} Y)$ . The composition of morphisms in $\mathbb{C}_\mathsf{T}$ is denoted by $\bullet$ and is defined from the composition $\circ$ in $\mathbb{C}$ as $g \bullet f \mathbin{\triangleq} g^{\#} \circ f$ . Following Moggi (Reference Moggi1991), we regard morphisms in $\mathbb{C}_\mathsf{T}$ as abstract representations of programs causing computational effects. There exists an adjunction $L \dashv R \colon \mathbb{C} \to \mathbb{C}_\mathsf{T}$ such that $R \circ L = T$ , called the Kleisli resolution of $\mathsf{T}$ .

An Eilenberg–Moore (EM for short) algebra of a monad $(\mathsf{T},\eta,\mu)$ is a pair (X,o) of an object $ X\in\mathbb{C}$ and a morphism $o \colon \mathsf{T} X \to X$ such that $o \circ \eta_ X = {\rm id}_ X$ and $o \circ To = o \circ \mu_ X$ .

Let $(\mathsf{T},\eta^\mathsf{T},\mu^\mathsf{T})$ and $(\mathsf{S},\eta^\mathsf{S},\mu^\mathsf{S})$ be monads on $\mathbb{C}$ . A distributive law (Beck Reference Beck1969) of $\mathsf{S}$ over $\mathsf{T}$ is a natural transformation $\alpha:\mathsf{S}\mathsf{T}\rightarrow \mathsf{T} \mathsf{S}$ such that

\begin{align*} \eta^\mathsf{T}\mathsf{S}&=\alpha\mathbin{\star} \mathsf{S}\eta^\mathsf{T} & \alpha\mathbin{\star} \mathsf{S}\mu^\mathsf{T}&=\mu^\mathsf{T}\mathsf{S}\mathbin{\star} \mathsf{T}\alpha\mathbin{\star} \alpha \mathsf{T} & \mathsf{T}\eta^\mathsf{S}&=\alpha\mathbin{\star}\eta^\mathsf{S}\mathsf{T} & \alpha\mathbin{\star}\mu^\mathsf{S}\mathsf{T}&=\mathsf{T}\mu^\mathsf{S}\mathbin{\star}\alpha \mathsf{S}\mathbin{\star} \mathsf{S}\alpha.\end{align*}

The distributive law yields the monad $\left(\mathsf{T}\mathsf{S},\eta^\mathsf{T}\mathbin{*}\eta^\mathsf{S},\left(\mu^\mathsf{T}\mathbin{*}\mu^\mathsf{S})\mathbin{\star} (\mathsf{T}\alpha \mathsf{S}\right)\right)$ over the composite functor. We denote this monad by $\mathsf{T}\circ_\alpha \mathsf{S}$ .

2.2 Fibrations

Dijkstra’s weakest precondition predicate transformer manipulates predicates over memory configurations. In the abstract study of predicate transformers, however, it is convenient to extend the concept of predicates so that they can be defined over arbitrary objects on a category. For this abstract and general treatment of predicates, we leverage the notions of fibered category theory (see e.g. Jacobs Reference Jacobs1999). Before introducing these concepts, we give an informal account of them.

Given a category $\mathbb{C}$ (with objects ranging over X, Y, Z and morphisms ranging over f,g,h) we aim to define predicates over its objects by introducing a category $\mathbb{P}$ (with objects ranging over P, Q, R and morphisms ranging over dotted letters ${\dot f},\dot g,\dot h$ ) and a functor $p:\mathbb{P}\rightarrow\mathbb{C}$ . We understand this general situation as follows:

• An object in $\mathbb{P}$ is a predicate over some object in $\mathbb{C}$ , which is recorded by the functor $p:\mathbb{P}\rightarrow\mathbb{C}$ . That is, $p P= X$ means that $ P\in\mathbb{P}$ is a predicate over $ X\in\mathbb{C}$ .

• A morphism ${\dot f}: \to P\to Q$ in $\mathbb{P}$ is a witness of the fact that the underlying morphism $p{\dot f}:p P\rightarrow p Q$ in $\mathbb{C}$ “preserves” these predicates, that is, $p{\dot f}$ maps elements satisfying the predicate P to those satisfying the predicate Q. In particular, if ${\dot f} : P\rightarrow Q$ satisfies $p{\dot f}={\rm id}_ X$ , then ${\dot f}$ witnesses that P implies Q.

The inverse image of an object $ X\in\mathbb{C}$ under the functor $p:\mathbb{P}\rightarrow\mathbb{C}$ forms a category denoted by $\mathbb{P}_ X$ , known as the fiber category above X. Formally, an object of $\mathbb{P}_ X$ is a $\mathbb{P}$ -object P such that $p P= X$ , and a morphism from P to Q in $\mathbb{P}_ X$ is a morphism ${\dot f}: P\to Q$ in $\mathbb{P}$ such that $p{\dot f}={\rm id}_ X$ . Intuitively, objects of this category are predicates over X, and morphisms of this category represent implication relations between them.

When defining weakest precondition predicate transformers, the strength of predicates is compared by an order relation, so we focus our attention on posetal fibrations. Recall that the weakest precondition predicate transformer collects all the memory configurations that entail the postcondition. Set-theoretically, this operation is called inverse image, and fibrations offer a more general and flexible treatment of the inverse image operation. Roughly speaking, a fibration is a functor $p:\mathbb{P}\rightarrow\mathbb{C}$ such that for any morphism $f: X\to Y$ in $\mathbb{C}$ and $ P\in\mathbb{P}_ Y$ , we can find the inverse image $f^* P\in\mathbb{P}_ X$ of P along f. The formal definition of a posetal fibration follows.

• For objects $ P, Q\in \mathbb{P}$ and a morphism $f:p P\to p Q$ in $\mathbb{C}$ , we define the set $\mathbb{P}_f( P, Q)$ of morphisms in $\mathbb{P}$ above f by $\mathbb{P}_f( P, Q)\triangleq \{{\dot f}\in\mathbb{P}( P, Q)~|~p{\dot f}=f\}$ .

• A morphism ${\dot f}: P\to Q$ in $\mathbb{P}$ is Cartesian if for any $ R \in \mathbb{P}$ and morphism $h:p R\to p P$ in $\mathbb{C}$ , the postcomposition of ${\dot f}$ , regarded as a function of type $\mathbb{P}_h( R, P)\rightarrow\mathbb{P}_{p{\dot f}\circ h}( R, Q)$ , is a bijection. This is the universal property of Cartesian morphisms. A Cartesian morphism ${\dot f}: P\to Q$ in $\mathbb{P}$ abstractly represents the situation that P is an inverse image of Q along $p{\dot f}$ .

• A functor $p:\mathbb{P}\rightarrow\mathbb{C}$ is a fibration if for any morphism $f: X\to Y$ in $\mathbb{C}$ and $ Q\in\mathbb{P}_ Y$ , there is an object $ P\in\mathbb{P}_ X$ and a Cartesian morphism ${\dot f}: P\to Q$ in $\mathbb{P}_f$ called the Cartesian lifting of f with Q.

• A fibration $p:\mathbb{P}\rightarrow\mathbb{C}$ is posetal if each fiber category $\mathbb{P}_ X$ is a poset. In any posetal fibration, the Cartesian lifting of a morphism $f: X\to Y$ in $\mathbb{C}$ with $ Q\in\mathbb{P}_ Y$ uniquely exists; we therefore denote it by $\overline f Q$ and its domain by $f^* Q$ . We note that posetal fibrations are faithful. Therefore, a morphism ${\dot f}: P\to Q$ in $\mathbb{P}$ is Cartesian if and only if $ P=(p{\dot f})^* Q$ .

• In a posetal fibration $p:\mathbb{P}\rightarrow\mathbb{C}$ , the assignment $ Q\mapsto f^* Q\in\mathbb{P}_ P$ for a morphism $f: X\to Y$ in $\mathbb{C}$ extends to a monotone function of type $\mathbb{P}_ Y\rightarrow\mathbb{P}_ X$ , which we call the reindexing functor (we use the word functor for the compatibility with the existing terminology). The assignment $f\mapsto f^*$ furthermore satisfies $({\rm id}_ X)^*={\rm id}_{\mathbb{P}_ X}$ and $(g\circ f)^*=f^* g^*$ .

• Let $\mathbb K$ be a subcategory of Pos. A functor $p:\mathbb{P}\rightarrow\mathbb{C}$ is a $\mathbb K$ -fibration if each fiber category $\mathbb{P}_ X$ belongs to $\mathbb K$ , and each reindexing functor $f^*$ belongs to $\mathbb K$ as a morphism.

A convenient way to obtain $\mathbb K$ -fibrations is by the Grothendieck construction (in fact every $\mathbb K$ -fibration is isomorphic to one obtained in this way). Let $F:\mathbb{C}^{op}\rightarrow\mathbb K$ be a functor. The Grothendieck construction applied to F yields a category $\int F$ defined by the data below:

• An object is a pair (X,x) of an object $ X\in\mathbb{C}$ and an element $x\in F X$ .

• A morphism from (X,x) to (Y,y) is a morphism $f: X\to Y$ in $\mathbb{C}$ such that $x\le Ff(y)$ in the poset F X belonging to $\mathbb K$ .

The forgetful functor $G_{F}:\int F\to \mathbb{C}$ defined by $G_{F}( X,x)\mathbin{\triangleq} X$ and $G_{F}(\,f)\mathbin{\triangleq} f$ is a $\mathbb K$ -fibration; see e.g. Jacobs (Reference Jacobs1999).

Toward defining the 2-category of $\mathbb K$ -fibrations, we introduce a few concepts. Let $p:\mathbb{P}\to\mathbb{C}$ and $q:\mathbb Q\to\mathbb D$ be $\mathbb K$ -fibrations.

• A $\mathbb K$ -functor is a pair of functors $(F:\mathbb{C}\to\mathbb D,\dot F:\mathbb{P}\to\mathbb Q)$ such that $Fp=q\dot F$ , and the restriction of $\dot F$ to each fiber, written $\dot F_ X:\mathbb{P}_ X\to\mathbb Q_{F X}$ , belongs to $\mathbb K$ . It is called fibered if $\dot F$ preserves Cartesian morphisms; this requirement is equivalent to requiring that the equality $\dot F(\,f^* P)=(Ff)^*(\dot F P)$ holds for any object $ P\in\mathbb{P}$ and morphism $f: X\to p P$ in $\mathbb{C}$ .

• Let $(F,\dot F),(G,\dot G):p\to q$ be $\mathbb K$ -functors. A natural transformation from the former to the latter is a pair of natural transformations $\alpha:F\to G$ and $\dot\alpha:\dot F\to\dot G$ such that $\alpha p=q\dot\alpha$ . It is called Cartesian if $\dot\alpha_{ P}$ is a Cartesian morphism above $\alpha_{p P}$ for each $ P\in\mathbb{P}$ .

The following lemma characterizes (Cartesian) natural transformations between (fibered) $\mathbb K$ -functors.

Lemma 2. Let $p:\mathbb{P}\to\mathbb{C}$ and $q:\mathbb Q\to\mathbb D$ be $\mathbb K$ -fibrations. Then the mapping $(\alpha,\dot\alpha)\mapsto \alpha$ gives the following bijections:

(1) \begin{align} \Xi:{\mathbb K}\text{-}{\bf Fib}_0(p,q)((F,\dot F),(G,\dot G)) & \cong\{\alpha:F\to G~|~\forall{ P\in\mathbb{P}}~.~\dot F P\le\alpha_{p P}^*(\dot G P)\}, \end{align}

(2) \begin{align} \Xi_c:{\mathbb K}\text{-}{\bf Fib}_c(p,q)((F,\dot F),(G,\dot G)) & \cong\{\alpha:F\to G~|~\forall{ P\in\mathbb{P}}~.~\dot F P=\alpha_{p P}^*(\dot G P)\}. \end{align}

We write $\Xi,\Xi_c$ for the above bijections from left to right, respectively. We will use them later in Section 4.1.

Proof. We show (1); (2) is proved similarly. Let $\alpha:F\to G$ be a natural transformation such that $\dot F P\le\alpha_{p P}^*(\dot G P)$ . It suffices to exhibit a unique natural transformation $\dot\alpha:\dot F\to\dot G$ such that $\alpha p=q\dot\alpha$ . Define $\dot\alpha_ P$ by

It routine to check that $\dot\alpha$ is a natural transformation satisfying $\alpha p=q\dot\alpha$ . Moreover, the faithfulness of q guarantees its uniqueness.

3.1 Dijkstra Structures

Let $\mathbb{C}$ be a category and $\mathsf{T}$ a monad over it. We aim to model the statement that a computation represented as a morphism $f: X\to Y$ in the Kleisli category $\mathbb{C}_\mathsf{T}$ satisfies a specification given by a precondition and a postcondition, which are predicates over X and Y, respectively. Since the codomain of f is $\mathsf{T} Y$ , we first need to construct a predicate over $\mathsf{T} Y$ from a predicate over Y. For this purpose, we define a lifting of $\mathsf{T}$ into a monad ${\dot {\mathsf{T}}}$ over $\mathbb{P}$ .

• $(\mathsf{T},{\dot {\mathsf{T}}})$ is a fibered $\mathbb K$ -functor from p to p, and

• $\dot\eta_ P$ and $\dot\mu_ P$ are respectively Cartesian above $\eta_{p P}$ and $\mu_{p P}$ for any $ P\in\mathbb{P}$ . This is equivalent to having that $ P=\eta_{p P}^*({\dot {\mathsf{T}}} P)$ and ${\dot {\mathsf{T}}}{\dot {\mathsf{T}}} P=\mu^*_{p P}{\dot {\mathsf{T}}} P$ for any object $ P\in\mathbb{P}$ .

The concept of monad lifting is not new; it appeared as a semantic counterpart of logical relations for monads (Filinski Reference Filinski1996; Filinski Reference Filinski2007; Goubault-Larrecq et al. Reference Goubault-Larrecq, Lasota and Nowak2008; Katsumata Reference Katsumata2005; Katsumata et al. Reference Katsumata, Sato and Uustalu2018). Hermida considered the comonadic case earlier than these works Hermida (Reference Hermida1993), Chapter 5. The definition of Cartesian lifting of monad makes sense when p is a non-posetal fibration. When $\mathbb{C}$ is a category with pullbacks, a monad $\mathsf{T}$ on $\mathbb{C}$ is Cartesian (see e.g. Leinster Reference Leinster2004, Section 4.1) if and only if the evident lifting $\mathsf{T}^\rightarrow:\mathbb{C}^\rightarrow\rightarrow\mathbb{C}^\rightarrow$ of $\mathsf{T}$ to the arrow category $\mathbb{C}^\rightarrow$ along the codomain fibration ${\rm cod}:\mathbb{C}^\rightarrow\rightarrow\mathbb{C}$ is Cartesian.

The tuple consisting of a $\mathbb K$ -fibration p, a monad $\mathsf{T}$ , and its $\mathbb K$ -lifting ${\dot {\mathsf{T}}}$ along p provides us a setting in which we can define the Hoare triple and the weakest precondition predicate transformer (wppt for short) associated to it. In this paper, we package these data into one, and call it a Dijkstra structure.

A (resp. Cartesian) ${\mathbb K}$ -Dijkstra structure is precisely a monad in ${\mathbb K}\text{-}{\bf Fib}_0$ (resp. ${\mathbb K}\text{-}{\bf Fib}_c$ ).

1. (1) For a morphism $f: X\to \mathsf{T} Y$ in $\mathbb{C}$ and objects $ P\in\mathbb{P}_ X, Q\in\mathbb{P}_ Y$ , we define the Hoare triple $ P \{ f \} Q$ by

   (3) \begin{equation}P\{f\} Q\mathbin{\triangleq} \exists{\dot f\in\mathbb{P}( P,{\dot {\mathsf{T}}} Q)}~.~p\dot f=f. \end{equation}
   Such $\dot f$ is unique because p is faithful.

2. (2) For a morphism $f: X\to \mathsf{T} Y$ in $\mathbb{C}$ , we define the weakest precondition predicate transformer $\mathrm{wp}(\,f,-)\in\mathbb K(\mathbb{P}_ Y,\mathbb{P}_ X)$ by

   (4) \begin{equation}\mathrm{wp}(f, Q) \mathbin{\triangleq} f^*({\dot {\mathsf{T}}} Q).\end{equation}

Since p is a fibration, Hoare triples and the wppt are linked by the following equivalence:

\begin{equation*} P \leq \mathrm{wp}(f, Q) \Longleftrightarrow P \{ f \} Q.\end{equation*}

We remark that for each morphism f, $\mathrm{wp}(\,f,\_)$ is a morphism in $\mathbb K$ . Therefore, if morphisms in $\mathbb K$ are required to preserve order-theoretic structures, so does $\mathrm{wp}(\,f,\_)$ . For instance, when $\mathbb K$ is the category ${\bf CLat}_\wedge$ of complete lattices and functions preserving all meets, the wppt of a Dijkstra structure ${{\bf CLat}_\wedge}$ preserves arbitrary meets in its second argument: $\mathrm{wp}(f,\bigwedge_i P_i) = \bigwedge_i\mathrm{wp}(f, P_i)$ . In the context of program verification, such a wppt is called conjunctive.

3.2 Composability of the Weakest Precondition Predicate Transformers

The Hoare triple and the wppt in our categorical setting are more general than the standard ones since we can supply any $\mathbb{P}$ -object and $\mathbb{C}_\mathsf{T}$ -morphism to the wppt. This liberation allows us to relate the composability of the wppt and the Cartesian-ness of ${\dot {\mathsf{T}}}$ . Since wp takes a Kleisli morphism as an argument, the composability should be discussed with respect to the Kleisli composition.

Theorem 6. Let $(p:\mathbb{P}\to\mathbb{C},\mathsf{T},{\dot {\mathsf{T}}})$ be a ${\mathbb K}$ -Dijkstra structure. We have inequalities

(5) \begin{equation} \mathrm{wp}(\eta_{p P}, P) \geq P,\quad \mathrm{wp}(f \bullet g, ) P \geq\mathrm{wp}(g, ){\mathrm{wp}(f, P)} \end{equation}

for any f,g, P of appropriate type; here, $\eta$ and $\bullet$ are the unit and the Kleisli composition of $\mathsf{T}$ , respectively. Moreover, inequalties in (5) become equalities if and only if the ${\mathbb K}$ -Dijkstra structure is Cartesian.

Proof. Let $(p:\mathbb{P}\to\mathbb{C},\mathsf{T},{\dot {\mathsf{T}}})$ be a ${\mathbb K}$ -Dijkstra structure. Then the unit $\dot\eta_ P: P\rightarrow{\dot {\mathsf{T}}} P$ of ${\dot {\mathsf{T}}}$ is above $\eta_{p P}$ . Therefore

\begin{equation*} \mathrm{wp}(\eta_{p P}, P)=\eta_{p P}^*({\dot {\mathsf{T}}} P)\ge P.\end{equation*}

If $\dot\eta_ P$ is Cartesian, this inequality becomes an equality. Next, the multiplication $\dot\mu_ P:{\dot {\mathsf{T}}}{\dot {\mathsf{T}}} P\rightarrow{\dot {\mathsf{T}}} P$ of ${\dot {\mathsf{T}}}$ is above $\mu_{p P}$ . Therefore ${\dot {\mathsf{T}}}{\dot {\mathsf{T}}} P\le\mu^*_{p P}{\dot {\mathsf{T}}} P$ holds; this becomes an equality if $\dot\mu_ P$ is Cartesian. Moreover, for any object $ X\in\mathbb{C}, P\in\mathbb{P}$ and morphism $f: X\to p P$ in $\mathbb{C}$ , we have ${\dot {\mathsf{T}}}(\,f^* P)\le (\mathsf{T} f)^*({\dot {\mathsf{T}}} P)$ ; this becomes an equality if ${\dot {\mathsf{T}}}$ is fibered. From these, we obtain the following inequality, which becomes an equality if $\dot\mu_ P$ is Cartesian and ${\dot {\mathsf{T}}}$ is fibered.

\begin{align*} (\,f\bullet g)^*({\dot {\mathsf{T}}} P) &= (\mu\circ \mathsf{T} f\circ g)^*({\dot {\mathsf{T}}} P)= g^*((\mathsf{T} f)^*(\mu^*({\dot {\mathsf{T}}} P))) \\ & \ge g^*((\mathsf{T} f)^*({\dot {\mathsf{T}}}{\dot {\mathsf{T}}} P)) \ge g^*({\dot {\mathsf{T}}}(\,f^*({\dot {\mathsf{T}}} P)) =\mathrm{wp}(g,\mathrm{wp}(\,f, P)). \end{align*}

We have thus proved inequalities (5), and if the assumed ${\mathbb K}$ -Dijkstra structure is Cartesian, these inequalities become equalities.

We conversely assume

(6) \begin{eqnarray} P & = & \mathrm{wp}(\eta_{p P}, P)=\eta_{p P}^* ({\dot {\mathsf{T}}} P), \end{eqnarray}

(7) \begin{eqnarray} g^* {\dot {\mathsf{T}}} (\,f^* {\dot {\mathsf{T}}} P)=\mathrm{wp}(g,\mathrm{wp}(\,f, P)) & = & \mathrm{wp}(\,f\bullet g, P)=g^* (T f)^* \mu_{p P}^* {\dot {\mathsf{T}}} P. \end{eqnarray}

Below let $ X=p P$ . (6) implies that $\dot\eta_{ P}$ is Cartesian. By putting $g = {{\mathrm{id}}}_{T T X}$ and $f = {{\mathrm{id}}}_{T X}$ in (7), we obtain $ {\dot {\mathsf{T}}} {\dot {\mathsf{T}}} P = \mu_ X^* ({\dot {\mathsf{T}}} P)$ , hence $\dot\mu_{ P}$ is Cartesian. Let $h: Y\to X$ be a morphism in $\mathbb{C}$ . By putting $g = {{\mathrm{id}}}_{T X}$ and $f = \eta_ X \circ h: Y\to T X$ in (7), we obtain ${\dot {\mathsf{T}}} (h^* P) = {\dot {\mathsf{T}}} (h^* \eta_ X^* {\dot {\mathsf{T}}} P) = (\mathsf{T} h)^* ({\dot {\mathsf{T}}} P)$ , hence ${\dot {\mathsf{T}}}$ is fibered.

Therefore, for a Cartesian ${\mathbb K}$ -Dijkstra structure $(p:\mathbb{P}\rightarrow\mathbb{C},\mathsf{T},{\dot {\mathsf{T}}})$ , the following assignments of posets in $\mathbb K$ and monotone functions in $\mathbb K$ become a functor $\mathrm{Wp}:(\mathbb{C}_\mathsf{T})^{op}\rightarrow\mathbb K$ :

\begin{align*} \mathrm{Wp}( X)&\mathbin{\triangleq}\mathbb{P}_ X,& \,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\mathrm{Wp}(\,f)&\mathbin{\triangleq}\mathrm{wp}(\,f,\_).\end{align*}

Then the Grothendieck construction G applied to Wp yields the $\mathbb K$ -fibration that is isomorphic to the evident functor from $\mathbb{P}_{\dot {\mathsf{T}}}$ to $\mathbb{C}_\mathsf{T}$ .

Theorem 7. Let $(p:\mathbb{P}\to\mathbb{C},\mathsf{T},{\dot {\mathsf{T}}})$ be a Cartesian ${\mathbb K}$ -Dijkstra Structure. We take Kleisli resolutions $(L\dashv R:\mathbb{C}_\mathsf{T}\rightarrow\mathbb{C},\eta,\varepsilon)$ of $\mathsf{T}$ and $(\dot L\dashv\dot R:\mathbb{P}_{{\dot {\mathsf{T}}}}\rightarrow\mathbb{P},\dot\eta,\dot\varepsilon)$ of ${\dot {\mathsf{T}}}$ . We define the functor $p_{\mathsf{T}, \dot{\mathsf{T}}} : \mathbb{P}_{{\dot {\mathsf{T}}}}\rightarrow \mathbb{C}_\mathsf{T}$ by

\begin{align*} p_{\mathsf{T}, \dot{\mathsf{T}}} P&\mathbin{\triangleq} p P,&\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\, p_{\mathsf{T}, \dot{\mathsf{T}}}f&\mathbin{\triangleq} pf. \end{align*}

1. (1) We have an isomorphism $p_{\mathsf{T},{\dot {\mathsf{T}}}}\cong G_{\mathrm{Wp}}$ in ${\mathbb K}\text{-}{\bf Fib}_c$ .

2. (2) We have an isomorphism $p\cong G_{\mathrm{Wp}\circ L}$ in ${\mathbb K}\text{-}{\bf Fib}_c$ .

3. (3) $((L,\dot L),(R,\dot R),(\eta,\dot\eta),(\varepsilon,\dot\varepsilon))$ is an adjunction in ${\mathbb K}\text{-}{\bf Fib}_c$ .

Proof. (1, 2) Routine. We note that the reindexing functor of the fibration $p_{\mathsf{T},{\dot {\mathsf{T}}}}$ is $\mathrm{wp}(\,f,\_)$ . (3) We first show that $(L,\dot L),(R,\dot R)$ are 1-cells in ${\mathbb K}\text{-}{\bf Fib}_c$ . A) Equations $p_{\mathsf{T},{\dot {\mathsf{T}}}}\dot L=L p$ and $p \dot R=R p_{\mathsf{T},{\dot {\mathsf{T}}}}$ easily follow from ${\dot {\mathsf{T}}}$ being a lifting of $\mathsf{T}$ along p. B) We show the fiberedness of $\dot L$ and $\dot R$ , that is, $ \dot L(\,f^* P)=\mathrm{wp}(Lf,\dot L P)$ and $\dot R(\mathrm{wp}(\,f, P))=(Rf)^*(\dot R P)$ . By the Cartesianness of ${\dot{\mathsf{T}}}$ , we have

\begin{align*} &\dot L(\,f^* P)= f^* P= f^*\eta^*({\dot {\mathsf{T}}} P)= \mathrm{wp}(Lf,\dot L P),\\ &\dot R(\mathrm{wp}(\,f, P))= {\dot {\mathsf{T}}}(\,f^*({\dot {\mathsf{T}}} P))= (Tf)^*({\dot {\mathsf{T}}}{\dot {\mathsf{T}}} P)= (Tf)^*\mu^*({\dot {\mathsf{T}}} P)= (\mu\circ Tf)^*({\dot {\mathsf{T}}} P)= (Rf)^*(\dot R P). \end{align*}

(C) We show that the restrictions of $\dot L,\dot R$ to fibers belong to $\mathbb K$ . The restriction $\dot L_ X:\mathbb{P}_ X\to (\mathbb{P}_{{\dot {\mathsf{T}}}})_{L X}$ is the identity morphism, hence belongs to $\mathbb K$ . The restriction $\dot R_ Y:(\mathbb{P}_{{\dot {\mathsf{T}}}})_{ Y}\rightarrow \mathbb{P}_{R Y}$ coincides with $\dot T_ Y$ , which belongs to $\mathbb K$ .

We next show that $(\eta,\dot\eta)$ and $(\varepsilon,\dot\varepsilon)$ are 2-cells in ${\mathbb K}\text{-}{\bf Fib}_c$ . The proof proceeds as follows:

\begin{align*} P&=\eta_{p P}^*\dot T P=\eta_{p P}^*\dot R\dot L P & \dot L\dot R Q&=\dot T Q={\rm id}_{\mathsf{T} p_{\mathsf{T},{\dot {\mathsf{T}}}} Q}^*{\dot {\mathsf{T}}} Q=wp(\varepsilon_{p_{\mathsf{T},{\dot {\mathsf{T}}}} Q}, Q). \end{align*}

It is routine to check that $((L,\dot L),(R,\dot R),(\eta,\dot\eta),(\varepsilon,\dot\varepsilon))$ forms an adjunction in ${\mathbb K}\text{-}{\bf Fib}_c$ .

Recent work (Aguirre et al. Reference Aguirre, Barthe, Hsu, Kaminski, Katoen and Matheja2021) presents a noncomposable predicate transformer to reason about relational pre-expectations of probabilistic programs. This noncomposability can be associated to the fact that the monad lifting used in the work is not Cartesian. Their relational pre-expectation operator coincides with our categorical wppt in the Dijkstra structure $(p : {\bf EPMet} \rightarrow {\bf Set}, \mathsf{D_\omega}, \mathsf{K})$ , where p is the forgetful functor from the category of extended pseudometric spaces, which is a posetal fibration, $\mathsf{D_\omega}$ is the countable probability distribution monad (see Example 40 for the finite case), and $\mathsf{K}$ is the Kantorovich metric construction:

\begin{align*} \mathsf{K}( X,d)&\mathbin{\triangleq}(\mathsf{D_\omega} X,d^K),& d^K(\mu_1,\mu_2)&\mathbin{\triangleq}\inf_{\mu\in\Gamma(\mu_1,\mu_2)}{E_{(x,y)\sim \mu}[d(x,y)]}.\end{align*}

Here $\Gamma(\mu_1,\mu_2)$ is the set of probabilistic couplings between $\mu_1,\mu_2$ , and E denotes the expectation; see Aguirre et al. (Reference Aguirre, Barthe, Hsu, Kaminski, Katoen and Matheja2021, Definition 2.2) for details. Since it fails to satisfy the composability, we conclude that the Dijkstra structure is not Cartesian.

3.3 Change-of-base of Dijkstra Structures

In fibrational category theory, the change-of-base is a convenient method to introduce a fibration over a category. This method takes a fibration $p:\mathbb{P}\rightarrow\mathbb{C}$ and a functor $F:\mathbb D\rightarrow\mathbb{C}$ as parameters and performs the following pullback in the (large) category CAT of categories and functors:

We explicitly specify the pullback category $F^*\mathbb{P}$ as follows: an object is a pair $( X\in\mathbb D, P\in\mathbb{P})$ of objects such that $F X=p P$ , and a morphism from (X, P) to (Y, Q) is a pair of morphisms $(\,f,\dot f)\in\mathbb D( X, Y)\times\mathbb{P}( P, Q)$ such that $Ff=p\dot f$ . The first projection functor $F^*p$ is called the change-of-base of p along F and is again a fibration Jacobs (Reference Jacobs1999, Lemma 1.5.1). The inverse image of $( Y, Q)\in F^*\mathbb{P}$ along a morphism $f: X\to Y$ in $\mathbb D$ is given by $( X,(Ff)^* Q)$ . When $p:\mathbb{P}\to\mathbb{C}$ is a $\mathbb K$ -fibration, so is $F^*p:F^*\mathbb{P}\to\mathbb D$ , and each homset of $F^*\mathbb{P}$ satisfies

\begin{equation*} F^*\mathbb{P}(( X, P),( Y, Q))\cong \{f\in\mathbb D( X, Y)~|~ P\le (Ff)^* Q\}.\end{equation*}

We therefore replace homsets of $F^*\mathbb{P}$ with the right-hand side when p is a $\mathbb K$ -fibration.

Now consider the functor $\times \colon {\bf Set}^2 \to {\bf Set}$ . The change-of-base construction induced by p and $\times$ constructs a fibration with total category ${\bf BRel}({\bf Set})$ , defined by the data below:

• Objects are triples $(P,X_1,X_2)$ of sets such that $P \subseteq X_1\times X_2$ .

• Morphisms from $(P,X_1,X_2)$ to $(Q,Y_1,Y_2)$ are pairs of morphisms $f_1\colon X_1 \to Y_1$ , $f_2\colon X_2\to Y_2$ such that for all $(x_1,x_2) \in P$ , $(\,f_1(x_1),f_2(x_2))\in Q$ .

The fibration is given by the forgetful functor $(\!\times\!)^\ast p$ mapping $(P,X_1,X_2)$ to $(X_1,X_2)$ .

In Section 10 we will see a generalization of this construction for a general base category $\mathbb{C}$ and a general truth-value object $\Omega$ .

We now apply the change-of-base method to Dijkstra structures. Since Dijkstra structures are fibrations with monads, we naturally expect that the functor, along which we take a pullback, interacts with the monad of a Dijkstra structure. We describe this interaction by the monad opfunctor axioms given by Street Street (Reference Street1972, Section 4).

Definition 9. A monad morphism from a monad $(\mathsf{S},\eta^\mathsf{S},\mu^\mathsf{S})$ on $\mathbb D$ to a monad $(\mathsf{T},\eta^\mathsf{T},\mu^\mathsf{T})$ on $\mathbb{C}$ is a pair of a functor $F:\mathbb D\rightarrow \mathbb{C}$ and a natural transformation $\alpha:F \mathsf{S}\rightarrow \mathsf{T} F$ satisfying the following axioms:

(8) \begin{align} \alpha\star(F\eta^\mathsf{S})&=\eta^\mathsf{T} F, & \alpha \star (F\mu^\mathsf{S})&= (\mu^\mathsf{T} F) \star (\mathsf{T}\alpha)\star(\alpha \mathsf{S}). \end{align}

The following theorem extends the change-of-base method to Dijkstra structures along monad morphism. It preserves Cartesianness of Dijkstra structures.

Theorem 10. Let $(p:\mathbb{P}\rightarrow \mathbb{C},\mathsf{T},{\dot {\mathsf{T}}})$ be a (resp. Cartesian) ${\mathbb K}$ -Dijkstra structure, $\mathsf{S} $ be a monad on a category $\mathbb D$ and $(F:\mathbb D\rightarrow\mathbb{C},\alpha:F \mathsf{S} \rightarrow \mathsf{T} F)$ be a monad morphism from $\mathsf{S} $ to $\mathsf{T}$ . We define a monad $({\dot {\mathsf{S}}},\eta^{\dot {\mathsf{S}}},\mu^{\dot {\mathsf{S}}})$ on $F^*\mathbb{P}$ by

\begin{align*} {\dot {\mathsf{S}}} ( X, P)&\mathbin{\triangleq}(\mathsf{S} X,\alpha^*_ X({\dot {\mathsf{T}}} P)), & {\dot {\mathsf{S}}} f&\mathbin{\triangleq} \mathsf{S} f,& \eta^{\dot {\mathsf{S}}}_{( X, P)}&\mathbin{\triangleq} \eta_ X^\mathsf{S}, & \mu^{\dot {\mathsf{S}}}_{( X, P)}&\mathbin{\triangleq} \mu_ X^\mathsf{S}. \end{align*}

Then the tuple $(F^*p:F^*\mathbb{P}\rightarrow\mathbb D, \mathsf{S} , {\dot {\mathsf{S}}} )$ is a (resp. Cartesian) ${\mathbb K}$ -Dijkstra structure.

We first verify that $f\in F^*\mathbb{P}(( X, P),( Y, Q))$ implies $\dot Sf\in F^*\mathbb{P}({\dot {\mathsf{S}}}( X, P),{\dot {\mathsf{S}}}( Y, Q))$ .

\begin{align*} \alpha_ X^*({\dot {\mathsf{T}}} P) &\le \alpha_ X^*({\dot {\mathsf{T}}}((F f)^* Q)) \le \alpha_ X^*(\mathsf{T} F f)^*({\dot {\mathsf{T}}} Q) =(F\mathsf{S} f)^*\alpha_ Y^*({\dot {\mathsf{T}}} Q). \end{align*}

We next verify that $\eta^{\dot {\mathsf{S}}}_{( X, P)}\in F^*\mathbb{P}(( X, P),{\dot {\mathsf{S}}}( X, P))$ and $\mu^{\dot {\mathsf{S}}}_{( X, P)}\in F^*\mathbb{P}({\dot {\mathsf{S}}}({\dot {\mathsf{S}}}( X, P)),{\dot {\mathsf{S}}}( X, P))$ .

\begin{align*} P &\le (\eta_{F X}^\mathsf{T})^*({\dot {\mathsf{T}}} P) = (F\eta^\mathsf{S} _{ X})^*\alpha_ X^*({\dot {\mathsf{T}}} P), \\ \alpha_{\mathsf{S} X}^*({\dot {\mathsf{T}}}(\alpha_{ X}^*({\dot {\mathsf{T}}} P))) &\le \alpha_{\mathsf{S} X}^*(\mathsf{T}\alpha_{ X})^*({\dot {\mathsf{T}}}{\dot {\mathsf{T}}} P) \le \alpha_{\mathsf{S} X}^*(\mathsf{T}\alpha_{ X})^*(\mu^\mathsf{T}_{F X})^*({\dot {\mathsf{T}}} P) = (F\mu^\mathsf{S} _{ X})^*\alpha_{ X}^*({\dot {\mathsf{T}}} P). \end{align*}

Now assume that the ${\mathbb K}$ -Dijkstra structure $(p,\mathsf{T},{\dot {\mathsf{T}}})$ is Cartesian. Then the last two inequalities become equalities. Moreover,

\begin{align*} {\dot {\mathsf{S}}} (\,f^*( Y, Q)) &={\dot {\mathsf{S}}} ( X,(Ff)^* Q) =(\mathsf{S} X,\alpha_ X^*({\dot {\mathsf{T}}}((Ff)^* Q))) \\ &=(\mathsf{S} X,\alpha_ X^*(\mathsf{T} Ff)^*({\dot {\mathsf{T}}} Q)) =(\mathsf{S} X,(F\mathsf{S} f)^*\alpha_ Y^*({\dot {\mathsf{T}}} Q)) =(\mathsf{S} f)^*({\dot {\mathsf{S}}} ( Y, Q)). \end{align*}

Therefore ${\dot {\mathsf{S}}}$ is fibered. The functor ${\dot {\mathsf{S}}}$ is a $\mathbb K$ -lifting of $\mathsf{S}$ , because its restriction ${\dot {\mathsf{S}}}_ X:F^*\mathbb{P}_ X\to F^*\mathbb{P}_{\mathsf{S} X}$ to the fiber over $ X\in\mathbb D$ is the composite of $\alpha_ X^*$ and ${\dot {\mathsf{T}}}_ X^*$ , both of which belong to $\mathbb K$ . This concludes that $(F^*p,\mathsf{S},{\dot {\mathsf{S}}})$ is a Cartesian ${\mathbb K}$ -Dijkstra structure.

We will see examples of change-of-base of Dijkstra structures in Section 10.

3.4 Dijkstra Structures with Strengths 60

In Moggi’s theory of monadic models of computational effects (Moggi Reference Moggi1991), monad strengths are an important ingredient, since they allow us to sequence effectful computations with a common context. Below we discuss an extension of Dijkstra structures with strengths.

Let $(\mathbb{C},1,\times)$ be a category with finite products and $(\mathsf{T},\eta,\mu)$ be a monad on it. We first recall the concept of strength on $\mathsf{T}$ Moggi (Reference Moggi1991, Definition 3.2). It is a natural transformation $\theta_{ X, Y}: X\times \mathsf{T} Y\to\mathsf{T}( X\times Y)$ satisfying four axioms (below $\alpha_{ X, Y, Z}:( X\times Y)\times Z\to X\times( Y\times Z)$ is the associator):

\begin{align*} \mathsf{T}(\pi_2)\circ \theta_{1, X}&=\pi_2& \mathsf{T}\alpha_{ X, Y, Z}\circ \theta_{ X\times Y, Z}&=\theta_{ X, Y\times Z}\circ( X\times\theta_{ Y, Z})\circ\alpha_{ X, Y,\mathsf{T} Z}\\ \eta_{ X\times Y}&=\theta_{ X, Y}\circ( X\times\eta_ Y)& \mu_{ X\times Y}\circ \mathsf{T}\theta_{ X, Y}\circ\theta_{ X,\mathsf{T} Y}&=\theta_{ X, Y}\circ( X\times\mu_ Y).\end{align*}

Let $f: X\to \mathsf{T} Y$ be a morphism in $\mathbb{C}$ and $ Z\in\mathbb{C}$ be an object. The strength allows us to extend the domain and codomain of the effectful computation represented by f with Z. The extension is given as follows:

\begin{equation*} Z\cdot_\theta f\triangleq \theta_{ Z, Y}\circ({\rm id}_ Z\times f) \in \mathbb{C}( Z\times X,\mathsf{T}( Z\times Y)).\end{equation*}

Intuitively, the morphism $ Z\cdot_\theta f$ takes an input (z,x) from the extended input space $ Z\times X$ , applies the effectful computation f to x, and returns the result (z,v), where v is the value part of the computation f(x). The input z is directly forwarded to the output.

To extend the concept of strength to Dijkstra structures, we first set-up the concept of finite products on Dijkstra structures. We define finite products on a posetal fibration $p:\mathbb{P}\to\mathbb{C}$ to be the following data:

1. (1) a pair of terminal objects 1 in $\mathbb{C}$ and $\dot 1$ in $\mathbb{P}$ such that $p\dot 1=1$ , and

2. (2) a pair of binary product functors $(\!\times\!):\mathbb{C}^2\to\mathbb{C}$ and $(\!\mathbin{\dot\times}\!):\mathbb{P}^2\to\mathbb{P}$ such that $(\!\mathbin{\dot\times}\!)$ preserves Cartesian morphisms and p strictly preserves binary products in the following sense:

   \begin{align*} (\,f\times g)^*( P\mathbin{\dot\times} Q)&=f^* P\mathbin{\dot\times} g^* Q & p( P\mathbin{\dot\times} Q)&=p P\times p Q,& p\pi_i^{ P, Q}&=\pi_i^{p P,p Q}. \end{align*}

A pair of a posetal fibration and finite products on it is denoted by $p:(\mathbb{P},\dot 1,\mathbin{\dot\times})\to(\mathbb{C},1,\times)$ . We remark that every fiber of p has finite meets, and reindexing functors preserve these meets. ^{Footnote 2} The top element of $\mathbb{P}_ X$ is $!_ X^*\dot {1}\in\mathbb{P}_ X$ , and the meet of $ P, Q\in\mathbb{P}_ X$ is given by $ P\wedge Q\mathbin{\triangleq}\langle{\rm id}_ X,{\rm id}_ X\rangle^*\circ( P\mathbin{\dot\times} Q)$ , and the binary product $(\!\mathbin{\dot\times}\!)$ satisfies $ P\mathbin{\dot\times} Q=\pi_1^* P\wedge\pi_2^* Q$ . A logical analogy of the binary product $(\!\mathbin{\dot\times}\!)$ on $\mathbb{P}$ is to take the conjunction $\phi(i)\wedge\psi(j)$ of unary predicates $\phi(i)$ and $\psi(j)$ and regard it as a binary predicate.

We define a Dijkstra structure with finite products to be a tuple of a Dijkstra structure $(p,\mathsf{T},{\dot {\mathsf{T}}})$ and a finite product $(1,\dot 1,\times,\mathbin{\dot\times})$ on p. We write $(p:(\mathbb{P},\dot 1,\mathbin{\dot\times})\to(\mathbb{C},1,\times),\mathsf{T},{\dot {\mathsf{T}}})$ for such a tuple.

Again, Dijkstra structures with strengths are considered in the context of logical relations for strong monads (Filinski 1996; Reference Filinski2007; Goubault-Larrecq et al. Reference Goubault-Larrecq, Lasota and Nowak2008; Katsumata Reference Katsumata2005; Katsumata et al. Reference Katsumata, Sato and Uustalu2018). Since we are considering posetal fibrations, a natural transformation $\dot\theta$ is a strength on ${\dot {\mathsf{T}}}$ if it is above a strength on $\mathsf{T}$ . We formally state this property as follows.

A strength on a Dijkstra structure with finite products is related to the reasoning principle behind the frame rule, which we informally explain below. Let f be an imperative program over a program variable context $\Gamma$ , and suppose that it satisfies a Hoare triple $\Gamma\vdash\phi\{f\}\psi$ ; it is explicitly annotated with the context $\Gamma$ for the program f and pre/post conditions $\phi,\psi$ . Let $\rho$ be another assertion over a program variable context $\Delta$ that is disjoint from $\Gamma$ . Then the frame rule allows us to derive a Hoare triple on the program f when executed in the extended program variable context $\Gamma,\Delta$ :

The frame rule can be expressed in a general Dijkstra structure with finite products (see item (2) below) whose base monad has a strength. We show that the soundness of the frame rule is equivalent to the existence of a strength on the Dijkstra structure with finite products.

1. (1) There exists a strength $\dot\theta$ on ${\dot {\mathsf{T}}}$ such that $(\theta,\dot\theta)$ is a strength of the Dijkstra structure.

2. (2) $ P\{f\} Q$ implies $( R\mathbin{\dot\times} P)\{p R\cdot_\theta f\}( R\mathbin{\dot\times} Q)$ for any $ P, Q, R\in\mathbb{P}$ and morphism $f:p P\to \mathsf{T} p Q$ in $\mathbb{C}$ .

3. (3) $ R\mathbin{\dot\times} \mathrm{wp}(\,f, Q)\leq \mathrm{wp}(p R\cdot_\theta f,( R\mathbin{\dot\times} Q))$ holds for any $ P, Q, R\in\mathbb{P}$ and morphism $f:p P\to \mathsf{T} p Q$ in $\mathbb{C}$ .

Furthermore, $(\theta,\dot\theta)$ in (1) is Cartesian if and only if the inequality in (3) is an equality.

Proof. Assume $f \colon X \to \mathsf{T} Y$ . We first prove (1) implies (3). Let $Z=p R$ . Note that $\dot\theta \colon R \mathbin{\dot\times} {\dot {\mathsf{T}}} Q \to {\dot {\mathsf{T}}} ( R \mathbin{\dot\times} Q)$ is above $\theta_{Z,Y} \colon Z \times \mathsf{T} Y \to \mathsf{T} (Z \times Y)$ . Therefore, $ R \mathbin{\dot\times} \mathsf{T} Q \leq \theta_{Z,Y}^\ast({\dot {\mathsf{T}}}( R \mathbin{\dot\times} Q))$ , and we have an equality if $\dot\theta$ is Cartesian. Then

\begin{align*} R\mathbin{\dot\times} \mathrm{wp}(\,f, Q) &= R \mathbin{\dot\times} f^\ast {\dot {\mathsf{T}}} Q = ({\rm id}_Z \times f)^\ast ( R \mathbin{\dot\times} {\dot {\mathsf{T}}} Q) \leq ({\rm id}_Z \times f)^\ast \theta_{Z,Y}^\ast {\dot {\mathsf{T}}}( R \mathbin{\dot\times} Q) \\ &= (\theta_{Z,Y} \circ ({\rm id}_Z \times f))^\ast {\dot {\mathsf{T}}}( R \mathbin{\dot\times} Q) = ( Z\cdot_\theta f)^\ast {\dot {\mathsf{T}}}( R \mathbin{\dot\times} Q) = \mathrm{wp}( Z\cdot_\theta f,( R\mathbin{\dot\times} Q)) \end{align*}

We then show that (3) implies (1). By definition, $ \mathrm{wp}( Z\cdot_\theta {\rm id}_{\mathsf{T} Y},( R\mathbin{\dot\times} Q)) = \theta_{Z,Y}^\ast {\dot {\mathsf{T}}}( R\mathbin{\dot\times} Q)$ and by (3) we have an inclusion $ R \mathbin{\dot\times} \mathrm{wp}({\rm id}_{\mathsf{T} Y}, Q) = R \mathbin{\dot\times} {\dot {\mathsf{T}}} Q \leq \theta_{Z,Y}^\ast {\dot {\mathsf{T}}}( R\mathbin{\dot\times} Q) $ in the fiber above $Z\times \mathsf{T} Y$ . From Lemma 12, we obtain a strength $(\theta,\dot\theta)$ for the Dijkstra structure. If $ R \mathbin{\dot\times} {\dot {\mathsf{T}}} Q = \theta_{Z,Y}^\ast {\dot {\mathsf{T}}}( R\mathbin{\dot\times} Q)$ , then the strength $(\theta,\dot\theta)$ is Cartesian.

We now show that (3) implies (2). From (3), we get $ ( R\mathbin{\dot\times} \mathrm{wp}(\,f, Q))\{ Z\cdot_\theta f\}( R\mathbin{\dot\times} Q) $ By assumption, also $ P\{f\} Q$ , so $P \leq \mathrm{wp}(\,f, Q)$ . From all this, it follows that $ ( R\mathbin{\dot\times} P)\{ Z\cdot_\theta f\}( R\mathbin{\dot\times} Q) $

Finally, we show that (2) implies (3). By definition,

\begin{equation*} \mathrm{wp}(\,f, Q)\{f\} Q \implies ( R \mathbin{\dot\times} \mathrm{wp}(\,f, Q))\{Z\cdot_\theta f\}( R\mathbin{\dot\times} Q) \implies R \mathbin{\dot\times} \mathrm{wp}(\,f, Q) \leq \mathrm{wp}(Z\cdot_\theta f, ( R\mathbin{\dot\times} Q)). \end{equation*}

3.5 Strongest Postcondition Predicate Transformers

We turn our attention to strongest postcondition predicate transformers. In Hoare logic, the strongest postcondition with respect to a program f and a precondition $\phi$ is a formula $\psi$ such that (1) $\phi\{f\}\psi$ holds, and (2) if $\phi\{f\}\xi$ holds, then $\psi$ must entail $\xi$ .

We formulate the concept of strongest postcondition in a ${\mathbb K}$ -Dijkstra structure $(p:\mathbb{P}\rightarrow\mathbb{C},\mathsf{T},{\dot {\mathsf{T}}})$ . The strongest postcondition with respect to a morphism $f: X\to \mathsf{T} Y$ in $\mathbb{C}$ and an object $ P\in\mathbb{P}_ X$ is an object $S\in\mathbb{P}_{ Y}$ such that for any $ Q\in\mathbb{P}_ Y$ , $S\le Q$ if and only if $ P\{f\} Q$ . If such S exists, it is uniquely determined by f and P, hence we write it by $\mathrm{sp}(\,f, P)$ . To summarize, we obtain the three-way equivalence:

(9) \begin{equation} \mathrm{sp}(\,f, P)\le Q\iff P\{f\} Q\iff P\le\mathrm{wp}(\,f, Q).\end{equation}

This exhibits that the sppt corresponds to the left adjoint of the wppt, leading us to the following definition.

We note that the sppt $\mathrm{sp}(\,f,\_)$ does not need to belong to $\mathbb K$ . From this definition, if $\mathbb K$ is a subcategory of Pos such that every morphism in $\mathbb K$ is a right adjoint, then any ${\mathbb K}$ -Dijkstra structure admits the sppt. A typical example of such $\mathbb K$ is the subcategory ${\bf CLat}_\wedge$ of Pos consisting of complete lattices and meet-preserving functions. Since every morphism in ${\bf CLat}_\wedge$ is a right adjoint, any Dijkstra structure ${{\bf CLat}_\wedge}$ admits the sppt.

Like the case of wppts, sppts in general do not satisfy the composability. They do so if and only if the ${\mathbb K}$ -Dijkstra structure is Cartesian:

Theorem 15. Let $(p:\mathbb{P}\to\mathbb{C},\mathsf{T},{\dot {\mathsf{T}}})$ be a ${\mathbb K}$ -Dijkstra structure admitting the sppt. We have inequalities

(10) \begin{equation} \mathrm{sp}(\eta_ X, P)\le P,\quad \mathrm{sp}(\,f\bullet g, P)\le \mathrm{sp}(\,f,\mathrm{sp}(g, P)), \end{equation}

for any f,g, P of appropriate type. Moreover, both inequalities in (10) become equalities if and only if the ${\mathbb K}$ -Dijkstra structure is Cartesian.

Proof. (10) easily follows by taking the adjoint mate of (5) in Theorem 6. Next, assume that inequalities in (10) are equalities. We show that inequalities in (5) become equalities. From the assumption, we obtain

\begin{equation*} \mathrm{wp}(\eta_ X, P)=\mathrm{sp}(\eta_ X,\mathrm{wp}(\eta_ X, P))\le P,\end{equation*}

and

\begin{equation*} \mathrm{sp}(\,f,\mathrm{sp}(g,\mathrm{wp}(\,f\bullet g, P)))=\mathrm{sp}(\,f\bullet g,\mathrm{wp}(\,f\bullet g, P))\le P,\end{equation*}

which implies $\mathrm{wp}(\,f\bullet g, P)\le \mathrm{wp}(g,\mathrm{wp}(\,f, P))$ . These are the other direction of (5), hence proved. The converse is proven similarly.

Therefore, for a Cartesian Dijkstra structure $(p:\mathbb{P}\to\mathbb{C},\mathsf{T},{\dot {\mathsf{T}}})$ admitting sppts, the functor $p_{\mathsf{T},{\dot {\mathsf{T}}}}:\mathbb{P}_{\dot {\mathsf{T}}}\to\mathbb{C}_\mathsf{T}$ between Kleisli categories defined in Theorem 7 is a posetal bifibration (a posetal fibration such that each reindexing functor is a right adjoint; see Jacobs (Reference Jacobs1999, Definition 9.1.1) for the definition).

4.1 Ordered Objects

With the goal of having fibers with a partial order structure, we consider slices over ordered objects, defined below:

Equivalently, an ordered object is a pair of an object $\Omega$ and a functor $A:\mathbb{C}^{op}\rightarrow{\bf Pos}$ such that $U\circ A=\mathbb{C}(\_,\Omega)$ , where $U:{\bf Pos}\rightarrow{\bf Set}$ is the forgetful functor. The object $\Omega$ corresponds to the set of truth values, and a morphism $i: X\to \Omega$ in $\mathbb{C}$ corresponds to an $\Omega$ -valued predicate on X. The order $\le_ X$ compares the strength of predicates: $i\le_ X j$ means that i implies j.

To impose further conditions on the partial order, we parameterize Definition 16 by a subcategory $\mathbb K$ of Pos.

Example 19. Generalizing the previous example, let $\mathbb{C}$ be a category with finite limits. An internal partial order is a monomorphism $m:R\rightarrowtail\Omega\times\Omega$ satisfying reflexivity, transitivity, and antisymmetry expressed diagrammatically; see Lane and Moerdijk (Reference Lane and Moerdijk1994, Section IV.8). For each $ X\in\mathbb{C}$ , the following binary relation $\le_ X$ over $\mathbb{C}( X,\Omega)$ becomes a partial order:

\begin{equation*} f\le_ X g \iff \exists{h: X\to R}~.~\langle f,g\rangle=m\circ h,\end{equation*}

Then $(\Omega,\le_{ X}\!)$ becomes an ordered object in $\mathbb{C}$ . To summarize, an internal partial order in $\mathbb{C}$ induces an ordered object in $\mathbb{C}$ .

Example 20. Not every ordered object arises in the way given in Example 19. In categories without finite limits (such as Kleisli categories of monads), we cannot have an internal partial order, but we can still have ordered objects. For example, the Kleisli category of the finite probability distribution monad $\mathsf{D}$ (Example 40) over Set does not have finite products, but there is an ordered object $\{\bot,\top\}$ (a two-point set) whose order is defined by

\begin{equation*} f\le_ X g\iff \forall{x\in X}~.~f(x)(\top)\le g(x)(\top).\end{equation*}

When $\mathbb{C}$ comes with a Pos-enrichment, that is, an assignment of a partial order $\sqsubseteq_{ X, Y}$ to each homset $\mathbb{C}( X, Y)$ making the composition monotone, any object $\Omega\in\mathbb{C}$ determines an ordered object $(\Omega,\sqsubseteq_{\_,\Omega})$ . However, it is not desirable to restrict our attention to such ordered objects in Pos-enriched categories, because there can be cases where the order $\sqsubseteq_{ X,\Omega}$ is not adequate for comparing strength of predicates on X. For instance, the category Set may be seen as a Pos-enriched category by considering the discrete order on each homset. However, the ordered object $(\Omega,=_{\_,\Omega})$ based on this enrichment only gives the discrete order on $\Omega$ -valued predicates, which is not very useful. Therefore we need freedom to give an ordered object independently from the Pos-enrichment on a category.

4.2 Lax Slice Construction 60

Let $\mathbb{C}$ be a category and $(\Omega,\le\!)$ be an ordered object in $\mathbb{C}$ belonging to a subcategory $\mathbb K$ of Pos. We define the lax slice category ${\mathbb{C}/_{\!\mathrm{\ell}}\Omega}$ by the following data:

• An object is a morphism in $\mathbb{C}$ whose codomain is $\Omega$ .

• A morphism from i to j is a morphism $h:{\rm dom}(i)\to {\rm dom}(j)$ in $\mathbb{C}$ such that $i\le_{{\rm dom}(i)} j\circ h$ .

The domain functor $d^{{\mathbb{C}},{\Omega}}:{\mathbb{C}/_{\!\mathrm{\ell}}\Omega}\rightarrow \mathbb{C}$ is defined by

\begin{align*} d^{{\mathbb{C}},{\Omega}} i&\mathbin{\triangleq} {\rm dom}(i),& d^{{\mathbb{C}},{\Omega}}(\,f)&\mathbin{\triangleq} f.\end{align*}

It is a $\mathbb K$ -fibration, and the fiber category $({\mathbb{C}/_{\!\mathrm{\ell}}\Omega})_ X$ at $ X\in\mathbb{C}$ is the poset $(\mathbb{C}( X,\Omega),\le_ X\!)$ . The pullback of $i: X\rightarrow\Omega$ along $h: Y\rightarrow X$ is given by $h^*i=i\circ h$ .

We further investigate the 2-categorical nature of the construction of lax slice categories. We introduce the following 2-categories ${\bf CO}(\mathbb K)$ and ${\bf CO}_c(\mathbb K)$ whose 0-cells are categories with ordered objects belonging to a subcategory $\mathbb K$ of Pos.

• A 0-cell is a tuple $(\mathbb{C},\Omega,\le\!)$ consisting of a category $\mathbb{C}$ and an ordered object $(\Omega,\le\!)$ in $\mathbb{C}$ belonging to $\mathbb K$ .

• A 1-cell from $(\mathbb{C},\Omega,\le\!)$ to $(\mathbb D,\Pi,\le\!)$ is a pair of a functor $F:\mathbb{C}\to\mathbb D$ and a morphism $o:F\Omega\to \Pi$ in $\mathbb D$ such that $o\circ F\_$ is a monotone function belonging to $\mathbb K$ in the following sense:

  (12) \begin{equation} \forall{ X\in\mathbb{C}}~.~ o\circ F\_ \in\mathbb K((\mathbb{C}( X,\Omega),\le_ X\!),(\mathbb D(F X,\Pi),\le_{F X}\!)). \end{equation}
  The identity 1-cell and the composition of 1-cells are defined by
  \begin{align*} {\rm id}_{(\mathbb{C},\Omega,\le\!)}&\mathbin{\triangleq}({\rm Id}_\mathbb{C},{\rm id}_\Omega), & (F,o)\circ (G,o')&\mathbin{\triangleq}(F\circ G,o\circ Fo'). \end{align*}

• For 1-cells $(F,o),(G,o'):(\mathbb{C},\Omega,\le\!)\to(\mathbb D,\Pi,\le\!)$ , a 2-cell from the former to the latter is a natural transformation $\alpha:F\to G$ such that $o\le o'\circ\alpha_\Omega$ .

We extend the lax slice construction to 2-functors. We first mention a few facts:

• For a 1-cell $(F,o)\in{\bf CO}(\mathbb K)((\mathbb{C},\Omega,\le\!),(\mathbb D,\Pi,\le\!))$ , let $F_o:{\mathbb{C}/_{\!\mathrm{\ell}}\Omega}\to{\mathbb D/_{\!\mathrm{\ell}}\Pi}$ be the functor defined by

  \begin{align*}F_o(i) & \mathbin{\triangleq} o\circ F i, & \,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,F_o(\,f) & \mathbin{\triangleq} F f.\end{align*}
  From (12) it follows that $(F,F_o)$ is a fibered $\mathbb K$ -functor from $d^{{\mathbb{C}},{\Omega}}$ to $d^{{\mathbb D},{\Pi}}$ .

• There is a bijective correspondence between 2-cells in ${\bf CO}(\mathbb K)$ and ${\mathbb K}\text{-}{\bf Fib}$ :

  (13) \begin{align} &{\bf CO}(\mathbb K)((\mathbb{C},\Omega,\le\!),(\mathbb D,\Pi,\le\!))((F,o),(G,o'))\end{align}
  (14) \begin{align} &=\{\alpha:F\to G~|~o\le o'\circ \alpha_\Pi\}\end{align}
  (15) \begin{align} &=\{\alpha:F\to G~|~\forall{i}~.~F_oi\le \alpha_{{\rm dom}(i)}^*(G_{o'}i)\} \end{align}
  (16) \begin{align} &\cong{\mathbb K}\text{-}{\bf Fib}(d^{{\mathbb{C}},{\Omega}},d^{{\mathbb D},{\Pi}})((F,F_o),(G,G_o)) . \end{align}
  The equality between (14) and (15) is by
  \begin{align*} (\forall{i}~.~F_oi\le \alpha_{{\rm dom}(i)}^*(G_{o'}i)) & \iff (\forall{i}~.~o\circ Fi\le o'\circ Gi\circ \alpha_{{\rm dom}(i)}=o'\circ \alpha_\Pi\circ Fi)\\ & \iff o\le o'\circ \alpha_\Pi, \end{align*}
  and the bijection from (15) to (16) is $\Xi^{-1}$ given in (1). A similar bijective correspondence between 2-cells of ${\bf CO}_c(\mathbb K)$ and ${\mathbb K}\text{-}{\bf Fib}_c$ also holds by using $\Xi^{-1}_c$ instead of $\Xi^{-1}$ :
  \begin{align*} &{\bf CO}_c(\mathbb K)((\mathbb{C},\Omega,\le\!),(\mathbb D,\Pi,\le\!))((F,o),(G,o'))\\ &\cong{\mathbb K}\text{-}{\bf Fib}_c(d^{{\mathbb{C}},{\Omega}},d^{{\mathbb D},{\Pi}})((F,F_o),(G,G_o)). \end{align*}

From these, we define 2-functors $L_{\mathbb K}:{\bf CO}(\mathbb K)\to{\mathbb K}\text{-}{\bf Fib}$ and $L_{\mathbb K,c}:{\bf CO}_c(\mathbb K)\to{\mathbb K}\text{-}{\bf Fib}_c$ by

\begin{align*} L_{\mathbb K}(\mathbb{C},\Omega,\le\!)&\mathbin{\triangleq}d^{{\mathbb{C}},{\Omega}}:{\mathbb{C}/_{\!\mathrm{\ell}}\Omega}\rightarrow \mathbb{C}, & L_{\mathbb K}(F,o)&\mathbin{\triangleq}(F,F_o), & L_{\mathbb K}(\alpha)&\mathbin{\triangleq}\Xi^{-1}(\alpha)\\ L_{\mathbb K,c}(\mathbb{C},\Omega,\le\!)&\mathbin{\triangleq}d^{{\mathbb{C}},{\Omega}}:{\mathbb{C}/_{\!\mathrm{\ell}}\Omega}\rightarrow \mathbb{C}, & L_{\mathbb K,c}(F,o)&\mathbin{\triangleq}(F,F_o), & L_{\mathbb K,c}(\alpha)&\mathbin{\triangleq}\Xi^{-1}_c(\alpha).\end{align*}

The verification of this being a 2-functor is routine, and omitted.

Proof. We first prove the case of $L_{\mathbb K}$ ; the proof of the case $L_{\mathbb K,c}$ is similar. It suffices to show that each hom-functor:

\begin{equation*} L_{\mathbb K}: {\bf CO}(\mathbb K)((\mathbb{C},\Omega,\le\!),(\mathbb D,\Pi,\le\!)) \to {\mathbb K}\text{-}{\bf Fib}(d^{{\mathbb{C}},{\Omega}},d^{{\mathbb D},{\Pi}})\end{equation*}

is bijective on objects, because full faithfulness is already guaranteed by (13)–(16). Let $(F,\dot F):d^{{\mathbb{C}},{\Omega}}\to d^{{\mathbb D},{\Pi}}$ be a 1-cell in ${\mathbb K}\text{-}{\bf Fib}$ . We show that $(F,\dot F({\rm id}_\Omega))\in{\bf CO}(\mathbb K)$ is the unique 1-cell yielding $(F,\dot F)$ . We first show the functor equality $F_{\dot F({\rm id}_\Omega)}=\dot F:{\mathbb{C}/_{\!\mathrm{\ell}}\Omega}\to{\mathbb D/_{\!\mathrm{\ell}}\Pi}$ .

\begin{align*} F_{\dot F({\rm id}_\Omega)}i&= \dot F({\rm id}_\Omega)\circ Fi =(F i)^*(\dot F({\rm id}_\Omega)) =\dot F(i^*({\rm id}_\Omega)) =\dot Fi,\\ F_{\dot F({\rm id}_\Omega)}h&=Fh=\dot Fh. \end{align*}

Therefore, $(F,\dot F({\rm id}_\Omega))$ is a 1-cell in ${\bf CO}(\mathbb K)$ . Next, let $(F,o)\in{\bf CO}(\mathbb K)$ be a 1-cell such that $(F,F_o)=(F,\dot F)$ . Then $\dot F({\rm id}_\Omega)=F_o({\rm id}_\Omega)=o$ , hence $(F,o)=(F,\dot F({\rm id}_\Omega))$ . This proves that $L_{\mathbb K}$ is bijective on objects.

We characterize the image of $L_{\mathbb K}$ and $L_{\mathbb K,c}$ . Let $p:\mathbb{P}\to\mathbb{C}$ be a $\mathbb K$ -fibration. A split generic object $\Omega\in\mathbb{P}$ is such that for any object $ P\in\mathbb{P}$ , there exists a unique morphism $\chi:\to p P$ in $p\Omega$ ${\mathbb{P}}$ such that $ P=\chi^*\Omega$ Jacobs (Reference Jacobs1999, Definition 5.2.1). Note that split generic objects are mutually isomorphic.

Proof. We first show that $L_{\mathbb K}$ is essentially surjective on 0-cells. Let $p:\mathbb{P}\to\mathbb{C}$ be a $\mathbb K$ -fibration with a split generic object $\Omega\in\mathbb{P}$ . We first extract an ordered object in $\mathbb{C}$ belonging to $\mathbb K$ . From the definition of split generic object, the function $(\!-\!)3^*\Omega:\mathbb{C}( X,p\Omega)\to {\bf Obj}(\mathbb{P}_ X)$ is a bijection; we write $\Psi_ X$ for its inverse. We put a partial order on $\mathbb{C}( X,p\Omega)$ by: $f\le_ X g\iff f^*\Omega\le g^*\Omega$ . Then the bijection becomes an isomorphism between $(\mathbb{C}( X,p\Omega),\le_ X\!)$ and $\mathbb{P}_ X$ in Pos, which further becomes an isomorphism in $\mathbb K$ because $\mathbb K$ is replete. Then for any morphism $f: X\to Y$ in $\mathbb{C}$ , the composite of the following morphisms in $\mathbb K$ is equal to $\_\circ f$ :

Therefore, $p\Omega$ is an ordered object in $\mathbb{C}$ belonging to $\mathbb K$ . It is then routine to show that $d^{{\mathbb{C}},{p\Omega}}:{\mathbb{C}/_{\!\mathrm{\ell}}p\Omega}\rightarrow \mathbb{C}$ is isomorphic to $p:\mathbb{P}\to\mathbb{C}$ in ${\mathbb K}\text{-}{\bf Fib}_{g}$ . The case of $L_{\mathbb K,c}$ is proved similarly.

4.3 Characterizing ${\mathbb K}$ -Dijkstra Structures on Domain Fibrations

Recall that a Cartesian ${\mathbb K}$ -Dijkstra structure is precisely a monad in ${\mathbb K}\text{-}{\bf Fib}_c$ . The local isomorphism theorem (Theorem 23) implies the following characterization of Cartesian ${\mathbb K}$ -Dijkstra structures on domain fibrations.

1. (1) A Cartesian ${\mathbb K}$ -Dijkstra structure whose $\mathbb K$ -fibration is $d^{{\mathbb{C}},{\Omega}}:{\mathbb{C}/_{\!\mathrm{\ell}}\Omega}\rightarrow \mathbb{C}$ .

2. (2) A pair of a monad $\mathsf{T}$ on $\mathbb{C}$ and an EM monotone $\mathsf{T}$ -algebra $(o,\Omega)$ belonging to $\mathbb K$ (when $\mathbb K={\bf Pos}$ , we omit “belonging to $\mathbb K$ ”), that is, an EM algebra such that $o\circ\mathsf{T}\_$ satisfies (12).

In many situations, monads for modeling computational effects are composites of simpler monads through distributive laws. We extend our lifting theory of monads to composite monads. Let $\mathsf{T},\mathsf{S}$ be monads on $\mathbb{C}$ and $\alpha:\mathsf{S} \mathsf{T}\rightarrow \mathsf{T} \mathsf{S}$ be a distributive law (see Section 2). We are interested in EM monotone $\mathsf{T}\circ_\alpha \mathsf{S}$ -algebras, which give Cartesian liftings of $\mathsf{T}\circ_\alpha \mathsf{S}$ . EM algebras of composite monads are studied in Beck (Reference Beck1969, Section 2), Manes and Mulry (Reference Manes and Mulry2007, Theorem 2.4.3). Below we mildly extend these results.

1. (1) An EM monotone $\mathsf{T}\circ_\alpha \mathsf{S}$ -algebra $(o,\Omega)$ belonging to $\mathbb K$ .

2. (2) A pair of an EM monotone $\mathsf{T}$ -algebra $(t,\Omega)$ belonging to $\mathbb K$ and an EM monotone $\mathsf{S}$ -algebra $(s,\Omega)$ belonging to $\mathbb K$ satisfying

   (17) \begin{equation} s\circ \mathsf{S} t=t\circ \mathsf{T} s\circ\alpha_\Omega. \end{equation}

3. (3) A triple $(\dot{\mathsf{T}},\dot{\mathsf{S}},\dot\alpha)$ where ${\dot {\mathsf{T}},\dot{\mathsf{S}}}$ are, respectively, Cartesian liftings of $\mathsf{T},\mathsf{S}$ along $d^{{\mathbb{C}},{\Omega}}$ , and ${\dot\alpha:\dot {\mathsf{S}}\dot {\mathsf{T}}\rightarrow\dot {\mathsf{T}}\dot {\mathsf{S}}}$ is a distributive law above $\alpha$ whose components are Cartesian.

Proof. The bijection between (2) and (3) is proved in the same way as Theorem 26. We show a bijective correspondence between (1) and (2). Let $(o,\Omega)$ be an EM monotone $\mathsf{T}\circ_\alpha\mathsf{S}$ -algebra belonging to $\mathbb K$ . Then it is routine to show that $t\mathbin{\triangleq} o\circ T\eta^\mathsf{S}_\Omega:\mathsf{T}\Omega\to\Omega$ and $s\mathbin{\triangleq} o\circ \eta^\mathsf{T}_{\mathsf{S}\Omega}:\mathsf{S}\Omega\to\Omega$ are both EM algebras. To show that t,s are monotone and belong to $\mathbb K$ , observe that functions on the left-hand side below are equal to composite monotone functions on the right-hand side belonging to $\mathbb K$ :

Conversely, let $t:\mathsf{T}\Omega\to\Omega,s:\mathsf{S}\Omega\to\Omega$ be EM monotone algebras belonging to $\mathbb K$ . Then it is routine to show that $o\mathbin{\triangleq} t\circ \mathsf{T} s$ is an EM $\mathsf{T}\circ_\alpha\mathsf{S}$ -algebra, provided that t,s satisfies (17). Moreover, o is a monotone and belongs to $\mathbb K$ because the function on the left-hand side below is the composite monotone function on the right-hand side, which belongs to $\mathbb K$ :

We note that the condition (17) appears in Beck (Reference Beck1969, Section 2). This theorem says that to identify a lifting of $\mathsf{T}\circ_\alpha \mathsf{S}$ , it suffices to identify a pair of EM monotone $\mathsf{T}$ - and $\mathsf{S}$ -algebras satisfying (17).

We next apply the local isomorphism theorem (Theorem 23) to characterize strengths on Cartesian Dijkstra structures whose fibrations are domain fibrations. We first identify the situation when domain fibrations have finite products.

1. (1) The domain fibration $d^{{\mathbb{C}},{\Omega}}:{\mathbb{C}/_{\!\mathrm{\ell}}\Omega}\rightarrow \mathbb{C}$ has finite products $(1,\dot 1,\times,\mathbin{\dot\times})$ .

2. (2) $\mathbb{C}$ has finite products $(1,\times)$ , and there are morphisms $\top:1\to\Omega, m:\Omega^2\to \Omega$ such that $\top\circ !_ X$ and $m\circ\langle \_,\_\rangle$ give finite meets in the poset $(\mathbb{C}( X,\Omega),\le_ X\!)$ .

1. (1) a strength on the Cartesian Dijkstra structure, and

2. (2) a strength $\theta$ on $\mathsf{T}$ such that $m\circ({\rm id}\times o)\le o\circ \mathsf{T}m\circ\theta_{\Omega,\Omega}$ .

Proof. Let $(\theta,\dot\theta)$ be a strength on a Cartesian Dijkstra structure. From Lemma 12, and the assumption that both $\mathbin{\dot\times}$ and $\mathsf{T}$ are fibered, the strength bijectively corresponds to the 2-cell $(\theta,\dot\theta)$ in ${{\bf Pos}}\text{-}{\bf Fib}$ such that $\theta$ is a strength on $\mathsf{T}$ .

By the local isomorphism theorem, such a 2-cell bijectively corresponds to a 2-cell in ${\bf CO}({\bf Pos})$ (see the right diagram above) where $\theta$ is a strength of $\mathsf{T}$ . This is equivalent to that $\theta$ is a strength on $\mathsf{T}$ satisfying $m\circ({\rm id}\times o)\le o\circ \mathsf{T} m \circ\theta.$

4.4 Algebraic Operations and Weakest Precondition Predicate Transformer

Various program constructs that cause computational effects can be naturally modeled by Plotkin and Power’s algebraic operations (Plotkin and Power Reference Plotkin, Power, Brooks and Mislove2001). They frequently occur in the monadic semantics of effectful programs. In this section, we give a wppt semantics of algebraic operations in the Cartesian Dijkstra structures whose fibrations are domain fibrations.

In this section we fix a Cartesian category $(\mathbb{C},1,\times)$ , an ordered object $(\Omega,\le\!)$ in $\mathbb{C}$ belonging to a subcategory $\mathbb K$ of Pos, and a strong monad $(\mathsf{T},\eta,\mu,\theta)$ .

Definition 30. A morphism $g: \to A$ in $\mathsf{T} B$ ${\mathbb{C}}$ is called generic effect (Plotkin and Power Reference Plotkin, Power, Brooks and Mislove2001). For an EM $\mathsf{T}$ -algebra $o:\mathsf{T} X\rightarrow X$ , we define the following operation ${{\mathrm{op}}}\!(o,g):\mathbb{C}( Y,A)\times \mathbb{C}( Y\times B, X)\to\mathbb{C}( Y, X)$ by

\begin{equation*} {{\mathrm{op}}}\!(o,g)(a,b) \mathbin{\triangleq} o \circ \mathsf{T}(b) \circ\theta_{ Y,B}\circ\langle{\rm id}_ Y,g\circ a\rangle.\end{equation*}

We specifically write $\alpha(g)_ X$ for ${{\mathrm{op}}}\!(\mu_ X,g)$ and call it the algebraic operation corresponding to g.

The first and second arguments of ${{\mathrm{op}}}\!(o,g)$ are, respectively, called a parameter and an argument. The above definition of algebraic operation is different from the original one presented in Plotkin and Power (Reference Plotkin, Power, Brooks and Mislove2001). Originally, an algebraic operation corresponding to a generic effect $g:A\to\mathsf{T} B$ is a certain natural transformation $\alpha_ X:A\times (B\Rightarrow \mathsf{T} X)\to\mathsf{T} X$ . In this paper, we present it as an operation on morphisms in a Cartesian category.

Proposition 31. Let $o:\mathsf{T}\Omega\to\Omega$ be an EM monotone $\mathsf{T}$ -algebra belonging to $\mathbb K$ . Then for any generic effect $g:A\to\mathsf{T} B$ and morphism $a: Y\to A$ , we have

\begin{equation*} {{\mathrm{op}}}\!(o,g)(a,\_)\in \mathbb K((\mathbb{C}( Y\times B,\Omega),\le_{ Y\times B}\!),(\mathbb{C}( Y,\Omega),\le_{ Y}\!)).\end{equation*}

Proof. Notice that ${{\mathrm{op}}}\!(o,g)(a,\_)$ is the composite of the following morphisms in $\mathbb K$ :

The following theorem helps us (in Section 7) to compute the wppt of programs involving algebraic operations:

Theorem 32. Let $o:\mathsf{T}\Omega\rightarrow\Omega$ be an EM monotone $\mathsf{T}$ -algebra belonging to $\mathbb K$ and $(d^{{\mathbb{C}},{\Omega}},\mathsf{T},\mathsf{T}_o)$ be the corresponding Cartesian ${\mathbb K}$ -Dijkstra structure. Then the following equality holds for any generic effect $g:A\to\mathsf{T} B$ and morphism $a: Y\to A,b: Y\times B\to\mathsf{T} X,i: X\to\Omega$ :

\begin{equation*} \mathrm{wp}(\alpha(g)_ X(a,b), )i= {{\mathrm{op}}}\!(o,g)(a,\mathrm{wp}(b, )i).\end{equation*}

Proof. The equation easily follows from the EM axiom $o\circ\mu_\Omega=o\circ \mathsf{T} o$ :

\begin{align*} \mathrm{wp} (\alpha (g)_ X (a, b), i) & = o \circ \mathsf{T} i \circ \mu_ X \circ \mathsf{T} (b) \circ \theta \circ \langle {{\mathrm{id}}}, g \circ a \rangle\\ & = o \circ \mu_{\Omega} \circ \mathsf{T}^2 i \circ \mathsf{T} (b) \circ \theta \circ \langle {{\mathrm{id}}}, g \circ a \rangle\\ & = o \circ \mathsf{T} o \circ \mathsf{T}^2 i \circ \mathsf{T} (b) \circ \theta \circ \langle {{\mathrm{id}}}, g \circ a \rangle\\ & = {{\mathrm{op}}}\!(o, g) (a, \mathrm{wp} (b, i)) . \end{align*}

When $\mathbb{C}$ has distributive finite coproducts, we can make algebraic operations to take tuples of morphisms as arguments. Below we look at the case $n=2$ . We write 2 for the coproduct $1+1$ . For the setting above, it is useful to define an operator $\beta \colon \mathbb{C}( X, Y) \times \mathbb{C}( X, Y) \to \mathbb{C}( X\times 2, Y)$ :

(18) \begin{equation} \beta(b_1,b_2) \triangleq [b_1\circ r_{ X}, b_2\circ r_{ X}] \circ \mathrm{dist}_{ Y,1,1}\end{equation}

where $r_{ X} : X\times 1 \to X$ is the right unitor and $\mathrm{dist}_{X,Y,Z} \circ X\times(Y+Z) \to X\times Y + X\times Z$ is the distributive law of the product over the coproduct. Then we can show:

Corollary 33. Let $o:\mathsf{T}\Omega\rightarrow\Omega$ be an EM monotone $\mathsf{T}$ -algebra belonging to $\mathbb K$ and $(d^{{\mathbb{C}},{\Omega}},\mathsf{T},\mathsf{T}_o)$ be the corresponding Cartesian ${\mathbb K}$ -Dijkstra structure. For any generic effect $g:A\to\mathsf{T} 2$ and morphism $a: Y\to A,b_1,b_2: Y\to\mathsf{T} X,i: X\to\Omega$ , the following equality holds:

\begin{equation*} \mathrm{wp}(\alpha(g)_ X(a,\beta(b_1,b_2)), )i= op(o,g)(a, \beta(\mathrm{wp}(b_1,i),\mathrm{wp}(b_2,i))).\end{equation*}

Proof. The key step is checking that $\mathrm{wp}(\beta(b_1,b_2),i) = \beta(\mathrm{wp}(b_1,i),\mathrm{wp}(b_2,i))$ . Indeed,

\begin{align*} \mathrm{wp}(\beta(b_1,b_2),i) &= o \circ \mathsf{T} i \circ [b_1\circ r, b_2\circ r] \circ\mathrm{dist} \\ &= [o \circ \mathsf{T} i \circ b_1\circ r, o \circ \mathsf{T} i \circ b_2\circ r] \circ\mathrm{dist} \\ &= \beta(\mathrm{wp}(b_1,i),\mathrm{wp}(b_2,i)). \end{align*}

6.1 Dijkstra Structures for Composite Monads

We next visit examples of liftings of composite monads via distributive laws.

Theorem 48. There are exactly four Cartesian liftings of ${\mathsf{P}^+} \circ_\beta \mathsf{M}$ along $d^{{{\bf Set}},{{\bf 2}}}$ . Let us denote these liftings by ${\mathsf{P}^+}_a\circ_\beta \mathsf{M}_b$ , where (a,b) range over the four-point set $\{\mathrm{may},\mathrm{must}\}\times \{\mathrm{tot},\mathrm{par}\}$ . Each lifting is explicitly described as follows:

\begin{equation*} {\mathsf{P}^+}_a\circ_\beta \mathsf{M}_b(I,X)=\left( {\mathsf{P}^+}(\mathsf{M}(I)), \left\{\begin{array}{ll} \{U~|~U\cap X\neq\emptyset\} & (a=\mathrm{may},b=\mathrm{tot}) \\ \{U~|~U\subseteq X\} & (a=\mathrm{must},a=\mathrm{tot}) \\ \{U~|~U\cap(X+\{*\})\neq\emptyset\} & (a=\mathrm{may},b=\mathrm{par}) \\ \{U~|~U\subseteq X+\{*\}\} & (a=\mathrm{must},b=\mathrm{par}) \end{array}\right. \right)\end{equation*}

Next, we look at examples of composite monads with the counting monad $\mathsf{C}$ in Example 43. The counting monad is useful for measuring various intensional quantities of program executions. The distributive law of any Set-monad $\mathsf{T}$ over the counting monad $\mathsf{C}$ exists and is provided by the unique strength $\theta_{ X, Y}: X\times \mathsf{T} Y\rightarrow \mathsf{T}( X\times Y)$ of $\mathsf{T}$ given as (22). Here we discuss giving a Cartesian lifting of $\mathsf{T}\circ_\theta \mathsf{C}$ .

Example 50. We consider the instance of Theorem 49 where $\mathsf{T}$ is the finite probability distribution monad $\mathsf{D}$ . The composite monad $\mathsf{D}\circ_\theta \mathsf{C}$ is suitable for modeling probabilistic programs that report cost counting during their executions. We will see this in Section 7. The EM monotone $\mathsf{D}$ -algebra $\mathrm{E}:\mathsf{D}[0,\infty]\rightarrow[0,\infty]$ and the successor function $s:[0,\infty]\rightarrow[0,\infty]$ evidently satisfies the equality condition of Theorem 49:

\begin{equation*} \mathrm{E}\circ \mathsf{D} s= \lambda{\mu}~.~{E_{x\sim \mu}[1+x]}= \lambda{\mu}~.~1+{E_{x\sim \mu}[ ]}x= s\circ \mathrm{E}.\end{equation*}

Therefore, E and o(s) satisfy (17) by Theorem 49. The composite $\mathsf{D}_{\mathrm{E}}\circ \mathsf{C}_{{o(s)}}$ is a Cartesian lifting of $\mathsf{D}\circ_\theta\mathsf{C}$ along $d^{{{\bf Set}},{[0,\infty]}}$ and is computed as $\mathsf{D}_{\mathrm{E}}\circ \mathsf{C}_{{o(s)}}(i) = \lambda{\mu}~.~{E_{(c,x)\sim \mu}[c+i(x)]}. $ The wppt in the Dijkstra structure $(d^{{{\bf Set}},{[0,\infty]}},\mathsf{D}\circ_\theta\mathsf{C},\mathsf{D}_{\mathrm{E}}\circ \mathsf{C}_{{o(s)}})$ is

\begin{equation*} \mathrm{wp}(f, )j(x)={E_{(c,y)\sim f(x)}[c+j(y)]}\quad (\,f: X\rightarrow \mathsf{D}\circ_\theta\mathsf{C}( Y),j: Y\rightarrow[0,\infty]).\end{equation*}

Example 51. The nonempty powerset monad $\mathsf{P}^+$ distributes over the finite indexed distribution monad $\mathsf{{I}}$ . The distributive law $\gamma:\mathsf{{I}}\circ{\mathsf{P}^+}\rightarrow {\mathsf{P}^+}\circ\mathsf{{I}}$ is given by

\begin{equation*} \gamma_ X[(p_1,U_1),\cdots,(p_n,U_n)]\mathbin{\triangleq} \{[(p_1,x_1),\cdots,(p_n,x_n)]~|~x_1\in U_1,\cdots,x_n\in U_n\}.\end{equation*}

It is easy to check that the expectation function $\mathrm{IE}:\mathsf{{I}}[0,\infty]\rightarrow[0,\infty]$ (Example 46) distributes over $\mathrm{sup}:{\mathsf{P}^+}[0,\infty]\rightarrow[0,\infty]$ (Example 44). Therefore, the wppt in the Cartesian Dijkstra structure $(d^{{{\bf Set}},{[0,\infty]}},{\mathsf{P}^+}\circ_\gamma\mathsf{{I}},{{\mathsf{P}^+}_{\mathrm{sup}}}\circ\mathsf{{I}}_{\mathrm{IE}})$ is

\begin{equation*} \mathrm{wp}(f, )i(j)=\sup_{\nu\in f(j)}{IE_{x\sim \nu}[i(x)]}\quad (\,f: X\rightarrow {\mathsf{P}^+}\circ_\gamma\mathsf{{I}}( Y), i: Y\to[0,\infty], j\in X ).\end{equation*}

This wppt performs angelic choice. We can also derive the one performing demonic choice by replacing $\sup$ with $\inf$ in this argument. Finally, we compose it with the counting monad $\mathsf{C}$ . This yields the Cartesian Dijkstra structure $(d^{{{\bf Set}},{[0,\infty]}},({\mathsf{P}^+}\circ_\gamma\mathsf{{I}})\circ_\theta \mathsf{C}, {\mathsf{P}^+}_{\mathrm{sup}}\circ\mathsf{{I}}_{\mathrm{IE}}\circ \mathsf{C}_{{o(s)}})$ , whose wppt is:

\begin{equation*} \mathrm{wp}(f, )i(j)=\sup_{\nu\in f(j)}{IE_{(c,x)\sim \nu}[c+i(x)]}\quad (\,f: X\rightarrow {\mathsf{P}^+}\circ_\gamma\mathsf{{I}}( Y), i: Y\to[0,\infty], j\in X ).\end{equation*}

Recently some new approaches to monadic models of nondeterministic and probabilistic branching have been proposed. Moggi et al. construct a monad structure on the composite functor ${\mathsf{P}^+}\circ \mathsf{T}$ for any monad $\mathsf{T}$ over Set (Moggi et al. Reference Moggi, Taha and Thunberg2020). This is not given by distributive law. Goy and Petrisan employ a weaker notion of distributive law to combine the powerset monad and the probability distribution monad (Goy and Petrisan Reference Goy and Petrisan2020). We leave it to a future work to study wppts for the monads arising from these approaches.