2024 Fiscal Year Research-status Report
Research on Computable Analysis and Verification of Efficient Exact Real Computation
| Project/Area Number |
24K20735
|
|---|
| Research Institution | Kyoto University |
|---|
Principal Investigator |
THIES HOLGER 京都大学, 人間・環境学研究科, 特定講師 (50839107)
|
|---|
| Project Period (FY) |
2024-04-01 – 2029-03-31
|
| Keywords | Formal Verification / Computable Analysis / Coq / Exact Real Computation |
|---|
| Outline of Annual Research Achievements |
During this fiscal year, significant progress was made on extending the Coq formalization library cAERN for formalizing exact real computation. The library was expanded to include solution operators for simple polynomial ordinary differential equations (ODEs). From these formal proofs, programs that compute ODE trajectories with arbitrary precision can be automatically extracted. Experimental results confirmed that these extracted programs perform efficiently in practice. The results were presented at the ITP 2024 international conference.
Building on this, the approach was further generalized to cover ODEs with analytic right-hand sides for any finite dimension. This generalization no longer depends on the cAERN library and can be used more broadly within the Coq ecosystem, improving accessibility and integration and allows to compute solutions directly in the proogf assistant additionally to extracting programs. A paper summarizing these results is currently being prepared.
In another direction, we extended our previous formalization of subsets and continuity from Euclidean spaces to general Polish spaces, which are important in analysis and probability theory. We showed the equivalence of several representations of subsets in this setting, and all results were fully formalized in Coq.
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
The research project has proceeded according to the planned schedule without major obstacles. Key milestones outlined in the original research plan were successfully achieved during the fiscal year, including the extension of the Coq library cAERN to support polynomial ODEs and the development of a more general formalization for analytic ODEs. These results were presented at major international conferences and form the basis of an upcoming publications. In addition, further progress was made in the formalization of foundational concepts in analysis, exceeding the original scope. While some technical challenges were encountered, they were resolved within expected timeframes. Overall, the project is on track and developing steadily toward its goals.
|
| Strategy for Future Research Activity |
Building on the formal foundations developed so far, the research will proceed in two main directions. First, the generalized solution method for analytic ordinary differential equations will be further refined and extended to cover a broader class of initial value problems. In particular, it is planned to integrate the results better with some existing libraries in the Coq ecosystem, such as mathcomp-analysis. To this end, it is planned to also formalize some results from classical analysis addtionally to the constructive theorems developed so far. This is also expected to enable further generalization of the approach to selected classes of partial differential equations.
At the same time, efforts will be made to improve the efficiency and practical applicability of the formalized theory. To this end, experimental evaluations will be conducted, including applications to concrete problems arising in fields such as physics.
|
