Values and Inclusivity in the ACT Community

In the tenth and final talk of this spring’s ACT@UCR seminar, Nina Otter led a discussion about diversity in the applied category theory community, with these speakers:

• Nina Otter: introduction, and some potential initiatives

• Jade Master: Experience in setting up an online research community for minorities in ACT

• Brendan Fong: Statement of values for ACT community

• Emily Riehl: Experience at MATRIX institute

• Christian Williams: Quick overview of ACT server

This is a change from her originally scheduled talk, due to the killing of George Floyd and ensuing events.

The discussion took place at the originally scheduled time on Wednesday June 3rd. Afterwards we had discussions at the Theory Community Server, here:

https://categorytheory.zulipchat.com/#narrow/stream/229966-ACT.40UCR-seminar/topic/June.203rd.3A.20Nina.20Otter

You can join the conversation there if you sign in.

You can see her slides here, or download a video here, or watch the video here:

• Nina Otter, Values and inclusivity in the applied category theory community.

Abstract. Saddened by the current events, we are taking this opportunity to pause and reflect on what we can do to change the status quo and try to bring about real and long-lasting change. Thus, we are holding a discussion aimed at finding concrete solutions to make the Applied Category Theory community more inclusive, and also to reflect about the values that our community would like to stand for and endorse, in particular, in terms of which sources of funding go against our values. While this discussion is specific to the applied category theory community, we believe that many of the topics will be of interest also to people in other fields, and thus we welcome anybody with an interest to attend. The discussion will consist of two parts: we will have first several people give short talks to discuss common issues that we need to address, as well as present specific plans for initiatives that we could take. We believe that the current pandemic, and the fact that all activities are now taking place remotely, gives us the opportunity to involve people who would otherwise find it difficult to travel, because of disabilities, financial reasons or care-taking responsibilities. Thus, now we have the opportunity to come up with new types of mentoring, collaborations, and many other initiatives that might have been difficult to envision until just a couple of months ago. The second part of the discussion will take place on the category theory community server, and its purpose is to allow for a broader participation in the discussion, and ideally during this part we will be able to flesh out in detail the specific initiatives that have been proposed in the talks.

The Legendre Transform: a Category Theoretic Perspective

In the ninth talk of the ACT@UCR seminar, Simon Willerton told us about a categorical approach to the Legendre transform, and its connection to tropical algebra.

He gave his talk on Wednesday May 27th. Afterwards we discussed it on the Category Theory Community Server, here:

https://categorytheory.zulipchat.com/#narrow/stream/229966-ACT.40UCR-seminar/topic/May.2027th.3A.20Simon.20Willerton

You can view or join the conversation there if you sign in.

You can see his slides here, or download a video here, or watch the video here:

• Simon Willerton, The Legendre–Fenchel transform from a category theoretic perspective.

Abstract. The Legendre-Fenchel transform is a classical piece of mathematics with many applications. In this talk I’ll show how it arises in the context of category theory using categories enriched over the extended real numbers It turns out that it arises out of nothing more than the pairing between a vector space and its dual in the same way that the many classical dualities (e.g. in Galois theory or algebraic geometry) arise from a relation between sets.

I won’t assume knowledge of the Legendre-Fenchel transform.

The talk is based on this paper:

• Simon Willerton, The Legendre-Fenchel transform from a category theoretic perspective.

Also see his blog article:

• Simon Willerton, The nucleus of a profunctor: some categorified linear algebra, The n-Category Café.

A Complete Axiomatisation of Partial Differentiation

In the eighth talk of the ACT@UCR seminar, Gordon Plotkin told us about partial differentiation, viewed as a logical theory.

He gave his talk on Wednesday May 20th. Afterwards we discussed it on the Category Theory Community Server, here:

https://categorytheory.zulipchat.com/#narrow/stream/229966-ACT.40UCR-seminar/topic/May.2020th.3A.20Gordon.20Plotkin

You can view or join the conversation there if you sign in.

You can see his slides here, or download a video of his talk here, or watch his video here:

• Gordon Plotkin, A complete axiomatisation of partial differentiation.

Abstract. We formalise the well-known rules of partial differentiation in a version of equational logic with function variables and binding constructs. We prove the resulting theory is complete with respect to polynomial interpretations. The proof makes use of Severi’s theorem that all multivariate Hermite problems are solvable. We also hope to present a number of related results, such as decidability and Hilbert–Post completeness.

Logic Extremists

 

I apologize for this entry, which doesn’t really belong here: it’s a piece of fan fiction, or actually fictional history, with only a slight bit of relevance to the problems this blog is about.

