Computational category theory
Computational category theory, including but not limited to computer algebra for categories, is an emerging area. Here are a few lists of software and systems compiled by others:
- Mathematical software listed on nLab
- Question on Math.SE
- Joshua Tan’s 2018 comparison of CT software
As one would expect, the word problem (deciding whether a diagram commutes) for finitely presented categories is undecidable, by reduction from the word problem for groups. However, computations are still feasible in many particular cases.
Software
General
- Catlab.jl , in Julia (GitHub )
- Created and maintained by me and other contributors
- More information at AlgebraicJulia.org
- Cateno, in Julia (GitHub )
- Slides from NIST Computational Category Theory Workshop 2015
- Written by Jason Morton, unmaintained since mid 2015
- My original inspiration for Catlab
- Computational Category Theory , in Standard ML
Monoidal categories
- Quantomatic , in Standard ML & JVM (GitHub )
- Cartographer , in Haskell (GitHub )
- Graphical editor and proof assistant for symmetric monoidal theories
- Sobociński, Wilson, Zanasi, 2019: Cartographer: a tool for string diagrammatic reasoning (pdf)
- DisCoPy, in Python (GitHub )
- Computing with compact closed categories for applications to CQM and NLP
- de Felice, Toumi, Coecke, 2020: DisCoPy: Monoidal categories in Python (arxiv)
Higher categories
- Globular , in JavaScript (GitHub , nLab )
- Homotopy.io , in JavaScript (GitHub , nLab )
- Opetopic , in Scala & JavaScript (GitHub )
- An online editor for opetopes , written by Eric Finster
- Documentation provides a nice interactive introduction to opetopes
Conferences
- Workshop on Higher-Dimensional Rewriting and Applications
Literature
Computing on categories
Categories
- Walters, 1991: Categories and Computer Science, Ch. 7: Computational
category theory
- Sec 7.1: Knuth-Bendix procedure for finitely presented category
- Sec 7.2: Generalized Todd-Coxeter procedure for computing left Kan extensions (aka, the Carmody-Walters algorithm)
- Spivak & Wisnesky, 2012: Relational foundations for functional data migration
(doi, arxiv)
- Sec 2.2: references on word problem for categories
Because all concepts are Kan extensions, there is a nonnegible literature on computing Kan extensions, particularly left Kan extensions of set-valued functors:
- Bush, Leeming, Walters, 2003: Computing left Kan extensions (doi)
- “Much simplified” version of algorithm in: Carmody & Walters, 1991: Computing quotients of actions of a free category (doi)
- See also: Carmody, Leeming, Walters, 1995: The Todd-Coxeter procedure and left Kan extensions (doi)
- Extended to finite product preserving functors in: Leeming & Walters, 1995: Computing left Kan extensions using the Todd-Coxeter procedure (doi)
- Brown & Heyworth, 2000: Using rewriting systems to compute left Kan extensions and induced actions of categories (arxiv, doi)
- Ghani & Heyworth, 2002: Computing over K-modules
- Computing left Kan extensions over the category of K-modules
- Earlier version: Heyworth, 2000: Groebner basis techniques for computing actions of K-categories (arxiv)
- Meyers, Spivak, Wisnesky, 2019: Fast left Kan extensions using the Chase
(arxiv, slides)
- Warning: this algorithm is encumbered by a patent
Monoidal categories and higher categories (MO )
- Burroni, 1993: Higher-dimensional word problems with applications to equational logic (doi)
- Lafont, 1995: Equational reasoning with 2-dimensional diagrams (doi)
- Morton, 2014: Belief propagation in monoidal categories (arxiv, slides)
- Mimram, 2014: Towards 3-dimensional rewriting theory (arxiv, slides)
- Nice introduction and literature review
- Bonchi et al, 2016: Rewriting modulo symmetric monoidal structure (doi, arxiv)
- Delpeuch & Vicary, 2021: The word problem for braided monoidal categories is unknot-hard (arxiv)
- Bremner & Dotsenko, 2016: Algebraic operads: An algorithmic companion (doi,
pdf, MR )
- Billed as a computational companion to Loday & Vallette, 2012: Algebraic operads
- Develops a theory of Gröbner bases for noncommutative associative algebras and, more generally, for algebraic operads
- Patterson, Spivak, Vagner, 2020: Wiring diagrams as normal forms for computing in symmetric monoidal categories (arxiv)
Computing with categories
Rewriting via 2-categories (also relevant to classical computer algebra)
- Rydeheard & Stell, 1987: Foundations of equational deduction: A categorical treatment of equational proofs and unification algorithms (doi)
- Seely, 1987: Modeling computations: a 2-categorical framework (pdf)
- Beta & eta conversion in typed lambda calculus as 2-morphisms
- Quite sketchy but conveys the general idea
- Commentary on nCat Cafe
- Power, 1989: An abstract formulation for rewrite systems (doi)
- Hilken, 1996: Towards a proof theory of rewriting: the simply typed
2λ-calculus (doi, pdf)
- Inspired by Seely, 1987, especially in Section 3.2
- Mellies, 2016: Five basic concepts of axiomatic rewriting theory (arxiv, pdf)
Formal proofs
I am more interested in computer algebra than in formal proofs, but there is certainly overlap, especially in representational issues. Some proof assistants are based on dependent type theory.