| 研究課題/領域番号 |
20K19744
|
|---|
| 研究機関 | 九州大学 |
|---|
研究代表者 |
THIES HOLGER 九州大学, システム情報科学研究院, 助教 (50839107)
|
|---|
| 研究期間 (年度) |
2020-04-01 – 2024-03-31
|
| キーワード | 計算可能解析学 / 計算量 / 計算機援用証明 / 実数計算 |
|---|
| 研究実績の概要 |
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.
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
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.
|
| 今後の研究の推進方策 |
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.
|
| 次年度使用額が生じた理由 |
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.
|
