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.

这项研究的目的是系统化迭代线性系统求解领域中算法的推导：迭代方法，预处理器，跨部。该方法是通过扩展正式的线性代数方法环境（火焰），该系统最初开发用于推导密集的矩阵算法。这项研究的优点首先在于它促进了实验，因为它促进了新算法的衍生，而不是长长的感应参数，而不是传统上是必要的。其次，它将通过衍生机理证明算法是正确的。 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算法。此外，它将影响迭代线性系统求解的主题的教学方式，因为火焰工作表提供了比传统上使用的更简单，更有见地的算法描述。