AF: Small: Toward mechanical derivation of Krylov space algorithms

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

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.