Collaborative Research: FMitF: Track I: Knitting Semantics

合作研究：FMitF：第一轨：针织语义

• 批准号: 2319181
• 负责人: Gilbert Bernstein
• 金额: $ 43万
• 依托单位: University of Washington
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2023
• 资助国家: 美国
• 起止时间: 2023-10-01 至 2026-09-30
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2319181&HistoricalAwards=false
• 关键词: Collaborative; Research; FMitF; Track; Knitting

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.

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