Let G be a (finite) directed acyclic graph (DAG). Then a structural causal model (SCM) on G consists of

• For each vertex v \in V(G), measurable spaces \mathcal {X}_v, \mathcal {E}_v
• A family of independent random variables E_v \in \mathcal {E}_v---these are called the exogenous variables
• For each v, a measurable function \phi _v: \mathcal {E}_v \times \prod _{v' \to v} \mathcal {X}_{v'} \to \mathcal {X}_v (note that if v has no parents, the product is just a singleton)

Let p be a 2-fibration with this property. Note that \mathsf {Cat} \subseteq \mathsf {BiCat} is a full sub(tri)category, hence the only question is whether the fibers are categories---that is, whether they have discrete hom-categories. The mapping category in the fiber, \mathcal {E}_x(x',y'), given x \in \mathcal {C}, x',y' \in \mathcal {E}_x, is given by the fiber of \mathcal {E}(x',y') \to \mathcal {C}(x,x) over the identity---but by assumption this is a discrete category.

Conversely, let F: \mathcal {C}^{\mathrm {co} \mathrm {op}} \to \mathsf {Cat} be a bifunctor and consider its Grothendieck construction. By definition, a 2-cell is (\alpha ,\alpha _-): (f,f_-) \to (g,g_-) : (x,x') \to (y,y') where \alpha : f \to g: x \to y, and \alpha _- is a 2-cell like this in F(x):

(Note, we use the notation \int for the Grothendieck construction/category of elements, where Buckley uses \mathrm {El})

A limit sketch consists of a (small) category \mathcal {I} equipped with a collection of cones (J_i \in \mathsf {Cat}, D_i: J_i^\triangleleft \to \mathcal {I}) (recall that J^\triangleleft is the "cone on J", the result of freely adjoining an initial object to J).

If \mathcal {C} is a category, a model of the limit sketch is a functor M: \mathcal {I} \to \mathcal {C} so that each composite J_i^\triangleleft \to \mathcal {I} \to \mathcal {C} is a limit cone. A morphism of models is any natural transformation. In other words, the category of models is the full subcategory of the functor category spanned by the models. It is denoted \mathsf {Mod}_\mathcal {I}(\mathcal {C}) (the collection of diagrams is left implicit).

Given a bicategory or other higher category \mathcal {C}, a model is a pseudofunctor \mathcal {I} \to \mathcal {C} which carries every diagram to a homotopy limit cone. \mathsf {Mod}_\mathcal {I}(\mathcal {C}) \subseteq \mathsf {Fun}(\mathcal {I},\mathcal {C}) is again the full sub-bicategory of the bicategory of pseudofunctors spanned by the models.

We will want to say that the category of pseudo double categories is the category of internal pseudocategories---modeled as Segal objects---in the bicategory of categories. There are two issues with this statement as written.

First of all, a priori, a weak Segal category is quite different from a pseudo double category. Not only is there not a canonical choice of composition given two horizontal maps f: x \nrightarrow y, g: y \nrightarrow z, we cannot even (a priori) guarantee the existence of a choice of composition gf which has the right boundaries on the nose---only up to vertical isomorphism (so we can find a composite x' \nrightarrow y' and isomorphisms x \cong x', y \cong y'). On the other hand, a weak Segal category is also stronger than a pseudo double category, in the sense that every vertical isomorphism has a companion.

We will see that the first defect can always be remedied after replacing our weak Segal category with an equivalent one. The issue of companions is a fundamental difference, but luckily all of the relevant double categories we want to consider have these companion pairs.

