Computational complexity and practice of verified and efficient algorithms for dynamical systems
| Project/Area Number |
20K19744
|
|---|
| Research Category |
Grant-in-Aid for Early-Career Scientists
|
| Allocation Type | Multi-year Fund |
|---|
| Review Section |
Basic Section 60010:Theory of informatics-related
|
|---|
| Research Institution | Kyoto University (2021)
Kyushu University (2020) |
|---|
Principal Investigator |
THIES HOLGER 京都大学, 人間・環境学研究科, 特定講師 (50839107)
|
|---|
| Project Period (FY) |
2020-04-01 – 2024-03-31
|
| Project Status |
Granted (Fiscal Year 2021)
|
| Budget Amount *help |
¥4,290,000 (Direct Cost: ¥3,300,000、Indirect Cost: ¥990,000)
Fiscal Year 2023: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
Fiscal Year 2022: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
Fiscal Year 2021: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
Fiscal Year 2020: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000)
|
|---|
| Keywords | Computable Analysis / Exact Real Computation / Formal Proofs / Proof Assistants / 計算可能解析学 / 計算量 / 計算機援用証明 / 実数計算 / Computable analysis / Differential equations / Verification / Formal proofs / Complexity Theory |
|---|
| Outline of Research at the Start |
The research project aims to get insights into the computational complexity of problems in the physical world and to provide efficient and formally verified algorithms for computations that involve real numbers. Such algorithms lead to better, more reliable and reusable software.
|
| Outline of Annual Research Achievements |
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.
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
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.
|
| Strategy for Future Research Activity |
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.
|
Report
(2 results)
Research Products
(16 results)
