Verified exact computation over continuous higher types
| 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 |
Granted (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 |
An imperative language for exact real number computation with pure higher-order function construction is proposed. The design is inspired by the standard functions in C++. The language is further equipped with primitive operators for countable nondeterministic choices and nondeterministic limits to make the language’s function construction useful. The language’s denotational semantics is formalized based on computable analysis and domain theory using an unbounded powerdomain for countable nondeterminism. Sound Hoare-style proof rules for the two additional primitive operations are devised. As an example, an imperative program nondeterministically computing a root of a continuous real function, a constructive variant of the Intermediate Value Theorem, is given and proved correct.
Coq-AERN is an axiomatic formalization of exact real number computation in a constructive type theory and Coq. The formalization is extended with function spaces, open subsets, closed subsets, compact subsets, and overt subsets. Similarly to the programming language counterpart, this formalization is extended with countable choices. Examples of drawing various subsets, including some fractals, in Euclidean spaces are given.
|
| 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 four steps were planned for FY2022: i) syntax for higher-order types, objects, and operations, ii) natural operational semantics, iii) domain-theoretic denotational semantics, and iv) the soundness of the semantics. Except for the operational semantics, the other steps are achieved as they were planned. A part of the achievement is submitted to an international conference and a part of the result is accepted for publication in Journal of Logic and Computation (Oxford Univ Press). Instead, some parts, including Hoare-style proof rules of some fundamental operations and the logical language part, of the next year’s plan are studied. The operational semantics part will be dealt in FY2023 when the implementation of the language is considered.
|
| Strategy for Future Research Activity |
There is no major deviation from the original plan FY2023. Based on the proof rules for countable choices and nondeterministic limits, we provide a complete set of proof rules to accommodate further necessary primitive operations that are to be specified further in FY2023 during seeking for example data types and operations. It may include extending the language further to have higher-order functions that cause side-effects, reference variables, and multi-threads that are communicating. Formal denotational semantics for the extensions, and their proof rules will be given. The soundness and (relative) completeness of the set of proof rules will be proven. The operational semantics of the language will be studied when we implement the language. It includes studying the possibility of including concurrent computing in realizing nondeterminism. We include several nontrivial examples and implementations for higher-order computations.
|
Report
(1 results)
Research Products
(6 results)
