2023 Fiscal Year Research-status Report
Computational complexity and practice of verified and efficient algorithms for dynamical systems
| Project/Area Number |
20K19744
|
|---|
| Research Institution | Kyoto University |
|---|
Principal Investigator |
THIES HOLGER 京都大学, 人間・環境学研究科, 特定講師 (50839107)
|
|---|
| Project Period (FY) |
2020-04-01 – 2025-03-31
|
| Keywords | Computable Analysis / Exact Real Computation / Formal Proofs / Type Theory / ODEs |
|---|
| Outline of Annual Research Achievements |
This year's main focus was on the implementation of exact real computation in the Coq proof assistant. Previous results on the computation on subsets have been extended and new efficient representations for dealing with subsets have been devised and compared. The results were summarized for presentation at the 48th International Symposium on Mathematical Foundations of Computer Science and an extended journal version is currently in progress.
Further, during a research visit by Pieter Collins (Maastricht University) possible applications to his work on verified numerics were discussed.
Large progress was also made toward one of the main goals stated in the research proposal, that is, toward a verified solver for ordinary differential equations in exact real computation. In joint work with Sewon Park (Kyoto University) a simple solver for polynomial ordinary differential equations was implemented in the Coq proof assistant. For this, it was also necessary to formalize a theory of classical functions in our system, and results from classical mathematics concering e.g. differentiabilty. From proofs in our formal system, we can extract Haskell programs for such a solvers.The programs can be used to solve polynomial ODEs on some interval and print out approximations of the result up to any desired output precision.
Lastly, some applications to particle physics could be discovered. Simulation of particle dynamics turns out to be a good case study for exact real computation, as it often requires a very high precision that can not be achieved by classical numerical methods.
|
| 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 advancements toward the original goal of verified ODE solving could be made during the last AY. First, the PI together with his collaborators could extend the previous formalization to a theory of classical functions, which e.g. could be used to formalize statements about continuity and differentiabilty, which are in turn needed to define solution operators for ODEs. Further, on top of this theory a simple solver for ODEs was implemented and verified to be correct. This solver can be extracted as a Haskell program which has shown to perform rather efficiently.
Also, some practical applications of the work in particle physics could be discovered.
The PI could present several of these new results on international conferences and workshops.
On the other hand, the solver currently only works for 1-dimensional polynomial ODEs and is thus not very generic. There is still some work left to generalize the solver to higher dimension and more generic types of functions.
|
| Strategy for Future Research Activity |
First, it is planned to summarize the results obtained in the previous AY in a publication at an international conference. The main task in this AY is then to extend the results further. Currently the ODE solver only works for 1-dimensional polynomial ODEs. As a first step, it is planned to extend the results to higher-dimensions. This is quite challenging, as it also requires the formalization of some classical results, that we currently only formalized for 1 dimension. Nonetheless, the algorithm itself generalizes nicely to higher dimension, and thus an implementation should be possible.
The PI plans to present these results at international conferences and workshops, in particular the CCA and CCC conferences.
Further, the applications of the work in particle physics will be explored more deeply, in collaboration with experts from physics.
Regarding changes to the research plan, while in previous years also the comparison to other proof assistants, and in particular the system IFP, was a central topic, it is planned to focus mostly on the Coq formalization in the coming AY, as more progress toward the initial goal of verified ODE solving could be done in Coq. Still it is planned to consider how some of the results could be formalized in a logic based system like IFP.
|
| Causes of Carryover |
Due to the pandemic, in the first years of the project international cooperation was difficult and less money than previously planned was allocated for travel expenses. This also slowed down the progress of the project in the first years. As international collaboration is very important for the progress of the project, the funds are planned to be used for visiting conferences and joint research with experts from other universities.
|
Research Products
(9 results)
