propositionApxtheoremApx propositionApx lemmaApxtheoremApx lemmaApx
definitionApxtheoremApx definitionApx exampleApxtheoremApx exampleApx

# Towards Trace Metrics
via Functor Lifting††thanks: This is an extended version of [BBKK15]. It
consists of the material of the original paper and an appendix containing the
proofs of the presented results.

Paolo Baldan  Dipartimento di Matematica, Università di Padova, Italy
<EMAIL_ADDRESS>Filippo Bonchi  CNRS, ENS Lyon, Université de Lyon,
France
<EMAIL_ADDRESS>Henning Kerstan  Universität Duisburg-Essen,
Germany
<EMAIL_ADDRESS><EMAIL_ADDRESS>Barbara König
Universität Duisburg-Essen, Germany
<EMAIL_ADDRESS><EMAIL_ADDRESS>
###### Abstract.

We investigate the possibility of deriving metric trace semantics in a
coalgebraic framework. First, we generalize a technique for systematically
lifting functors from the category $\mathbf{Set}$ of sets to the category
$\mathbf{PMet}$ of pseudometric spaces, by identifying conditions under which
also natural transformations, monads and distributive laws can be lifted. By
exploiting some recent work on an abstract determinization, these results
enable the derivation of trace metrics starting from coalgebras in
$\mathbf{Set}$. More precisely, for a coalgebra on $\mathbf{Set}$ we
determinize it, thus obtaining a coalgebra in the Eilenberg-Moore category of
a monad. When the monad can be lifted to $\mathbf{PMet}$, we can equip the
final coalgebra with a behavioral distance. The trace distance between two
states of the original coalgebra is the distance between their images in the
determinized coalgebra through the unit of the monad. We show how our
framework applies to nondeterministic automata and probabilistic automata.

###### Key words and phrases:

trace metric, monad lifting, pseudometric, coalgebra

###### 1991 Mathematics Subject Classification:

F.3.1 Specifying and Verifying and Reasoning about Programs, D.2.4
Software/Program Verification

##  1\. Introduction

When considering the behavior of state-based system models embodying
quantitative information, such as probabilities, time or cost, the interest
normally shifts from behavioral equivalences to behavioral distances. In fact,
in a quantitative setting, it is often quite unnatural to ask that two systems
exhibit exactly the same behavior, while it can be more reasonable to require
that the distance between their behaviors is sufficiently small (see, e.g.,
[GJS90, DGJP04, vBW05, BBLM15, dAFS04, dAFS09, FLT11]).

Coalgebras [Rut00] are a well-established abstract framework where a canonical
notion of behavioral equivalence can be uniformly derived. The behavior of a
system is represented as a coalgebra, namely a map of the form $X\to HX$,
where $X$ is a state space and $H$ is a functor that describes the type of
computation performed. For instance nondeterministic automata can be seen as
coalgebras $X\to 2\times\mathcal{P}(X)^{A}$: for any state we specify whether
it is final or not, and the set of successors for any given input in $A$.
Under suitable conditions a final coalgebra exists which can be seen as
minimized version of the system, so that two states are deemed equivalent when
they correspond to the same state in the final coalgebra.

In a recent paper [BBKK14] we faced the problem of devising a framework where,
given a coalgebra for an endofunctor $H$ on $\mathbf{Set}$, one can
systematically derive pseudometrics which measure the behavioral distance of
states. A first crucial step is the lifting of $H$ to a functor $\overline{H}$
on $\mathbf{PMet}$, the category of pseudometric spaces. In particular, we
presented two different approaches which can be viewed as generalizations of
the Kantorovich and Wasserstein pseudometrics for probability measures. One
can prove that the final coalgebra in $\mathbf{Set}$ can be endowed with a
metric, arising as a solution of a fixpoint equation, turning it into the
final coalgebra for the lifting $\overline{H}$. Since any coalgebra $X\to HX$
can be seen as a coalgebra in $\mathbf{PMet}$ by endowing $X$ with the
discrete metric, the unique mapping into the final coalgebra provides a
behavioral distance on $X$.

The canonical notion of equivalence for coalgebras, in a sense, fully captures
the behavior of the system as expressed by the functor $H$. As such, it
naturally corresponds to bisimulation equivalences already defined for various
concrete formalisms. Sometimes one is interested in coarser equivalences,
ignoring some aspects of a computation, a notable example being trace
equivalence where the computational effect which is ignored is branching.

In this paper, relying on recent work on an abstract determinization
construction for coalgebras in [SBBR13, JSS12, JSS15], we extend the above
framework in order to systematically derive trace metrics. The mentioned work
starts from the observation that the distinction between the behavior to be
observed and the computational effects that are intended to be hidden from the
observer, is sometimes formally captured by splitting the functor $H$
characterizing system computations in two components, a functor $F$ for the
observable behavior and a monad $T$ describing the computational effects,
e.g., lifting $1+-$, the powerset functor $\mathcal{P}$ or the distribution
functor $\mathcal{D}$ provides partial, nondeterministic or probabilistic
computations, respectively. For instance, the functor for nondeterministic
automata $2\times\mathcal{P}(X)^{A}$ can be seen as the composition of the
functor $FX=2\times X^{A}$, describing the transitions, with the powerset
monad $T=\mathcal{P}$, capturing nondeterminism. Trace semantics can be
derived by viewing a coalgebra $X\to 2\times\mathcal{P}(X)^{A}$ as a coalgebra
$\mathcal{P}(X)\to 2\times\mathcal{P}(X)^{A}$, via a determinization
construction. Similarly probabilistic automata can be seen as coalgebras of
the form $X\to[0,1]\times\mathcal{D}(X)^{A}$, yielding coalgebras
$\mathcal{D}(X)\to[0,1]\times\mathcal{D}(X)^{A}$ via determinization.

On this basis, [JSS15] develops a framework for deriving behavioral
equivalences which only considers the visible behavior, ignoring the
computational effects. The core idea consists in “incorporating” the effect of
the monad also in the set of states $X$, which thus becomes $TX$, by means of
a construction that can be seen as an abstract form of determinization. For
functors of the shape $FT$, this can be done by lifting $F$ to a functor
$\widehat{F}$ in $\mathcal{EM}(T)$, the Eilenberg-Moore category of $T$, using
a distributive law between $F$ and $T$. In fact, the final $F$-coalgebra lifts
to the final $\widehat{F}$-coalgebra in $\mathcal{EM}(T)$. The technique
works, at the price of some complications, also for functors of the shape $TF$
[JSS15].

Here, we exploit the results in [JSS15] for systematically deriving metric
trace semantics for $\mathbf{Set}$-based coalgebras. The situation is
summarized in the diagram at the end of Subsection 5.1. As a first step,
building on our technique for lifting functors from the category
$\mathbf{Set}$ of sets to the category $\mathbf{PMet}$ of pseudometric spaces,
we identify conditions under which also natural transformations, monads and
distributive laws can be lifted. In this way we obtain an adjunction between
$\mathbf{PMet}$ and $\mathcal{EM}(\overline{T})$, where $\overline{T}$ is the
lifted monad. Via the lifted distributive law we can transfer a functor
$\overline{F}\colon\mathbf{PMet}\to\mathbf{PMet}$ to an endofunctor
$\widehat{\overline{F}}$ on $\mathcal{EM}(\overline{T})$. By using the trivial
discrete distance, coalgebras of the form $TX\to FTX$ can now live in
$\mathcal{EM}(\overline{T})$ and can be equipped with a trace distance via a
map into the final coalgebra. This final coalgebra is again obtained by
lifting the final $\overline{F}$-coalgebra, i.e. a coalgebra equipped with a
behavioral distance, to $\mathcal{EM}(\overline{T})$.

The trace distance between two states of the original coalgebra can then be
defined as the distance between their images in the determinized coalgebra
through the unit of the monad. We illustrate our framework by thoroughly
discussing two running examples, namely nondeterministic automata and
probabilistic automata. We show that it allows us to recover known or
meaningful trace distances such as the standard ultrametric on word languages
for nondeterministic automata or the total variation distance on distributions
for probabilistic automata.

The paper is structured as follows. In Section 2 we will introduce our
notation and quickly recall the basics of our lifting framework from [BBKK14].
Then, in Section 3, we tackle the question of compositionality, i.e. we
investigate whether based on liftings of two functors we can obtain a lifting
of the composed functor. The lifting of natural transformations and monads is
treated in Section 4. Equipped with these tools, we show as main result in
Section 5 how to obtain trace pseudometrics in the Eilenberg-Moore category of
a lifted monad. We conclude our paper with a discussion on related and future
work (Section 6). Proofs can be found in Appendix P.

##  2\. Preliminaries

In this section we recap some basic notions and fix the corresponding
notation. We also briefly recall the results in [BBKK14] which will be
exploited in the paper.

We assume that the reader is familiar with the basic notions of category
theory, especially with the definitions of functor, product, coproduct and
weak pullbacks.

For a function $f\colon X\to Y$ and sets $A\subseteq X$, $B\subseteq Y$ we
write $f[A]:=\left\\{f(a)\mid a\in A\right\\}$ for the _image_ of $A$ and
$f^{-1}[B]=\left\\{a\in A\mid f(x)\in B\right\\}$ for the _preimage_ of $B$.
Finally, if $Y\subseteq[0,\infty]$ and $f,g\colon X\to Y$ are functions we
write $f\leq g$ if $\forall x\in X:f(x)\leq g(x)$.

A _probability distribution_ on a given set $X$ is a function $P\colon
X\to[0,1]$ satisfying $\sum_{x\in X}P(x)=1$. For any set $B\subseteq X$ we
define $P(B)=\sum_{x\in B}P(x)$. The _support_ of $P$ is the set
$\mathrm{supp}(P):=\left\\{x\in X\mid P(x)>0\right\\}$.

Given a natural number $n\in\mathbb{N}$ and a family $(X_{i})_{i=1}^{n}$ of
sets $X_{i}$ we denote the projections of the (cartesian) product of the
$X_{i}$ by $\pi_{i}\colon\prod_{i=1}^{n}X_{i}\to X_{i}$. For a source
$(f_{i}\colon X\to X_{i})_{i=1}^{n}$ we denote the unique mediating arrow to
the product by $\langle f_{1},\dots,f_{n}\rangle\colon
X\to\prod_{i=1}^{n}X_{i}$. Similarly, given a family of arrows $(f_{i}\colon
X_{i}\to Y_{i})_{i=1}^{n}$, we write $f_{1}\times\dots\times f_{n}=\langle
f_{1}\circ\pi_{1},\dots,f_{n}\circ\pi_{n}\rangle\colon\prod_{i=1}^{n}X_{i}\to\prod_{i=1}^{n}Y_{i}$.

For $\top\in(0,\infty]$ and a set $X$ we call any function $d\colon
X^{2}\to[0,\top]$ a ($\top$-)_distance_ on $X$ (for our examples we will use
$\top=1$ or $\top=\infty$). Whenever $d$ satisfies, for all $x,y,z\in X$,
$d(x,x)=0$ (reflexivity), $d(x,y)=d(y,x)$ (symmetry) and $d(x,y)\leq
d(x,z)+d(z,y)$ (triangle inequality) we call it a _pseudometric_ and if it
additionally satisfies $d(x,y)=0\implies x=y$ we call it a _metric_. Given
such a function $d$ on a set $X$, we say that $(X,d)$ is a pseudometric/metric
space. By $d_{e}\colon{[0,\top]}^{2}\to{[0,\top]}$ we denote the ordinary
Euclidean distance on ${[0,\top]}$, i.e., $d_{e}(x,y)=|x-y|$ for
$x,y\in{[0,\top]}\setminus\\{\infty\\}$, and – where appropriate –
$d_{e}(x,\infty)=\infty$ if $x\neq\infty$ and $d_{e}(\infty,\infty)=0$.
Addition is defined in the usual way, in particular $x+\infty=\infty$ for
$x\in[0,\infty]$. We call a function $f\colon X\to Y$ between pseudometric
spaces $(X,d_{X})$ and $(Y,d_{Y})$ _nonexpansive_ and write
$f\colon(X,d_{X})\raisebox{-1.5pt}{$\,\mathop{\overset{1}{\to}}\,$}(Y,d_{Y})$
if $d_{Y}\circ(f\times f)\leq d_{X}$. If equality holds we call $f$ an
_isometry_.

By choosing a fixed maximal element $\top$ in our definition of distances, we
ensure that the set of pseudometrics over a fixed set with pointwise order is
a complete lattice (since ${[0,\top]}$ is) and we obtain a complete and
cocomplete category of pseudometric spaces and nonexpansive functions, which
we denote by $\mathbf{PMet}$. Given a functor $F$ on $\mathbf{Set}$, we aim at
constructing a functor $\overline{F}$ on $\mathbf{PMet}$ which is a lifting of
$F$ in the following sense.

######  Definition 2.1 (Lifting).

Let $U\colon\mathbf{PMet}\to\mathbf{Set}$ be the forgetful functor which maps
every pseudometric space to its underlying set. A functor
$\overline{F}\colon\mathbf{PMet}\to\mathbf{PMet}$ is called a _lifting_ of a
functor $F\colon\mathbf{Set}\to\mathbf{Set}$ if it satisfies
$U\overline{F}=FU$.

Similarly to predicate lifting of coalgebraic modal logic [Sch08], lifting to
$\mathbf{PMet}$ can be conveniently defined once a suitable (evaluation)
function from $F[0,\top]$ to $[0,\top]$ is fixed.

######  Definition 2.2 (Evaluation Function & Evaluation Functor).

Let $F$ be an endofunctor on $\mathbf{Set}$. An _evaluation function_ for $F$
is a function $ev_{F}\colon F[0,\top]\to[0,\top]$. Given such a function, we
define the _evaluation functor_ to be the endofunctor $\widetilde{F}$ on
$\mathbf{Set}/[0,\top]$, the slice category111The slice category
$\mathbf{Set}/[0,\top]$ has as objects all functions $g\colon X\to[0,\top]$
where $X$ is an arbitrary set. Given $g$ as before and $h\colon Y\to[0,\top]$,
an arrow from $g$ to $h$ is a function $f\colon X\to Y$ satisfying $h\circ
f=g$. over $[0,\top]$, via $\widetilde{F}(g)=ev_{F}\circ Fg$ for all
$g\in\mathbf{Set}/[0,\top]$. On arrows $\widetilde{F}$ is defined as $F$.

A first lifting technique leads to what we called the Kantorovich
pseudometric, which is the smallest possible pseudometric $d^{F}$ on $FX$ such
that, for all nonexpansive functions
$f\colon(X,d)\raisebox{-1.5pt}{$\,\mathop{\overset{1}{\to}}\,$}({[0,\top]},d_{e})$,
also
$\widetilde{F}f\colon(FX,d^{F})\raisebox{-1.5pt}{$\,\mathop{\overset{1}{\to}}\,$}({[0,\top]},d_{e})$
is again nonexpansive.

######  Definition 2.3 (Kantorovich Pseudometric & Kantorovich Lifting).

Let $F\colon\mathbf{Set}\to\mathbf{Set}$ be a functor with an evaluation
function $ev_{F}$. For every pseudometric space $(X,d)$ the _Kantorovich
pseudometric_ on $FX$ is the function $d^{\,\uparrow{F}}\colon FX\times
FX\to{[0,\top]}$, where for all $t_{1},t_{2}\in FX$:

$\displaystyle
d^{\,\uparrow{F}}(t_{1},t_{2}):=\sup\left\\{d_{e}(\widetilde{F}f(t_{1}),\widetilde{F}f(t_{2}))\mid
f\colon(X,d)\raisebox{-1.5pt}{$\,\mathop{\overset{1}{\to}}\,$}({[0,\top]},d_{e})\right\\}\,.$

The _Kantorovich lifting_ of the functor $F$ is the functor
$\overline{F}\colon\mathbf{PMet}\to\mathbf{PMet}$ defined as
$\overline{F}(X,d)=(FX,d^{\,\uparrow{F}})$ and $\overline{F}f=Ff$.

This definition is sound i.e. $d^{\,\uparrow{F}}$ is guaranteed to be a
pseudometric so that we indeed obtain a lifting of the functor. A dual way for
obtaining a pseudometric on $FX$ relies on ideas from probability and
transportation theory. It is based on the notion of couplings, which can be
understood as a generalization of joint probability measures.

######  Definition 2.4 (Coupling).

Let $F\colon\mathbf{Set}\to\mathbf{Set}$ be a functor and $n\in\mathbb{N}$.
Given a set $X$ and $t_{i}\in FX$ for $1\leq i\leq n$ we call an element $t\in
F(X^{n})$ such that $F\pi_{i}(t)=t_{i}$ a _coupling_ of the $t_{i}$ (with
respect to $F$). We write $\Gamma_{F}(t_{1},t_{2},\dots,t_{n})$ for the set of
all these couplings.

Based on these couplings we are now able to define an alternative distance on
$FX$.

######  Definition 2.5 (Wasserstein Distance & Wasserstein Lifting).

Let $F\colon\mathbf{Set}\to\mathbf{Set}$ be a functor with evaluation function
$ev_{F}$. For every pseudometric space $(X,d)$ the _Wasserstein distance_ on
$FX$ is the function $d^{\,\downarrow{F}}\colon FX\times FX\to{[0,\top]}$
given by, for all $t_{1},t_{2}\in FX$,

$\displaystyle
d^{\,\downarrow{F}}(t_{1},t_{2}):=\inf\left\\{\widetilde{F}d(t)\mid
t\in\Gamma_{F}(t_{1},t_{2})\right\\}\,.$

If $d^{\,\downarrow{F}}$ is a pseudometric for all pseudometric spaces
$(X,d)$, we define the _Wasserstein lifting_ of $F$ to be the functor
$\overline{F}\colon\mathbf{PMet}\to\mathbf{PMet}$,
$\overline{F}(X,d)=(FX,d^{\,\downarrow{F}})$, $\overline{F}f=Ff$.

The names Kantorovich and Wasserstein used for the liftings derive from
transportation theory [Vil09]. Indeed we obtain a transport problem if we
instantiate $F$ with the distribution functor $\mathcal{D}$ (see also 2.9
below). In order to measure the distance between two probability distributions
$s,t\colon X\to[0,1]$ it is useful to think of the following analogy: assume
that $X$ is a collection of cities (with distance function $d$ between them)
and $s,t$ represent supply and demand (in units of mass). The distance between
$s,t$ can be measured in two ways: the first is to set up an optimal
transportation plan with minimal costs (also called coupling) to transport
goods from cities with excess supply to cities with excess demand. The cost of
transport is determined by the product of mass and distance. In this way we
obtain the Wasserstein distance. A different view is to imagine a logistics
firm that is commissioned to handle the transport. It sets prices for each
city and buys and sells for this price at every location. However, it has to
ensure that the price function (here, $f$) is nonexpansive, i.e., the
difference of prices between two cities is smaller than the distance of the
cities, otherwise it will not be worthwhile to outsource this task. This firm
will attempt to maximize its profit, which can be considered as the
Kantorovich distance of $s,t$. The Kantorovich-Rubinstein duality informs us
that these two views lead to the exactly same result

In 2.5 we are not guaranteed, in general, that $d^{\,\downarrow{F}}$ is a
pseudometric. This is the case if we require $F$ to preserve weak-pullbacks
and impose the following restrictions on the evaluation function.

######  Definition 2.6 (Well-Behaved).

Let $F$ be a functor with an evaluation function $ev_{F}$. We call $ev_{F}$
_well-behaved_ if it satisfies the following conditions:

  1. W1.

$\widetilde{F}$ is monotone, i.e., for $f,g\colon X\to[0,\top]$ with $f\leq
g$, we have $\widetilde{F}f\leq\widetilde{F}g$.

  2. W2.

For each $t\in F([0,\top]^{2})$ it holds that
$d_{e}(ev_{F}(t_{1}),ev_{F}(t_{2}))\leq\widetilde{F}d_{e}(t)$ for
$t_{i}:=F\pi_{i}(t)$.

  3. W3.

$ev_{F}^{-1}[\left\\{0\right\\}]=Fi[F\\{0\\}]$ where
$i\colon\left\\{0\right\\}\hookrightarrow[0,\top]$ is the inclusion map.

While condition W1 is quite natural, for W2 and W3 some explanations are in
order. Condition W2 ensures that
$\widetilde{F}\mathrm{id}_{[0,\top]}=ev_{F}\colon F{[0,\top]}\to{[0,\top]}$ is
nonexpansive once $d_{e}$ is lifted to $F{[0,\top]}$ (recall that for the
Kantorovich lifting we require $\widetilde{F}f$ to be nonexpansive for any
nonexpansive $f$). Condition W3 requires that exactly the elements of
$F\\{0\\}$ are mapped to $0$ via $ev_{F}$. This is necessary for reflexivity
of the Wasserstein pseudometric. Indeed, with this definition at hand we were
able to prove the desired result.

######  Proposition 2.7 ([BBKK14]).

If $F$ preserves weak pullbacks and $ev_{F}$ is well-behaved, then
$d^{\,\downarrow{F}}$ is a pseudometric for any pseudometric space $(X,d)$.

From now on, whenever we use the Wasserstein lifting $d^{\,\downarrow{F}}$, we
implicitly assume to be in the hypotheses of 2.7. It can be shown that, in
general, $d^{\,\uparrow{F}}\leq d^{\,\downarrow{F}}$. Whenever equality holds
we say that the functor and the evaluation function satisfy the _Kantorovich-
Rubinstein duality_. This is helpful in many situations (e.g., in [vBW06] it
allowed to reuse an efficient linear programming algorithm to compute
behavioral distance) but it is usually difficult to obtain.

