-
What kind of linearly distributive category do polynomial functors form?
Authors:
David I. Spivak,
Priyaa Varshinee Srinivasan
Abstract:
This paper has two purposes. The first is to extend the theory of linearly distributive categories by considering the structures that emerge in a special case: the normal duoidal category $(\mathsf{Poly} ,\mathcal{y}, \otimes, \triangleleft )$ of polynomial functors under Dirichlet and substitution product. This is an isomix LDC which is neither $*$-autonomous nor fully symmetric. The additional s…
▽ More
This paper has two purposes. The first is to extend the theory of linearly distributive categories by considering the structures that emerge in a special case: the normal duoidal category $(\mathsf{Poly} ,\mathcal{y}, \otimes, \triangleleft )$ of polynomial functors under Dirichlet and substitution product. This is an isomix LDC which is neither $*$-autonomous nor fully symmetric. The additional structures of interest here are a closure for $\otimes$ and a co-closure for $\triangleleft$, making $\mathsf{Poly}$ a bi-closed LDC, which is a notion we introduce in this paper.
The second purpose is to use $\mathsf{Poly}$ as a source of examples and intuition about various structures that can occur in the setting of LDCs, including duals, cores, linear monoids, and others, as well as how these generalize to the non-symmetric setting. To that end, we characterize the linearly dual objects in $\mathsf{Poly}$: every linear polynomial has a right dual which is a representable. It turns out that the linear and representable polynomials also form the left and right cores of $\mathsf{Poly}$. Finally, we provide examples of linear monoids, linear comonoids, and linear bialgebras in $\mathsf{Poly}$.
△ Less
Submitted 1 July, 2024;
originally announced July 2024.
-
A Polynomial Construction of Nerves for Higher Categories
Authors:
Brandon T. Shapiro,
David I. Spivak
Abstract:
We show that the construction due to Leinster and Weber of a generalized Lawvere theory for a familially representable monad on a (co)presheaf category, and the associated ``nerve'' functor from monad algebras to (co)presheaves, have an elegant categorical description in the double category $\mathbb{C}\mathbf{at}^{\#}$ of categories, cofunctors, familial functors, and transformations. In…
▽ More
We show that the construction due to Leinster and Weber of a generalized Lawvere theory for a familially representable monad on a (co)presheaf category, and the associated ``nerve'' functor from monad algebras to (co)presheaves, have an elegant categorical description in the double category $\mathbb{C}\mathbf{at}^{\#}$ of categories, cofunctors, familial functors, and transformations. In $\mathbb{C}\mathbf{at}^{\#}$, which also arises from comonoids in the category of polynomial functors, both a familial monad and a (co)presheaf it acts on can be modeled as horizontal morphisms; from this perspective, the theory category associated to the monad is built using left Kan extension in the category of endomorphisms, and the nerve functor is modeled by a single composition of horizontal morphisms in $\mathbb{C}\mathbf{at}^{\#}$. For the free category monad $path$ on graphs, this provides a new construction of the simplex category as $Δ:= \lens{path}{path \circ path}$. We also explore the free Eilenberg-Moore completion of $\mathbb{C}\mathbf{at}^{\#}$, in which constructions such as the free symmetric monoidal category monad on $\mathbf{Cat}$ can modeled using the rich language of polynomial functors.
△ Less
Submitted 21 May, 2024;
originally announced May 2024.
-
Pattern runs on matter: The free monad monad as a module over the cofree comonad comonad
Authors:
Sophie Libkind,
David I. Spivak
Abstract:
Interviews run on people, programs run on operating systems, voting schemes run on voters, games run on players. Each of these is an example of the abstraction pattern runs on matter. Pattern determines the decision tree that governs how a situation can unfold, while matter responds with decisions at each juncture.
In this article, we will give a straightforward and concrete construction of the…
▽ More
Interviews run on people, programs run on operating systems, voting schemes run on voters, games run on players. Each of these is an example of the abstraction pattern runs on matter. Pattern determines the decision tree that governs how a situation can unfold, while matter responds with decisions at each juncture.
In this article, we will give a straightforward and concrete construction of the free monad monad for $(\mathbf{Poly}, \mathbin{\triangleleft}, \mathcal{y})$, the category of polynomial functors with the substitution monoidal product. Although the free monad has been well-studied in other contexts, the construction we give is streamlined and explicitly illustrates how the free monad represents terminating decision trees. We will also explore the naturally arising interaction between the free monad and cofree comonad. Again, while the interaction itself is known, the perspective we take is the free monad as a module over the cofree comonad. Lastly, we will give four applications of the module action to interviews, computer programs, voting, and games. In each example, we will see how the free monad represents pattern, the cofree comonad represents matter, and the module action represents runs on.
△ Less
Submitted 24 April, 2024;
originally announced April 2024.
-
Organizing Physics with Open Energy-Driven Systems
Authors:
Matteo Capucci,
Owen Lynch,
David I. Spivak
Abstract:
Organizing physics has been a long-standing preoccupation of applied category theory, going back at least to Lawvere. We contribute to this research thread by noticing that Hamiltonian mechanics and gradient descent depend crucially on a consistent choice of transformation -- which we call a reaction structure -- from the cotangent bundle to the tangent bundle. We then construct a compositional th…
▽ More
Organizing physics has been a long-standing preoccupation of applied category theory, going back at least to Lawvere. We contribute to this research thread by noticing that Hamiltonian mechanics and gradient descent depend crucially on a consistent choice of transformation -- which we call a reaction structure -- from the cotangent bundle to the tangent bundle. We then construct a compositional theory of reaction structures. Reaction-based systems offer a different perspective on composition in physics than port-Hamiltonian systems or open classical mechanics, in that reaction-based composition does not create any new constraints that must be solved for algebraically.
The technical contributions of this paper are the development of symmetric monoidal categories of open energy-driven systems and open differential equations, and a functor between them, functioning as a "functorial semantics" for reaction structures. This approach echoes what has previously been done for open games and open gradient-based learners, and in fact subsumes the latter. We then illustrate our theory by constructing an $n$-fold pendulum as a composite of $n$-many pendula.
△ Less
Submitted 24 April, 2024;
originally announced April 2024.
-
Polynomial Functors: A Mathematical Theory of Interaction
Authors:
Nelson Niu,
David I. Spivak
Abstract:
This monograph is a study of the category of polynomial endofunctors on the category of sets and its applications to modeling interaction protocols and dynamical systems. We assume basic categorical background and build the categorical theory from the ground up, highlighting pictorical techniques and concrete examples to build intuition and provide applications.
This monograph is a study of the category of polynomial endofunctors on the category of sets and its applications to modeling interaction protocols and dynamical systems. We assume basic categorical background and build the categorical theory from the ground up, highlighting pictorical techniques and concrete examples to build intuition and provide applications.
△ Less
Submitted 1 December, 2023;
originally announced December 2023.
-
All Concepts are $\mathbb{C}\mathbf{at}^\#$
Authors:
Owen Lynch,
Brandon T. Shapiro,
David I. Spivak
Abstract:
We show that the double category $\mathbb{C}\mathbf{at}^\#$ of comonoids in the category of polynomial functors (previously shown by Ahman-Uustalu and Garner to be equivalent to the double category of categories, cofunctors, and prafunctors) contains several formal settings for basic category theory and has subcategories equivalent to both the double category $\mathbb{O}\mathbf{rg}$ of dynamic rew…
▽ More
We show that the double category $\mathbb{C}\mathbf{at}^\#$ of comonoids in the category of polynomial functors (previously shown by Ahman-Uustalu and Garner to be equivalent to the double category of categories, cofunctors, and prafunctors) contains several formal settings for basic category theory and has subcategories equivalent to both the double category $\mathbb{O}\mathbf{rg}$ of dynamic rewiring systems and the double category $\mathbb{P}\mathbf{oly}_{\mathcal{E}}$ of generalized polynomials in a finite limit category $\mathcal{E}$. Also serving as a natural setting for categorical database theory and generalized higher category theory, $\mathbb{C}\mathbf{at}^\#$ at once hosts models of a wide range of concepts from the theory and applications of polynomial functors and category theory.
△ Less
Submitted 23 May, 2024; v1 submitted 4 May, 2023;
originally announced May 2023.
-
Structures on Categories of Polynomials
Authors:
Brandon T. Shapiro,
David I. Spivak
Abstract:
We define the monoidal category $(Poly_E,y,\triangleleft)$ of polynomials under composition in any category $E$ with finite limits, including both cartesian and vertical morphisms of polynomials, and generalize to this setting the Dirichlet tensor product of polynomials $\otimes$, duoidality of $\otimes$ and $\triangleleft$, closure of $\otimes$, and coclosures of $\triangleleft$. We also prove th…
▽ More
We define the monoidal category $(Poly_E,y,\triangleleft)$ of polynomials under composition in any category $E$ with finite limits, including both cartesian and vertical morphisms of polynomials, and generalize to this setting the Dirichlet tensor product of polynomials $\otimes$, duoidality of $\otimes$ and $\triangleleft$, closure of $\otimes$, and coclosures of $\triangleleft$. We also prove that $\triangleleft$-comonoids in $Poly_E$ are precisely the internal categories in $E$ whose source morphism is exponentiable, generalizing a result of Ahman-Uustalu equating categories with polynomial comonads, and show that coalgebras in this setting correspond to internal copresheaves. Finally, the double category of ``typed'' polynomials in $E$ is recovered using $\triangleleft$-bicomodules in $Poly_E$.
△ Less
Submitted 18 May, 2023; v1 submitted 29 April, 2023;
originally announced May 2023.
-
Dynamic Tracing: a graphical language for rewriting protocols
Authors:
Kristopher Brown,
David I. Spivak
Abstract:
The category Set_* of sets and partial functions is well-known to be traced monoidal, meaning that a partial function S+U -/-> T+U can be coherently transformed into a partial function S -/-> T. This transformation is generally described in terms of an implicit procedure that must be run. We make this procedure explicit by enriching the traced category in Cat#, the symmetric monoidal category of c…
▽ More
The category Set_* of sets and partial functions is well-known to be traced monoidal, meaning that a partial function S+U -/-> T+U can be coherently transformed into a partial function S -/-> T. This transformation is generally described in terms of an implicit procedure that must be run. We make this procedure explicit by enriching the traced category in Cat#, the symmetric monoidal category of categories and cofunctors: each hom-category has such procedures as objects, and advancement through the procedures as arrows. We also generalize to traced Kleisli categories beyond Set_*, providing a conjectural trace operator for the Kleisli category of any polynomial monad of the form t+1. The main motivation for this work is to give a formal and graphical syntax for performing sophisticated computations powered by graph rewriting, which is itself a graphical language for data transformation.
△ Less
Submitted 1 May, 2023; v1 submitted 24 April, 2023;
originally announced April 2023.
-
Algebraic Model Management: A Survey
Authors:
Patrick Schultz,
David I. Spivak,
Ryan Wisnesky
Abstract:
We survey the field of model management and describe a new model management approach based on algebraic specification.
We survey the field of model management and describe a new model management approach based on algebraic specification.
△ Less
Submitted 12 January, 2023;
originally announced January 2023.
-
Duoidal Structures for Compositional Dependence
Authors:
Brandon T. Shapiro,
David I. Spivak
Abstract:
We provide a categorical framework for mathematical objects for which there is both a sort of "independent" and "dependent" composition. Namely we model them as duoidal categories in which both monoidal structures share a unit and the first is symmetric. We construct the free such category and observe that it is a full subcategory of the category of finite posets. Indeed each algebraic expression…
▽ More
We provide a categorical framework for mathematical objects for which there is both a sort of "independent" and "dependent" composition. Namely we model them as duoidal categories in which both monoidal structures share a unit and the first is symmetric. We construct the free such category and observe that it is a full subcategory of the category of finite posets. Indeed each algebraic expression in the two monoidal operators corresponds to the poset built by taking disjoint unions and joins of the singleton poset. We characterize these "expressible" posets as precisely those which contain no "zig-zags." We then move on to describe categories equipped with $n$-ary operations for each $n$-element finite poset; we refer to them as "dependence categories" since they allow for combinations of objects based on any network of dependencies between them.
These structures model various sorts of dependence including the space-like and time-like juxtaposition of weighted probability distributions in relativistic spacetime, which we model using polynomial endofunctors on the category of sets, as well as the runtimes for multiple computer programs run in parallel and series, which we model using the tropical semiring structure on nonnegative real numbers. With these examples in mind, we conclude by describing ways in which morphisms in a partial monoidal category can be "decorated" in a coherent manner by objects in a dependence category, such as labeling a network of parallel programs with their runtimes.
△ Less
Submitted 4 October, 2022;
originally announced October 2022.
-
Dynamic Operads, Dynamic Categories: From Deep Learning to Prediction Markets
Authors:
Brandon T. Shapiro,
David I. Spivak
Abstract:
Natural organized systems adapt to internal and external pressures and this happens at all levels of the abstraction hierarchy. Wanting to think clearly about this idea motivates our paper, and so the idea is elaborated extensively in the introduction, which should be broadly accessible to a philosophically-interested audience. In the remaining sections, we turn to more compressed category theory.…
▽ More
Natural organized systems adapt to internal and external pressures and this happens at all levels of the abstraction hierarchy. Wanting to think clearly about this idea motivates our paper, and so the idea is elaborated extensively in the introduction, which should be broadly accessible to a philosophically-interested audience. In the remaining sections, we turn to more compressed category theory. We define the monoidal double category Org of dynamic organizations, we provide definitions of Org-enriched, or dynamic, categorical structures -- e.g. dynamic categories, operads, and monoidal categories -- and we show how they instantiate the motivating philosophical ideas. We give two examples of dynamic categorical structures: prediction markets as a dynamic operad and deep learning as a dynamic monoidal category.
△ Less
Submitted 31 July, 2023; v1 submitted 8 May, 2022;
originally announced May 2022.
-
Fast Left Kan Extensions Using The Chase
Authors:
Joshua Meyers,
David I. Spivak,
Ryan Wisnesky
Abstract:
We show how computation of left Kan extensions can be reduced to computation of free models of cartesian (finite-limit) theories. We discuss how the standard and parallel chase compute weakly free models of regular theories and free models of cartesian theories, and compare the concept of "free model" with a similar concept from database theory known as "universal model". We prove that, as algorit…
▽ More
We show how computation of left Kan extensions can be reduced to computation of free models of cartesian (finite-limit) theories. We discuss how the standard and parallel chase compute weakly free models of regular theories and free models of cartesian theories, and compare the concept of "free model" with a similar concept from database theory known as "universal model". We prove that, as algorithms for computing finite free models of cartesian theories, the standard and parallel chase are complete under fairness assumptions. Finally, we describe an optimized implementation of the parallel chase specialized to left Kan extensions that achieves an order of magnitude improvement in our performance benchmarks compared to the next fastest left Kan extension algorithm we are aware of.
△ Less
Submitted 4 May, 2022;
originally announced May 2022.
-
Generalized Interference of Fermions and Bosons
Authors:
Dylan Spivak,
Murphy Yuezhen Niu,
Barry C. Sanders,
Hubert de Guise
Abstract:
Using tools from representation theory, we derive expressions for the coincidence rate of partially-distinguishable particles in an interferometry experiment. Our expressions are valid for either bosons or fermions, and for any number of particles. In an experiment with $n$ particles the expressions we derive contain a term for each partition of the integer $n$; Gamas's theorem is used to determin…
▽ More
Using tools from representation theory, we derive expressions for the coincidence rate of partially-distinguishable particles in an interferometry experiment. Our expressions are valid for either bosons or fermions, and for any number of particles. In an experiment with $n$ particles the expressions we derive contain a term for each partition of the integer $n$; Gamas's theorem is used to determine which of these terms are automatically zero based on the pairwise level of distinguishability between particles. Most sampling schemes (such as Boson Sampling) are limited to completely indistinguishable particles; our work aids in the understanding of systems where an arbitrary level of distinguishability is permitted. As an application of our work we introduce a sampling scheme with partially-distinguishable fermions, which we call Generalized Fermion Sampling.
△ Less
Submitted 11 March, 2022;
originally announced March 2022.
-
A reference for categorical structures on $\mathbf{Poly}$
Authors:
David I. Spivak
Abstract:
In this document, we collect a list of categorical structures on the category $\mathbf{Poly}$ of polynomial functors. There is no implied claim that this list is in any way complete. It includes: infinitely many monoidal structures, all but one of which is symmetric, closed, and distributes over $+$, several of which interact duoidally; it also includes a right-coclosure and two indexed left coclo…
▽ More
In this document, we collect a list of categorical structures on the category $\mathbf{Poly}$ of polynomial functors. There is no implied claim that this list is in any way complete. It includes: infinitely many monoidal structures, all but one of which is symmetric, closed, and distributes over $+$, several of which interact duoidally; it also includes a right-coclosure and two indexed left coclosures; it also includes various adjunctions of which $\mathbf{Poly}$ is a part, including the free monad and cofree comonad and their interaction with various monoidal structures.
△ Less
Submitted 4 May, 2024; v1 submitted 1 February, 2022;
originally announced February 2022.
-
Polynomial Functors and Shannon Entropy
Authors:
David I. Spivak
Abstract:
Past work shows that one can associate a notion of Shannon entropy to a Dirichlet polynomial, regarded as an empirical distribution. Indeed, entropy can be extracted from any d:Dir by a two-step process, where the first step is a rig homomorphism out of Dir, the *set* of Dirichlet polynomials, with rig structure given by standard addition and multiplication. In this short note, we show that this r…
▽ More
Past work shows that one can associate a notion of Shannon entropy to a Dirichlet polynomial, regarded as an empirical distribution. Indeed, entropy can be extracted from any d:Dir by a two-step process, where the first step is a rig homomorphism out of Dir, the *set* of Dirichlet polynomials, with rig structure given by standard addition and multiplication. In this short note, we show that this rig homomorphism can be upgraded to a rig *functor*, when we replace the set of Dirichlet polynomials by the *category* of ordinary (Cartesian) polynomials.
In the Cartesian case, the process has three steps. The first step is a rig functor PolyCart -> Poly sending a polynomial p to (dp)y, where dp is the derivative of p. The second is a rig functor Poly -> Set x Set^op, sending a polynomial q to the pair (q(1),Gamma(q)), where Gamma(q)=Poly(q,y) can be interpreted as the global sections of q viewed as a bundle, and q(1) as its base. To make this precise we define what appears to be a new distributive monoidal structure on Set x Set^op, which can be understood geometrically in terms of rectangles. The last step, as for Dirichlet polynomials, is simply to extract the entropy as a real number from a pair of sets (A,B); it is given by log A - log B^(1/A) and can be thought of as the log aspect ratio of the rectangle.
△ Less
Submitted 31 July, 2023; v1 submitted 30 January, 2022;
originally announced January 2022.
-
Collectives: Compositional protocols for contributions and returns
Authors:
Nelson Niu,
David I. Spivak
Abstract:
We introduce a concept called a collective: an interface with a protocol for aggregating contributions and distributing returns. Through such a protocol, many members may participate in a mutual endeavor. We present a variety of real-world examples of collectives to explore the many kinds of things that members can contribute (such as time, work, ideas, or resources) as well as the many ways these…
▽ More
We introduce a concept called a collective: an interface with a protocol for aggregating contributions and distributing returns. Through such a protocol, many members may participate in a mutual endeavor. We present a variety of real-world examples of collectives to explore the many kinds of things that members can contribute (such as time, work, ideas, or resources) as well as the many ways these contributions can be aggregated and returns distributed. In addition, we illustrate several ways in which new collectives can be constructed from old, alluding to the fact that all these constructions have a natural mathematical description within the category of polynomial functors equipped with a certain monoidal structure.
△ Less
Submitted 27 January, 2022; v1 submitted 21 December, 2021;
originally announced December 2021.
-
Functorial aggregation
Authors:
David I. Spivak
Abstract:
Aggregating data in a database could also be called "integrating along fibers": given functions $π\colon E\to D$ and $s\colon E\to R$, where $(R,\circledast)$ is a commutative monoid, we want a new function $(\circledast s)_π$ that sends each $d\in D$ to the "sum" of all $s(e)$ for which $π(e)=d$. The operation lives alongside querying -- or more generally data migration -- in typical database usa…
▽ More
Aggregating data in a database could also be called "integrating along fibers": given functions $π\colon E\to D$ and $s\colon E\to R$, where $(R,\circledast)$ is a commutative monoid, we want a new function $(\circledast s)_π$ that sends each $d\in D$ to the "sum" of all $s(e)$ for which $π(e)=d$. The operation lives alongside querying -- or more generally data migration -- in typical database usage: one wants to know how much Canadians spent on cell phones in 2021, for example, and such requests typically require both aggregation and querying. But whereas querying has an elegant category-theoretic treatment in terms of parametric right adjoints between copresheaf categories, a categorical formulation of aggregation -- especially one that lives alongside that for querying -- appears to be completely absent from the literature.
In this paper we show how both querying and aggregation fit into the "polynomial ecosystem". Starting with the category $\mathbf{Poly}$ of polynomial functors in one variable, we review the relatively recent results of Ahman-Uustalu and Garner, which showed that the framed bicategory $\mathbb{C}\mathbf{at}^\sharp$ of comonads in $\mathbf{Poly}$ is precisely the right setting for data migration: its objects are categories and its bicomodules are parametric right adjoints between their copresheaf categories. We then develop a great deal of theory, compressed for space reasons, including local monoidal closed structures, a coclosure to bicomodule composition, and an understanding of adjoints in $\mathbb{C}\mathbf{at}^\sharp$. Doing so allows us to derive interesting mathematical results, e.g.\ that the ordinary operation of transposing a span can be decomposed into the composite of two more primitive operations, and then finally to explain how aggregation arises, alongside querying, in $\mathbb{C}\mathbf{at}^\sharp$.
△ Less
Submitted 12 June, 2023; v1 submitted 21 November, 2021;
originally announced November 2021.
-
Deep neural networks as nested dynamical systems
Authors:
David I. Spivak,
Timothy Hosgood
Abstract:
There is an analogy that is often made between deep neural networks and actual brains, suggested by the nomenclature itself: the "neurons" in deep neural networks should correspond to neurons (or nerve cells, to avoid confusion) in the brain. We claim, however, that this analogy doesn't even type check: it is structurally flawed. In agreement with the slightly glib summary of Hebbian learning as "…
▽ More
There is an analogy that is often made between deep neural networks and actual brains, suggested by the nomenclature itself: the "neurons" in deep neural networks should correspond to neurons (or nerve cells, to avoid confusion) in the brain. We claim, however, that this analogy doesn't even type check: it is structurally flawed. In agreement with the slightly glib summary of Hebbian learning as "cells that fire together wire together", this article makes the case that the analogy should be different. Since the "neurons" in deep neural networks are managing the changing weights, they are more akin to the synapses in the brain; instead, it is the wires in deep neural networks that are more like nerve cells, in that they are what cause the information to flow. An intuition that nerve cells seem like more than mere wires is exactly right, and is justified by a precise category-theoretic analogy which we will explore in this article. Throughout, we will continue to highlight the error in equating artificial neurons with nerve cells by leaving "neuron" in quotes or by calling them artificial neurons.
We will first explain how to view deep neural networks as nested dynamical systems with a very restricted sort of interaction pattern, and then explain a more general sort of interaction for dynamical systems that is useful throughout engineering, but which fails to adapt to changing circumstances. As mentioned, an analogy is then forced upon us by the mathematical formalism in which they are both embedded. We call the resulting encompassing generalization deeply interacting learning systems: they have complex interaction as in control theory, but adaptation to circumstances as in deep neural networks.
△ Less
Submitted 1 November, 2021;
originally announced November 2021.
-
Regular Calculi I: Graphical Regular Logic
Authors:
Tslil Clingman,
Brendan Fong,
David I. Spivak
Abstract:
What is ergonomic syntax for relations? In this first paper in a series of two, to answer the question we define regular calculi: a suitably structured functor from a category representing the syntax of regular logic to the category of posets, that takes each object to the poset of relations on that type. We introduce two major classes of examples, regular calculi corresponding to regular theories…
▽ More
What is ergonomic syntax for relations? In this first paper in a series of two, to answer the question we define regular calculi: a suitably structured functor from a category representing the syntax of regular logic to the category of posets, that takes each object to the poset of relations on that type. We introduce two major classes of examples, regular calculi corresponding to regular theories, and regular calculi corresponding to regular categories. For working in regular calculi, we present a graphical framework which takes as primitive the various moves of regular logic. Our main theorem for regular calculi is a syntax-semantics $2$-dimensional adjunction to regular categories.
△ Less
Submitted 28 September, 2021;
originally announced September 2021.
-
Dirichlet polynomials and entropy
Authors:
David I. Spivak,
Timothy Hosgood
Abstract:
A Dirichlet polynomial $d$ in one variable ${\mathcal{y}}$ is a function of the form $d({\mathcal{y}})=a_n n^{\mathcal{y}}+\cdots+a_22^{\mathcal{y}}+a_11^{\mathcal{y}}+a_00^{\mathcal{y}}$ for some $n,a_0,\ldots,a_n\in\mathbb{N}$. We will show how to think of a Dirichlet polynomial as a set-theoretic bundle, and thus as an empirical distribution. We can then consider the Shannon entropy $H(d)$ of t…
▽ More
A Dirichlet polynomial $d$ in one variable ${\mathcal{y}}$ is a function of the form $d({\mathcal{y}})=a_n n^{\mathcal{y}}+\cdots+a_22^{\mathcal{y}}+a_11^{\mathcal{y}}+a_00^{\mathcal{y}}$ for some $n,a_0,\ldots,a_n\in\mathbb{N}$. We will show how to think of a Dirichlet polynomial as a set-theoretic bundle, and thus as an empirical distribution. We can then consider the Shannon entropy $H(d)$ of the corresponding probability distribution, and we define its length (or, classically, its perplexity) by $L(d)=2^{H(d)}$. On the other hand, we will define a rig homomorphism $h\colon\mathsf{Dir}\to\mathsf{Rect}$ from the rig of Dirichlet polynomials to the so-called rectangle rig, whose underlying set is $\mathbb{R}_{\geq0}\times\mathbb{R}_{\geq0}$ and whose additive structure involves the weighted geometric mean; we write $h(d)=(A(d),W(d))$, and call the two components area and width (respectively).
The main result of this paper is the following: the rectangle-area formula $A(d)=L(d)W(d)$ holds for any Dirichlet polynomial $d$. In other words, the entropy of an empirical distribution can be calculated entirely in terms of the homomorphism $h$ applied to its corresponding Dirichlet polynomial. We also show that similar results hold for the cross entropy.
△ Less
Submitted 28 October, 2021; v1 submitted 10 July, 2021;
originally announced July 2021.
-
Learners' Languages
Authors:
David I. Spivak
Abstract:
In "Backprop as functor", the authors show that the fundamental elements of deep learning -- gradient descent and backpropagation -- can be conceptualized as a strong monoidal functor Para(Euc)$\to$Learn from the category of parameterized Euclidean spaces to that of learners, a category developed explicitly to capture parameter update and backpropagation. It was soon realized that there is an isom…
▽ More
In "Backprop as functor", the authors show that the fundamental elements of deep learning -- gradient descent and backpropagation -- can be conceptualized as a strong monoidal functor Para(Euc)$\to$Learn from the category of parameterized Euclidean spaces to that of learners, a category developed explicitly to capture parameter update and backpropagation. It was soon realized that there is an isomorphism Learn$\cong$Para(Slens), where Slens is the symmetric monoidal category of simple lenses as used in functional programming.
In this note, we observe that Slens is a full subcategory of Poly, the category of polynomial functors in one variable, via the functor $A\mapsto Ay^A$. Using the fact that (Poly,$\otimes$) is monoidal closed, we show that a map $A\to B$ in Para(Slens) has a natural interpretation in terms of dynamical systems (more precisely, generalized Moore machines) whose interface is the internal-hom type $[Ay^A,By^B]$.
Finally, we review the fact that the category p-Coalg of dynamical systems on any $p \in$ Poly forms a topos, and consider the logical propositions that can be stated in its internal language. We give gradient descent as an example, and we conclude by discussing some directions for future work.
△ Less
Submitted 3 November, 2022; v1 submitted 1 March, 2021;
originally announced March 2021.
-
Wiring diagrams as normal forms for computing in symmetric monoidal categories
Authors:
Evan Patterson,
David I. Spivak,
Dmitry Vagner
Abstract:
Applications of category theory often involve symmetric monoidal categories (SMCs), in which abstract processes or operations can be composed in series and parallel. However, in 2020 there remains a dearth of computational tools for working with SMCs. We present an "unbiased" approach to implementing symmetric monoidal categories, based on an operad of directed, acyclic wiring diagrams. Because t…
▽ More
Applications of category theory often involve symmetric monoidal categories (SMCs), in which abstract processes or operations can be composed in series and parallel. However, in 2020 there remains a dearth of computational tools for working with SMCs. We present an "unbiased" approach to implementing symmetric monoidal categories, based on an operad of directed, acyclic wiring diagrams. Because the interchange law and other laws of a SMC hold identically in a wiring diagram, no rewrite rules are needed to compare diagrams. We discuss the mathematics of the operad of wiring diagrams, as well as its implementation in the software package Catlab.
△ Less
Submitted 25 January, 2021;
originally announced January 2021.
-
Behavioral Mereology: A Modal Logic for Passing Constraints
Authors:
Brendan Fong,
David Jaz Myers,
David I. Spivak
Abstract:
Mereology is the study of parts and the relationships that hold between them. We introduce a behavioral approach to mereology, in which systems and their parts are known only by the types of behavior they can exhibit. Our discussion is formally topos-theoretic, and agnostic to the topos, providing maximal generality; however, by using only its internal logic we can hide the details and readers may…
▽ More
Mereology is the study of parts and the relationships that hold between them. We introduce a behavioral approach to mereology, in which systems and their parts are known only by the types of behavior they can exhibit. Our discussion is formally topos-theoretic, and agnostic to the topos, providing maximal generality; however, by using only its internal logic we can hide the details and readers may assume a completely elementary set-theoretic discussion. We consider the relationship between various parts of a whole in terms of how behavioral constraints are passed between them, and give an inter-modal logic that generalizes the usual alethic modalities in the setting of symmetric accessibility.
△ Less
Submitted 25 January, 2021;
originally announced January 2021.
-
A Compositional Sheaf-Theoretic Framework for Event-Based Systems
Authors:
Gioele Zardini,
David I. Spivak,
Andrea Censi,
Emilio Frazzoli
Abstract:
A compositional sheaf-theoretic framework for the modeling of complex event-based systems is presented. We show that event-based systems are machines, with inputs and outputs, and that they can be composed with machines of different types, all within a unified, sheaf-theoretic formalism. We take robotic systems as an exemplar of complex systems and rigorously describe actuators, sensors, and algor…
▽ More
A compositional sheaf-theoretic framework for the modeling of complex event-based systems is presented. We show that event-based systems are machines, with inputs and outputs, and that they can be composed with machines of different types, all within a unified, sheaf-theoretic formalism. We take robotic systems as an exemplar of complex systems and rigorously describe actuators, sensors, and algorithms using this framework.
△ Less
Submitted 25 January, 2021;
originally announced January 2021.
-
Proceedings of the 3rd Annual International Applied Category Theory Conference 2020
Authors:
David I. Spivak,
Jamie Vicary
Abstract:
The third annual International Applied Category Theory Conference (ACT2020) was planned to take place at MIT in Cambridge, Massachusetts USA. However, the global COVID-19 pandemic made the prospect of holding a large in-person meeting impossible, and the event was thus held completely online. Holding the talks online had the new benefits of reducing carbon footprint, being inclusive of people from…
▽ More
The third annual International Applied Category Theory Conference (ACT2020) was planned to take place at MIT in Cambridge, Massachusetts USA. However, the global COVID-19 pandemic made the prospect of holding a large in-person meeting impossible, and the event was thus held completely online. Holding the talks online had the new benefits of reducing carbon footprint, being inclusive of people from more parts of the world, and producing higher-quality video talks, which have been posted online for posterity.
The ACT2020 contributions spanned a broad spectrum of application areas, including databases, dynamical systems, functional programming, game theory, lenses, neuroscience, probabilistic programming, natural language processing, quantum mechanics, and cyberphysical systems. Papers featured a broad range of categorical techniques.
Papers in this Proceedings volume represents about half of the talks presented at ACT2020. Being included in the proceedings vs. not is not an indication of talk quality, but instead almost exclusively the choice of the authors, e.g. to present work already published elsewhere.
△ Less
Submitted 19 January, 2021;
originally announced January 2021.
-
Monitoring and Diagnosability of Perception Systems
Authors:
Pasquale Antonante,
David I. Spivak,
Luca Carlone
Abstract:
Perception is a critical component of high-integrity applications of robotics and autonomous systems, such as self-driving vehicles. In these applications, failure of perception systems may put human life at risk, and a broad adoption of these technologies requires the development of methodologies to guarantee and monitor safe operation. Despite the paramount importance of perception systems, curr…
▽ More
Perception is a critical component of high-integrity applications of robotics and autonomous systems, such as self-driving vehicles. In these applications, failure of perception systems may put human life at risk, and a broad adoption of these technologies requires the development of methodologies to guarantee and monitor safe operation. Despite the paramount importance of perception systems, currently there is no formal approach for system-level monitoring. In this work, we propose a mathematical model for runtime monitoring and fault detection and identification in perception systems. Towards this goal, we draw connections with the literature on diagnosability in multiprocessor systems, and generalize it to account for modules with heterogeneous outputs that interact over time. The resulting temporal diagnostic graphs (i) provide a framework to reason over the consistency of perception outputs -- across modules and over time -- thus enabling fault detection, (ii) allow us to establish formal guarantees on the maximum number of faults that can be uniquely identified in a given perception system, and (iii) enable the design of efficient algorithms for fault identification. We demonstrate our monitoring system, dubbed PerSyS, in realistic simulations using the LGSVL self-driving simulator and the Apollo Auto autonomy software stack, and show that PerSyS is able to detect failures in challenging scenarios (including scenarios that have caused self-driving car accidents in recent years), and is able to correctly identify faults while entailing a minimal computation overhead (< 5 ms on a single-core CPU).
△ Less
Submitted 16 October, 2021; v1 submitted 11 November, 2020;
originally announced November 2020.
-
String Diagrams for Regular Logic (Extended Abstract)
Authors:
Brendan Fong,
David Spivak
Abstract:
Regular logic can be regarded as the internal language of regular categories, but the logic itself is generally not given a categorical treatment. In this paper, we understand the syntax and proof rules of regular logic in terms of the free regular category FRg(T) on a set T. From this point of view, regular theories are certain monoidal 2-functors from a suitable 2-category of contexts -- the 2-c…
▽ More
Regular logic can be regarded as the internal language of regular categories, but the logic itself is generally not given a categorical treatment. In this paper, we understand the syntax and proof rules of regular logic in terms of the free regular category FRg(T) on a set T. From this point of view, regular theories are certain monoidal 2-functors from a suitable 2-category of contexts -- the 2-category of relations in FRg(T) -- to that of posets. Such functors assign to each context the set of formulas in that context, ordered by entailment. We refer to such a 2-functor as a regular calculus because it naturally gives rise to a graphical string diagram calculus in the spirit of Joyal and Street. We shall show that every natural category has an associated regular calculus, and conversely from every regular calculus one can construct a regular category.
△ Less
Submitted 14 September, 2020;
originally announced September 2020.
-
Monitoring and Diagnosability of Perception Systems
Authors:
Pasquale Antonante,
David I. Spivak,
Luca Carlone
Abstract:
Perception is a critical component of high-integrity applications of robotics and autonomous systems, such as self-driving cars. In these applications, failure of perception systems may put human life at risk, and a broad adoption of these technologies relies on the development of methodologies to guarantee and monitor safe operation as well as detect and mitigate failures. Despite the paramount i…
▽ More
Perception is a critical component of high-integrity applications of robotics and autonomous systems, such as self-driving cars. In these applications, failure of perception systems may put human life at risk, and a broad adoption of these technologies relies on the development of methodologies to guarantee and monitor safe operation as well as detect and mitigate failures. Despite the paramount importance of perception systems, currently there is no formal approach for system-level monitoring. In this work, we propose a mathematical model for runtime monitoring and fault detection of perception systems. Towards this goal, we draw connections with the literature on self-diagnosability for multiprocessor systems, and generalize it to (i) account for modules with heterogeneous outputs, and (ii) add a temporal dimension to the problem, which is crucial to model realistic perception systems where modules interact over time. This contribution results in a graph-theoretic approach that, given a perception system, is able to detect faults at runtime and allows computing an upper-bound on the number of faulty modules that can be detected. Our second contribution is to show that the proposed monitoring approach can be elegantly described with the language of topos theory, which allows formulating diagnosability over arbitrary time intervals.
△ Less
Submitted 16 November, 2020; v1 submitted 24 May, 2020;
originally announced May 2020.
-
A Compositional Sheaf-Theoretic Framework for Event-Based Systems (Extended Version)
Authors:
Gioele Zardini,
David I. Spivak,
Andrea Censi,
Emilio Frazzoli
Abstract:
A compositional sheaf-theoretic framework for the modeling of complex event-based systems is presented. We show that event-based systems are machines, with inputs and outputs, and that they can be composed with machines of different types, all within a unified, sheaf-theoretic formalism. We take robotic systems as an exemplar of complex systems and rigorously describe actuators, sensors, and algor…
▽ More
A compositional sheaf-theoretic framework for the modeling of complex event-based systems is presented. We show that event-based systems are machines, with inputs and outputs, and that they can be composed with machines of different types, all within a unified, sheaf-theoretic formalism. We take robotic systems as an exemplar of complex systems and rigorously describe actuators, sensors, and algorithms using this framework.
△ Less
Submitted 22 June, 2020; v1 submitted 10 May, 2020;
originally announced May 2020.
-
Poly: An abundant categorical setting for mode-dependent dynamics
Authors:
David I. Spivak
Abstract:
Dynamical systems---by which we mean machines that take time-varying input, change their state, and produce output---can be wired together to form more complex systems. Previous work has shown how to allow collections of machines to reconfigure their wiring diagram dynamically, based on their collective state. This notion was called "mode dependence", and while the framework was compositional (for…
▽ More
Dynamical systems---by which we mean machines that take time-varying input, change their state, and produce output---can be wired together to form more complex systems. Previous work has shown how to allow collections of machines to reconfigure their wiring diagram dynamically, based on their collective state. This notion was called "mode dependence", and while the framework was compositional (forming an operad of re-wiring diagrams and algebra of mode-dependent dynamical systems on it), the formulation itself was more "creative" than it was natural.
In this paper we show that the theory of mode-dependent dynamical systems can be more naturally recast within the category Poly of polynomial functors. This category is almost superlatively abundant in its structure: for example, it has \emph{four} interacting monoidal structures $(+,\times,\otimes,\circ)$, two of which ($\times,\otimes$) are monoidal closed, and the comonoids for $\circ$ are precisely categories in the usual sense. We discuss how the various structures in Poly show up in the theory of dynamical systems. We also show that the usual coalgebraic formalism for dynamical systems takes place within Poly. Indeed one can see coalgebras as special dynamical systems---ones that do not record their history---formally analogous to contractible groupoids as special categories.
△ Less
Submitted 11 June, 2020; v1 submitted 4 May, 2020;
originally announced May 2020.
-
Sum rules in multiphoton coincidence rates
Authors:
David Amaro Alcalá,
Dylan Spivak,
Hubert de Guise
Abstract:
We show that sums of carefully chosen coincidence rates in a multiphoton interferometry experiment can be simplified by replacing the original unitary scattering matrix with a coset matrix containing $0$s. The number and placement of these $0$s reduces the complexity of each term in the sum without affecting the original sum of rates. In particular, the evaluation of sums of modulus squared of per…
▽ More
We show that sums of carefully chosen coincidence rates in a multiphoton interferometry experiment can be simplified by replacing the original unitary scattering matrix with a coset matrix containing $0$s. The number and placement of these $0$s reduces the complexity of each term in the sum without affecting the original sum of rates. In particular, the evaluation of sums of modulus squared of permanents is shown to turn in some cases into a sum of modulus squared of determinants. The sums of rates are shown to be equivalent to the removal of some optical elements in the interferometer.
△ Less
Submitted 11 January, 2021; v1 submitted 23 April, 2020;
originally announced April 2020.
-
Dirichlet Functors are Contravariant Polynomial Functors
Authors:
David Jaz Myers,
David I. Spivak
Abstract:
Polynomial functors are sums of covariant representable functors from the category of sets to itself. They have a robust theory with many applications -- from operads and opetopes to combinatorial species. In this paper, we define a contravariant analogue of polynomial functors: Dirichlet functors. We develop the basic theory of Dirichlet functors, and relate them to their covariant analogues.
Polynomial functors are sums of covariant representable functors from the category of sets to itself. They have a robust theory with many applications -- from operads and opetopes to combinatorial species. In this paper, we define a contravariant analogue of polynomial functors: Dirichlet functors. We develop the basic theory of Dirichlet functors, and relate them to their covariant analogues.
△ Less
Submitted 8 April, 2020;
originally announced April 2020.
-
Dirichlet Polynomials form a Topos
Authors:
David I. Spivak,
David Jaz Myers
Abstract:
One can think of power series or polynomials in one variable, such as $P(x)=2x^3+x+5$, as functors from the category $\mathsf{Set}$ of sets to itself; these are known as polynomial functors. Denote by $\mathsf{Poly}_{\mathsf{Set}}$ the category of polynomial functors on $\mathsf{Set}$ and natural transformations between them. The constants $0,1$ and operations $+,\times$ that occur in $P(x)$ are a…
▽ More
One can think of power series or polynomials in one variable, such as $P(x)=2x^3+x+5$, as functors from the category $\mathsf{Set}$ of sets to itself; these are known as polynomial functors. Denote by $\mathsf{Poly}_{\mathsf{Set}}$ the category of polynomial functors on $\mathsf{Set}$ and natural transformations between them. The constants $0,1$ and operations $+,\times$ that occur in $P(x)$ are actually the initial and terminal objects and the coproduct and product in $\mathsf{Poly}_{\mathsf{Set}}$.
Just as the polynomial functors on $\mathsf{Set}$ are the copresheaves that can be written as sums of representables, one can express any Dirichlet series, e.g.\ $\sum_{n=0}^\infty n^x$, as a coproduct of representable presheaves. A Dirichlet polynomial is a finite Dirichlet series, that is, a finite sum of representables $n^x$. We discuss how both polynomial functors and their Dirichlet analogues can be understood in terms of bundles, and go on to prove that the category of Dirichlet polynomials is an elementary topos.
△ Less
Submitted 4 November, 2020; v1 submitted 10 March, 2020;
originally announced March 2020.
-
A Categorical Semantics for Guarded Petri Nets
Authors:
Fabrizio Genovese,
David I. Spivak
Abstract:
We build on the correspondence between Petri nets and free symmetric strict monoidal categories already investigated in the literature, and present a categorical semantics for Petri nets with guards. This comes in two flavors: Deterministic and with side-effects. Using the Grothendieck construction, we show how the guard semantics can be internalized in the net itself.
We build on the correspondence between Petri nets and free symmetric strict monoidal categories already investigated in the literature, and present a categorical semantics for Petri nets with guards. This comes in two flavors: Deterministic and with side-effects. Using the Grothendieck construction, we show how the guard semantics can be internalized in the net itself.
△ Less
Submitted 10 February, 2020; v1 submitted 29 January, 2020;
originally announced February 2020.
-
Regular and relational categories: Revisiting 'Cartesian bicategories I'
Authors:
Brendan Fong,
David I Spivak
Abstract:
Regular logic is the fragment of first order logic generated by $=$, $\top$, $\wedge$, and $\exists$. A key feature of this logic is that it is the minimal fragment required to express composition of binary relations; another is that it is the internal logic of regular categories. The link between these two facts is that in any regular category, one may construct a notion of binary relation using…
▽ More
Regular logic is the fragment of first order logic generated by $=$, $\top$, $\wedge$, and $\exists$. A key feature of this logic is that it is the minimal fragment required to express composition of binary relations; another is that it is the internal logic of regular categories. The link between these two facts is that in any regular category, one may construct a notion of binary relation using jointly-monic spans; this results in what is known as the bicategory of relations of the regular category. In this paper we provide a direct axiomatization of bicategories of relations, which we term relational po-categories, reinterpreting the earlier work of Carboni and Walters along these lines. Our main contribution is an explicit proof that the 2-category of regular categories is equivalent to that of relational po-categories. Throughout, we emphasize the graphical nature of relational po-categories.
△ Less
Submitted 30 August, 2019;
originally announced September 2019.
-
Supplying bells and whistles in symmetric monoidal categories
Authors:
Brendan Fong,
David I Spivak
Abstract:
It is common to encounter symmetric monoidal categories $\mathcal{C}$ for which every object is equipped with an algebraic structure, in a way that is compatible with the monoidal product and unit in $\mathcal{C}$. We define this formally and say that $\mathcal{C}$ supplies the algebraic structure. For example, the category $\mathsf{Rel}$ of relations between sets has monoidal structures given by…
▽ More
It is common to encounter symmetric monoidal categories $\mathcal{C}$ for which every object is equipped with an algebraic structure, in a way that is compatible with the monoidal product and unit in $\mathcal{C}$. We define this formally and say that $\mathcal{C}$ supplies the algebraic structure. For example, the category $\mathsf{Rel}$ of relations between sets has monoidal structures given by both cartesian product and disjoint union, and with respect to either one it supplies comonoids. We prove several facts about the notion of supply, e.g. that the associators, unitors, and braiding of $\mathcal{C}$ are automatically homomorphisms for any supply, as are the coherence isomorphisms for any strong symmetric monoidal functor that preserve supplies. We also show that any supply of structure in a symmetric monoidal category can be extended to a supply of that structure on its strictification.
△ Less
Submitted 5 May, 2020; v1 submitted 7 August, 2019;
originally announced August 2019.
-
Generalized Lens Categories via functors $\mathcal{C}^{\rm op}\to\mathsf{Cat}$
Authors:
David I. Spivak
Abstract:
Lenses have a rich history and have recently received a great deal of attention from applied category theorists. We generalize the notion of lens by defining a category $\mathsf{Lens}_F$ for any category $\mathcal{C}$ and functor $F\colon \mathcal{C}^{\rm op}\to\mathsf{Cat}$, using a variant of the Grothendieck construction. All of the mathematics in this note is straightforward; the purpose is si…
▽ More
Lenses have a rich history and have recently received a great deal of attention from applied category theorists. We generalize the notion of lens by defining a category $\mathsf{Lens}_F$ for any category $\mathcal{C}$ and functor $F\colon \mathcal{C}^{\rm op}\to\mathsf{Cat}$, using a variant of the Grothendieck construction. All of the mathematics in this note is straightforward; the purpose is simply to see lenses in a broader context where some closely-related examples, such as ringed spaces and open continuous dynamical systems, can be included.
△ Less
Submitted 16 March, 2022; v1 submitted 6 August, 2019;
originally announced August 2019.
-
Temporal Landscapes: A Graphical Logic of Behavior
Authors:
Brendan Fong,
Alberto Speranzon,
David I. Spivak
Abstract:
We present an elementary introduction to a new logic for reasoning about behaviors that occur over time. This logic is based on temporal type theory. The syntax of the logic is similar to the usual first-order logic; what differs is the notion of truth value. Instead of reasoning about whether formulas are true or false, our logic reasons about temporal landscapes. A temporal landscape may be thou…
▽ More
We present an elementary introduction to a new logic for reasoning about behaviors that occur over time. This logic is based on temporal type theory. The syntax of the logic is similar to the usual first-order logic; what differs is the notion of truth value. Instead of reasoning about whether formulas are true or false, our logic reasons about temporal landscapes. A temporal landscape may be thought of as representing the set of durations over which a statement is true. To help understand the practical implications of this approach, we give a wide variety of examples where this logic is used to reason about autonomous agents.
△ Less
Submitted 3 November, 2022; v1 submitted 1 April, 2019;
originally announced April 2019.
-
Categorical Data Integration for Computational Science
Authors:
Kristopher Brown,
David I. Spivak,
Ryan Wisnesky
Abstract:
Categorical Query Language is an open-source query and data integration scripting language that can be applied to common challenges in the field of computational science. We discuss how the structure-preserving nature of CQL data migrations protect those who publicly share data from the misinterpretation of their data. Likewise, this feature of CQL migrations allows those who draw from public data…
▽ More
Categorical Query Language is an open-source query and data integration scripting language that can be applied to common challenges in the field of computational science. We discuss how the structure-preserving nature of CQL data migrations protect those who publicly share data from the misinterpretation of their data. Likewise, this feature of CQL migrations allows those who draw from public data sources to be sure only data which meets their specification will actually be transferred. We argue some open problems in the field of data sharing in computational science are addressable by working within this paradigm of functorial data migration. We demonstrate these tools by integrating data from the Open Quantum Materials Database with some alternative materials databases.
△ Less
Submitted 25 March, 2019;
originally announced March 2019.
-
Graphical Regular Logic
Authors:
Brendan Fong,
David I Spivak
Abstract:
Regular logic can be regarded as the internal language of regular categories, but the logic itself is generally not given a categorical treatment. In this paper, we understand the syntax and proof rules of regular logic in terms of the free regular category $\mathsf{FRg}(\mathrm{T})$ on a set $\mathrm{T}$. From this point of view, regular theories are certain monoidal 2-functors from a suitable 2-…
▽ More
Regular logic can be regarded as the internal language of regular categories, but the logic itself is generally not given a categorical treatment. In this paper, we understand the syntax and proof rules of regular logic in terms of the free regular category $\mathsf{FRg}(\mathrm{T})$ on a set $\mathrm{T}$. From this point of view, regular theories are certain monoidal 2-functors from a suitable 2-category of contexts---the 2-category of relations in $\mathsf{FRg}(\mathrm{T})$---to the 2-category of posets. Such functors assign to each context the set of formulas in that context, ordered by entailment. We refer to such a 2-functor as a regular calculus because it naturally gives rise to a graphical string diagram calculus in the spirit of Joyal and Street. Our key aim to prove that the category of regular categories is essentially reflective in that of regular calculi. Along the way, we demonstrate how to use this graphical calculus.
△ Less
Submitted 20 June, 2019; v1 submitted 13 December, 2018;
originally announced December 2018.
-
Behavioral Mereology (Proofs and Properties)
Authors:
Brendan Fong,
David Jaz Myers,
David I. Spivak
Abstract:
Mereology is the study of parts and the relationships that hold between them. We introduce a behavioral approach to mereology, in which systems and their parts are known only by the types of behavior they can exhibit. Our discussion is formally topos-theoretic, and agnostic to the topos, providing maximal generality; however, by using only its internal logic we can hide the details and readers may…
▽ More
Mereology is the study of parts and the relationships that hold between them. We introduce a behavioral approach to mereology, in which systems and their parts are known only by the types of behavior they can exhibit. Our discussion is formally topos-theoretic, and agnostic to the topos, providing maximal generality; however, by using only its internal logic we can hide the details and readers may assume a completely elementary set-theoretic discussion. We consider the relationship between various parts of a whole in terms of how behavioral constraints are passed between them, and give an inter-modal logic that generalizes the usual alethic modalities in the setting of symmetric accessibility.
△ Less
Submitted 2 July, 2020; v1 submitted 1 November, 2018;
originally announced November 2018.
-
Evaluating the Pixel Array Method as Applied to Partial Differential Equations
Authors:
Cynthia T. Liu,
David I. Spivak
Abstract:
The Pixel Array (PA) Method, originally introduced by Spivak et. al., is a fast method for solving nonlinear or linear systems. One of its distinguishing features is that it presents all solutions within a bounding box, represented by a plot whose axes are the values of "exposed variables." Here we develop a set-theoretic variant of the PA method, named the Pixel Array Solution-Set (PASS) method,…
▽ More
The Pixel Array (PA) Method, originally introduced by Spivak et. al., is a fast method for solving nonlinear or linear systems. One of its distinguishing features is that it presents all solutions within a bounding box, represented by a plot whose axes are the values of "exposed variables." Here we develop a set-theoretic variant of the PA method, named the Pixel Array Solution-Set (PASS) method, that gives PA access to "hidden variables" whose values are not displayed on plot axes. We evaluate the effectiveness of PASS at numerically finding steady states for several partial differential equations. We discretize several one-dimensional solved reaction-diffusion equations, such as the Fisher equation and the Benjamin-Bona-Mohany equation, using finite differences. Then, we run PASS on each equation, and determine whether it successfully finds all boundary conditions for which a numerical steady state might exist. Then we verify whether the steady states found by PASS are correct. Finally, we discuss the benefits and weaknesses of PASS.
△ Less
Submitted 5 August, 2018;
originally announced August 2018.
-
Decomposition-space slices are toposes
Authors:
Joachim Kock,
David I. Spivak
Abstract:
We show that the category of decomposition spaces and CULF maps is locally a topos. Precisely, the slice category over any decomposition space D is a presheaf topos, namely decomp/D=Psh(tw D).
We show that the category of decomposition spaces and CULF maps is locally a topos. Precisely, the slice category over any decomposition space D is a presheaf topos, namely decomp/D=Psh(tw D).
△ Less
Submitted 2 September, 2019; v1 submitted 16 July, 2018;
originally announced July 2018.
-
Hypergraph Categories
Authors:
Brendan Fong,
David I Spivak
Abstract:
Hypergraph categories have been rediscovered at least five times, under various names, including well-supported compact closed categories, dgs-monoidal categories, and dungeon categories. Perhaps the reason they keep being reinvented is two-fold: there are many applications---including to automata, databases, circuits, linear relations, graph rewriting, and belief propagation---and yet the standar…
▽ More
Hypergraph categories have been rediscovered at least five times, under various names, including well-supported compact closed categories, dgs-monoidal categories, and dungeon categories. Perhaps the reason they keep being reinvented is two-fold: there are many applications---including to automata, databases, circuits, linear relations, graph rewriting, and belief propagation---and yet the standard definition is so involved and ornate as to be difficult to find in the literature. Indeed, a hypergraph category is, roughly speaking, a "symmetric monoidal category in which each object is equipped with the structure of a special commutative Frobenius monoid, satisfying certain coherence conditions".
Fortunately, this description can be simplified a great deal: a hypergraph category is simply a "cospan-algebra". The goal of this paper is to remove the scare-quotes and make the previous statement precise. We prove two main theorems. First is a coherence theorem for hypergraph categories, which says that every hypergraph category is equivalent to an objectwise-free hypergraph category. Second, we prove that the category of objectwise-free hypergraph categories is equivalent to the category of cospan-algebras.
△ Less
Submitted 18 January, 2019; v1 submitted 21 June, 2018;
originally announced June 2018.
-
Seven Sketches in Compositionality: An Invitation to Applied Category Theory
Authors:
Brendan Fong,
David I Spivak
Abstract:
This book is an invitation to discover advanced topics in category theory through concrete, real-world examples. It aims to give a tour: a gentle, quick introduction to guide later exploration. The tour takes place over seven sketches, each pairing an evocative application, such as databases, electric circuits, or dynamical systems, with the exploration of a categorical structure, such as adjoint…
▽ More
This book is an invitation to discover advanced topics in category theory through concrete, real-world examples. It aims to give a tour: a gentle, quick introduction to guide later exploration. The tour takes place over seven sketches, each pairing an evocative application, such as databases, electric circuits, or dynamical systems, with the exploration of a categorical structure, such as adjoint functors, enriched categories, or toposes.
No prior knowledge of category theory is assumed.
A feedback form for typos, comments, questions, and suggestions is available here: https://docs.google.com/document/d/160G9OFcP5DWT8Stn7TxdVx83DJnnf7d5GML0_FOD5Wg/edit
△ Less
Submitted 12 October, 2018; v1 submitted 14 March, 2018;
originally announced March 2018.
-
Abstraction, Composition and Contracts: A Sheaf Theoretic Approach
Authors:
Alberto Speranzon,
David I. Spivak,
Srivatsan Varadarajan
Abstract:
Complex systems of systems (SoS) are characterized by multiple interconnected subsystems. Typically, each subsystem is designed and analyzed using methodologies and formalisms that are specific to the particular subsystem model of computation considered --- Petri nets, continuous time ODEs, nondeterministic automata, to name a few. When interconnecting subsystems, a designer needs to choose, based…
▽ More
Complex systems of systems (SoS) are characterized by multiple interconnected subsystems. Typically, each subsystem is designed and analyzed using methodologies and formalisms that are specific to the particular subsystem model of computation considered --- Petri nets, continuous time ODEs, nondeterministic automata, to name a few. When interconnecting subsystems, a designer needs to choose, based on the specific subsystems models, a common abstraction framework to analyze the composition. In this paper we introduce a new framework for abstraction, composition and analysis of SoS that builds on results and methods developed in sheaf theory, category theory and topos theory. In particular, we will be modeling behaviors of systems using sheaves, leverage category theoretic methods to define wiring diagrams and formalize composition and, by establishing a connection with topos theory, define a formal (intuitionistic/constructive) logic with a sound sheaf semantics
△ Less
Submitted 8 February, 2018;
originally announced February 2018.
-
Backprop as Functor: A compositional perspective on supervised learning
Authors:
Brendan Fong,
David I. Spivak,
Rémy Tuyéras
Abstract:
A supervised learning algorithm searches over a set of functions $A \to B$ parametrised by a space $P$ to find the best approximation to some ideal function $f\colon A \to B$. It does this by taking examples $(a,f(a)) \in A\times B$, and updating the parameter according to some rule. We define a category where these update rules may be composed, and show that gradient descent---with respect to a f…
▽ More
A supervised learning algorithm searches over a set of functions $A \to B$ parametrised by a space $P$ to find the best approximation to some ideal function $f\colon A \to B$. It does this by taking examples $(a,f(a)) \in A\times B$, and updating the parameter according to some rule. We define a category where these update rules may be composed, and show that gradient descent---with respect to a fixed step size and an error function satisfying a certain property---defines a monoidal functor from a category of parametrised functions to this category of update rules. This provides a structural perspective on backpropagation, as well as a broad generalisation of neural networks.
△ Less
Submitted 1 May, 2019; v1 submitted 28 November, 2017;
originally announced November 2017.
-
An infinite quantum Ramsey theorem
Authors:
Matthew Kennedy,
Taras Kolomatski,
Daniel Spivak
Abstract:
We prove an infinite Ramsey theorem for noncommutative graphs realized as unital self-adjoint subspaces of linear operators acting on an infinite dimensional Hilbert space. Specifically, we prove that if V is such a subspace, then provided there is no obvious obstruction, there is an infinite rank projection P with the property that the compression PVP is either maximal or minimal in a certain nat…
▽ More
We prove an infinite Ramsey theorem for noncommutative graphs realized as unital self-adjoint subspaces of linear operators acting on an infinite dimensional Hilbert space. Specifically, we prove that if V is such a subspace, then provided there is no obvious obstruction, there is an infinite rank projection P with the property that the compression PVP is either maximal or minimal in a certain natural sense.
△ Less
Submitted 26 November, 2017;
originally announced November 2017.
-
Temporal Type Theory: A topos-theoretic approach to systems and behavior
Authors:
Patrick Schultz,
David I. Spivak
Abstract:
This book introduces a temporal type theory, the first of its kind as far as we know. It is based on a standard core, and as such it can be formalized in a proof assistant such as Coq or Lean by adding a number of axioms. Well-known temporal logics---such as Linear and Metric Temporal Logic (LTL and MTL)---embed within the logic of temporal type theory.
The types in this theory represent "behavi…
▽ More
This book introduces a temporal type theory, the first of its kind as far as we know. It is based on a standard core, and as such it can be formalized in a proof assistant such as Coq or Lean by adding a number of axioms. Well-known temporal logics---such as Linear and Metric Temporal Logic (LTL and MTL)---embed within the logic of temporal type theory.
The types in this theory represent "behavior types". The language is rich enough to allow one to define arbitrary hybrid dynamical systems, which are mixtures of continuous dynamics---e.g. as described by a differential equation---and discrete jumps. In particular, the derivative of a continuous real-valued function is internally defined.
We construct a semantics for the temporal type theory in the topos of sheaves on a translation-invariant quotient of the standard interval domain. In fact, domain theory plays a recurring role in both the semantics and the type theory.
△ Less
Submitted 23 December, 2017; v1 submitted 27 October, 2017;
originally announced October 2017.
-
Permutational symmetries for coincidence rates in multi-mode multi-photonic interferometry
Authors:
Abdullah Khalid,
Dylan Spivak,
Barry C. Sanders,
Hubert de Guise
Abstract:
We obtain coincidence rates for passive optical interferometry by exploiting the permutational symmetries of partially distinguishable input photons, and our approach elucidates qualitative features of multi-photon coincidence landscapes. We treat the interferometer input as a product state of any number of photons in each input mode with photons distinguished by their arrival time. Detectors at t…
▽ More
We obtain coincidence rates for passive optical interferometry by exploiting the permutational symmetries of partially distinguishable input photons, and our approach elucidates qualitative features of multi-photon coincidence landscapes. We treat the interferometer input as a product state of any number of photons in each input mode with photons distinguished by their arrival time. Detectors at the output of the interferometer count photons from each output mode over a long integration time. We generalize and prove the claim of Tillmann et al. [Phys. Rev. X 5 041015 (2015)] that coincidence rates can be elegantly expressed in terms of immanants. Immanants are functions of matrices that exhibit permutational symmetries and the immanants appearing in our coincidence-rate expressions share permutational symmetries with the input state. Our results are obtained by employing representation theory of the symmetric group to analyze systems of arbitrary number of photons in arbitrarily sized interferometers.
△ Less
Submitted 20 June, 2018; v1 submitted 19 September, 2017;
originally announced September 2017.
