Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: practice: software

Topic: Computer algebra

Patrick Nicodemus (Jun 08 2025 at 12:24):

How useful are Sage, Mathematica and other computer algebra systems (or symbolic algebra systems) for doing category theory?

I do not know much about computer algebra. Here is my rough stereotyped understanding:

• there are computer algebra systems which deal with finitely presented algebraic structures
• there are symbolic algebra systems which can deal with abstract, not necessarily finite structures, and they can do things like equational rewriting between words in a group, or integration/differentiation; maybe they can even do conditional rewriting (a = b under hypothesis H where H is something decidable)
• there are theorem provers and proof assistants, which are maximally flexible and can encode arbitrary reasoning

I use Rocq to formalize category theory but I'm wondering if there is a less time intensive way to use computers to help me do long computations in category theory.

Evan Patterson (Jun 08 2025 at 12:29):

You might also check out CAP - Categories, Algorithms, and Programming. I haven't tried it yet myself but the system looks quite impressive. It seems to have a focus on additive and abelian categories, though there's also plenty of stuff for ordinary category theory.

Patrick Nicodemus (Jun 08 2025 at 12:30):

Thank you. This is not the first time that GAP has come up here. I recall this conversation - #theory: category theory > software packages for computer-assisted category theory @ 💬

Patrick Nicodemus (Jun 08 2025 at 12:31):

I will check out GAP I guess and try to understand what it can be useful for

Evan Patterson (Jun 08 2025 at 12:35):

Though CAP is written in GAP, from what I understand, it's best understood as its own system.

Jacques Carette (Jun 08 2025 at 13:28):

The "old school" CASes (Maple, Mathematica) are largely useless for CT. Oh, you can program them with what you want, but out of the box, there is nothing.

It would be nice to see the area of "computational category theory" get reborn. With even more types than the original.

Ryan Wisnesky (Jun 08 2025 at 17:48):

When we originally stated building CQL (http://categoricaldata.net) we looked at a bunch of computer algebra systems to power it. But none of them had sufficient automated theorem proving capability to be able to routinely decide word problems in finite presentations. For example, Mathematica's Knuth-Bendix completion algorithm was (is?) from the 90s and simply didn't perform. On the other hand, our survey was ten years ago; perhaps CAS systems have improved.

Tyler Bryson (Jul 14 2026 at 20:23):

I've been working on a Knuth-Bendix implementation that handles finitely presented categories. The algorithm itself has scaling challenges but I have been getting incrementally better results over time. I'd be happy to try to benchmark some presentations. I'm far from an expert in this area...just someone trying to automate the boring stuff

Tyler Bryson (Jul 14 2026 at 20:33):

@Ryan Wisnesky oh oops! I should have read that closer. I actually just emailed David today on this exact subject (then came here to idly search "Knuth Bendix" and see what came up). Didn't put the connection together 'til a bit after replying

Patrick Nicodemus (Jul 14 2026 at 20:36):

Hey Tyler. I'd be happy to talk about what you find. Recently the more I read about e-graphs, the more I think they seem like an improvement over rewriting systems. Knuth Bendix seems to involve so many arbitrary choices and it seems like more of an art than a science to choose a presentation that admits a convergent system of rewrites. The e-graph approach seems rather more general by comparison, without too much tailoring required.

Tyler Bryson (Jul 14 2026 at 21:02):

Interesting. My stuff has been mostly a performance hunt with some quality of life improvements. I haven't looked into e-graphs as yet.
On KB style algorithms, my original code (all python and lots of intermediate dataclass instantiation) was total crap. But a Rust rewrite (w/ python bindings) together with some optimization and parallelization strategies and an util that lets you speculatively confluent rulesets along functors have me at a point where I'm looking for new test problems.

Patrick Nicodemus (Jul 14 2026 at 21:03):

Can you elaborate on "speculatively confluent rulesets along functors"

Tyler Bryson (Jul 14 2026 at 21:12):

Sure :) Suppose you have a functor or a suspected functor between two Finitely Presented Categories (or groups/monoids if you prefer) F: D -> C. This embodies two rewriting problems: one each for D and C.
Here's a process:

1. start KB for C while keeping a list of the images of relations of D in C under F....say FG_D for short.
2. reduce FG_D periodically dropping relations as they are validated (good KB algorithms are Noetherian...their rulesets only ever get more expressive)
3. if at any point in C's KB FG_D is empty, then F is functor, and you can pullback the weights of C's generators to D (there's details here I'm glossing over)
4. Complete KB on D
5. then you can inject the confluent subsystem into FD into C's KB

Tyler Bryson (Jul 14 2026 at 21:15):

If you label rules as native or originating from a functor (and keep track of whether they reduce) then you can use the confluence of the subsystem to avoid generating a bunch critical pairs (for example, all in subsystem critical pairs and some block skipping hacks....the point is, knowing you have a confluent subsystem lets you cheat.)

