MIT (Applied) Categories Seminar

The operad of undirected wiring diagrams and its algebras model systems that compose in an undirected style. We explain these ideas informally and show how they are implemented in Catlab, a framework for applied category theory written in the Julia programming language. The abstract notions are illustrated by the examples of tensor networks and pixel arrays, conjunctive queries on relational databases, and open systems as modeled by structured cospans.

The idea is to explore the concept "Point", to look at it from different perspectives and see the connections given by the Stone Duality and the Gelfand Duality. Starting from a topological perspective, a point as an element of a topological space, we'll see the correspondences with ultrafilters, global elements in the category of Stone Spaces, morphisms that have as codomain the initial algebra 2 and how this morphisms correspond to valuations of a language in classical logic. We'll then go to boolean valued models, see how the points there have a probabilistic behavior and see some interesting consequences given by doing the forcing method through principal ultrafilters vs non-principal ultrafilters.Then we'll see the equivalences given by the Gelfand Duality: global elements in the category of locally compact spaces, characters of commutative C* algebras, maximal ideals, pure states (as positive, normalized functionals) and irreducible representations.

Videos: Part I, Part II, Part III, Teaser/Addendum

Series outline available here.

"Higher categories" are algebraic structures which generalise categories, in the same way that categories generalise sets. The theory of these structures is ubiquitous in many areas of application of category theory. In this talk, we will motivate higher structure from applications in logic, type theory and programming languages. Surprisingly, a formulation of higher categories which is amendable to computer implementation has been missing for decades — with homotopy type theory being a notable exception of the special case of “higher groupoids”. Starting from elementary observations about compositionality in higher dimensions, will sketch a combinatorial approach to higher categories that gives rise to a programming language which we call “Globular” and which comes with an elegant geometric model. We will see that programs in Globular can capture complex higher-dimensional geometric deformations, and learn how, for instance, they can capture higher homotopy groups of spheres and other interesting geometric facts.

System Dynamics is a moniker coined by Jay Forrester over 50 years ago at MIT, when computers were just beginning to be used to simulate the behaviors of complex models of social and economic processes. Today it has a substantial following in business schools, management consulting firms, and some multinational corporations, with the goal of teaching "Systems Thinking" to their respective stake holders (see "Business Dynamics" by John Sterman). While it has since branched out into more sophisticated agent-based and dynamic network models (see this short article), it was initially based on a diagrammatic language for nonlinear ODEs that continues to play a central role in its applications. This talk will introduce this language and give some examples, with the hope that the audience will discover some analogies, and new applications, for the categorical formalisms it has developed for modeling and analyzing systems in a broader sense.

Series outline available here.

I'll talk about an algebraic setting (in particular, a category) in which supervised learning algorithms can be composed, and then explain how this articulates the structure underlying backpropagation on a neural network. More details here.

Decomposition spaces are combinatorial objects that allow one to decompose maps in a natural (co-associative and co-unital) way. All categories are decomposition spaces, but not vice versa. Decomposition spaces form a category, called Decomp, where the maps preserve the decomposition structure. I'll discuss these ideas and recent work (joint with J. Kock) where we show that every slice category of Decomp is a topos. One of them is the topos I discussed recently: that of "discrete temporal type theory".

Decomposition spaces are combinatorial objects that allow one to decompose maps in a natural (co-associative and co-unital) way. All categories are decomposition spaces, but not vice versa. Decomposition spaces form a category, called Decomp, where the maps preserve the decomposition structure. I'll discuss these ideas and recent work (joint with J. Kock) where we show that every slice category of Decomp is a topos. One of them is the topos I discussed recently: that of "discrete temporal type theory".

Formal verification is the process of proving that a system adheres to a specification of its intended behavior. Like programming languages, there exists a variety of specification languages, each suited to describing distinct types of behavior. Some systems may require a combination of specification types and reasoning strategies to verify the whole system. This scenario motivates the need for heterogeneous specification languages. In this talk, we shall explore Farrell et. al.'s 2017 paper entitled "Combining Event-B and CSP: An Institution Theoretic approach to Interoperability". We shall see how the authors use category theory to establish interoperability between two specification languages, Event-B and CSP, focusing particularly on how they develop semantic preserving translations between the two languages.

In last week's seminar, we heard from Antwane Mason about Goguen and Burstall's notion of institution, which is a category-theoretic formalism used for software specification and verification. The definition is usually phrased in terms of a satisfaction relation between models and sentences of signatures, and a certain bivariant coherence condition on it.

In this talk I will discuss a few different category-theoretic perspectives on this notion, including from categorical database theory, posetal bifibrations, and topos theory. In the order "signatures, models, sentences, satisfaction", we can view

• databases as an institution via "schemas, instances, embedded dependency constraints, satisfaction",
• any posetal bifibration as an institution via: "base objects, fiber elements, fiber elements, ≤", and
• toposes as an institution via "toposes, points, truth values, satisfaction".

Finally, I'll give an alternative, equivalent definition of institution in terms of fibrations and opfibrations.

A simple tutorial on Kan extensions: their definition, relationship with (co)limits and adjoints, and some basic examples. There will be plenty of time for questions.

In this talk, we will use the concepts of left Kan extension and monomorphism to describe Genome-wide association studies used in genetics. This will be the opportunity to review the concept of Kan extension and see its real world applications.

In cooperative conversation, speakers tend to prefer informative utterances, and listeners assume the speaker is being informative in order to draw inferences. For instance, if you hear me say "John liked half of the concert", you infer that he did not like to other half, since as an informative speaker, I would then have said "John liked the concert", were that true. Bayesian models can be used to formalize these inferences.

I show that a model of an informative speaker (that says as much as is possible) can be defined as a right Galois connection (right adjoint between posets) to a literal listener, understood as a monotone function (functor between posets) from utterances to possible worlds. Dually, a pragmatic listener (that deduces that no more is meant that is said) is a left adjoint of a literal speaker, understood as a monotone function from possible worlds to utterances. While elementary, this points to a deeper category-theoretic formulation of Gricean pragmatics and more generally, cooperative games.

Monads are a categorical concept which can be interpreted as encoding formal expressions, or formal operations in the sense of universal algebra. We give a construction which formalizes the idea of “evaluating an expression partially”: for example, “2+3” can be obtained as a partial evaluation of “2+2+1”, and conversely, we can view “2+2+1” as a partial decomposition of “2+3”. This construction can be given for all monads on a concrete category, and it is linked to a simplicial object called the bar construction, of which it gives an operational interpretation: the bar construction is a simplicial set, and its 1-cells are partial evaluations.

We study the properties of partial evaluations for general monads on concrete categories. We prove that whenever the multiplication of the monad is weakly cartesian, partial evaluations can be composed via the usual Kan filler property of simplicial sets, of which we give an interpretation in terms of substitution of terms.

