Kleisli, Parikh and Peleg Compositions and Liftings for Multirelations

TL;DR

This paper formalizes various compositions and liftings of multirelations, revealing their algebraic properties and conditions under which they form categories, advancing the semantic modeling of nondeterministic systems.

Contribution

It provides relational formalizations of Kleisli, Parikh, and Peleg compositions for multirelations, analyzing their algebraic properties and categorical structures.

Findings

Kleisli composition is associative but may lack units.

Parikh composition is non-associative and unitless, forming a category on up-closed multirelations.

Peleg composition has units but is not necessarily associative, forming a category on union-closed multirelations.

Abstract

Multirelations provide a semantic domain for computing systems that involve two dual kinds of nondeterminism. This paper presents relational formalisations of Kleisli, Parikh and Peleg compositions and liftings of multirelations. These liftings are similar to those that arise in the Kleisli category of the powerset monad. We show that Kleisli composition of multirelations is associative, but need not have units. Parikh composition may neither be associative nor have units, but yields a category on the subclass of up-closed multirelations. Finally, Peleg composition has units, but need not be associative; a category is obtained when multirelations are union-closed.

Equations

$$(a,A)\in R\circ S\leftrightarrow \exists B.(a,B)\in R\wedge A=\bigcup S(B),$$

$$(a,A)\in R\diamond S\leftrightarrow \exists B.(a,B)\in R\wedge (\forall b\in B.(b,A)\in S);$$

$$(a,A)\in R\ast S\leftrightarrow \exists B.(a,B)\in R\wedge (\exists f.(\forall b\in B.(b,f(b))\in S)\wedge A=\bigcup f(B)),$$

$$R\bullet S=R;\lambda (S).$$

$$(B,A)\in S_{\circ }$$

$$(B,A)\in S_{\diamond }$$

$$(B,A)\in S_{\ast }$$

$$\lambda (R;\lambda (S))=\lambda (R);\lambda (S).$$

$$\begin{array}[]{ll}\mbox{(Sub)}&\forall\rho:I\rightharpoondown X~{}\exists j:S\to X.~{}{(\,}{\rho=\nabla_{IS}j}{\,)}\land{(\,}{jj^{\sharp}=\mbox{\rm id}_{S}}{\,)},\\ \mbox{(DF)}&\alpha\beta\sqcap\gamma\sqsubseteq\alpha(\beta\sqcap\alpha^{\sharp}\gamma).\end{array}$$

$$\lfloor \alpha \rfloor =\alpha {\alpha }^{♯}\sqcap \text{mbox}{\mathrm{id}}_X={\nabla }_{XY}{\alpha }^{♯}\sqcap \text{mbox}{\mathrm{id}}_X.$$

$$\delta ⊑\alpha ⊲\beta \leftrightarrow \delta {\beta }^{♯}⊑\alpha .$$

$$\delta ⊑\alpha ⊳\beta \leftrightarrow {\alpha }^{♯}\delta ⊑\beta .$$

$$\begin{array}[]{rcl}(x,z)\in\alpha\lhd\beta&\leftrightarrow&\forall y\in Y.~{}{(\,}{(x,y)\in\alpha\leftarrow(y,z)\in\beta}{\,)},\\ (x,z)\in\alpha\rhd\beta&\leftrightarrow&\forall y\in Y.~{}{(\,}{(x,y)\in\alpha\to(y,z)\in\beta}{\,)}.\end{array}$$

$$\begin{array}[]{ccll}(\alpha^{@})^{\sharp}\alpha^{@}&=&(({\ni}_{Y}\lhd\alpha^{\sharp})\sqcap({\ni}_{Y}\rhd\alpha^{\sharp}))((\alpha\rhd{\ni}_{Y}^{\sharp})\sqcap(\alpha\lhd{\ni}_{Y}^{\sharp}))\\ &\sqsubseteq&({\ni}_{Y}\rhd\alpha^{\sharp})(\alpha\rhd{\ni}_{Y}^{\sharp})\sqcap({\ni}_{Y}\lhd\alpha^{\sharp})(\alpha\lhd{\ni}_{Y}^{\sharp})\\ &\sqsubseteq&({\ni}_{Y}\rhd{\ni}_{Y}^{\sharp})\sqcap({\ni}_{Y}\lhd{\ni}_{Y}^{\sharp})\\ &\sqsubseteq&\mbox{\rm id}_{\wp(Y)}.\end{array}$$

$$\wp (X)\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$$Set(X,\wp (Y))\ni f\mapsto f{\ni }_Y\in Rel(X,Y)$$

$$Rel(X,Y)\ni \alpha \mapsto {\alpha }^{@}\in Set(X,\wp (Y)).$$

$${\hat{u}}_v=({\nabla }_{\wp (Y)Y}v⊲{\ni }_Y^{♯})\sqcap \text{mbox}{\mathrm{id}}_{\wp (Y)}.$$

$$\begin{array}[]{ccll}\hat{u}_{v}\hat{u}_{v^{\prime}}&=&\hat{u}_{v}\sqcap\hat{u}_{v^{\prime}}\\ &=&(\nabla v\lhd{\ni}_{Y}^{\sharp})\sqcap(\nabla v^{\prime}\lhd{\ni}_{Y}^{\sharp})\sqcap\mbox{\rm id}_{\wp(Y)}&\{~{}\nabla=\nabla_{\wp(Y)Y}~{}\}\\ &=&((\nabla v\sqcap\nabla v^{\prime})\lhd{\ni}_{Y}^{\sharp})\sqcap\mbox{\rm id}_{\wp(Y)}&\{~{}\mbox{\ref{lhd-basic}\,(d)}~{}\}\\ &=&(\nabla vv^{\prime}\lhd{\ni}_{Y}^{\sharp})\sqcap\mbox{\rm id}_{\wp(Y)}&\{~{}\nabla v\sqcap\nabla v^{\prime}=\nabla vv^{\prime}~{}\}\\ &=&\hat{u}_{vv^{\prime}}.\end{array}$$

$$\begin{array}[]{ccll}\hat{u}_{v}{\ni}_{Y}&=&\hat{u}_{v}{\ni}_{Y}\sqcap(\nabla_{\wp(Y)Y}v\lhd{\ni}_{Y}^{\sharp}){\ni}_{Y}\\ &\sqsubseteq&\hat{u}_{v}{\ni}_{Y}\sqcap\nabla_{\wp(Y)Y}v\\ &=&\hat{u}_{v}{\ni}_{Y}v&\{~{}\mbox{\ref{nabla-basic}\,(a)}~{}\}\\ &\sqsubseteq&\hat{u}_{v}{\ni}_{Y},&\{~{}v\sqsubseteq\mbox{\rm id}_{Y}~{}\}\end{array}$$

$$\begin{array}[]{rcll}\nabla_{Z\wp(Y)}\hat{u}_{v}&=&\nabla_{Z\wp(Y)}((\nabla_{\wp(Y)Y}v\lhd\varepsilon_{Y}^{\sharp})\sqcap\mbox{\rm id}_{\wp(Y)})\\ &=&\nabla_{Z\wp(Y)}(\nabla_{\wp(Y)I}(\nabla_{IY}v\lhd\varepsilon_{Y}^{\sharp})\sqcap\mbox{\rm id}_{\wp(Y)})&\{~{}\nabla_{\wp(Y)I}:\mbox{tfn}~{}\}\\ &=&\nabla_{ZI}(\nabla_{IY}v\lhd\varepsilon_{Y}^{\sharp})\\ &=&\nabla_{ZI}\nabla_{IY}v\lhd\varepsilon_{Y}^{\sharp}&\{~{}\nabla_{ZI}:\mbox{tfn}~{}\}\\ &=&\nabla_{ZY}v\lhd\varepsilon_{Y}^{\sharp}.&\{~{}\nabla_{ZI}\nabla_{IY}=\nabla_{ZY}~{}\}\end{array}$$

$$\begin{array}[]{ccll}\hat{u}_{{\rm id}_{Y}}&=&(\nabla_{\wp(Y)Y}\lhd{\ni}_{Y}^{\sharp})\sqcap\mbox{\rm id}_{\wp(Y)}\\ &=&\nabla_{\wp(Y)\wp(Y)}\sqcap\mbox{\rm id}_{\wp(Y)}&\{~{}\nabla\sqsubseteq\nabla\lhd\alpha~{}\}\\ &=&\mbox{\rm id}_{\wp(Y)}.\end{array}$$

$$\begin{array}[]{ccll}\hat{u}_{0_{YY}}&=&(\nabla_{\wp(Y)Y}0_{YY}\lhd{\ni}_{Y}^{\sharp})\sqcap\mbox{\rm id}_{\wp(Y)}\\ &=&(\nabla_{\wp(Y)I}0_{IY}\lhd{\ni}_{Y}^{\sharp})\sqcap\mbox{\rm id}_{\wp(Y)}\\ &=&\nabla_{\wp(Y)I}(0_{IY}\lhd{\ni}_{Y}^{\sharp})\sqcap\mbox{\rm id}_{\wp(Y)}&\{~{}\nabla_{\wp(Y)I}:\mbox{tfn}~{}\}\\ &=&\nabla_{\wp(Y)I}0_{IY}^{@}\sqcap\mbox{\rm id}_{\wp(Y)}&\{~{}0_{IY}\lhd{\ni}_{Y}^{\sharp}=0_{IY}^{@}~{}\}\\ &=&(0_{IY}^{@})^{\sharp}0_{IY}^{@}.&\{~{}0_{IY}^{@}:\mbox{tfn, (DF)}~{}\}\end{array}$$

