# Computational category theory

Computer algebra for category theory is an emerging area. The existing technologies are immature. 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

The word problem (deciding whether a diagram commutes) for finitely presented
categories is *undecidable*, by reduction from the word problem for groups.
However, more restricted computations are still feasible.

## Software

**General**

- Catlab.jl , in Julia (GitHub )
- Written by me and other contributors

- 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 category theory**

- 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: DisCoPy: Monoidal categories in Python (arxiv)

**Higher category theory**

- 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

**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 some overlap, especially in representational issues. Some proof assistants are based on dependent type theory.