For the case of probability monads, partial evaluations correspond to what probabilists call conditional expectation of random variables, which is used to define martingales. It follows that a martingale is equivalently described as a chain of partial decompositions.

This talk is part of a work in progress on a general operational interpretation of the bar construction.

This is joint work with Tobias Fritz.

In order to make a model of some system, we have in mind the sort of things in that system we intend to model; we have an ontology of our model, and we hope the things in this ontology correspond to the things in the system. But coming up with such an ontology is more of an art than a science. A model's success is judged on its ability to predict, not how much it matches our intuitive ontology. What things do our best models actually model?

Can we find a "natural ontology" of a model, one that comes from the model itself and contains only the things the model is modelling? What is a thing, anyway? In this talk, we will look at a categorical approach to these problems using the yoga of behavior types.

How can category theory be productively applied to extend concepts and techniques of logic and linguistics, so as to elucidate the behavior of biological networks?

I will discuss some concrete initial steps, based upon current categorical constructs in logic and topology, and will explain the relevance of emerging semiotic ideas concerning meaning-making and meaning transformation in biological networks.

Linkage disequilibrium is the existence of a non-random relationship between two loci in the genome. I will show how one can talk about this type of relationship using a certain type of pedigrads in the category of idempotent commutative monoids.

A first look at a software development effort to implement the causal theory methodology in Brendan Fong's masters thesis, "Causal Theories: A Categorical Perspective on Bayesian Networks" (presented by Brendan at a seminar in May). This talk, which includes a demo of the prototype version, will have a brief overview of causal modeling, the categorical framework for causal theory models, the Python software used, how the users can draw causal graphs with the program, and plans for ongoing development. We will discuss the applicability of the causal theory model program and the potential benefits of applying category theory to analytical modeling.

Brendan and I have been developing a new categorical viewpoint—and graphical calculus for—regular logic. I've recently been thinking about how some of the surrounding ideas might apply to learning and adaptation via something I might call a "theory building" adjunction. Some of these ideas seem to connect to Reuben Cohn-Gordon's recent seminar talk on the "Gricean adjunction" from pragmatics.

The ideas I'll present are at an early stage in terms of maturity, and the goal of the talk is to be fun and pictorial. Still, I will certainly make connections to the underlying mathematical abstractions.

It is informally understood that the purpose of modal (i.e. unary) type constructors in programming calculi is to control the flow of information between types. I will introduce a number of such constructors that are useful for security-aware functional programming, i.e. for writing programs without accidental high-level leaks of information flow. Following that, I will prove that the well-typed programs in calculi of this sort preserve confidentiality and integrity by design, by using some categorical algebra and a few background ideas from topology. (This talk is based on arXiv:1809.07897.)

I'll present some foundational ideas behind the work David and I have been doing on graphical regular logic. In particular, I'll give a number of characterisations of the notion of meet semilattice. The aim will be to not only give an understanding of meet semilattices, but to illustrate general categorical lessons about limits, adjunctions, and monoidal functors.

Open games are a foundation of non-cooperative game theory that is strongly compositional: all games are built from small pieces using sequential and parallel composition operators. They form the morphisms of a symmetric monoidal category, and string diagrams provide a useful and intuitive way of visualising them that is an alternative to the traditional extensive form. I will focus on the foundations, which involves a careful analysis of how observable and counterfactual information interact in a game. Time permitting I'll discuss a close connection with open learners, from the paper Backprop as Functor by Fong, Spivak and Tuyéras.

In this talk I'll introduce monads and their algebras, illustrating the concepts using the finite probability distribution monad. In particular, in addition to defining monads and algebras for monads, I'll talk about free algebras and the Kleisli category for a monad. Examples will include the power set monad, maybe monad, and the Giry monad. We'll see how the notion of a stochastic matrix or conditional probability distribution arises from this set up.

I will explain how monads often arise as Kan extensions of graded monads. For example, the set of lists over an alphabet is the disjoint union of the sets of lists of each length. I will then show how this leads to a construction of a probability monad similar to the Giry monad. The graded monad approach lets us replace the use of measure theory by the combinatorics of finite sets, and makes precise the idea that a probability measure is an idealized version of a finite sample.

Joint work with Paolo Perrone.

Come hear about my favorite category, the category whose objects are convex sets and whose morphisms are affine maps. Among these objects are the simplices. Maps between simplices correspond to (finite-support) conditional probability distributions. In fact, this category has (co)limits, tensor, and hom, and we may interpret these concepts probabilistically, too! We will end by diagrammatically reasoning about independence and statistical sufficiency to show Fisher's and Basu's theorems. This theory is incomplete, so I'd love your feedback during and after the talk.

The Yoneda lemma is a central result in category theory. Roughly speaking, it states that any object in a category is determined by its web of relationships (ie. its hom-sets) with other objects. In this talk I'll make this idea precise, and discuss what limits look like from this perspective.

This talk is a very informal introduction to adjoint functors, particularly from the perspective of software development. I'll give lots of examples of adjunctions to help the audience develop a general feel for how they come up in programming and indeed in everyday life. A basic familiarity with category theory and functional programming is assumed.