We now recall two examples which will play an important role in this paper.
First, we consider the following bounded variant of the powerset functor.

######  Example 2.8 (Finite Powerset).

The finite powerset functor $\mathcal{P}_{\\!f\\!i\\!n}$ assigns to each set
$X$ the set $\mathcal{P}_{\\!f\\!i\\!n}X=\left\\{S\subseteq
X\mid|S|<\infty\right\\}$ and to each function $f\colon X\to Y$ the function
$\mathcal{P}_{\\!f\\!i\\!n}f\colon\mathcal{P}_{\\!f\\!i\\!n}X\to\mathcal{P}_{\\!f\\!i\\!n}Y$,
$\mathcal{P}_{\\!f\\!i\\!n}f(S):=f[S]$. This functor preserves weak pullbacks
and the evaluation function
$\max\colon\mathcal{P}_{\\!f\\!i\\!n}([0,\infty])\to[0,\infty]$ with
$\max\emptyset=0$ is well-behaved. The Kantorovich-Rubinstein duality holds
and the resulting distance is the Hausdorff pseudometric which, for any
pseudometric space $(X,d)$ and any
$X_{1},X_{2}\in\mathcal{P}_{\\!f\\!i\\!n}X$, is defined as

$\displaystyle d_{H}(X_{1},X_{2})=\max\left\\{\max_{x_{1}\in
X_{1}}\min_{x_{2}\in X_{2}}d(x_{1},x_{2}),\max_{x_{2}\in X_{2}}\min_{x_{1}\in
X_{1}}d(x_{1},x_{2})\right\\}\,.$

Our second example is the following finite variant of the distribution
functor.

######  Example 2.9 (Finitely Supported Distributions).

The probability distribution functor $\mathcal{D}$ assigns to each set $X$ the
set $\mathcal{D}X=\left\\{P\colon X\to[0,1]\ \middle|\
|\mathrm{supp}(P)|<\infty,P(X)=1\right\\}$ and to each function $f\colon X\to
Y$ the function $\mathcal{D}f\colon\mathcal{D}X\to\mathcal{D}Y$,
$\mathcal{D}f(P)(y)=\sum_{x\in
f^{-1}[\left\\{y\right\\}]}P(x)=P(f^{-1}[\left\\{y\right\\}])$. $\mathcal{D}$
preserves weak pullbacks and the evaluation function
$ev_{\mathcal{D}}\colon\mathcal{D}[0,1]\to[0,1]$,
$ev_{\mathcal{D}}(P)=\sum_{r\in[0,1]}r\cdot P(r)$ is well-behaved. For any
pseudometric space $(X,d)$ we obtain the Wasserstein pseudometric which, for
any $P_{1},P_{2}\in\mathcal{D}X$, is defined as

$\displaystyle
d^{\,\downarrow{\mathcal{D}}}(P_{1},P_{2})=\min\left\\{\sum_{x_{1},x_{2}\in
X}d(x_{1},x_{2})\cdot P(x_{1},x_{2})\ \middle|\
P\in\Gamma_{\mathcal{D}}(P_{1},P_{2})\right\\}\,.$

The Kantorovich-Rubinstein duality [Vil09] holds from classical results in
transportation theory.

While these two functors can be nicely lifted using the theory developed so
far, there are other functors that require a more general treatment. For
instance, consider the endofunctor $F=B\times\\_$ (left product with $B$) for
some fixed $B$. Notice that for $t_{1},t_{2}\in FX=B\times X$ with
$t_{i}=(b_{i},x_{i})$ a coupling exists iff $b_{1}=b_{2}$. As a consequence,
when $b_{1}\neq b_{2}$, irrespectively of the evaluation function we choose
and of the distance between $x_{1}$ and $x_{2}$ in $(X,d)$, the lifted
Wasserstein pseudometric will always result in
$d^{\,\downarrow{F}}(t_{1},t_{2})=\top$. This can be counterintuitive, e.g.,
taking $B=[0,1]$, $X\not=\emptyset$ and $t_{1}=(0,x)$ and
$t_{2}=(\varepsilon,x)$ for a small $\varepsilon>0$ and an $x\in X$. The
reason is that we think of $B=[0,1]$ as endowed with a non-discrete
pseudometric, like e.g. the Euclidean metric $d_{e}$, plugged into the product
after the lifting. This intuition can be indeed formalized by considering the
lifting of the product seen as a functor from $\mathbf{Set}\times\mathbf{Set}$
into $\mathbf{Set}$. More generally, it can be seen that the definitions and
results introduced so far for endofunctors in $\mathbf{Set}$ straightforwardly
extend to multifunctors on $\mathbf{Set}$, namely functors
$F\colon\mathbf{Set}^{n}\to\mathbf{Set}$ on the product category
$\mathbf{Set}^{n}$ for a natural number $n\in\mathbb{N}$. For ease of
presentation we will not spell out the details here (they are spelled out in
[BBKK14]), but just provide an important example of a bifunctor (i.e. $n=2$).

######  Example 2.10 (Product Bifunctor).

The weak pullback preserving product bifunctor
$F\colon\mathbf{Set}^{2}\to\mathbf{Set}$ maps two sets $X_{1},X_{2}$ to
$F(X_{1},X_{2})=X_{1}\times X_{2}$ and two functions $f_{i}\colon X_{i}\to
Y_{i}$ to the function $F(f_{1},f_{2})=f_{1}\times f_{2}$. In this paper we
will use the well-behaved evaluation functions $ev_{F}\colon[0,1]^{2}\to[0,1]$
presented in the table below. Therein we also list the pseudometric
$(d_{1},d_{2})^{F}\colon X_{1}\times X_{2}\to[0,\top]$ we obtain for
pseudometric spaces $(X_{1},d_{1})$, $(X_{2},d_{2})$.

Parameters | $ev_{F}(r_{1},r_{2})$ | $(d_{1},d_{2})^{F}((x_{1},x_{2}),(y_{1},y_{2}))$
---|---|---
$c_{1},c_{2}\in(0,1]$ | $\max\left\\{c_{1}r_{1},c_{2}r_{2}\right\\}$ | $\max\left\\{c_{1}d_{1}(x_{1},y_{1}),c_{2}d_{2}(x_{2},y_{2})\right\\}$
$c_{1},c_{2}\in(0,1],c_{1}+c_{2}\leq 1$ | $c_{1}x_{1}+c_{2}x_{2}$ | $c_{1}d_{1}(x_{1},y_{1})+c_{2}d_{2}(x_{2},y_{2})$

For $c_{1}=c_{2}=1$, the first evaluation map yields exactly the categorical
product in $\mathbf{PMet}$. In both cases the Kantorovich-Rubinstein duality
holds and the supremum [infimum] of the Kantorovich [Wasserstein] pseudometric
is always a maximum [minimum].

##  3\. Compositionality for the Wasserstein Lifting

Our first step is to study compositionality of functor liftings, i.e. we
identify some sufficient conditions ensuring
$\overline{F}\,\overline{G}=\overline{FG}$. This technical result will be
often very useful since it allows us to reason modularly and, consequently, to
simplify the proofs needed in the treatment of our examples. We will
explicitly only consider the Wasserstein approach which is the one employed in
all the examples of this paper.

Given evaluation functions $ev_{F}$ and $ev_{G}$, we can easily construct an
evaluation function for the composition $FG$ by defining
$ev_{FG}:=\widetilde{F}ev_{G}=ev_{F}\circ Fev_{G}$. Our first observation is
that, whenever $F$ and $G$ preserve weak pullbacks, well-behavedness is
inherited.

######  Proposition 3.1 (Well-Behavedness of Composed Evaluation Function).

Let $F$, $G$ be endofunctors on $\mathbf{Set}$ with evaluation functions
$ev_{F}$, $ev_{G}$. If both functors preserve weak pullbacks and both
evaluation functions are well-behaved then also $ev_{FG}=ev_{F}\circ Fev_{G}$
is well-behaved.

In the light of this result and the fact that $FG$ certainly preserves weak
pullbacks if $F$ and $G$ do, we can safely use the Wasserstein lifting for
$FG$. A sufficient criterion for compositionality is the existence of optimal
couplings for $G$.

######  Proposition 3.2 (Compositionality).

Let $F,G$ be weak pullback preserving endofunctors on $\mathbf{Set}$ with
well-behaved evaluation functions $ev_{F}$, $ev_{G}$ and let $(X,d)$ be a
pseudometric space. Then
$d^{\,\downarrow{FG}}\geq(d^{\,\downarrow{G}})^{\,\downarrow{F}}$. Moreover,
if for all $t_{1},t_{2}\in GX$ there is an optimal $G$-coupling, i.e.
$\gamma(t_{1},t_{2})\in\Gamma_{G}(t_{1},t_{2})$ such that
$d^{\,\downarrow{G}}(t_{1},t_{2})=\widetilde{G}d(\gamma(t_{1},t_{2}))$, then
$d^{\,\downarrow{FG}}=(d^{\,\downarrow{G}})^{\,\downarrow{F}}$.

This criterion will turn out to be very useful for our later results.
Nevertheless it provides just a sufficient condition for compositionality as
the next example shows.

######  Example 3.3.

We consider the finite powerset functor $\mathcal{P}_{\\!f\\!i\\!n}$ of 2.8
and the distribution functor $\mathcal{D}$ of 2.9 with their evaluation
functions. Let $(X,d)$ be a pseudometric space.

  1. (1)

We have
$d^{\,\downarrow{\mathcal{D}\mathcal{D}}}=\left(d^{\,\downarrow{\mathcal{D}}}\right)^{\,\downarrow{\mathcal{D}}}$,
by 3.2, because optimal couplings always exist.

  2. (2)

We have
$d^{\,\downarrow{\mathcal{P}_{\\!f\\!i\\!n}\mathcal{P}_{\\!f\\!i\\!n}}}=\left(d^{\,\downarrow{\mathcal{P}_{\\!f\\!i\\!n}}}\right)^{\,\downarrow{\mathcal{P}_{\\!f\\!i\\!n}}}$
although $\mathcal{P}_{\\!f\\!i\\!n}$-couplings do not always exist.

Note that when we lift the functor $\mathcal{P}_{\\!f\\!i\\!n}$ we do not have
couplings in the case when we determine the distance between an empty set
$\emptyset$ and a non-empty set $Y\subseteq X$, since there exists no subset
of $X\times X$ that projects to both.

Compositionality can be defined analogously for multifunctors. Again, we will
not spell this out completely but we will use it to obtain the machine
bifunctor. Before we can do that, we first need to define another endofunctor.

######  Example 3.4 (Input Functor).

Let $A$ be a fixed finite set of inputs. The input functor
$F=\\_^{A}\colon\mathbf{Set}\to\mathbf{Set}$ maps a set $X$ to the exponential
$X^{A}$ and a function $f\colon X\to Y$ to $f^{A}\colon X^{A}\to Y^{A}$,
$f^{A}(g)=f\circ g$. This functor preserves weak pullbacks. The two evaluation
functions listed below are well-behaved and yield the given Wasserstein
pseudometric on $X^{A}$ for any pseudometric space $(X,d)$.

$ev_{F}(s)$ | $d^{\,\downarrow{F}}(s_{1},s_{2})$
---|---
$\max\limits_{a\in A}s(a)$ | $\max\limits_{a\in A}d\big{(}s_{1}(a),s_{2}(a)\big{)}$
$\sum\limits_{a\in A}s(a)$ | $\sum\limits_{a\in A}d\big{(}s_{1}(a),s_{2}(a)\big{)}$

By composing this functor with the product bifunctor we obtain the machine
bifunctor which we will use to obtain trace semantics.

######  Example 3.5 (Machine Bifunctor).

Let $A$ be a finite set of inputs, $I=\\_^{A}$ the input functor of 3.4,
$\mathrm{Id}$ the identity endofunctor on $\mathbf{Set}$ and $P$ be the
product bifunctor of 2.10. The _machine bifunctor_ is the composition
$M:=P\circ(\mathrm{Id}\times I)$ i.e. the bifunctor
$M\colon\mathbf{Set}^{2}\to\mathbf{Set}$ with $M(B,X):=B\times X^{A}$. Since
for $\mathrm{Id}$ and $I$ there are unique (thus optimal) couplings we have
compositionality. Depending on the choices of evaluation function for $P$ and
$I$ (for $\mathrm{Id}$ we always take $\mathrm{id}_{[0,1]})$ we obtain the
following well-behaved evaluation functions
$ev_{M}\colon[0,1]\times[0,1]^{A}\to[0,1]$.

Parameters | $ev_{P}(r_{1},r_{2})$ | $ev_{I}(s)$ | $ev_{M}(o,s)$
---|---|---|---
$c_{1},c_{2}\in(0,1]$ | $\max\left\\{c_{1}r_{1},c_{2}r_{2}\right\\}$ | $\max\limits_{a\in A}s(a)$ | $\max\Big{\\{}c_{1}o,c_{2}\max\limits_{a\in A}s(a)\Big{\\}}$
$\begin{matrix}c_{1},c_{2}\in(0,1],\\\ c_{1}+c_{2}\leq 1\end{matrix}$ | $c_{1}x_{1}+c_{2}x_{2}$ | $|A|^{-1}\sum\limits_{a\in A}s(a)$ |  $c_{1}o+c_{2}|A|^{-1}\sum\limits_{a\in A}s(a)$.

Let $(B,d_{B})$, $(X,d)$ be pseudometric spaces. For any $t_{1},t_{2}\in
M(B,X)$ with $t_{i}=(b_{i},s_{i})\in B\times X^{A}$ there is a unique and
therefore necessarily optimal coupling $t:=(b_{1},b_{2},\left\langle
s_{1},s_{2}\right\rangle)$. Depending on the evaluation function, we obtain
for the first case

$\displaystyle(d_{B},d)^{\,\downarrow{M}}(t_{1},t_{2})=\max\left\\{c_{1}d_{B}(b_{1},b_{2}),c_{2}\cdot\max_{a\in
A}d\big{(}s_{1}(a),s_{2}(a)\big{)}\right\\}$

and for the second case

$\displaystyle(d_{B},d)^{\,\downarrow{M}}(t_{1},t_{2})={c_{1}d_{B}(b_{1},b_{2})+{c_{2}}{|A|}^{-1}\sum_{a\in
A}d\big{(}s_{1}(a),s_{2}(a)\big{)}}\,.$

Usually we will fix the first argument (the set of outputs) of the machine
bifunctor and consider the obtained machine endofunctor $M_{B}:=M(B,\\_)$.
However, for the same reasons as explained above for the product bifunctor, we
need to consider it as bifunctor. One notable exception is the case where
$B=2$, endowed with the discrete metric. Then we have the following result.

######  Example 3.6.

Consider the machine endofunctor $M_{2}:=M(2,\\_)=2\times\\_^{A}$ with
evaluation function $ev_{M_{2}}\colon 2\times[0,1]^{A},(o,s)\mapsto c\cdot
ev_{I}(s)$ where $c\in(0,1]$ and $ev_{I}$ is one of the evaluation functions
for the input functor from 3.4. If $d_{2}$ is the discrete metric on $2$ and
$c=c_{2}$ (where $c_{2}$ is the parameter for the evaluation function of the
machine bifunctor as in 3.5) then the pseudometric obtained via the bifunctor
lifting coincides with the one obtained by endofunctor lifting i.e. for all
pseudometric spaces $(X,d)$ we have
$(d_{2},d)^{\,\downarrow{M}}=d^{\,\downarrow{M_{2}}}$. Moreover, although
couplings for $M_{2}$ do not always exist we have
$d^{\,\downarrow{\mathcal{P}_{\\!f\\!i\\!n}M_{2}}}=\left(d^{\,\downarrow{M_{2}}}\right)^{\,\downarrow{\mathcal{P}_{\\!f\\!i\\!n}}}$.

##  4\. Lifting of Natural Transformations and Monads

Recall that a monad on an arbitrary category $\mathbf{C}$ is a triple
$(T,\eta,\mu)$ where $T\colon\mathbf{C}\to\mathbf{C}$ is an endofunctor and
$\eta\colon\mathrm{Id}\Rightarrow T$, $\mu\colon T^{2}\Rightarrow T$ are
natural transformations called _unit_ ($\eta$) and _multiplication_ ($\mu$)
such that the two diagrams below commute.

${T}$${T^{2}}$${T}$${T^{3}}$${T^{2}}$${T}$${T^{2}}$${T}$$\eta
T$$T\eta$$\mu$$\mu T$$T\mu$$\mu$$\mu$

If we have a monad on $\mathbf{Set}$, we can of course use our framework to
lift the endofunctor $T$ to a functor $\overline{T}$ on pseudometric spaces. A
natural question that arises is, whether we also obtain a monad on
pseudometric spaces, i.e. if the components of the unit and the multiplication
are nonexpansive with respect to the lifted pseudometrics. In order to answer
this question, we first take a closer look at sufficient conditions for
lifting natural transformations.

######  Proposition 4.1 (Lifting of a Natural Transformation).

Let $F$, $G$ be endofunctors on $\mathbf{Set}$ with evaluation functions
$ev_{F}$, $ev_{G}$ and $\lambda\colon F\Rightarrow G$ be a natural
transformation. Then the following holds for all pseudometric spaces $(X,d)$.
For the Kantorovich lifting:

  1. (1)

If $ev_{G}\circ\lambda_{[0,\top]}\leq ev_{F}$ then
$d^{\,\uparrow{G}}\circ(\lambda_{X}\times\lambda_{X})\leq d^{\,\uparrow{F}}$,
i.e. $\lambda_{X}$ is nonexpansive.

  2. (2)

If $ev_{G}\circ\lambda_{[0,\top]}=ev_{F}$ then
$d^{\,\uparrow{G}}\circ(\lambda_{X}\times\lambda_{X})=d^{\,\uparrow{F}}$, i.e.
$\lambda_{X}$ is an isometry.

while for the Wasserstein lifting

  1. (3)

If $ev_{G}\circ\lambda_{[0,\top]}\leq ev_{F}$ then
$d^{\,\downarrow{G}}\circ(\lambda_{X}\times\lambda_{X})\leq
d^{\,\downarrow{F}}$, i.e. $\lambda_{X}$ is nonexpansive.

  2. (4)

If $ev_{G}\circ\lambda_{[0,\top]}=ev_{F}$ and the Kantorovich Rubinstein
duality holds for $F$, i.e. $d^{\,\uparrow{F}}=d^{\,\downarrow{F}}$, then
$d^{\,\downarrow{G}}\circ(\lambda_{X}\times\lambda_{X})=d^{\,\downarrow{F}}$,
i.e. $\lambda_{X}$ is an isometry.

In the rest of the paper we will call a natural transformation $\lambda$
nonexpansive [an isometry] if (and only if) each of its components are
nonexpansive [isometries] and write $\overline{\lambda}$ for the resulting
natural transformation from $\overline{F}$ to $\overline{G}$. Instead of
checking nonexpansiveness separately for each component of a natural
transformation, we can just check the above (in-)equalities involving the two
evaluation functions.

By applying these conditions on the unit and multiplication of a given monad,
we can now provide sufficient criteria for a monad lifting.

######  Corollary 4.2 (Lifting of a Monad).

Let $(T,\eta,\mu)$ be a $\mathbf{Set}$-monad and $ev_{T}$ an evaluation
function for $T$. Then the following holds.

  1. (1)

If $ev_{T}\circ\eta_{[0,\top]}\leq\mathrm{id}_{[0,\top]}$ then $\eta$ is
nonexpansive for both liftings. Hence we obtain the unit
$\overline{\eta}\colon\overline{\mathrm{Id}}\Rightarrow\overline{T}$ in
$\mathbf{PMet}$.

  2. (2)

If $ev_{T}\circ\eta_{[0,\top]}=\mathrm{id}_{[0,\top]}$ then $\eta$ is an
isometry for both liftings.

  3. (3)

Let $d^{T}\in\\{d^{\,\uparrow{T}},d^{\,\downarrow{T}}\\}$. If
$ev_{T}\circ\mu_{[0,\top]}\leq ev_{T}\circ Tev_{T}$ and compositionality holds
for $TT$, i.e. $(d^{T})^{T}=d^{TT}$, then $\mu$ is nonexpansive, i.e.
$d^{T}\circ(\mu_{X}\times\mu_{X})\leq(d^{T})^{T}$. This yields the
multiplication
$\overline{\mu}\colon\overline{T}\,\overline{T}\Rightarrow\overline{T}$ in
$\mathbf{PMet}$.

We conclude this section with two examples of liftable monads.

######  Example 4.3 (Finite Powerset Monad).

The finite powerset functor $\mathcal{P}_{\\!f\\!i\\!n}$ of 2.8 can be seen as
a monad, with unit $\eta$ consisting of the functions $\eta_{X}\colon
X\to\mathcal{P}_{\\!f\\!i\\!n}X$, $\eta_{X}(x)=\left\\{x\right\\}$ and
multiplication given by
$\mu_{X}\colon\mathcal{P}_{\\!f\\!i\\!n}\mathcal{P}_{\\!f\\!i\\!n}X\to\mathcal{P}_{\\!f\\!i\\!n}X$,
$\mu_{X}(S)=\cup S$. We check if our conditions for the Wasserstein lifting
are satisfied. Given $r\in[0,\infty]$ we have
$ev_{T}\circ\eta_{[0,\infty]}(r)=\max\left\\{r\right\\}=r$ and for
$\mathcal{S}\in\mathcal{P}_{\\!f\\!i\\!n}(\mathcal{P}_{\\!f\\!i\\!n}[0,\top])$
we have
$ev_{T}\circ\mu_{[0,1]}(\mathcal{S})=\max\cup\mathcal{S}=\max\cup_{S\in\mathcal{S}}S$
and $ev_{T}\circ
Tev_{T}(\mathcal{S})=\max\left(ev_{T}[\mathcal{S}]\right)=\max\left\\{\max
S\mid S\in\mathcal{S}\right\\}$ and thus both values coincide. Moreover, we
recall from 3.3.2 that we have compositionality for
$\mathcal{P}_{\\!f\\!i\\!n}\mathcal{P}_{\\!f\\!i\\!n}$. Therefore, by 4.2
$\eta$ is an isometry and $\mu$ nonexpansive.