$$X\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$$\alpha \bullet \beta =\alpha \lambda (\beta )$$

$$\begin{array}[]{rcl}\lambda(\beta\lambda(\gamma))=\lambda(\beta)\lambda(\gamma)&\rightarrow&\alpha\lambda(\beta\lambda(\gamma))=\alpha\lambda(\beta)\lambda(\gamma)\\ &\leftrightarrow&\alpha\bullet(\beta\lambda(\gamma))=(\alpha\lambda(\beta))\bullet\gamma\\ &\leftrightarrow&\alpha\bullet(\beta\bullet\gamma)=(\alpha\bullet\beta)\bullet\gamma\enskip.\end{array}$$

$$\begin{array}[]{rcl}(B,A)\in\beta_{\circ}&\leftrightarrow&A=\bigcup\{C\in\wp(Z)\mid\,\exists b\in B.\,(b,C)\in\beta\}.\end{array}$$

$$\alpha \circ \beta =\alpha {\beta }_{\circ }$$

$$\begin{array}[]{ccll}(\beta\gamma_{\circ})_{\circ}&=&\wp(\beta\gamma_{\circ}{\ni}_{W})\\ &=&\wp(\beta\wp(\gamma{\ni}_{W}){\ni}_{W})\\ &=&\wp(\beta{\ni}_{Z}\gamma{\ni}_{W})&\{~{}\wp(\alpha){\ni}_{Y}={\ni}_{X}\alpha~{}\}\\ &=&\wp(\beta{\ni}_{Z})\wp(\gamma{\ni}_{W})&\{~{}\wp:\mbox{functor}~{}\}\\ &=&\beta_{\circ}\gamma_{\circ}.\\ \end{array}$$

$$\begin{array}[]{ccll}{\lfloor}{\beta}{\rfloor}1_{Y}\beta_{\circ}{\ni}_{Z}&=&{\lfloor}{\beta}{\rfloor}1_{Y}{\ni}_{Y}\beta{\ni}_{Z}\\ &=&{\lfloor}{\beta}{\rfloor}\beta{\ni}_{Z}&\{~{}1_{Y}{\ni}_{Y}=\mbox{\rm id}_{Y}~{}\}\\ &=&\beta{\ni}_{Z},&\{~{}{\lfloor}{\beta}{\rfloor}\beta=\beta~{}\}\end{array}$$

$$0=0_{X\wp (X)},\alpha =\{(a,\varnothing )\},\beta =\{(a,\{a\})\},\gamma =\{(a,\varnothing ),(a,\{a\})\}$$

Full text

1 Introduction

Multirelations are binary relations between sets and powersets of sets; they therefore have the type pattern $X\times\wp(Y)$. Applications include reasoning about games with cooperation [18, 23] and reasoning about computing systems with alternation [4, 12, 19, 20] or dual angelic and demonic nondeterminism [1], including alternating automata (cf. [9]).

This article studies three kinds of composition of multirelations $R\subseteq X\times\wp(Y)$ and $S\subseteq Y\times\wp(Z)$: the Kleisli composition $R\circ S$, which is defined by

[TABLE]

where $S(B)=\{C\in\wp(Z)\mid\,\exists b\in B.\,(b,C)\in S\}$; the Parikh composition $R\diamond S$, which is defined by

[TABLE]

and the Peleg composition $R\ast S$, which is defined by

[TABLE]

where $f(B)$ denotes the image of $B$ under $f$. Although multirelations are just relations of a particular type pattern, these three compositions differ from the standard composition $R;S$ of binary relations, which is defined by $(a,b)\in R;S\leftrightarrow\exists c.(a,c)\in R\wedge(c,b)\in S$. In the rest of the article, the composition of binary relations is referred to as relational composition.

To our knowledge, the Kleisli composition of multirelations has not been studied previously. It is inspired not by applications, but by the eponymous operation on the Kleisli category of the powerset monad [14]. The Parikh composition arises in the multirelational semantics of Parikh’s game logic [18]. Finally, the Peleg composition occurs in the multirelational semantics of Peleg’s concurrent dynamic logic [19, 20]. It has been discussed further by Goldblatt [12] and studied in detail by Furusawa and Struth [9, 10].

Our main contribution is the study of lifting or extension operations on multirelations within an algebraic calculus of (multi)relations, which is introduced in Section 2. These liftings translate Kleisli, Parikh and Peleg’s nonstandard multirelational compositions back to relational compositions on lifted binary relations. The approach is inspired by the well known Kleisli lifting or Kleisli extension on homsets, which translates a nonstandard composition of arrows in a monad back to a standard composition in the associated Kleisli category, for instance a function composition. By this analogy, the lifting of multirelations seems therefore natural for studying algebras of multirelations in the setting of enriched categories, but over $\mathit{Rel}$ instead of $\mathit{Set}$ (Section 3).

More precisely, for multirelations $R\subseteq X\times\wp(Y)$ and $S\subseteq Y\times\wp(Z)$, we wish to lift $S$ to a relation $\lambda(S)\subseteq\wp(Y)\times\wp(Z)$ so that we can translate a Kleisli, Parikh and Peleg composition $R\bullet S$ back to a relational composition $R;\lambda(S)$. Hence we aim at defining $\lambda:Y\times\wp(Z)\to\wp(Y)\times\wp(Z)$ in such a way that the three multirelational compositions satisfy the identity

[TABLE]

It is straightforward to check that the Kleisli lifting $S_{\circ}$, the Parikh lifting $S_{\diamond}$ and the Peleg lifting $S_{\ast}$ of multirelation $S$, which are defined by

[TABLE]

respectively, satisfy the identities $R\circ S=R;S_{\circ}$, $R\diamond S=R;S_{\diamond}$ and $R\ast S=R;S_{\ast}$, as expected. Moreover, we show that associativity of relational composition translates to $\circ$, $\diamond$ or $\ast$ if and only if the associated lifting satisfies

[TABLE]

This is, of course, one of the defining identities of Kleisli extensions. It is known that the compositions $\diamond$ and $\ast$ are not associative for general multirelations. Hence the previous identity for $\lambda$ fails. We are then looking for specific classes of or constraints on multirelations that satisfy this identity and hence have associative Parikh or Peleg composition. In a similar fashion, by following the standard definition of Kleisli extension, we investigate the presence of units of composition. A general aim is therefore the identification of categories of multirelations with respect to Kleisli, Parikh or Peleg composition.

For the class of up-closed multirelations under Parikh composition, Martin and Curtis [16] have already established categorical foundations, including a multirelational lifting. For this class, Parikh composition is associative [18]. We complement their investigation by negative results in the absence of up-closure, presenting counterexamples both to associativity and the existence of units (Section 5).

Kleisli composition, by contrast, is always associative, but we show that units need not exist. Hence multirelations under Kleisli composition need not form categories (Section 4).

Finally, we study Peleg composition in more detail (Section 6, 7). Here it is known that associativity may fail, but that units always exist [9]. Using relation-algebraic reasoning we prove associativity of composition for the subclass of union-closed multirelations, and show, accordingly, that this subclass forms a category (Section 8).

A further contribution is that we express all lifting operations within the language of relation algebra, and can therefore derive the results in this article by equational reasoning. They could therefore be checked by proof assistants such as Coq. We believe that such relation-algebraic proofs are generally much simpler than set-theoretic ones, which, in the presence of Peleg composition, are essentially higher-order. In addition, the introduction of lifting constructions allows us to investigate categories of multirelations in a principled uniform way.

Many of the results in this article have already been presented in a previous conference version [8]. Beyond the presentation of additional proofs and explanations, a significant difference lies in the systematic study of units and therefore of categories of multirelations with respect to Kleisli, Parikh and Peleg composition.

Despite of our category-theoretical motivations, however, we obtain our results in relation-algebraic style. In fact, we mention neither allegories [6] nor Dedekind categories [17], which are categorical frameworks suitable for relations. One main reason is that we use the strict point axiom (PA∗) in our development. In its presence, every Dedekind category (equivalently, every locally complete division allegory) becomes isomorphic to some full subcategory of $\mathit{Rel}$ [7]. Another one is that our approach to composition and lifting does not fit within the standard monadic framework. We cannot associate suitable Kleisli triples $(\wp,\eta,\mu)$ with natural transformations $\eta$ and $\mu$ with all identities and compositions of multirelations in $\mathit{Rel}$.

2 Preliminaries

This section presents the calculus of relations used in this article. Many properties used can be found in standard textbooks; hence we list them without proof. The typed relation algebras described by Freyd and Scedrov [6], Bird and de Moor [3] and Schmidt [21] are most closely related, but use slightly different notation.

We use $I$ to denote any singleton set. A (binary) relation $\alpha$ from set $X$ to set $Y$, written $\alpha:X\rightharpoondown Y$, is a subset $\alpha\subseteq X\times Y$. The empty relation $0_{XY}:X\rightharpoondown Y$ and the universal relation $\nabla_{XY}:X\rightharpoondown Y$ are defined as $0_{XY}=\emptyset$ and $\nabla_{XY}=X\times Y$, respectively. The inclusion, union and intersection of relations $\alpha,\alpha^{\prime}:X\rightharpoondown Y$ are denoted by $\alpha\sqsubseteq\alpha^{\prime}$, $\alpha\sqcup\alpha^{\prime}$ and $\alpha\sqcap\alpha^{\prime}$, respectively. The converse of relation $\alpha:X\rightharpoondown Y$ is denoted by $\alpha{{}^{\sharp}}$. The identity relation $\{(x,x)\mid x\in X\}$ over $X$ is denoted by $\mbox{\rm id}_{X}$. For relation $\alpha:X\rightharpoondown Y$, the partial identity $\{(x,x)\mid\exists y.~{}(x,y)\in\alpha\}$ is denoted by ${\lfloor}{\alpha}{\rfloor}$ and called domain relation of $\alpha$. The standard composition of relations (which includes functions) is denoted by juxtaposition. For example, the composite of relation $\alpha:X\rightharpoondown Y$ followed by $\beta:Y\rightharpoondown Z$ is denoted by $\alpha\beta$, and of course the composition of functions $f:X\to Y$ and $g:Y\to Z$ by $fg$. In addition, the traditional notation $f(x)$ is written $xf$ as a composite of functions $x:I\to X$ and $f:X\to Y$.

