Proposition [efr-002C]

Let T: \mathsf {Set} \to \mathsf {Set} be a functor which preserves weak pullbacks. Then the assignment \bar {T}(R: A \nrightarrow B) = im(T(R)) \subseteq T(A) \times T(B) defines a functor \mathsf {\mathbb Rel} \to \mathsf {\mathbb Rel} (which just acts as T on the objects).

Proof

Recall that there is a functor \mathsf {\mathbb Span}(\mathsf {Set}) \to \mathsf {\mathbb Rel}, which carries a span A \leftarrow R \to B to its image inside A \times B. Observe that two spans are identified under this mapping precisely if there exist span maps (not necessarily inverses) between them in both directions.

It follows that, given two composable relations R: A \nrightarrow B, R': B \nrightarrow C, the composite of \bar {T}(R) and \bar {T}(R') can be computed by taking the pullback T(R) \times _{T(B)} T(R'), then taking its image inside T(A) \times T(C). But since T preserves weak limits, the map from T(R \times _B R') to this pullback admits a section, and hence they go to the same relation. This proves that \bar {T} preserves composition (the claim about identities is straightforward).

Context

Review of coalgebraic modal logic [efr-002A]

Definition Weak limits [efr-002B]

Let X: I \to \mathcal {C} be a diagram. A cone A \xrightarrow {f_i} X_i is said to be a weak limit if, for any other cone B, there exists a map B \to A (but this map is not necessarily unique).

Observe that, if an actual limit L exists, a cone is a weak limit if and only if the induced map A \to L admits a section. It follows that any functor which preserves the limit of some diagram also preserves the weak limits (in the sense that they are carried to another weak limit).

Proposition [efr-002C]

Let T: \mathsf {Set} \to \mathsf {Set} be a functor which preserves weak pullbacks. Then the assignment \bar {T}(R: A \nrightarrow B) = im(T(R)) \subseteq T(A) \times T(B) defines a functor \mathsf {\mathbb Rel} \to \mathsf {\mathbb Rel} (which just acts as T on the objects).

Proof

Recall that there is a functor \mathsf {\mathbb Span}(\mathsf {Set}) \to \mathsf {\mathbb Rel}, which carries a span A \leftarrow R \to B to its image inside A \times B. Observe that two spans are identified under this mapping precisely if there exist span maps (not necessarily inverses) between them in both directions.

It follows that, given two composable relations R: A \nrightarrow B, R': B \nrightarrow C, the composite of \bar {T}(R) and \bar {T}(R') can be computed by taking the pullback T(R) \times _{T(B)} T(R'), then taking its image inside T(A) \times T(C). But since T preserves weak limits, the map from T(R \times _B R') to this pullback admits a section, and hence they go to the same relation. This proves that \bar {T} preserves composition (the claim about identities is straightforward).

The basic idea is the following: suppose we have a system of formula L we know how to interpret in coalgebras. This interpretation is a relation \vDash : L \nrightarrow X, given some coalgebra \xi : X \to TX. Now, given an element \alpha \in TL, we can define its interpretation in TX simply using the lifting \bar {T}. And finally we can take the inverse image of the given subset of TX under \xi to give a subset of X

For example, let T(X) = A \times X, so that a coalgebra is a simple labeled transition system. Then we get a modal operator \nabla _a for each a. The meaning of \nabla _a(\phi )(x) is that \xi (x) = (a,x'), and \phi (x') holds.

