Collaborative Research: FMitF: Track I: Knitting Semantics

点击翻译按钮获取中文摘要

What is the meaning of a program written to control an industrial knitting machine? Usually we say two programs are equivalent (mean the same thing) if they compute the same output data for every given input. But manufacturing programs don’t take input; and they manufacture objects rather than output data. This project studies when two programs to control knitting machines are equivalent in the sense that they manufacture equivalent garments or fabric. It does so by connecting the mathematical study of programming languages with the mathematical field of Knot Theory (a branch of Topology). In tandem with the basic theory, this project develops a new, more robust software stack for compiling knitting machine programs, and new design tools leveraging the theory and infrastructure. This project’s novelties are in providing the first precise definition of manufacturing programs for non-rigid objects, and in developing theory, compilers and tools on that basis. The project’s impacts are the potential to improve the efficiency and robustness of machine knitting – the only presently viable approach to whole-garment manufacturing not reliant on extensive manual labor. Such advances in textile production may eventually enable onshoring/localization of garment production, as well as more ecologically sustainable manufacturing through just-in-time production, customization, and waste reduction.The project covers the research and development of three layers: a basic theory of knitting machine programs, a new compiler infrastructure, and new design tools exploiting and demonstrating these advances. The theory level consists of a formal (denotational) semantics for a machine-independent knitting machine language called Knitout. Programs denote knot theoretic diagrams. Investigators are developing a complete axiomatic characterization of this equivalence, a decision procedure for the equivalence (possibly in P), and associated normal forms/optimization procedures. The compiler level consists of a number of scheduling, checking, and optimization passes operating on formalized knitout programs, and interoperability links to tools in the existing Kintout ecosystem. The design tool level consists of tools for creating and debugging complex, non-standard textile designs, as well as the design of user hints and scheduling controls to help expert users ensure efficient manufacturability of their designs.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.