Like many scientists I have a grudging admiration for the Star Trek franchise: grudging because the science is so often silly, and could often have been improved easily without spoiling the stories; admiration because it has created a hopeful vision of the future, some fun stories, and some enduringly interesting characters.

In Discovery we heard about the Logic Extremists, a dissident faction of Vulcans who wanted to leave the Federation. But we didn’t learn much about their core beliefs! They seemed rather similar to the Vulcan Isolationists, who came about a hundred years later. There seemed to be an interesting untold story lurking behind the name.

So, I went to T’Karath and spent a couple of weeks poring through the historical documents on this movement. Here’s a quick sketch of what I found.

In the first half of the 22nd century, the central government had become corrupt, with Romulan operatives infiltrating the Vulcan High Command. Some Vulcans, the Syrannites, attempted to reinstate and develop the original teachings of the Vulcan philosopher Surak. But around 2140, another small group decided that Surak had not developed logic with sufficient thoroughness.

This group of thinkers argued that all deductive reasoning should be formalized, all inductive reasoning should be Bayesian with explicit probabilities on hypotheses, and all decision-making should maximize utility.

This group, who called themselves the Pure Logic movement, moved to Xir’tan and set up a commune there. They began a program of formal concept analysis so that all words would have precise definitions. Before each meal they bowed, seemingly in prayer, but actually to optimize their activities to come. Children were schooled in an even more disciplined way than usual: less high-tech than the skill domes of the 2200s, but with an intense focus on logic, semiotics, probability, and statistics.

Conflicts erupted in 2200 between what we would call Jaynesian-Bayesians and hardcore subjective Bayesians. The former advocated entropy-maximizing priors. The latter argued that no prior counts as “right” without further assumptions, so one is free to start with any prior.

As the Pure Logic movement became established, they spread and set up communes the main continent, especially in Gol, Xial and Raal. They started influencing the political establishment, first locally and then at the federal level.

As this happened, factions with radical positions gradually gained influence. Especially important were the subjective Bayesians who argued that ethics could not be logically derived, so that instead of maximizing utility, a rational agent was free to maximize any chosen quantity. Their motto was remarkably similar to a saying credited to Hume:

From an “is” one cannot derive an “ought”.

Going further, the most extreme subjective Bayesians adopted spreading the Pure Logic movement as their only goal. All decisions were to be evaluated based on how much they furthered the spread of logical thinking. They took a vow to this effect, and pressed this vow on other citizens as a prerequisite for holding office of any sort. Their opponents dubbed them “Logic Extremists”, and the term stuck.

In 2226, in a hard-fought political struggle, these extremists triumphed and completely pushed the Jaynesian-Bayesians and moderate subjective Bayesians out of power. Two years later V’Arak took control: a charismatic leader who asserted with 100% prior probability that the Federation was trying to subvert Vulcan culture and stop the spread of the Pure Logic movement.

Any attempt to reason with V’arak and his supporters, or compromise with them, was interpreted as further evidence of an increasingly elaborate Federation conspiracy. Most Vulcans repudiated this stance, and as the Logic Extremists’ public support shrank they turned to terrorism.

The violence came to a head around 2256, when V’latak (shown below) attempted to assassinate Sarek before the peace talks on Cancri IV, saying:

My sacrifice will be a rallying cry to those who value
logic above all. Vulcans will soon recognize and withdraw from
the failed experiment known as the Federation.

At this point support for the Logic Extremists rapidly dropped and the movement began to dissipate, though Patar still managed to infiltrate Section 31.

However, the most interesting aspect of the Logic Extremists are their early theoretical writings — especially those of Avarak, and Patar’s father Tesov. They were an extremely bold attempt to plan a society based purely on logic. I hope they’re translated soon.

Formal Concepts vs Eigenvectors of Density Operators

In the seventh talk of the ACT@UCR seminar, Tai-Danae Bradley told us about applications of categorical quantum mechanics to formal concept analysis.

She gave her talk on Wednesday May 13th. Afterwards we discussed her talk at the Category Theory Community Server. You can see those discussions here if you become a member:

https://categorytheory.zulipchat.com/#narrow/stream/229966-ACT.40UCR-seminar/topic/May.2013th.3A.20Tai-Danae.20Bradley

You can see her slides here, or download a video here, or watch the video here:

• Tai-Danae Bradley: Formal concepts vs. eigenvectors of density operators.

