Collaborative Research: FMitF: Track I: Knitting Semantics

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

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.