Remember that a relation $\alpha$ is univalent iff $\alpha^{\sharp}\alpha\sqsubseteq\mbox{\rm id}_{Y}$, and it is total iff $\mbox{\rm id}_{X}\sqsubseteq\alpha\alpha^{\sharp}$. So, $\alpha$ is a partial function (pfn, for short) iff $\alpha^{\sharp}\alpha\sqsubseteq\mbox{\rm id}_{Y}$, and a (total) function (tfn, for short) iff $\alpha^{\sharp}\alpha\sqsubseteq\mbox{\rm id}_{Y}$ and $\mbox{\rm id}_{X}\sqsubseteq\alpha\alpha^{\sharp}$. Moreover, a singleton set $I$ satisfies $0_{II}\neq\mbox{\rm id}_{I}=\nabla_{II}$ and $\nabla_{XI}\nabla_{IX}=\nabla_{XX}$ for all sets $X$. A tfn $x:I\to X$ is called $I$-point of $X$ and is denoted by $x\,\dot{\in}\,X$. It is easy to see that $xx^{\sharp}=x\nabla_{XI}=\mbox{\rm id}_{I}$. For a relation $\rho:I\rightharpoondown X$ and an $I$-point $x:I\to X$, we write $x\,\dot{\in}\,\rho$ instead of $x\sqsubseteq\rho$.

Some proofs below refer to the axiom of subobjects (Sub) and the Dedekind formula (DF), that is,

[TABLE]

In fact, the subset $S\subseteq X$ and tfn $j:S\to X$ from (Sub) are $S=\{x\mid(*,x)\in\rho\}$ and $j=\{(x,x)\mid(*,x)\in\rho\}$. Note that (DF) is equivalent to

(DF∗) $\alpha\beta\sqcap\gamma\sqsubseteq(\alpha\sqcap\gamma\beta^{\sharp})(\beta\sqcap\alpha^{\sharp}\gamma)$.

Also note that the equation $\nabla_{ZY}(\nabla_{YX}\alpha\sqcap\mbox{\rm id}_{Y})=\nabla_{ZX}\alpha$ follows from (DF). See [21] for more details on basic properties in the calculus of relations.

2.1 Subidentities and domain relations

First, we list some simple properties of subidentities without proof.

Proposition 1**.**

Let $\alpha:X\rightharpoondown Y$ be a relation and $v,v^{\prime}\sqsubseteq\mbox{\rm id}_{Y}$.

1. (a)

$\alpha\sqcap\nabla_{XY}v=\alpha v$. 2. (b)

$v\sqsubseteq v^{\prime}\leftrightarrow\nabla_{YY}v\sqsubseteq\nabla_{YY}v^{\prime}$. 3. (c)

$v=v^{\prime}\leftrightarrow\nabla_{YY}v=\nabla_{YY}v^{\prime}$.

The domain relation ${\lfloor}{\alpha}{\rfloor}\sqsubseteq\mbox{\rm id}_{X}$ of a relation $\alpha:X\rightharpoondown Y$ can be defined explicitly as

[TABLE]

Proposition 2**.**

Let $\alpha,\alpha^{\prime}:X\rightharpoondown Y$ and $\beta:Y\rightharpoondown Z$ be relations.

1. (a)

$\alpha={\lfloor}{\alpha}{\rfloor}\alpha$. 2. (b)

${\lfloor}{\alpha\beta}{\rfloor}\sqsubseteq{\lfloor}{\alpha}{\rfloor}$* and ${\lfloor}{\alpha\beta}{\rfloor}={\lfloor}{\alpha{\lfloor}{\beta}{\rfloor}}{\rfloor}$.* 3. (c)

${\lfloor}{\alpha\sqcap\alpha^{\prime}}{\rfloor}=\alpha\alpha^{\prime\,\sharp}\sqcap\mbox{\rm id}_{X}$. 4. (d)

If $\beta$ is total, then ${\lfloor}{\alpha\beta}{\rfloor}={\lfloor}{\alpha}{\rfloor}$. 5. (e)

If $v\sqsubseteq\mbox{\rm id}_{X}$, then ${\lfloor}{v\alpha}{\rfloor}=v{\lfloor}{\alpha}{\rfloor}$. 6. (f)

$\nabla_{XX}{\lfloor}{\alpha}{\rfloor}=\nabla_{XY}\alpha^{\sharp}$.

The following properties of partial functions are useful below.

Proposition 3**.**

Let $\alpha,\beta:X\rightharpoondown Y$ be relations.

1. (a)

*If $\beta$ is a pfn satisfying $\alpha\sqsubseteq\beta$ and ${\lfloor}{\alpha}{\rfloor}={\lfloor}{\beta}{\rfloor}$, then $\alpha=\beta$. * 2. (b)

*If $\beta$ is a pfn satisfying $\alpha\sqsubseteq\beta$, then $\alpha={\lfloor}{\alpha}{\rfloor}\beta$. * 3. (c)

*If $\beta$ is a pfn and $v\sqsubseteq\mbox{\rm id}_{Y}$, then $\beta v={\lfloor}{\beta v}{\rfloor}\beta$. * 4. (d)

$f=fv$* iff ${\lfloor}{f^{\sharp}}{\rfloor}\sqsubseteq v$ for each pfn $f:X\rightharpoondown Y$ and $v\sqsubseteq\mbox{\rm id}_{Y}$. *

2.2 Residual composition

Notions of residuation are widely used in algebra [11], relation algebra [21] and allegories [6].

Let $\alpha:X\rightharpoondown Y$ and $\beta:Y\rightharpoondown Z$ be relations. The left residual composition $\alpha\lhd\beta$ of $\alpha$ followed by $\beta$ is a relation such that

[TABLE]

The right residual composition $\alpha\rhd\beta$ of $\alpha$ followed by $\beta$ is a relation such that

[TABLE]

The two compositions are related by conversion as $\alpha\lhd\beta=(\beta^{\sharp}\rhd\alpha^{\sharp})^{\sharp}$. Set-theoretically, moreover,

[TABLE]

In the literature, residuals are often defined as adjoints of composition without using converse, that is, $\delta\sqsubseteq\alpha/\gamma\leftrightarrow\delta\gamma\sqsubseteq\alpha\leftrightarrow\gamma\sqsubseteq\delta\backslash\alpha$, so that $\alpha\lhd\beta=\alpha/\beta^{\sharp}$ and $\alpha\rhd\beta=\alpha^{\sharp}\backslash\beta$. We prefer $\lhd$ and $\rhd$ to $/$ and $\backslash$ as they make it easier to recognise sources and targets of relations. Freyd and Scedrov use the same concept and notation for residuals, but call them divisions.

Proposition 4**.**

Let $\alpha,\alpha^{\prime}:X\rightharpoondown Y$, $\beta,\beta^{\prime}:Y\rightharpoondown Z$ and $\gamma:Z\to W$ be relations.

1. (a)

$\alpha^{\prime}\sqsubseteq\alpha\land\beta\sqsubseteq\beta^{\prime}$* implies $\alpha\rhd\beta\sqsubseteq\alpha^{\prime}\rhd\beta^{\prime}$ and $\alpha\sqsubseteq\alpha^{\prime}\land\beta^{\prime}\sqsubseteq\beta$ implies $\alpha\lhd\beta\sqsubseteq\alpha^{\prime}\lhd\beta^{\prime}$. * 2. (b)

$\alpha\beta\rhd\gamma=\alpha\rhd(\beta\rhd\gamma)$* and $\alpha\lhd\beta\gamma=(\alpha\lhd\beta)\lhd\gamma$.* 3. (c)

$(\alpha\sqcup\alpha^{\prime})\rhd\beta=(\alpha\rhd\beta)\sqcap(\alpha^{\prime}\rhd\beta)$* and $\alpha\lhd(\beta\sqcup\beta^{\prime})=(\alpha\lhd\beta)\sqcap(\alpha\lhd\beta^{\prime})$.* 4. (d)

$\alpha\rhd(\beta\sqcap\beta^{\prime})=(\alpha\rhd\beta)\sqcap(\alpha\rhd\beta^{\prime})$* and $(\alpha\sqcap\alpha^{\prime})\lhd\beta=(\alpha\lhd\beta)\sqcap(\alpha^{\prime}\lhd\beta)$.* 5. (e)

$\alpha:\mbox{\rm tfn}$* implies $\alpha\rhd\beta=\alpha\beta$ and $\beta^{\sharp}:\mbox{\rm tfn}$ implies $\alpha\lhd\beta=\alpha\beta$. * 6. (f)

$\alpha(\beta\lhd\gamma)\sqsubseteq\alpha\beta\lhd\gamma$* and $(\alpha\rhd\beta)\gamma\sqsubseteq\alpha\rhd\beta\gamma$.* 7. (g)

