Jenny Lin

Formalizing Object Equivalence in Machine Knitting Degree Type: CS
Advisor(s): James McCann
Graduated: August 2024

Abstract:

Correctness is a desirable property for any program, whether that program computes an equation, controls a machine, or interprets data. Defining what it means for a program to be correct can be surprisingly nuanced, however, especially when that program is used to create a physical object. We can reframe this problem by treating correctness as a question of equivalence. Given some target object, is the result of a fabrication process equivalent to the target object? However, this now requires that we answer the still complicated question of what it means for two objects to be equivalent. In order to do so, we not only need a precise definition of object meaning, but also a strong understanding of how we create and interact with the objects around us.

In this thesis, I tackle this problem of meaning and equivalence for machine knitting programs. Knitting is the act of taking a few strands of yarn and deforming them into interlocking loops that result in a stable structure. While knitting machines are capable of quickly fabricating a vast array of structures with controllable material properties, the complexity of both the machine control process and the resulting physical object makes translating between the two incredibly difficult. This gap prevents existing programing and design tools from accessing the full breadth of its fabrication possibilities. To address this, I formally characterize the complete space of machine knitting programmings. I begin by introducing fenced tangles, a novel mathematical object designed to match intuition about knit object meaning. From there, I use fenced tangles to define a semantics for knitout, which is a low-level language for controlling v-bed knitting machines. The underlying program meaning is then used to reason about the correctness of a set of practical program transformations. I then use this semantic function as guidance for developing Instruction Graphs, which are an intermediate representation of knit objects. Unlike existing knit object representations, Instruction Graphs can capture the full range of machine knittable objects and can be verified as machine knittable using three easy to check graph embedding properties. Finally, I discuss how fabrication constraints may enable an algebraic approach to computing machine knitting program equivalence.

Thesis Committee:
James McCann (Chair)
Jan Hoffmann
Scott Hudson
Adriana Schulz (University of Washington)

Srinivasan Seshan, Head, Computer Science Department
Martial Hebert, Dean, School of Computer Science

Keywords:
Computer-aided Manufacturing, Computer-aided Design, Program Semantics, Domain Specific Languages, Machine Knitting, Knot Theory