######  Example 4.4 (Distribution Monad).

The probability distribution functor $\mathcal{D}$ of 2.9 can be seen as a
monad: the unit $\eta$ consists of the functions $\eta_{X}\colon
X\to\mathcal{D}X$, $\eta_{X}(x)=\delta_{x}^{X}$ where $\delta_{x}^{X}$ is the
Dirac distribution and the multiplication is given by
$\mu_{X}\colon\mathcal{D}\mathcal{D}X\to\mathcal{D}X$, $\mu_{X}(P)=\lambda
x.\sum_{q\in\mathcal{D}X}P(q)\cdot q(x)$. We consider its Wasserstein lifting.
Since $[0,1]=\mathcal{D}2$ we can see that $ev_{\mathcal{D}}=\mu_{2}$. Using
this and the monad laws we have
$ev_{\mathcal{D}}\circ\eta_{[0,1]}=\mu_{2}\circ\eta_{\mathcal{D}2}=\mathrm{id}_{\mathcal{D}X}=\mathrm{id}_{[0,1]}$
and also
$ev_{\mathcal{D}}\circ\mu_{[0,1]}=\mu_{2}\circ\mu_{\mathcal{D}2}=\mu_{2}\circ\mathcal{D}\mu_{2}=ev_{\mathcal{D}}\circ\mathcal{D}ev_{\mathcal{D}}$.
Moreover, since we always have optimal couplings, we have compositionality for
$\mathcal{D}\mathcal{D}$ by 3.2. Thus by 4.2 $\eta$ is an isometry and $\mu$
nonexpansive.

##  5\. Trace Metrics in Eilenberg-Moore

As mentioned in the introduction, trace semantics can be characterized by
means of coalgebras either over Kleisli [PT99, HJS07] or over Eilenberg-Moore
[SBBR13, JSS15] categories. We focus on the latter approach. We first recall
the basic notions of Eilenberg-Moore algebras and distributive laws, and
discuss how the results in the paper can be used to “lift” the associated
determinization construction. This is then applied to derive trace metrics for
nondeterministic automata and probabilistic automata, by relying on suitable
liftings of the machine functor.

###  5.1. Generalized Powerset Construction

An _Eilenberg-Moore algebra_ for a monad $(T,\eta,\mu)$ is a
$\mathbf{C}$-arrow $a\colon TA\to A$ making the left and middle diagram below
commute. Given two such algebras $a\colon TA\to A$ and $b\colon TB\to B$, a
morphism from $a$ to $b$ is a $\mathbf{C}$ arrow $f\colon A\to B$ making the
right diagram below commute.

${A}$${TA}$${T^{2}A}$${TA}$${TA}$${TB}$${A}$${TA}$${A}$${A}$${B}$$\eta_{A}$$a$$\mu_{A}$$a$$Tc$$a$$Tf$$b$$a$$f$

Eilenberg-Moore algebras and their morphisms form a category denoted by
$\mathcal{EM}(T)$. A functor
$\widehat{F}\colon\mathcal{EM}(T)\to\mathcal{EM}(T)$ is called a _lifting_ of
$F\colon\mathbf{C}\to\mathbf{C}$ to $\mathcal{EM}(T)$ if
$U^{T}\widehat{F}=FU^{T}$, with $U^{T}\colon\mathcal{EM}(T)\to\mathbf{C}$ the
forgetful functor. A natural transformation $\lambda\colon TF\Rightarrow FT$
is an _$\mathcal{EM}$ -law_ (also called _distributive law_) if it satisfies:

${F}$${F}$${T^{2}F}$${TFT}$${FT^{2}}$${TF}$${FT}$${TF}$${FT}$$\eta
F$$F\eta$$\lambda$$T\lambda$$\lambda T$$\mu F$$\lambda$$F\mu$

Liftings and $\mathcal{EM}$-laws are related by the following folklore result
(see e.g. [JSS12]).

######  Proposition 5.1.

There is a bijective correspondence between $\mathcal{EM}$-laws and liftings
to $\mathcal{EM}$-categories.

$\mathcal{EM}$-laws and liftings are crucial to characterize trace semantics
via coalgebras. Given a coalgebra $c\colon X\to FTX$, for a functor $F$ and a
monad $(T,\eta,\mu)$ such that there is a distributive law $\lambda\colon
TF\Rightarrow FT$, one can build an $F$-coalgebra as

${c^{\sharp}:=\Big{(}TX}$${TFTX}$${FTTX}$${FTX\big{)}}$$Tc$$\lambda_{TX}$$F\mu_{X}$

If there exists a final $F$-coalgebra $\omega\colon\Omega\to F\Omega$, one can
define a semantic map for the $FT$-coalgebra $c$ into $\Omega$. First let
$[\\![\,-\,]\\!]\colon TX\to\Omega$ be the unique coalgebra morphism from
$c^{\sharp}$. Then take the map $[\\![\,-\,]\\!]\circ\eta\colon X\to\Omega$.

${X}$${TX}$${\Omega}$${FTX}$${T\Omega}$$\eta$$[\\![\,-\,]\\!]$$c$$\omega$$F[\\![\,-\,]\\!]$$c^{\sharp}$

One can readily check that $c^{\sharp}$ is an algebra map from the $T$-algebra
$\mu_{X}$ to $\widehat{F}\mu_{X}$, namely it is an $\widehat{F}$-coalgebra or,
equivalently, a $\lambda$-_bialgebra_ [TP97, Kli11]. Similarly for $\omega$,
$\Omega$ carries a $T$-algebra structure obtained by finality and hence the
final $F$-coalgebra $\omega$ can be lifted in order to obtain the final
$\widehat{F}$-coalgebra (see [JSS12, Prop. 4]).

This result holds for arbitrary categories and, in particular, we can reuse it
for our setting: we only need an $\mathcal{EM}$-law on $\mathbf{PMet}$. Note
that 4.1 not only provides sufficient conditions for monad liftings but also
can be exploited to lift $\mathcal{EM}$-laws. Indeed the additional
commutativity requirements for $\mathcal{EM}$-laws trivially hold when all
components are nonexpansive.

######  Corollary 5.2 (Lifting of an $\mathcal{EM}$-law).

Let $F,G$ be weak pullback preserving endofunctors on $\mathbf{Set}$ with
well-behaved evaluation functions $ev_{F}$, $ev_{G}$ and $\lambda\colon
FG\Rightarrow GF$ be an $\mathcal{EM}$-law. If the evaluation functions
satisfy $ev_{G}\circ Gev_{F}\circ\lambda_{[0,\top]}\leq ev_{F}\circ Fev_{G}$
and compositionality holds for $FG$, then $\lambda$ is nonexpansive and hence
$\overline{\lambda}\colon\overline{F}\,\overline{G}\Rightarrow\overline{G}\,\overline{F}$
is also an $\mathcal{EM}$-law.

We will now consider $\mathcal{EM}$-laws for nondeterministic and
probabilistic automata. In the first case, $T$ is the powerset monad
$\mathcal{P}_{\\!f\\!i\\!n}$ and $F$ is the machine functor
$M_{2}=2\times\\_^{A}$, while in the second case $T$ is the distribution monad
$\mathcal{D}$ and $F$ is the machine functor $M_{[0,1]}=[0,1]\times\\_^{A}$.
Note however that while in the first case 5.2 is directly applicable, this is
not true in the second case, since we need to deal with multifunctors.

######  Example 5.3 ($\mathcal{EM}$-law for Nondeterministic Automata).

Let $(\mathcal{P}_{\\!f\\!i\\!n},\eta,\mu)$ be the finite powerset monad from
4.3. The $\mathcal{EM}$-law
$\lambda\colon\mathcal{P}_{\\!f\\!i\\!n}(2\times\\_^{A})\Rightarrow
2\times\mathcal{P}_{\\!f\\!i\\!n}(\\_)^{A}$ is defined, for any set $X$, as

$\displaystyle\lambda_{X}(S)=\big{(}o,\lambda a\in
A.\left\\{s^{\prime}(a)\mid(o^{\prime},s^{\prime})\in S\right\\}\big{)},\ \
\text{where}\ \ o=\begin{cases}1&\exists s^{\prime}\in X^{A}.(1,s^{\prime})\in
S\\\ 0&\text{else}\end{cases}\,.$

This is exactly the one exploited for the standard powerset construction from
automata theory [SBBR13]. Indeed, for a nondeterministic automaton $c\colon
X\to 2\times\mathcal{P}_{\\!f\\!i\\!n}(X)^{A}$, the map
$[\\![\,-\,]\\!]\circ\eta_{X}$ assigns to each state its accepted language.
5.2 ensures that it is nonexpansive (see Appendix P for a detailed proof).

######  Example 5.4 ($\mathcal{EM}$-law for Probabilistic Automata).

Let $(\mathcal{D},\eta,\mu)$ be the distribution monad from 4.4 and $M$ be the
machine bifunctor from 3.5. There is a known [SBBR13] $\mathcal{EM}$-law
$\lambda\colon\mathcal{D}([0,1]\times\\_^{A})\Rightarrow[0,1]\times\mathcal{D}^{A}$
given by the assignment

$\displaystyle\lambda_{X}(P)=\left(\sum_{r\in[0,1]}r\cdot P(r,X^{A}),\lambda
a\in A.\lambda x\in X.\sum_{{s\in
X^{A},\,s(a)=x}}\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!P([0,1],s)\right)$

Also this $\mathcal{EM}$-law is nonexpansive, as shown in Appendix P.

Any $FT$-coalgebra $c\colon X\to FTX$ can always be regarded as an
$\overline{F}\,\overline{T}$-coalgebra by equipping $X$ with the discrete
metric assigning $\top$ to non equal states (in this way, $c$ is trivially
nonexpansive). The consequence of the nonexpansiveness of the
$\mathcal{EM}$-laws $\lambda$ is the following: the “generalized
determinization” procedure for nondeterministic and probabilistic automata can
now be lifted to pass from $\overline{F}\,\overline{T}$-coalgebras to
$\widehat{\overline{F}}$-coalgebras in $\mathcal{EM}(\overline{T})$ by using
the upper adjunction in the diagram below (analogously to [JSS12, JSS15]).

${\mathbf{PMet}}$${\mathcal{EM}(\overline{T})}$${\mathbf{Set}}$${\mathcal{EM}(T)}$$U$$V$$L^{\overline{T}}$$U^{\overline{T}}$$L^{T}$$U^{T}$$\overline{F}$$F$$\widehat{\overline{F}}$$\widehat{F}$

Since we can also lift the final $\overline{F}$-coalgebra to
$\mathcal{EM}(\overline{T})$, we can use it to define trace distance. This
procedure is detailed in the next section.

###  5.2. Final Coalgebra for the Lifted Machine Functor

If we fix the first component of the machine bifunctor $M$ on $\mathbf{Set}$
we obtain an endofunctor $M_{B}\colon\mathbf{Set}\to\mathbf{Set}$,
$M_{B}(X)=B\times\\_^{A}$. It is known [MA86] that the final coalgebra for
this functor is $\kappa\colon B^{A^{*}}\to B\times(B^{A^{*}})^{A}$ with
$\kappa(t)=(t(\varepsilon),\lambda a\in A.\lambda w\in A^{*}.t(aw))$. We
employ an analogous construction with our lifted machine bifunctor
$\overline{M}$ on $\mathbf{PMet}$, i.e. we fix a pseudometric space
$(B,d_{B})$ of outputs and consider coalgebras of the functor
$\overline{M}_{(B,d_{B})}:=\overline{M}((B,d_{B}),\\_)$. To obtain the final
coalgebra for this functor in $\mathbf{PMet}$, we use the following result
from [BBKK14].

######  Proposition 5.5 ([BBKK14, Thm. 6.1]).

Let $\overline{F}\colon\mathbf{PMet}\to\mathbf{PMet}$ be a lifting of a
functor $F\colon\mathbf{Set}\to\mathbf{Set}$ which has a final coalgebra
$\kappa\colon\Omega\to F\Omega$. For every ordinal $i$ we construct a
pseudometric $d_{i}\colon\Omega\times\Omega\to{[0,\top]}$ as follows:
$d_{0}:=0$ is the zero pseudometric,
$d_{i+1}:=d_{i}^{F}\circ(\kappa\times\kappa)$ for all ordinals $i$ and
$d_{j}=\sup_{i<j}d_{i}$ for all limit ordinals $j$. This sequence converges
for some ordinal $\theta$, i.e
$d_{\theta}=d_{\theta}^{F}\circ(\kappa\times\kappa)$. Moreover
$\kappa\colon(\Omega,d_{\theta})\raisebox{-1.5pt}{$\,\mathop{\overset{1}{\to}}\,$}(F\Omega,d_{\theta}^{F})$
is the final $\overline{F}$-coalgebra.

It is hence enough to do fixed-point iteration for the functor $F$ on the
determinized state set $TX$ in order to obtain trace distance. The lifted
monad is ignored at this stage, but its lifting is of course necessary to
establish the Eilenberg-Moore category and its adjunction.

We now consider our two example cases, where in both cases $F$ is the machine
functor $M_{B}$ (for two different choices of $B$):

######  Example 5.6 (Final Coalgebra Pseudometric).

Let $M$ be the machine bifunctor.

  1. (1)

We start with nondeterministic automata where the output set is $B=2$ and we
use the discrete metric $d_{2}$ as distance on $2$ as in 3.6. As maximal
distance we take $\top=1$ and as evaluation function we use
$ev_{M}(o,s)=c\cdot\max_{a\in A}s(a)$ for $0<c<1$.

For any pseudometric $d$ on $2^{A^{*}}$ – the carrier of the final
$M_{2}$-coalgebra – we know that for elements $(o_{1},s_{1}),(o_{2},s_{2})\in
2\times(2^{A^{*}})^{A}$ we have the Wasserstein pseudometric
$d^{\,\downarrow{F}}\big{(}(o_{1},s_{1}),(o_{2},s_{2})\big{)}=\max\left\\{d_{2}(o_{1},o_{2}),c\cdot\max_{a\in
A}d\big{(}s_{1}(a),s_{2}(a)\big{)}\right\\}$. Thus the fixed-point equation
from 5.5 is, for $L_{1},L_{2}\in 2^{A^{*}}$,

$\displaystyle
d(L_{1},L_{2})=\max\left\\{d_{2}\big{(}L_{1}(\varepsilon),L_{2}(\varepsilon)\big{)},c\cdot\max_{a\in
A}d\big{(}\lambda w.L_{1}(aw),\lambda w.L_{2}(aw)\big{)}\right\\}$

Now because $d_{2}$ is the discrete metric with $d_{2}(0,1)=1$ we see that
$d_{2^{A^{*}}}$ as defined below is indeed the least fixed-point of this
equation and thus $(2^{A^{*}},d_{2^{A^{*}}})$ is the carrier of the final
$\overline{M_{2}}$-coalgebra.

$\displaystyle d_{2^{A^{*}}}\colon 2^{A^{*}}\times 2^{A^{*}}\to[0,1],\quad
d_{2^{A^{*}}}(L_{1},L_{2})=c^{\inf\left\\{n\in N\mid\exists w\in
A^{n}.L_{1}(w)\not=L_{2}(w)\right\\}}\,.$

A determinized coalgebra has as carrier set sets of states $\mathcal{P}(X)$.
Each of these sets is mapped to the language that it accepts and the distance
between two languages $L_{1},L_{2}\colon A^{*}\to 2$ can be determined by
looking for a word $w$ of minimal length which is contained in one and not in
the other. Then, the distance is computed as $c^{|w|}$. This corresponds to
the standard ultrametric on words.

  2. (2)

Next we consider probabilistic automata where $B=[0,1]$ equipped with the
standard Euclidean metric $d_{e}$.

Furthermore the remaining parameters are set as follows: let $\top=1$ and the
evaluation function is $ev_{M}(o,s)=c_{1}o+{c_{2}}{|A|}^{-1}\sum_{a\in A}s(a)$
for $c_{1},c_{2}\in(0,1)$ such that $c_{1}+c_{2}\leq 1$ as in 3.5. This time,
the machine functor must be lifted as a bifunctor in order to obtain the
appropriate distance (cf. the discussion before 2.10).

For any pseudometric $d$ on $[0,1]^{A^{*}}$ we know that for
$(r_{1},s_{1}),(r_{2},s_{2})\in[0,1]\times([0,1]^{A^{*}})^{A}$ we have
$d^{\,\downarrow{F}}((r_{1},s_{1}),(r_{2},s_{2}))=c_{1}|r_{1}-r_{2}|+\frac{c_{2}}{|A|}\cdot\sum_{a\in
A}d(s_{1}(a),s_{2}(a))$. Thus the fixed-point equation from 5.5 is, for
$p_{1},p_{2}\in[0,1]^{A^{*}}$:

$\displaystyle
d(p_{1},p_{2})=c_{1}|p_{1}(\varepsilon)-p_{2}(\varepsilon)|+\frac{c_{2}}{|A|}\cdot\sum_{a\in
A}d\Big{(}\lambda w.p_{1}(aw),\lambda w.p_{2}(aw)\Big{)}$

It is again easy to see that
$d_{[0,1]^{A^{*}}}\colon[0,1]^{A^{*}}\times[0,1]^{A^{*}}\to[0,1]$ as presented
below is the least fixed-point of this equation and therefore
$([0,1]^{A^{*}},d_{[0,1]^{A^{*}}})$ the carrier of the final
$\overline{M}_{([0,1],d_{e})}$-coalgebra.

$\displaystyle d_{[0,1]^{A^{*}}}(p_{1},p_{2})=c_{1}\cdot\sum_{w\in
A^{*}}\left(\frac{c_{2}}{|A|}\right)^{|w|}\left|p_{1}(w)-p_{2}(w)\right|\,.$

Here, a determinized coalgebra has as carrier distributions on states
$\mathcal{D}(X)$. Each such distribution is mapped to a function $p\colon
A^{*}\to[0,1]$ assigning numerical values to words. Then the distance, which
can be thought of as a form of total variation distance with discount, is
computed by the above formula.

If instead of working in the interval $[0,1]$ we use $[0,\infty]$ with
$\top=\infty$, we can drop the conditions $c_{1},c_{2}<1$ and $c_{1}+c_{2}\leq
1$. In this case we may set $c_{2}:=|A|$ and $c_{1}:=1/2$ and then the above
distance is equal to the total variation distance, i.e.,

$\displaystyle d_{[0,\infty]^{A^{*}}}(p_{1},p_{2})=\frac{1}{2}\cdot\sum_{w\in
A^{*}}\left|p_{1}(w)-p_{2}(w)\right|\,.$

##  6\. Conclusion, Related and Future Work

In the last years, an impressive amount of papers has studied behavioral
distances for both probabilistic and nondeterministic systems (see, e.g.,
[GJS90, DGJP04, vBW05, BBLM15, dAFS04, dAFS09, FLT11]). The necessity of a
general understanding of such metrics is not a mere intellectual whim but it
is perceived also by researchers exploiting distances for differential privacy
and quantitative information flow (see for instance [CGPX14]). As far as we
know, the first use of coalgebras for this purpose dates back to [vBW05],
where the authors consider systems and distance for a fixed endofunctor on
$\mathbf{PMet}$. In [BBKK14], we introduced the Kantorovich and Wasserstein
approaches as a general way to define “canonical liftings” to $\mathbf{PMet}$
and behavioral distances by finality. These are usually branching-time, while
many properties of interest for applications (see again [CGPX14]) are usually
expressed by means of distances on set of traces. In this paper, we have shown
that the work developed in [BBKK14] can be fruitfully combined with [JSS15] to
obtain various trace distances.

Among the several trace distances introduced in literature, it is worth to
mention [BBLM15, dAFS04, dAFS09, FLT11]. Similar to the trace distance we
obtain in 5.6 for probabilistic automata is the one introduced in [BBLM15] for
Semi-Markov chains with residence time. In [dAFS04, dAFS09], both branching-
time and linear-time distances are introduced for _metric transition systems_
, namely Kripke structures where states are associated with elements of a
fixed (pseudo-)metric space $M$, that would correspond to coalgebras of the
form $X\to M\times\mathcal{P}(X)$. In [BBKK14], we have shown an example
capturing branching-time distance for metric transition systems, but for
linear distances we require a distributive law of the form
$\mathcal{P}(M\times\\_)\Rightarrow M\times\mathcal{P}(\\_)$, for which we
would need at least $M$ carrying an algebra for the monad $\mathcal{P}$. We
also plan to investigate trace metrics in a Kleisli setting [HJS07], where it
might be easier to incorporate such examples.

There are two other direct consequences of our work that we did not explain in
the main text, but that are important properties of the distances that we
obtain (and, indeed, are mentioned in [CGPX14] amongst the desiderata for
“good” metrics). First, the behavioral branching-distance for
$\overline{F}\,\overline{T}$ provides an upper bound to the linear-distance
$\overline{F}$, analogously to the well-known fact that bisimilarity implies
trace equivalence. To see this, it is enough to observe that there is a
functor from the category of $\overline{F}\,\overline{T}$-coalgebras to the
one of $\overline{F}$-coalgebras mapping $c\colon
X\to\overline{F}\,\overline{T}X$ into
$c^{\sharp}\colon\overline{T}X\to\overline{F}\,\overline{T}X$.