$\alpha:\mbox{\rm tfn}$* implies $\alpha(\beta\lhd\gamma)=\alpha\beta\lhd\gamma$ and $\gamma^{\sharp}:\mbox{\rm tfn}$ implies $(\alpha\rhd\beta)\gamma=\alpha\rhd\beta\gamma$. * 8. (h)

$(\alpha\rhd\beta)\lhd\gamma=\alpha\rhd(\beta\lhd\gamma)$.

2.3 Powerset functor $\wp$

The powerset functor $\wp$ and the membership relation ${\ni}_{Y}:\wp(Y)\rightharpoondown Y$ satisfy the following laws.

  (M1) $\ni_{Y}^{@}\sqsubseteq\mbox{\rm id}_{\wp(Y)}$,

  (M2) $\forall\alpha:X\rightharpoondown Y.~{}{(\,}{{\lfloor}{\alpha^{@}}{\rfloor}=\mbox{\rm id}_{X}}{\,)}$,

where $\alpha^{@}=(\alpha\rhd{\ni}_{Y}^{\sharp})\sqcap(\alpha\lhd{\ni}_{Y}^{\sharp})$. Note that

[TABLE]

The conditions (M1) and (M2) for membership relations assert that the relation $\alpha^{@}$ is a tfn. The tfn $\alpha^{@}$ is the unique tfn such that $\alpha^{@}{\ni}_{Y}=\alpha$, namely $(a,B)\in\alpha^{@}$ iff $B=\{b\mid(a,b)\in\alpha\}$. In [3], $\alpha^{@}$ is introduced as the power transpose $\Lambda_{\alpha}$.

The order relation $\Xi_{Y}:\wp(Y)\rightharpoondown\wp(Y)$ is defined by $\Xi_{Y}={\ni}_{Y}\rhd{\ni}_{Y}^{\sharp}$. In fact $\Xi_{Y}=({\ni}_{Y}\lhd{\ni}_{Y}^{\sharp})^{\sharp}$ and $(A,B)\in\Xi_{Y}$ iff $A\subseteq B$. Define a tfn $\wp(\alpha):\wp(X)\to\wp(Y)$ by $\wp(\alpha)=({\ni}_{X}\alpha)^{@}$. Then $\wp(\alpha)$ is the unique tfn such that the following diagram commutes.

[TABLE]

In set theory, $(A,B)\in\wp(\alpha)$ iff $B=\{b\mid\exists a\in A.~{}(a,b)\in\alpha\}$. In other words, $B$ is the image of set $A$ under relation $\alpha$.

A tfn $1_{X}:X\to\wp(X)$ is defined by $1_{X}=\mbox{\rm id}_{X}^{@}$ and called the singleton map on $X$. Set-theoretically, $(x,A)\in 1_{X}$ iff $A=\{x\}$.

The following lemma shows that $\wp$ is indeed a functor from the category $\mathit{Rel}$ of sets and relations into the category $\mathit{Set}$ of sets and (total) functions.

Lemma 1**.**

Let $\alpha:X\rightharpoondown Y$ and $\beta:Y\rightharpoondown Z$ be relations. Then

1. (a)

$\wp(\mbox{\rm id}_{X})=\mbox{\rm id}_{\wp(X)}$, 2. (b)

$\wp(\alpha\beta)=\wp(\alpha)\wp(\beta)$.

Proof.

(a) follows from $\wp(\mbox{\rm id}_{X}){\ni}_{X}={\ni}_{X}\mbox{\rm id}_{X}=\mbox{\rm id}_{\wp(X)}{\ni}_{X}$.

(b) follows from $\wp(\alpha\beta){\ni}_{Z}={\ni}_{X}\alpha\beta=\wp(\alpha){\ni}_{Y}\beta=\wp(\alpha)\wp(\beta){\ni}_{Z}$. ∎

The isomorphism

[TABLE]

is called the power adjunction together with its inverse

[TABLE]

Proposition 5**.**

*Let $f,f^{\prime}:Y\rightharpoondown\wp(Z)$ be pfns. Then ${\lfloor}{f}{\rfloor}={\lfloor}{f^{\prime}}{\rfloor}$ and $f{\ni}_{Z}=f^{\prime}{\ni}_{Z}$ imply $f=f^{\prime}$. *

Proof.

Assume ${\lfloor}{f}{\rfloor}={\lfloor}{f^{\prime}}{\rfloor}$ and $f{\ni}_{Z}=f^{\prime}{\ni}_{Z}$. By the axiom of subobjects (Sub) there exists a tfn $j:S\to Y$ such that ${\lfloor}{f}{\rfloor}=j^{\sharp}j$ and $jj^{\sharp}=\mbox{\rm id}_{S}$. Then both of $jf$ and $jf^{\prime}$ are tfns. (For $\mbox{\rm id}_{S}=jj^{\sharp}jj^{\sharp}=j{\lfloor}{f}{\rfloor}j^{\sharp}\sqsubseteq jff^{\sharp}j^{\sharp}$.) As $jf{\ni}_{Z}=jf^{\prime}{\ni}_{Z}$ is trivial, by the power adjunction we have $jf=jf^{\prime}$ and so $f={\lfloor}{f}{\rfloor}f=j^{\sharp}jf=j^{\sharp}jf^{\prime}={\lfloor}{f^{\prime}}{\rfloor}f^{\prime}=f^{\prime}$. ∎

2.4 Power subidentities

For all subidentities $v\sqsubseteq\mbox{\rm id}_{Y}$ define a subidentity $\hat{u}_{v}\sqsubseteq\mbox{\rm id}_{\wp(Y)}$ by

[TABLE]

The subidentity $\hat{u}_{v}$ is called the power subidentity of $v$. In set theory, $(A,A)\in\hat{u}_{v}$ iff $\forall a\in A.~{}(a,a)\in v$. Power subidentities are used in the context of Peleg composition in Section 6.

Proposition 6**.**

Let $v,\,v^{\prime}\sqsubseteq\mbox{\rm id}_{Y}$.

1. (a)

$\hat{u}_{v}\hat{u}_{v^{\prime}}=\hat{u}_{vv^{\prime}}$. 2. (b)

$v\sqsubseteq v^{\prime}$* implies $\hat{u}_{v}\sqsubseteq\hat{u}_{v^{\prime}}$. * 3. (c)

$\hat{u}_{v}\wp(v)=\hat{u}_{v}$. 4. (d)

$\nabla_{Z\wp(Y)}\hat{u}_{v}=\nabla_{ZY}v\lhd{\ni}_{Y}^{\sharp}$* for all objects $Z$.* 5. (e)

$\hat{u}_{{\rm id}_{Y}}=\mbox{\rm id}_{\wp(Y)}$* and $\hat{u}_{0_{YY}}=(0_{IY}^{@})^{\sharp}0_{IY}^{@}$.*

Proof.

1. (a)

follows from

[TABLE] 2. (b)

is a corollary of (a). 3. (c)

First, ${\lfloor}{\hat{u}_{v}\wp(v)}{\rfloor}={\lfloor}{\hat{u}_{v}}{\rfloor}$ is trivial, since $\wp(v)$ is total. Also, by

[TABLE]

Thus $\hat{u}_{v}{\ni}_{Y}=\hat{u}_{v}{\ni}_{Y}v$. So we have $\hat{u}_{v}\wp(v){\ni}_{Y}=\hat{u}_{v}{\ni}_{Y}v=\hat{u}_{v}{\ni}_{Y}$. Since both of $\hat{u}_{v}\wp(v)$ and $\hat{u}_{v}$ are pfns, $\hat{u}_{v}\wp(v)=\hat{u}_{v}$ holds by 5. 4. (d)

Since $\nabla_{ZY}(\nabla_{YX}\alpha\sqcap\mbox{\rm id}_{Y})=\nabla_{ZX}\alpha$, we have

[TABLE] 5. (e)

The equation (e1) $\hat{u}_{{\rm id}_{Y}}=\mbox{\rm id}_{\wp(Y)}$ follows from

[TABLE]

Also, the equation (e2) $\hat{u}_{0_{YY}}=(0_{IY}^{@})^{\sharp}0_{IY}^{@}$ follows from

[TABLE]

∎

3 Compositions and Liftings

Multirelational compositions can be understood as “nonstandard” compositions in the setting of categories of relations that deviate from the standard relational composition. This section introduces suitable notions of lifting that translate them into the latter.

Consider how to define a multirelational composition for $\alpha:X\rightharpoondown\wp(Y)$ and $\beta:Y\rightharpoondown\wp(Z)$. If one can construct a relation $\lambda(\beta):\wp(Y)\rightharpoondown\wp(Z)$ from $\beta$, then a composite

[TABLE]

is obtained; and relational composition can be used for modelling it. Different notions of lifting can then be used for defining different non-standard notions of multirelational composition. This situation is reminiscent of the definition of Kleisli liftings or Kleisli extensions in Kleisli categories; in particular for the powerset monad in the category $\mathit{Set}$ of sets and functions. In our case, as mentioned in the introduction, we wish to define functions $\lambda$ in such a way that the identity

[TABLE]

holds for composition $\bullet$, which stands for the Kleisli, Parikh or Peleg composition of multirelations. In that case we call $\lambda(\beta)$ a lifting of $\beta$. Liftings and compositions are of course mutually dependent. In the introduction we have argued that we can define functions $\lambda$ from compositions $\bullet$ so that the above identity holds. In the following sections we take the opposite view and define Kleisli, Parikh and Peleg compositions from suitable functions $\lambda$ and relational composition.

