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 图书馆的一部分，可以在网上找到。一些主要结果也已总结在论文中，预计很快就会发表。