ICFP/SPLASH 2025 (series) / ICFP 2025 (series) / ICFP Papers /
Polynomial-Time Program Equivalence for Machine Knitting
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 yarns into interlocking loop structures. Our semantics are defined using a variant of a monoidal category, and they closely correspond with 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.