On the one hand, the translations from multirelational compositions to relational composition allows us to use our knowledge about the latter to reason about the former. The complexity of reasoning in particular about Peleg’s second-order definition below can thus be encapsulated in the lifting and relational composition can be used in calculations. On the other hand, however, properties of relational composition, including its associativity or the existence of units, need not translate to its multirelational counterparts. Parikh and Peleg composition, in particular, are not in general associative on multirelations [9, 10].

The following identity, which is well known from Kleisli categories as one of the defining identities of Kleisli extensions, yields a generic necessary and sufficient condition for associativity of multirelational compositions and explains this situation.

Lemma 2**.**

The lifting operator $\lambda$ satisfies $\lambda(\alpha\lambda(\beta))=\lambda(\alpha)\lambda(\beta)$ for all multirelations $\alpha$ and $\beta$ if and only if the composition $\bullet$ defined by $\alpha\bullet\beta=\alpha\lambda(\beta)$, for all multirelations $\alpha$ and $\beta$, is associative.

Proof.

[TABLE]

Conversely, suppose that $\bullet$ is associative. Hence $\mbox{\rm id}\bullet(\beta\bullet\gamma)=(\mbox{\rm id}\bullet\beta)\bullet\gamma$ holds for all multirelations $\beta$ and $\gamma$ of suitable type. The previous proof can then be reversed and it follows that $\lambda(\beta\lambda(\gamma))=\lambda(\beta)\lambda(\gamma)$ (order of composition reversed) holds for all multirelations $\beta$ and $\gamma$. ∎

Similarly, the two other defining identities of Kleisli extensions, which relate to the morphisms $\eta$ of a monad, yield necessary and sufficient conditions for the existence of left and right units of multirelational compositions.

Lemma 3**.**

For any set $X$, the relation $\iota_{X}:X\rightharpoondown\wp(X)$ and the lifting operator $\lambda$ satisfy $\lambda(\iota_{X})=\mbox{\rm id}_{\wp(X)}$ if and only if $\iota_{X}$ is a right unit of the composition $\bullet$ defined by $\alpha\bullet\beta=\alpha\lambda(\beta)$.

Proof.

By definition of $\bullet$, $\lambda(\iota_{X})=\mbox{\rm id}_{\wp(X)}$ implies $\delta\bullet\iota_{Y}=\delta$ for each $\delta:W\rightharpoondown\wp(X)$. Conversely, replacing $\delta:W\rightharpoondown\wp(X)$ by $\mbox{\rm id}_{\wp(X)}:\wp(X)\rightharpoondown\wp(X)$ yields $\mbox{\rm id}_{\wp(X)}=\mbox{\rm id}_{\wp(X)}\bullet\iota_{X}=\mbox{\rm id}_{\wp(X)}\lambda(\iota_{X})=\lambda(\iota_{X})$. ∎

The analogous fact for left units, and the remaining defining identity of Kleisli extensions, is entirely trivial: For any set $X$, the relation $\iota_{X}$ is a left unit of $\bullet$ if and only if it satisfies $\iota_{X}\lambda(\alpha)=\alpha$, by definition of $\bullet$. The following property is thus immediate from Lemma 3.

Corollary 1**.**

For any set $X$, the relation $\iota_{X}:X\rightharpoondown\wp(X)$ and the lifting operator $\lambda$ satisfy $\lambda(\iota_{X})=\mbox{\rm id}_{\wp(X)}$ and $\iota_{X}\lambda(\alpha)=\alpha$, for each relation $\alpha:X\rightharpoondown Y$, if and only if $\iota_{X}$ is the identity on $X$ for the composition $\bullet$ defined by $\alpha\bullet\beta=\alpha\lambda(\beta)$.

These facts raise the question whether, beyond a mere analogy, our entire approach could be developed in the setting of a powerset monad, but for $\mathit{Rel}$ instead of $\mathit{Set}$. However, it is easy to check that $\iota$ is not a natural transformation from the identity function in $\mathit{Rel}$ to the powerset functor in $\mathit{Rel}$, at least in the case of Peleg composition. Any deeper evaluations of this failure, as well as more general investigations of suitable monads for multirelations, are left for future work.

The following sections consider the Kleisli, Parikh and Peleg liftings in detail.

4 Kleisli lifting

The Kleisli lifting $\beta_{\circ}:\wp(Y)\rightharpoondown\wp(Z)$ of a relation $\beta:Y\rightharpoondown\wp(Z)$ is defined by $\beta_{\circ}=\wp(\beta{\ni}_{Z})\;.$ By definition, the Kleisli lifting is always a tfn, and it satisfies the property outlined in the introduction:

[TABLE]

This lifting is used to give a relational definition of the Peleg lifting in Section 6.

Moreover, we obtain the Kleisli composition of relations $\alpha:X\rightharpoondown\wp(Y)$ and $\beta:Y\rightharpoondown\wp(Z)$ as the relation

[TABLE]

of type $X\rightharpoondown\wp(Z)$. Its set-theoretic counterpart has been presented in the introduction.

The first two conditions in the following propositions are characteristic identities for Kleisli extensions in Kleisli categories.

Proposition 7**.**

Let $\beta:Y\rightharpoondown\wp(Z)$ and $\gamma:Z\rightharpoondown\wp(W)$ be relations.

1. (a)

$(\beta\gamma_{\circ})_{\circ}=\beta_{\circ}\gamma_{\circ}$. 2. (b)

$(1_{Y})_{\circ}=\mbox{\rm id}_{\wp(Y)}$. 3. (c)

$(0_{YZ}^{@})_{\circ}=0_{\wp(Y)Z}^{@}$. 4. (d)

If $\beta$ is a pfn, then ${\lfloor}{\beta}{\rfloor}1_{Y}\beta_{\circ}=\beta$.

Proof.

1. (a)

follows from

[TABLE] 2. (b)

follows from $(1_{Y})_{\circ}1_{Y}=\wp(1_{Y}{\ni}_{Y})=\wp(\mbox{\rm id}_{Y})=\mbox{\rm id}_{\wp(Y)}$ since $1_{Y}{\ni}_{Y}=\mbox{\rm id}_{Y}$. 3. (c)

follows from $(0_{YZ}^{@})_{\circ}=\wp(0_{YZ}^{@}{\ni}_{Z})=\wp(0_{YZ})=({\ni}_{Y}0_{YZ})^{@}=(0_{\wp(Y)Z})^{@}$. 4. (d)

Since ${\lfloor}{{\lfloor}{\beta}{\rfloor}1_{Y}\beta_{\circ}}{\rfloor}={\lfloor}{{\lfloor}{\beta}{\rfloor}}{\rfloor}={\lfloor}{\beta}{\rfloor}$ and

[TABLE]

${\lfloor}{\beta}{\rfloor}1_{Y}\beta_{\circ}=\beta$ holds by Proposition 5.

∎

Case (a) of the last proposition ensures that Kleisli composition $\alpha\circ\beta$, is indeed associative, and (b) ensures that $1_{X}$ is a right unit of Kleisli composition.

Proposition 8**.**

Kleisli composition of multirelations is associative: $\alpha\circ(\beta\circ\gamma)=(\alpha\circ\beta)\circ\gamma$, and $1_{X}$ is a right unit of Kleisli composition on each $X$.

However it turns out that multirelations with respect to Kleisli composition do not form a category. The following proposition shows that the third defining identity of Kleisli liftings, $\iota_{X}\lambda(\alpha)=\alpha$, need not hold.

Proposition 9**.**

Kleisli composition need not have left units.

Proof.

Let $X=\{a\}$. Then

[TABLE]

are all multirelations over $X$. We obtain the Kleisli liftings

[TABLE]

and the composition table for the Kleisli composition $\circ$ as follows:

[TABLE]

Thus $\beta$ and $\gamma$ are right units by Lemma 3, however the composition table shows that there is no left unit. ∎

5 Parikh lifting

The Parikh lifting $\beta_{\diamond}:\wp(Y)\rightharpoondown\wp(Z)$ of a relation $\beta:Y\rightharpoondown\wp(Z)$ is defined by $\beta_{\diamond}={\ni}_{Y}\rhd\beta$ . The Parikh lifting satisfies, by definition,

[TABLE]

In addition, one can define the Parikh composition of relations $\alpha:X\rightharpoondown\wp(Y)$ and $\beta:Y\rightharpoondown\wp(Z)$ as

[TABLE]

Its set-theoretic counterpart has again been presented in the introduction. This lifting and the associated composition have been studied by Martin and Curtis [16]. However, they have concentrated on up-closed multirelations $\alpha:X\rightharpoondown\wp(Y)$ such that $\alpha\Xi_{Y}=\alpha$, whereas we complement their investigation by the general case where up-closure need not hold. Independently of the work presented here, Berghammer and Guttmann have studied Parikh composition without up-closure, but without explicit liftings [2]. Set-theoretically, a multirelation $\alpha$ is up-closed if $(a,B)\in\alpha$ and $B\subseteq C$ imply $(a,C)\in\alpha$.

First, we present some properties of general multirelations under Parikh composition.

Proposition 10**.**

Let $\beta:Y\rightharpoondown\wp(Z)$ and $\gamma:Z\rightharpoondown\wp(W)$ be relations.

1. (a)

$\beta_{\diamond}\gamma_{\diamond}\sqsubseteq(\beta\gamma_{\diamond})_{\diamond}$. 2. (b)

$\gamma_{\diamond}=\Xi_{Z}\gamma^{\sharp\,@\,\sharp}$*. * 3. (c)