Second, since the final map $[\\![\,-\,]\\!]$ is a morphism in
$\mathcal{EM}(\overline{T})$, the behavioral distance for $\overline{F}$ is
nonexpansive w.r.t. the operators of the monad $\overline{T}$.
Nonexpansiveness with respect to some operators is a desirable property which
has been studied, for instance in [DGJP04], as a generalization of the notion
of being a congruence for behavioral equivalence. Several researchers are now
studying syntactic rule formats ensuring this and other sorts of
compositionality (see e.g. [GT13] and the references therein) and we believe
that our 5.2 may provide some helpful insights.

In this perspective, however, our results are still unsatisfactory if compared
to what happens in the case of behavioral equivalences. From a fibrational
point of view, one has a _canonical lifting_ to $\mathbf{Rel}$ (the category
of relations and relation preserving morphisms) such that compositionality
holds on the nose and distributive laws always lift [Jac12, Exercise 4.4.6].
The forgetful functor $U\colon\mathbf{PMet}\to\mathbf{Set}$ is also a
fibration [BBKK14], but Kantorovich and Wasserstein liftings are not always so
well-behaved. Fibrations might be useful also to guarantee soundness of up-to
techniques [BPPR14] for behavioral distances that, hopefully, will lead to
more efficient proofs and algorithms.

Another interesting future work would be to show that Kantorovich and
Wasserstein liftings arise from some universal properties, i.e., that they are
the smallest and largest metric in some continuum of metrics with certain
properties. Here we would like to draw inspiration from [vB05] which
characterizes the Giry monad via a universal property on monad morphisms.

Finally, we would like to have an abstract understanding of the Kantorovich-
Rubinstein duality. Preliminary attempts suggest that this is very difficult:
indeed the proof for the probabilistic case relies on specific properties of
distributions.

## References

  * [BBKK14] Paolo Baldan, Filippo Bonchi, Henning Kerstan, and Barbara König.  Behavioral Metrics via Functor Lifting.  In Venkatesh Raman and S. P. Suresh, editors, 34th International Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2014), volume 29 of Leibniz International Proceedings in Informatics (LIPIcs), pages 403–415. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2014.
  * [BBKK15] Paolo Baldan, Filippo Bonchi, Henning Kerstan, and Barbara König.  Towards Trace Metrics via Functor Lifting.  In Proc. of CALCO 2015, Leibniz International Proceedings in Informatics (LIPIcs). Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2015\.  \- to appear -.
  * [BBLM15] Giorgio Bacci, Giovanni Bacci, Kim G. Larsen, and Radu Mardare.  On the total variation distance of semi-markov chains.  In Foundations of Software Science and Computation Structures (FOSSACS 2015), volume 9034 of Lecture Notes in Computer Science. Springer, 2015.
  * [BPPR14] Filippo Bonchi, Daniela Petrisan, Damien Pous, and Jurriaan Rot.  Coinduction up to in a fibrational setting.  In Proc. of CSL-LICS ’14, 2014.
  * [CGPX14] Konstantinos Chatzikokolakis, Daniel Gebler, Catuscia Palamidessi, and Lili Xu.  Generalized bisimulation metrics.  In CONCUR 2014 – Concurrency Theory, Lecture Notes in Computer Science, pages 32–46, 2014.
  * [dAFS04] Luca de Alfaro, Marco Faella, and Mariëlle Stoelinga.  Linear and branching metrics for quantitative transition systems.  In Proc. of ICALP ’04, volume 3142 of Lecture Notes in Computer Science, pages 97–109. Springer, 2004.
  * [dAFS09] Luca de Alfaro, Marco Faella, and Mariëlle Stoelinga.  Linear and branching system metrics.  IEEE Transactions on Software Engineering, 25(2), 2009.
  * [DGJP04] Josée Desharnais, Vineet Gupta, Radha Jagadeesan, and Prakash Panangaden.  Metrics for labelled Markov processes.  Theoretical Computer Science, 318(3):323–354, 2004.
  * [FLT11] Uli Fahrenberg, Axel Legay, and Claus Thrane.  The quantitative linear-time–branching-time spectrum.  In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011), volume 13 of Leibniz International Proceedings in Informatics (LIPIcs), pages 103–114. Schloss Dagstuhl – Leibniz Center for Informatics, 2011.
  * [GJS90] Alessandro Giacalone, Chi-Chang Jou, and Scott A. Smolka.  Algebraic reasoning for probabilistic concurrent systems.  In Proc. IFIP TC2 Working Conference on Programming Concepts and Methods, pages 443–458. North-Holland, 1990.
  * [GT13] Daniel Gebler and Simone Tini.  Compositionality of approximate bisimulation for probabilistic systems.  In Proc. of EXPRESS/SOS ’13, pages 32–46, 2013.
  * [HJS07] Ichiro Hasuo, Bart Jacobs, and Ana Sokolova.  Generic trace semantics via coinduction.  Logical Methods in Computer Science, 3 (4:11):1–36, November 2007\.
  * [Jac12] Bart Jacobs.  Introduction to coalgebra. Towards mathematics of states and observations, 2012.  Draft.
  * [JSS12] Bart Jacobs, Alexandra Silva, and Ana Sokolova.  Trace semantics via determinization.  In Dirk Pattinson and Lutz Schröder, editors, Coalgebraic Methods in Computer Science, volume 7399 of Lecture Notes in Computer Science, pages 109–129. Springer Berlin Heidelberg, 2012.
  * [JSS15] Bart Jacobs, Alexandra Silva, and Ana Sokolova.  Trace semantics via determinization.  Journal of Computer and System Sciences, 81(5):859 – 879, 2015\.  11th International Workshop on Coalgebraic Methods in Computer Science, CMCS 2012 (Selected Papers).
  * [Kli11] Bartek Klin.  Bialgebras for structural operational semantics: An introduction.  Theoretical Computer Science, 412(38):5043–5069, 2011.
  * [MA86] E.G. Manes and M.A. Arbib.  Algebraic approaches to program semantics.  Texts and Monographs in Computer Science, 1986.
  * [PT99] John Power and Daniele Turi.  A coalgebraic foundation for linear time semantics.  Electronic Notes in Theoretical Computer Science, 29:259–274, 1999\.
  * [Rut00] J.J.M.M. Rutten.  Universal coalgebra: a theory of systems.  Theoretical Computer Science, 249:3–80, 2000.
  * [SBBR13] Alexandra Silva, Filippo Bonchi, Marcello M. Bonsangue, and Jan J. M. M. Rutten.  Generalizing determinization from automata to coalgebras.  Logical Methods in Computer Science, 9(1), 2013.
  * [Sch08] Lutz Schröder.  Expressivity of coalgebraic modal logic: The limits and beyond.  Theoretical Computer Science, 390(2–3):230–247, 2008.
  * [TP97] Daniele Turi and Gordon D. Plotkin.  Towards a mathematical operational semantics.  In Proc. of LICS ’97, pages 280–291, 1997.
  * [vB05] Franck van Breugel.  The metric monad for probabilistic nondeterminism, April 2005.
  * [vBW05] Franck van Breugel and James Worrell.  A behavioural pseudometric for probabilistic transition systems.  Theoretical Computer Science, 331:115–142, 2005.
  * [vBW06] Franck van Breugel and James Worrell.  Approximating and computing behavioural distances in probabilistic transition systems.  Theoretical Computer Science, 360(1):373–385, 2006.
  * [Vil09] Cédric Villani.  Optimal Transport – Old and New, volume 338 of A Series of Comprehensive Studies in Mathematics.  Springer, 2009.

##  Appendix P Proofs

Here we provide proofs for the soundness of our definitions (where needed),
the stated theorems, propositions, lemmas, examples and also for all claims
made in the in-between texts. If a theorem environment starts with the symbol
$\circlearrowleft$ it has been stated in the main text and is repeated here
for convenience of the reader (using the numbering from the main text).
Otherwise it is a new statement which clarifies/justifies claims made in the
main text and its number starts with _P_.

###  P.2. Preliminaries

For the upcoming proofs we will often use the following, alternative
characterization of W3.

######  Lemma  (Weak Pullback Characterization of W3).

Let $F$ be an endofunctor on $\mathbf{Set}$ with evaluation function $ev_{F}$
and $i\colon\left\\{0\right\\}\hookrightarrow[0,\top]$ be the inclusion
function. For any set $X$ we denote the unique arrow into $\left\\{0\right\\}$
by $!_{X}\colon X\to\left\\{0\right\\}$. Then $ev_{F}$ satisfies
$ev_{F}^{-1}[\left\\{0\right\\}]=Fi[F\left\\{0\right\\}]$ if and only if the
diagram on the right is a weak pullback.
${F\left\\{0\right\\}}$${\left\\{0\right\\}}$${F[0,\top]}$${{[0,\top]}}$$!_{F\left\\{0\right\\}}$$Fi$$i$$ev_{F}$

######  Proof P.1.

Commutativity of the diagram is equivalent to
$ev_{F}^{-1}[\left\\{0\right\\}]\supseteq Fi[F\left\\{0\right\\}]$. Given a
set $X$ and a function $f\colon X\to F[0,\top]$ as depicted below, we conclude
again by commutativity ($i\circ!_{X}=ev_{F}\circ f$) that $f(x)\in
ev_{F}^{-1}[\left\\{0\right\\}]$ for all $x\in X$.

${X}$${F\left\\{0\right\\}}$${\left\\{0\right\\}}$${F[0,\top]}$${{[0,\top]}}$$!_{X}$$f$$\varphi$$!_{F\left\\{0\right\\}}$$Fi$$i$$ev_{F}$

Now if $ev_{F}^{-1}[\left\\{0\right\\}]\subseteq Fi[F\left\\{0\right\\}]$ then
for $f(x)\in ev_{F}^{-1}[\left\\{0\right\\}]$ we can choose a (not necessarily
unique) $x_{0}\in F\left\\{0\right\\}$ such that $f(x)=Fi(x_{0})$. If we
define $\varphi\colon X\to F\left\\{0\right\\}$ by $\varphi(x)=x_{0}$ then
clearly $\varphi$ makes the above diagram commute and thus we have a weak
pullback.

Conversely if the diagram is a weak pullback consider the set
$X=ev_{F}^{-1}[\left\\{0\right\\}]$ and the function $f\colon
ev_{F}^{-1}[\left\\{0\right\\}]\hookrightarrow F[0,\top],f(x)=x$. Now for any
$x\in ev_{F}^{-1}[\left\\{0\right\\}]$ we have
$Fi(\varphi(x))=(Fi\circ\varphi)(x)=f(x)=x$, hence since $\varphi(x)\in
F\left\\{0\right\\}$ we have $x\in Fi[F\left\\{0\right\\}]$.

######  $\circlearrowleft$ Example 2.9 _(Finitely Supported Distributions)_.

The probability distribution functor $\mathcal{D}$ assigns to each set $X$ the
set $\mathcal{D}X=\left\\{P\colon X\to[0,1]\ \middle|\
|\mathrm{supp}(P)|<\infty,P(X)=1\right\\}$ and to each function $f\colon X\to
Y$ the function $\mathcal{D}f\colon\mathcal{D}X\to\mathcal{D}Y$,
$\mathcal{D}f(P)(y)=\sum_{x\in
f^{-1}[\left\\{y\right\\}]}P(x)=P(f^{-1}[\left\\{y\right\\}])$. $\mathcal{D}$
preserves weak pullbacks and the evaluation function
$ev_{\mathcal{D}}\colon\mathcal{D}[0,1]\to[0,1]$,
$ev_{\mathcal{D}}(P)=\sum_{r\in[0,1]}r\cdot P(r)$ is well-behaved. For any
pseudometric space $(X,d)$ we obtain the Wasserstein pseudometric which, for
any $P_{1},P_{2}\in\mathcal{D}X$, is defined as

$\displaystyle
d^{\,\downarrow{\mathcal{D}}}(P_{1},P_{2})=\min\left\\{\sum_{x_{1},x_{2}\in
X}d(x_{1},x_{2})\cdot P(x_{1},x_{2})\ \middle|\
P\in\Gamma_{\mathcal{D}}(P_{1},P_{2})\right\\}\,.$

The Kantorovich-Rubinstein duality [Vil09] holds from classical results in
transportation theory.

######  Proof P.2.

Weak pullback preservation, well-behavedness and the duality was already
presented in [BBKK14]. Here we just quickly check that indeed the infimum is a
minimum: Let
$\mathrm{supp}(P_{1})\cup\mathrm{supp}(P_{2})=\left\\{s_{1},\dots,s_{n}\right\\}$
be the union of the finite supports of $P_{1}$ and $P_{2}$. Then define the
following finitely many real numbers $p_{1i}:=P_{1}(s_{i})$,
$p_{2j}:=P_{2}(s_{j})$, $d_{ij}:=d(s_{i},s_{j})$. Then the distance of $P_{1}$
and $P_{2}$ can be equivalently expressed as the following LP:

minimize $\displaystyle\sum_{1\leq i,j\leq n}d_{ij}\cdot x_{ij}$ subject to
$\displaystyle\sum_{1\leq j\leq n}x_{ij}=p_{1i}$ $\displaystyle,\ $
$\displaystyle 1\leq i\leq n$ $\displaystyle\sum_{1\leq i\leq n}x_{ij}=p_{2j}$
$\displaystyle,\ $ $\displaystyle 1\leq j\leq n$ $\displaystyle 0\leq
x_{ij}\leq 1,$ $\displaystyle 1\leq i,j\leq n$

whose feasible region is nonempty ($x_{ij}:=p_{1i}\cdot p_{2j}$ is in it) and
bounded. Thus we indeed get an optimal solution $x_{ij}^{*}$ and can define
the optimal coupling as $P^{*}(s_{i},s_{j}):=x_{ij}^{*}$.

######  $\circlearrowleft$ Example 2.10 _(Product Bifunctor)_.

The weak pullback preserving product bifunctor
$F\colon\mathbf{Set}^{2}\to\mathbf{Set}$ maps two sets $X_{1},X_{2}$ to
$F(X_{1},X_{2})=X_{1}\times X_{2}$ and two functions $f_{i}\colon X_{i}\to
Y_{i}$ to the function $F(f_{1},f_{2})=f_{1}\times f_{2}$. In this paper we
will use the well-behaved evaluation functions $ev_{F}\colon[0,1]^{2}\to[0,1]$
presented in the table below. Therein we also list the pseudometric
$(d_{1},d_{2})^{F}\colon X_{1}\times X_{2}\to[0,\top]$ we obtain for
pseudometric spaces $(X_{1},d_{1})$, $(X_{2},d_{2})$.

Parameters | $ev_{F}(r_{1},r_{2})$ | $(d_{1},d_{2})^{F}((x_{1},x_{2}),(y_{1},y_{2}))$
---|---|---
$c_{1},c_{2}\in(0,1]$ | $\max\left\\{c_{1}r_{1},c_{2}r_{2}\right\\}$ | $\max\left\\{c_{1}d_{1}(x_{1},y_{1}),c_{2}d_{2}(x_{2},y_{2})\right\\}$
$c_{1},c_{2}\in(0,1],c_{1}+c_{2}\leq 1$ | $c_{1}x_{1}+c_{2}x_{2}$ | $c_{1}d_{1}(x_{1},y_{1})+c_{2}d_{2}(x_{2},y_{2})$

For $c_{1}=c_{2}=1$, the first evaluation map yields exactly the categorical
product in $\mathbf{PMet}$. In both cases the Kantorovich-Rubinstein duality
holds and the supremum [infimum] of the Kantorovich [Wasserstein] pseudometric
is always a maximum [minimum].

######  Proof P.3.

We adapt the proof given in [BBKK14, Exa. 5.1] to also include the discounted
maximum (all other cases were covered there). First we show well-behavedness.

  1. (1)

Let $f_{i},g_{i}\colon X_{i}\to[0,\top]$ with $f_{i}\leq g_{i}$ be given. Then
we have

$\displaystyle\widetilde{F}(f_{1},f_{2})=\max(c_{1}f_{1},c_{2}f_{2})\leq\max(c_{1}g_{1},c_{2}g_{2})=\widetilde{F}(g_{1},g_{2})\,.$

  2. (2)

Let $t:=(x_{11},x_{21},x_{12},x_{22})\in
F([0,\top]^{2},[0,\top]^{2})=[0,\top]^{2}\times[0,\top]^{2}$. We have to show
the inequality
$d_{e}\big{(}\widetilde{F}(\pi_{1},\pi_{1})(t),\widetilde{F}(\pi_{2},\pi_{2})(t))\leq\widetilde{F}(d_{e},d_{e})(t)$.
We observe that
$\widetilde{F}(d_{e},d_{e})(t)=ev_{F}(d_{e}(x_{11},x_{21}),d_{e}(x_{12},x_{22}))$
and if we define
$z_{i}=ev_{F}(x_{i1},x_{i2})=\max\left\\{c_{1}x_{i1},c_{2}x_{i2}\right\\}$
then
$d_{e}\big{(}\widetilde{F}(\pi_{1},\pi_{1})(t),\widetilde{F}(\pi_{2},\pi_{2})(t))=d_{e}(z_{1},z_{2})$.
We thus have to show the inequality

$d_{e}\left(z_{1},z_{2}\right)\leq
ev_{F}(d_{e}(x_{11},x_{21}),d_{e}(x_{12},x_{22}))\,.$ (1)

If $z_{1}=z_{2}$ this is obviously true because $d_{e}(z_{1},z_{2})=0$ and the
rhs is non-negative. We now assume $z_{1}>z_{2}$ (the other case is
symmetrical). For $\infty=z_{1}>z_{2}$ the inequality holds because then
$x_{11}=\infty$ or $x_{12}=\infty$ and $x_{21},x_{22}<\infty$ (otherwise we
would have $z_{2}=\infty$) so both lhs and rhs are $\infty$. Thus we can now
restrict to $\infty>z_{1}>z_{2}$ where necessarily also
$x_{11},x_{12},x_{21},x_{22}<\infty$ (otherwise we would have $z_{1}=\infty$
or $z_{2}=\infty$). According to [BBKK14, Lemma P2.1], the inequality (1) is
equivalent to showing the two inequalities

$\displaystyle z_{1}$ $\displaystyle\leq
z_{2}+ev_{F}\big{(}d_{e}(x_{11},x_{21}),d_{e}(x_{12},x_{22})\big{)},\quad\text{and}$
$\displaystyle\ z_{2}$ $\displaystyle\leq
z_{1}+ev_{F}\big{(}d_{e}(x_{11},x_{21}),d_{e}(x_{12},x_{22})\big{)}\,.$

By our assumption ($\infty>z_{1}>z_{2}$) the second of these inequalities is
satisfied, so we just have to show the first. If $z_{1}=c_{1}x_{11}$ we have

$\displaystyle
z_{2}+\max\left\\{c_{1}d_{e}(x_{11},x_{21}),c_{2}d_{e}(x_{12},x_{22})\right\\}$
$\displaystyle\geq z_{2}+c_{1}d_{e}(x_{11},x_{21})=z_{2}+c_{1}|x_{11}-x_{21}|$
$\displaystyle\geq z_{2}+c_{1}(x_{11}-x_{21})=z_{2}+c_{1}x_{11}-c_{1}x_{21}$
$\displaystyle=z_{2}+z_{1}-c_{1}x_{21}=z_{1}+(z_{2}-c_{1}x_{21})\geq z_{1}$

because $z_{2}=\max\left\\{c_{1}x_{21},c_{2}x_{22}\right\\}>c_{1}x_{21}$ and
therefore $(z_{2}-c_{1}x_{21})\geq 0$. The same line of argument can be
applied if $z_{1}=c_{2}x_{12}$.

  3. (3)

$F(i,i)[F(\left\\{0\right\\},\left\\{0\right\\})]=(i\times
i)[\left\\{0\right\\}\times\left\\{0\right\\}]=\left\\{(0,0)\right\\}$ and
$ev_{F}^{-1}[\left\\{0\right\\}]=\left\\{(0,0)\right\\}$.

We now prove that the Kantorovich-Rubinstein duality holds and simultaneously
that the supremum (in the Kantorovich pseudometric) is a maximum and the
infimum (of the Wasserstein pseudometric) is a minimum. Let $(X_{1},d_{1})$,
$(X_{1},d_{2})$ be pseudometric spaces and let $t_{i}=(x_{i1},x_{i2})\in
F(X_{1},X_{2})=X_{1}\times X_{2}$ be given. Their unique coupling is
$t:=((x_{11},x_{21}),(x_{12},x_{2}))\in\Gamma_{F}(t_{1},t_{2})$ and we have
$\widetilde{F}(d_{1},d_{2})(t)=\max\\{c_{1}d_{1}(x_{1},y_{1}),c_{2}d_{2}(x_{2},y_{2})\\}$.
We define $f_{i}:=d_{i}(x_{1i},\\_)$, which are nonexpansive due to [BBKK14,
Lemma 2.3]. Then we clearly have $f_{i}(x_{1i})=0$ and moreover

$\displaystyle
d_{e}\big{(}\widetilde{F}(f_{1},f_{2})(t_{1}),\widetilde{F}(f_{1},f_{2})(t_{2})\big{)}$
$\displaystyle=d_{e}\left(ev_{F}\big{(}f_{1}(x_{11}),f_{2}(x_{12})\big{)},ev_{F}\big{(}f_{1}(x_{21}),f_{2}(x_{22})\big{)}\right)$
$\displaystyle=d_{e}\big{(}0,\max\left\\{c_{1}d_{1}(x_{11},x_{21}),c_{2}d_{2}(x_{12},x_{22})\right\\}\big{)}$
$\displaystyle=\max\left\\{c_{1}d_{1}(x_{11},x_{21}),c_{2}d_{2}(x_{12},x_{22})\right\\}=\widetilde{F}(d_{1},d_{2})(t)$