Abstract. In this talk, I’ll show how any probability distribution on a product of finite sets gives rise to a pair of linear maps called density operators, whose eigenvectors capture “concepts” inherent in the original probability distribution. In some cases, the eigenvectors coincide with a simple construction from lattice theory known as a formal concept. In general, the operators recover marginal probabilities on their diagonals, and the information stored in their eigenvectors is akin to conditional probability. This is useful in an applied setting, where the eigenvectors and eigenvalues can be glued together to reconstruct joint probabilities. This naturally leads to a tensor network model of the original distribution. I’ll explain these ideas from the ground up, starting with an introduction to formal concepts. Time permitting, I’ll also share how the same ideas lead to a simple framework for modeling hierarchy in natural language. As an aside, it’s known that formal concepts arise as an enriched version of a generalization of the Isbell completion of a category. Oftentimes, the construction is motivated by drawing an analogy with elementary linear algebra. I like to think of this talk as an application of the linear algebraic side of that analogy.

Her talk is based on her thesis:

• Tai-Danae Bradley, At the Interface of Algebra and Statistics.

Separation Logic Through a New Lens

In the sixth talk of the ACT@UCR seminar, Sarah Rovner-Frydman told us about a new approach to separation logic, a way to reason about programs.

She gave her talk on May 6th, 2020. Afterwards we discussed it on the Category Theory Community Server, here:

https://categorytheory.zulipchat.com/#narrow/stream/229966-ACT.40UCR-seminar/topic/May.204th.3A.20Sarah.20Rovner-Frydman/near/196269053

You can view or join the conversation there if you sign in.

You can see her slides here, or download a video of her talk here, or watch the video here:

• Sarah Rovner-Frydman: Separation logic through a new lens.

Abstract. Separation logic aims to reason compositionally about the behavior of programs that manipulate shared resources. When working with separation logic, it is often necessary to manipulate information about program state in patterns of deconstruction and reconstruction. This achieves a kind of “focusing” effect which is somewhat reminiscent of using optics in a functional programming language. We make this analogy precise by showing that several interrelated techniques in the literature for managing these patterns of manipulation can be derived as instances of the general definition of profunctor optics. In doing so, we specialize the machinery of profunctor optics from categories to posets and to sets. This simplification makes most of this machinery look more familiar, and it reveals that much of it was already hiding in separation logic in plain sight.

A Localic Approach to Dependency, Conflict, and Concurrency

In the fifth talk of the ACT@UCR seminar, Gershom Bazerman told how to use locales to study the semantics of dependency, conflict, and concurrency.

Afterwards we discussed his talk at the Category Theory Community Server, here:

https://categorytheory.zulipchat.com/#narrow/stream/229966-ACT.40UCR-seminar/topic/April.2029th.3A.20Gershom.20Bazerman

You can view or join the conversation there if you sign in.

You can see his slides here, or download a video here, or watch the video here:

• Gershom Bazerman, A localic approach to the semantics of dependency, conflict, and concurrency.

Abstract. Petri nets have been of interest to applied category theory for some time. Back in the 1980s, one approach to their semantics was given by algebraic gadgets called “event structures.” We use classical techniques from order theory to study event structures without conflict restrictions (which we term “dependency structures with choice”) by their associated “traces”, which let us establish a one-to-one correspondence between DSCs and a certain class of locales. These locales have an internal logic of reachability, which can be equipped with “versioning” modalities that let us abstract away certain unnecessary detail from an underlying DSC. With this in hand we can give a general notion of what it means to “solve a dependency problem” and combinatorial results bounding the complexity of this. Time permitting, I will sketch work-in-progress which hopes to equip these locales with a notion of conflict, letting us capture the full semantics of general event structures in the form of homological data, thus providing one avenue to the topological semantics of concurrent systems. This is joint work with Raymond Puzio.

The Monoidal Grothendieck Construction

My student Joe Moeller gave a talk at the MIT Categories Seminar today! People discussed his talk at the Category Theory Community Server, and if you join that you can see the discussion here:

https://categorytheory.zulipchat.com/#narrow/stream/229457-MIT-Categories.20Seminar/topic/April.2023.20-.20Joe.20Moeller’s.20talk

You can see his slides here, and watch a video of his talk here:

The monoidal Grothendieck construction

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

The talk is based on this paper:

• Joe Moeller and Christina Vasilakopoulou, Monoidal Grothendieck construction.

This, in turn, had its roots in our work on network models, a setup for the compositional design of networked systems:

• John Baez, John Foley, Joe Moeller and Blake Pollard, Network models.

Star-Autonomous Envelopes

In the fourth talk of the ACT@UCR seminar, Michael Shulman told us how to create nice string diagams for any closed symmetric monoidal category.

Mike had to teach right after his talk, but he rejoined us for discussions later at the Category Theory Community Server, here:

https://categorytheory.zulipchat.com/#narrow/stream/229966-ACT.40UCR-seminar/topic/April.2022nd.3A.20Michael.20Shulman

You can view or join the conversation there if you sign in.

You can see his slides here, or download a video of his talk here, or watch the video here:

• April 22, Michael Shulman, Star-autonomous envelopes.

