Normalization for planar string diagrams and a quadratic equivalence algorithm

TL;DR

This paper introduces normalization strategies for planar string diagrams, providing efficient algorithms for diagram equivalence and proving a key coherence theorem in categorical diagram calculus.

Contribution

It presents strongly normalizing rewrite strategies for exchange moves and offers linear and quadratic algorithms for diagram equivalence, along with a proof of the Joyal-Street coherence theorem.

Findings

Linear-time algorithm for connected diagram equivalence

Quadratic-time algorithm for general diagram equivalence

Proof of the Joyal-Street coherence theorem

Abstract

In the graphical calculus of planar string diagrams, equality is generated by exchange moves, which swap the heights of adjacent vertices. We show that left- and right-handed exchanges each give strongly normalizing rewrite strategies for connected string diagrams. We use this result to give a linear-time solution to the equivalence problem in the connected case, and a quadratic solution in the general case. We also give a stronger proof of the Joyal-Street coherence theorem, settling Selinger's conjecture on recumbent isotopy.