Antonin Delpeuch ; Jamie Vicary - Normalization for planar string diagrams and a quadratic equivalence algorithm

lmcs:6067 - Logical Methods in Computer Science, January 14, 2022, Volume 18, Issue 1 - https://doi.org/10.46298/lmcs-18(1:10)2022
Normalization for planar string diagrams and a quadratic equivalence algorithmArticle

Authors: Antonin Delpeuch ORCID; Jamie Vicary

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.

https://doi.org/10.46298/lmcs-18(1:10)2022
Source: arXiv.org:1804.07832
Volume: Volume 18, Issue 1
Published on: January 14, 2022
Accepted on: November 10, 2021
Submitted on: February 3, 2020
Keywords: Computer Science - Logic in Computer Science
Licence: Attribution 4.0 International (CC BY 4.0)

Classifications

Mathematics Subject Classification 20201
Sources:
  • [1] zbMATH Open.

Share and export

Consultation statistics

This page has been seen 3142 times.
This article's PDF has been downloaded 992 times.