Abstract. Symmetric monoidal categories with duals, a.k.a. compact monoidal categories, have a pleasing string diagram calculus. In particular, any compact monoidal category is closed with [A,B] = (A* ⊗ B), and the transpose of A ⊗ B → C to A → [B,C] is represented by simply bending a string. Unfortunately, a closed symmetric monoidal category cannot even be embedded fully-faithfully into a compact one unless it is traced; and while string diagram calculi for closed monoidal categories have been proposed, they are more complicated, e.g. with “clasps” and “bubbles”. In this talk we obtain a string diagram calculus for closed symmetric monoidal categories that looks almost like the compact case, by fully embedding any such category in a star-autonomous one (via a functor that preserves the closed structure) and using the known string diagram calculus for star-autonomous categories. No knowledge of star-autonomous categories will be assumed.

His talk is based on this paper:

• Michael Shulman, Star-autonomous envelopes.

This subject is especially interesting to me since Mike Stay and I introduced string diagrams for closed monoidal categories in a somewhat ad hoc way in our Rosetta Stone paper—but the resulting diagrams required clasps and bubbles:

This is the string diagram for beta reduction in the cartesian closed category coming from the lambda calculus.

Bigness (Part 3)

Last time I talked about a 200-terabyte proof, completed in 2016, that the journal Nature called the “largest ever”. But Michael Nielsen pointed me to a vastly longer proof from 2012. This one required about 60,000,000 terabytes—that is, 60 exabytes! So, they were unable to store the whole proof.

Let’s pause to contemplate what 60 exabytes amounts to. It’s been estimated that all words ever spoken by human beings, if transcribed into text, would take just 5 exabytes to store. As of 2020, the genome of all the humans on Earth would take about 10 exabytes to store (if one foolishly didn’t do any data compression). On the other hand, in 2011 the total capacity of all hard drives sold by Seagate Technology was 330 exabytes.

So what proof was 60 exabytes long?

A semigroup is a set with a binary associative operation, which we write as multiplication. We say two semigroups and are isomorphic if there is a bijection such that

for all , and anti-isomorphic if there’s a bijection with

for all . We say two semigroups are equivalent if they are isomorphic or anti-isomorphic.

In 2012, Andreas Distler, Chris Jefferson, Tom Kelsey, and Lars Kottho showed that up to equivalence, there are

12,418,001,077,381,302,684 ≈ 1.2 · 10¹⁹

semigroups with 10 elements. That’s the fact that took 60 exabytes to establish! They also checked their method against previous calculations of the number of semigroups with 7, 8, or 9 elements.

Upon hearing of the much shorter proof called the “largest ever” by Nature, Chris Jefferson wrote:

Darn, I had no idea one could get into the media with this kind of stuff. I had a much larger “proof”, where we didn’t bother storing all the details, in which we enumerated 718,981,858,383,872 semigroups, towards counting the semigroups of size 10.

Uncompressed, it would have been about 63,000 terabytes just for the semigroups, and about a thousand times that to store the “proof”, which is just the tree of the search.

Of course, it would have compressed extremely well, but also I’m not sure it would have had any value, you could rebuild the search tree much faster than you could read it from a disc, and if anyone re-verified our calculation I would prefer they did it by a slightly different search, which would give us much better guarantees of correctness.

As I mentioned, his team found a total of 12,418,001,077,381,302,684 semigroups of size 10. But they took advantage of a formula, also published in 2012, that counts most of the semigroups of a given size, namely those that are ‘nilpotent of degree 3’. Thus, they only had to find 718,981,858,383,872 by a brute force search, a mere 0.006% of the total:

• Andreas Distler, Chris Jefferson, Tom Kelsey, and Lars Kottho, The semigroups of order 10, in Principles and Practice of Constraint Programming, Springer Lecture Notes in Computer Science 7514, Springer, Berlin, 2012, pp. 883–899.

What does it mean for a semigroup to be nilpotent of degree 3? It means that if you multiply any three elements of the semigroup you always get the same answer! Here’s the paper that showed how to count those:

• Andreas Distler and James D. Mitchell, The number of nilpotent semigroups of degree 3, Electron. J. Combin. 19 (2012) 51.

It’s a piece of semigroup folklore that as the size approaches infinity, the fraction of semigroups of that size that are nilpotent of degree 3 approaches 1.

Puzzle. Can you prove this?

Apparently nobody has yet.

Puzzle. Assuming the folklore is true, what’s the rough growth rate of the number of semigroups with elements, counted up to equivalence? The formulas given by Distler and Mitchell are very complicated, but they may have simple asymptotics.

Here they count the number of semigroups that are nilpotent of degree 3 with various numbers of elements, up to equivalence: