Reference Categorical logic of names and abstraction in action calculi [pavlovic-categorical-names]

Abstract

  • December , 1997
  • Duško Pavlović

Milner’s action calculus implements abstraction in monoidal categories, so that familiar λ-calculi can be subsumed together with the π-calculus and the Petri nets. Variables are generalised to names , which allow only a restricted form of substitution. In the present paper, the well-known categorical semantics of the λ-calculus is generalised to the action calculus. A suitable functional completeness theorem for symmetric monoidal categories is proved: we determine the conditions under which the abstraction is definable. Algebraically, the distinction between the variables and the names boils down to the distinction between the transcendental and the algebraic elements. The former lead to polynomial extensions, like, for example, the ring ℤ[ x ]; the latter lead to algebraic extensions like ℤ[√2] or ℤ[ i ]. Building upon the work of P. Gardner, we introduce action categories , and show that they are related to the static action calculus in exactly the same way as cartesian closed categories are related to the λ-calculus. Natural examples of this structure arise from allegories and cartesian bicategories. On the other hand, the free algebras for any commutative Moggi monad form an action category. The general correspondence of action calculi and Moggi monads will be worked out in a sequel to this work. 

 @article
{pavlovic-categorical-names, title={Categorical logic of names and abstraction in action calculi}, volume={7}, rights={https://www.cambridge.org/core/terms}, ISSN={0960-1295, 1469-8072}, DOI={10.1017/S0960129597002296}, number={6}, journal={Mathematical Structures in Computer Science}, author={Pavlović, Duško}, year={1997}, month={Dec}, pages={619–637},language={en} }

Backlinks

The Para Construction as a double category [efr-002H]

In many different situations, we want to understand some morphism as parametrized by some data. For example, in machine learning one tries to find a function f: X \to Y with some desirable behaviour by choosing a parametrization F: P \times X \to Y and searching for some p \in P so that F(p,-) has this behaviour (for example by gradient descent on p).

In situations where we want to understand F as being built up as a composite of multiple functions (for example, the layers of a neural network), it is convenient to introduce a category of parametrized morphisms, where the composition combines the parameter spaces of each composite map. We can do this in a general setting with the following definition:

Definition [efr-002G]

Let \mathcal {M} be a monoidal category, and let \bullet : \mathcal {M} \times \mathcal {C} \to \mathcal {C} be an action of \mathcal {M} on another category \mathcal {C}. Then the \mathsf {Para} construction is the category \mathsf {Para}_\mathcal {M}(\mathcal {C}) where

  1. Objects are objects of \mathcal {C}
  2. Morphisms A \to B are tuples P \in \mathcal {M}, P \bullet A \to B up to the natural notion of isomorphism.
  3. Composition is by tensoring the parameter objects and composing.

The fact that the parametrization object may live in a different category than the domain and codomain objects, which initially seems like a superfluous generalization, is in fact highly useful. For example, we will often want to consider parametrized morphisms where the parameter space is decorated with some additional data, for example a probability distribution. In most such cases, the category of spaces decorated with such data will act on the category of spaces without such data (simply by forgetting the data and tensoring), and hence we can realize such parametrized morphisms as examples of this \mathsf {Para} construction. We may also want only Euclidean parameter space (so that we can run gradient descent simply), but allow the parametrized morphism to go between more general manifolds.

\mathsf {Para}, and generalizations of it, have been introduced many times. One of the earliest occurrences is by Hermida and Tennent, Reference [hermida-monoidal-indeterminates], in the special case of a symmetric monoidal category acting on another such via a functor i: \mathcal {C} \to \mathcal {D} (by a result of Capucci and Gavranović, Reference [actegories-amthematician-capucci-gavranovic], every "structure-preserving" action of a symmetric monoidal category on another has this form). Hermida and Tennent actually give a very intuitive universal property of \mathsf {Para}_\mathcal {C}(\mathcal {D}): it is freely generated by adding a morphism I \to i(C) for each C \in \mathcal {C}, subject to the equations that this must be a monoidal natural transformation. This type of idea actually goes all the way back to Pavlović in Reference [pavlovic-categorical-names].

The notation \mathsf {Para} was introduced inReference [backprop-as-functor], where the special case of parametrized morphisms of euclidean spaces was used to study gradient descent. In Reference [towards-cybercat], a bicategorical variant (replacing the quotient by isomorphism in the above variant in the obvious way) is introduced.

Example [efr-MN7C]

Let \mathcal {C} be a monoidal category, and let S: \mathcal {C} \to \mathsf {Set} be any functor. Recall that \int S is the category whose objects are pairs (X \in \mathcal {C}, s \in S(X)) and whose morphisms (X,s) \to (Y,s') are f: X \to Y so that S(f)(s) = s'. If S is lax monoidal (for (\mathsf {Set},\times ),) \int S acquires a lax monoidal structure making the forgetful functor \int S \to \mathcal {C} strong (even strict) monoidal.

With the action induced by this functor, the bicategory \mathsf {Para}_{\int S}(\mathcal {C}) has morphisms given by maps M \otimes X \to Y, m \in S(M), and maps given by reparametrizations which preserve the decoration m.

For example, let \mathcal {C} be a Markov category and let S(X) = \mathcal {C}(I,X). Then morphisms are parametrized maps equipped with a measure on the parameter space.

Example [efr-WEST]

If \mathbb {C} = \mathsf {Set} regarded as a discrete 2-category, as noted, a pseudomonoid action is just a monoid action in the ordinary sense---that is, a monoid M, a set X and a function m \cdot x so that m \cdot (n \cdot x) = (mn) \cdot x. The para construction is then the action category, whose objects are the points of X and whose morphisms x \to y are elements m so that m \cdot x = y (with multiplication as composition).

Example [efr-QH7O]

Let \operatorname {\mathsf {Ab} - \mathsf {Cat}} be the 2-category of \mathsf {Ab}-enriched categories, functors and natural transformations. Recall that a ring R is the same as a one-object category enriched in \mathsf {Ab}, and it admits a monoidal structure if and only if it is commutative (this is not particular to \mathsf {Ab}-enriched categories). An enriched R-action on an \mathsf {Ab}-category \mathcal {C} is then an R-module structure on each hom-set so that composition is R-linear in each variable.

[efr-KL7V]

If a category has coproducts, then \mathsf {Set} acts on it via S \cdot X = \coprod _{s \in S}X. (This is the \mathsf {Set}-enriched case of what in enriched categories is called a copower or tensor, the dual of the power objects from Example [efr-K3YI]). The morphisms of \mathsf {Para}_\mathsf {Set}(\mathcal {C}) are pairs (I \in \mathsf {Set}, (f_i: X \to Y \in \mathcal {C})_{i \in I}), which compose in the obvious way.

Note that this definition clearly makes sense even if \mathcal {C} does not actually have coproducts. This is an example of another construction which has been called \mathsf {Para}, which takes a monoidal category \mathcal {V} and a \mathcal {V}-enriched category \mathcal {C} and constructs a double category where the morphisms are pairs (J \in \mathcal {V}, J \to \mathcal {C}(X,Y)). It is not hard to see that this also extends to a double category in the same way, but we do not presently know the correct definition of internal enriched object that would replace pseudomonoid actions to replicate our general theory for this case. (note that the literature contains a notion of internal enriched category, Reference [internal-enriched], but these are categories enriched over internal monoidal categories---that is, the ambient category \mathcal {E} is a 1-category and the categorical structure of the base of enrichment \mathcal {V} is formulated on top of this, not as part of the structure of the objects of the category \mathcal {E})

There is a very natural double categorical version of \mathsf {Para}, where the vertical morphisms are just the unparametrized morphisms of \mathcal {C}, and the 2-cells with this boundary:

are morphisms M \to N (if f is parametrized by M, g by N) so that the square
commutes.

This notion is not original---we learned of it from Matteo Capucci---but it seems to have remained somewhat on the level of folklore. Our main goal for this section will be to construct this (pseudo) double category, and show that it is functorial---that is, given a homomorphism of actions, there is an induced functor between double categories. In fact, we will show that this construction works in any 2-category. Later we will apply it to a pseudomonoid action in (strict) double categories to construct a pseudocategory internal to double categories---our triple category of bimachines.

Theorem [efr-55CC]

Let \mathcal {M} be a monoidal category, and let \mathcal {C} be a category with an \mathcal {M}-action.

Then there is a pseudo double category \mathsf {\mathbb Para}_\mathcal {M}(\mathcal {C}), with

  1. \mathsf {\mathbb Para}_\mathcal {M}(\mathcal {C})_0 = \mathcal {C}
  2. \mathsf {\mathbb Para}_\mathcal {M}(\mathcal {C})_1 = \mathcal {M} \times \mathcal {C} \downarrow \mathcal {C}, with domain and codomain given by the two projections to \mathcal {C}
  3. The identities map \mathcal {C} \to \mathcal {M} \times \mathcal {C} \downarrow \mathcal {C} is given by (I, 1_\mathcal {C}, 1_\mathcal {C}, \lambda ), where \lambda : I \cdot - \to - is the left unitor of \mathcal {M}.
  4. The horizontal composition map is the composition in \mathsf {Para}: given M \cdot X \to Y, N \cdot Y \to Z, their composite is given by (N \otimes M) \cdot X \cong N \cdot (M \cdot X) \to N \cdot Y \to Z. The horizontal composition of 2-cells is defined analogously.

Moreover, if \mathcal {C} \to \mathcal {D} is strict homomorphism of \mathcal {M}-modules, there is an induced pseudofunctor \mathsf {\mathbb Para}_\mathcal {M}(\mathcal {C}) \to \mathsf {\mathbb Para}_\mathcal {M}(\mathcal {D}). If \mathcal {N} \to \mathcal {M} is a strict monoidal functor, then regarding \mathcal {C} as an \mathcal {N}-module along this map, there is an induced pseudofunctor \mathsf {\mathbb Para}_\mathcal {N}(\mathcal {C}) \to \mathsf {\mathbb Para}_\mathcal {M}(\mathcal {C}). These combine into a 2-functor \mathsf {Act}_s \to \mathsf {PsDbl}_s between the 2-category of actions and strictly linear functors and the category of pseudo double categories and strict double functors. This functor preserves (strict) limits.

Proof

Note that every actegory \mathcal {M} \curvearrowright \mathcal {C} is equivalent to a strict action of a strict monoidal category \mathcal {M}_s \curvearrowright \mathcal {C}_s (in the sense that there exists \mathcal {M}_s \xrightarrow {\sim } \mathcal {M} strong monoidal equivalence and \mathcal {C}_s \xrightarrow {\sim } \mathcal {C} an equivalence such that these maps together form a map of actegories). It follows that it suffices to show unitality and associativity for our composition in the strict case (since these are plainly preserved by equivalence).

Let \mathcal {M} \curvearrowright \mathcal {C}, \mathcal {M}' \curvearrowright \mathcal {C}', F: \mathcal {M} \to \mathcal {M}' be a strict monoidal functor, and let G: \mathcal {C} \to \mathcal {C}' be a linear functor "over F", that is a (strict) \mathcal {M}-linear functor when \mathcal {C}' is viewed as a \mathcal {M}-actegory along F. Then the induced functor \mathsf {\mathbb Para}_\mathcal {M}(\mathcal {C}) \to \mathsf {\mathbb Para}_{\mathcal {M}'}(\mathcal {C}') is given by G on the vertical category, and on the horizontal category by (M,X,X',\phi : M \cdot X \to X') \mapsto (F(M), G(X), G(X'), F(M) \cdot G(X) \simeq G(M \cdot X) \to G(X')) where the isomorphism is the linearity---noting that the M-action on \mathcal {C}' is precisely acting by F(M).

By naturality of the lineator it is straightforward to see that this is a functor, and it clearly preserves domain and codomain. It preserves units (strictly!) by the compatibility between the unitor and lineator. It remains to see that this preserves composition. For brevity, denote the induced functor H from here.

It suffices to verify this for strict actions. So the composite of M \cdot X \to Y, N \cdot Y \to Z is given by the composite (N \otimes M) \cdot X = N \cdot M \cdot X \to N \cdot Y \to Z.

Given two such composable maps, call them f,g, the two objects H(fg), H(f)H(g) are given by (F(M \otimes N), G(X), G(Z), \beta ), (F(M) \otimes F(N), G(X), G(Z), \alpha ) ,where \alpha , \beta are respectively the maps across the top and bottom of this diagram:

This proves that H preserves the composition strictly, as desired. (The rightmost triangle commutes by definition, and the leftmost rectangle is a lineator coherence)

Since the strict limits in \mathsf {PsDbl}_s and \mathsf {Act}_s are computed levelwise, it suffices to observe that the slice category also preserves limits, being a weighted limit itself.

Remark [efr-HUEE]

Note that \mathsf {\mathbb Para}_\mathcal {M}(\mathcal {C}) comes equipped with a strict functor to B\mathcal {M} (viewed as a double category). In fact, one can recover the action \cdot : \mathcal {M} \times \mathcal {C} \to \mathcal {C} from this data: the object M \cdot X is characterized up to isomorphism by its universal property: parametrized maps M \cdot X \nrightarrow Y with parameter N are in bijection with maps X \to Y parametrized by N \otimes M.