AF: Small: Toward mechanical derivation of Krylov space algorithms

AF：小：走向 Krylov 空间算法的机械推导

• 批准号: 0917096
• 负责人: Victor Eijkhout
• 金额: $ 47.31万
• 依托单位: University of Texas at Austin
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2009
• 资助国家: 美国
• 起止时间: 2009-08-15 至 2013-07-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0917096&HistoricalAwards=false
• 关键词: AF; Small; Toward; mechanical; derivation

The objective of this research is to systematize the derivation of algorithms in the field of iterative linear system solving: iterative methods, preconditioners, multigrid. The approach is by extending the Formal Linear Algebra Methods Environment (FLAME), a system originally developed for deriving dense matrix algorithms.The merit of this research lies firstly in the fact that it facilitates experimentation, since it makes derivation of new algorithms essentially simpler than the lengthy induction arguments that are traditionally necessary. Secondly, it will lead to algorithms being proved correct by the very mechanism of derivation. Finally, a complete systematization of FLAME may take the form of a symbolic system, where algorithm implementations are derived mechanically, steered by the user but otherwise autonomously, from a specification of their properties rather than from an algorithmic description.The impact of this research will be on the computational community, since it lowers the threshold to exploring new algorithmic strategies, and on software developers, since it makes it easier to derive correct implementations of algorithms. Additionally, it will impact the way the subject of iterative linear system solving is taught, since FLAME worksheets offer a simpler and more insightful description of algorithms than is used traditionally.

本研究的目的是将迭代线性系统求解领域的算法推导系统化：迭代方法、预处理器、多重网格。该方法是通过扩展形式线性代数方法环境（FLAME）来实现的，该环境最初是为推导稠密矩阵算法而开发的系统。这项研究的优点首先在于它促进了实验，因为它使新算法的推导本质上比传统算法更简单。传统上必要的冗长的归纳论证。其次，它将导致算法通过推导机制本身被证明是正确的。最后，FLAME 的完整系统化可能采取符号系统的形式，其中算法实现是机械地导出的，由用户引导，但在其他方面是自主的，来自其属性的规范而不是来自算法描述。这项研究的影响将是对于计算社区来说，因为它降低了探索新算法策略的门槛；对于软件开发人员来说，因为它可以更容易地推导出算法的正确实现。此外，它将影响迭代线性系统求解主题的教学方式，因为 FLAME 工作表提供了比传统使用的更简单、更深入的算法描述。