The Topos Institute Berkeley Seminar is a weekly, informal seminar on topics relevant to the Topos Institute community, held at our Berkeley Campus. Unless otherwise noted, the talks will begin at 11am PT on Tuesdays.
RSVP at the Google Form here. Please note that, unlike many academic departments, the Wells Fargo building is a secured space, so if you don’t remember to RSVP you’re likely to be delayed on arrival.
Talks are often recorded and posted to our Berkeley Seminar YouTube playlist. Links to recordings and slides from past talks are also available below.
Amortized Analysis via Coalgebra
Harrison Grodin Dec 3, 2024
Amortized analysis is a technique for analyzing the efficiency of operations on a data structure in which cost is studied in aggregate: rather than considering the cost of a single operation in isolation, one bounds the total cost encountered throughout multiple operations in sequence. Traditionally, amortized analysis is phrased inductively, quantifying over finite sequences of operations. Connecting to prior work on coalgebraic semantics for data structures, we develop the alternative perspective that amortized analysis is naturally viewed coalgebraically in a category of cost algebras. In addition to simplifying the precise definition of amortized analysis, this perspective also generalizes the technique to other settings and incorporates type- and category-theoretic intuition.
What is it like to be a lax double functor?
Kevin Carlson Nov 19, 2024
I will attempt to impart the vibe that the models of double theories that are the basis of CatColab are certain kinds of families of categories, even though the definition looks like a generalization of the families of sets we know and love as presheaves. Furthermore, CatColab does (on a sufficiently bleeding-edge branch) contain families of sets that live over these families of categories in an appropriate way, which we call instances of models of double theories. (Deep breath.) Probably only two people know what those are, yet, so let me try to tell you, because they're going to be important; it's not all that bad, just new.
Cartesian polynomial monads in HoTT
Dennis Chen Nov 12, 2024
Modern math has shown the necessity of higher categories and higher structures. Infinite coherence data arises quite naturally as one considers various types of topological spaces and homotopy theory, as well as modern treatments of algebraic geometry. One can see simple versions of this problem already when looking at path composition in a topological space. Path composition is not strictly associative, but only associative up to a higher cell. One promising method of presenting higher structures is the development of homotopy type theory, which formulates spaces (up to homtopy equivalence) as its basic objects. However one major obstacle is notating the infinite coherences of infinity categories in homotopy type theory. This is due to the autophagy problem: how can one talk about algebraic structures on types, if the algebraic structures themselves are encoded as types? Here we discuss a solution to the problem by Finster, Allioux, and Sozeau by axiomatizing the nature of polynomial monads, hence allowing themselves certain computational equalities. They then go on to use these polynomial monads to discuss higher structures including higher categories. Essential to their method is Baez and Dolan's slice construction, which is able to capture infinite coherences of polynomial monads even if one starts from very strict, classical polynomial monads. This integration of HoTT with polynomial monads I believe is incredibly interesting and could prove to be a very useful foundation/computational system.
Lightning talks
everyone Oct 29, 2024
Two takeaways from ACT2Infer
Sophie Libkind Oct 22, 2024
In September, David Spivak and I hosted the ACT2Infer workshop which brought together experts in applied category theory and active inference together in order to begin the process of articulating and clarifying the underlying principles of active inference via the formalism of category theory. In this two-part talk I'll (1) share the logistics of hosting this workshop and (2) share my main conceptual takeaway --- a polynomial functor account of active inference.
Collaborative modeling with domain-specific categorical logics: the early design of CatColab
Category theory is a toolbox to build and interoperate formal languages for a wide array of domains, from logic and programming to data science and statistics to science and engineering. Despite having transformative potential, this viewpoint is not yet widely appreciated outside of specialized research communities. We believe that category-theoretic modeling can become a mainstay if it is embodied in useful technologies that do not require their users to have specialized mathematical knowledge. To this end, we are building CatColab, a new platform for formal, interoperable, conceptual modeling within domain-specific categorical logics. In this talk, we describe our early progress on CatColab, focusing on the interplay between the mathematical foundation and its embodiment as a technology intended for human use.
Monad Translations Compose
David Espinosa Oct 8, 2024
Many people have observed that monad translations compose. We give this idea a try using the ML module system and see what mileage we can get out of it.
Safety by Shared Synthesis
Shaowei Lin Sep 24, 2024
Today, critical infrastructure is vulnerable to both malicious attacks and unintended failures, and these risks are expected to grow in the foreseeable future. Deploying formal verification (FV) across critical cyber physical systems would dramatically improve safety and security, but has historically been too costly to use outside the simplest or most critical subsystems. AI could allow widespread use of FV in years not decades, shifting cyber risks strongly in favor of defense. In this talk, I will outline our report with Atlas Computing on AI-enabled tools for scaling formal verification (https://atlascomputing.org/ai-assisted-fv-toolchain.pdf). I will also discuss some lessons that I learnt along the way, especially about shared synthesis - the collaborative construction of formal specifications, implementations and proofs.
Lightning Talks
everyone Sep 17, 2024
Stateful Lenses: A Recipe for Expressive Systems-Theoretic Cartesian Double Categories
Owen Lynch Sep 10, 2024
This is a talk on work-in-progress that was started with
David Spivak, and this abstract should be seen as "well-motivated
conjecture" rather than math that has been completely worked out.
Double categorical systems theory tells us how to unify various types
of system under a single heading: operad algebras of symmetric
monoidal double categories. Both resource sharers being composed by
undirected wiring diagrams and Moore machines being composed by
directed wiring diagrams are examples of double categorical systems
theories. However, it turns out that both resource sharers and Moore
machines can be found in the same (cartesian!) double category:
resource sharers make up the horizontal morphisms into the
(vertically) terminal object, and Moore machines make up the
horizontal morphisms out of the (vertically) terminal object. Even
better, variants of this construction produce both discrete and
continuous resource sharers/Moore machines. Another special case of
these stateful lenses include the "energy-driven open systems" from
Spivak, Capucci, and _'s "Organizing Physics" paper. Finally, the fact
that stateful lenses form a cartesian double category dramatically
reduces the amount of structure in formulating them compared to the
double operad/operad algebra perspective on Moore machines/resource
sharers.
Roads not (yet) taken: Some times when more mathematical structure might have helped in the progress of Economics
Owen Haaga Sep 3, 2024
At more than a few points in the history of economic thought, a promising modeling strategy or line of research has stagnated, failed to deliver actionable results, or been abandoned. I would like to suggest that in many cases, researchers have been forced to throw away too much problem structure in the pursuit of tractability, and that newer modeling technology could solve that problem.
It makes sense to look for applications of new mathematical modeling techniques at the cutting edge of economics as it is currently practiced, as well as by reasoning about the domain from first principles. I would suggest that it's also worthwhile, in between these two extremes, to revisit stalled (or perhaps "paused") modeling efforts from the past, to see if the ability to handle more of the relevant structure can unlock new insights going forward.
This talk will highlight a few currently overlooked modeling agendas in economics, in the hope that one or more of them may provide some inspiration for working applied category theorists with an interest in economic applications. Time permitting, examples will include Input-Output modeling, Flow-of-Funds accounting, and the Cambridge capital controversy, with a possible digression into survey weighting methods.
Categorical approaches to inferentialist semantics
Kris Brown Aug 27, 2024
There are remarkable similarities between applied category theory and inferentialist semantics in the philosophy of language: a focus on making pre-existing structure explicit, sensemaking without rigid foundations, characterizing content in terms of external structure rather than internal structure, emphasis on open systems, and putting syntax and semantics in the same playing field. I will present some formalizations of inferentialism (a generalization of Girard's phase semantics) due to Hlobil and Brandom and show some progress towards understanding what is taking place, categorically.
As one might expect, a generalized Fibonacci sequence is a doubly-infinite sequence of integers in which every term is the sum of the two previous, such as
..., -11, 8, -3, 5, 2, 7, 9, 16, 25, 41, ...
We will see that it is possible to give an unambiguous mathematical definition of the middle term of such a sequence, and that doing so leads to a means of organizing all Fibonacci sequences that is natural, compelling, and beautiful.
Composing Instantaneous Machines
Keri D'Angelo Aug 6, 2024
In this talk, I’ll discuss recent progress Sophie and I have made on composing instantaneous machines. Instantaneous machines means that at any point in time, input can be given to the machine and the machine will give output based on this input and its current state. In this talk, I’ll show how we can compose such machines. We first create an extended category of directed wiring diagrams accounting for the dependency between input and output, and then define an operad algebra giving us the semantics that defines composition. Depending on where the interest lies, we can delve into some details including that since the output now depends on the input, we come into the “problem” that every time the output changes, the input may also change. This can be accounted for by giving a fixed point that shows after finite time, our input and output will stabilize.
Lawvere's categorical formulation of algebraic theories enables one to study some of the most common structures found in mathematics – e.g. groups, rings, etc. – at a high level of precision and generality. However, many significant mathematical concepts, including categories, topological spaces, etc., turn out not to be algebraic, in this sense. Notably, the very framework used by Lawvere to describe algebraic theories and their models – categories with finite products and product-preserving functors between them – cannot be described as an algebraic theory, and so it seems that algebra alone cannot encompass the whole of mathematics (nor even itself). There is, however, a deeper sense in which all of mathematics is essentially algebraic. What is needed to reveal this fact is to adapt the classical notion of algebraic theories, which are fundamentally simply typed, to an appropriate notion of dependently typed algebraic theories. At this level of generality, one is capable of defining not only individual mathematical structures, but structures that themselves encompass whole universes of mathematics, including topoi, models of type theory, etc. In particular, the theory of dependently-typed algebraic theories is itself describable as a dependently-typed algebraic theory. This fact has many profound consequences, of which I shall highlight just one: using the framework of dependently-typed algebraic theories, one can construct a type theory whose types themselves correspond to type theories, with functions between these types corresponding to translations between the corresponding type theories.
Free cocompletions made friendly?
Kevin Carlson Jul 23, 2024
Lots of us are familiar with computations in Poly, some of which are made really nice by the fact that Poly is the category of families in Set^op, more formally, the free cocompletion of Set^op under coproducts. Free cocompletions under all colimits are also really important; they're presheaf categories! However, presheaf categories are kind of annoying to actually calculate colimits in (coequalizers of sets are scary), in contrast to how trivial it is to calculate coproducts of polynomials. Free cocompletions are supposed to be closing a category up under "formal" colimits in some sense, so shouldn't taking the colimits also be "formal"?
Actually, it can be! There is a category structure on the class of all small diagrams in C that models the free cocompletion of C in an extremely elementary way with lots of nice properties. This has been known to a few people, such as Andrée Ehresmann, for decades, and in the case of free cocompletions under filtered colimits to a lot more people, such as Grothendieck, but has only been known to me for a couple of weeks. I'd like to make it known to you too. I'm hoping this will be helpful both for generalizations of Poly beyond mere sets of positions and for better expressing data migrations, which is all about writing down functors from a category into a free cocompletion.
Building the science of predictive systems for AI safety
Adam Shai Jul 16, 2024
What computational structure are we building into large language models when we train them on next-token prediction? Here, we present evidence that this structure is given by the meta-dynamics of belief updating over hidden states of the data generating process. Leveraging the theory of optimal prediction from Computational Mechanics, we anticipate and then find that belief states are linearly represented in the residual stream of transformers, even in cases where the predicted belief state geometry has highly nontrivial fractal structure. Furthermore we demonstrate that the inferred belief states contain information about the entire future, beyond the local next-token prediction that the transformers are explicitly trained on. We will then zoom out and quickly mention a number of fun and interesting topics which Computational Mechanics touches on, and will follow the conversation wherever it goes.
Lightning Talks
Everyone Jul 9, 2024
Communicating Relational Thinking
Priyaa Srinivasan Jul 2, 2024
In this talk I will give an overview of our recently completed experiment of communicating categorical thinking to a STEM-oriented audience outside mathematics. Angeline, Brendan, Paul and myself recently authored a free online textbook titled "Relational thinking: from Abstractions to Applications". In this talk, I will walk through the contents of the book and equally importantly the open source technologies behind the book. This talk is an invitation to the audience not only to read the book but also to create their own inclusive material around category theory / math leveraging new technologies.
Lightning Talks
everyone Jun 25, 2024
A tour of EM(Cat#)
David Spivak
(Topos Institute)
May 20, 2024
Small categories are graphs with extra structure: namely, every path
"composes" to form an arrow. As such, small categories are algebras for a
certain monad—the "paths" monad—on the category of graphs. This monad is
familial, i.e. its underlying functor can be identified with a loose map in
the double category Cat#.
But what is an appropriate sort of morphism between monads in Cat#? Shulman's "monoids and modules" construction doesn't apply, because Cat# doesn't have local coequalizers. Instead we consider Lack and Street’s (2002) construction of the free completion of Cat# under Eilenberg-Moore objects, denoted EM(Cat#). Its objects are monads m in Cat# and its morphisms m→n are "quintets" satisfying expectable properties; as the name would suggest, these morphisms induce functors m-Alg → n-Alg between the associated Eilenberg-Moore categories. The 2-cells in this "free completion" are slightly surprising—in particular, they are more flexible than those of (Street 1972)—but still simple to describe.
We'll discuss various examples of objects in EM(Cat#), i.e. monads in Cat#, e.g. those arising from cofunctors out of a category, from functors into a category, from Grothendieck topologies on a category, from multicategories, and more. Then we'll discuss morphisms in EM(Cat#), e.g. a free-forgetful adjunction for algebras, a method for turning convex spaces into monoids, one that takes the category of elements of a copresheaf, and perhaps more.
In the category of Polynomial functors, the substitution monoidal
product $\mathbin{\triangleleft}$ is not symmetric. In this talk, we will
explore how distributive maps $p \mathbin{\triangleleft} q \to q
\mathbin{\triangleleft} p$ give notions of "conditioning". These notions in
probabilistic conditions (such as "conditioned on it being sunny, what is the
probability that I will go outside") and namespace conditioning (such as searching "what
directories satisfy the condition of containing 3 files"). Of particular
interest will be a derivation of Bayesian inference, whose key insight is a
simple braiding map.
Category theory over a minimalist or no foundation
Giovanni Sambin Apr 22, 2024
I call dynamic construction the vision of mathematics as a human enterprise. Truth is not universal and given, but local and constructed, which ultimately means a judicious management of certain and reliable information. The corresponding foundation is minimalist in assumptions, since it aims to maximize conceptual distinctions. However, in a dynamic view there is no single formal system or single language, however powerful, not even that of categories, to which the activity of mathematicians can be reduced.
After a quick introduction to dynamic constructivism and to the minimalist foundation, I will illustrate some technical modifications and additions to category theory and topos theory that they suggest: mathematization of existential statements (related to the absence of the Law of Excluded Middle), abstract treatment of well-foundedness and of effectivity (related to the absence of Power Set Axiom and of the Axiom of (unique) Choice, respectively).
Lightning talks
Everyone! Apr 15, 2024
Products in double categories, revisited
Evan Patterson
(Topos Institute)
Apr 8, 2024
Pattern runs on matter
Sophie Libkind
(Topos Institute)
Mar 25, 2024
Interviews run on people, programs run on computers, voting schemes run on voters, games run on players. Each of these is an example of the abstraction “pattern runs on matter”. In these cases, pattern determines the flow of how a situation might unfold, while matter responds with decisions at each juncture. In this talk, we will show how the free monad monad in the category of polynomial functors with the substitution monoidal product represents “pattern” while the cofree comonad represents “matter”. Lastly, “runs on” is represented by a naturally arising interaction law between a free monad and a cofree comonad.
Doctrine-specific ur-algorithms
Mohamed Barakat
(University of Siegen)
Mar 18, 2024
Various constructions of categories have a universal property expressing the freeness/initiality of the construction within a specific categorical doctrine. Expressed in an algorithmic framework, it turns out that this universal property is in a certain sense a doctrine-specific “ur-algorithm” from which various known categorical constructions/algorithms (including spectral sequences of bicomplexes) can be derived in a purely computational way. This can be viewed as a categorical version of the Curry-Howard correspondence to extract programs from proofs.
A Theoretical Computer Science Perspective on Consciousness and Artificial General Intelligence
Lenore Blum
(CMU)
Feb 12, 2024
The quest to understand consciousness, once the purview of philosophers and theologians, is now actively pursued by scientists of many stripes. We have defined the Conscious Turing Machine (CTM) for the purpose of investigating a Theoretical Computer Science (TCS) approach to consciousness. For this, we have hewn to the TCS demand for simplicity and understandability. The CTM is consequently and intentionally a simple machine. It is not a model of the brain, though its design has greatly benefited - and continues to benefit - from cognitive neuroscience, in particular the global (neuronal) workspace theory. Although it is developed to understand consciousness, the CTM offers a thoughtful and novel guide to the creation of an Artificial General Intelligence (AGI). For example, the CTM has an enormous number of powerful processors, some with specialized expertise, others unspecialized but poised to develop an expertise. For whatever problem must be dealt with, the CTM has an excellent way to utilize those processors that have the required knowledge, ability, and time to work on the problem, even if it, the CTM, is not aware of which of the processors these may be. This is joint work with Manuel Blum and Avrim Blum.
Probing the Developmental Landscape of Neural Networks
Jesse Hoogland
(Timaeus)
Feb 5, 2024
Do neural networks learn gradually and continuously, or does their learning occur in sudden, discontinuous shifts? In this talk, I will argue that neural network development occurs through distinct developmental stages, drawing an analogy with developmental biology. The learning process of neural networks can be seen as navigating a developmental landscape, in which developmental milestones are geometric structures that guide networks from an initial "pluripotent" state to a final "differentiated" form. To make this case, I will present the theoretical background behind this research, highlighting connections to algebraic geometry, statistical physics, and singular learning theory. In addition, I will present empirical evidence from recent papers that discover interpretable developmental stages in real-world systems. The talk will conclude by exploring potential future applications of these insights, particularly in interpreting the internal workings of neural networks.
The 2-category of categories, controls, and flows
David Spivak
(Topos)
Jan 29, 2024
For any monoidal category C, there is an associated 2-category Comod(C) of comonoids in C, homomorphisms, and what I'll call natural cotransformations between homomorphisms; colax monoidal functors C→D induce 2-functors Comod(C)→Comod(D). I'll briefly discuss the 2-category Comod(Rel) associated to Rel as a monoidal category, but we'll focus on the 2-category Cat^# associated to the monoidal category of polynomial functors under substitution. I'll also briefly discuss a certain colax monoidal functor Poly→Rel relating them. An object in Cat^# is a category c, whose objects and morphisms we imagine as the points and paths in c as a kind of space. A morphism c→d is a cofunctor, which we imagine as a d-control on c; we refer to a natural cotransformation between these controllers as a flow, which looks something like a homotopy. This imagery is especially vivid in the case of 𝓎^ℝ-control on the fundamental groupoid of a space. We'll explore how various flavors of polynomial monoids m represent various monoidal structures on m-controlled categories.
Polarity tagging is the task of taking a sentence and indicating which words are in upward-entailing or downward-entailing positions. So the topic is relevant to natural language semantics and to computational semantics. The talk will mainly be about the theory, and one would not need to know about the applications to understand it.
Prior work mainly worked with sentences drawn from relatively simple forms of categorial grammar, or it incorporated proof-theoretic tools based on the Lambek Calculus. While much of that work had interesting and useful results, the overall topic has not been extended to handle stronger grammatical formalisms which make use of flexible type systems. It also had not been extended in a semantic way, in ways that we shall make precise. This paper proposes such extensions. We work with type hierarchies built from preorders and monotone/antitone functions, rather than sets and functions. We adapt higher-order combinators such as type raising and composition to the ordered setting, and crucially we do the same for argument raising. Our exposition aims at the mathematics and tries to clarify some of the subtle points in this subject, points that easily lead to errors.
Algebraic data types (i.e. sum types, product types, and recursive types) are a solid foundation for data that can be interchanged between programs. There are many software libraries that allow cross-language serialization of algebraic data types, and software based on these libraries is used across the industry. However, it is impossible to express self-reference within algebraic data types. Specifically, one can write down a type of lists as an algebraic data type, but one cannot write down the type of "a list of strings, and a valid index into that list", or more advanced structures like graphs or petri nets. One might think that dependent types are needed for this, but in fact a small extension of the theory of algebraic data types based on constructions standard in System F suffices to express the validity constraint for indices into arrays. With this extension, we can well-type many more data structures, including acsets, within a type theory that also encompasses algebraic data types.
We then discuss two potential semantics for this type theory. The first semantics is in groupoids, which is related to the fact that self-referential structures have natural symmetries based on "relabelings" of their combinatorial data. This semantics builds off of the "stuff types" introduced by Baez and Dolan in their 2000 paper "From Finite Sets to Feynman Diagrams." While this semantics captures the symmetries of self-referential data, the second semantics captures the mutation of self-referential data. Specifically, we posit that the essense of both in-place mutation and version control is that updating only part of a data structure should be treated differently than simply replacing the data structure with a new copy. Thus, for every data structure (expressed as a type in this type theory), there should be a category where the objects are seen as values and the morphisms are edits. The essence of version control is then a way of remembering the history of values and edits. We propose that such a history should be a finitely-presented poset along with a functor into the category of values and edits.
In this talk, we will mainly give an overview of all of this material, without going too far into the mathematical details, concentrating on the overall vision of structured version control for combinatorial/self-referential data.
Color Logic: a language for CT education and research
We have a magic power: we can draw an entire matrix of categories with the stroke of a pen. In this talk, we begin to explore the visual language of dependent categories.
The basic concepts of CT are systematized in the language of a bifibrant double category, also known as a proarrow equipment or framed bicategory. The language can be visualized in colors, strings, and beads; and we propose a three-part story which gives the full language of CT, without requiring any math background.
My thesis constructs the complete metalanguage of bifibrant double categories. Miraculously, the visual language expands into the third dimension: a "flow" from an inner bead to an outer bead is a transformation from one double profunctor into another. Double categories have two distinct kinds of profunctors, and both of these dimensions have yet to be explored. We propose a research program based on this language.
Yet in the hour, as stated above, this presentation focuses mainly on the basics of the visual language of dependent categories.
We present an abstract version of the Operational Transform algorithm
for collaborative editing (Ellis and Gibbs, 1989). The algorithm is a
functor from Time to State, where Time is a lattice and State is a
commutative category. We discuss connections with Distributed
Systems, Topology, Probability, Term Rewriting, and Topological Sort.
Provenance Analysis for First-order Model Checking
Is a given finite structure a model of a given first-order sentence? The provenance analysis of this question determines how its answer depends on the atomic facts that determine the structure. Provenance questions like this one have emerged in databases, scientific workflows, networks, formal verification, and other areas. In joint work with Erich Grädel (RWTH Aachen University) we extend the semiring provenance framework, developed in databases, to the first-order model checking problem. This provides a non-standard semantics for first-order logic that refines logical truth to values in commutative semirings: a semiring of provenance polynomials, the Viterbi semiring of confidence scores, access control semirings, etc. The semantics can be used to synthesize models based on criteria like maximum confidence or public access. Our uniform treatment of logical negation can be used to explain missing answers for queries, and failures of integrity constraints, as well to compute corresponding repairs that fix these issues. Other collaborators: Abdu Alawini, Jane Xu, and Waley Zhang (UPenn).
I want to discuss three prototypes that we have been developing recently with different collaborators. They are first steps in our large program of using NLP tools to better understand and better explain the mathematical literature. We have contended for a while (see "Introducing the MathFoldr Project") that simple availability of mathematics is not enough: true access is more than an open door. We need clear, legible street signs, elevators, and gently sloping on-ramps, which we hope to provide via NLP tools. The prototypes we discuss are Parmesan, MathGloss, and MathAnnotator. They are just the beginning.
At different levels of description, dynamical systems can appear to take on different forms. In particular, many systems exhibit the following discrepancy. At high-levels of description the changes appear to occur discretely, moving from one symbolic concept to the next. However, at lower levels of description the changes appear to occur continuously, with the state smoothly modulating over time. We see this phenomena in all sorts of systems from brains to computers. In this talk, we propose that attractors define a consistent, robust, and emergent bridge between a low-level, continuous system and the high-level, discrete computation that it implements.
We review the history of the area and the connections with logic and outline the proof that identities valid in all Heyting Algebras can be decided in finite distributive lattices.
Classical Mechanics, Poisson Geometry, Factorization Algebras, and Operads
Eugene Rabinovich Oct 9, 2023
In this expository talk, we explain how Poisson geometry naturally arises in the study of some simple ODEs (namely those that arise in classical mechanics). We describe how to encode and generalize the notion of Poisson geometry in the language of factorization algebras (in the process, giving a definition of factorization algebras). Finally, we sketch some ways to use the theory of operads to study the homotopy theory of factorization algebras.
Cartesian double theories: A double-categorical framework for categorical doctrines
The categorified theories known as "doctrines" specify a category equipped with extra structure, analogous to how ordinary theories specify a set with extra structure. We introduce a new framework for doctrines based on double category theory. A cartesian double theory is defined to be a small double category with finite products and a model of a cartesian double theory to be a finite product-preserving lax functor out of it. Many familiar categorical structures are models of cartesian double theories, including categories, presheaves, monoidal categories, braided and symmetric monoidal categories, 2-groups, multicategories, and cartesian and cocartesian categories. We show that every cartesian double theory has a unital virtual double category of models, with lax maps between models given by cartesian lax natural transformations, bimodules between models given by cartesian modules, and multicells given by multimodulations. In many cases, the virtual double category of models is representable, hence is a double category. Moreover, when restricted to pseudo maps, every cartesian double theory has a virtual equipment of models, hence an equipment of models in the representable case. Compared with 2-monads, double theories have the advantage of being straightforwardly presentable by generators and relations, as we illustrate through a large number of examples.
In the mid 1960s Auslander introduced a notion of the defect of a finitely presented functor on a module category. In 2021 Martsinkovsky generalized it to arbitrary additive functors. In this talk I will show how to define a defect of any enriched functor with a codomain a cosmos. Under mild assumptions, the covariant (contravariant) defect functor turns out to be a left covariant (right contravariant) adjoint to the covariant (contravariant) Yoneda embedding. Both defects can be defined for any profunctor enriched in a cosmos V. They happen to be adjoints to the embeddings of V-Cat in V-Prof. Moreover, the Isbell duals of a profunctor are completely determined by the profunctor's covariant and contravariant defects. These results are based on applications of the Tensor-Hom-Cotensor adjunctions and the (co)end calculus. As a further generalization, the covariant (contravariant) defects can be defined in arbitrary proarrow equipments.
The notion of generalized algebraic theory (GAT) introduced by Cartmell in the early '80s has been applied in AlgebraicJulia, with the main motivation being simply that implementation of such a theory, with its dependent types, is more elegant and straightforward than alternatives. In the meantime, the study of the categorical semantics of dependent type theory developed extensively, also considerably inspired by Cartmell's work, in a substantially different direction centered around the semantics of Martin-Löf type theory. My aim in this talk is to explain the semantics of GATs within the context of modern thinking about the semantics of dependent type theory, namely, in terms of the categories with families (cwfs) of Dybjer.
All You Need is Relative Information
Shaowei Lin
(Topos)
Aug 28, 2023
Singular learning theory has taught me that relative information (or Kullback-Leibler divergence) is all you need. For instance, the level sets of relative information give us state density functions, whose Fourier, Laplace and Mellin transforms reveal different facets of learning algorithms and their ability to generalize. In this talk, I will outline two ongoing projects involving relative information. The first project explores the information theory of time series, for the purpose of understanding language models and reinforcement learning. Using relative information rate, we derive stochastic learning algorithms for spiking neural networks with memory. The second project explores cohomological generalizations of relative information, building on recent work by Pierre Baudot and Daniel Bennequin and by Tai-Danae Bradley. The hope is to uncover new tools for studying non-statistical spaces, by analyzing the level sets of generalized relative information and their transforms.
We first recall that dynamic monoidal categories are categories enriched in the monoidal double category Org of dynamic organizations. We then define the notion of a reverse chain rule category. Equipped with a reverse chain rule category A and a strong monoidal functor from A to Set^op, we will construct a dynamic monoidal category Dyn with the same objects as A. For a specific example, we consider any Cartesian category A equipped with a functor to Set^op. We additionally show that the deep learning as a dynamic monoidal category example from “Dynamic operads, dynamic categories” (Shapiro, Spivak) can be viewed as an example of this construction.
Entropy and Energy
Owen Lynch
(Topos)
Aug 14, 2023
Classical mechanics and quantum mechanics are both "driven by energy", in the sense that one has a free choice of Hamiltonian and then the dynamics is a function of that. Statistical mechanics, on the other hand, is "driven by entropy" in that the derivation of equilibria and the distribution of ensembles is chosen by the entropy maximization principle. In the real world, however, systems behave in both ways; they are driven both by energy and entropy. How can we model this within mathematical physics? In this talk, I will dig into this question in more detail and discuss some partial answers.
This talk is an invitation to embark on a journey to solve one of the most naive yet insanely convoluted open question in software architecture: the problem of unit systems and physical quantities. As surprising as it may seem, in 2023, there is still no software library available in any of the most common programming languages that covers the issue in its full complexity including its myriad of edge cases. In the context of a standardization effort within the C++ programming language committee on the topic of units this talk constitutes an attempt to reach out to the applied category theory community in order to approach the subject from a new angle. Throughout the presentation, a particular attention will be put on the underlying reasons behind the emerging complexity of the subject and why applied category theory may be key to disentangle this apparent complexity. This will be illustrated by concrete applications in computational physics and metrology, including particularly pathological cases that will put into question the very notion of what a unit is. Exploring conceptual boundaries through edge cases will help putting constraints on the mathematical structures that may be used to abstract the problem. Beyond the mere scope of being able to standardize a unit systems software library, the challenge raised in this talk represents a gateway to deep questions about physics, its language, its structure, and how to translate it into type theory. It also constitutes a perfect playground for applied category theory, going from a naive and well-framed question to an interdisciplinary open problem at the intersection of physics, computer science, and mathematics with broad impacts for programming languages and international standards.
Combinatorial Approaches to Multiphysics: Discrete Exterior Calculus Applied to Partial and Ordinary Differential Equations
Luke Morris
(Florida/Topos)
Jul 17, 2023
Multiphysics modeling presents complex challenges both *compositionally* and *numerically.* We recognize the combinatorial nature of systems of multiphysics equations by encoding them diagrammatically, and maintain their expressive power by providing them semantics from the discrete exterior calculus. We present here an overview of the *Decapodes* approach to scientific computing, and demonstrate how to implement maintainable and executable multiphysics models using applied category theory.
Many data science tasks—like dimensionality reduction or synchronization problems—can be phrased in terms of bundle-theoretic constructions. However, noise and error measurements can prevent said interpretations from being readily applicable in practice. In this talk, I will present recent work introducing notions of approximate and discrete vector bundles, along with examples of how they can be applied.
How to use ChatGPT as a research and communications tool
Many common structures are difficult to deal with in contemporary programming languages. For example, HTML, HTTP, and relational databases are all used daily by billions of people, and yet mainstream type systems struggle to express any of them. We observe that (second-order multiplicative exponential) linear logic has a natural interpretation in terms of graphs and graph substitutions, and that this framing conveniently expresses HTML, HTTP, and relational databases, as well as many additional useful structures. In this talk, we show how such structures can be expressed and manipulated in linear logic, and we suggest that linear logic would be a good foundation for a future programming language.
Amortized Analysis via Coinduction
Harrison Grodin
(CMU/Topos)
Jun 12, 2023
Amortized analysis is a program cost analysis technique for data structures in which the cost of operations is specified in aggregate, under the assumption of continued sequential use. Typically, amortized analyses are presented inductively, in terms of finite sequences of operations. We give an alternative coinductive formulation and prove that it is equivalent to the standard inductive definition. We describe a classic amortized data structure, the batched queue, and outline a coinductive proof of its amortized efficiency in calf, a type theory for cost analysis.
Type classes, Monads, and a Big Idea
Philip Wadler
(Edinburgh)
Jun 5, 2023
This talk will look back to two of my major contributions, type classes and monads for functional programming, and look forward to consider the need to reconcile the two strands of AI, machine learning and logic.
Many mathematical objects follow a similar pattern of "a set with operations and laws." For instance, monoids, groups, rings, vector spaces, Boolean algebras, and variations on the above. In this talk, I am going to talk about how to make sense of these sorts of objects using category theory, and how this category theory can be used to guide the implementation of computer implementation for such theories. This follows a line of research going back to 1963 with F. W. Lawvere's Ph.D thesis on algebraic theories, and in one way or another the ideas from that thesis exemplify many of the main themes of category theory that would prove successful in many ways over the next half century.
Scientific and software engineering examples of applied category theory
Abstraction is something all programmers are familiar with. We like to add abstractions in the form of little helpful scripts and functions in order to save time and avoid repeating ourselves; however, these eventually start to not fit well together, become hard to modify, and, most importantly, cannot be made sense of by others. Ad hoc abstractions are stacked like a house of cards; eventually it's easier to start over from scratch once our scientific models or workflows have to update. Category theory (CT) is math suitable for talking about abstraction, and thinking about our scientific models and workflows with CT leads to abstractions which fit well together. I argue that the scientific workflow can be fundamentally improved by involving more conceptual programming (via computational CT, e.g. AlgebraicJulia) rather than manual, ad hoc scripting. I will showcase how this paradigm leads to more robust representations of data, models, and simulators.
1. A case for a category-theoretic (hence relatively mathematically fresh) perspective on basic linguistics in the age of LLMs.
2. A flash history of DisCoCat, its drawbacks, and how I killed it.
3. Text as circuits.
4. The present practical value of our new perspective.
5. Future work: natural language ontologies for complex domain modelling.
Dagger linear logic for categorical quantum mechanics
Priyaa Srinivasan
(NIST)
Invalid Date
Dagger monoidal and dagger compact closed categories are the standard settings for Categorical Quantum Mechanics (CQM). These settings of CQM are categorical proof theories of compact dagger linear logic and are motivated by the interpretation of quantum systems in the category of finite dimensional Hilbert spaces. In this talk, I will describe a new non-compact framework called Mixed Unitary Categories (MUCs) built on linearly distributive and *-autonomous categories which are categorical proof theories of (non-compact) multiplicative linear logic. One of the motivations to develop a non-compact framework is to accommodate arbitrary dimensional systems in CQM in a structurally seamless manner. The standard categorical frameworks of finite dimensional quantum mechanics can be recovered from this general non-compact framework. This talk will be primarily based on the first part of my thesis.
Let's face it, homology is scary. Cokernels of kernels of boundary homomorphisms, oh my! Snake lemma? Long exact sequence of a pair? Utterly terrifying.
While it has become commonly practiced in both pure and applied mathematics, homological algebra is quite complicated and can be challenging to learn for those whose interests are less algebraic. However, the "logic" of homology and how it is most commonly manipulated is relatively simple and not particularly reliant on algebraic or even topological ideas.
I will introduce a notion of chain complexes of sets equipped with a theory of homology that is much simpler than the classical version using groups or modules. This homology theory includes purely set-based analogues of classical theorems like the Snake Lemma, and may have potential as a pedagogical tool for introducing homological ideas without the algebraic prerequisites. Chain complexes of sets also form a particularly well-behaved double category and a motivating example for double categorical localizations. (Joint with Maru Sarazola and Inna Zakharevich)
In their 1967 book "Calculus of Fractions and Homotopy Theory", P. Gabriel and M. Zisman introduced calculus of fractions as a tool for understanding the localization of a category at a class of weak equivalences. While powerful, the condition of calculus of fractions is quite restrictive and it is rarely satisfied in various homotopical settings, like model categories or Brown's categories of fibrant objects, where one instead has *homotopy* calculus of fractions.
This talk is based on joint work with D. Carranza and Z. Lindsey, which aims to reconcile the two. We define calculus of fractions for quasicategories and give a workable model for marked quasicategories satisfying our condition. Although we have already found several applications of this result, I would be very interested in getting feedback from the audience and exploring new applications from diverse areas.
Category Theory and Engineering Design: A Computational Support Challenge
This talk is not a math talk on Category theory. The primary focus will be on the nature of engineering design practice from an informational and socio-cognitive perspective. Based on the nature of the engineering task, the talk will lay out the categorical modeling requirements for supporting engineering design from a product and process perspective. The talk will begin with a characterization of Engineering as a collective activity, the design of a simple artifact, followed by how engineers use mathematics and modeling. We will define design as a distributed cognitive activity to motivate modeling requirements in engineering design to create a collective memory and coordination of work.
The paper is driven by the ambition of constructing a new, fully-fledged dynamic theory of ideas, but one firmly grounded in contemporary philosophical theories of ideas and such that it will amount to a categorification of the ontology of ideas. Such an attempt to apply category theory to modern ontology allows new arguments to be formulated in favour of Platonism.
Automating discovery in experimental science
Gabriel Reder
(Chalmers)
Mar 27, 2023
The life sciences are a source of huge potential gains in quality of life and deeper understanding of the fundamental mechanisms driving our daily well-being. Drug development, agricultural technology, biotechnology, and materials science are all sources of exciting new inventions and techniques that may address some of the largest issues we face today. All these fields are largely empirical – they are driven by cycles of hypotheses tested in controlled laboratory settings followed by data analysis and interpretation. But this process is slow, error-prone, and often irreproducible. In this talk, I'll discuss some aspects of the laboratory-driven discovery process from experiences in gut microbiome metabolomics. I'll also discuss recent efforts to automate the discovery process using a combination of laboratory robotics performing physical experiments coupled to automated data analysis tools. These robotic experimental platforms open the door to integrate higher-order computational reasoning techniques to further move us towards autonomous scientific discovery.
Reasoning Under Uncertainty
Adele Lopez Mar 7, 2023
What makes Bayes' theorem tick? By going to the logical level, we can get a clearer view, as well as see how to extend the notion of uncertainty in various ways.
An agent is something that has beliefs and acts on them. What if an agent's beliefs are about other agents? Then the space of agents satisfies a recursive type equation roughly like Agents = [Beliefs about agents –> Actions]. We can find a solution to this equation by combining imprecise probability with Dana Scott's domain theory. The result resembles an infinite-order version of Nigel Howard's metagame theory. The construction is rich enough to express all sorts of agents from open-source game theory, both familiar and novel.
My (nonlinear) scientific career path: a project-based approach
Anh Thai Nhan Feb 22, 2023
What is the goal of my (scientific) career? I have recently been asking this question to myself after learning about the goals and missions of Topos. For me and my family specifically, a narrow answer to the question is to provide better opportunities (in many ways) to our next generation. In a broader view, I realize that advancing in science alone is not the ultimate goal of our society; rather we should take the advantages of science and technology into account considering social impacts and other "real-life" factors to build a better place and a better future for our communities by correcting the existing, but "unhealthy" systems.
In this talk, I survey my career path through a scientific project-based lens with a focus on its applications to our communities. My nonlinear computer-driven project topics range from topology and geometry in my early career days (2001–2008) to mathematical modeling (2009–2011; and 2021–), numerical analysis and scientific computing (2011–) for singularly perturbed differential equations (for which I briefly present our several notable accomplishments in the field), together with other offshoot projects in education, approximations of elementary functions.
The microservices operad -OR- the free monad monad is a module over the cofree comonad comonad
In this talk, I'll apply a fact from the theory of polynomial functors to obtain a framework for composing microservices. I'll explain the application below, but the basic technical idea involves an interaction between the free monad m_p on a polynomial functor p, which one can think of as being about syntax, and the cofree comonad c_q, which one can think of as being about behavior. The free monad functor m: Poly -> Poly is itself a monad on Poly, and the cofree comonad functor c: Poly -> Poly is itself a comonad. The categorical fact that we will apply, which appears to be new, is that m is a c-module satisfying some useful additional coherence.
Applying the above fact will enable us to define the microservices operad. The idea is to see a polynomial p as a collection of problems and solutions: if we think of p as a bundle E -> B, then the type of problems is B, and for each b:B the type of solutions is the fiber E[b]. Polynomials form the objects of the microservices operad M; a morphism p_1,...,p_k -> q in M is a specified way to take a q-problem, hand it off as a series of problems for the p_i's to solve, and then translating their solution back as an solution to the q-problem, as well as a way to update this process. Thus (h/t David Dalrymple) we can think of the p_i's as microservices for q. I'll end by showing that M maps to a generalization of Org, meaning that we can interpret these microservices in the context of machines.
In this talk, I will present some research projects that I worked on while at Columbia University. They will be different from the usual topics presented at this seminar, in the sense that there will be no category theory. Instead my background and perspective are more of a traditional machine learning and statistics researcher, a perspective which I hope will be insightful to anyone applying category theory in this context.
Concreteness From Pedagogy to Brown Representability
I'll discuss a couple of case studies in making abstract things concrete. First, I'll describe a group theory course for high schoolers that can handle a real exposure to mathematical thinking as well as quite sophisticated computations with geometric groups by replacing parts of a standard course's pedantic abstraction with 3D graphics. Second, I'll tell the story of how Christensen and I repaired a long-standing confusion in the foundations of homotopy theory by drawing a very specific transfinite sequence of spaces and staring at it.
Category theory is the math of (function) composition. One may wonder whether there exists a dual 'cocategory' theory where decomposition rather than composition is the central operation. I will talk about some preliminary work (joint with Jade Master) on a form of cocategory theory we call contra-categories. These formalize the notion of directed obstructions and have tight relations with apartness spaces, Lawvere metric spaces and ultrafilters.
A Sketch of a Program for a Type System for Probabilistic Conformational Molecular Computing, A Computadic Introduction to Shulman's PTT, and Variations on PTT for Semicartesian and Markov Categories
Discrete homotopy theory, introduced by H. Barcelo and collaborators, is a homotopy theory of (simple) graphs. Homotopy invariants of graphs have found numerous applications, for instance, in the theory of matroids, hyperplane arrangements, topological data analysis, and time series analysis. Discrete homotopy theory is also a special instance of a homotopy theory of simplicial complexes, developed by R. Atkin, to study social and technological networks.
I will report on the joint work with C. Kapulkin (arXiv:2202.03516) on developing a new foundation for discrete homotopy theory, based on the homotopy theory of cubical sets. We use this foundation to prove the conjecture of Babson, Barcelo, de Longueville, and Laubenbacher from 2006 relating homotopy groups of a graph to the homotopy groups of a certain cubical complex associated to it, as well as a discrete homotopy theory analogue of the Hurewicz theorem.
An Algebraic Approach to Bidirectional Elaboration
Bidirectional type-checking has become a popular technique for implementing sophisticated type systems. In this talk I will discuss an approach to modelling such systems via polynomial functors, and describe applications of the theory of polynomials to the implementation of interactive proof assistants. If time permits I will also explore a more general theory of mixed indexed and fibred structure.
Grothendieck Constructions and Universal Maps
Brandon Shapiro
(Topos Institute)
Oct 31, 2022
In this mostly expository talk, I will describe a variety of different "Grothendieck constructions" for building a map out of its fibers in algebraic and combinatorial settings. In each case, the maps that are classified in this manner arise as pullbacks of a certain "universal" map. Time permitting, I will discuss new Grothendieck constructions for "prolynomial" functors and double categories.
Does recursion help? (In honor of Dana Scott's 90th birthday)
As everyone knows, Alonzo Church proposed that the effectively calculable natural number functions are those definable in the untyped lambda calculus. (He used Church numerals to represent natural numbers.) The lambda-definable functions were shown to be the same as the Gödel-Herbrand general recursive functions and the same as the functions computable by Turing machines. The fixed-point combinator Y is crucial for the proofs, as it enables functions to be defined recursively.
If we switch to the typed lambda-calculus the situation changes drastically. Helmut Schwichtenberg and Richard Statman showed that only the extended polynomials can then be defined (they used a typed version of the Church numerals).
It is natural, therefore, to ask what happens if one adds typed fixed-point combinators to the typed lambda calculus. We present an answer to this question. Our answer makes essential use of Dana Scott's domain theory to model the fixed-point combinators.
Games with Cats
Matteo Capucci
(University of Strathclyde)
Oct 10, 2022
In this programmatic talk I'm going to walk you through the new, rebooted theory of open games, founded in the recently introduced 'diegetic' formalism, itself the cherry on top of a cake which has been patiently baking for years. The diegetic formalism corrected extant conceptual issues in the setup of compositional game theory and has triggered several changes in me and my collaborators' approach to open games. After reminding you of some basic definitions and their game-theoretic motivation, I'm going to introduce the behavioural study of games through a 'cybernetic systems theory', inspired by David Jaz Myer's notion of 'system theory'. If time permits, I'll show how David and Brandon's notion of dynamic operad is closely related.
Space-time tradeoffs of lenses and optics via higher category theory
Bruno Gavranovic
(University of Strathclyde)
Oct 3, 2022
Optics and lenses are abstract categorical gadgets that model systems with bidirectional data flow. In this paper we observe that the denotational definition of optics - identifying two optics as equivalent by observing their behaviour from the outside - is not suitable for operational, software oriented approaches where optics are not merely observed, but built with their internal setups in mind. We identify operational differences between denotationally isomorphic categories of cartesian optics and lenses: their different composition rule and corresponding space-time tradeoffs, positioning them at two opposite ends of a spectrum. With these motivations we lift the existing categorical constructions and their relationships to the 2-categorical level, showing that the relevant operational concerns become visible. We define the 2-category 2-Optic(C) whose 2-cells explicitly track optics' internal configuration. We show that the 1-category Optic(C) arises by locally quotienting out the connected components of this 2-category. We show that the embedding of lenses into cartesian optics gets weakened from a functor to an oplax functor whose oplaxator now detects the different composition rule. We determine the difficulties in showing this functor forms a part of an adjunction in any of the standard 2-categories. We establish a conjecture that the well-known isomorphism between cartesian lenses and optics arises out of the lax 2-adjunction between their double-categorical counterparts. In addition to presenting new research, this paper is also meant to be an accessible introduction to the topic.
Assembly in the Algebraic K-theory of Lawvere Theories
Anna Marie Bohmann
(Vanderbilt University)
Sep 26, 2022
Lawvere's algebraic theories are an elegant and flexible way of encoding algebraic structures, ranging from group actions on sets to modules over rings and beyond. We discuss a construction of the algebraic K-theory of such theories that generalizes the algebraic K-theory of a ring and show that this construction allows us to build Loday assembly-style maps. This is joint work with Markus Szymik.
Lightning Talks
Sep 19, 2022
Towards a Categorical Treatment of Economics
Fernando Tohme
(Universidad Nacional del Sur)
Sep 15, 2022
Economics has been late in adopting the formalisms of Category Theory. But if we understand the discipline broadly as the study of interactions among intentional entities, categorical formalisms can contribute to clarify relevant issues arising in goal-oriented exchanges. In this talk we use CT to study the structure of problems of decision-making by a single agent, detecting settings in which non-locality and contextuality lead to obstructions to the compatibility of different models of agenthood. We then consider an operadic treatment of local interactive problems (known as games) showing the restrictive conditions that are required for the preservation of equilibria. We end with a speculation about how to develop a general dynamic model of interactions as a category enriched in the bicategory Org.
Dialectica constructions and lenses
Jonathan Weinberger
(Johns Hopkins University)
Sep 12, 2022
In the 1940s, Gödel devised the Dialectica interpretation, a so-called proof interpretation used for relative consistency proofs in constructive logic.
In her doctoral dissertation (late 1980s to early 1990s), de Paiva introduced the notion of so-called Dialectica categories supporting various versions of the Dialectica construction. This has since been generalized to fibrations in later work by Hyland and Hofstra, leading e.g. to Dialectica models of type theory (cf. the works by von Glehn and Moss).
In the talk, I will discuss work in progress concerning the connections of the (categorical or fibrational) Dialectica construction with so-called lenses.
The concept of a lens is known from database theory and it formalizes a kind of transition system that is able to receive inputs and internally convert them to a different form. Lenses can be seen as an instance of the general concept of a so-called optic. On the other hand, using (fibered) categorical language, lenses can also be seen as an instance of de Paiva's Dialectica construction.
The relevant notions concerning Dialectica constructions and lenses will be introduced in the talk. This is joint work in progress with Matteo Capucci, Bruno Gavranović, Abdullah Malik, Francisco Rios under the direction of Valeria de Paiva as a (sub-)project of the AMS Math Research Community on Applied Category Theory 2022-2023.
A Categorical Formulation of Predictive Processing
Sean Tull
(Cambridge Quantum)
Sep 9, 2022
I will speak about ongoing work with Johannes Kleiner and Toby St Clere Smithe aiming to formalise the Predictive Processing (PP) approach to cognition and AI, and more specifically the framework of Active Inference developed by Karl Friston and collaborators. To do so we use the tools of categorical probability theory, i.e. Markov categories, and their associated string diagrams. I'll discuss the diagrammatic account of generative models, Bayesian inference in perception and planning, and its approximation via Free Energy minimization. Ultimately we aim to arrive at a conceptually clear presentation of PP which can then be generalised and related to other approaches to categorical cybernetics.
Double-categorical databases and knowledge representation
Category theory yields efficient mathematical formalisms for relational databases and, relatedly, for knowledge representation systems. The most direct approach is based on the category of sets and functions and is therefore functional in nature. In a more overtly relational approach, it has also been proposed to use the bicategory of sets, relations, and implications. The functional and relational views have their pros and cons, as we will explain. We will then argue that working with the double category of sets, functions, relations, and implications, and its abstraction in cartesian equipments and "double categories of relations," is a unification that captures many of the benefits of both approaches.
This talk is based on joint work with Michael Lambert.
A type theory for (∞,1)-categories.
Jonathan Weinberger (Johns Hopkins University) Sep 6, 2022
Port-Hamiltonian systems are a geometric formalism for open mechanical systems used widely within engineering. In my thesis, I showed how to formalize the composition of port-Hamiltonian systems using category theory. In this talk, I will give an overview of the technical framework that allowed me to do this, and then an overview of how this framework applies to port-Hamiltonian systems.
Applications of category theory to automated planning and program compilation in robotics
Robot manipulators are employed in millions of factories around the world using computer programs that are specifically tailored to the robotic platform, work cell, material, and task. To add to these degrees of freedom, each of these programs are written by humans that bring their own variations to the programmed solution. This makes every program a point solution that does not scale beyond the robots in that specific work cell configuration, and at best, beyond robots from the same vendor. This phenomena suggests that, in practice, robotic architectures are held together by a linchpin which is a consensus-driven syntax or, in other words, agreed upon data formats. This informality limits our ability to verify behavior, synthesize implementations, and evaluate the impact of change at scale. Therefore, denotational semantics is a necessary ingredient if we wish to evaluate for such properties in our robotic systems. This talk will discuss proposed formal semantic frameworks based on category theory that enable the synthesis of automated task planning and programs in robotics. In addition, this talk will cover a categorical model for knowledge representation and how it may be used in contextual reasoning.
The Digital Abacus
Paul Dancstep Aug 18, 2022
Paul Dancstep will share concepts and prototypes from a math education project called The Digital Abacus. The project goals are to develop alternative formal systems for high school algebra, and to explore whether video games can be an effective context for introducing learners to these systems.
Both the category of polynomial functors and the dependent Dialectica category are extremely rich, and for the same reason: each emerges as the free distributive category on a simpler category, namely on the free object and the free arrow, respectively: Poly= FD(∙), DDial=FD(∙→∙). But in fact, the free distributive category construction has a kind of "square root": a simpler construction, which I'll call the agenda category construction, such that FD(C)=Agenda(Agenda(C)). An object in Agenda(C) is a list of items, each of which has an associated C-object (called its value), and a morphism (A,c)→(A',c') in Agenda(C) is a method: given any item a:A we specify an item a':A' by which to accomplish it, as well as a map c'(a')→c(a) returning the value of that item.
The agenda category enjoys excellent formal properties. Agenda(C) always has extensive coproducts; Agenda(C) has a distributive monoidal operation for every monoidal operation on C; Agenda(C) is complete/cocomplete if C is cocomplete/complete; Agenda(C) has monoidal closures/coclosures if C has monoidal coclosures/closures, etc. We can also define a composition operation on FD(C) for any monoidal category C, and we learned from Nelson Niu that a comonoid in FD(C) is precisely a category enriched in Agenda(C).
From this laundry list of formal properties and the fact that the free object category ∙ has exactly one of every categorical structure, we recover many known properties of Poly, DDial, etc. Focusing on Poly, we recover the usual operations +, ×, ⊗, ⊲, as well as many if not all the known facts about ×, ⊗ being monoidal closed, ⊗ and ⊲ being coclosed, etc, and the fact that a comonoid in Poly is a (Set-enriched) category. Finally, we will show that we can almost build Poly inside of Poly—making Poly a "self-reflective theory"—using just the above operations (namely, composition and coclosure): the only thing missing is a better understanding of the generally-assumed-trivial opposite category construction, which is more interesting in this setting because comonoids in FD(C) are oriented and hence are not trivial to transpose. This last piece is work in progress and help is welcome!
Axioms for the category of Hilbert spaces
Andre Kornell
(Tulane University)
Jul 5, 2022
The category of Hilbert spaces and bounded linear operators is the canonical setting of categorical quantum information theory. This talk will focus on a recent axiomatization of this category, which draws on research on dagger categories and on orthomodular lattices. The novelty of this axiomatization is that it is entirely category-theoretic. Much of the discussion will be grounded in comparisons to the category of sets and partial injections.
The topology, geometry, and combinatorics of ReLU neural network functions
Elisenda Grigsby
(Boston College)
Jun 29, 2022
Feedforward neural networks are a class of parameterized functions that have proven remarkably successful at making predictions about unseen data from finite labeled data sets. They do so even in regimes where classical notions of complexity suggest that they ought to be overfitting the training data. I will describe recent and ongoing work (joint with various subsets of K. Lindsey, M. Masden, R. Meyerhoff, D. Rolnick, C. Wu) aimed at studying natural notions of complexity that we hope will shed light on why overparameterized ReLU neural networks perform so well. Along the way, I will introduce you to some of the beautiful geometry and combinatorics underlying this subject.
How can we create intelligent systems that retain and expand into that which we find valuable in the universe? During this talk I will present my own thoughts based on ontology mapping, and I will communicate why I believe that mathematicians who think about systemic interactions are in an especially good place to answer this important question. I will start with a framework in which read-eval-print loops (repls) form a basis for reasoning about agents and computation in general. Then I will build ontology maps as an alignment framework on top of repls, and discuss its implications. Lastly I will invite discussion on what we might want out of the future, and talk about my thoughts on the central role of communication and its relation to both repls and ontology maps.
The free monad, cofree comonad, and topological space associated to a polynomial
To each polynomial p, one can associate a free monad m_p, the "operad of well-founded p-trees", and a cofree comonad c_p, the "category of (possibly infinite) p-trees". It turns out that the object-set c_p(1) of the latter category forms the point-set of a topological space, which is called a Stone space when p is finite, and that the morphism-set m_p(1) of the operad forms a base for this topology! I imagine the topological space (c_p(1), m_p(1)) could provide an alternative point of view for studying p-dynamical systems, or more precisely p-coalgebras. I'll explain what I know about all this, starting from very little background beyond standard category theory.
The logical notion of equality, when considered from the point of view of Lawvere's hyperdoctrines, is determined by a Kock-Zoeberlein comonad (aka a lax 2-comonad) on the 2-category of primary doctrines. The construction of the comonad is very similar to well-known constructions which involve a kind of quotient completion, e.g. the exact completion of a category with finite limits, or the separated presheaves on a complete Heyting algebra. In fact, the comonad offers a precise explanation for this similarity. If time permits, we shall also suggest how to extend the comonad to the general case of fibrations with finite products.
Computability theory is the sub-area of mathematical logic that studies ways to measure the complexity of objects, constructions, theorems, and mathematical proofs related to countably infinite objects. On one hand, the natural objects seem to be linearly ordered from simpler to more complex, while, on the other hand the general objects are ordered in a chaotic way. This dichotomy between natural objects and objects in general is hard to study mathematically, as we don't have a formal definition of "natural object." The objective of this talk is to introduce Martin's conjecture (open for more than 40 years) and see how it explains this dichotomy.
Combinatorial Representation of Scientific Knowledge
Computational models are core to modern scientific practice, yet there are improvements that can be made to traditional means of representing, comparing, exploring, and simulating with models. We'll take a tour of recent developments within AlgebraicJulia relevant to modeling in epidemiology, and we'll focus on the ways in which combinatorial data structures (e.g. slices, cospans, and diagrams in C-Set) lead to models which are more transparent, predictable, general in scope, transferable, and hierarchical.
Enrichment of General Categorical Structures
Brandon Shapiro
(Topos Institute)
Apr 18, 2022
Classically, the notion of a category can be "enriched" in some monoidal category V to get a structure similar to a category but with the sets Hom(x,y) of arrows from x to y replaced by objects called Hom(x,y) in $V$ for each pair of objects, such as categories where the hom-sets naturally form abelian groups or topological spaces or dynamical systems. One generalization of this notion due to Leinster relaxes the requirement that V is a monoidal category, and in my thesis I generalize in a different direction by defining V-enrichment for a broad class of structures other than categories, including n-categories, double categories, and monoidal categories. In this talk I'll discuss these notions of enrichment as well as my recent work at Topos on a theory of enrichment that subsumes both generalizations and facilitates an elegant definition of "adaptives" to describe systems of nested dynamics.
Retina-inspired Representations of Natural Signals
Chris Hillar
(Awecom, Inc.)
Apr 11, 2022
Theoretical constructs from biophysics have profoundly impacted signal processing and engineering from McCulloch-Pitt's theory of mind seeding modern computer design (von Neumann) to the hierarchical neural network approach underlying recent breakthroughs in deep learning. This history will be discussed as the backdrop for a new biologically-inspired paradigm for digital sensory encoding, originally developed at the Redwood Center for Theoretical Neuroscience (founded by Jeff Hawkins) and now fueling initial applications in signal processing. Consequences for source/channel coding, learning in AI, and experimental neuroscience will also be explored.
Clifford algebra and rigid motions
Alok Singh Apr 4, 2022
Clifford algebra (also known as geometric algebra) is an extension of linear algebra that gives a theory of directed numbers. The basic operation is geometric product, which combines the inner and outer product. All rigid motions (rotation, translation, reflection) are conjugations by geometric products. Formulas in this framework are dimension-independent. This allows for a synthetic approach to geometry, where complicated objects are formed from simpler ones by union/intersection. Complex numbers and quaternions correspond to rotations, and the weird quaternion multiplication table makes more sense in this perspective. We will see that all the "angular" quantities in physics (angular momentum, the magnetic field, torque) are not vectors but planes (bivectors).
AlgebraicDynamics is one year old and we'll celebrate with a tour of what it can do and where it's going. We'll see examples of composing dynamical systems as resource sharers and as machines. We'll also discuss on-going work on the implementation of semi-instantaneous machines and DILS (deeply interacting learning systems). Get ready to party!
Adaptives: evolving systems of organized contributions
We describe ongoing work at Topos on the theory of "adaptives," which are systems that arrange contributions to a project and update these arrangements based on performance, in a way that respects the internal organization of the project. A project of this sort could be a deep learning program, a computer that updates its internal wiring, or even the Topos Institute itself.
Categories by proxy and the limits of Para
Toby St Clere Smithe
(Topos Institute)
Mar 7, 2022
The notion of parameterization is of great importance in categorical cybernetics, providing space for morphisms to be learnt, or for their choice to be 'externally' determined. At the same time, the concept of 'randomness pushback' tells us that the randomness of a stochastic channel can also (in nice circumstances) be so externalized, leaving instead a random choice of deterministic map. The usual perspective on parameterization is an 'internal' one, treating the parameter as a modification of a morphism's (co)domain. In general, however, this perspective is not wide enough to retain all the structure of the category at hand: an 'external' perspective seems mathematically, as well as philosophically, necessary. In earlier work, we attempted to provide such an external perspective using an enriched-categorical notion of parameterization, but this is similarly insufficient.
Here, we describe an alternative perspective, considering an internal category parameterized by its 'external' universe. We build an indexed double category over the double category of spans in the universe, with each base object representing a choice of 'parameterizing context'. When the internal category has limits or a subobject classifier, so does its parameterization; with appropriate quotienting, so does the corresponding Grothendieck construction. By decorating the spans with (sub)distributions, the same facts hold true even in the stochastic case, giving semantics for notions of 'stochastic type' and 'stochastic term'. In this setting, we can reformulate Bayesian lenses as "Bayesian dependent optics", treating generative models as such stochastic terms.
Dependent Optics
Eigil Rischel
(University of Strathclyde)
Feb 28, 2022
The applied category theory literature contains a large zoo of "lens-like" categories - simple lenses, dependent lenses, linear lenses, simple optics, mixed optics, polynomial functors, are some of the names people throw around. These have found applications in a number of different fields. For applications in game theory, we want a category of "lens-like" morphisms with two particular features: Categories of "dependent lenses", unlike categories of optics or simple lenses, can often be constructed with all finite coproducts. This allows us to model "external choice", where the game being played depends on decisions made previously by another player. On the other hand, we also want to consider games involving random outcomes, and therefore to work with lenses or optics in the category of Markov kernels. However, formulations of dependent optics require categories with finite limits, while the category of Markov kernels does not even have products. I'll present a framework for "dependent optics" which allows these two features to be combined in one category.
Principles and pitfalls of designing software for applied category theory
AlgebraicJulia is a family of software packages for applied category theory, written in the Julia programming language. It includes the general framework Catlab and a growing collection of packages for specific domains, such as dynamical systems and epidemiology modeling. In this informal talk, I describe some of the principles and pitfalls discovered by the AlgebraicJulia team over the course of several years of hard work toward making viable technologies out of the mathematics of applied category theory.
Modeling decentralized markets using (mostly free) categories
Standard models of financial markets assume that transactions are mediated by a single unit of account. However, in some real-world markets, there is no distinguished unit of account, transactions consist of an exchange of two assets, and arbitrage is often possible. We attempt to define a categorical formalism for these "decentralized" markets, and a path integral description of the stochastic dynamics of exchange-values in such markets.
Integrating machine learning into scientific spatial and temporal modeling
Aditi Krishnapriyan
(UC Berkeley)
Jan 31, 2022
Natural Language Inference: for humans and machines
One hears much about the incredible results of recent neural nets methods in Natural Language Processing (NLP). In particular much has been made of the results on the Natural Language Inference (NLI) task using the huge new corpora SNLI, MultiNLI, SciTail, etc, constructed since 2015. Wanting to join in the fun, we decided to check the results on the corpus SICK (Sentences Involving Compositional Knowledge), which is two orders of magnitude smaller than SLNI and hence presumably easier to deal with.
We discovered that there were many results that did not agree with our intuitions. As a result, we have written several papers on the subject of NLI on SICK. I want to show you a potted summary of this work, to explain why we think this work is not near completion, yet, how we're planning to tackle it and why we think this is very important.
Familial and Polynomial Functors for Higher Category Theories
Brandon Shapiro
(Cornell)
Dec 13, 2021
Familial functors between presheaf categories (sometimes called parametric right adjoints) arise in both the theories of databases and algebraic higher categories. Algebras for any familial monad can be treated as a type of higher category, where the cell shapes may differ from vertices and arrows, and many classical features of category theory generalize to this "shape independent" setting. Familial monads are equivalent to certain "schema" for types of higher categories, given in terms of the underlying cell shapes and their composition operations. I will describe how the proof of this equivalence uses the relationship between familial and polynomial functors, and discuss connections between higher categories and databases.
Partially observing graphs - when can we infer underlying community structure?
Fiona Skerman
(Uppsala)
Dec 6, 2021
Suppose edges in an underlying graph G appear independently with some probability in our observed graph G' - or alternately that we can query uniformly random edges. We describe how high a sampling probability we need to infer the modularity of the underlying graph.
Modularity is a function on graphs which is ubiquitous in algorithms for community detection. For a given graph G, each partition of the vertices has a modularity score, with higher values indicating that the partition better captures community structure in G. The (max) modularity q*(G) of the graph G is defined to be the maximum over all vertex partitions of the modularity score, and satisfies 0 ≤ q*(G) ≤ 1.
It was noted when analysing ecological networks that under-sampled networks tended to over-estimate modularity - we indicate how the asymmetry of our results gives some theoretical backing for this phenomenon - but questions remain.
In the seminar I will spend time on intuition for the behaviour of modularity, how it can be approximated, links to other graph parameters and to present some open problems.
Joint work with Colin McDiarmid.
Path Space Monomials: Signatures and Applications to Sequential Data
Darrick Lee
(EPFL)
Aug 17, 2021
Path signatures are characterizations of paths initially developed to study the topology of loop spaces, and has recently been used to form the foundations of rough paths in stochastic analysis. In this talk, we introduce the path signature as a set of monomials for path spaces, which have several properties in common with the set of monomials for Euclidean space. These path space monomials can be used as a complete feature set for sequential data, and we discuss recent work on extensions to geometric and topological data.
Invitation to the next dimension: 2D doesn't mean double the work, only twice as much
tslil clingman
(Johns Hopkins University)
Aug 10, 2021
This talk is intended to serve as an invitation to the world of 2-(category theory) – note the associativity. While much work has been done on understanding the nature of 2-categories and their morphisms as objects of study, there still remains low-hanging fruit in the realm of
2-dimensional category theory. Throughout the talk we will emphasise the many results that were, at the time, undocumented or unknown in 2-category theory and which "just worked", as well as the new and interesting surprises along the way. Our overall story is that of a recent result concerning "bi-representations".
Algebraic Property Graphs
Joshua Meyers
(Indiana University)
Aug 3, 2021
Algebraic Property Graphs (APGs) are a new graph data model which allow for the seamless integration of edges between more than two vertices, labels on vertices and edges, edges between edges, edges from an edge to a vertex, and much more. Notwithstanding the usual tradeoff in data models between flexibility and the potential for a well-defined formal semantics, APGs have both these qualities. In my work for Conexus AI, I have been devising formal descriptions on APGs. In this talk, I will present some of these descriptions, along with examples of APG schemas, APGs, and transformations, and I will also showcase some of the challenges involved in adding constraints and performing left and right Kan extensions (sigma and pi).
One goal of applied category theory is to understand open systems: that is, systems that can interact with the external world. We compare two approaches to describing open systems as morphisms: structured and decorated cospans. Each approach provides a symmetric monoidal double category. Structured cospans are easier, decorated cospans are more general, but under certain conditions the two approaches are equivalent. We take this opportunity to explain some tricky issues that have only recently been resolved.
The Universal Library: A novel approach to teaching category theory
I will offer a STEM educator's take on the unique challenges of learning category theory and present an extended thought experiment - roughly derived from the Jorge Luis Borges story *The Library of Babel* - as a strategy for sharing this subject with a general audience.
In this talk, I will present a reflection of my journey thus far as an engineer using category theory to aid in robot programming and software reverse engineering. I will also provide thoughts on how to bolster applied category theory outreach to the software engineering community.
The Algebraic Julia Ecosystem, a categorical approach to technical computing
James Fairbanks
(University of Florida)
Jun 29, 2021
I'll give an overview of the AlgebraicJulia ecosystem, providing the context for the existing tools and a roadmap of future developments.