# 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)

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