文章基本信息

标题：NORMALIZATION FOR PLANAR STRING DIAGRAMS AND A QUADRATIC EQUIVALENCE ALGORITHM
本地全文：下载
作者：Antonin Delpeuch ; Jamie Vicary
期刊名称：Logical Methods in Computer Science
印刷版ISSN：1860-5974
电子版ISSN：1860-5974
出版年度：2022
卷号：18
期号：1
页码：1-38
DOI：10.46298/lmcs-18(1:10)2022
语种：English
出版社：Technical University of Braunschweig
摘要：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.