Towards efficient solvers for ordinary differential equations in exact real arithmetic

精确实数运算中常微分方程的高效求解器

基本信息

批准号：
18J10407
负责人：
THIES HOLGER
金额：
$ 1.22万
依托单位：
Kyushu University
依托单位国家：
日本
项目类别：
Grant-in-Aid for JSPS Fellows
财政年份：
2018
资助国家：
日本
起止时间：
2018-04-25 至 2020-03-31
项目状态：
已结题

项目摘要

In the first year of the project, some of the theoretical results on the computational complexity of ODE solving could be improved. The main goal of this year was to make progress on the more practical side of the project, more specifically on formalizing algorithms from computable analysis in the coq proof assistant.This formalization was done in close collaboration with researchers in Europe and the formalized results have been made part of a library called "Incone", a Coq library for computable analysis.As a first result, some more theoretical aspects have been formalized. Part of the work has been published in the proceedings of the 10th International Conference on Interactive Theorem Proving (ITP 2019).A longer version containing several additional results has also been accepted as a journal publication.In a second step more practical facets have been considered. In particular, a verified implementation of error-free real number computation (exact real computation) was developed in the Coq framework. The focus of this implementation was to not only verify its correctness, but also be comparable to non-verified implementations of exact real arithmetic in terms of efficiency.The above work also lead to some new theoretical results regarding the semantics of exact real computation and the formulation of computable analysis in a type-theoretic setting. The work has been made part of the incone library which can be found online. Some of the main results have also been summarized in papers and are expected to be published soon.

在项目的第一年中，可以改善有关ode解决的计算复杂性的一些理论结果。今年的主要目的是在项目的更实际方面取得进展，更具体地是在COQ证明助理中可计算分析的算法上形式化算法。这是与欧洲的研究人员密切合作进行的，并将正式的结果与一个名为“ Incone”的图书馆的一部分合作，可用于计算分析的Coq图书馆。这项工作的一部分已发表在第十届国际交互式定理会议论文集（ITP 2019）。较长的版本包含几个其他结果也已被接受为期刊出版物。在第二步中，已经考虑了更实用的方面。特别是，在COQ框架中开发了经过验证的无错误实际数量计算（确切的实际计算）的实现。该实施的重点不仅是要验证其正确性，而且还可以与效率上的精确实际算术的未验证实现相媲美。这项工作已成为Incone库的一部分，可以在线找到。一些主要结果也已在论文中进行了总结，预计将很快发表。