Normalization for planar string diagrams and a quadratic equivalence algorithm
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 linea...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2022-01-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/6067/pdf |
| _version_ | 1797268498836094976 |
|---|---|
| author | Antonin Delpeuch Jamie Vicary |
| author_facet | Antonin Delpeuch Jamie Vicary |
| author_sort | Antonin Delpeuch |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-04-25T01:33:27Z |
| format | Article |
| id | doaj.art-75230fa23ea24d42b6e55c3f4d36580d |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:33:27Z |
| publishDate | 2022-01-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-75230fa23ea24d42b6e55c3f4d36580d2024-03-08T10:36:53ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742022-01-01Volume 18, Issue 110.46298/lmcs-18(1:10)20226067Normalization for planar string diagrams and a quadratic equivalence algorithmAntonin Delpeuchhttps://orcid.org/0000-0002-8612-8827Jamie VicaryIn 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://lmcs.episciences.org/6067/pdfcomputer science - logic in computer science |
| spellingShingle | Antonin Delpeuch Jamie Vicary Normalization for planar string diagrams and a quadratic equivalence algorithm Logical Methods in Computer Science computer science - logic in computer science |
| title | Normalization for planar string diagrams and a quadratic equivalence algorithm |
| title_full | Normalization for planar string diagrams and a quadratic equivalence algorithm |
| title_fullStr | Normalization for planar string diagrams and a quadratic equivalence algorithm |
| title_full_unstemmed | Normalization for planar string diagrams and a quadratic equivalence algorithm |
| title_short | Normalization for planar string diagrams and a quadratic equivalence algorithm |
| title_sort | normalization for planar string diagrams and a quadratic equivalence algorithm |
| topic | computer science - logic in computer science |
| url | https://lmcs.episciences.org/6067/pdf |
| work_keys_str_mv | AT antonindelpeuch normalizationforplanarstringdiagramsandaquadraticequivalencealgorithm AT jamievicary normalizationforplanarstringdiagramsandaquadraticequivalencealgorithm |