2020 Fiscal Year Research-status Report
Computational complexity and practice of verified and efficient algorithms for dynamical systems
| Project/Area Number |
20K19744
|
|---|
| Research Institution | Kyushu University |
|---|
Principal Investigator |
THIES HOLGER 九州大学, システム情報科学研究院, 助教 (50839107)
|
|---|
| Project Period (FY) |
2020-04-01 – 2024-03-31
|
| Keywords | 計算可能解析学 / 計算量 / 計算機援用証明 / 実数計算 |
|---|
| Outline of Annual Research Achievements |
The goal of this project is to work towards the verification of efficient algorithms for solving ordinary differential equations based on the computational model of computable analysis. This year's focus was on using the Coq proof assistant to develop the underlying theory.
Several new results could be obtained. Previous theoretical results on the formalziation of the model have been extended and summarized in a journal publication to appear in LMCS. Additional theoretical results regarding descriptions of partial functions and machine models could be obtained and published in the conference proceedings of MFCS.Progress was also made with regards to more practical work on the formalization of algorithms for exact real computation in Coq.
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
Several new theoretical and practical results could be obtained. In particular, progress on the formalization of exact real computation went more smoothly than originally expected. The work has lead to one journal publication and two conference publications in highly rated venues. Additionally, some results were presented as talks in smaller conferences and workshops.
Still, some difficulties arose because of the spread of the novel corona virus and the resulting challenges for international collaboration. While many things could be organized online, time differences and technical limitations made long and thoroughful discussions difficult.
|
| Strategy for Future Research Activity |
The results obtained in the current year will be extended to solving ordinary differential equations with analytic right hand side. This makes it necessary to also formalize some classical mathematical results about power series and ODEs. Further, some recent progress has been made on complexity theoretical results for partial differential equations. It is planned to use these results as basis for an implementation in exact real computation for certain types of PDEs and to further extend the results to other types of PDEs. Finally, it is also planned to compare the formalization results in Coq with work in other proof assistants such as the Minlog and IFP proof assistants.
|
| Causes of Carryover |
Due to the spread of the novel corona virus and the related travel restrictions, joint research could only be performed online. As joint research is a fundamental part of the project, domestic and international travel usually require a large amount of the allocated funds. In the coming academic year, it is expected that travel will be possible again at some point and thus joint research can be resumed. Further, the applicant plans to buy some new equipment such as a new computer for which the remaining amount will be used.
|
