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-2022)
Kyushu University (2020) |
|---|
Principal Investigator |
THIES HOLGER 京都大学, 人間・環境学研究科, 特定講師 (50839107)
|
|---|
| Project Period (FY) |
2020-04-01 – 2024-03-31
|
| Project Status |
Granted (Fiscal Year 2022)
|
| 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 / Type Theory / Program Extraction / Spaces of subsets / ODEs / 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 |
Large progress has been made on the formalization of exact real computation in type theory and its implementation in the Coq proof assistant. Previous work on formalizing nondeterministic computation on real and complex numbers has been extended and unified. In particular, progress has been made on formalizing nondeterminism occuring in exact real computation and a sound notion of a multivalued limit operator was devised. The theory was implemented in the Coq proof assistant and using Coq's program extraction mechanism efficient Haskell programs for exact real computation can be extracted. As a non-trivial application we extract a nondeterministic program computing the complex square root.
As Covid-19 related border restrictions loosened during this year, international joint research could be resumed. During a visit by Michal Konecny (Aston University, UK), we extended the aforementioned formalization to spaces of subsets and functions, which has important applications to differential equations, in particular regarding reachability questions.
Several representations for dealing with subsets have been compared in terms of efficiency and certfied programs for generating drawings of subsets have been extracted and shown to behave well in terms of running time. Examples include fractals in two dimensional Euclidean space.
Progress has also been made on integrating the logic based proof system IFP into our type theoretical work. A system for IFP style proofs in Coq and a new program extraction to untyped lambda calculus similar to IFP was developed based on the meta-coq framework.
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
In the beginning of the AY international collaboration was still difficult due to the pandemic which made the project progress a bit slower than expected. However, as restrictions became less strict during the AY, international research could be resumed and large advancements was made.
Several new results on formalizing nondeterministic computation, in particular the formalization of limits were made.The results have been presented at NASA Formal Methods 2022 and published in the proceedings. Further, an extended version has been accepted for publication in the Journal of Logic and Computation.
In international joint research, the work has been extended to not only include computations on real and complex numbers but also on hyperspaces of subsets and function spaces. This extension is necessary to consider algorithms for differential equations which is one of the main goals of this project.
The PI presented some of the results at an invited talk at the Sirius Math Institute (online) and at smaller international workshops. A conference publication summarizing the new results is in preparation.
While the above results focus on formalization in type-theory and Coq, another proof system that is well-suited for exact real computation is the system IFP.To compare those two systems, the PI in joint work with researchers from Kyoto University is developing an interpretation of IFP in type theory and its implementation in Coq. The implementation was renewed this AY, allowing IFP style proofs and code extraction in Coq. Partial results have been presented at international conferences.
|
| Strategy for Future Research Activity |
First, it is planned to summarize the results regarding computation of subsets for presentation at an international conference and possibly a journal publication.
As a next step, it is planned to (i) extend the results on verified exact real computation, (ii) compare with other proof systems in particular IFP, (iii) unify the work with complexity results for differential equations obtained during the first year of the project and (iv) extend the Coq implementation towards algorithms for solving of differential equations.
For (i) it is planned to further investigate representations for spaces of compact subsets, also in terms of their computational complexity. Further, extensions to spaces of multivariate functions and their efficient representation e.g. by polynomial models are planned.
For (ii) it is necessary to further expand the current proof extraction mechanism for IFP style proofs in Coq and prove its soundness.
For (iii) in particular the work on subsets and function spaces is important as efficient algorithm make use of polynomial models for functions. Thus, formalizing these results, it is possible to consider operations like integration and solution operators for differential equations as well as reachability questions on certain classes of real subsets.
For (iv) it is also necessary to prove classical mathematical results about ordinary and partial differential equations in Coq. It is then planned to use this to verify computational properties for DEs in Coq and extract Haskell programs containing solution operators that solve DEs with arbitrary high precision.
|
Report
(3 results)
Research Products
(22 results)
