| 研究課題/領域番号 |
22F22071
|
|---|
| 配分区分 | 補助金 |
|---|
| 研究機関 | 京都大学 |
|---|
研究代表者 |
河村 彰星 京都大学, 数理解析研究所, 准教授 (20600117)
|
|---|
| 研究分担者 |
PARK SEWON 京都大学, 数理解析研究所, 外国人特別研究員
|
|---|
| 研究期間 (年度) |
2022-04-22 – 2024-03-31
|
| キーワード | exact real computation / program verification / higher-order Hoare logic / constructive type theory / formalized mathematics |
|---|
| 研究実績の概要 |
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.
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
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.
|
| 今後の研究の推進方策 |
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.
|
