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 |
| Summary: | 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. |
|---|---|
| ISSN: | 1860-5974 |