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:

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

Monoidal categories

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

Higher categories

  • 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)
  • Opetopic , in Scala & JavaScript (GitHub )

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

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)
    • Heyworth, 1999: Rewriting as a special case of noncommutative Groebner basis theory (arxiv)
    • Heyworth, 1998, PhD thesis: Applications of rewriting systems and Groebner bases to computing Kan extensions and identities among relations (arxiv)
  • 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)
    • Bonchi et al, 2020: String diagram rewrite theory I: Rewriting with Frobenius structure (arxiv)
    • Bonchi et al, 2021: String diagram rewrite theory I: Rewriting with symmetric monoidal structure (arxiv)
  • Delpeuch & Vicary, 2021: The word problem for braided monoidal categories is unknot-hard (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
  • 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.

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