In this talk I'll discuss a Fong, et al.'s setting for composable learning algorithms (details here: https://arxiv.org/abs/1711.10455), and formalize the category of recurrent models on top of this framework. I'll then attempt and fail to equip this category with a trace, a notion that usually formalizes recursion in categories of computations. I'll discuss the obstructions to finding a trace, and speculate about what a traced category of learning algorithms might look like.

A PERT chart is a project management tool used to schedule, organize, and coordinate tasks within a project. The data of a PERT chart is a list of activities, together with their durations and dependencies on each other; the PERT chart formats this data as a certain duration-weighted graph. In this talk we'll discuss how these durations form a preorder R, which in fact has the structure of a quantale. This allows us to see PERT charts simply as R-enriched categories, and think about project scheduling in terms of categorical constructions.

This talk is based on the following n-Category Café post by Simon Willerton: https://golem.ph.utexas.edu/category/2013/03/project_planning_parallel_proc.html. No familiarity with enriched categories will be assumed.

I'll discuss the mathematical specification of a graphical user interface for logical reasoning. I'll begin with a detective story, where we see this graphical reasoning in action. Then I'll briefly discuss the math—we've seen most of it before in this seminar—namely that of "ajax bifunctors from the monoidal bi-category of corelations to that of posets." With that out of the way, I'll talk more about the GUI and consider further examples of how such a tool could be used in practice, for fun and profit.
(slides)

Abelian categories are "convenient places to calculate", e.g. to do homological algebra. One nice feature of abelian categories is that they are regular, meaning that each has a well-working calculus of relations. This calculus can be given a graphical formulation, with a "user interface" of wiring diagrams that we can specify mathematically.

I'll present abelian categories from this point of view, with the following compressed mathematical specification: a graphical abelian calculus is a bi-ajax po-functor P: LinRel-->Poset. Unpacking this, I'll explain that there is a graphical syntax of linear relations, which is a mild ("thin") extension of Sobocinski's graphical linear algebra. It forms a po-category LinRel, and functors from LinRel to the po-category of posets provide semantic content to this syntax: they tell us how we can "fill the shells". Any lax monoidal po-functor P: LinRel-->Poset whose laxators have both left and right adjoints gives rise to an abelian category, and all abelian categories (up to equivalence) arise in this way.

We describe a novel approach to mapping an unknown indoor environment based on sparse sampling of people paths with minimalist sensor data. The problem is inspired by mapping the geometry of a building floorplan via “uncooperative sensing” — using data from such as camera feeds and other tracking-capable sensors. Unique challenges include having no knowledge of sensor placement, coverage or parameters, thus making such sensors “uncooperative”. The methods we develop are, at first, topological, to build a combinatorial model with the appropriate topology. We focus the modeling and analysis assuming sensors being cameras: using statistical information based on how people are detected in various cameras field of views, we are able to develop a model that captures topological information about the unobservable space. Such a model is further augmented to include a weak form of geometric information, and optimization techniques are used to approximate domain geometry.

An introductory overview of the paper "Total maps of Turing Categories", by Cockett, Hofstra and Hrubes.

Planning in autonomous systems is generally hierarchical. A goal is given to a higher-level planner, which decides on a sequence of actions that will accomplish it given the current conditions. Each of these actions is then handed off as a goal to some lower-level planner. To make dinner, we need to go to the store, get ingredients, bring them home, and cook, but going to the store requires choosing a route, and in turn, each step along the route is accomplished by choosing and executing a certain sequence of muscle movements.

We will think of planners as generalized Markov decision processes, where we replace the nondeterminism-and-reward aspect of an MDP by an arbitrary monad M on Set. These will be the objects of a category M-MDP, and we formalize "handing off high-level actions to lower-level planners" as morphisms. If M is monoidal, the result will be a symmetric monoidal category, the idea being that a team of bosses can issue commands to be executed by a team of performers.

Bidirectional data accessors such as lenses, prisms and traversals are all instances of the same general "optic" construction. After a crash-course in the (co)end calculus, we will define optics generally and see that we recover lenses, including the lens laws.

Many learning algorithms have invariances: when their training data is transformed in certain ways, the function they learn transforms in a predictable manner. Here we formalize this notion using concepts from category theory. The invariances that a supervised learning algorithm possesses are formalized by categories of predictor and target spaces, whose morphisms represent the algorithm's invariances, and an index category whose morphisms represent permutations of the training examples. An invariant learning algorithm is a natural transformation between two functors from the product of these categories to the category of sets, representing training datasets and learned functions respectively. We illustrate the framework by characterizing and contrasting the invariances of linear regression and ridge regression.

I will describe the idempotent distributive lattice completion of a partially ordered set, and characterize it as a reflector in a subcategory of Pos which shares all objects but only contains a special class of morphisms. From there we will examine Dependency Structures with Choice, which are a way of reformulating the ideas behind the Event Structures used in models of concurrent semantics, including those of Petri nets. Reachable posets of DSCs, under the the distributive lattice completion, let us view dependency structures topologically, and provide an elegant logical interpretation of “covering” relations of dependencies. Time permitting, I can also sketch future work that makes use of induced homological structure as well. This project is jww Raymond Puzio.

Tolerance relations are binary relations where just reflexivity and symmetry, but not transitivity, are assumed to hold. Forcing transitivity is obviously natural (and very useful) in many mathematical contexts, but there are a variety of interesting applications where imposing transitivity simply does not seem appropriate. The category of tolerance spaces (with tolerance-preserving functions) has monoidal closed structures, and I will mostly look closely at a few applications and examples displaying what it looks like to enrich over this category.

I may also look briefly at some connections to t-norms—in particular lattice-valued t-norms (lifting the set of truth-values in a fuzzy logic beyond the real interval [0,1])—and some properties of fuzzy tolerance, in the course of which I will touch on some broader interactions with generalized (Lawvere) metric spaces.

Finally, I will make a few connections between all this and sheaves, and possibly indicate some more general ideas on metrics on the category of sheaves.

When manipulating data, it is often convenient only to read and write to part of a data structure, leaving the rest untouched or changed in some minimal compatible way. Optics provide a modular, composable, and increasingly popular method for structuring such manipulations. Examples of optics include lenses and prisms. Optics are heavily based on the categorical notion of profunctor. In this talk I'll introduce both profunctors and optics, and give some idea about how the categorical theory influences the practical design of data accessors.

Many algorithms are specified on real numbers and then implemented with finite-precision arithmetic, with the result that the implementations do not soundly compute the results expected from their specifications. I will present a programming language MarshallB, which in contrast allows sound computation with continuous values. MarshallB types are generalized topological spaces, and functions are generalized continuous maps; the generalization is because MarshallB has higher-order functions but the category of topological spaces and continuous maps is not closed, so we instead use a category of presheaves over spaces, which is closed. These higher-order functions are useful! There are higher-order functions for logical quantification, for optimization, for integration, and for constructing real numbers via Dedekind cuts. In this talk, I’ll give a brief demonstration of MarshallB, I’ll review the interpretation of simply-typed lambda calculus into cartesian closed categories, and then we’ll look in particular at presheaves over spaces, focusing on some specific higher-order functions and how they work.

We construct a nerve functor parametrized by a choice of quantale, exhibiting both the Vietoris-Rips complex and the magnitude nerve as instances of this nerve for different choices of monoidal structure on the nonnegative reals. Furthermore, the difference between how persistent homology processes the Vietoris-Rips complex and how magnitude homology processes the magnitude nerve is cast as a choice of whether or not to "localize" the corresponding nerves in a precise sense. Lastly, we mention some application-oriented observations naturally suggested by the perspective mentioned above.

In this talk, we'll discuss lenses, which have lately been showing up all over applied category theory: in the theory of functional programming, databases, hierarchical planning, open discrete dynamical systems, open economic games, and supervised learning. Lenses are somewhat peculiar-looking things, but at least they form a symmetric monoidal category, denoted Lens.

I hold the opinion that lenses should really be viewed within the larger, more geometrically-flavored category of bundles—objects in Lens are the trivial bundles—and that the reason lenses look peculiar is because the geometric aspect is obscured when we restrict to the special case.

To explain this, I'll show that Lens embeds into a larger symmetric monoidal category that provides geometric intuition, has better formal properties, and will likely be more familiar to mathematicians, e.g. to algebraic geometers. From this viewpoint, lenses become strongly related to that of polynomial functors, which show up in functional programming as "containers" and in database theory as "functorial data migration". I'll generalize further so that examples of lenses include continuous dynamical systems and a more principled (though still partial) solution to the view-update problem in database theory.

Morphisms in a symmetric monoidal category can be depicted using string diagrams; this is a celebrated fact that underpins much of applied catgeory theory. It often happens, however, that one wishes to use special, additional icons in a string diagram language; more formally, this means every object is equipped with additional algebraic structure. For example, in a hypergraph category each object is equipped with a notion of wiring, or in a category with products each object has a diagonal map. In these cases, the minimal structure required for a nice string diagram language is a simple compatibility condition between the algebraic structures on each object and the monoidal product. If this condition holds, we say that the category supplies the structure.

In this talk I'll give some examples of supply, and outline a few theorems that show the compatibility condition is really what is necessary for nice diagrams. The material will form an accessible introduction to my paper with David of the above title.

The market has plenty of user-friendly programming languages like Python and JavaScript, efficient, resource-aware languages like Rust and C, and secure, mathematical proof languages like Agda and Coq, but it is almost impossible to find one with all those characteristics. In this talk, we'll highlight the design decisions behind Formality, an upcoming non-garbage-collected, parallel, accessible proof language that targets this sweet-spot by using insights from elementary affine logic, optimal reductions and interaction nets.

Probabilistic modeling and inference are central tools in multiple fields, including artificial intelligence, statistics, and robotics, but can be tricky for practitioners to apply correctly. To make these techniques more accessible, probabilistic programming languages give users a formal language for expressing probabilistic models, and automate tedious and error-prone aspects of implementing Bayesian inference algorithms. But how can we think formally about what these tools are doing, and whether their inference engines are implemented correctly? And when the default inference algorithms don’t converge quickly enough, how can users tailor inference to the problem at hand without invalidating correctness guarantees?

In this talk, I’ll introduce the core ideas behind probabilistic programming languages and motivate the need for a formal approach to understanding their semantics. I’ll present a brief sketch of the recently introduced category of quasi-Borel spaces [1], which has been used to validate the correctness of several general-purpose inference algorithms for probabilistic programs [2]. Finally, I’ll present a new extension to that work that allows programmers to customize the behavior of these inference algorithms on a per-model basis in a sound-by-construction manner, ensuring that the resulting inference algorithms are still correct.

[1] Chris Heunen, Ohad Kammar, Sam Staton and Hongseok Yang, A convenient cateogry for higher-order probability theory, Logic in Computer Science 2017.

[2] Ścibior, Adam, et al. "Denotational validation of higher-order Bayesian inference." Proceedings of the ACM on Programming Languages 2.POPL (2017): 60.

Natural language has both a compositional and a statistical structure. These structures emerge when expressions in language combine to form longer expressions, and where the validity of an expression is captured by the statistics in the language. One model for this is a monoidal functor from a category of grammar to an appropriate semantics category. Another modeling choice is to let statistics serve as a proxy for grammar, taking inspiration from quantum probability theory. This talk features the latter. I’ll share an elementary passage from classical probability to quantum probability and use it to describe a tensor network model for language.

The emerging field of applied category theory studies mathematical models of compositional processes in a unified, systematic way. However, going from a mathematical model, written on paper, to an operational method, realized in practice, is a challenge demanding significant effort. In particular, the computational tools supporting applied category theory are immature. Over the past several years, we have developed Catlab.jl, an early programming library and computer algebra system for applied category theory, written in Julia. Catlab provides data structures and algorithms for defining, manipulating, serializing, and visualizing symbolic expressions and wiring diagrams for different flavors of categories. In this talk, we introduce the design and some of the features of Catlab. We also discuss lessons learned along the way and how we hope to improve the system in the future.

Slides available here.

Category theory can be very useful for many domains of engineering, because the synthetic and rigorous language it provides can help describe and analyze complex systems. In this talk I will describe a categorical theory of “co-design” (collaborative, compositional, computational, continuous design) to be used to describe and solve formal engineering design problems. I will discuss the design and implementation of a formal co-design language. Finally, I will discuss the work to be done to achieve the representation power necessary to fully capture the domain of engineering design.

Slides available here.

A (closed) dynamical system is a notion of how things can be, together with a notion of how they may change given how they are. The idea and mathematics of closed dynamical systems has proven incredibly useful in those sciences that can isolate their object of study from its environment. But many changing situations in the world cannot be meaningfully isolated from their environment -- a cell will die if it is removed from everything beyond its walls. To study systems that interact with their environment, and to design such systems in a modular way, we need a robust theory of open dynamical systems.

In this talk, I'll present a general definition of open dynamical system based on the idea of generaliz ed lenses due to Spivak. Given a particular notion of generalized lens (with a small bit of extra data), we'll construct a symmetric monoidal category of open dynamical systems and show how these systems can be connected using wiring diagrams. We'll see a handful of examples -- discrete, non-deterministic, probabilistic, continuous -- and show how a class of these, the discrete-time monadic open dynamical systems, can be implemented in Haskell.

Decorated Cospans provide a framework for describing systems composed of interacting open subsystems such as Open Petri Nets. I will discuss the SemanticModels library, which provides an implementation of automated model fusion where models are described as decorated cospans and hierarchically composed into larger models. The implementation uses expressions within generalized algebraic theories as a computer algebra system for the syntactic representations of the models and numerical ODE solvers to simulate the dynamic behaviors that give semantics to the models. Users describe primitive models and a specification of how to connect them and the system generates a simulator for the combined system. This software uses the Catlab Library, which was recently presented to the Seminar along with dynamic code generation to build an end to end category theory based scientific application. Our illustrative example uses Petri Nets to model ecological and epidemiological phenomena.

James Koppel: Pushouts in Software Engineering -- You build something. Then Alice extends it one way. Then Bob extends it another way. Now you want to use both of their extensions, but they might not interoperate. How to reconcile? If you're a category theorist, you know the answer: pushouts! In this talk, we'll survey uses of pushouts in three domains: graph-rewriting (used in software modeling), specification refinement, and the generalization of equational rules.

Cody Roux: Running with Cats -- We present a method, developed in the late 90s, to use properties of the category of presheaves/sheaves to give an operational semantics to various free categorical theories. This method has both theoretical and practical applications, not least of which is the ability to prove decidability of conversion, and build normalization algorithms, without messy considerations of rewriting theory.

An open dynamical system yields an output in a given state, and then accepts an input and updates to a new state. At the full level of generality afforded by category theory (and in particular the generalized lens framework of Spivak), these updates can be non-deterministic, probabilistic, and more. Recently, we saw a general definition of open dynamical system. In this talk, we will look at the morphisms of open dynamical systems by looking at two examples: trajectories and hierarchical planners.

The category Poly of polynomial functors on Set has excellent formal properties: it's a distributive category in two ways, it's tensored and cotensored over Set, etc. But its objects are simply polynomials P(x) in one variable, e.g. x^2+2x+1, and its morphisms are given by a very workable combinatorial structure.

It turns out that there is a strong connection between polynomial functors and mode-dependent networks of dynamical systems, i.e. interacting dynamical systems that change who they wire to based on their internal state. The simpler mode-independent interfaces are the monomials Bx^A, where A is input and B is output. A dynamical system with state set S and mode-dependent interface P(x) is a morphism in Poly of the form Sx^S --> P(x). For example, a programmer might define a stream of B's to consist of a carrier set S and functions S->S and S->B; this is exactly the data of a map Sx^S --> Bx in Poly.

During the last two decades, a huge body of research has been dedicated to the challenging problem of reconciling data and process management within contemporary organizations. This requires to move from a purely control-flow understanding of business processes to a more holistic approach that also considers how data are manipulated and evolved by the process. In parallel, a flourishing series of results has been dedicated to the formalization of such integrated models, and to the study of the boundaries of decidability for their analysis and verification. However, in these integrated models a compositional description of the control-flow is still missing: indeed, it is not clear in the literature how to define the process component so as to guarantee the availability of significant semantic compositional operations. The lack of an algebra formalizing the control-flow makes very challenging the problem of describing and also verifying the combined models.

In this talk, I will present a categorical way for expressing fully compositional workflows, relying on the algebra of CospanSpan(Graph). In this model, the algebras employed to formalize finite-state control-flows are equipped with a plethora of algebraic operations: some of them can semantically be interpreted as sequential or parallel (with and without communication) composition of automata. However, the integration with data here is not supported yet.

Then, I will introduce the verification problem for DABs --- a data-aware extension of BPMN (Business Process Model and Notation), the standard language for modeling business processes --- to assess (parameterized) safety properties. Such integrated model exploits the model-theoretic framework of array-based systems, which allows to adapt the well-known backward reachability procedure in a full-fledged SMT (Satisfiability Modulo Theories) setting. By using suitable forms of quantifier elimination, backward reachability can be proved to be sound and complete for checking (un)safety, and interesting fragments where backward reachability is a full decision procedure can be isolated. Moreover, the SMT technology can be exploited in implementations, building on the well-known MCMT model checker for array-based system.

Finally, I will argue why the DAB model seems to be the right candidate to incorporate the compositional description of control-flows provided by CospanSpan(Graph).

We all know that the sum 1+2+4 can be evaluated to 7. What is less known, but just as easy, is that 1+2+4 can be also *partially* evaluated to 3+4. We say that the formal expressions 1+2+4 and 3+4 are related by a partial evaluation. This notion can be generalized from natural numbers to algebras over an arbitrary monad, and sometimes it gives known constructions (such as the factorization of natural numbers, and conditional expectations in measure theory).

A more difficult problem is the following. Given three formal expressions s, t and u, suppose that s and t are related by a partial evaluation, and that t and u are as well. Can we conclude that s and u are directly related by a "composite" partial evaluation? Perhaps surprisingly, the answer is not always positive, and almost never easy to get.

We can solve this problem in a number of cases borrowing methods from homotopy theory. Partial evaluations can be seen as edges between formal expressions, forming the 1-dimensional skeleton of a canonical simplicial set called the bar construction. The geometry of this simplicial set can say a lot about when and how partial evaluations compose.

This way we can show, for example, that a composite partial evaluation always exists for the case of cartesian and weakly cartesian monads.

This is a joint work with my ACT 2019 group (Tobias Fritz, Carmen Constantin, Martin Lundfall, Brandon Shapiro)

Homotopy Type Theory is a new foundations of mathematics which starts by asking what what it means to identify two mathematical objects. It depends on what type of objects they are: to identify the tangent space of the sphere at (0,0,1) with R^2, we need to choose a basis; to identify H^n(S^n; Z) with Z, we need to choose an orientation of the n-sphere; and to identify the smallest perfect number n with 6, we must prove that n = 6. So, type theory concerns itself with what type of thing everything is. As a result, we can derive what it means to identify two objects just from knowing what type of things they are.

This later property is very useful in category theory, where one is often tempted to say "...and with the obvious morphisms". In this talk, we will see how the HoTT point of view influences categorical practice. We'll see that universal properties give a unique way to identify an object, and therefore there are no issues with choosing functorial representatives of limits, or constructing an inverse to an essentially surjective, fully faithful functor -- even if one does not assume any choice principles.

So-called "regular logic" is logic constrained to truth, conjunction, and existential quantification, forming the logical substrate of a form of relational calculus with equality. From a categorical perspective, following Carboni-Walters, such relational calculus may be captured by the notion of a "discrete cartesian bicategory", aka a "bicategory of relations", in which equality behaves according to rules familiar from the study of symmetric Frobenius monoids. The close connection between Frobenius monoids and 2-dimensional cobordisms suggests the possibility of developing "surface diagrams" (and certain "directed" cobordisms between them), akin to string diagrams but one dimension up, to represent the syntax, i.e., the structure of free discrete cartesian bicategories. This talk will outline some ideas and speculations on how I think this might work.

"Structured cospans" are a general way to study networks with inputs and outputs. Here we illustrate this using a type of network popular in theoretical computer science: Petri nets. An "open" Petri net is one with certain places designated as inputs and outputs. We can compose open Petri nets by gluing the outputs of one to the inputs of another. Using the formalism of structured cospans, open Petri nets can be treated as morphisms of a symmetric monoidal category - or better, a symmetric monoidal double category. We explain two forms of semantics for open Petri nets using symmetric monoidal double functors out of this double category. The first, an operational semantics, gives for each open Petri net a category whose morphisms are the processes that this net can carry out. The second, a "reachability" semantics, simply says which markings of the outputs can be reached from a given marking of the inputs. This is joint work with Kenny Courser and Jade Master.

Starting from any operad P, one can consider on one hand the free operad on P, and on the other hand the Baez--Dolan construction on P. These two new operads have the same space of operations, but with very different notions of arity and substitution. The main result is that the incidence bialgebras of the two-sided bar constructions of the two operads constitute together a comodule bialgebra. The motivating example is the Calaque--Ebrahimi-Fard--Manchon comodule bialgebra of trees from numerical analysis. The purpose of the talk is to explain all the concepts mentioned in the abstract, and also some background on polynomial monads, simplicial groupoids, and homotopy combinatorics.

Reference: http://arxiv.org/abs/1912.11320

The Grothendieck construction gives an equivalence between fibrations and indexed categories. We will begin with a review of the classical story. We will then lift this correspondence to two monoidal variants, a global version and a fibre-wise version. Under certain conditions these are equivalent, so one can transfer fibre-wise monoidal structures to the total category. We will give some examples demonstrating the utility of this construction in applied category theory and categorical algebra.

Dynamical systems describe the evolution of physical and computational processes. Although they are traditionally studied as changing systems in a static environment, applied category theorists have been interested in studying open dynamical systems whose evolution both affects and depends on other systems in its environment. Two flavors of open dynamical systems include (1) Spivak's input/output machines which compose by feeding the output of one machine into the input of another, and (2) the input/output agnostic systems defined by Baez and Pollard to describe chemical reaction networks and which compose by sharing resources.

In this talk, we will examine the differences between these two approaches to the "openness" of open dynamical systems and define an algebra which unifies these perspectives. We will consider in detail two examples: continuous flows on a manifold induced by a vector field and non-deterministic finite state automata.

Recently we performed quantum natural language processing on an IBM quantum computer [1]. What got us to the point is the observation that quantum theory and natural language are governed by much of the same category-theoretic structure [2]. From a ML perspective, QNLP is arguably the first form of compositional machine learning where composition embodies a fundamental structure of the data involved, and which is moreover also native to the hardware it is implemented on.

The talk requires no background in quantum theory, nor in natural language theory, nor in machine learning. All relevant references are in [1, 2], where there are also the names of the people involved in getting to this point.

[1] B. Coecke, G. De Felice, K. Meichanetzidis & A. Toumi (2020) Quantum Natural Language Processing: We did it! https://medium.com/cambridge-quantum-computing/quantum-natural-language-processing-748d6f27b31d.

[2] B. Coecke (2016) From quantum foundations via natural language meaning to a theory of everything. arXiv:1602.07618.

Dual objects in monoidal categories have many applications, including channels in parallel programming, input-output modes in logic programming, and string diagrams for internal-homs. Thus, it is natural to ask whether duals intrinsically strengthen the theory, i.e. whether monoidal categories with duals are "conservative", in a suitable sense, over monoidal categories without duals. While "compact closed" duals are not generally conservative, we show that "∗-autonomous" duals frequently are: in particular, the free extension of any closed symmetric monoidal category to a ∗-autonomous category is a fully faithful embedding. Thus, "richer" languages with ∗-autonomous duals can be unambiguously used to reason about "poorer" languages that lack them.

This talk is about the same paper as my talk at ACT@UCR (video, slides), but the talks will be complementary, with no expectation that anyone attending this talk has seen the other one.

The algebraic path problem provides a general setting for the Floyd--Warshall algorithm in optimization and computer science. This work extends the algebraic path problem to networks equipped with input and output boundaries. We show that the algebraic path problem is functorial as a mapping from a bicategory whose composition is gluing of open networks. In particular, we provide an isomorphism relating the solution of the path problem on a composite to the solutions on its components.

On March 5 in this seminar, I discussed the category Poly of polynomial functors on Set and its applications to mode-dependent dynamical systems—machines that can change their interface and which other machines they wire to, based on their internal state.

At that time, I didn't know how to think about the composition monoidal structure on Poly in terms of dynamical systems, but it turns out that the story is quite nice. The composition product can be used to model strategies in the sense of game theory, as well as a way to "speed up" dynamical systems. But it comes with lots of other surprises too, both theoretical and applied, e.g. due to Gambino and Kock, Ahman and Uustalu, and Garner. It's a truly remarkable monoidal category.

In this talk I'll briefly review the previous one, so no special background is necessary.

In this talk I’ll be discussing an attempt to treat classical and quantum entropies in a unified setting which takes contextuality into account explicitly. I will show how this construction inherits most of the properties of its classical and quantum counterparts, and moreover encodes sufficient information to allow us to reconstruct quantum states directly from it.

One way to interpret a left Kan extension is as a sort of "partial colimit", which replaces parts of a diagram with their colimits. We make this intuition precise by means of the "partial evaluations" sitting in the bar construction of monads, which I explained in a previous talk. The (pseudo)monads of interest for forming colimits are the monad of diagrams and the monad of small presheves, both on the category CAT of locally small categories. (Yes, diagrams form a monad!)

We in particular show that a pointwise left Kan extension of a diagram corresponds to a partial evaluation of its colimit.

This work is motivated by analogous work that I've been doing in the context of measure and probability theory. One can indeed say that "Kan extensions are to conditional expectations as coends are to integrals". Depending on time and interest, we can explore this link too.

(Joint work with Walter Tholen.)

RChain is a distributed computing system based on a concurrent language with reflection. The ρ calculus, or reflective higher-order π calculus, is a concurrent language with operations that control the distinction between data and code. This gives networks intrinsic structure, which can offer deep knowledge and utility. This can be used to think globally about the web.

To reason about this structure, Namespace Logic [Meredith, Radestock 2005] augments the ρ calculus with first order logic, to create a predicate calculus for denoting subclasses of terms. For example, the predicate for a process to be single-threaded is "not[null] and not[par(not[null],not[null])]" -- like an integer being prime. These predicates provide types for the ρ calculus, which condition programs and enable high-level reasoning in concurrent networks.

We present a categorical formulation of the algorithm (-) + first order logic. A language can be presented as an algebraic theory with binding; we then form its topos of presheaves, and therein construct a polymorphic type system with subtyping. The algorithm extends the idea of namespace logic to a broad class of formal languages, and it is especially powerful in concurrent languages with reflection.

A draft paper can be found here.

In this talk, I will show how one can use the category of unlabeled partitions to design a causal inference algorithm. At the heart of this algorithm is a categorical translation of the concepts of dependent variable, independent variable and latent variable in terms of products and arrows. In particular, I will demonstrate how the proposed algorithm accounts for possible hidden variables, such as environment variables or noise and how it can be interpreted statistically in terms of p-values. This interpretation, from the categorical language to statistics, is made possible by a collection of theorems on the functorial nature of ANOVA. Importantly, this functorial properties can be used to provide solutions to causal inference problems with both sound algebraic and statistical properties. If time allows, I will explain how the proposed algorithm can be applied in the field of genetics to address the challenging question of making genome-wide association studies detect "combinatorial" genetic effects.

In this talk, I will argue that Markov categories provide a very general theory of information flow, and that this generalizes probability theory in a manner analogous to how topos theory generalizes set theory. First, developing probability theory synthetically in terms of Markov categories is surprisingly expressive and powerful; and second, there is a vast and largely unexplored landscape of Markov categories on which these synthetic results can be instantiated. Some basic knowledge of monoidal categories and discrete probability should be enough to follow the talk.

Using tools from categorical logic, a precise analogy is drawn between models in logic and statistics. The notion of a statistical theory is introduced as a small Markov category with extra linear algebraic structure. Models of statistical theories in a category of Markov kernels are then seen to be statistical models, in the conventional sense. Morphisms between statistical theories, and their induced model migration functors, formalize relationships between different statistical models. These ideas are illustrated by a wide range of models from classical applied statistics, such as linear models, mixed models, and generalized linear models.

Distributive laws give a way of combining two algebraic structures expressed as monads; in this paper we propose a theory of distributive laws for combining algebraic structures expressed as Lawvere theories. We propose four approaches, involving profunctors, monoidal profunctors, an extension of the free finite-product category 2-monad from Cat to Prof, and factorisation systems respectively. We exhibit comparison functors between CAT and each of these new frameworks to show that the distributive laws between the Lawvere theories correspond in a suitable way to distributive laws between their associated finitary monads. The different but equivalent formulations then provide, between them, a framework conducive to generalisation, but also an explicit description of the composite theories arising from distributive laws.

This talk is part of a series on recently published papers in the journal Compositionality. The paper can be found here.

I will give a potted history of the more mathematical versions of Dialectica Categories which were introduced some 30 years ago. Dialectica categories were used to produce models of Linear Logic, inspired by Goedel's original Dialectica Interpretation (1958), but many more applications were introduced since then. An initial application that has not been much discussed so far is to Relevant Logic. I will discuss a "cheating" way to deal with Relevant logic and why this is important for my research program, with respect to semantics of natural languages.

Cybernetic systems are those that interact with their environment to achieve some goal, though this goal may only be to continue existing. Many such systems can be characterized as performing "active" Bayesian inference: dynamically inferring the relevant external state and the course of action expected to achieve the goal. We introduce these ideas and present some first steps towards their categorical formalization as dynamical realisations of "statistical open games", concentrating on examples from neuroscience and machine learning. We show that Bayesian updates compose according to the "lens" pattern, thereby giving an abstract justification for the bidirectionality empirically observed in cortical circuits. Finally, we sketch on-going work on the structure of nested and interacting cybernetic systems.

In this talk, I will present recent joint work with Lyne Moser and Paula Verdugo, where we construct two model structures for (the category of) double categories. Unlike the model structures previously present in the literature, both of our model structures contain the homotopy theory of 2-categories, and moreover, they both induce Lack’s model structure on 2-categories, through some version of the horizontal embedding H: 2Cat → DblCat.

After recalling some preliminaries on double categories, 2-categories, and Lack’s model structure on 2Cat, we will introduce our two model structures on DblCat together with their main features, and discuss the pros and cons of each of them.

An assignment to a sheaf is the choice of a local section from each open set in the sheaf's base space, without regard to how these local sections are related to one another. This article explains that the consistency radius --- which quantifies the agreement between overlapping local sections in the assignment --- is a continuous map. When thresholded, the consistency radius produces the consistency filtration, which is a filtration of open covers. This article shows that the consistency filtration is a functor that transforms the structure of the sheaf and assignment into a nested set of covers in a structure-preserving way. Furthermore, this article shows that consistency filtration is robust to perturbations, establishing its validity for arbitrarily thresholded, noisy data.

This talk is part of a series on recently published papers in the journal Compositionality. The paper can be found here.

This is the third of a series of talks on a categorical approach to approximating Markov processes by averaging. In the first, I described a functorial view of conditional expectation and in the second I described how one could use this to define an approximation of a Markov process. In this talk I will show how to construct a family of finite approximations to a Markov process and how to reconstruct the Markov process as the colimit of this diagram. Along the way, I will show that this is a minimal realization of the Markov process. While this talk builds on the first two, I will try to provide enough of a recap so that it will be self contained.

An algebraic expression like 3 + 2 + 6 can be evaluated to 11, but it can also first be partially evaluated to 5 + 6 or 3+8 and then evaluated to 11. For any algebraic structure described by an algebra of a monad, formal expressions like this can be treated as points in a space with partial evaluations as directed paths between them. The monad structure also provides higher dimensional cells in this space, formally a simplicial set called the bar construction. Computational properties of partial evaluations such as transitivity and symmetry, or similarly the extent to which partial evaluations behave like morphisms in a category or groupoid, correspond to geometric properties of the bar construction. This talk will cover this correspondence between computation, compositionality, and combinatorial spaces, with examples of algebraic theories illustrating how composition of partial evaluations can come in many forms, when it even exists at all.

A polynomial functor is a sum of representables Set --> Set. As you might expect or know, the morphisms between them are the natural transformations, and polynomial functors can be composed one after the other, giving a monoidal structure. Who would guess that comonoids for this composition monoidal structure---polynomial comonads---are exactly categories?! Every category is a polynomial comonad, and every polynomial comonad is a category.

This striking result of Ahman and Uustalu leads to a categorical treasure box, full of unexpected connections. I'll begin to lead you through it with the help of a simplifying notational tool, which I call poly-boxes. I'll use poly-boxes to show why polynomial comonads are categories, and how to think about the morphisms between them, which are being called cofunctors. Time permitting, I'll explain why bimodules between polynomial comonads are parametric right adjoints between copresheaf categories, sometimes called the more friendly-sounding "data-migration functors" in applied category theory circles.

The usual tensor product operations of algebras and bimodules provide the bicategory of algebras, bimodules and bimodule morphisms with a symmetric monoidal structure. The coherence data for this structure is naturally expressed as the coherence data of a simpler object: The symmetric monoidal double category of algebras. This situation is expected for reasonable module-like bicategories, but ultimately depends on a choice of 'lift' to a double category with a specified category of vertical arrows. Such lifts are known to exist in particular cases, or under the presence of additional structure, e.g. a cartesian or cocartesian monoidal fibration, but no generally applicable lifting methods are known. This is problem is particularly acute when considering symmetric monoidal structures on bicategories and tricategories of operator algebras.

Globularly generated double categories are minimal solutions to lifting problems for bicategories. I will introduce the globularly generated condition and I will mention recent results on both the internal structure of globularly generated double categories and on the structure of the category of globularly generated double categories. I will explain in particular how these results allow for the construction of two previously unknown inequivalent double categories of von Neumann algebras.

Scientists and engineers manage the blistering complexity of the natural world by telling simplified stories that focus on just a small part, and with just a particular narrative. These simplified stories are called systems, and every different field has a different notion of system tailored the kinds of questions its practitioners are asking, and the kinds of interventions they seek to make. Electrical engineers use circuit diagrams, epidemiologists and chemists use Petri nets, biologists use continuous time Markov processes, physicists use Lagrangians and Hamiltonians, computer scientists use deterministic automata, decision theorists use Markov decision processes, and everyone uses systems of differential equations.

These fields also have a sense of how their systems can be put together --- composed --- to form more complex systems. Circuits may be plugged into one another, Petri nets may share species, Markov processes may share places, Lagrangian and Hamiltonian systems may share variables, the output of one automaton may be fed into the input of another, and parameters of differential equations may be set by the variables of other differential equations. These examples fall into three general kinds:

• Port Plugging: A system has a boundary of ports, or exposed places, and systems are composed by plugging in ports or gluing together exposed places.
• Variable Sharing: A system exposes some of its variables. Systems are composed by sharing variables --- that is, by setting two exposed variables equal.
• Input/Output: A system exposes some of its variables (outputs) and depends for its definition on some parameters (inputs). Systems are composed by setting parameters as functions of exposed variables.

In each of these paradigms of composition, there are many different specific doctrines of system: circuits, Petri nets, Markov processes in the port plugging paradigm; Hamiltonian and Lagrangian mechanics in the variable sharing paradigm; deterministic automata, Markov decision processes, and systems of differential equations in the input/output paradigm.

Applied category theorists have set out to make formal the ways these systems can be composed in order to study the way the behaviors --- trajectories, solutions, steady states, operational semantics, etc --- of composite systems relate to the behaviors of component systems. In this talk, I will give a formal definition of paradigm of composition which includes the three above, and show how this notion organizes much of the recent work in categorical systems theory. I will argue that the basic algebra of composing open systems is a doubly indexed category, and give examples of doubly indexed categories of systems. Time permitting, I will then talk about how behaviors of systems can be organized into lax doubly indexed functors.

An important property of bicategories is biclosedness, i.e. the functors giving composition have right adjoints in each variable. Most good bicategories are part of naturally occurring double categories, and this point of view often simplifies things considerably. However the internal homs, those right adjoints just mentioned, are not functorial at this level. The problem is that in the domain variable they are neither covariant nor contravariant, but a combination of both. To remedy this failure we introduce retro cells. We see how this naturally leads to cofunctors.

The original development of quantum theory was tumultuous and a good mathematical description was only found after decades of ad-hoc explanations of physical phenomena. This is in contrast to the development of relativity where a strong grounding in physical principles led to a mathematical theory, even without much empirical evidence. This raises the question of whether quantum theory could have been derived from physical principles as well, and what those principles would be. This quest of finding physical principles and deriving quantum theory from it has a long history, but the last 20 years especially has seen a renewed interest in the question. Modern reconstructions are in general much more focused on the compositional structure of physical systems, having many principles fundamentally depend on the interaction between subsystems.

In this talk I will present a reconstruction of quantum theory based on 'effectus theory' as developed by Jacobs et al. An effectus is a very basic type of category that has the minimal structure necessary to talk about many familiar operational concepts (states, effects, probabilities). I define a special type of effectus I call a 'pure effect theory' where there is a notion of pure transformation, and those pure transformations form a dagger-category. I show that when the probabilities in the effectus are the regular real numbers, the effectus must consist of Euclidean Jordan algebras. By additionally requiring the existence of tensor products this reduces further to the standard mathematical framework of quantum theory.

This talk is part of a series on recently published papers in the journal Compositionality. The paper can be found here.

I will introduce and discuss monad-comonad interaction laws (Katsumata, Rivas, Uustalu, LICS 2020) as a mathematical concept and a device for formalizing interaction protocols between effectful computations and coeffectful environments where they may be placed to run. For an example of such interaction, think of a program relying on a memory service provided by a machine on which it is run, or a program trusting such a machine to make choices for it. Memory access and choices as services requested are effects; as services provided, they are coeffects.

I will especially focus on a certain connection between monad-comonad interaction laws, monad algebras and comonad coalgebras. Besides its mathematical content, this connection is interesting because monad algebras formalize effect handlers in programming semantics. This is based on joint work with Niels Voorneveld (APLAS 2020).

Automatic differentiation (AD) in reverse mode (RAD) is a central component of deep learning and other uses of large-scale optimization. Efficient AD has previously appeared complicated primarily due to two unfortunate choices of representation: graphs and matrices. Commonly used RAD algorithms such as backpropagation are complex and stateful, hindering deep understanding, improvement, and parallel execution. Moreover, these algorithms are typically presented without proof, and even without precise specification in terms of differentiation.

This talk presents an inevitable, functorial specification of AD and solves the implied homomorphism equations to produce a simple, generalized, correct-by-construction AD algorithm. The general algorithm is then specialized by varying the representation of derivatives. In particular, applying well-known constructions to a naive representation yields two RAD algorithms that are far simpler than previously known. These algorithms are inherently parallel-friendly and usable directly from an existing programming language with no need for new data types or programming style, thanks to use of an AD-agnostic compiler plugin. In retrospect, the suitability of category theory is suggested by the compositional properties of differentiation.

The recipe used in this talk to calculate an efficient AD algorithm exemplifies a methodology for defining and constructing correct and elegant software.

There was a small buzz among TDA people in 2017-18 about applications of fuzzy set theory. I thought at the time that we should get the foundations right, so that's what the Compositionality paper "Fuzzy sets and presheaves" is about.

The outcome of the early dreams of application have been a bit mixed. I initially believed that fuzzy simplicial sets would lead to an understanding of TDA in terms of local homotopy theory, but we're still waiting for a good sheaf theoretic application. There was also the introduction of the UMAP algorithm by Healy-McInnes in 2018, which depended aggressively on a gluing construction in the fuzzy set category. This algorithm has been highly successful for applications in cluster analysis, but the construction itself was a black box for almost everybody on account of the fuzzy content. It turns out to be far better to take a presheaf theoretic approach to construct and analyze the variations of the UMAP complex directly, and to actually understand what they are.

This talk is part of a series on recently published papers in the journal Compositionality. The paper can be found here.

Markov categories are a recent category-theoretic approach to the foundations of probability and statistics. Here we develop this approach further by treating infinite products and the Kolmogorov extension theorem. This is relevant for all aspects of probability theory in which infinitely many random variables appear at a time. These infinite tensor products come in two versions: a weaker but more general one for families of objects in semicartesian symmetric monoidal categories, and a stronger but more specific one for families of objects in Markov categories.

As a first application, we state and prove versions of the zero--one laws of Kolmogorov and Hewitt--Savage for Markov categories. This gives general versions of these results which can be instantiated not only in measure-theoretic probability, where they specialize to the standard ones in the setting of standard Borel spaces, but also in other contexts.

This talk is part of a series on recently published papers in the journal Compositionality. The paper can be found here.

Given a representation of a unital C∗-algebra A on a Hilbert space H, together with a bounded linear map V:K → H from some other Hilbert space, one obtains a completely positive map on A via restriction using the adjoint action associated to V. We show this restriction forms a natural transformation from a functor of C∗-algebra representations to a functor of completely positive maps. We exhibit Stinespring's construction as a left adjoint of this restriction. Our Stinespring adjunction provides a universal property associated to minimal Stinespring dilations and morphisms of Stinespring dilations. We use these results to prove the purification postulate for all finite-dimensional C∗-algebras.

This talk is part of a series on recently published papers in the journal Compositionality. The paper can be found here.