Due to [BBKK14, Proposition P.5.7] we can now conclude that duality holds and
both supremum and infimum are attained and equal to the above maximum.

###  P.3. Compositionality for the Wasserstein Lifting

####  P.3.1. Compositionality for Endofunctors

We first collect a few simple observations that we will use in the upcoming
proofs.

######  Lemma .

Let $F,G$ be endofunctors on $\mathbf{Set}$ with evaluation functions
$ev_{F},ev_{G}$ and $a:=\langle G\pi_{1},G\pi_{2}\rangle$ (i.e. the unique
mediating arrow into the product) and $(X,d)$ an arbitrary pseudometric space.
Then the following holds.

  1. (1)

$\widetilde{G}d\geq d^{\,\downarrow{G}}\circ a\geq d^{\,\uparrow{G}}\circ a$

  2. (2)

$\forall t_{1},t_{2}\in FGX:\quad t\in\Gamma_{FG}(t_{1},t_{2})\implies
Fa(t)\in\Gamma_{F}(t_{1},t_{2})$.

  3. (3)

If $F$ and $G$ preserve weak pullbacks then so does $FG$.

  4. (4)

For any $f\in\mathbf{Set}/[0,\top]$ we have
$\widetilde{FG}f=\widetilde{F}(\widetilde{G}f)$.

######  Proof P.4.

We first of all observe that $a$ is the unique mediating arrow into the
product as indicated in the following diagram.

${G(X\times X)}$${GX}$${GX\times
GX}$${GX}$$G\pi_{1}$$G\pi_{2}$$\pi_{1}$$\pi_{2}$$a=\left\langle
G\pi_{1},G\pi_{2}\right\rangle$

  1. (1)

Let $s\in G(X\times X)$ and define $s_{i}:=G\pi_{i}^{X}(s)=\pi_{i}^{GX}\circ
a(s)$. Then by definition $s\in\Gamma_{G}(s_{1},s_{2})$ and we conclude
$\widetilde{G}d(s)\geq\inf\\{\widetilde{G}d(s^{\prime})\mid
s^{\prime}\in\Gamma_{G}(s_{1},s_{2})\\}=d^{\,\downarrow{G}}(s_{1},s_{2})=d^{\,\downarrow{G}}(\pi_{1}^{GX}\circ
a(s),\pi_{2}^{GX}\circ a(s))=d^{\,\downarrow{G}}\circ a(s)$. Since we always
have $d^{\,\downarrow{G}}\geq d^{\,\uparrow{G}}$ as shown in [BBKK14], the
statement follows.

  2. (2)

$F\pi_{i}^{GX}(Fa(t))=F(\pi_{i}^{GX}\circ
a)(t)=F(G\pi_{i}^{X})(t)=FG\pi_{i}^{X}=t_{i}$.

  3. (3)

This is indeed clear by definition.

  4. (4)

Let $f\colon X\to[0,\top]$, then $\widetilde{FG}f=ev_{FG}\circ FGf=ev_{F}\circ
Fev_{G}\circ FGf=ev_{F}\circ F(ev_{G}\circ Gf)=\widetilde{F}(\widetilde{G}f)$.

######  Lemma .

Let $F$,$G$ be functors with evaluation functions $ev_{F}$ and $ev_{G}$ and
define $ev_{FG}:=ev_{F}\circ Fev_{G}$. Then the following holds.

  1. (1)

If $\widetilde{F}$ and $\widetilde{G}$ are monotone (Condition W1), then so is
$\widetilde{FG}$.

  2. (2)

If $G$ preserves weak pullbacks, $ev_{G}$ is well-behaved and $\widetilde{F}$
is monotone then $ev_{FG}$ satisfies Condition W2 of well-behavedness.

  3. (3)

If $F$ preserves weak pullbacks and $ev_{F},ev_{G}$ satisfy Condition W3 of
well-behavedness, then also $ev_{FG}$ satisfies Condition W3 of well-
behavedness.

######  Proof P.5.

  1. (1)

Let $f,g\colon X\to[0,\top]$ with $f\leq g$, then by monotonicity of $ev_{G}$
we have $\widetilde{G}f\leq\widetilde{G}g$ and using monotonicity of $ev_{F}$
we get
$\widetilde{FG}f=\widetilde{F}(\widetilde{G}f)\leq\widetilde{F}(\widetilde{G}g)=\widetilde{FG}g$.

  2. (2)

Let $t\in FG([0,\top]^{2})$ and define $t_{i}:=FG\pi_{i}(t)\in FG[0,\top]$. By
definition $t\in\Gamma_{FG}(t_{1},t_{2})$ so subsubsection P.3.1 tells us
$Fa(t)\in\Gamma_{F}(t_{1},t_{2})$ for $a:=\langle G\pi_{1},G\pi_{2}\rangle$.
Moreover, since
$ev_{G}\colon(G[0,\top],d_{e}^{\,\uparrow{G}})\raisebox{-1.5pt}{$\,\mathop{\overset{1}{\to}}\,$}([0,\top],d_{e})$
is nonexpansive (by definition of the Kantorovich pseudometric), we can apply
[BBKK14, Prop. P.4.2] to obtain the inequality

$\displaystyle
d_{e}(ev_{FG}(t_{1}),ev_{FG}(t_{2}))=d_{e}(\widetilde{F}ev_{G}(t_{1}),\widetilde{F}ev_{G}(t_{2}))\leq\widetilde{F}d_{e}^{\,\uparrow{G}}(Fa(t))=\widetilde{F}(d_{e}^{\,\uparrow{G}}\circ
a)(t)\,.$

By subsubsection P.3.1 we have $d_{e}^{\,\uparrow{G}}\circ
a\leq\widetilde{G}{d_{e}}$ and using monotonicity of $\widetilde{F}$ we can
continue our inequality with $\widetilde{F}(d_{e}^{\,\uparrow{G}}\circ
a)(t)\leq\widetilde{F}(\widetilde{G}{d_{e}})(t)=\widetilde{FG}d_{e}(t)$ which
concludes the proof!

  3. (3)

Using Appendix P.2 we just have to show that the following diagram is a weak
pullback.

${FG\left\\{0\right\\}}$${F\left\\{0\right\\}}$${\left\\{0\right\\}}$${FG[0,\top]}$${F{[0,\top]}}$${{[0,\top]}}$$F!_{G\left\\{0\right\\}}$$FGi$$Fi$$Fev_{G}$$!_{F\left\\{0\right\\}}$$i$$ev_{F}$$!_{FG\left\\{0\right\\}}$$ev_{FG}$

Appendix P.2 tells us that the right square is a weak pullback and since $F$
preserves weak pullbacks also the left square is. The outer part is
necessarily a weak pullback again yielding by Appendix P.2 that $ev_{FG}$
satisfies the third condition.

######  $\circlearrowleft$ Proposition 3.1 _(Well-Behavedness of Composed
Evaluation Function)_.

Let $F$, $G$ be endofunctors on $\mathbf{Set}$ with evaluation functions
$ev_{F}$, $ev_{G}$. If both functors preserve weak pullbacks and both
evaluation functions are well-behaved then also $ev_{FG}=ev_{F}\circ Fev_{G}$
is well-behaved.

######  Proof P.6.

This is an immediate corollary of subsubsection P.3.1.

To prove our compositionality criteria, we use the following results.

######  Lemma .

Let $F$, $G$ be endofunctors on $\mathbf{Set}$ with evaluation functions
$ev_{F}\colon F[0,\top]\to[0,\top]$, $ev_{G}\colon G[0,\top]\to[0,\top]$. We
define $ev_{FG}:=ev_{F}\circ Fev_{G}$. Then the following holds for every
pseudometric space $(X,d)$.

  1. (1)

$d^{\,\uparrow{FG}}\leq(d^{\,\uparrow{G}})^{\,\uparrow{F}}$.

  2. (2)

If $F$ and $G$ preserve weak pullbacks and $ev_{F},ev_{G}$ are well-behaved
then $d^{\,\downarrow{FG}}\geq(d^{\,\downarrow{G}})^{\,\downarrow{F}}$.

  3. (3)

If for all $t_{1},t_{2}\in FGX$ there is a function
$\nabla(t_{1},t_{2})\colon\Gamma_{F}(t_{1},t_{2})\to\Gamma_{FG}(t_{1},t_{2})$
such that
$\widetilde{FG}d\circ\nabla(t_{1},t_{2})=\widetilde{F}d^{\,\downarrow{G}}$
then $d^{\,\downarrow{FG}}\leq(d^{\,\downarrow{G}})^{\,\downarrow{F}}$.

######  Proof P.7.

Let $t_{1},t_{2}\in FGX$.

  1. (1)

Recall that $d^{\,\uparrow{G}}$ is the smallest pseudometric such that for
every nonexpansive function
$f\colon(X,d)\raisebox{-1.5pt}{$\,\mathop{\overset{1}{\to}}\,$}([0,\top],d_{e})$
also
$\widetilde{G}f\colon(GX,d^{\,\uparrow{G}})\raisebox{-1.5pt}{$\,\mathop{\overset{1}{\to}}\,$}([0,\top],d_{e})$
is nonexpansive (see remark after [BBKK14, Def. 3.1]). Moreover,
$\widetilde{FG}f=\widetilde{F}(\widetilde{G}f)$ by subsubsection P.3.1. Thus

$\displaystyle d^{\,\uparrow{FG}}(t_{1},t_{2})$
$\displaystyle=\sup\left\\{d_{e}\big{(}\widetilde{FG}f(t_{1}),\widetilde{FG}f(t_{2})\big{)}\mid
f\colon(X,d)\raisebox{-1.5pt}{$\,\mathop{\overset{1}{\to}}\,$}([0,\top],d_{e})\right\\}$
$\displaystyle=\sup\left\\{d_{e}\big{(}\,\widetilde{F}(\widetilde{G}f)(t_{1}),\widetilde{F}(\widetilde{G}f)(t_{2})\big{)}\mid
f\colon(X,d)\raisebox{-1.5pt}{$\,\mathop{\overset{1}{\to}}\,$}([0,\top],d_{e})\right\\}$
$\displaystyle\leq\sup\left\\{d_{e}\big{(}\,\widetilde{F}(g)(t_{1}),\widetilde{F}(g)(t_{2})\big{)}\mid
g\colon(GX,d^{\,\uparrow{G}})\raisebox{-1.5pt}{$\,\mathop{\overset{1}{\to}}\,$}([0,\top],d_{e})\right\\}$
$\displaystyle=(d^{\,\uparrow{G}})^{\,\uparrow{F}}(t_{1},t_{2})$

  2. (2)

subsubsection P.3.1 tells us $\widetilde{G}d\geq d^{\,\downarrow{G}}\circ a$
and for any coupling $t\in\Gamma_{FG}(t_{1},t_{2})$ we have
$Fa(t)\in\Gamma_{F}(t_{1},t_{2})$. Using these facts and the monotonicity of
$\widetilde{F}$ we obtain:

$\displaystyle d^{\,\downarrow{FG}}(t_{1},t_{2})$
$\displaystyle=\inf\left\\{\widetilde{FG}d(t)\mid
t\in\Gamma_{FG}(t_{1},t_{2})\right\\}=\inf\left\\{\widetilde{F}(\widetilde{G}d)(t)\mid
t\in\Gamma_{FG}(t_{1},t_{2})\right\\}$
$\displaystyle\geq\inf\left\\{\widetilde{F}(d^{\,\downarrow{G}}\circ a)(t)\mid
t\in\Gamma_{FG}(t_{1},t_{2})\right\\}$
$\displaystyle=\inf\left\\{\widetilde{F}d^{\,\downarrow{G}}\big{(}Fa(t)\big{)}\mid
t\in\Gamma_{FG}(t_{1},t_{2})\right\\}$
$\displaystyle\geq\inf\left\\{\widetilde{F}d^{\,\downarrow{G}}(t^{\prime})\mid
t^{\prime}\in\Gamma_{F}(t_{1},t_{2})\right\\}=(d^{\,\downarrow{G}})^{\,\downarrow{F}}(t_{1},t_{2})$

  3. (3)

Using $\nabla(t_{1},t_{2})$ we compute

$\displaystyle d^{\,\downarrow{FG}}(t_{1},t_{2})$
$\displaystyle=\inf{\left\\{\widetilde{FG}d(t^{\prime})\mid
t^{\prime}\in\Gamma_{FG}(t_{1},t_{2})\right\\}}$
$\displaystyle\leq\inf{\left\\{\widetilde{FG}d\big{(}\nabla(t_{1},t_{2})(t)\big{)}\mid
t\in\Gamma_{F}(t_{1},t_{2})\right\\}}$
$\displaystyle=\inf{\left\\{\widetilde{F}d^{\,\downarrow{G}}(t)\mid
t\in\Gamma_{F}(t_{1},t_{2})\right\\}}=(d^{\,\downarrow{G}})^{\,\downarrow{F}}(t_{1},t_{2})\,.$

With this result at hand we can prove

######  $\circlearrowleft$ Proposition 3.2 _(Compositionality)_.

Let $F,G$ be weak pullback preserving endofunctors on $\mathbf{Set}$ with
well-behaved evaluation functions $ev_{F}$, $ev_{G}$ and let $(X,d)$ be a
pseudometric space. Then
$d^{\,\downarrow{FG}}\geq(d^{\,\downarrow{G}})^{\,\downarrow{F}}$. Moreover,
if for all $t_{1},t_{2}\in GX$ there is an optimal $G$-coupling, i.e.
$\gamma(t_{1},t_{2})\in\Gamma_{G}(t_{1},t_{2})$ such that
$d^{\,\downarrow{G}}(t_{1},t_{2})=\widetilde{G}d(\gamma(t_{1},t_{2}))$, then
$d^{\,\downarrow{FG}}=(d^{\,\downarrow{G}})^{\,\downarrow{F}}$.

######  Proof P.8.

From subsubsection P.3.1.2 we know
$d^{\,\downarrow{FG}}\geq(d^{\,\downarrow{G}})^{\,\downarrow{F}}$. By our
requirement we have a function $\gamma\colon GX\times GX\to G(X\times X)$,
such that $d^{\,\downarrow{G}}=\widetilde{G}d\circ\gamma$. Given
$t_{1},t_{2}\in FGX$ and $t\in\Gamma_{F}(t_{1},t_{2})$, we define
$\nabla(t_{1},t_{2})(t)=F\gamma(t)$, then this satisfies the conditions of
subsubsection P.3.1.3. First, we have $F\gamma(t)\in\Gamma_{FG}(t_{1},t_{2})$
because
$FG\pi_{i}^{X}(F\gamma(t))=F(G\pi_{i}^{X}\circ\gamma)(t)=F\pi_{i}^{GX}(t)=t_{i}$.
Moreover

$\displaystyle\widetilde{FG}d\big{(}F\gamma(t)\big{)}$
$\displaystyle=ev_{FG}\circ F\big{(}Gd\circ\gamma(t)\big{)}=ev_{F}\circ
Fev_{G}\circ F(Gd\circ\gamma)(t)$ $\displaystyle=ev_{F}\circ
F\big{(}\widetilde{G}d\circ\gamma\big{)}(t)=ev_{F}\circ
Fd^{\,\downarrow{G}}(t)=\widetilde{F}d^{\,\downarrow{G}}(t)\,.$

######  $\circlearrowleft$ Example 3.3.

We consider the finite powerset functor $\mathcal{P}_{\\!f\\!i\\!n}$ of 2.8
and the distribution functor $\mathcal{D}$ of 2.9 with their evaluation
functions. Let $(X,d)$ be a pseudometric space.

  1. (1)

We have
$d^{\,\downarrow{\mathcal{D}\mathcal{D}}}=\left(d^{\,\downarrow{\mathcal{D}}}\right)^{\,\downarrow{\mathcal{D}}}$,
by 3.2, because optimal couplings always exist.

  2. (2)

We have
$d^{\,\downarrow{\mathcal{P}_{\\!f\\!i\\!n}\mathcal{P}_{\\!f\\!i\\!n}}}=\left(d^{\,\downarrow{\mathcal{P}_{\\!f\\!i\\!n}}}\right)^{\,\downarrow{\mathcal{P}_{\\!f\\!i\\!n}}}$
although $\mathcal{P}_{\\!f\\!i\\!n}$-couplings do not always exist.

######  Proof P.9.

We just have to prove the second claim. We already know from subsubsection
P.3.1.2 that

$\displaystyle
d^{\,\downarrow{\mathcal{P}_{\\!f\\!i\\!n}\mathcal{P}_{\\!f\\!i\\!n}}}\geq\left(d^{\,\downarrow{\mathcal{P}_{\\!f\\!i\\!n}}}\right)^{\,\downarrow{\mathcal{P}_{\\!f\\!i\\!n}}}$
(2)

holds. We now show that we always have equality. Let $(X,d)$ be a pseudometric
space and
$T_{1},T_{2}\in\mathcal{P}_{\\!f\\!i\\!n}\mathcal{P}_{\\!f\\!i\\!n}X$. We
distinguish three cases:
_Case 1_ : If $T_{1}=T_{2}=\emptyset$ we know by reflexivity that both values
are $0$.
_Case 2_ : If $T_{1}=\emptyset\not=T_{2}$ or $T_{1}\not=\emptyset=T_{2}$ we
know from [BBKK14] that
$\Gamma_{\mathcal{P}_{\\!f\\!i\\!n}}(T_{1},T_{2})=\emptyset$ and therefore
$\left(d^{\,\downarrow{\mathcal{P}_{\\!f\\!i\\!n}}}\right)^{\,\downarrow{\mathcal{P}_{\\!f\\!i\\!n}}}(T_{1},T_{2})=\top$
and thus (2) is an equality.
_Case 3_ : Let $T_{1},T_{2}\not=\emptyset$. We know from [BBKK14] that we have
an optimal coupling
$T^{*}\in\Gamma_{\mathcal{P}_{\\!f\\!i\\!n}}(T_{1},T_{2})$, say
$T^{*}=\left\\{(V_{j1},V_{j2})\in\mathcal{P}_{\\!f\\!i\\!n}X\times\mathcal{P}_{\\!f\\!i\\!n}X\mid
j\in J\right\\}$ for a suitable index set $J$. Then
$T_{i}=\mathcal{P}_{\\!f\\!i\\!n}\pi_{i}(T^{*})=\pi_{i}[T^{*}]=\left\\{\pi_{i}((V_{j1},V_{j2}))\mid
j\in J\right\\}=\left\\{V_{ji}\mid j\in J\right\\}$. By optimality:

$\displaystyle\left(d^{\,\downarrow{\mathcal{P}_{\\!f\\!i\\!n}}}\right)^{\,\downarrow{\mathcal{P}_{\\!f\\!i\\!n}}}(T_{1},T_{2})=\widetilde{\mathcal{P}_{\\!f\\!i\\!n}}{d^{\,\downarrow{\mathcal{P}_{\\!f\\!i\\!n}}}}(T^{*})=\max
d^{\,\downarrow{\mathcal{P}_{\\!f\\!i\\!n}}}[T^{*}]=\max_{j\in
J}d^{\,\downarrow{\mathcal{P}_{\\!f\\!i\\!n}}}(V_{j1},V_{j2})\,.$ (3)

Again we will make a case distinction:

  * •

If there is a $j^{\prime}\in J$ such that
$\Gamma_{\mathcal{P}_{\\!f\\!i\\!n}}(V_{j^{\prime}1},V_{j^{\prime}2})=\emptyset$,
we have
$d^{\,\downarrow{\mathcal{P}_{\\!f\\!i\\!n}}}(V_{j^{\prime}1},V_{j^{\prime}2})=\top$
and using (3) also
$\left(d^{\,\downarrow{\mathcal{P}_{\\!f\\!i\\!n}}}\right)^{\,\downarrow{\mathcal{P}_{\\!f\\!i\\!n}}}(T_{1},T_{2})=\top$
which again shows that (2) is an equality.

  * •

Otherwise we can take optimal couplings
$V_{j}^{*}\in\Gamma_{\mathcal{P}_{\\!f\\!i\\!n}}(V_{j1},V_{j2})$. Continuing
(3) we have

$\displaystyle\left(d^{\,\downarrow{\mathcal{P}_{\\!f\\!i\\!n}}}\right)^{\,\downarrow{\mathcal{P}_{\\!f\\!i\\!n}}}(T_{1},T_{2})=\max_{j\in
J}\widetilde{\mathcal{P}_{\\!f\\!i\\!n}}d(V_{j}^{*})=\max_{j\in J}\max
d[V_{j}^{*}]$ (4)

Then we define $T:=\left\\{V_{j}^{*}\mid j\in
J\right\\}\subseteq\mathcal{P}_{\\!f\\!i\\!n}\mathcal{P}_{\\!f\\!i\\!n}(X\times
X)$. We calculate for $\pi_{i}\colon X\times X\to X$

$\displaystyle\mathcal{P}_{\\!f\\!i\\!n}\mathcal{P}_{\\!f\\!i\\!n}\pi_{i}(T)=\mathcal{P}_{\\!f\\!i\\!n}\pi_{i}[T]=\left\\{\mathcal{P}_{\\!f\\!i\\!n}\pi_{i}(V_{j}^{*})\mid
j\in J\right\\}=\left\\{V_{ji}\mid j\in J\right\\}=T_{i}$

