2023 Fiscal Year Annual Research Report
Verified exact computation over continuous higher types
| Project/Area Number |
22KF0198
|
|---|
| Allocation Type | Multi-year Fund |
|---|
| Research Institution | Kyoto University |
|---|
Principal Investigator |
河村 彰星 京都大学, 数理解析研究所, 准教授 (20600117)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
PARK SEWON 京都大学, 数理解析研究所, 外国人特別研究員
|
|---|
| Project Period (FY) |
2023-03-08 – 2024-03-31
|
| Keywords | exact real computation / program verification / higher-order Hoare logic / constructive type theory / formalized mathematics |
|---|
| 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.
|
