Polynomial-Time Program Equivalence for Machine Knitting

• Nat Hurtig
• Jenny Lin
• Tom Price
• Adriana Schulz
• Jim McCann
• Gilbert Bernstein

Abstract

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.

Files

• Paper
• Supplement (proofs and definitions)

Citation

Nathan Hurtig, Jenny Han Lin, Thomas S. Price, Adriana Schulz, James McCann, and Gilbert Louis Bernstein. 2025. Polynomial-Time Program Equivalence for Machine Knitting. Proc. ACM Program. Lang. 9, ICFP, Article 248 (August 2025), 29 pages. https://doi.org/10.1145/3747517

@article{hurtig:2025:knit-equivalence,
author = {Hurtig, Nathan and Lin, Jenny Han and Price, Thomas S. and Schulz, Adriana and McCann, James and Bernstein, Gilbert Louis},
title = {Polynomial-Time Program Equivalence for Machine Knitting},
year = {2025},
issue_date = {August 2025},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {9},
number = {ICFP},
url = {https://doi.org/10.1145/3747517},
doi = {10.1145/3747517},
journal = {Proc. ACM Program. Lang.},
month = aug,
articleno = {248},
numpages = {29},
}