and thus
$T\in\Gamma_{\mathcal{P}_{\\!f\\!i\\!n}\mathcal{P}_{\\!f\\!i\\!n}}(T_{1},T_{2})$.
Moreover we have

$\displaystyle
d^{\,\downarrow{\mathcal{P}_{\\!f\\!i\\!n}\mathcal{P}_{\\!f\\!i\\!n}}}(T_{1},T_{2})$
$\displaystyle\leq\widetilde{\mathcal{P}_{\\!f\\!i\\!n}\mathcal{P}_{\\!f\\!i\\!n}}d(T)=\max\left(\mathcal{P}_{\\!f\\!i\\!n}\max\left(\mathcal{P}_{\\!f\\!i\\!n}\mathcal{P}_{\\!f\\!i\\!n}(T)\right)\right)$
$\displaystyle=\max\left(\max\left[\mathcal{P}_{\\!f\\!i\\!n}d[T]\right]\right)=\max\left(\max\left\\{d[V_{j}^{*}]\mid
j\in J\right\\}\right)$ $\displaystyle=\max_{j\in J}\max d[V_{j}^{*}]$ (5)

thus using this, (4) and (2) we conclude that

$\displaystyle
d^{\,\downarrow{\mathcal{P}_{\\!f\\!i\\!n}\mathcal{P}_{\\!f\\!i\\!n}}}(T_{1},T_{2})\leq\max_{j\in
J}\max
d[V_{j}^{*}]=\left(d^{\,\downarrow{\mathcal{P}_{\\!f\\!i\\!n}}}\right)^{\,\downarrow{\mathcal{P}_{\\!f\\!i\\!n}}}(T_{1},T_{2})\leq
d^{\,\downarrow{\mathcal{P}_{\\!f\\!i\\!n}\mathcal{P}_{\\!f\\!i\\!n}}}(T_{1},T_{2})$

which proves equality.

To verify the claims made in 3.4 we need the following intermediary result.

######  Lemma .

For finite $A$ and functions $f,g\colon A\to[0,\infty]$ we have

  1. (1)

$d_{e}\big{(}\max_{a\in A}f(a),\max_{a\in A}g(a)\big{)}\leq\max_{a\in
A}d_{e}\big{(}f(a),g(a)\big{)}$.

  2. (2)

$d_{e}\left(\sum_{a\in A}f(a),\sum_{a\in A}g(a)\right)\leq\sum_{a\in
A}d_{e}\big{(}f(a),g(a)\big{)}$.

######  Proof P.10.

  1. (1)

Let $a_{f}\in\operatorname*{arg\max}_{a\in A}f(a)$ and
$a_{g}\in\operatorname*{arg\max}_{a\in A}g(a)$, i.e. $a_{f}=\max_{a\in A}f$
and $a_{g}=\max_{a\in A}g$. If $f(a_{f})=g(a_{g})$ the lhs is $0$ and the
inequality is satisfied. From here we assume wlog $f(a_{f})>g(a_{g})$. Now if
$f(a_{f})=\infty$, the lhs is $\infty$ but also $\max_{a\in
A}d_{e}(f(a),g(a))\geq d_{e}(f(a_{f}),g(a_{f}))=\infty$. Finally, for
$f(a_{f})<\infty$ we have $g(a_{f})\leq g(a_{g})$ and thus
$d_{e}(f(a_{f}),g(a_{g}))=f(a_{f})-g(a_{g})\leq
f(a_{f})-g(a_{f})\leq\max_{a\in A}d_{e}(f(a),g(a))$.

  2. (2)

Let $s_{f}:=\sum_{a\in A}f(a)$ and $s_{g}:=\sum_{g\in A}f(a)$. If
$s_{f}=s_{g}$ the lhs is $0$ and the inequality is satisfied. From here we
assume wlog $s_{f}>s_{g}$. Now if $s_{f}=\infty$, the lhs is $\infty$ but we
also must have an $a^{\prime}\in A$ such that $f(a^{\prime})=\infty$
(otherwise $s_{f}<\infty$) and thus $\sum_{a\in A}d_{e}(f(a),g(a))\geq
d_{e}(f(a^{\prime}),g(a^{\prime}))=\infty$. Finally, for $s_{f}<\infty$ we
have $d_{e}(s_{f},s_{g})=s_{f}-s_{g}=\sum_{a\in A}f(a)-\sum_{a\in
A}g(a)=\sum_{a\in A}\left(f(a)-g(a)\right)\leq\sum_{a\in
A}|f(a)-g(a)|=\sum_{a\in A}d_{e}(f(a),g(a))$.

######  $\circlearrowleft$ Example 3.4 _(Input Functor)_.

Let $A$ be a fixed finite set of inputs. The input functor
$F=\\_^{A}\colon\mathbf{Set}\to\mathbf{Set}$ maps a set $X$ to the exponential
$X^{A}$ and a function $f\colon X\to Y$ to $f^{A}\colon X^{A}\to Y^{A}$,
$f^{A}(g)=f\circ g$. This functor preserves weak pullbacks. The two evaluation
functions listed below are well-behaved and yield the given Wasserstein
pseudometric on $X^{A}$ for any pseudometric space $(X,d)$.

$ev_{F}(s)$ | $d^{\,\downarrow{F}}(s_{1},s_{2})$
---|---
$\max\limits_{a\in A}s(a)$ | $\max\limits_{a\in A}d\big{(}s_{1}(a),s_{2}(a)\big{)}$
$\sum\limits_{a\in A}s(a)$ | $\sum\limits_{a\in A}d\big{(}s_{1}(a),s_{2}(a)\big{)}$

######  Proof P.11.

We first show that the functor $F:=\\_^{A}$ on $\mathbf{Set}$ preserves
pullbacks. If we have a pullback in $\mathbf{Set}$ as indicated in the left of
the diagram below, then we have to show that the right diagram is a pullback.

${P}$${X_{1}}$${P^{A}}$${X_{1}^{A}}$${X_{2}}$${Y}$${X_{2}^{A}}$${Y^{A}}$$p_{1}$$p_{2}$$f_{1}$$f_{2}$$p_{1}^{A}$$p_{2}^{A}$$f_{1}^{A}$$f_{2}^{A}$

We consider the canonical pullback: $P:=\left\\{(x_{1},x_{2})\in X_{1}\times
X_{2}\mid f_{1}(x_{1})=f_{2}(x_{2})\right\\}$ along with $p_{i}:=\pi_{i}|_{P}$
and

$\displaystyle P^{\prime}$ $\displaystyle:=\left\\{(g_{1},g_{2})\in
X_{1}^{A}\times X_{2}^{A}\mid f_{1}^{A}(g_{1})=f_{2}^{A}(g_{2})\right\\}$
$\displaystyle\cong\left\\{\langle g_{1},g_{2}\rangle\in(X_{1}\times
X_{2})^{A}\mid\forall a\in
A.f_{1}\big{(}g_{1}(a)\big{)}=f_{2}\big{(}g_{2}(a)\big{)}\right\\}$
$\displaystyle\cong\left\\{\langle g_{1},g_{2}\rangle\in(X_{1}\times
X_{2})^{A}\mid\forall a\in A.\Big{(}\big{(}g_{1}(a),g_{2}(a)\big{)}\in
P\Big{)}\right\\}\cong P^{A}$

which completes the proof of weak pullback preservation. We now show that the
evaluation functions are well-behaved. For $f\colon X\to[0,\top]$ we have
$\widetilde{F}f=ev_{F}\circ f^{A}$ i.e. applying it to $g\in X^{A}$ yields
$\max{a\in A}f(g(a))$ or $\sum_{a\in A}f(g(a))$.

  1. W1.

For $f_{1},f_{2}\colon X\to[0,\top]$ with $f_{1}\leq f_{2}$ we obviously also
have $\widetilde{F}f_{1}\leq\widetilde{F}f_{2}$.

  2. W2.

Let $t\in([0,\top]^{2})^{A}$ and $t_{i}:=\pi_{i}^{A}(t)$, i.e. necessarily
$t=\langle t_{1},t_{2}\rangle$. We have to show

$\displaystyle
d_{e}\big{(}ev_{F}(t_{1}),ev_{F}(t_{2})\big{)}\leq\widetilde{F}d_{e}(t)=ev_{F}\big{(}d_{e}^{A}(t)\big{)}=ev_{F}(d_{e}\circ
t)=ev_{F}(d_{e}\circ\left\langle t_{1},t_{2}\right\rangle)\,.$

which for our evaluation functions follows from subsubsection P.3.1 with
$f=t_{1}$, $g=t_{2}$.

  3. W3.

We have $ev_{F}^{-1}[\left\\{0\right\\}]=\left\\{g\colon A\to[0,\top]\mid
ev_{F}(g)=0\right\\}$. Clearly for both functions this is the case only if $r$
is the constant $0$-function. Since $\left\\{0\right\\}$ is a final object in
$\mathbf{Set}$, there is a unique function $z\colon A\to\left\\{0\right\\}$.
Thus
$Fi[F\left\\{0\right\\}]=i^{A}[\left\\{0\right\\}^{A}]=\left\\{i^{A}(z)\right\\}=\left\\{i\circ
z\right\\}$ and clearly $i\circ z\colon A\to[0,\top]$ is also the constant
$0$-function.

Now if we have $s_{1},s_{2}\in X^{A}$ their unique coupling is
$s:=\left\langle s_{1},s_{2}\right\rangle\colon A\to X\times X$. Moreover
$\widetilde{F}d(s)=ev_{F}(d^{A}(s))=ev_{F}(\lambda a.d(\left\langle
s_{1},s_{2}\right\rangle))=ev_{F}(\lambda a.d(s_{1}(a),s_{2}(a))$ and using
the two different evaluation functions we obtain the given pseudometrics.

####  P.3.2. Compositionality for Multifunctors

We conclude this section with a more detailed presentation on how our theory
extends to multifunctors.

For $n\in\mathbb{N}$ we denote by $[n]:=\\{1,\dots,n\\}\subseteq\mathbb{N}$
the set of all positive natural numbers less than or equal to $n$. Now let
$n_{i}\in\mathbb{N}$ for all $i\in[n]$ and
$F\colon\mathbf{Set}^{n}\to\mathbf{Set}$ and
$G_{i}\colon\mathbf{Set}^{n_{i}}\to\mathbf{Set}$ (for $i\in[n]$) be
multifunctors with evaluation functions $ev_{F}\colon
F({[0,\top]}^{n})\to[0,\top]$ and $ev_{G_{i}}\colon
G_{i}([0,\top]^{n_{i}})\to[0,\top]$. We define $N:=\sum_{i=1}^{n}n_{i}$ and
define the functor

$\displaystyle H:=F\circ\prod_{i=1}^{n}G_{i}=F\circ(G_{1}\times
G_{2}\times\dots\times G_{n})\colon\mathbf{Set}^{N}\to\mathbf{Set}$

Then we can define the evaluation function $ev_{H}\colon
H([0,\top]^{N})\to[0,\top]$ by

$\displaystyle ev_{H}:=ev_{F}\circ
F(ev_{G_{1}},ev_{G_{2}},\dots,ev_{G_{n}})\,.$

In this setting, compositionality for the Wasserstein lifting means that
whenever we have $N$ pseudometric spaces $(X_{i},d_{i})$ the pseudometric
$(d_{1},\dots,d_{N})^{\,\downarrow{H}}$ is equal to

$\displaystyle\left((d_{1},\dots,d_{n_{1}})^{\,\downarrow{G_{1}}},(d_{n_{1}+1},\dots,d_{n_{1}+n_{2}})^{\,\downarrow{G_{2}}}\dots,(d_{N-n_{n}+1},\dots,d_{N})^{\,\downarrow{G_{n}}}\right)^{\,\downarrow{F}}\,.$

In the examples in this paper we will just have the following two cases:

  1. (1)

$n=1$, $n_{1}=2$ so that $F\colon\mathbf{Set}\to\mathbf{Set}$ is an
endofunctor with evaluation function $ev_{F}\colon F[0,\top]\to[0,\top]$ and
$G\colon\mathbf{Set}^{2}\to\mathbf{Set}$ is a bifunctor with evaluation
function $ev_{G}\colon G([0,\top],[0,\top])\to[0,\top]$. Then we have
$N=n_{1}=2$ and obtain the bifunctor $H=F\circ
G\colon\mathbf{Set}^{2}\to\mathbf{Set}$ with evaluation $ev_{H}=ev_{F}\circ
Fev_{G}\colon FG([0,1],[0,1])\to[0,1]$. Compositionality means that for an two
pseudometric spaces $(X_{1},d_{1})$, $(X_{2},d_{2})$ we have
$(d_{1},d_{2})^{\,\downarrow{H}}=((d_{1},d_{2})^{\,\downarrow{G}})^{\,\downarrow{F}}$.

  2. (2)

$n=2$, $n_{1}=n_{2}=1$ so that $F\colon\mathbf{Set}^{2}\to\mathbf{Set}$ is a
bifunctor with evaluation function $ev_{F}\colon
F([0,\top],[0,\top])\to[0,\top]$ and
$G_{1},G_{2}\colon\mathbf{Set}\to\mathbf{Set}$ are endofunctors with
evaluations $ev_{G_{i}}\colon G_{i}[0,\top]\to[0,\top]$. Then we have
$N=n_{1}+n_{2}=1+1=2$ and obtain the bifunctor $H=F\circ(G_{1}\times
G_{2})\colon\mathbf{Set}^{2}\to\mathbf{Set}$ with evaluation
$ev_{H}=ev_{F}\circ F(ev_{G_{1}},ev_{G_{2}})\colon
F(G_{1}[0,\top],G_{2}[0,\top])\to[0,\top]$. Compositionality means that for an
two pseudometric spaces $(X_{1},d_{1})$, $(X_{2},d_{2})$ we have
$(d_{1},d_{2})^{\,\downarrow{H}}=(d_{1}^{\,\downarrow{G}},d_{2}^{\,\downarrow{G_{2}}})^{\,\downarrow{F}}$.

The results presented for endofunctors work analogously in the multifunctor
case (the proofs can be transferred almost verbatim), so we do not explicitly
present them here.

######  $\circlearrowleft$ Example 3.5 _(Machine Bifunctor)_.

Let $A$ be a finite set of inputs, $I=\\_^{A}$ the input functor of 3.4,
$\mathrm{Id}$ the identity endofunctor on $\mathbf{Set}$ and $P$ be the
product bifunctor of 2.10. The _machine bifunctor_ is the composition
$M:=P\circ(\mathrm{Id}\times I)$ i.e. the bifunctor
$M\colon\mathbf{Set}^{2}\to\mathbf{Set}$ with $M(B,X):=B\times X^{A}$. Since
for $\mathrm{Id}$ and $I$ there are unique (thus optimal) couplings we have
compositionality. Depending on the choices of evaluation function for $P$ and
$I$ (for $\mathrm{Id}$ we always take $\mathrm{id}_{[0,1]})$ we obtain the
following well-behaved evaluation functions
$ev_{M}\colon[0,1]\times[0,1]^{A}\to[0,1]$.

Parameters | $ev_{P}(r_{1},r_{2})$ | $ev_{I}(s)$ | $ev_{M}(o,s)$
---|---|---|---
$c_{1},c_{2}\in(0,1]$ | $\max\left\\{c_{1}r_{1},c_{2}r_{2}\right\\}$ | $\max\limits_{a\in A}s(a)$ | $\max\Big{\\{}c_{1}o,c_{2}\max\limits_{a\in A}s(a)\Big{\\}}$
$\begin{matrix}c_{1},c_{2}\in(0,1],\\\ c_{1}+c_{2}\leq 1\end{matrix}$ | $c_{1}x_{1}+c_{2}x_{2}$ | $|A|^{-1}\sum\limits_{a\in A}s(a)$ |  $c_{1}o+c_{2}|A|^{-1}\sum\limits_{a\in A}s(a)$.

Let $(B,d_{B})$, $(X,d)$ be pseudometric spaces. For any $t_{1},t_{2}\in
M(B,X)$ with $t_{i}=(b_{i},s_{i})\in B\times X^{A}$ there is a unique and
therefore necessarily optimal coupling $t:=(b_{1},b_{2},\left\langle
s_{1},s_{2}\right\rangle)$. Depending on the evaluation function, we obtain
for the first case

$\displaystyle(d_{B},d)^{\,\downarrow{M}}(t_{1},t_{2})=\max\left\\{c_{1}d_{B}(b_{1},b_{2}),c_{2}\cdot\max_{a\in
A}d\big{(}s_{1}(a),s_{2}(a)\big{)}\right\\}$

and for the second case

$\displaystyle(d_{B},d)^{\,\downarrow{M}}(t_{1},t_{2})={c_{1}d_{B}(b_{1},b_{2})+{c_{2}}{|A|}^{-1}\sum_{a\in
A}d\big{(}s_{1}(a),s_{2}(a)\big{)}}\,.$

######  Proof P.12.

We first compute the composed evaluation functions. Let
$(o,s)\in[0,1]\times[0,1]^{A}$, then

$\displaystyle ev_{M}(o,s)$ $\displaystyle=ev_{P}\circ
P(\mathrm{id}_{[0,\top]},ev_{I})(o,s)=ev_{P}\circ(\mathrm{id}_{[0,\top]}\times
ev_{I})(o,s)=ev_{P}\Big{(}o,ev_{I}(s)\Big{)}$

For the first case we thus have
$ev_{M}(o,s)=\max\left\\{c_{1}o,c_{2}\max_{a\in A}s(a)\right\\}$ and for the
second $ev_{M}(o,s)=c_{1}o+c_{2}{|A|}^{-1}\sum_{a\in A}d(s_{1}(a),s_{2}(a))$
as claimed. Given $t_{1},t_{2}\in M(B,X)$ with $t_{i}=(b_{i},s_{i})\in B\times
X^{A}$ we take their unique coupling $t:=(b_{1},b_{2},\left\langle
s_{1},s_{2}\right\rangle)$ to compute for pseudometrics $d_{B}$ on $B$ and $d$
on $X$:

$\displaystyle(d_{B},d)^{\,\downarrow{M}}(t_{1},t_{2})$
$\displaystyle=\widetilde{M}(d_{B},d)(t)=ev_{M}\circ M(d_{B},d)(t)$
$\displaystyle=ev_{M}\circ\left(d_{B}\times
d^{A}\right)\left(b_{1},b_{2},\left\langle s_{1},s_{2}\right\rangle\right)$
$\displaystyle=ev_{M}\Big{(}d_{B}(b_{1},b_{2}),\lambda
a.d\big{(}s_{1}(a),s_{2}(a)\big{)}\Big{)}\,.$

Now if we take the two evaluation functions from above, we obtain the
Wasserstein pseudometrics which are given in the example.

######  $\circlearrowleft$ Example 3.6.

Consider the machine endofunctor $M_{2}:=M(2,\\_)=2\times\\_^{A}$ with
evaluation function $ev_{M_{2}}\colon 2\times[0,1]^{A},(o,s)\mapsto c\cdot
ev_{I}(s)$ where $c\in(0,1]$ and $ev_{I}$ is one of the evaluation functions
for the input functor from 3.4. If $d_{2}$ is the discrete metric on $2$ and
$c=c_{2}$ (where $c_{2}$ is the parameter for the evaluation function of the
machine bifunctor as in 3.5) then the pseudometric obtained via the bifunctor
lifting coincides with the one obtained by endofunctor lifting i.e. for all
pseudometric spaces $(X,d)$ we have
$(d_{2},d)^{\,\downarrow{M}}=d^{\,\downarrow{M_{2}}}$. Moreover, although
couplings for $M_{2}$ do not always exist we have
$d^{\,\downarrow{\mathcal{P}_{\\!f\\!i\\!n}M_{2}}}=\left(d^{\,\downarrow{M_{2}}}\right)^{\,\downarrow{\mathcal{P}_{\\!f\\!i\\!n}}}$.

######  Proof P.13.

We first prove that the bifunctor and endofunctor liftings coincide. Given
$t_{1},t_{2}\in 2\times X^{A}$, say $t_{i}=(o_{i},s_{i})$, their unique
$M$-coupling is $t=(o_{1},o_{2},\left\langle s_{1},s_{2}\right\rangle)$.

If $o_{1}\not=o_{2}$ no $M_{2}$-coupling of $t_{1},t_{2}$ exists so we have
$d^{\,\downarrow{M_{2}}}{(t_{1},t_{2})}=\top$ but also
$d_{2}(o_{1},o_{2})=\top$ so
$(d_{2},d)^{\,\downarrow{M}}(t_{1},t_{2})=\widetilde{M}(d_{2},d)(t)\geq
c_{1}d_{2}(o_{1},o_{2})\geq\top$.

If $o_{1}=o_{2}$ the unique $M_{2}$-coupling of $t_{1},t_{2}$ is
$t^{\prime}=(o_{1},\left\langle s_{1},s_{2}\right\rangle)$ and
$d_{2}(o_{1},o_{2})=0$ thus

$\displaystyle(d_{2},d_{e})^{\,\downarrow{M}}(t_{1},t_{2})$
$\displaystyle=\widetilde{M}(d_{2},d)(t)=c_{2}ev_{I}\Big{(}\lambda
a.d\big{(}s_{1}(a),s_{2}(a)\big{)}\Big{)}$
$\displaystyle=ev_{M_{2}}\Big{(}o_{1},\lambda
a.d\big{(}s_{1}(a),s_{2}(a)\big{)}\Big{)}=ev_{M_{2}}\Big{(}\big{(}\mathrm{id}_{2}\times
d^{A}\big{)}\big{(}o_{1},\left\langle s_{1},s_{2}\right\rangle\big{)}\Big{)}$
$\displaystyle=\widetilde{M_{2}}(t^{\prime})=d^{\,\downarrow{M_{2}}}(t_{1},t_{2})\,.$

For compositionality we adapt the proof of 3.3. We know from subsubsection
P.3.1.2 that

$\displaystyle
d^{\,\downarrow{\mathcal{P}_{\\!f\\!i\\!n}M_{2}}}\geq\left(d^{\,\downarrow{M_{2}}}\right)^{\,\downarrow{\mathcal{P}_{\\!f\\!i\\!n}}}$
(6)

holds. We now show that we always have equality. Let $(X,d)$ be a pseudometric
space and
$T_{1},T_{2}\in\mathcal{P}_{\\!f\\!i\\!n}M_{2}X=\mathcal{P}_{\\!f\\!i\\!n}(2\times
X^{A})$. We distinguish three cases:
_Case 1_ : If $T_{1}=T_{2}=\emptyset$ we know by reflexivity that both values
are $0$.
_Case 2_ : If $T_{1}=\emptyset\not=T_{2}$ or $T_{1}\not=\emptyset=T_{2}$ we
know from [BBKK14] that
$\Gamma_{\mathcal{P}_{\\!f\\!i\\!n}}(T_{1},T_{2})=\emptyset$ and therefore
$\left(d^{\,\downarrow{M_{2}}}\right)^{\,\downarrow{\mathcal{P}_{\\!f\\!i\\!n}}}(T_{1},T_{2})=\top$
and thus (6) is an equality.
_Case 3_ : Let $T_{1},T_{2}\not=\emptyset$. We know from [BBKK14] that we have
an optimal coupling
$T^{*}\in\Gamma_{\mathcal{P}_{\\!f\\!i\\!n}}(T_{1},T_{2})$, say
$T^{*}=\left\\{\big{(}(o_{j1},s_{j1}),(o_{j2},s_{j2})\big{)}\in M_{2}X\times
M_{2}X\mid j\in J\right\\}$ for a suitable index set $J$. Then using
$\pi_{i}\colon M_{2}X\times M_{2}X\to M_{2}X$ we have
$T_{i}=\mathcal{P}_{\\!f\\!i\\!n}\pi_{i}(T^{*})=\pi_{i}[T^{*}]=\left\\{\pi_{i}\big{(}(o_{j1},s_{j1}),(o_{j2},s_{j2})\big{)}\mid
j\in J\right\\}=\left\\{(o_{ji},s_{ji})\mid j\in J\right\\}$. By optimality:

$\displaystyle\left(d^{\,\downarrow{M_{2}}}\right)^{\,\downarrow{\mathcal{P}_{\\!f\\!i\\!n}}}(T_{1},T_{2})$
$\displaystyle=\widetilde{\mathcal{P}_{\\!f\\!i\\!n}}{d^{\,\downarrow{M_{2}}}}(T^{*})=\max
d^{\,\downarrow{M_{2}}}[T^{*}]$ $\displaystyle=\max_{j\in
J}d^{\,\downarrow{M_{2}}}\big{(}(o_{j1},s_{j1}),(o_{j2},s_{j2})\big{)}\,.$ (7)

Again we will make a case distinction:

  * •

If there is a $j^{\prime}\in J$ such that
$\Gamma_{M_{2}}\big{(}(o_{j^{\prime}1},s_{j^{\prime}1}),(o_{j^{\prime}2},s_{j^{\prime}2})\big{)}=\emptyset$
(iff $o_{j^{\prime}1}\not=o_{j^{\prime}2}$), we have
$d^{\,\downarrow{M_{2}}}\big{(}(o_{j1},s_{j1}),(o_{j2},s_{j2})\big{)}=\top$
and using (7) also
$\left(d^{\,\downarrow{M_{2}}}\right)^{\,\downarrow{\mathcal{P}_{\\!f\\!i\\!n}}}(T_{1},T_{2})=\top$
which again shows that (6) is an equality.

  * •

Otherwise for every $j\in J$ we can take the unique coupling
$(o_{j1},\left\langle
s_{j1},s_{j2}\right\rangle)\in\Gamma_{M_{2}}\big{(}(o_{j1},s_{j1}),(o_{j2},s_{j2})\big{)}$
which is necessarily optimal. Continuing (7) we have

$\displaystyle\left(d^{\,\downarrow{M_{2}}}\right)^{\,\downarrow{\mathcal{P}_{\\!f\\!i\\!n}}}(T_{1},T_{2})$
$\displaystyle=\max_{j\in J}\widetilde{M_{2}}d\left(o_{j1},\left\langle
s_{j1},s_{j2}\right\rangle\right)$ $\displaystyle=\max_{j\in
J}ev_{M_{2}}\Big{(}\big{(}\mathrm{id}_{2}\times
d^{A}\big{)}\big{(}o_{j1},\left\langle
s_{j1},s_{j2}\right\rangle\big{)}\Big{)}$ $\displaystyle=\max_{j\in
J}ev_{M_{2}}\Big{(}o_{j1},\lambda a.d\big{(}s_{j1}(a),s_{j2}(a)\big{)}\Big{)}$
$\displaystyle=c\cdot\max_{j\in J}ev_{I}\Big{(}\lambda
a.d\big{(}s_{j1}(a),s_{j2}(a)\big{)}\Big{)}$ (8)

Then we define

$\displaystyle T:=\left\\{(o_{j1},\left\langle s_{j1},s_{j2}\right\rangle)\mid
j\in J\right\\}\subseteq\mathcal{P}_{\\!f\\!i\\!n}M_{2}(X\times
X)=\mathcal{P}_{\\!f\\!i\\!n}\Big{(}2\times(X\times X)^{A}\Big{)}\,.$

We calculate for $\pi_{i}\colon X\times X\to X$

$\displaystyle\mathcal{P}_{\\!f\\!i\\!n}M_{2}\pi_{i}(T)=(\mathrm{id}_{2}\times\pi_{i}^{A})[T]=\left\\{(o_{j1},s_{ji})\mid
j\in J\right\\}=T_{i}$

and thus $T\in\Gamma_{\mathcal{P}_{\\!f\\!i\\!n}M_{2}}(T_{1},T_{2})$. Moreover
we have

$\displaystyle d^{\,\downarrow{\mathcal{P}_{\\!f\\!i\\!n}M_{2}}}(T_{1},T_{2})$
$\displaystyle\leq\widetilde{\mathcal{P}_{\\!f\\!i\\!n}M_{2}}d(T)=ev_{\mathcal{P}_{\\!f\\!i\\!n}}\circ\mathcal{P}_{\\!f\\!i\\!n}ev_{M2}\circ\mathcal{P}_{\\!f\\!i\\!n}M_{2}d(T)$
$\displaystyle=\max\left(\mathcal{P}_{\\!f\\!i\\!n}\left(ev_{M2}\circ
M_{2}d\right)(T)\right)=\max\left((ev_{M_{2}}\circ M_{2}d)[T]\right)$
$\displaystyle=\max\Big{(}ev_{M2}\big{[}(\mathrm{id}_{2}\times
d^{A})[T]\big{]}\Big{)}$ $\displaystyle=\max_{j\in
J}ev_{M2}\Big{(}o_{j1},\lambda a.d\big{(}s_{j1}(a),s_{j2}(a)\big{)}\Big{)}$
$\displaystyle=c\cdot\max_{j\in J}ev_{I}\Big{(}\lambda
a.d\big{(}s_{j1}(a),s_{j2}(a)\big{)}\Big{)}$ (9)

thus using this, (8) and (6) we conclude that

$\displaystyle d^{\,\downarrow{\mathcal{P}_{\\!f\\!i\\!n}M_{2}}}(T_{1},T_{2})$
$\displaystyle\leq c\cdot\max_{j\in J}ev_{I}\Big{(}\lambda
a.d\big{(}s_{j1}(a),s_{j2}(a)\big{)}\Big{)}$
$\displaystyle=\left(d^{\,\downarrow{M_{2}}}\right)^{\,\downarrow{\mathcal{P}_{\\!f\\!i\\!n}}}(T_{1},T_{2})\leq
d^{\,\downarrow{\mathcal{P}_{\\!f\\!i\\!n}M_{2}}}(T_{1},T_{2})$

which proves equality.

###  P.4. Lifting of Natural Transformations and Monads

######  $\circlearrowleft$ Proposition 4.1 _(Lifting of a Natural
Transformation)_.