$(\beta\gamma_{\diamond})_{\diamond}\sqsubseteq(\beta\Xi_{Z})_{\diamond}\gamma_{\diamond}$. 4. (d)

$1_{Y}\Xi_{Y}={\ni}_{Y}^{\sharp}$* and $1_{Y}\sqsubseteq{\ni}_{Y}^{\sharp}$.* 5. (e)

${\ni}_{Y}^{\sharp}\beta_{\diamond}=\beta$. 6. (f)

$({\ni}_{Z}^{\sharp})_{\diamond}=\Xi_{Z}$*. *

Proof.

1. (a)

follows from

[TABLE] 2. (b)

follows from

[TABLE] 3. (c)

follows from

[TABLE] 4. (d)

$1_{Y}\Xi_{Y}={\ni}_{Y}^{\sharp}$ follows from

[TABLE]

So, $1_{Y}\sqsubseteq{\ni}_{Y}^{\sharp}$ by $\mbox{\rm id}_{\wp(Y)}\sqsubseteq\Xi_{Y}$. 5. (e)

follows from

[TABLE] 6. (f)

is immediate from the definitions of the Parikh lifting and $\Xi_{Z}$.

∎

It is known that Parikh composition $\alpha\diamond\beta$ need not be associative [22]. The following example confirms that, in fact, the converse of inclusion (a) need not hold.

Example 1** (Tsumagari, [22]).**

Let $X=\{a,b,c\}$, and $\alpha,\beta:X\rightharpoondown\wp(X)$ be multirelations defined by

[TABLE]

Then we obtain Parikh liftings

[TABLE]

of $\alpha$ and $\beta$. Therefore the inequality \beta_{\diamond}\alpha_{\diamond}\mbox{{\ooalign{\hfil\sqsubseteq\hfil\crcr\lower 2.15277pt\hbox{{\small\,{}_{/}}}}}}(\beta\alpha_{\diamond})_{\diamond} holds, since $(\beta\alpha_{\diamond})_{\diamond}=\alpha_{\diamond}$, and

[TABLE]

∎**

In addition, $\lambda(\iota_{X})=\mbox{\rm id}_{\wp(X)}$ fails this time.

Proposition 11**.**

Parikh composition need not have right units.

Proof.

Consider again the multirelations from the proof of Proposition 9. We obtain Parikh liftings

[TABLE]

of these multirelations and the composition table for Parikh composition $\diamond$ as follows:

[TABLE]

The composition table shows that $\beta$ is the left unit and there is no right unit by Lemma 3. ∎

The failure of the right unit law has been noted by Berghammer and Guttmann, too [2]. Parikh composition is, however, associative for up-closed multirelations, and in fact, the inequalities (a) and (c) of Proposition 10 imply this. In addition, (e) and (f) of Proposition 10 imply that the converses of the membership relations serve as the units of Parikh composition in the up-closed case. Equation (b) of Proposition 10 implies that $\alpha\diamond\beta=\alpha\beta^{\sharp\,@\,\sharp}$ if $\alpha$ is up-closed. In other words, up-closed multirelations form categories with respect to Parikh composition. We recover this result of Martin and Curtis within the more general setting of multirelations that need not be up-closed.

6 Peleg lifting

Before providing relational definitions of Peleg lifting and Peleg composition, we introduce some notation and prove a technical property.

For a relation $\alpha:X\rightharpoondown Y$ the expressions $f\sqsubseteq_{p}\alpha$ and $f\sqsubseteq_{c}\alpha$ denote the conditions

[TABLE]

respectively. Some proofs below assume the point axiom (PA) and a variant of the (relational) axiom of choice (AC∗), that is,

[TABLE]

in addition to (Sub) and (DF). Note that (PA) is equivalent to $\mbox{\rm id}_{X}=\bigsqcup_{x\in X}\,x^{\sharp}x$. Also note that (AC∗) implies the (relational) axiom of choice

[TABLE]

Proposition 12**.**

*For all relations $\alpha:X\rightharpoondown Y$, the identity $\alpha=\bigsqcup_{f\sqsubseteq_{c}\alpha}f$ holds. *

Proof.

The inclusion $\bigsqcup_{f\sqsubseteq_{c}\alpha}f\sqsubseteq\alpha$ is clear. It remains to show its converse. Using the point axiom (PA) we have

[TABLE]

Each relation $x^{\sharp}x\alpha y^{\sharp}y$ is a pfn and $x^{\sharp}x\alpha y^{\sharp}y\sqsubseteq x^{\sharp}y\sqcap\alpha$. By the axiom of choice (AC∗), there is a pfn $f:X\rightharpoondown Y$ such that $x^{\sharp}x\alpha y^{\sharp}y\sqsubseteq f\sqsubseteq_{c}\alpha$. Hence we have $x^{\sharp}x\alpha y^{\sharp}y\sqsubseteq\bigsqcup_{f\sqsubseteq_{c}\alpha}f$, which proves the converse inclusion $\alpha\sqsubseteq\bigsqcup_{f\sqsubseteq_{c}\alpha}f$. ∎

Proposition 12 above indicates that $(a,b)\in\alpha$ if and only if there exists a pfn $f\sqsubseteq_{c}\alpha$ such that $(a,b)\in f$.

The following example gives an intuition for the condition $\sqsubseteq_{c}$.

Example 2**.**

Consider the multirelations from Propositions 9 and 11. Then we have pfns $0\sqsubseteq_{c}0$, $\alpha\sqsubseteq_{c}\alpha$, $\beta\sqsubseteq_{c}\beta$, and $\alpha,\beta\sqsubseteq_{c}\gamma$. ∎**

The Peleg lifting $\beta_{*}:\wp(Y)\rightharpoondown\wp(Z)$ of a relation $\beta:Y\rightharpoondown\wp(Z)$ is defined by

[TABLE]

where $f_{\circ}=\wp(f{\ni}_{Z})$ is the Kleisli lifting, as previously. As before, we define the Peleg composition of relations $\alpha:X\rightharpoondown\wp(Y)$ and $\beta:Y\rightharpoondown\wp(Z)$ as

[TABLE]

A set-theoretic definition can be found in the introduction; the Peleg lifting satisfies

[TABLE]

The Peleg lifting can be defined as the composite $\hat{u}_{{\lfloor}{\beta}{\rfloor}}(\sqcup_{f\sqsubseteq_{c}\beta}\;f_{\circ})$ of the subidentity and the join of Kleisli liftings of pfns. In fact, the Peleg lifting of a relation $\beta$ is the join of Peleg liftings of pfns $f\sqsubseteq_{c}\beta$ as shown in the following proposition.

Proposition 13**.**

Let $\beta,\,\beta^{\prime}:Y\rightharpoondown\wp(Z)$ be relations and $v\sqsubseteq\mbox{\rm id}_{Y}$.

1. (a)

If $\beta\sqsubseteq\beta^{\prime}$, then $\beta_{*}\sqsubseteq\beta^{\prime}_{*}$. 2. (b)

If $\beta$ is pfn, then $\beta_{*}=\hat{u}_{{\lfloor}{\beta}{\rfloor}}\beta_{\circ}$. 3. (c)

If $\beta$ is pfn, then so is $\beta_{*}$. 4. (d)

$\beta_{*}=\bigsqcup_{f\sqsubseteq_{c}\beta}f_{*}$. 5. (e)

${\lfloor}{\beta_{*}}{\rfloor}=\hat{u}_{{\lfloor}{\beta}{\rfloor}}$. 6. (f)

$(v\beta)_{*}=\hat{u}_{v}\beta_{*}$.

Proof.

1. (a)

Assume $\beta\sqsubseteq\beta^{\prime}$ and $f\sqsubseteq_{c}\beta$. By the axiom of choice (AC∗) there exists a pfn $f^{\prime}$ such that $f\sqsubseteq f^{\prime}\sqsubseteq_{c}\beta^{\prime}$. Then $f={\lfloor}{f}{\rfloor}f^{\prime}$ by 3 (b) and hence

[TABLE]

which proves the statement. 2. (b)

Let $\beta$ be a pfn and $f\sqsubseteq_{c}\beta$. Then $f=\beta$ is immediate from 3 (a). Hence the statement is obvious by the definition of Peleg lifting. 3. (c)

is a corollary of (b). 4. (d)

follows from

[TABLE] 5. (e)

follows from

[TABLE] 6. (f)

With

[TABLE]

we have

[TABLE]

and

[TABLE]

∎

The following proposition indicates that the singleton maps serve as the units of Peleg composition, which is well known [9], but the algebraic proofs are new.

Proposition 14**.**

Let $\beta:Y\rightharpoondown\wp(Z)$ be a relation and $v\sqsubseteq\mbox{\rm id}_{Y}$.

1. (a)

$1_{Y}\hat{u}_{v}=v1_{Y}$. 2. (b)

$1_{Y}\beta_{*}=\beta$. 3. (c)

$(v1_{Y})_{*}=\hat{u}_{v}$. 4. (d)

$(1_{Y})_{*}=\mbox{\rm id}_{\wp(Y)}$.

Proof.

1. (a)

follows from

[TABLE] 2. (b)

By 5, ${\lfloor}{f}{\rfloor}1_{Y}f_{\circ}=f$ holds since it is clear that ${\lfloor}{{\lfloor}{f}{\rfloor}1_{Y}f_{\circ}}{\rfloor}={\lfloor}{f}{\rfloor}$ and

