| Project/Area Number |
22KF0198
|
|---|
| Project/Area Number (Other) |
22F22071 (2022)
|
|---|
| Research Category |
Grant-in-Aid for JSPS Fellows
|
| Allocation Type | Multi-year Fund (2023)
Single-year Grants (2022) |
|---|
| Section | 外国 |
|---|
| Review Section |
Basic Section 60010:Theory of informatics-related
|
|---|
| Research Institution | Kyoto University |
|---|
Principal Investigator |
河村 彰星 京都大学, 数理解析研究所, 准教授 (20600117)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
PARK SEWON 京都大学, 数理解析研究所, 外国人特別研究員
|
|---|
| Project Period (FY) |
2023-03-08 – 2024-03-31
|
| Project Status |
Completed (Fiscal Year 2023)
|
| Budget Amount *help |
¥2,300,000 (Direct Cost: ¥2,300,000)
Fiscal Year 2023: ¥1,100,000 (Direct Cost: ¥1,100,000)
Fiscal Year 2022: ¥1,200,000 (Direct Cost: ¥1,200,000)
|
|---|
| Keywords | exact real computation / program verification / higher-order Hoare logic / constructive type theory / formalized mathematics |
|---|
| Outline of Research at the Start |
The goal of this research project is to obtain a formal framework for conveniently expressing, analyzing, and reasoning on exact computations over higher-order objects such as real sequences, functions, operators, subsets, et cetera that are commonly used in real-world practices in scientific computing. An imperative programming language providing such higher-order objects will be designed together with its formal denotational and operational semantics, specification logic, verification logic, and implementation.
|
| Outline of Annual Research Achievements |
We have axiomatically formalized ERC in a mathematical language (which is a constructive type theory) such that the users' informative proofs get extracted to ERC programs that are certified to be correct. Our axiomatization provides an axiomatic type for exact real numbers and basic real number operations. It further provides a nondeterminism monad thus nondeterministic computation can be expressed and formally analyzed. We have implemented it in the Coq proof assistant and customized the extraction mechanism.
Taking this development in Coq as a formal system for studying the foundational aspect of the higher-order ERC computation, we have extended the work with higher-order objects such as (continuous) functions, subspaces, and fractals. We extend the above system with functions, and open, closed, compact and overt subsets that allow short and elegant proofs with computational content for various higher-order operations. From these proofs, we can also extract programs for testing inclusion, overlapping of sets, et cetera.
The lemmas proven in the system then guide us on how the operations should be provided in the language design. We provide an imperative programming language with higher-order pure functions and a nondeterministic limit operation whose semantics are then defined regarding the lemma that appeared in our Coq development. The formal semantics and sound proof rules are provided along with an example of nondeterministic root-finding and its correctness proof.
|
