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.
Tyler Bryson (Jul 16 2026 at 21:55):Hi all,
I have a personal software project I've been working on for some time. One component is an implementation of Knuth Bendix for finitely presented categories. I'm starting to see results that, to me are good. But huge grain of salt I am no expert in term rewriting.
I'm curious if people here know of some good benchmarks / interesting completion problems I might try. Some recent results. I brought the wall time for Brauer monoid on 12 points down from over 4hrs to just under 3hrs. That's a confluent system with 8,341,198 rules and 316,234,143,224 non-identity elements.
Big normal form counts are handled as well. For example, the truncated simplex category Δ(55) completes in ~26 seconds with 115499 rules and the exact expected ~7.7×10^17 normal forms.
These laptop calculations using a recursive ordering, but I can also run wtlex.
I know performance is hard to gauge. The point is more...my laptop doesn't explode when I ask it to do tasks like the above that require handling 10s-100's of millions of critical pairs. Anyway, happy to chat with folks
Ryan Wisnesky (Jul 16 2026 at 22:11):there are problem sets available at https://www.tptp.org , look for the "UEQ" / unit equality problems. E and Vampire are the systems to beat performance-wise, and they go beyond equational logic. For CQL, we like the 1980s algorithm because it is complete, more so than it being fast.
Harrison Grodin (Jul 17 2026 at 01:51):I have an (outdated, likely bit-rotted) implementation of Knuth-Bendix here - in case you're interested, there are a few test cases included, the most substantial of which is the axioms for a group.
Harrison Grodin (Jul 17 2026 at 01:52):(Fwiw, this implementation only handles trees, not categories more generally; and it's hilariously inefficient and slow!)