权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

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.

在项目的第一年，一些关于常微分方程求解的计算复杂性的理论结果可以得到改进。今年的主要目标是在项目的更实用方面取得进展，更具体地说，是在coq proof assistant中对可计算分析的算法进行形式化。这种形式化是与欧洲的研究人员密切合作完成的，形式化的结果已经成为一个名为“Incone”的库的一部分，这是一个用于可计算分析的Coq库。作为第一个结果，一些更理论性的方面已经正式确定。部分工作已发表在第十届交互式定理证明国际会议（ITP 2019）的会议记录中。包含几个额外结果的较长版本也已被接受为期刊出版物。在第二步中，考虑了更多实用方面。特别地，在Coq框架中开发了无错误的真实的数计算（精确的真实的计算）的验证实现。这个实现的重点是不仅要验证其正确性，但也可以媲美未经验证的实现的精确真实的arithmetic在efficiency.The上述工作也导致了一些新的理论结果，关于语义的精确真实的计算和制定可计算分析的类型理论设置。这项工作已经成为incone图书馆的一部分，可以在网上找到。一些主要结果也已在论文中总结，预计很快就会发表。