The second question is somewhat subtler (but also less important). The category of internal pseudocategories, computed in any higher category, has a priori the same homotopy level as the input---just as the category of monoids is a 1-category (like \mathsf {Set},) but the category of monoidal categories is a bicategory. This makes sense if we view categories as just a plain (generalized) algebraic theory, but we usually want to think of categories of categories as having some extra homotopy theory coming from the category structure---the category of categories in \mathsf {Set} is a bicategory (actually a 2-category, i.e it's strict), not a plain category. The preceding construction does not account for this---the homotopy limits implicit in the phrase "a pseudocategory in pseudo double categories" are, for us, merely homotopy limits of plain categories, not accounting for the extra categorical structure in a double category.

It is not clear what this means in general (and in any case, our output category will actually be strict in two directions,) but it is an important subtlety to remember.

(A category viewed as an object merely of the 1-category of categories is sometimes called a strict category, but obviously we can't speak about "strict pseudo double categories")

Consider the simplicial category \Delta . For every n,m, the following square commutes:

A simplicial object X in a category \mathcal {C} is called a Segal object if each of these squares goes to a pullback square.

Let X: \Delta ^\mathrm {op} \to \mathsf {Cat} be a (strict) simplicial category (note that every simplicial category is equivalent to a strict one). Suppose further the face maps X[1] \rightrightarrows X[0] are both isofibrations. Then if X is a Segal category in the strict sense, it is automatically a Segal category in the pseudo sense.

Proof

• June 25, 2024
• Eigil Fjeldgren Rischel

Since, up to isomorphism of categories, the higher X[n] are pullbacks of the two indicated face maps, and the projections in the diagram

are compositions of pullback projections, and pullbacks and composition of isofibrations are again isofibrations, it follows that all of these squares are pullbacks of two isofibrations. Such a pullback is always also a homotopy pullback, which proves the first statement.

The simplicial category is the category of finite, nonempty, totally ordered sets, and order-preserving functions, denoted \mathbb {\Delta }. We denote by [n] for n \geq 0 the ordered set \{0 < 1 < \dots < n\} of n+1 elements---every object on \mathbb {\Delta } is isomorphic to one of the form [n].

A simplicial object in a category \mathcal {C} is a functor \Delta ^\mathrm {op} \to \mathcal {C}.

Let \mathcal {C} be a category with finite limits. The internal nerve functor \mathsf {Cat}(\mathcal {C}) \to \mathsf {Simp}\mathcal {C} is fully faithful, and the essential image consists exactly of those simplicial objects X where the maps p_i: X[n] \to X[1] given by evaluating at p^i: [1] \to [n] : k \mapsto k+i, i = 0,\dots n-1 exhibits X[n] as the iterated pullback X[1] \times _{X[0]} \dots \times _{X[0]} X[1]

A pseudo double category is equivalently a simplicial object in \mathsf {Cat} so that the diagrams X[n] \to X[1] are homotopy pullbacks.

Let \mathcal {I},\mathcal {J} be limit sketches, and let \mathcal {C} be a bicategory. Then \mathsf {Mod}_\mathcal {I}(\mathsf {Mod}_\mathcal {J}(\mathcal {C})) \simeq \mathsf {Fun}'(\mathcal {I} \times \mathcal {J}, \mathcal {C}) \simeq \mathsf {Mod}_\mathcal {J}(\mathsf {Mod}_\mathcal {I}(\mathcal {C})), where \mathsf {Fun}'(\mathcal {I} \times \mathcal {J},\mathcal {C}) denotes the full subcategory of the functor bicategory spanned by those pseudofunctors F so that, for each I \in \mathcal {I},, F(I,-) is a model of \mathcal {J}, and for each J \in \mathcal {J}, F(-,J) is a model of \mathcal {I}.

A weak Segal category is similar to a virtual double category: we don't directly have a composition operator \mathbb {C}_1 \times _{\mathbb {C}_0} \mathbb {C}_1---rather, we have a category of "compositions" \mathbb {C}_2, each of which contains three faces in \mathbb {C}_1. Hence we have a choice of composites for every composable pair, although it is uniquely defined up to contractible choice.

Let \mathbb {C} be a pseudo double category. Then the coherent nerve is the simplicial category N(\mathbb {C}) defined as follows:

1. N(\mathbb {C})_0 = \mathbb {C}_0
2. N(\mathbb {C})_1 = \mathbb {C}_1
3. The objects of N(\mathbb {C})_2 are tuples f: x \nrightarrow y, g: y \nrightarrow z, h: x \nrightarrow z, \alpha : gf \simeq h, where x,y,z are objects of \mathbb {C}_0, f,g,h are horizontal morphisms, and \alpha is a globular isomorphism in \mathbb {C}_1
4. The morphisms of N(\mathbb {C})_2 are triples of 2-cells \phi : f \to f', \psi : g \to g', \xi : h \to h' so that the two possible 2-cells gf \to h' agree
5. Given four compatible objects of \N (\mathbb {C})_2 defining a 3-boundary (a tetrahedron), there is a unique objects of \N (\mathbb {C})_3 filling it if and only if the square of globular isomorphisms commute
6. Given four compatible morphisms of \N (\mathbb {C})_2, there is always a unique morphism in \N (\mathbb {C})_3 filling the boundary
7. The face- and degeneracy functors are the obvious ones
8. \N (\mathbb {C}) is 3-coskeletal, which defines the rest of the structure

1. A pseudo double functor \mathbb {C} \to \mathbb {D} is equivalent to a natural transformation N(\mathbb {C}) \to N(\mathbb {D})
2. If \mathbb {C} is a double category in which each vertical isomorphism has a companion, N(\mathbb {C}) is a weak Segal category
3. Every weak Segal category is equivalent to one of the form N(\mathbb {C}) for \mathbb {C} a pseudo double category of this type.

Let \mathbb {C} be a double category in which every vertical isomorphism has a companion. Then by

reference here, Shulman stuff,

Now, let X be a weak Segal. By

reference

This means the functor X[n] \to X(\partial \Delta ^n) is an isofibration for each n. First, let n=1. This means X[1] \to X[0] \times X[0] is an isofibration. Since such fibrations are stable under pullback, this implies that the projection X(\partial \Delta ^2) \to X[1] \times _{X[0]} X[1] is again an isofibration, which means the composite X[2] \to X[1] \times _{X[0]} X[1] is an isofibration. Since this pullback is a homotopy pullback, and X is weak Segal, it is an equivalence, and hence a trivial equivalence. Choose a (strict!) section s.

By a completely analogous argument, choose a section of X[3] \to X[1] \times _{X[0]} X[1] \times _{X[0]} X[1], which is again a trivial fibration.

Let our pseudo double category have X[1] \rightrightarrows X[0] as the underlying reflective graph, composition defined by the composite X[1] \times _{X[0]} X[1] \to X[2] \xrightarrow {d_1} X[1], associator defined using the degeneracies, and unitor defined using the section of X[3]. Call this pseudo double category \mathbb {X}

It is easy to see there is a functor X \to N(\mathbb {X}), which is the identity on the first two levels. Since the higher levels are homotopy pullbacks of the lower levels, this implies it is an equivalence at each level, concluding the proof.

The pseudofunctor \mathsf {\mathbb Para}: \mathsf {Arr}(\mathsf {SymMonCat}) \to \mathsf {PsDbl}, which carries a symmetric monoidal functor \mathcal {C} \to \mathcal {D} to the pseudo double category \mathsf {\mathbb Para}_\mathcal {C}(\mathcal {D}), preserves homotopy limits.

Let \mathcal {C}, \mathcal {A}(-), T be a dynamical systems theory, let \mathsf {\mathbb Arena} be the associated category of arenas. Recall that \mathsf {\mathbb Arena}_0 is the category of lenses. Consider the (strict) category internal to \mathsf {Arr}(\mathsf {SymMonCat}) given by the following diagram:

(Note the difference between \mathsf {Arr}(\mathcal {C})^\simeq and \mathsf {Arr}(\mathcal {C}^\simeq )---the former has objects all morphisms of \mathcal {C}, and the morphisms between them given by isomorphisms, whereas the latter has objects only the isomorphisms in \mathcal {C})

The objects of \mathsf {\mathbb Ctrl} are arenas.

The three directions of morphism in \mathsf {\mathbb Ctrl} are lenses, charts, and controlled processes.

The lens-chart double category is isomorphically \mathsf {\mathbb Arena}---in particular, composition of both lenses and charts is strictly associative.

The process-chart double category has 2-cells the chart reparametrizations. The process-lens double category has 2-cells the lens isoparametrizations. They both compose in the obvious way.

Processes compose as morphisms of \mathsf {Para}_{\mathcal {C}^\simeq }(\mathsf {Lens})---that is, (S,TS \otimes A \to B) ; (S', TS' \otimes B \to C) = (S' \otimes S, T(S' \otimes S) \otimes A \cong TS' \otimes TS \otimes A \to TS' \otimes B \to C), this is associative up to a coherent choice of globular isoparametrization.

We can consider two strategies for constructing the "full" triple category of controlled processes:

1. Give a construction of the double category of controlled processes and all lens reparametrizations, in a functorial way so that we can extend this to a triple category
2. Prove that freely(?) adding companions, in a suitable sense, of each globular chart reparametrization, gives the right thing (this should amount to checking a composition rule)

Let \mathsf {\mathbb Ctrl}_1 \to \tilde {\mathsf {\mathbb Ctrl}_1} be constructed by freely adding companions of every globular chart reparametrization. Then \tilde {\mathsf {\mathbb Ctrl}_1} admits the following description:

1. The objects are the objects of \mathsf {\mathbb Ctrl}_1, i.e tuples A,B,S, TS \otimes A \leftrightarrows B
2. The vertical morphisms are chart reparametrizations
3. The horizontal morphisms are lens reparametrizations
4. \mathsf {\mathbb Ctrl}_1 is thin, and a square exists if and only if the underlying square in \mathcal {C} commutes.

Fix the notation of \mathsf {\mathbb Ctrl} vs \tilde {\mathsf {\mathbb Ctrl}}

Observe that this diagram is a Kolmogorov limit in \mathsf {BorelStoch}:

This gives a coalgebra structure on A^\omega in the usual way.

Given \xi : X \to X \otimes A, we can build a cone by iteratively applying A \times - to the unique map X \to I:

It will be instructive to work out the theory in the discrete case, which is to say, for the Kleisli category of the discrete (i.e finite-support) distribution monad on \mathsf {Set}. Note that even for discrete-time discrete-space applications, this setup is not really adequate, as we lack the structure to construct terminal systems.

Proposition [efr-001D]

• June 24, 2024
• Eigil Fjeldgren Rischel

The set of indexed stochastic charts is just the set of commutative squares in \mathsf {Kl}(\Delta ) of this form:

(where the vertical maps are, by assumption, deterministic, but the horizontal ones aren't necessarily)

Proof

• June 24, 2024
• Eigil Fjeldgren Rischel

Note that an indexed stochastic chart X \to Y is equivalently a family of stochastic charts \binom {\bar {X}_{x}}{\{x\}} \to \binom {\bar {Y}}{Y} for each x \in X. The analogous statement is true for commutative diagrams of this form (since coproducts in diagram categories are pointwise, and coproducts of sets are again coproducts in Kleisli categories). Hence it suffices to check the case X = *. In this case, a commutative square amounts to a family of distributions on \bar {Y}, each of which induces the same distribution on Y. On the other hand, we are looking at the convex set

\sum _{y \in Y}[\Delta (\bar {X}),\Delta (\bar {Y}_y)] = \sum _y \Delta (\bar {Y}_y)^{\bar {X}},

where this exponential denotes the iterated Cartesian product in convex spaces. An element of this set clearly gives a commutative square, because for each y \in Y, there is a square which deterministically chooses that y, and uses the given family of distributions on \bar {Y}_y depending on \bar {X}. This mapping is injective, since each map \bar {X} \to \Delta (\bar {Y}_y) can be recovered as a conditional distribution, and the convex combination of ys is merely the underlying distribution on Y. On the other hand, by choosing conditional distributions, it is also seen to be surjective, finishing the proof.

Definition [efr-001V]

• June 28, 2024
• Eigil Fjeldgren Rischel

Let \alpha : TS \leftrightarrows A be a system with interface A, and let P be another arena. A P-valued predicate on \alpha is a lift

For discrete-time deterministic systems, a P = {\bar {P} \choose P}-valued predicate amounts to a mapping S \to P---since the diagram implies the update can't depend on the extra input \bar {P}, and in the deterministic case, a lift of S \to A over A \otimes P is simply a choice of S \to P. (In the non-deterministic case, this is not true, of course).

Let F: \mathsf {Set} \to \mathsf {Set} be a functor, and let \xi : X \to FX be a coalgebra of it. Then we can describe a predicate of X valued in P \in \mathsf {Set} as simply a function \phi : X \to P. Note that this makes X a coalgebra of F(-) \times P, and as such it has a unique map to the terminal coalgebra (if it exists) of this functor X \to (F(-) \times P)^\infty .

This means, given a predicate on that terminal coalgebra, p: (F(-) \times P)^\infty \to P, by composing these two operations, we get a new predicate on X. Thus, predicates on these cofree coalgebras are a sort of "modal operators"---for example, if P = \{\bot ,\top \} is the set of booleans, and F(X) = X (so that coalgebras are just discrete dynamical systems), the cofree coalgebra on P is the set \{\bot ,\top \}^\omega of streams of booleans. Then we can take p((\phi _i)) to be true if and only if each \phi _i is true. Then the modal operator of p is essentially "necessity"---the composite predicate is true for exactly those x \in X so that \phi (x_n) is true for every x_n on the trajectory.

In good cases, there will be a monadic adjunction associated to the lens A' \leftrightarrows A, and so this operation will give an endomorphism on predicates for each choice of lift of the cofree predicate (it can of course lift as itself, which corresponds to the identity operation).

When moving from deterministic, ordinary differential equations, to stochastic differential equations---or, from another point of approach, moving from discrete-time stochastic systems to continuous-time stochastic systems---we are forced to confront the problem that typical stochastic differential equations do not have differentiable solutions.

A few questions immediately pose themselves when confronted with this statement:

1. Since a solution of a stochastic differential equation is not merely a function but some sort of distribution of functions, what do you mean by them not being differentiable?
2. Whatever the solutions are, how can they solve a differential equation if they aren't't differentiable?

It will be instructive to consider Brownian motion. For each t \in \mathbb {R}, let E_t be an independent standard Gaussian. There are some issues with defining the integral X_r = \int _0^r E_t dt, since t \mapsto E_t can't be guaranteed to be even measurable, but these can be sidestepped without too many problems. Then X_r is Brownian motion, but with probability 1 it is nowhere differentiable. The integral equation above describes the sense in which X solves a stochastic differential equation saying it's derivative at each point is standard Gaussian distributed.

Of course, since not all systems are integrable (this is not even true in the deterministic case,) there is not gonna be an integral operator lying around that we can use to define the solutions of our differential equations. Hence we must use a different solution concept.

Recall that, if f,g: \mathbb {R} \to \mathbb {R} are differentiable functions, \int _a^b f(x)g'(x)dx = f(a)g(a)---f(b)g(b)---\int _a^b f'(x)g(x)dx, (integration by parts). Now if we choose f to be zero except on a bounded interval, and let the endpoints to infinity, we get \int _\mathbb {R} f(x)g'(x) dx =---\int _\mathbb {R} f'(x)g(x)dx. The trick here is that the right-hand side is defined even if g is not differentiable, and so it gives us a way of talking about "the derivative of g", at least for some purposes, even when it doesn't exist.

Since two functions have the same integral after multiplication by every differentiable f, if and only if they're equal almost everywhere, this is fairly robust---if g is C^1 and satisfies some differential equation "weakly", it follows it must satisfy it on the nose as well, for example.

Let \phi : C_c(Y) \to C_c(X) be a positive linear map. Then dualizing gives a linear map \phi ^*: C_c(X)^* \to C_c(Y)^*. If we assume the initial map preserves the constant 1 function, this will preserve probability measures, making it a sort of infinity-dimensional stochastic matrix.

In particular, we get a composite map X \to C_c(X)^* \to C_c(Y)^*, where the first map just includes the dirac measures (or, alternatively, takes x to the "evaluate at x" functional).

If we further assume \phi is continuous for the uniform convergence topology, \phi ^* will be continuous for the pointwise convergence topology. Since every probability measure is a limit of linear combinations of dirac measures in this topology, that means \phi ^* will be controlled by the above map, so we really have an injective correspondence between linear, continuous and unit-preserving maps C_c(Y) \to C_c(X) and some subset of the Markov kernels X \to Y.

If we stare at this sequence of composites a bit, we realize that the linear operation corresponding to a kernel pX \to Y carries a function f: Y \to \mathbb {R} to the expected value function x \mapsto E_{y \sim p(x)} f(y). Not all Markov kernels will have the property that this preserves continuity of f (all measurable functions are Markov kernels, even)---but we would probably want to impose some notion of continuity on our kernels in any case.

Instead of thinking about the classes of Markov kernels with this continuity-of-expectation property, we can simply use the space of continuous, unit-preserving linear maps C_c(Y) \to C_c(X) as our class of stochastic maps X \to Y.

Naively, we would think that a stochastic differential equation on a manifold X should be a stochastic section of the tangent bundle, f: X \to \Delta (TX) (with the understanding that such a thing may not always have a solution).

Indeed, we will see that such a thing does lead to a differential equation. But unlike the deterministic case, there is not a 1-1 correspondence---different sections may determine the same differential equation (in the sense of having the same solutions).

The issue is that, as we have discussed, by necessity solutions of stochastic differential equations are defined by integration, in a certain sense. The solution concept we have in mind is a Markov process, where each derivative is sampled independently from its distribution. But by the central limit theorem, integrating a family of independent random variables will always give a normal distribution, no matter what those variables are.

In particular, the only aspect of the assigned distribution of derivatives f(x) \in \Delta (T_xX) is its mean Ef(x) \in T_xX and its covariance matrix, which is the expectation of v \otimes v inside the tensor product T_xX \otimes T_xX when v \sim f(x).

(Another way of viewing the covariance is as an operator on the tensor product of the covector space T_x^*X \otimes T_x^*X \to \mathbb {R}, which carries a simple tensor of two covectors \phi \otimes \psi to the expected value of \phi (v)\psi (v) when v is sampled according to the given distribution).

In our study of discrete-time systems, we used the observation that the terminal system with a given interface can be characterized as the set of trajectories of that interface (eg § [efr-000X]). This allows us to develop an algebra of predicates on systems in the vein of coalgebraic modal logic.

However, for continuous-time systems, the situation is much more complicated. In general, we can't expect an ordinary differential equation to have a unique solution for each initial value. There are two basic reasons for this:

1. A simple system like y' = y^2, y \in \mathbb {R} experiences finite-time blowup, escaping to infinity inside a finite time horizon. In this example, the solutions have the form y(t) = 1/(t+C), and so they clearly can't be continued past a certain horizon. Given some function \alpha (y), we can't extend this to a function t \mapsto \alpha (y(t)) on all of \mathbb {R}
2. The differential equation y' = 2 \sqrt {|y|} has both the solution y(t) = 0 and y(t) = y^2 (and many others)

The second issue can be solved by assuming our equations are Lipschitz (which the square root function is not). Since smooth functions are at least Lipschitz on compact domains (with Lipschitz constant bounded by the maximal derivative), there is some hope that we can get rid of this problem (but note that, when studying stochastic processes, there are reasons for wanting to study processes with jumps, complicating the situation).

However, the first issue is more resilient. One approach is to restrict our attention to compact manifolds---this is enough to guarantee that every smooth differential equation has a (global) solution. The problem with this is that the spaces of trajectories---like the space of smooth functions \mathbb {R} \to A---will not even be a manifold, but some type of generalized smooth space. Hence we will not a priori be able to extend this class

Consider the category of smooth microlinear spaces X equipped with a map X \to A and a vector field X \to TX.

1. This category has a terminal object, given by the colimit taken over a suitable class of small objects. In other words, a point in the terminal system is given by some system U \to TU \times A and a point u_0 \in U, up to an equivalence relation of bisimulation
2. The mapping space A^R, equipped with the evaluation at 0 map A^R \to A and the flow \frac {du}{dt} = \frac {du}{dx} is a subterminal object.
3. A system X \to A \times TX admits a map to A^R if and only if it is integrable in both directions

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

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.

Consider the theory of discrete dynamical systems, and let \xi : TS \leftrightarrows A = {\bar {A} \choose A} be a system. Let \phi : S \to \{\bot ,\top \} be a predicate on S, and let {\bar {U} \choose U} \subseteq {\bar {A} \choose A} be a subobject of A (that is, \bar {U} \subset \bar {A} and U \subset A, and if (a,a') \in \bar {U} then a \in A).

Then write \nabla _{U}(\phi ) for the predicate on S which is true if and only if the following hold: \xi (s) \in U, and if a' \in \bar {U} \times _A S, then \xi ^\#(s,a') satisfies \phi . In other words---the output is in U, and if the input is further in \bar {U}, then the next step will satisfy \phi .

Note that by taking U = A, \bar {U} = \bar {A} this encodes a simple next-step modality.

Observe also that, if A,\bar {A} are both finite, we can encode all the classical covering modality operators as (finite) conjunctions of \nabla _{\{(a,a_i)\}}\phi _i, and hence the logic built up of these modal operators and Boolean operations will enjoy the Hennessy-Milner property.

Let an MDP (or partially observable MDP) be given, and consider a statement like "given policy \pi , the expected reward is \geq r", or "the probability that the total reward is less than r is \leq \epsilon ", and so on. In one sense, these are statements about policies---but, fixing a policy, they become statements about the states of the MDP (meaning: if the problem is initialized in state s_0, and we use policy \pi , ...). In particular, they are statements about the behaviour of the state of the MDP, and so should be expressible using the modal logic.

In particular, given a system TS \to A, if we have a good way of controlling the composite system TS \to A \to B---that is, a modal formula providing that certain behavior on the interface will lead to a high reward---then we can translate this into a statement that certain behavior on the interface A (namely, the same behaviour translated back) will lead to a high reward in the original system. Moreover, we're not restricted to statements about expected reward, but can encode all sorts of statements about the behavior, like a bound on the probability that some region will be crossed.

Both the endofunctor \Delta (- \times A): \mathsf {Meas} \to \mathsf {Meas}, and the endofunctor - \otimes A: \mathsf {Stoch} \to \mathsf {Stoch} express the idea of a stochastic transition system which produces an output in the measurable space A at each step. (We could also have considered the similar endofunctor on \mathsf {Set}, using a discrete probability monad, and its Kleisli category). In fact, in one sense, these are equivalent---since \mathsf {Stoch} is the Kleisli category of \Delta , and \otimes on objects is simply defined as the product measurable space, the sets \mathsf {Stoch}(X,X \otimes A) and \mathsf {Meas}(X, \Delta (X \times A)) are by definition equal to each other.

The difference is in the category of coalgebras. A morphism between \Delta (- \times A)-coalgebras must be deterministic---it must assign to each x \in X a y \in Y so that the obvious diagram commutes. In contrast, a morphism on - \otimes A-algebras is a morphism in \mathsf {Stoch}---it must assign to each x \in X a distribution on Y, so that the two implied distributions on A \times Y agree.

We can see the difference most clearly if we consider which properties are bisimulation invariant (i.e are properties of "behaviours"). We have seen that the terminal - \otimes A-coalgebra is A^\omega , so a behaviour in this sense is simply a distribution on streams---the questions we can ask are what the probability of a certain sequence of outputs is.

In contrast, of an element in a \Delta (- \times A)-coalgebra, we can ask a question like this: "What is the probability that, after 10 steps, we will be in a state which produces output a with probability at least p"? In a - \otimes A-coalgebra, we can ask "what is the probability that the output on the 11th step is a", or "what is the probability that, after 10 steps, the conditional probability of the next output being a, conditional on the first 10 outputs, is at least p?"---but we cannot access the probabilities of an output given the future state directly, only the correlations that exist between the outputs.