Upcoming talks

May 28: David Spivak (MIT)

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.

June 4: Carmen Constantin (Oxford)

June 11: Paolo Perrone (MIT)

June 18: Christian Williams (UC Riverside)

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.

June 25: Remy Tuyeras (MIT)

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.

July 16: Tobias Fritz (Perimeter Institute)

July 23: Evan Patterson (Stanford)

August 6: Valeria de Paiva (Topos Institute)

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.

August 13: Toby St Clere Smithe (Oxford)


Past talks

2018

February 15 : Brendan Fong
An overview of Coecke, Sadrzadeh, and Clark's Mathematical foundations for a compositional distributional model of meaning.

February 22 : David Spivak
Fuzzy simplicial sets I.

March 1 : David Spivak
Fuzzy simplicial sets II.

March 8 : Brendan Fong
An overview of McInnes and Healy's UMAP: Uniform manifold approximation and projection for dimension reduction.

March 29 : Brendan Fong
The equivalence of hypergraph categories and lax monoidal functors Cospan(FinSet) --> Set.

April 5 : Enrique Boroquez (UNAM)

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.

April 12 : David Spivak

April 19 : Remy Tuyeras
How to do genetics with category theory I.

April 26 : David Spivak

May 10 : Remy Tuyeras
How to do genetics with category theory II: Recognition of biological mechanisms.

May 17 : Christoph Dorn (Oxford)

"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.

May 24 : Tim Havel
(Slides)

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.

May 31 : Brendan Fong
Causal theories: a categorical approach to Bayesian networks.

June 7 : David Spivak

June 14 : Remy Tuyeras
How to do genetics with category theory III.

June 21 : Brendan Fong

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.

July 19 : David Spivak

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".

July 26 : David Spivak

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".

August 2 : Antwane Mason (Rensselaer Polytechnic Institute)

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.

August 9 : David Spivak

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.

August 16 : Brendan Fong

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.

August 23 : David Spivak
An introduction to double categories

August 30 : Brendan Fong
2-categories and adjunctions

September 10 : David Spivak
Adjunctions and Mates

September 17 : Remy Tuyeras

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.

October 1 : Reuben Cohn-Gordon (Stanford)

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.

October 11 : Paolo Perrone (Max Planck Institute for Mathematics in the Sciences)

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.

October 15 : David Myers (Johns Hopkins University)

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.

October 29 : Lee Mondshein

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.

November 5 : Remy Tuyeras

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.

November 19 : Ed Wike
(Slides)

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.

November 26 : David Spivak

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.

December 3 : Alex Kavvos (Wesleyan)

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.)

December 10 : Brendan Fong

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.

2019

January 31 : Jules Hedges (Oxford)

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.

February 7 : Brendan Fong
An overview of Ellerman's Partition Logic.

February 14 : Brendan Fong

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.

February 21 : Tobias Fritz (Perimeter Institute)

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.

February 28 : Sam Tenka

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.

March 7 : Brendan Fong

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.

March 21 : Rúnar Bjarnason (Unison Computing)

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.

March 28 : Anthony Bau

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.

April 4 : Natalie Stewart

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.

April 11 : David Spivak

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)

May 2 : David Spivak

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.

May 9 : Alberto Speranzon (Honeywell)

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.

May 16 : Diego Roque

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

May 23 : David Spivak

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.

May 30 : Mitchell Riley (Wesleyan)

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.

July 30 : Kenneth Harris (UCL)

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.

August 8 : Gershom Bazerman (Awake Security)

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.

August 15 : Daniel Rosiak (DePaul)

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.

August 22 : Brendan Fong

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.

August 29 : Ben Sherman

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.

September 26 : Simon Cho (Michigan)

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.

October 3 : David Spivak

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.

October 10 : Brendan Fong

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.

October 17 : John Burnham (Sunshine Cybernetics)

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.

November 21 : Alex Lew

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.

December 5 : Tai-Danae Bradley (CUNY)

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.

2020

January 16: Evan Patterson (Stanford)

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.

January 23: Andrea Censi (ETH Zurich)

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.

January 30: David Jaz Myers (Johns Hopkins)

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.

February 6: James Fairbanks (Georgia Tech)

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.

February 13: James Koppel and Cody Roux

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.

February 20: David Jaz Myers (Johns Hopkins)

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.

March 5: David Spivak (MIT)

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.

March 12: Alessandro Gianola (Free University of Bozen-Bolzano)

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).

March 19: Paolo Perrone (MIT)

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)

March 26: David Jaz Myers (Johns Hopkins University)

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.

April 2: Todd Trimble (Western Connecticut State University)

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.

April 9: John Baez (UC Riverside)

"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.

April 16: Joachim Kock (Universitat Autònoma de Barcelona)

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

April 23: Joe Moeller (UC Riverside)

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.

April 30: Sophie Libkind (Stanford)

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.

May 7: Bob Coecke (CQC & Oxford Uni)

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.

May 14: Mike Shulman (San Diego)

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.

May 21: Jade Master (UC Riverside)

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.