Data Structures for Topologically Sound Higher-Dimensional Diagram Rewriting

TL;DR

This paper introduces data structures and algorithms for higher-dimensional diagram rewriting that are topologically sound, enabling applications in higher algebra, category theory, and computational topology, with a practical Python implementation.

Contribution

It presents a novel computational framework for diagrammatic sets with topological soundness, including data structures, isomorphism algorithms, and a type theory, implemented in Python.

Findings

Data structures for arbitrary-dimensional diagrams

Isomorphism problem solved in O(n^3 log n) time

Python library rewalt supports visualization and manipulation

Abstract

We present a computational implementation of diagrammatic sets, a model of higher-dimensional diagram rewriting that is "topologically sound": diagrams admit a functorial interpretation as homotopies in cell complexes. This has potential applications both in the formalisation of higher algebra and category theory and in computational algebraic topology. We describe data structures for well-formed shapes of diagrams of arbitrary dimensions and provide a solution to their isomorphism problem in time O(n^3 log n). On top of this, we define a type theory for rewriting in diagrammatic sets and provide a semantic characterisation of its syntactic category. All data structures and algorithms are implemented in the Python library rewalt, which also supports various visualisations of diagrams.