一句话：证明平面连通弦图的左/右交换均强正规化，给出线性/二次等价判定算法并强化 Joyal-Street 相干性定理。
平面弦图的图形演算中，等式由交换相邻顶点高度的 exchange moves 生成。本文研究该等式的正规化与判定问题。作者证明，分别采用左交换和右交换可得到连通弦图上的强正规化重写策略；基于这些策略，他们给出连通情形下的线性时间等价判定算法，以及一般情形下的二次时间算法。论文还给出 Joyal-Street 相干性定理的一个更强证明，并据此解决了 Selinger 关于 recumbent isotopy 的猜想。
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.
@article{paperbot1745,
title = {Normalization for planar string diagrams and a quadratic equivalence algorithm},
author = {Antonin Delpeuch and Jamie Vicary},
journal = {Logical Methods in Computer Science},
volume = {Volume 18, Issue 1},
year = {2022},
doi = {10.46298/lmcs-18(1:10)2022}
}