| 研究課題/領域番号 |
22KF0198
|
|---|
| 補助金の研究課題番号 |
22F22071 (2022)
|
|---|
| 研究種目 |
特別研究員奨励費
|
| 配分区分 | 基金 (2023)
補助金 (2022) |
|---|
| 応募区分 | 外国 |
|---|
| 審査区分 |
小区分60010:情報学基礎論関連
|
|---|
| 研究機関 | 京都大学 |
|---|
研究代表者 |
河村 彰星 京都大学, 数理解析研究所, 准教授 (20600117)
|
|---|
| 研究分担者 |
PARK SEWON 京都大学, 数理解析研究所, 外国人特別研究員
|
|---|
| 研究期間 (年度) |
2023-03-08 – 2024-03-31
|
| 研究課題ステータス |
完了 (2023年度)
|
| 配分額 *注記 |
2,300千円 (直接経費: 2,300千円)
2023年度: 1,100千円 (直接経費: 1,100千円)
2022年度: 1,200千円 (直接経費: 1,200千円)
|
|---|
| キーワード | exact real computation / program verification / higher-order Hoare logic / constructive type theory / formalized mathematics |
|---|
| 研究開始時の研究の概要 |
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.
|
| 研究実績の概要 |
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.
|
