# 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, in collaboration with 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**

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

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

**Doctrines** (nLab , nCat Cafe , This Week’s Finds )

Like generalized algebraic theories, could be an organizing principle for a category theory CAS.

- Kock & Reyes, 1977: Doctrines in categorical logic (doi)
- Kelly & Street, 1974: Review of the elements of 2-categories, Sec 3: Monads in a 2-category (doi, nCat Cafe )
- Paugam, 2014:
*Towards the Mathematics of QFT*, Sec 2.1: Higher categories, doctrines, and theories- Doctrine of n-categories is an (n+1)-category, e.g., doctrine of categories is an (arbitrary) 2-category

**Formal proofs**

I am 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.