Collaborative Research: FMitF: Track I: Knitting Semantics

用来控制工业针织机的程序有什么意义？通常，如果两个程序为每个给定的输入计算相同的输出数据，我们说这两个程序是等价的(意思相同)。但制造程序不接受输入，它们制造对象，而不是输出数据。这个项目研究两个控制针织机的程序何时等价，即它们生产相同的服装或面料。它通过将编程语言的数学研究与纽结理论(拓扑学的一个分支)的数学领域联系起来来做到这一点。与基本理论相结合，该项目开发了一个新的、更强大的软件堆栈，用于编译针织机程序，以及利用该理论和基础设施的新设计工具。该项目的创新之处在于提供了非刚性物体制造程序的第一个精确定义，并在此基础上开发了理论、编译器和工具。该项目有可能提高机器编织的效率和坚固性--这是目前唯一可行的不依赖大量体力劳动的整衣制造方法。纺织品生产方面的这种进步最终可能使服装生产的本地化/本地化，以及通过即时生产、定制和减少废物，实现更具生态可持续性的制造。该项目包括三个层面的研究和开发：针织机程序的基本理论，新的编译器基础设施，以及开发和展示这些进步的新设计工具。理论层面包括一种称为Knitout的与机器无关的针织机语言的形式(外延)语义。程序表示纽结理论图。研究人员正在开发这种等价性的完整公理描述、等价性(可能在P中，即在多项式时间内)的判定程序，以及相关的范式/优化程序。编译器级别包括在正式编织程序上操作的多个调度、检查和优化通道，以及与现有编织生态系统中的工具的互操作性链接。设计工具级别包括创建和调试复杂、非标准纺织品设计的工具，以及用户提示和调度控制的设计，以帮助专家用户确保其设计的高效可制造性。该奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

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 has 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, i.e., in polynomial time), 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 Knitout 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.