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.

为控制工业编织机而编写的程序是什么意思？通常，我们说两个程序是等效的（含义是同一件事），如果它们为每个给定输入计算相同的输出数据。但是制造计划不会投入；它们制造对象而不是输出数据。该项目研究了两个控制编织机的程序在制造等效的服装或织物的意义上是等效的。它通过将编程语言的数学研究与结理论的数学领域（拓扑结构）联系起来来做到这一点。与基本理论同时，该项目开发了一个新的，更强大的软件堆栈，用于编译针织机程序，并利用理论和基础架构的新设计工具。该项目的新颖性在于为非刚性对象提供制造计划的第一个精确定义，以及在开发理论，编译器和工具的基础上。项目的影响是提高机器编织的效率和鲁棒性的潜力 - 目前，唯一可行的全套制造方法不依赖大量的手动劳动。纺织品生产的这种进步有时可能使服装生产的出现/定位，以及通过及时生产，定制和减少废物的生态可持续制造。该项目涵盖了三层的研究和开发：针织机程序的基本理论，新的编译器基础设施以及新的设计工具以及新的设计工具利用和展示这些建议。该理论级别由一种称为编织的机器编织机语言的形式（表示）语义组成。程序表示结理论图。研究人员正在开发这种等价性的完整公理表征，等效性的决策程序（可能在p中）以及相关的正常形式/优化程序。编译器级别由在正式的编织程序上运行的许多调度，检查和优化通过，以及与现有Kintout生态系统中工具的互操作性链接。设计工具级别由用于创建和调试复杂的，非标准的纺织品设计的工具，以及用户提示和调度控件的设计，以帮助专家确保有效地制造其设计。该奖项反映了NSF的法定任务，并通过使用该基金会的知识分子功能和广泛影响来评估NSF的法定任务，并被认为是诚实的支持。