Collaborative Research: FMitF: Track I: Knitting Semantics

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

• 批准号: 2319182
• 负责人: James McCann
• 金额: $ 32万
• 依托单位: Carnegie-Mellon University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2023
• 资助国家: 美国
• 起止时间: 2023-10-01 至 2026-09-30
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2319182&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’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.

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