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:

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 )
  • 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
    • Rydeheard & Burstall, 1988: Computational Category Theory (pdf)
    • Overview of OBJ in Ch 10: Formal systems for category theory

Monoidal category theory

  • Quantomatic , in Standard ML & JVM (GitHub )
    • Proof assistant for compact closed categories
    • Kissinger & Zamdzhiev, 2015: Quantomatic: A proof assistant for diagrammatic reasoning (doi, arxiv)
    • Kissinger, 2012, PhD thesis: Pictures of processes: Automated graph rewriting for monoidal categories (arxiv)
  • 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 )
    • Blog posts on Azimuth and n-Cat Cafe (1 ,2 ,3 ,4 )
    • Bar, Vicary, 2016: Data structures for quasistrict higher categories (arxiv)
    • Bar, Kissinger, Vicary, 2016: Globular: an online proof assistant for higher-dimensional rewriting (arxiv)
  • Homotopy.io , in JavaScript (GitHub , nLab )
    • Successor to Globular, by Jamie Vicary and collaborators
    • Dorn, 2018, PhD thesis: Associative n-categories (arxiv)
    • Reutter & Vicary, 2019: High-level methods for homotopy construction in associative n-categories (arxiv)

Conferences

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)

Operads

  • 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

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.

  • O’Keefe, 2004: Towards a readable formalization of category theory (doi)
    • Nice summary of work up to 2004
  • Gross, Chlipala, Spivak, 2014: Experience implementing a performant category-theory library in Coq (doi, arxiv)