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），系统最初开发用于推导稠密矩阵algorithm.The优点，这项研究首先在于，它有利于实验的事实，因为它使推导新的算法本质上比冗长的归纳参数，传统上是必要的。其次，它将导致算法被证明是正确的派生机制。最后，FLAME的完整系统化可能采取符号系统的形式，其中算法实现是机械地导出的，由用户操纵，但在其他方面是自主的，从它们的属性的规范而不是从算法描述。这项研究的影响将在计算社区，因为它降低了探索新算法策略的门槛，并对软件开发人员，因为它使得更容易导出算法的正确实现。此外，它将影响迭代线性系统求解主题的教学方式，因为FLAME算法提供了比传统方法更简单和更有见地的算法描述。