一句话：提出机器针织程序拓扑语义的规范化算法，并证明其正确性与多项式时间，从而判定程序等价。
机器针织通过数百枚机针将纱线编织成互锁线圈，其程序具有复杂的拓扑语义，直接判定两段针织程序是否等价并不容易。本文以一类 monoidal 范畴变体刻画机器针织程序的拓扑语义，该语义与 string diagram 紧密对应。作者将等价性判定转化为范畴中词上的规范化问题，设计一个 abstract rewriting system（ARS），并给出把代数表示化为规范形式的算法。论文证明了该规范化算法能够正确判定程序等价，且运行时间为多项式时间。该工作为机器针织程序的编译、优化与验证提供了可判定且高效的语义基础。
We present an algorithm that canonicalizes the algebraic representations of the topological semantics of machine knitting programs. Machine knitting is a staple technology of modern textile production where hundreds of mechanical needles are manipulated to form yarn into interlocking loop structures. Our semantics are defined using a variant of a monoidal category, and they closely correspond to string diagrams. We formulate our canonicalization as an Abstract Rewriting System (ARS) over words in our category, and prove that our algorithm is correct and runs in polynomial time.
@article{paperbot3049,
title = {Polynomial-Time Program Equivalence for Machine Knitting},
author = {Nathan Hurtig and Jenny Han Lin and Thomas S. Price and Adriana Schulz and James McCann and Gilbert Louis Bernstein},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {ICFP},
year = {2025},
doi = {10.1145/3747517}
}