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 1856 times.
    This article's PDF has been downloaded 756 times.