If we let our basic language be Boolean logic, and our functor T is not too bad (for example, if it's finitary), we get a result called the Hennessy-Milner property: two states satisfy the same formulae of the logic precisely if they are bisimilar.

(It is not quite the same as saying formulas up to semantic equivalence are the same as bisimilarity classes---in the above example, we only get to ask about some finite prefix of the stream of outputs produced by x. But of course two streams are equal if all the prefixes agree).

Let \mathsf {Stone} denote the category of stone spaces, that is topological spaces which are compact, Hausdorff, and totally disconnected (meaning every connected component is a singleton). Then we have the following theorem, due to Stone

Theorem Stone duality [efr-002D]

If X is a Stone space, the set of clopen subsets is a Boolean algebra. Moreover, the functor \mathsf {Stone}^\mathrm {op} \to \mathsf {Bool} which carries a Stone space to its set of clopen subsets is an equivalence of categories.

Now suppose our behaviour is given by an endofunctor T: \mathsf {Stone} \to \mathsf {Stone}. Then we immediately get a corresponding functor T^\mathrm {op}: \mathsf {Bool} \to \mathsf {Bool}, and the category of T-coalgebras is dual to the category ot T^\mathrm {op}-algebras.

Hence, giving a space the structure of a T-coalgebra \xi : X \to TX is equivalent to giving its set of clopen subsets a T^\mathrm {op}-algebra structure T^\mathrm {op} B(X) \to B(X). This algebra structure can be interpreted as a (system of) modal operators---for example, if T(X) = A \times X, giving such a structure amounts to choosing maps B(A) \to B(X) and B(X) \to B(X), corresponding to the operations "will x produce an output a that satisfies statement \phi (a)?" and "will the next state after x satisfy \psi ?"

We would like to move this framework to the setting of categorical systems theory. Of course, we are hampered by two immediate problems: our systems are not, in general, coalgebras of functors, nor are they in general sets.

The opposite of \mathsf {FinStoch} [efr-0030]

Recall that (perhaps by definition, perhaps as a trivial theorem, depending on our choice of definition), there is a faithful functor \mathsf {FinStoch} \to \mathsf {Vect} carrying a set X to the vector space \mathbb {R}\langle X \rangle freely generated by X, and a stochastic map f: X \to Y to the map which takes the basis vector x \in X to the linear combination \sum _{y \in Y} y f(y|x). The essential image of this functor is, of course, the finite-dimensional vector spaces. The morphisms in the image are the stochastic matrices, which can be characterized as those that are positive (they carry vectors with positive coordinates to other such vectors) and preserve the constant 1 vector (note that neither of these properties are invariant under isomorphism of finite-dimensional vector space).

One way to think about this is that it proves \mathsf {FinStoch} is equivalent to the category of finite-dimensional, ordered, pointed vector spaces, where we assume that the chosen point must be positive in the order. (To see the inclusion is essentially surjective, note that given a vector space pointed by (a_1, \dots a_n), all those coordinates positive, it receives an isomorphism from the same spaces pointed by (1, \dots 1) given by the diagonal matrix with entries a_1, \dots a_n).

Now, let \mathsf {fdVect}^\leq denote the category of finite-dimensional ordered vector spaces. Then equipping a space V with a positive point is exactly choosing an order-preserving linear map \mathbb {R} \to V, so we have proven \mathsf {FinStoch} \simeq \mathsf {fdVect}^\leq _{ \mathbb {R} /}. Now we can compute \mathsf {FinStoch}^\mathrm {op} \simeq (\mathsf {fdVect}^\leq _{ \ RR/})^\mathrm {op} \cong (\mathsf {fdVect}^\leq )^\mathrm {op}_{ / \mathbb {R}} \cong \mathsf {fdVect}^\leq _{ / \mathbb {R}}, where the last isomorphism is via transposition (note that transposing a positive matrix yields a positive matrix).

This isomorphism merely describes the fact that stochastic maps \phi : X \to Y can also be described as linear maps f: \mathbb {R}\langle Y \rangle \to \mathbb {R}\langle X \rangle so that \sum _x f((a_y))_x = \sum _y a_y. This map interprets a vector as a function on Y, and carries it to the function on X which finds the expected value if y \in Y is distributed as \phi (x). The normalization condition merely says a constant function always has that constant as its expectation.

The self-duality of \mathsf {fdVect} does not generalize to infinite-dimensional vector spaces, so once we move beyond finite state spaces, this story will get somewhat more complicated. However, the basic idea that, to carry the tools of coalgebraic modal logic into the stochastic case, the sort of "predicate" we should consider is actually a function on the state space, will remain the central idea.

(Indeed, to consider the right notion of stochastic function between, for example, smooth manifolds, we will in any case want to use the tools of functional analysis to think of these in terms of transformation on integration operators, which is essentially this idea).

Another way to justify this idea is to note that \Omega = \{\bot ,\top \} is the subobject classifier for \mathsf {Fin} \subseteq \mathsf {FinStoch}. Hence if we want our notion of predicate to transform under stochastic maps, and include the logical predicates in the usual sense, we have to at least consider the stochastic maps X \to \Omega , which of course amount to functions X \to [0,1] in this case. But a positive linear map on functions is determined by what it does to functions like this, so whether we work only with these or all functions X \to \mathbb {R} is more or less a matter of taste.

Instead of having a logic consisting of the operations of Boolean algebra, augmented with extra operations described by T^\mathrm {op} B \to B, we have the operations of a vector space, augmented by some extra modal operations. The Markov structure of \mathsf {FinStoch}, or whichever category we work in, will give the vector space of functions an \mathbb {R}-algebra structure, but we should note that some equations fail to hold in general (dual to the fact that not all morphisms in the Markov category are homomorphisms for the comonoid structure). The Hennessy-Milner property is essentially the same in this situation, saying that our set of modally-expressible functions should separate points in the terminal coalgebra. Since we will have multiplication and linear combinations of functions, this entails under some mild topological conditions that it's dense in the set of functions on the terminal coalgebra.

It is worth examining this analogy a bit further, in the simpler setup of coalgebraic modal logic. If X is a space in some general sense, let us schematically write C(X) for the space of functions on X, so that as above stochastic maps X \to Y are identified with certain linear maps C(Y) \to C(X). Again, the Markov structure on the category of stochastic maps (whatever it is) amounts to the fact that C(X) carries the structure of an \mathbb {R}-algebra, and deterministic maps are those which are not algebra homomorphisms.

Let now \xi : X \to A \otimes X be a simple stochastic dynamical system which outputs a value of type A at each step. The dual of this is C(A) \otimes C(X) \to C(X), where the tensor here is now the tensor product of vector spaces.

Among algebras, the tensor product is the coproduct, so we may restrict the above map to form two modal operators, C(A) \to C(X) and C(X) \to C(X)---the latter being simply the transition operator taking a function \phi (x) to the expected value of the next step, the former computing the expected value of the output given x. But since the transition may be nondeterministic, these two restrictions do not determine it. From a logical point of view, the problem is that we can't express statements about the correlation between the output and the next step.

As a simple counterexample, consider two system where X = A = \{0,1\}. In the first, the output and the next state are independent, and both equal the current state with probability 1-\epsilon . In the other, the output and next state are always equal, and again are equal to the current state with probability 1-\epsilon

These systems have the same marginals X \to A and X \to X, and hence the two modal operators above have the same behaviour, and hence every modally expressible function is the same. But in the former, the probability of seeing ab output sequence beginning 1,0,\dots when starting in state 0 is proportional to \epsilon , whereas in the latter it is proportional to \epsilon ^2 (since you have to flip twice), so these systems have very different behaviour.

Using § [efr-000X], we can deduce a version of Hennessy-Milner for stochastic transition systems (with no input and outputs in finite set A). Namely, fix a system \xi : X \to A \otimes X, and let \nabla (u,v), with u: A \to \mathbb {R} and v: X \to \mathbb {R} denote the function which carries x \in X to the expected value of u(a)v(x') when (a,x') are distributed according to the system. Then \nabla is precisely the bilinear function C(A) \otimes C(X) \to C(X) dual to \xi . Since A^\omega is the terminal coalgebra, and the inverse limit of A \leftarrow A^2 \leftarrow \dots , we can infer that C(A^\omega ) is the colimit of the sequence C(A) \to C(A) \otimes C(A) \to \dots in some category of \mathbb {R}-algebras (we must think a little about topology to make this precise.)

But this should imply that the union of the images of C(A)^{\otimes n} inside this algebra is dense. So certainly they separate points. But this image consists exactly of formulas given by functions on A, applications of \nabla , and sums and products. So these formulae are sufficiently expressive to separate points of the terminal coalgebra (which are, of course, exactly bisimulation classes).