${\lfloor}{f}{\rfloor}1_{Y}f_{\circ}{\ni}_{Z}={\lfloor}{f}{\rfloor}1_{Y}{\ni}_{Y}f{\ni}_{Z}={\lfloor}{f}{\rfloor}f{\ni}_{Z}=f{\ni}_{Z}$. So, we have

[TABLE] 3. (c)

follows from

[TABLE] 4. (d)

is a corollary of (c).

∎

The following proposition is immediate from (b) and (d) of Proposition 14 and Corollary 1.

Proposition 15**.**

$1_{X}$* is the identity on $X$ for Peleg composition.*

We now reconsider our standard example in the context of the Peleg lifting and Peleg composition as an illustration.

Example 3**.**

Consider the multirelations from the proofs of Propositions 9, 11 and Example 2. Then $\hat{u}_{{\lfloor}{0}{\rfloor}}=\{(\emptyset,\emptyset)\}$ and $\hat{u}_{{\lfloor}{\alpha}{\rfloor}}=\hat{u}_{{\lfloor}{\beta}{\rfloor}}=\hat{u}_{{\lfloor}{\gamma}{\rfloor}}=\{(\emptyset,\emptyset),(\{a\},\{a\})\}$. Thus we obtain the Peleg liftings

[TABLE]

of these multirelations and the Peleg composition table:

[TABLE]

The singleton map $\beta$ is the unit with respect to Peleg composition. ∎**

It is known that Peleg composition need not be associative [9].

Example 4** (Furusawa and Struth, [9]).**

Let $X=\{a,b\}$, $\alpha,\beta:X\rightharpoondown\wp(X)$,

[TABLE]

Then

[TABLE]

Therefore $(\alpha*\alpha)*\beta\neq\alpha*(\alpha*\beta)$.∎**

The question thus arises under which conditions Peleg composition becomes associative. In the rest of this paper, we examine associativity of Peleg composition more closely. Furusawa and Struth have shown that Peleg composition is associative if one of the three multirelations involved is a subidentity [9]. The next section presents a more general constraint. After that we introduce a general class of multirelations in which Peleg composition is associative.

7 Associativity of Peleg Composition for Partial Functions

This section shows that Peleg composition of multirelations is associative whenever one of the three multirelations that participate in an instance of an associativity law is a partial function. All subidentities are, of course, partial functions. The following technical lemmas prepare for this result.

For a subidentity $v\sqsubseteq\mbox{\rm id}_{Y}$, $v\beta$ and $vf$ are restrictions of a relation $\beta:Y\rightharpoondown\wp(Z)$ and a pfn $\beta:Y\rightharpoondown\wp(Z)$ to $v$. The following proposition describes the Peleg lifting of such restrictions.

Proposition 16**.**

Let $\beta:Y\rightharpoondown\wp(Z)$ be a relation, $f:Y\rightharpoondown\wp(Z)$ a pfn, and $v\sqsubseteq\mbox{\rm id}_{Y}$.

1. (a)

$(v\beta)_{*}=(v1_{Y})_{*}\beta_{*}$. 2. (b)

$v\sqsubseteq{\lfloor}{f}{\rfloor}$* implies $(vf)_{*}=\hat{u}_{v}f_{\circ}=\hat{u}_{v}f_{*}$. *

Proof.

1. (a)

follows from

[TABLE] 2. (b)

Assume $v\sqsubseteq{\lfloor}{f}{\rfloor}$. Then

[TABLE]

∎

Proposition 17**.**

Let $f:Y\rightharpoondown\wp(Z)$ and $g:Z\rightharpoondown\wp(W)$ be pfns and $\gamma:Z\rightharpoondown\wp(W)$ a relation.

1. (a)

$f\gamma_{*}=\bigsqcup_{g\sqsubseteq_{c}\gamma}{\lfloor}{f\hat{u}_{{\lfloor}{\gamma}{\rfloor}}}{\rfloor}fg_{\circ}$. 2. (b)

$f_{*}\gamma_{*}=\bigsqcup_{g\sqsubseteq_{c}\gamma}{\lfloor}{f_{*}\hat{u}_{{\lfloor}{\gamma}{\rfloor}}}{\rfloor}f_{\circ}g_{\circ}$*. * 3. (c)

$f_{*}g_{*}={\lfloor}{f_{*}\hat{u}_{{\lfloor}{g}{\rfloor}}}{\rfloor}f_{\circ}g_{\circ}$. 4. (d)

$(fg_{*})_{*}=\hat{u}_{{\lfloor}{f\hat{u}_{{\lfloor}{g}{\rfloor}}}{\rfloor}}f_{\circ}g_{\circ}$.

Proof.

1. (a)

follows from $f\gamma_{*}=\bigsqcup_{g\sqsubseteq_{c}\gamma}f\hat{u}_{{\lfloor}{\gamma}{\rfloor}}g_{\circ}=\bigsqcup_{g\sqsubseteq_{c}\gamma}{\lfloor}{f\hat{u}_{{\lfloor}{\gamma}{\rfloor}}}{\rfloor}fg_{\circ}$ by 3 (c). 2. (b)

follows from

[TABLE] 3. (c)

is a particular case of (b) when $\gamma$ is a pfn. 4. (d)

follows from

[TABLE]

∎

Proposition 18**.**

Let $f:Y\rightharpoondown\wp(Z)$ be a pfn and $v\sqsubseteq\mbox{\rm id}_{Z}$. Then the identity ${\lfloor}{f_{*}\hat{u}_{v}}{\rfloor}=\hat{u}_{{\lfloor}{f\hat{u}_{v}}{\rfloor}}$ holds.

Proof.

Set $\nabla=\nabla_{\wp(Y)\wp(Z)}$ for short.

(1) $\nabla\hat{u}_{v}\wp(f{\ni}_{Z})^{\sharp}=(\nabla\hat{u}_{v}\lhd f^{\sharp})\lhd{\ni}_{Y}^{\sharp}:$

[TABLE]

(2) $\nabla\hat{u}_{v}f^{\sharp}=\nabla f^{\sharp}\sqcap(\nabla\hat{u}_{v}\lhd f^{\sharp}):$

[TABLE]

By (1) and (2),

[TABLE]

holds. This completes the proof. ∎

Associativity of Peleg composition for pfns now follows from the following fact, according to Section 3.

Proposition 19**.**

*If $f:Y\rightharpoondown\wp(Z)$ and $g:Z\rightharpoondown\wp(W)$ are pfns, then $f_{*}g_{*}=(fg_{*})_{*}$. *

Proof.

[TABLE]

∎

Proposition 20**.**

Let $\alpha:X\rightharpoondown\wp(Y)$ be a relation. If $f:Y\rightharpoondown\wp(Z)$ and $g:Z\rightharpoondown\wp(W)$ are pfns, then $(\alpha*f)*g=\alpha*(f*g)$.

In the general case, at least a weak associativity law holds [9]. Once more we give an algebraic proof.

Corollary 2**.**

For relations $\beta:Y\rightharpoondown\wp(Z)$ and $\gamma:Z\rightharpoondown\wp(W)$ the inclusion $\beta_{*}\gamma_{*}\sqsubseteq(\beta\gamma_{*})_{*}$ holds.

Proof.

It follows from

[TABLE]

∎

This establishes the inclusion $(\alpha*\beta)*\gamma\sqsubseteq\alpha*(\beta*\gamma)$.

The condition for associativity may be relaxed slightly from Proposition 19, as the following fact shows.

Proposition 21**.**

For a relation $\beta:Y\rightharpoondown\wp(Z)$ and a pfn $g:Z\rightharpoondown\wp(W)$ the identity $\beta_{*}g_{*}=(\beta g_{*})_{*}$ holds.

Proof.

As $\beta_{*}g_{*}\sqsubseteq(\beta g_{*})_{*}$ by Corollary 2, it remains to show the converse inclusion $(\beta g_{*})_{*}\sqsubseteq\beta_{*}g_{*}$. Since $(\beta g_{*})_{*}=\bigsqcup_{h\sqsubseteq_{c}\beta g_{*}}h_{*}$, it suffices to see that $h_{*}\sqsubseteq\beta_{*}g_{*}$ for each pfn $h\sqsubseteq_{c}\beta g_{*}$. Assume that $h\sqsubseteq_{c}\beta g_{*}$. By the axiom of choice (AC∗) there is a pfn $f:Y\rightharpoondown\wp(Z)$ such that $f\sqsubseteq\beta\sqcap hg_{*}^{\sharp}$ and ${\lfloor}{f}{\rfloor}={\lfloor}{\beta\sqcap hg_{*}^{\sharp}}{\rfloor}$. Then the following holds.

(1) ${\lfloor}{f}{\rfloor}={\lfloor}{h}{\rfloor}:$

[TABLE]

(2) $h\sqsubseteq fg_{*}:$

[TABLE]

(3) $h_{*}\sqsubseteq\beta_{*}g_{*}:$

[TABLE]

This completes the proof. ∎

Thus, the following proposition is obtained by Lemma 2.

Proposition 22**.**

Let $\alpha:X\rightharpoondown\wp(Y)$ and $\beta:Y\rightharpoondown\wp(Z)$ be relations. If $g:Z\rightharpoondown\wp(W)$ is a pfn, then $(\alpha*\beta)*g=\alpha*(\beta*g)$.

8 Associativity of Peleg Composition for Union-Closed Multirelations

Finally we show that Peleg composition is generally associative for a restricted class of union-closed multirelations. This implies that union-closed multirelations under Peleg composition form categories.

The following notion has been suggested by Tsumagari [22].

