The local state monad has rank (WIP)
In this post we will show that the local state monad of (Plotkin & Power, 2002) (which was suggested by Peter O’Hearn) has rank. In other words, dependent on the choice of values used for the state, the local state monad preserves $\lambda$-filtered colimits for a regular cardinal $\lambda$.
1Background
Toggle to show all details:
Let us first recall the necessary background details. Some details are hidden by default, and the heading can be clicked to open them, or the above switch can be used to reveal them all.
Regular cardinals and filtered colimits
Regular cardinals generalize the statement “a finite union of finite sets is finite”.
definition1.1Regular cardinal (Borceux, 1994, Page I.268) An infinite cardinal $\lambda$ is regular when, for arbitrary sets $J$ and $\{ X_j\}_{j \in J}$, it satisfies \[ \left( \left|J\right| < \lambda \, \wedge \, \forall j \in J, X_j < \lambda \right) \;\Rightarrow\; \left| \bigcup_{j \in J} X_j \right| < \lambda \] i.e. a union of size less than $\lambda$ of sets size less than $\lambda$ is size less than $\lambda$.
For a filtered category, every finite diagram over it has a cocone. For a $\lambda$-filtered category, we want every diagram of size less than $\lambda$ over it has a cocone. This leads to the following definition.
definition1.2$\lambda$-filtered category (Borceux, 1994, Page I.268) Let $\lambda$ be a regular cardinal. A category $\cat{C}$ is $\lambda$-filtered when
- there exists at least one object in $\cat{C}$,
- given a set $J$ with $\left\vert J \right\vert < \lambda$ and a family $\left( C_j \in \cat{C} \right)_{j \in J}$ of objects of $\cat{C}$, there exists an object $C \in \cat{C}$ and a morphisms $f_j \colon C_j \to C$,
- given a set $J$ with $\left\vert J \right\vert < \lambda$ and a family $\left(f_j \colon C_j \to C' \, \right)_{j \in J}$ in $\cat{C}$, there exists an object $C'' \in \cat{C}$ and a morphism $f \colon C' \to C''$ such that $f \circ f_{j_1} = f \circ f_{j_2}$ for all $j_1, j_2 \in J$.
We then have the desired property.
lemma1.3$\lambda$-filtered cocone (Borceux, 1994, Page I.269) Let $\lambda$ be a regular cardinal and $\cat{C}$ a $\lambda$-filtered category. For every category $\cat{D}$ such that the cardinality of all of its arrows is less than $\lambda$ and every functor $F \colon \cat{D} \to \cat{C}$, there exists a cocone on $F$.
Recall that finite limits commute with filtered colimits in $\Set$. Thus, $\lambda$-filtered colimits and $\lambda$-limits are defined to achieve an analogous theorem.
definition1.4$\lambda$-filtered colimits and $\lambda$-limits (Borceux, 1994, Page I.268) Let $\lambda$ be a regular cardinal.
- By a $\lambda$-filtered colimit in a category $\cat{C}$ we mean the colimit of a functor $F \colon \cat{D} \to \cat{C}$ where the category $\cat{D}$ is $\lambda$-filtered.
- By an $\lambda$-limit in a category $\cat{C}$, we mean the limit of a functor $F \colon \cat{D} \to \cat{C}$ where $\cat{D}$ is a small category and the cardinality of the union of all of its arrows is less than $\lambda$.
theorem1.5$\lambda$-filtered colimits and $\lambda$-limits commute in $\Set$ (Borceux, 1994, Page I.269) Let $\lambda$ be a regular cardinal. In $\Set$, $\lambda$-limits commute with $\lambda$-filtered colimits.
definition1.6Rank of a functor (Borceux, 1994, Page II.272) A functor $F \colon \cat{C} \to \cat{D}$ has rank $\lambda$, for some regular cardinal $\lambda$, when $F$ preserves $\lambda$-filtered colimits. It has rank when it has rank $\lambda$ for some regular cardinal $\lambda$.
definition1.7Finite sets and injections Let $I$ denote the category whose objects are the sets $n \defeq \{ 1, \ldots, n \}$ for $n \in \N$ (so that $0 = \emptyset$) and whose maps are injections.
Under category
definition1.8Under category Let $\cat{C}$ be a category and $x \in \cat{C}$. Then the under category $x / C$ has as objects $f \colon x \to y$ maps in $\cat{C}$ and morphisms $g \colon (f_1 \colon x \to y_1) \to (f_2 \colon x \to y_2)$ are given by maps $g \colon y_1 \to y_2$ in $\cat{C}$ such that
commutes.
Distributive law of monads
definition1.9Distributive law (Beck, 1969) Let $(T, \eta^T, \mu^T)$ and $(S, \eta^S, \mu^S)$ be monads over the same category. A distributive law of $S$ over $T$ is a natural transformation $\theta \colon TS \to ST$ such that the following diagrams commute:
proposition1.10Composed monad from distributive law (Beck, 1969) Let $(T, \eta^T, \mu^T)$ and $(S, \eta^S, \mu^S)$ be monads over the same categoryand $\theta \colon TS \to ST$ a distributive law of $S$ over $T$. Then $(ST, \eta^S \eta^T, \mu^S \mu^T \circ S \theta T)$ is a monad. That is, the functor $ST$ is a monad with unit and multiplication given by
respectively.
2Original definition
Let $V \in \Set$ be a fixed set, and define the functor $S \colon I^{\op} \to \Set$ by $S(n) \defeq V^n$ on objects and for a morphism $\rho \colon n \to m$ in $I$, \[ \begin{aligned} S(\rho) \colon S(m) &\to S(n) \cr (v_{1}, \ldots, v_{m}) &\mapsto \left(v_{\rho(1)}, \ldots, v_{\rho(n)}\right) \end{aligned} \] i.e. re-indexing by $\rho$. Then the monad for local state of (Plotkin & Power, 2002) on $[I, \Set]$ , suggested to them by Peter O’Hearn, is
labeled2.1 \[ (TX)(n) \defeq S(n) \Rightarrow \int^{m \in (n / I)} S(m) \times X(m) \]
For the functorial actions of $TX$, let $\rho \colon n \to p$ in $I$. Then $n \leq p$, and so define $q \defeq p - n$ so that $\rho \colon n \to n + q$. Observe that $S(n + q) \simeq S(n) \times S(q)$. Thus, a map of type $(TX)(\rho) \colon (TX)(n) \to (TX)(n + q)$ is equivalent to a map of type \[ \left(S(n) \Rightarrow \int^{m \in (n / I)} S(m) \times X(m)\right) \times S(n) \times S(q) \to \int^{m' \in \left((n + q) / I\right)} S(m') \times X(m'). \] We can then use evaluation at $S(n)$ and colimit preservation of $- \times S(q)$, followed by the inclusion of the $m$-th component of the domain coend into the $(m + q)$-th component of the codomain coend, to define the functorial action. Note that the category of which we take the coend over changes. We will not recall the monad structure of $T$ here.
To make our later proofs simpler and more modular, we will work with an alternative definition of $T$. Namely, we will decompose $T$ into two monads $F$ and $B$ with a distributive law $\theta \colon BF \to FB$ such that their composition is $T$.
3Modular definition
Let $V \in \Set$ be a fixed set and define $S \colon I^{\op} \to \Set$ as before. The distributive law we will use is from (Melliès, 2014). Their distributive law is between the fiber monad $F$ and the basis monad B.
definition3.1Fiber monad The fiber monad $F$ on $[I, \Set]$ is defined on $X \colon I \to \Set$ by \[ (FX)(n) \defeq S(n) \Rightarrow \left( S(n) \times X(n) \right) \] so that it is “fiberwise” the global state monad.
What is the functorial action of $FX \colon I \to \Set$?
todo
References
- Plotkin, G., & Power, J. (2002). Notions of Computation Determine Monads. In M. Nielsen & U. Engberg (Eds.), Foundations of Software Science and Computation Structures (pp. 342–356). Springer. https://doi.org/10.1007/3-540-45931-6_24
- Borceux, F. (1994). Handbook of Categorical Algebra: Volume 1: Basic Category Theory (Vol. 1). Cambridge University Press. https://doi.org/10.1017/CBO9780511525858
- Borceux, F. (1994). Handbook of Categorical Algebra: Volume 2: Categories and Structures (Vol. 2). Cambridge University Press. https://doi.org/10.1017/CBO9780511525865
- Beck, J. (1969). Distributive laws. In H. Appelgate, M. Barr, J. Beck, F. W. Lawvere, F. E. J. Linton, E. Manes, M. Tierney, F. Ulmer, & B. Eckmann (Eds.), Seminar on Triples and Categorical Homology Theory (pp. 119–140). Springer. https://doi.org/10.1007/BFb0083084
- Melliès, P.-A. (2014). Local States in String Diagrams. In G. Dowek (Ed.), Rewriting and Typed Lambda Calculi (pp. 334–348). Springer International Publishing. https://doi.org/10.1007/978-3-319-08918-8_23
- Staton, S. (2010). Completeness for Algebraic Theories of Local State. In L. Ong (Ed.), Foundations of Software Science and Computational Structures (pp. 48–63). Springer. https://doi.org/10.1007/978-3-642-12032-9_5