Polynomial-Time Program Equivalence for Machine Knitting
summary
An algorithm canonicalizes algebraic representations of knitting-program string diagrams into a normal form, reducing program equivalence to comparing those forms; equivalence is decidable by applying a complete set of seven rewrite rules and a three-stage procedure (layer swap braid) that pushes crossings down, reorders stitches, and simplifies braids. Snag detection uses braid-group facts plus adjoint functors to decompose obstructing braids, enabling vertical swaps when possible. The procedure runs in polynomial time (worst-case bound m^7, observed heuristics near quadratic) and supports translation validation and optimization for execution speed.
AI-written summary · about
chapters (7)
- 0:00Machine knitting as computing
- 3:54Knitting machine challenges
- 7:01Topological semantics
- 10:12Categorical stitches
- 13:23Canonicalization algorithm
- 19:23Polynomial-time results
- 20:47Q&A
related talks
19mBeyond Affine Loops: A Geometric Approach to Program Synthesis
01h 09mPlenary: Neighborhoods Banding Together: Reasoning Globally about Programs
23mE-Stitch: Top-Down Library Learning for E-Graphs
15mDynaplex: Analyzing Program Complexity using Dynamically Inferred Recurrence Relations
59mThe Proof Complexity of Integer Programming
40mRelational Reasoning in Object-based Programs
29mGraph Colouring Is Hard on Average for Polynomial Calculus and Nullstellensatz
01h 05mVerifying Infinitely Many Programs at Once