Patrick Nicodemus (Jul 14 2026 at 21:15):

Okay, I think I get the picture.

Tyler Bryson (Jul 14 2026 at 21:19):

Implementing it is a little finicky...I kept breaking correctness with subsystem rule tagging causing nasty subtle interactions with Sims style covering block skip. But after that, adding functors proved a good speed up

Ryan Wisnesky (Jul 14 2026 at 21:37):

@Tyler Bryson CQL uses an optimized version of this algorithm: https://epubs.siam.org/doi/10.1137/0214073 for handling finitely presented categories. It will decide any presentation for which an equivalent non-length decreasing re-write system exists, and contains a pspace algorithm as a sub-component that's where most of the computational cost goes. You're certainly welcome to benchmark against CQL's built-in examples. CQL also has a specialized left kan extension algorithm, but I understand it should be less performant than using egraphs (and cql can emit egglog code to do the computation)

Ryan Wisnesky (Jul 14 2026 at 21:38):

in CQL we never considered how to transport decision procedures along functors; to have a functor F : C -> D in CQL, one must already have decision procedures for C and D's word problems

Tyler Bryson (Jul 14 2026 at 21:45):

Yeah. my typical use case is very paranoid. I use the word problem to assign a certainly, possibly, refuted truth value to my "functors" it was a natural place to just knit together the computational engine

Tyler Bryson (Jul 21 2026 at 04:27):

@Ryan Wisnesky I'd love to run your examples/compare perf. I don't immediately follow the connection to ground term rewriting though...new to your software. Where should I start?

Tyler Bryson (Jul 21 2026 at 06:35):

Oh wait. Looking at examples/Quotient.html this is a monoid completion problem...FindConnections makes a category w/ one object "Connection", generators for each of the 10 entities (6 people and 4 like actions), and relations imposed by the foreign keys....
Sigma equations (liker → id, likee → id):
l = liker(l) and liker(l) = likee(l)
i.e. l = A and A = B
That's a bit more like instances of schema as categories...but I'm missing some stuff surely.
The answer if you do KB on that category is that there are two normal forms corresponding to the equivalence classes:
Equivalence classes (2):
Maud: ['Maud', 'Ned', 'Rodd', 'Todd', 'l1', 'l2', 'l3']
MrBurns: ['MrBurns', 'Smithers', 'l4']
But I'm definitely missing some stuff.

Ryan Wisnesky (Jul 21 2026 at 06:50):

Anywhere that cql uses categories it uses presentations with attached decision
procedures in order to do much of anything. Those decision procedures are
sometimes created through knuth bendix completion of an equational theory into
a rewrite system. But cql may also use congruence closure to decide a ground
theory, or a decision procedure for which there does not exist an equivalent
rewriting system (such as the main workhorse prover from the 1980s paper; it
is impossible to define a normal form sometimes and so the algorithm uses a
pspace algorithm to reason over all possible normal form choices).

The “kb” example has a bunch of test cases for unfailing knuth bendix
completion, including entropic groupoids, which I also understand are
difficult or impossible to turn into a rewrite system.

Tyler Bryson (Jul 21 2026 at 13:37):

@Ryan Wisnesky Where? https://categoricaldata.net/examples/KB.html only has a few examples, none appear to be ground term rewriting.

Ryan Wisnesky (Jul 21 2026 at 14:23):

Indeed, rarely are equational theories in cql ground, and for ground theories,
cql uses congruence closure automatically. But you can force specific provers
to be used, if say you wanted to use knuth bendix or any other provers on a
ground theory you can use the “prover” option to pick one.

Cqls knuth bendix is not optimized for ground theories, but for maximizing the
class of theories it can decide.

Ryan Wisnesky (Jul 21 2026 at 14:25):

The kb examples come primarily from “completion without failure” by Bachmair
et al

[|
researchgate.net|
---|---](https://ww
[message truncated]

Morgan Rogers (he/him) (Jul 21 2026 at 16:26):

@Ryan Wisnesky was that huge link intentional?

Tyler Bryson (Jul 21 2026 at 21:09):

I've made my researchgate request...gosh I had forgotten how annoying getting papers was. I should say, how privileged I've been to be allowed to forget... :) Good reference though

Ryan Wisnesky (Jul 22 2026 at 00:37):

If you’re referring to the bachmair link, I didn’t see the preview, I just
pasted the paper URL into an email… the URL itself looked small when i pasted
it, less than 250 characters :-). Perhaps the lesson here is not to link to
research gate?

Morgan Rogers (he/him) (Jul 22 2026 at 06:11):

I think if you adjust the square brackets appropriately the link will hide in the link text

John Baez (Jul 23 2026 at 12:24):

Yeah, I often link to things like

[this](http://math.ucr.edu/home/baez/jordan_pair.pdf)

which produces

this