| 研究課題/領域番号 |
20K19744
|
|---|
| 研究機関 | 京都大学 |
|---|
研究代表者 |
THIES HOLGER 京都大学, 人間・環境学研究科, 特定講師 (50839107)
|
|---|
| 研究期間 (年度) |
2020-04-01 – 2024-03-31
|
| キーワード | Computable Analysis / Exact Real Computation / Formal Proofs / Proof Assistants |
|---|
| 研究実績の概要 |
The project can be broadly divided into two parts, the first dealing with complexity of differential equations and exact real computation (ERC) algorithms, the second dealing with formalizing ERC in the Coq proof assistant.
Regarding the first part, novel algorithms for computing solutions of certain partial differential equations (PDEs) were found and shown to behave well in terms of complexity. In particular, the focus was on linear PDEs with analytic matrix coefficients and the Heat and the Schroedinger equation with given analytic initial data. The algorithms were implemented in the ERC framework iRRAM and tested on several practical examples.
Regarding the second part, together with international collaborators a new framework for formal verification of ERC based on a type-theoretical setting was derived. The type-theoretical setting is chosen to be simple and allows a realizability interpretation to validate certain axioms in the theory. Building on the framework a new formalization of ERC in the Coq proof assistant was built. The formalization is conceptually similar to modern implementations of ERC and it allows to extract efficient Haskell programs from proofs. The extracted programs use the AERN framework, a popular Haskell framework for exact real computation, for basic operations on real numbers.
Lastly, comparisons to other formal proof systems, in particular the system IFP have been made. IFP is based on intutionistic fixed point logic and is mainly used for the extraction of ERC programs from proofs, and thus comparing the two approaches lead to new insights.
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
Large progress was made for both parts of the project.
Regarding PDEs, several new algorithms based on power series have been devised and implemented in the iRRAM C++ framework. The results were published in the proceedings of a well-known international conference (CASC 2021) and the PI presented the results at invited talks at CCA2021 and an autumn school on proof and computation.
Progress was also made on the formalization of ERC in the Coq proof assistant. The new type-theorical framework devised during this AY allowed to quickly prove several results in the proof assistant and progress was faster than initially planned. Further, the extraction directly to an ERC framework is a new idea that had not been considered before and lead to much more efficient extracted code.
First results have already been published in the proceedings of WoLLiC2021 and further results have been accepted for publication at Nasa Formal Methods 2022.
Some smaller results on the comparison to the formal system IFP have also been presented at workshops.
Still, the ongoing Covid-19 pandemic made international collaboration difficult. Although online meetings were helpful, they could not completely replace physical meetings. As the project is done in close collaboration with international researchers and progress could have been faster without the ongoing restrictions.
|
| 今後の研究の推進方策 |
First, it is planned to summarize the currently obtained results on the formalization of ERC in a larger journal publication.
Afrer that the framework will be extended to other mathematical operations.
In particulat, a representation for spaces of functions will be considered that makes it possible to implement not only functions but also operators and functionals on real numbers. Other extensions that will be considered are matrices of real and complex numbers and operations like computing eigenvalues and Matrix diagonalization. Furtehr, more theoretical work on relating results on classical real numbers in Coq to our implementations of real numbers will be conducted.
Regarding algorithms for differential equations, it is planned to collaborate more closely with numerical scientists and devise solution methods of other forms of PDEs and their extension to ERC. Possible applications include fluid dynamics and other areas of physics and such applications will also be considered.
Finally, it is planned to unify the two parts of the project. In particular, the extension to spaces of functions allows to consider operations like integration and solution operators for ordinary and partial differential equations. The ERC algorithms which have been found can then be formalized and be proven correct in Coq. To this end, some classical mathematical results about differential equations also need to be proven in Coq.
|
| 次年度使用額が生じた理由 |
Due to ongoing travel restrictions, international travel and joint international research in person could still not be conducted this academic year. However, as online meetings can not completely replace physical meetings, it is planned to meet in person with international collaborators as soon as possible and thus funds can be used for travel expenses in the next fiscal year.
|