Let $F$, $G$ be endofunctors on $\mathbf{Set}$ with evaluation functions
$ev_{F}$, $ev_{G}$ and $\lambda\colon F\Rightarrow G$ be a natural
transformation. Then the following holds for all pseudometric spaces $(X,d)$.
For the Kantorovich lifting:

  1. (1)

If $ev_{G}\circ\lambda_{[0,\top]}\leq ev_{F}$ then
$d^{\,\uparrow{G}}\circ(\lambda_{X}\times\lambda_{X})\leq d^{\,\uparrow{F}}$,
i.e. $\lambda_{X}$ is nonexpansive.

  2. (2)

If $ev_{G}\circ\lambda_{[0,\top]}=ev_{F}$ then
$d^{\,\uparrow{G}}\circ(\lambda_{X}\times\lambda_{X})=d^{\,\uparrow{F}}$, i.e.
$\lambda_{X}$ is an isometry.

while for the Wasserstein lifting

  1. (3)

If $ev_{G}\circ\lambda_{[0,\top]}\leq ev_{F}$ then
$d^{\,\downarrow{G}}\circ(\lambda_{X}\times\lambda_{X})\leq
d^{\,\downarrow{F}}$, i.e. $\lambda_{X}$ is nonexpansive.

  2. (4)

If $ev_{G}\circ\lambda_{[0,\top]}=ev_{F}$ and the Kantorovich Rubinstein
duality holds for $F$, i.e. $d^{\,\uparrow{F}}=d^{\,\downarrow{F}}$, then
$d^{\,\downarrow{G}}\circ(\lambda_{X}\times\lambda_{X})=d^{\,\downarrow{F}}$,
i.e. $\lambda_{X}$ is an isometry.

######  Proof P.14.

Let $t_{1},t_{2}\in FX$.

  1. (1)

By naturality of $\lambda$ and $ev_{G}\circ\lambda_{[0,\top]}\leq ev_{F}$ we
obtain for every $f\colon X\to[0,\top]$:

$\displaystyle\widetilde{G}f\circ\lambda_{X}=ev_{G}\circ
Gf\circ\lambda_{X}=ev_{G}\circ\lambda_{[0,\top]}\circ Ff\leq ev_{F}\circ
Ff=\widetilde{F}f\,.$ (10)

Using this we compute

$\displaystyle
d^{\,\uparrow{G}}\left(\lambda_{X}(t_{1}),\lambda_{X}(t_{2})\right)=\sup\left\\{d_{e}\left(\widetilde{G}f\big{(}\lambda_{X}(t_{1})\big{)},\widetilde{G}f\big{(}\lambda_{X}(t_{2})\big{)}\right)\,\middle|\,f\colon(X,d)\raisebox{-1.5pt}{$\,\mathop{\overset{1}{\to}}\,$}([0,\top],d_{e})\right\\}$
$\displaystyle\quad\leq\sup\left\\{d_{e}\left(\widetilde{F}f(t_{1}),\widetilde{F}f(t_{2})\right)\,\middle|\,f\colon(X,d)\raisebox{-1.5pt}{$\,\mathop{\overset{1}{\to}}\,$}([0,\top],d_{e})\right\\}=d^{\,\uparrow{F}}(t_{1},t_{2})\,.$
(11)

  2. (2)

We just have to replace the inequality by equality in (10) and (11).

  3. (3)

Naturality of $\lambda$ yields the following equations, where $\pi_{i}\colon
X\times X\to X$ are the projections of the product and $d\colon X\times
X\to[0,\top]$ a pseudometric on $X$.

$\displaystyle\lambda_{X}\circ F\pi_{i}$
$\displaystyle=G\pi_{i}\circ\lambda_{X\times X}$ (12)
$\displaystyle\lambda_{[0,\top]}\circ Fd$
$\displaystyle=Gd\circ\lambda_{X\times X}$ (13)

Using (12), we can see that $\lambda_{X\times X}$ maps every coupling $t$ of
$t_{1}$ and $t_{2}$ to a coupling $\lambda_{X\times X}(t)$ of
$\lambda_{X}(t_{1})$ and $\lambda_{X}(t_{2})$ because
$G\pi_{i}(\lambda_{X\times
X}(t))=\lambda_{X}(F\pi_{i}(t))=\lambda_{X}(t_{i})$. Moreover, by our
requirement we obtain

$\displaystyle\widetilde{G}d(\lambda_{X\times X}(t))=ev_{G}\circ
Gd\circ\lambda_{X\times X}(t)$
$\displaystyle=ev_{G}\circ\lambda_{[0,\top]}\circ Fd(t)\leq ev_{F}\circ
Fd(t)=\widetilde{F}d(t)$

With these preparations at hand we can finally see that

$\displaystyle d^{\,\downarrow{G}}(\lambda_{X}(t_{1}),\lambda_{X}(t_{2}))$
$\displaystyle=\inf\left\\{\widetilde{G}d(t^{\prime})\mid
t^{\prime}\in\Gamma_{G}\big{(}\lambda_{X}(t_{1}),\lambda_{X}(t_{2})\big{)}\right\\}$
$\displaystyle\leq\inf\left\\{\widetilde{G}d(\lambda_{X\times X}(t))\mid
t\in\Gamma_{F}(t_{1},t_{2})\right\\}$
$\displaystyle\leq\inf\left\\{\widetilde{F}d(t)\mid
t\in\Gamma_{F}(t_{1},t_{2})\right\\}=d^{\,\downarrow{F}}(t_{1},t_{2})\,.$

  4. (4)

Using the previous two results and the fact that Wasserstein is an upper bound
yields:

$\displaystyle
d^{\,\uparrow{F}}=d^{\,\uparrow{G}}\circ(\lambda_{X}\times\lambda_{X})\leq
d^{\,\downarrow{G}}\circ(\lambda_{X}\times\lambda_{X})\leq
d^{\,\downarrow{F}}$

and since $d^{\,\uparrow{F}}=d^{\,\downarrow{F}}$ all these inequalities are
equalities.

######  $\circlearrowleft$ Corollary 4.2 _(Lifting of a Monad)_.

Let $(T,\eta,\mu)$ be a $\mathbf{Set}$-monad and $ev_{T}$ an evaluation
function for $T$. Then the following holds.

  1. (1)

If $ev_{T}\circ\eta_{[0,\top]}\leq\mathrm{id}_{[0,\top]}$ then $\eta$ is
nonexpansive for both liftings. Hence we obtain the unit
$\overline{\eta}\colon\overline{\mathrm{Id}}\Rightarrow\overline{T}$ in
$\mathbf{PMet}$.

  2. (2)

If $ev_{T}\circ\eta_{[0,\top]}=\mathrm{id}_{[0,\top]}$ then $\eta$ is an
isometry for both liftings.

  3. (3)

Let $d^{T}\in\\{d^{\,\uparrow{T}},d^{\,\downarrow{T}}\\}$. If
$ev_{T}\circ\mu_{[0,\top]}\leq ev_{T}\circ Tev_{T}$ and compositionality holds
for $TT$, i.e. $(d^{T})^{T}=d^{TT}$, then $\mu$ is nonexpansive, i.e.
$d^{T}\circ(\mu_{X}\times\mu_{X})\leq(d^{T})^{T}$. This yields the
multiplication
$\overline{\mu}\colon\overline{T}\,\overline{T}\Rightarrow\overline{T}$ in
$\mathbf{PMet}$.

######  Proof P.15.

This is an immediate consequence of 4.1. For the unit take $F=\mathrm{Id}$
with evaluation function $ev_{F}=\mathrm{id}_{[0,\top]}$, hence
$d^{\,\uparrow{F}}=d^{\,\downarrow{F}}=d$ and $G=T$, $ev_{G}=ev_{T}$,
$\lambda=\eta\colon\mathrm{Id}\Rightarrow T$. For the multiplication take
$F=TT$, $G=T$, $ev_{F}=ev_{TT}=ev_{T}\circ Tev_{T}$, $ev_{G}=ev_{T}$ and
$\lambda=\mu$.

###  P.5. Trace Metrics in Eilenberg-Moore

######  $\circlearrowleft$ Corollary 5.2 _(Lifting of an $\mathcal{EM}$-law)_.

Let $F,G$ be weak pullback preserving endofunctors on $\mathbf{Set}$ with
well-behaved evaluation functions $ev_{F}$, $ev_{G}$ and $\lambda\colon
FG\Rightarrow GF$ be an $\mathcal{EM}$-law. If the evaluation functions
satisfy $ev_{G}\circ Gev_{F}\circ\lambda_{[0,\top]}\leq ev_{F}\circ Fev_{G}$
and compositionality holds for $FG$, then $\lambda$ is nonexpansive and hence
$\overline{\lambda}\colon\overline{F}\,\overline{G}\Rightarrow\overline{G}\,\overline{F}$
is also an $\mathcal{EM}$-law.

######  Proof P.16.

For $FG$ we take the evaluation function $ev_{FG}=ev_{F}\circ Fev_{G}$ and for
$GF$ the evaluation function $ev_{GF}=ev_{G}\circ Gev_{F}$. We have

$\displaystyle ev_{GF}\circ\lambda_{[0,\top]}=ev_{G}\circ
Gev_{F}\circ\lambda_{[0,\top]}\leq ev_{F}\circ Fev_{G}=ev_{FG}$

By 4.1 we know that
$d^{\,\downarrow{GF}}\circ(\lambda_{X}\times\lambda_{X})\leq
d^{\,\downarrow{FG}}$ and by subsubsection P.3.1.2 we have
$(d^{\,\downarrow{F}})^{\,\downarrow{G}}\leq d^{\,\downarrow{GF}}$. Plugging
everything together we see that

$\displaystyle(d^{\,\downarrow{F}})^{\,\downarrow{G}}\circ(\lambda_{X}\times\lambda_{X})\leq
d^{\,\downarrow{GF}}\circ(\lambda_{X}\times\lambda_{X})\leq
d^{\,\downarrow{FG}}=(d^{\,\downarrow{G}})^{\,\downarrow{F}}$

which is the desired nonexpansiveness.

######  $\circlearrowleft$ Example 5.3 _( $\mathcal{EM}$-law for
Nondeterministic Automata)_.

Let $(\mathcal{P}_{\\!f\\!i\\!n},\eta,\mu)$ be the finite powerset monad from
4.3. The $\mathcal{EM}$-law
$\lambda\colon\mathcal{P}_{\\!f\\!i\\!n}(2\times\\_^{A})\Rightarrow
2\times\mathcal{P}_{\\!f\\!i\\!n}(\\_)^{A}$ is defined, for any set $X$, as

$\displaystyle\lambda_{X}(S)=\big{(}o,\lambda a\in
A.\left\\{s^{\prime}(a)\mid(o^{\prime},s^{\prime})\in S\right\\}\big{)},\ \
\text{where}\ \ o=\begin{cases}1&\exists s^{\prime}\in X^{A}.(1,s^{\prime})\in
S\\\ 0&\text{else}\end{cases}\,.$

This is exactly the one exploited for the standard powerset construction from
automata theory [SBBR13]. Indeed, for a nondeterministic automaton $c\colon
X\to 2\times\mathcal{P}_{\\!f\\!i\\!n}(X)^{A}$, the map
$[\\![\,-\,]\\!]\circ\eta_{X}$ assigns to each state its accepted language.
5.2 ensures that it is nonexpansive (see Appendix P for a detailed proof).

######  Proof P.17.

The functors are a composition of known endofunctors. We have
$F=\mathcal{P}_{\\!f\\!i\\!n}(2\times\\_^{A})=\mathcal{P}_{\\!f\\!i\\!n}M_{2}$,
and $G=2\times\mathcal{P}_{\\!f\\!i\\!n}^{A}=M_{2}\mathcal{P}_{\\!f\\!i\\!n}$
where $M_{2}:=M(2,\\_)$ is the endofunctor obtained from the machine bifunctor
$M$ by fixing its first component to $2$. The evaluation functions are
$ev_{F}\colon\mathcal{P}_{\\!f\\!i\\!n}(2\times[0,1]^{A})\to[0,1]$ where for
$S\in\mathcal{P}_{\\!f\\!i\\!n}(2\times[0,1]^{A})$

$\displaystyle ev_{F}(S)$
$\displaystyle=ev_{\mathcal{P}_{\\!f\\!i\\!n}}\circ\mathcal{P}_{\\!f\\!i\\!n}ev_{M_{2}}(S)=\max\left\\{ev_{M_{2}}(o,s)\mid(o,s)\in
S\right\\}$ $\displaystyle=\max\left\\{c\cdot\max_{a\in A}s(a)\mid(o,s)\in
S\right\\}=c\cdot\max_{(o,s)\in S}\max_{a\in A}s(a)$

and $ev_{G}\colon 2\times(\mathcal{P}_{\\!f\\!i\\!n}[0,1])^{A}\to[0,1]$ where
for $(o,s)\in 2\times(\mathcal{P}_{\\!f\\!i\\!n}X)^{A}$

$\displaystyle ev_{G}(o,s)=ev_{M_{2}}\circ
M_{2}(ev_{\mathcal{P}_{\\!f\\!i\\!n}})(o,s)$
$\displaystyle=ev_{M_{2}}\big{(}o,\lambda a.\max s(a)\big{)}=c\cdot\max_{a\in
A}\max s(a)\,.$

As we have seen in 3.6 we have compositionality for $F$. We want to apply
4.1.3 to show nonexpansiveness. For this we have to check that the inequality
$ev_{G}\circ\lambda_{[0,1]}\leq ev_{F}$ holds. Indeed we have:

$\displaystyle ev_{G}\circ\lambda_{[0,1]}(S)=c\cdot\max_{a\in
A}\max\left\\{s(a)\mid(o,s)\in S\right\\}=c\cdot\max_{a\in A}\max_{(o,s)\in
S}s(a)=ev_{F}(S)$

which concludes the proof.

######  $\circlearrowleft$ Example 5.4 _( $\mathcal{EM}$-law for Probabilistic
Automata)_.

Let $(\mathcal{D},\eta,\mu)$ be the distribution monad from 4.4 and $M$ be the
machine bifunctor from 3.5. There is a known [SBBR13] $\mathcal{EM}$-law
$\lambda\colon\mathcal{D}([0,1]\times\\_^{A})\Rightarrow[0,1]\times\mathcal{D}^{A}$
given by the assignment

$\displaystyle\lambda_{X}(P)=\left(\sum_{r\in[0,1]}r\cdot P(r,X^{A}),\lambda
a\in A.\lambda x\in X.\sum_{{s\in
X^{A},\,s(a)=x}}\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!P([0,1],s)\right)$

Also this $\mathcal{EM}$-law is nonexpansive, as shown in Appendix P.

######  Proof P.18.

We first quickly check that the definition is sound, i.e. that we get a
probability distribution for each $a\in A$:

$\displaystyle\sum_{x\in X}\left(\sum_{{s\in X^{A},s(a)=x}}P([0,1],s)\right)$
$\displaystyle=\sum_{s\in X^{A}}P([0,1],s)=1$

Having verified this, we now want to show nonexpansiveness. The involved
bifunctors $F,G$ are given by the assignments $F(B,X)=\mathcal{D}(B\times
X^{A})$ and $G(B,X)=B\times(\mathcal{D}X)^{A}$ and arise from composition of
the distribution functor, the identity functor and the machine bifunctor: We
have $F=\mathcal{D}\circ M$ and $G=M\circ(\mathrm{Id}\times\mathcal{D})$.

Since all of these functors have optimal couplings, we have compositionality
and the canonical evaluation functions for the composed functors are

$\displaystyle
ev_{F}:=ev_{\mathcal{D}}\circ\mathcal{D}ev_{M}\colon\mathcal{D}([0,1]\times[0,1]^{A})\to[0,1]\quad\text{and}$
$\displaystyle ev_{G}:=ev_{M}\circ
M(\mathrm{id}_{[0,1]},ev_{\mathcal{D}})\colon[0,1]\times(\mathcal{D}X)^{A}\to[0,1]\,.$

We will now define a function
$\Lambda_{X}\colon\mathcal{D}([0,1]^{2}\times(X\times
X)^{A})\to[0,1]^{2}\times(\mathcal{D}(X\times X))^{A}$ which transfers
$F$-couplings to suitable $G$-couplings in the following sense. For any
$P_{1},P_{2}\in\mathcal{D}([0,1]\times X^{A})$ and any
$P\in\Gamma_{F}(P_{1},P_{2})\subseteq\mathcal{D}([0,1]\times[0,1]\times(X\times
X)^{A})$ the function $\Lambda_{X}$ has to satisfy the following two
requirements

$\displaystyle\Lambda_{X}(P)\in\Gamma_{G}\big{(}\lambda_{X}(P_{1}),\lambda_{X}(P_{2})\big{)}$
(14)
$\displaystyle\widetilde{G}(d_{B},d)\big{(}\Lambda_{X}(P)\big{)}\leq\widetilde{F}(d_{B},d)(P)$
(15)

because then we have

$\displaystyle(d_{B},d)^{\,\downarrow{G}}(\lambda_{X}(P_{1}),\lambda_{X}(P_{2}))$
$\displaystyle=\inf\left\\{\widetilde{G}(d_{B},d)(P^{\prime})\mid
P^{\prime}\in\Gamma_{G}\big{(}\lambda_{X}(P_{1}),\lambda_{X}(P_{2})\big{)}\right\\}$
$\displaystyle\leq\inf\left\\{\widetilde{G}(d_{B},d)\big{(}\Lambda_{X}(P)\big{)}\mid
P\in\Gamma_{F}(P_{1},P_{2})\right\\}$
$\displaystyle\leq\inf\left\\{\widetilde{F}(d_{B},d)(P)\mid
t\in\Gamma_{F}(P_{1},P_{2})\right\\}=(d_{B},d)^{\,\downarrow{F}}(P_{1},P_{2})$

which, due to compositionality, proves the desired nonexpansiveness of
$\lambda_{X}$. So let us now define $\Lambda_{X}$ and prove that it satisfies
the above requirements: For any set $X$ and any
$P\in\mathcal{D}([0,1]\times[0,1]\times(X\times X)^{A})$ we define
$\Lambda_{X}(P)=(\mathfrak{o}_{1}(P),\mathfrak{o}_{2}(P),\mathfrak{s}(P))$
where

$\displaystyle\mathfrak{o}_{1}(P)=\sum_{r\in[0,1]}r\cdot P(r,[0,1],(X\times
X)^{A}),\quad\mathfrak{o}_{2}(P)=\sum_{r\in[0,1]}r\cdot P([0,1],r,(X\times
X)^{A})\quad\text{and}$ $\displaystyle\mathfrak{s}(P)\colon
A\to\mathcal{D}(X\times
X),\quad\mathfrak{s}(P)(a)(x,y)=\\!\\!\\!\\!\sum_{{s\in(X\times X)^{A},\
s(a)=(x,y)}}\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!P([0,1]^{2},s)\,.$

Observe that this is completely analogous to the definition of the components
$\lambda_{X}$ of our distributive law where for any
$Q\in\mathcal{D}([0,1]\times X^{A})$ we have
$\lambda_{X}(Q)=(\mathfrak{o}^{\prime}(Q),\mathfrak{s}^{\prime}(Q))$ with

$\displaystyle\mathfrak{o}^{\prime}(Q)=\sum_{r\in[0,1]}\\!r\cdot
Q(r,X^{A}),\quad\text{and}\quad\mathfrak{s}^{\prime}(Q)\colon
A\to\mathcal{D}X,\ \ \mathfrak{s}^{\prime}(Q)(a)(x)=\\!\\!\\!\\!\sum_{{s\in
X^{A},s(a)=x}}\\!\\!\\!\\!\\!\\!\\!Q([0,1],s)\,.$

Let us now show that the above definition of $\Lambda_{X}$ satisfies our
requirements. We thus assume from here on that $P\in\Gamma_{F}(P_{1},P_{2})$
for some arbitrary $P_{1},P_{2}\in\mathcal{D}([0,1]\times X^{A})$ i.e. we know
$F(\pi_{i},\pi_{i})=P_{i}$. In order to show (14), we have to prove that the
equation

$\displaystyle
G(\pi_{i},\pi_{i})\big{(}\Lambda_{X}(P)\big{)}=\lambda_{X}(P_{i})$ (16)

holds. The left hand side of this equation evaluates to

$\displaystyle G(\pi_{i},\pi_{i})\big{(}\Lambda_{X}(P)\big{)}$
$\displaystyle=\big{(}\pi_{i}\times(\mathcal{D}\pi_{i})^{A}\big{)}\left(\mathfrak{o}_{1}(P),\mathfrak{o}_{2}(P),\mathfrak{s}(P)\right)=\big{(}\mathfrak{o}_{i}(P),\mathcal{D}\pi_{i}\circ\mathfrak{s}(P)\big{)}$
(17)

and since $F(\pi_{i},\pi_{i})=P_{i}$ the right hand side of (16) evaluates to

$\displaystyle\lambda_{X}(P_{i})=\lambda_{X}\big{(}F(\pi_{i},\pi_{i})(P)\big{)}$
$\displaystyle=\Big{(}\mathfrak{o}^{\prime}\left(\mathcal{D}(\pi_{i}\times\pi_{i}^{A})(P)\right),\mathfrak{s}^{\prime}\left(\mathcal{D}(\pi_{i}\times\pi_{i}^{A})(P)\right)\Big{)}\,.$
(18)

In order to prove (16) we will thus have to show that
$\mathfrak{o}^{\prime}\left(\mathcal{D}(\pi_{i}\times\pi_{i}^{A})(P)\right)=\mathfrak{o}_{i}(P)$
and also
$\mathfrak{s}^{\prime}\left(\mathcal{D}(\pi_{i}\times\pi_{i}^{A})(P)\right)=\mathcal{D}\pi_{i}\circ\mathfrak{s}(P)$
holds. We first compute

$\displaystyle\mathfrak{o}^{\prime}\left(\mathcal{D}(\pi_{i}\times\pi_{i}^{A})(P)\right)=\sum_{r\in[0,1]}r\cdot\mathcal{D}(\pi_{i}\times\pi_{i}^{A})(P)(r,X^{A})$
$\displaystyle=\sum_{r\in[0,1]}r\cdot\left(P\circ(\pi_{i}\times\pi_{i}^{A})^{-1}[\left\\{r\right\\}\times
X^{A}]\right)$ $\displaystyle=\sum_{r\in[0,1]}r\cdot
P\left(\left\\{(o_{1},o_{2},s)\in\mathcal{D}([0,1]^{2}\times(X\times X)^{A})\
\middle|\ \pi_{i}\times\pi_{i}^{A}(o_{1},o_{2},s)\in\left\\{r\right\\}\times
X^{A}\right\\}\right)$ $\displaystyle=\sum_{r\in[0,1]}r\cdot
P\left(\left\\{(o_{1},o_{2},s)\in\mathcal{D}([0,1]^{2}\times(X\times X)^{A})\
\middle|\ o_{i}=r\right\\}\right)=\mathfrak{o}_{i}(P)$

showing that indeed the first components of the tuples in (17) and (18) are
the same. For the second components we have

$\displaystyle\mathfrak{s}^{\prime}\left(\mathcal{D}(\pi_{i}\times\pi_{i}^{A})(P)\right)(a)(x)=\sum_{\left\\{s\in
X^{A},s(a)=x\right\\}}\mathcal{D}(\pi_{i}\times\pi_{i}^{A})(P)([0,1],s)$
$\displaystyle=\sum_{{s\in
X^{A},s(a)=x}}\\!\\!\\!\\!\\!P\left(\left\\{(o_{1},o_{2},s^{\prime})\in\mathcal{D}([0,1]^{2}\times(X^{2})^{A})\
\middle|\
\pi_{i}\times\pi_{i}^{A}(o_{1},o_{2},s^{\prime})\in[0,1]\times\left\\{s\right\\}\right\\}\right)$
$\displaystyle=\sum_{{s\in
X^{A},s(a)=x}}\\!\\!\\!\\!\\!P\left(\left\\{(o_{1},o_{2},s^{\prime})\in\mathcal{D}([0,1]^{2}\times(X^{2})^{A})\
\middle|\ \pi_{i}\circ s^{\prime}=s\right\\}\right)$
$\displaystyle=\sum_{{s^{\prime}\in(X\times X)^{A},\pi_{i}\circ
s^{\prime}(a)=x}}P([0,1]^{2},s^{\prime})$

and

$\displaystyle(\mathcal{D}\pi_{i}\circ\mathfrak{s}(P))(a)(x)$
$\displaystyle=\mathfrak{s}(P)(a)\circ\pi_{i}^{-1}[\left\\{x\right\\}]=\mathfrak{s}(P)(a)\left(\left\\{y\in
X\times X\mid\pi_{i}(y)=x\right\\}\right)$ $\displaystyle=\sum_{{s\in(X\times
X)^{A},\pi_{i}\circ s(a)=x}}\\!\\!\\!\\!\\!\\!\\!P([0,1]^{2},s)$ (19)

which shows that also the second components of (17) and (18) coincide.
Therefore (16) holds i.e. we have proved
$\Lambda_{X}(P)\in\Gamma_{G}(\lambda_{X}(P_{1}),\lambda_{X}(P_{2}))$ as
claimed in (14). We now show (15). For the left hand side of that inequality
we compute

$\displaystyle\widetilde{G}(d_{B},d)\big{(}\Lambda_{X}(P)\big{)}$
$\displaystyle=\big{(}ev_{G}\circ
G(d_{B},d)\big{)}\big{(}\lambda_{X}(P)\big{)}=ev_{G}\Big{(}G(d_{B},d)\big{(}\Lambda_{X}(P)\big{)}\Big{)}$
$\displaystyle=ev_{G}\Big{(}\big{(}d_{B}\times(\mathcal{D}d)^{A}\big{)}\big{(}\mathfrak{o}_{1}(P),\mathfrak{o}_{2}(P),\mathfrak{s}(P)\big{)}\Big{)}$
$\displaystyle=ev_{G}\Big{(}d_{B}\big{(}\mathfrak{o}_{1}(P),\mathfrak{o}_{2}(P)\big{)},\lambda
a.\mathcal{D}d\big{(}\mathfrak{s}(P)(a)\big{)}\Big{)}$
$\displaystyle=\Big{(}ev_{M}\circ
M\left(\mathrm{id}_{[0,1]},ev_{\mathcal{D}}\right)\Big{)}\Big{(}d_{B}\big{(}\mathfrak{o}_{1}(P),\mathfrak{o}_{2}(P)\big{)},\lambda
a.\mathcal{D}d\big{(}\mathfrak{s}(P)(a)\big{)}\Big{)}$
$\displaystyle=ev_{M}\left(M\left(\mathrm{id}_{[0,1]},ev_{\mathcal{D}}\right)\Big{(}d_{B}\big{(}\mathfrak{o}_{1}(P),\mathfrak{o}_{2}(P)\big{)},\lambda
a.\mathcal{D}d\big{(}\mathfrak{s}(P)(a)\big{)}\Big{)}\right)$
$\displaystyle=ev_{M}\Bigg{(}d_{B}\big{(}\mathfrak{o}_{1}(P),\mathfrak{o}_{2}(P)\big{)},ev_{\mathcal{D}}^{A}\Big{(}\lambda
a.\mathcal{D}d\big{(}\mathfrak{s}(P)(a)\big{)}\Big{)}\Bigg{)}$
$\displaystyle=ev_{M}\Bigg{(}d_{B}\big{(}\mathfrak{o}_{1}(P),\mathfrak{o}_{2}(P)\big{)},\lambda
a.ev_{\mathcal{D}}\Big{(}\mathcal{D}d\big{(}\mathfrak{s}(P)(a)\big{)}\Big{)}\Bigg{)}$
$\displaystyle=c_{1}d_{B}\big{(}\mathfrak{o}_{1}(P),\mathfrak{o}_{2}(P)\big{)}+\frac{c_{2}}{|A|}\sum_{a\in
A}ev_{\mathcal{D}}\Big{(}\mathcal{D}d\big{(}\mathfrak{s}(P)(a)\big{)}\Big{)}$
(20)

and since for each $a\in A$ we have

$\displaystyle
ev_{\mathcal{D}}\Big{(}\mathcal{D}d\big{(}\mathfrak{s}(P)(a)\big{)}\Big{)}$
$\displaystyle=\sum_{r\in[0,1]}r\cdot\mathfrak{s}(P)(a)\big{(}d^{-1}[\left\\{r\right\\}]\big{)}=\sum_{(x,y)\in
X^{2}}d(x,y)\cdot\mathfrak{s}(P)(a)(x,y)$ $\displaystyle=\sum_{(x,y)\in
X^{2}}d(x,y)\cdot\left(\sum_{{s\in(X\times X)^{A},\
s(a)=(x,y)}}\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!P([0,1]^{2},s)\right)$
$\displaystyle=\sum_{s\in(X\times X)^{A}}d\big{(}s(a)\big{)}\cdot
P([0,1]^{2},s)$

we may continue (20) as follows:

$\displaystyle\widetilde{G}(d_{B},d)\big{(}\Lambda_{X}(P)\big{)}$
$\displaystyle=c_{1}d_{B}\big{(}\mathfrak{o}_{1}(P),\mathfrak{o}_{2}(P)\big{)}+\frac{c_{2}}{|A|}\sum_{a\in
A}\sum_{s\in(X\times X)^{A}}d\big{(}s(a)\big{)}\cdot P([0,1]^{2},s)\,.$ (21)

For the right hand side of (15) we have

$\displaystyle\widetilde{F}$
$\displaystyle(d_{B},d)(P)=\big{(}ev_{F}\circ{F}(d_{B},d)\big{)}(P)=\Big{(}\big{(}ev_{\mathcal{D}}\circ\mathcal{D}ev_{M}\big{)}\circ\mathcal{D}\big{(}M(d_{B},d)\big{)}\Big{)}(P)$
$\displaystyle=ev_{\mathcal{D}}\Bigg{(}\mathcal{D}ev_{M}\Big{(}\mathcal{D}\big{(}M(d_{B},d)\big{)}(P)\Big{)}\Bigg{)}=ev_{\mathcal{D}}\Bigg{(}\mathcal{D}ev_{M}\Big{(}\mathcal{D}\big{(}d_{B}\times
d^{A}\big{)}(P)\Big{)}\Bigg{)}$
$\displaystyle=ev_{\mathcal{D}}\Bigg{(}\Big{(}\mathcal{D}\big{(}d_{B}\times
d^{A}\big{)}(P)\Big{)}\circ
ev_{M}^{-1}\Bigg{)}=\sum_{r\in[0,1]}r\cdot\Big{(}\mathcal{D}\big{(}d_{B}\times
d^{A}\big{)}(P)\Big{)}\big{(}ev_{M}^{-1}[\left\\{r\right\\}]\big{)}$
$\displaystyle=\sum_{(o,s^{\prime})\in[0,1]\times[0,1]^{A}}\\!\\!\\!\\!ev_{M}(o,s^{\prime})\cdot\Big{(}\mathcal{D}\big{(}d_{B}\times
d^{A}\big{)}(P)\Big{)}(o,s^{\prime})$
$\displaystyle=\sum_{(o,s^{\prime})\in[0,1]\times[0,1]^{A}}\\!\\!\\!\\!ev_{M}(o,s^{\prime})\cdot
P\Big{(}\big{(}d_{B}\times
d^{A}\big{)}^{-1}\big{[}\left\\{(o,s^{\prime})\right\\}\big{]}\Big{)}$
$\displaystyle=\sum_{(o_{1},o_{2},s)\in[0,1]^{2}\times(X\times
X)^{A}}ev_{M}\Big{(}\big{(}d_{B}\times d^{A}\big{)}(o_{1},o_{2},s)\Big{)}\cdot
P(o_{1},o_{2},s)$
$\displaystyle=\sum_{(o_{1},o_{2},s)\in[0,1]^{2}\times(X\times
X)^{A}}ev_{M}\Big{(}d_{B}(o_{1},o_{2}),\lambda
a.d\big{(}s(a)\big{)}\Big{)}\cdot P(o_{1},o_{2},s)$
$\displaystyle=\sum_{(o_{1},o_{2},s)\in[0,1]^{2}\times(X\times
X)^{A}}\left(c_{1}d_{B}(o_{1},o_{2})+\frac{c_{2}}{|A|}\sum_{a\in
A}d\big{(}s(a)\big{)}\right)\cdot P(o_{1},o_{2},s)$
$\displaystyle=c_{1}\mathfrak{o}(P)+\frac{c_{2}}{|A|}\sum_{s\in(X\times
X)^{A}}\sum_{a\in A}d\big{(}s(a)\big{)}\cdot P([0,1]^{2},s)$ (22)

with

$\displaystyle\mathfrak{o}(P)=\sum_{(o_{1},o_{2})\in[0,1]^{2}}\\!\\!d_{B}(o_{1},o_{2})\cdot
P\big{(}o_{1},o_{2},(X\times X)^{A}\big{)}\,.$

Comparing (21) and (22) we see that in order to obtain inequality (15) we just
have to show

$\displaystyle
d_{B}\big{(}\mathfrak{o}_{1}(P),\mathfrak{o}_{2}(P)\big{)}\leq\mathfrak{o}(P)$

This is easily done using the fact that $d_{B}=d_{e}$ is the euclidean metric
and the triangle inequality:

$\displaystyle d_{B}\big{(}\mathfrak{o}_{1}(P),$
$\displaystyle\mathfrak{o}_{2}(P)\big{)}=$
$\displaystyle=\left|\sum_{r_{1}\in[0,1]}r_{1}\cdot
P\big{(}r_{1},[0,1],(X\times X)^{A}\big{)}-\sum_{r_{2}\in[0,1]}r_{2}\cdot
P\big{(}[0,1],r_{2},(X\times X)^{A}\big{)}\right|$
$\displaystyle=\left|\sum_{r_{1},r_{2}\in[0,1]}r_{1}\cdot
P\big{(}r_{1},r_{2},(X\times
X)^{A}\big{)}-\sum_{r_{1},r_{2}\in[0,1]}r_{2}\cdot
P\big{(}r_{1},r_{2},(X\times X)^{A}\big{)}\right|$
$\displaystyle=\left|\sum_{r_{1},r_{2}\in[0,1]}(r_{1}-r_{2})\cdot
P\big{(}r_{1},r_{2},(X\times X)^{A}\big{)}\right|$
$\displaystyle\leq\sum_{r_{1},r_{2}\in[0,1]}\left|(r_{1}-r_{2})\cdot
P\big{(}r_{1},r_{2},(X\times X)^{A}\big{)}\right|$
$\displaystyle=\sum_{r_{1},r_{2}\in[0,1]}|r_{1}-r_{2}|\cdot
P\big{(}r_{1},r_{2},(X\times X)^{A}\big{)}=\mathfrak{o}(P)\,.$

We have thus also completed the proof of our second claim: the inequality
(15).