A relation $\gamma:Z\rightharpoondown\wp(W)$ is union-closed if ${\lfloor}{\rho}{\rfloor}(\rho{\ni}_{W})^{@}\sqsubseteq\gamma$ for all relations $\rho:Z\rightharpoondown\wp(W)$ such that $\rho\sqsubseteq\gamma$. Set-theoretically, $\gamma:Z\rightharpoondown\wp(W)$ is union-closed iff for each $a\in Z$

[TABLE]

For example, every pfn is union-closed, since the identity ${\lfloor}{\rho}{\rfloor}(\rho{\ni}_{W})^{@}=\rho$ holds for all pfns $\rho:Z\rightharpoondown\wp(W)$ by ${\lfloor}{{\lfloor}{\rho}{\rfloor}(\rho{\ni}_{W})^{@}}{\rfloor}={\lfloor}{\rho}{\rfloor}$ and

[TABLE]

Proposition 23**.**

*If a relation $\gamma:Z\rightharpoondown\wp(W)$ is union-closed, then for all relations $\rho:Z\rightharpoondown\wp(W)$ with $\rho\sqsubseteq\gamma$ there exists a pfn $g:Z\rightharpoondown\wp(W)$ such that $g\sqsubseteq_{c}\gamma$ and ${\lfloor}{\rho}{\rfloor}g{\ni}_{W}=\rho{\ni}_{W}$. *

Proof.

As ${\lfloor}{\rho}{\rfloor}(\rho{\ni}_{W})^{@}$ is a pfn, by the axiom of choice (AC∗) there exists a pfn $g$ such that ${\lfloor}{\rho}{\rfloor}(\rho{\ni}_{W})^{@}\sqsubseteq g$ and $g\sqsubseteq_{c}\gamma$. Hence

[TABLE]

∎

For tfns $f:X\to Y$, $h:X\to X$, and relations $\alpha:X\rightharpoondown Y$, $\beta:Y\rightharpoondown Z$, the following interchange law holds:

[TABLE]

This interchange law is needed for the proof of the next proposition; and so is the strict point axiom (PA∗), that is,

[TABLE]

Note that (PA∗) implies (PA).

Proposition 24**.**

Let $\gamma:Z\rightharpoondown\wp(W)$ be a relation, and $f:Y\rightharpoondown\wp(Z)$ and $h:Y\rightharpoondown\wp(W)$ pfns. If $\gamma$ is union-closed, $h\sqsubseteq f\gamma_{*}$ and ${\lfloor}{h}{\rfloor}={\lfloor}{f}{\rfloor}$, then $h_{*}\sqsubseteq f_{*}\gamma_{*}$.

Proof.

For an $I$-point $A:I\to\wp(X)$, set $u_{A}={\lfloor}{(A\ni_{X})^{\sharp}}{\rfloor}$. Let $B:I\to\wp(Y)$ be an $I$-point (tfn) such that $u_{B}\sqsubseteq{\lfloor}{h}{\rfloor}$.

(1) $\forall y\sqsubseteq B{\ni}_{Y}\,\exists g_{y}.~{}{(\,}{g_{y}\sqsubseteq_{c}\gamma}{\,)}\land{(\,}{yh=yfg_{y\,\circ}}{\,)}:$

Assume $y\sqsubseteq B{\ni}_{Y}$. Then $y^{\sharp}y={\lfloor}{y^{\sharp}}{\rfloor}\sqsubseteq{\lfloor}{(B{\ni}_{Y})^{\sharp}}{\rfloor}=u_{B}\sqsubseteq{\lfloor}{h}{\rfloor}={\lfloor}{f}{\rfloor}$. This means that $yh$ and $yf$ are $I$-points (atoms). Thus

[TABLE]

(2) $\forall z\sqsubseteq Bf_{\circ}{\ni}_{Z}.~{}\mu_{z}=z(f{\ni}_{Z})^{\sharp}\sqcap B{\ni}_{Y}\neq 0_{IY}:$

[TABLE]

So, since $z\neq 0_{IZ}$, $\mu_{Z}\neq 0_{IY}$.

(3) $\exists g_{B}.~{}{(\,}{g_{B}\sqsubseteq_{c}\gamma}{\,)}\land{(\,}{\forall z\sqsubseteq Bf_{\circ}{\ni}_{Z}.~{}zg_{B}{\ni}_{W}=\bigsqcup_{y\sqsubseteq\mu_{z}}zg_{y}{\ni}_{W}}{\,)}:$

Set $\rho_{B}=\bigsqcup_{y\sqsubseteq B{\ni}_{Y}}u_{yf}g_{y}$. It is trivial that $\rho_{B}\sqsubseteq\gamma$ and ${\lfloor}{\rho_{B}}{\rfloor}=\bigsqcup_{y\sqsubseteq B{\ni}_{Y}}u_{yf}{\lfloor}{\gamma}{\rfloor}$.

[TABLE]

Hence $z\rho_{B}=\bigsqcup_{y\sqsubseteq\mu_{z}}zg_{y}$ for all $z\sqsubseteq Bf_{\circ}{\ni}_{Z}$. On the other hand, by Prop. 23 we have

[TABLE]

Hence for all $z\sqsubseteq Bf_{\circ}{\ni}_{Z}$

[TABLE]

(4) $Bh_{\circ}=Bf_{\circ}g_{B\,\circ}:$

[TABLE]

Hence $Bh_{\circ}=Bf_{\circ}g_{B\,\circ}$, since both sides of the last identity are tfns.

(5) $h_{*}\sqsubseteq f_{*}\gamma_{*}:$

[TABLE]

∎

Assume that $h\sqsubseteq_{c}\beta\gamma_{*}$ for relations $\beta:Y\rightharpoondown\wp(Z)$ and $\gamma:Z\rightharpoondown\wp(W)$. By (AC∗), there is a pfn $f:Y\rightharpoondown\wp(Z)$ such that $f\sqsubseteq\beta\sqcap h\gamma_{*}^{\sharp}$ and ${\lfloor}{f}{\rfloor}={\lfloor}{\beta\sqcap h\gamma_{*}^{\sharp}}{\rfloor}$. Then, by a calculation that is similar to those for (1) and (2) in the proof of 21, we have ${\lfloor}{h}{\rfloor}={\lfloor}{f}{\rfloor}$ and $h\sqsubseteq f\gamma_{*}$. Thus, by Proposition 24, $h_{*}\sqsubseteq\beta_{*}\gamma_{*}$ whenever $\gamma$ is union-closed. Moreover, this implies that

[TABLE]

Therefore, together with Corollary 2, we have $\beta_{*}\gamma_{*}=(\beta\gamma_{*})_{*}$ if $\gamma$ is union-closed. By Lemma 2, this implies the following proposition.

Proposition 25**.**

Peleg composition $*$ is associative over union-closed multirelations, namely $\alpha*(\beta*\gamma)=(\alpha*\beta)*\gamma$.

Proposition 15 and 25 ensure the following proposition.

Proposition 26**.**

Union-closed multirelations form a category with Peleg composition $*$ and the unit $1_{X}$ on each $X$.

9 Conclusion

We have used relational calculi for studying three kinds of composition of multirelations through suitable liftings, which have been inspired by Kleisli extensions in the context of Kleisli categories. We have introduced relational definitions of the Kleisli and Peleg lifting. Then, we have shown that Kleisli composition is associative but need not have units, and that the singleton map serves as the unit of Peleg composition. We have also shown some basic properties of Parikh composition without restriction to up-closed multirelations, in contrast to Martin and Curtis [16]. It is known that Peleg composition need not be associative [9]. Introducing the notion of union-closed multirelations, we have shown that Peleg composition becomes associative if the third argument is union-closed. It is obvious that the singleton map is union-closed. The set of union-closed multirelations thus forms a category under Peleg composition. The main contribution of this work is thus the translation from complex non-standard reasoning about multirelations to well known tools, namely reasoning with complex higher-order set-theoretic definitions or a non-associative operation of sequential composition can be replaced by standard relational reasoning, and categories of multirelations can be defined and standard category-theoretic tools applied.

Binary relations of type $X\times Y$ have often been studied as nondeterministic functions of type $X\to\wp(Y)$ in the category $\mathit{Set}$ of sets and functions. It is well known that the Kleisli category of the resulting powerset monad is isomorphic to the category of sets and binary relations under standard composition. A similar correspondence exists between the category of up-closed multirelations of type $X\times\wp(Y)$ with respect to Parikh composition and that of certain doubly nondeterministic functions of type $X\to\wp^{2}(Y)$ [5, 13, 15]. The well known isomorphisms between (multi)relations and classes of predicate transformers can be explained elegantly in this setting of monadic computation.

The constructions in this article, however, require greater generality, because relations of type $X\times\wp(Y)$ as arrows in $\mathit{Rel}$, which have motivated the lifting operations in this article, do not fall within the standard monadic setting. This is evidenced by the fact that natural transformations $\eta$, as they arise in Kleisli triples $(\wp,\eta,\mu)$, need not exist for Kleisli and Parikh composition, whereas definitions of $\mu$ in this setting, for instance for Peleg composition, seem far from obvious. A more detailed comparison of lifting constructions in monads and multirelations thus presents a very interesting avenue for further investigation.

Acknowledgment

The authors are grateful to the anonymous referees, as well as those for the previous RAMiCS 2015 version, for their careful reading and helpful comments. They acknowledge support by the Royal Society and JSPS KAKENHI grant number 25330016 and 16K21557 for this research. They are grateful to Koki Nishizawa and Toshinori Takai for enlightening discussions. The fourth author would like to thank Ichiro Hasuo and members of his group at the University of Tokyo for their generous support.